17 #include "mlir/IR/ImplicitLocOpBuilder.h"
18 #include "llvm/ADT/APSInt.h"
19 #include "llvm/ADT/SmallPtrSet.h"
20 #include "llvm/ADT/TypeSwitch.h"
21 #include "llvm/Support/JSON.h"
23 using namespace circt;
24 using namespace firrtl;
33 template <
typename JsonType>
34 class ExtractionSummaryCursor {
38 friend class ExtractionSummaryCursor;
41 template <
typename T,
typename FnType>
42 friend ParseResult parseJson(Location loc,
const T &jsonValue, FnType fn);
45 ExtractionSummaryCursor(Location loc, Twine path, JsonType
value)
47 ~ExtractionSummaryCursor() =
default;
50 ExtractionSummaryCursor(
const ExtractionSummaryCursor &) =
delete;
51 ExtractionSummaryCursor &operator=(
const ExtractionSummaryCursor &) =
delete;
59 InFlightDiagnostic emitError()
const {
60 auto diag = mlir::emitError(loc,
"extraction summary ");
61 if (!path.isTriviallyEmpty())
62 diag <<
"field `" << path <<
"` ";
67 ParseResult withField(StringRef field,
68 llvm::function_ref<ParseResult(
69 const ExtractionSummaryCursor<json::Value *> &)>
71 bool optional =
false)
const {
72 auto fieldValue =
value->get(field);
76 emitError() <<
"missing `" << field <<
"` field";
79 return fn({loc, path.isTriviallyEmpty() ? field : path +
"." + field,
84 ParseResult withObject(llvm::function_ref<ParseResult(
85 const ExtractionSummaryCursor<json::Object *> &)>
87 auto obj =
value->getAsObject();
89 emitError() <<
"must be an object";
92 return fn({loc, path, obj});
96 ParseResult withString(llvm::function_ref<ParseResult(
97 const ExtractionSummaryCursor<StringRef> &)>
99 auto str =
value->getAsString();
101 emitError() <<
"must be a string";
104 return fn({loc, path, *str});
108 ParseResult withArray(llvm::function_ref<ParseResult(
109 const ExtractionSummaryCursor<json::Value *> &)>
111 auto array =
value->getAsArray();
113 emitError() <<
"must be an array";
116 for (
size_t i = 0, e = array->size(); i < e; ++i)
117 if (fn({loc, path +
"[" + Twine(i) +
"]", &(*array)[i]}))
124 withObjectField(StringRef field,
125 llvm::function_ref<ParseResult(
126 const ExtractionSummaryCursor<json::Object *> &)>
128 bool optional =
false)
const {
130 field, [&](
const auto &cursor) {
return cursor.withObject(fn); },
135 ParseResult withStringField(StringRef field,
136 llvm::function_ref<ParseResult(
137 const ExtractionSummaryCursor<StringRef> &)>
139 bool optional =
false)
const {
141 field, [&](
const auto &cursor) {
return cursor.withString(fn); },
147 withArrayField(StringRef field,
148 llvm::function_ref<ParseResult(
149 const ExtractionSummaryCursor<json::Value *> &)>
151 bool optional =
true)
const {
153 field, [&](
const auto &cursor) {
return cursor.withArray(fn); },
159 template <
typename JsonType,
typename FnType>
160 ParseResult parseJson(Location loc,
const JsonType &jsonValue, FnType fn) {
161 return fn(ExtractionSummaryCursor<JsonType>{loc, {}, jsonValue});
183 static std::optional<StringRef>
185 if (ex.value ==
"formalOnly")
186 return {
"USE_FORMAL_ONLY_CONSTRAINTS"};
187 else if (ex.value ==
"unrOnly")
188 return {
"USE_UNR_ONLY_CONSTRAINTS"};
189 ex.emitError() <<
"must be `formalOnly` or `unrOnly`";
194 static std::optional<PredicateModifier>
196 if (ex.value ==
"noMod")
198 else if (ex.value ==
"trueOrIsX")
200 ex.emitError() <<
"must be `noMod` or `trueOrIsX`";
206 static std::optional<StringRef>
208 if (ex.value ==
"sva" || ex.value ==
"ifElseFatal")
210 ex.emitError() <<
"must be `sva` or `ifElseFatal`";
226 auto *context = printOp.getContext();
227 auto whenStmt = dyn_cast<WhenOp>(printOp->getParentOp());
235 if (whenStmt.hasElseRegion())
240 Block &thenBlock = whenStmt.getThenBlock();
241 auto opIt = std::next(printOp->getIterator());
242 auto opEnd = thenBlock.end();
254 auto stopOp = dyn_cast<StopOp>(*opIt++);
255 if (!stopOp || opIt != opEnd || stopOp.getClock() != printOp.getClock() ||
256 stopOp.getCond() != printOp.getCond())
263 auto fmt = printOp.getFormatString();
265 if (fmt.contains(
"[verif-library-assert]"))
267 else if (fmt.contains(
"[verif-library-assume]"))
269 else if (fmt.contains(
"[verif-library-cover]"))
271 else if (fmt.consume_front(
"assert:"))
273 else if (fmt.consume_front(
"assume:"))
275 else if (fmt.consume_front(
"cover:"))
277 else if (fmt.consume_front(
"assertNotX:"))
279 else if (fmt.startswith(
"Assertion failed"))
292 Value flippedCond = whenStmt.getCondition();
293 if (
auto node = flippedCond.getDefiningOp<NodeOp>())
294 flippedCond = node.getInput();
295 if (
auto notOp = flippedCond.getDefiningOp<NotPrimOp>()) {
296 flippedCond = notOp.getInput();
297 }
else if (
auto eqOp = flippedCond.getDefiningOp<EQPrimOp>()) {
298 auto isConst0 = [](Value v) {
299 if (
auto constOp = v.getDefiningOp<ConstantOp>())
300 return constOp.getValue().isZero();
303 if (isConst0(eqOp.getLhs()))
304 flippedCond = eqOp.getRhs();
305 else if (isConst0(eqOp.getRhs()))
306 flippedCond = eqOp.getLhs();
320 SmallPtrSet<Operation *, 1> opsToErase;
321 for (
const auto &user : flippedCond.getUsers()) {
322 TypeSwitch<Operation *>(user).Case<AssertOp, AssumeOp, CoverOp>(
324 if (op.getClock() == printOp.getClock() &&
325 op.getEnable() == printOp.getCond() &&
326 op.getPredicate() == flippedCond && !op.getIsConcurrent())
327 opsToErase.insert(op);
330 for (
auto op : opsToErase)
335 std::function<void(Operation *)> moveOperationsToParent = [&](Operation *op) {
337 if (!op || op->getBlock() != &whenStmt.getThenBlock())
340 llvm::for_each(op->getOperands(), [&](Value
value) {
341 moveOperationsToParent(value.getDefiningOp());
346 if (op->getBlock() != &whenStmt.getThenBlock())
349 op->moveBefore(whenStmt);
353 llvm::for_each(printOp->getOperands(), [&](Value
value) {
354 moveOperationsToParent(value.getDefiningOp());
357 ImplicitLocOpBuilder
builder(whenStmt.getLoc(), whenStmt);
358 builder.setInsertionPointAfter(whenStmt);
388 StringRef message = fmt;
389 auto index = fmt.find(
':');
390 if (index != StringRef::npos) {
391 label = fmt.slice(0, index);
392 message = fmt.slice(index + 1, StringRef::npos);
400 Value predicate = whenStmt.getCondition();
402 predicate =
builder.create<NotPrimOp>(predicate);
405 if (printOp.getSubstitutions().size() != 1) {
406 printOp.emitError(
"printf-encoded assertNotX requires one operand");
410 Value notCond = predicate;
411 predicate =
builder.create<XorRPrimOp>(printOp.getSubstitutions()[0]);
412 predicate =
builder.create<IsXIntrinsicOp>(predicate);
413 predicate =
builder.create<NotPrimOp>(predicate);
414 predicate =
builder.create<OrPrimOp>(notCond, predicate);
427 if (printOp.getSubstitutions().size())
428 args = printOp.getSubstitutions().drop_front();
430 printOp.emitWarning()
431 <<
"printf-encoded assertion has format string arguments which may "
432 "cause lint warnings";
434 builder.create<AssertOp>(printOp.getClock(), predicate, printOp.getCond(),
435 message, args, label,
true);
437 builder.create<AssumeOp>(printOp.getClock(), predicate, printOp.getCond(),
438 message, args, label,
true);
440 builder.create<CoverOp>(printOp.getClock(), predicate, printOp.getCond(),
441 message, args, label,
true);
448 auto op =
builder.create<AssertOp>(
449 printOp.getClock(),
builder.create<NotPrimOp>(whenStmt.getCondition()),
450 printOp.getCond(), fmt, printOp.getSubstitutions(),
"chisel3_builtin",
465 StringRef prefix, exStr, suffix;
466 std::tie(prefix, exStr) = fmt.split(
"<extraction-summary>");
467 std::tie(exStr, suffix) = exStr.split(
"</extraction-summary>");
472 auto diag = printOp.emitError(
473 "printf-encoded assert/assume requires extraction summary");
474 diag.attachNote(printOp.getLoc())
475 <<
"because printf message contains "
476 "`[verif-library-{assert,assume,cover}]` tag";
477 diag.attachNote(printOp.getLoc())
478 <<
"expected JSON-encoded extraction summary in "
479 "`<extraction-summary>` XML tag";
485 auto ex = json::parse(exStr);
486 if (
auto err = ex.takeError()) {
487 handleAllErrors(std::move(err), [&](
const json::ParseError &a) {
488 printOp.emitError(
"failed to parse JSON extraction summary")
496 auto exObj = ex->getAsObject();
498 printOp.emitError(
"extraction summary must be a JSON object");
504 if (parseJson(printOp.getLoc(), exObj, [&](
const auto &ex) {
505 return ex.withObjectField(
"predicateModifier", [&](const auto &ex) {
506 return ex.withStringField(
"type", [&](const auto &ex) {
507 if (auto pm = parsePredicateModifier(ex)) {
517 Value predicate = whenStmt.getCondition();
518 predicate =
builder.create<NotPrimOp>(
526 Value orX =
builder.create<XorRPrimOp>(predicate);
528 "{{0}} === 1'bx", orX);
529 predicate =
builder.create<OrPrimOp>(predicate, orX);
534 SmallVector<Attribute> guards;
535 if (parseJson(printOp.getLoc(), exObj, [&](
const auto &ex) {
536 return ex.withArrayField(
537 "conditionalCompileToggles", [&](
const auto &ex) {
538 return ex.withObject([&](
const auto &ex) {
539 return ex.withStringField(
"type", [&](
const auto &ex) {
553 SmallString<32> label(
"verif_library");
554 if (parseJson(printOp.getLoc(), exObj, [&](
const auto &ex) {
555 return ex.withArrayField(
"labelExts", [&](const auto &ex) {
556 return ex.withString([&](const auto &ex) {
557 label.push_back(
'_');
558 label.append(ex.value);
565 StringRef message = fmt;
566 if (parseJson(printOp.getLoc(), exObj, [&](
const auto &ex) {
567 return ex.withStringField(
"baseMsg", [&](const auto &ex) {
575 std::optional<StringRef> format;
577 if (parseJson(printOp.getLoc(), exObj, [&](
const auto &ex) {
578 return ex.withObjectField(
"format", [&](const auto &ex) {
579 return ex.withStringField(
"type", [&](const auto &ex) {
580 if (auto f = parseAssertionFormat(ex)) {
596 op =
builder.create<AssertOp>(printOp.getClock(), predicate,
597 printOp.getCond(), message,
598 printOp.getSubstitutions(), label,
true);
600 op =
builder.create<AssumeOp>(printOp.getClock(), predicate,
601 printOp.getCond(), message,
602 printOp.getSubstitutions(), label,
true);
604 op =
builder.create<CoverOp>(printOp.getClock(), predicate,
605 printOp.getCond(), message,
606 printOp.getSubstitutions(), label,
true);
619 if (thenBlock.empty())
static std::optional< PredicateModifier > parsePredicateModifier(const ExtractionSummaryCursor< StringRef > &ex)
Parse a string into a PredicateModifier.
static std::optional< StringRef > parseAssertionFormat(const ExtractionSummaryCursor< StringRef > &ex)
Check that an assertion "format" is one of the admissible values, or report an error.
PredicateModifier
A modifier for an assertion predicate.
static std::optional< StringRef > parseConditionalCompileToggle(const ExtractionSummaryCursor< StringRef > &ex)
Parse a conditional compile toggle (e.g.
VerifFlavor
A flavor of when-printf-encoded verification statement.
Direction get(bool isOutput)
Returns an output direction if isOutput is true, otherwise returns an input direction.
ParseResult foldWhenEncodedVerifOp(PrintFOp printOp)
Chisel has a tendency to emit complex assert/assume/cover statements encoded as print operations with...
This file defines an intermediate representation for circuits acting as an abstraction for constraint...