CIRCT  18.0.0git
FIRParserAsserts.cpp
Go to the documentation of this file.
1 //===- FIRParserAsserts.cpp - Printf-encoded assert handling --------------===//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 //
9 // This file implements handling of printf-encoded verification operations
10 // embedded in when blocks.
11 //
12 //===----------------------------------------------------------------------===//
13 
14 #include "FIRAnnotations.h"
16 #include "circt/Support/LLVM.h"
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"
22 
23 using namespace circt;
24 using namespace firrtl;
25 
26 namespace json = llvm::json;
27 
28 namespace {
29 /// Helper class to destructure parsed JSON and emit appropriate error messages.
30 /// This class should be treated with the same care as a Twine; it should never
31 /// be assigned to a local variable and should only be passed by constant
32 /// reference parameters.
33 template <typename JsonType>
34 class ExtractionSummaryCursor {
35 
36  // Allow ExtractionSummaryCursor to construct other instances.
37  template <typename T>
38  friend class ExtractionSummaryCursor;
39 
40  // This is a friend function since we have no public contructors.
41  template <typename T, typename FnType>
42  friend ParseResult parseJson(Location loc, const T &jsonValue, FnType fn);
43 
44  // Private constructor and destructor.
45  ExtractionSummaryCursor(Location loc, Twine path, JsonType value)
46  : loc(loc), path(path), value(value) {}
47  ~ExtractionSummaryCursor() = default;
48 
49  // Deleted constructors.
50  ExtractionSummaryCursor(const ExtractionSummaryCursor &) = delete;
51  ExtractionSummaryCursor &operator=(const ExtractionSummaryCursor &) = delete;
52 
53 public:
54  Location loc;
55  Twine path;
56  JsonType value;
57 
58  /// Report an error about the current path.
59  InFlightDiagnostic emitError() const {
60  auto diag = mlir::emitError(loc, "extraction summary ");
61  if (!path.isTriviallyEmpty())
62  diag << "field `" << path << "` ";
63  return diag;
64  }
65 
66  /// Access a field in an object.
67  ParseResult withField(StringRef field,
68  llvm::function_ref<ParseResult(
69  const ExtractionSummaryCursor<json::Value *> &)>
70  fn,
71  bool optional = false) const {
72  auto fieldValue = value->get(field);
73  if (!fieldValue) {
74  if (optional)
75  return success();
76  emitError() << "missing `" << field << "` field";
77  return failure();
78  }
79  return fn({loc, path.isTriviallyEmpty() ? field : path + "." + field,
80  fieldValue});
81  }
82 
83  /// Access a JSON value as an object.
84  ParseResult withObject(llvm::function_ref<ParseResult(
85  const ExtractionSummaryCursor<json::Object *> &)>
86  fn) const {
87  auto obj = value->getAsObject();
88  if (!obj) {
89  emitError() << "must be an object";
90  return failure();
91  }
92  return fn({loc, path, obj});
93  }
94 
95  /// Access a JSON value as a string.
96  ParseResult withString(llvm::function_ref<ParseResult(
97  const ExtractionSummaryCursor<StringRef> &)>
98  fn) const {
99  auto str = value->getAsString();
100  if (!str) {
101  emitError() << "must be a string";
102  return failure();
103  }
104  return fn({loc, path, *str});
105  }
106 
107  /// Access a JSON value as an array.
108  ParseResult withArray(llvm::function_ref<ParseResult(
109  const ExtractionSummaryCursor<json::Value *> &)>
110  fn) const {
111  auto array = value->getAsArray();
112  if (!array) {
113  emitError() << "must be an array";
114  return failure();
115  }
116  for (size_t i = 0, e = array->size(); i < e; ++i)
117  if (fn({loc, path + "[" + Twine(i) + "]", &(*array)[i]}))
118  return failure();
119  return success();
120  }
121 
122  /// Access an object field as an object.
123  ParseResult
124  withObjectField(StringRef field,
125  llvm::function_ref<ParseResult(
126  const ExtractionSummaryCursor<json::Object *> &)>
127  fn,
128  bool optional = false) const {
129  return withField(
130  field, [&](const auto &cursor) { return cursor.withObject(fn); },
131  optional);
132  }
133 
134  /// Access an object field as a string.
135  ParseResult withStringField(StringRef field,
136  llvm::function_ref<ParseResult(
137  const ExtractionSummaryCursor<StringRef> &)>
138  fn,
139  bool optional = false) const {
140  return withField(
141  field, [&](const auto &cursor) { return cursor.withString(fn); },
142  optional);
143  }
144 
145  /// Access an object field as an array.
146  ParseResult
147  withArrayField(StringRef field,
148  llvm::function_ref<ParseResult(
149  const ExtractionSummaryCursor<json::Value *> &)>
150  fn,
151  bool optional = true) const {
152  return withField(
153  field, [&](const auto &cursor) { return cursor.withArray(fn); },
154  optional);
155  }
156 };
157 
158 /// Convenience function to create a `ExtractionSummaryCursor`.
159 template <typename JsonType, typename FnType>
160 ParseResult parseJson(Location loc, const JsonType &jsonValue, FnType fn) {
161  return fn(ExtractionSummaryCursor<JsonType>{loc, {}, jsonValue});
162 }
163 } // namespace
164 
165 /// A flavor of when-printf-encoded verification statement.
166 enum class VerifFlavor {
167  VerifLibAssert, // contains "[verif-library-assert]"
168  VerifLibAssume, // contains "[verif-library-assume]"
169  VerifLibCover, // contains "[verif-library-cover]"
170  Assert, // begins with "assert:"
171  Assume, // begins with "assume:"
172  Cover, // begins with "cover:"
173  ChiselAssert, // begins with "Assertion failed"
174  AssertNotX // begins with "assertNotX:"
175 };
176 
177 /// A modifier for an assertion predicate.
179 
180 /// Parse a conditional compile toggle (e.g. "unrOnly") into the corresponding
181 /// preprocessor guard macro name (e.g. "USE_UNR_ONLY_CONSTRAINTS"), or report
182 /// an error.
183 static std::optional<StringRef>
184 parseConditionalCompileToggle(const ExtractionSummaryCursor<StringRef> &ex) {
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`";
190  return std::nullopt;
191 }
192 
193 /// Parse a string into a `PredicateModifier`.
194 static std::optional<PredicateModifier>
195 parsePredicateModifier(const ExtractionSummaryCursor<StringRef> &ex) {
196  if (ex.value == "noMod")
198  else if (ex.value == "trueOrIsX")
200  ex.emitError() << "must be `noMod` or `trueOrIsX`";
201  return std::nullopt;
202 }
203 
204 /// Check that an assertion "format" is one of the admissible values, or report
205 /// an error.
206 static std::optional<StringRef>
207 parseAssertionFormat(const ExtractionSummaryCursor<StringRef> &ex) {
208  if (ex.value == "sva" || ex.value == "ifElseFatal")
209  return ex.value;
210  ex.emitError() << "must be `sva` or `ifElseFatal`";
211  return std::nullopt;
212 }
213 
214 /// Chisel has a tendency to emit complex assert/assume/cover statements encoded
215 /// as print operations with special formatting and metadata embedded in the
216 /// message literal. These always reside in a when block of the following form:
217 ///
218 /// when invCond:
219 /// printf(clock, UInt<1>(1), "...[verif-library-assert]...")
220 /// stop(clock, UInt<1>(1), 1)
221 ///
222 /// Depending on the nature the verification operation, the `stop` may be
223 /// optional. The Scala implementation simply removes all `stop`s that have the
224 /// same condition as the printf.
225 ParseResult circt::firrtl::foldWhenEncodedVerifOp(PrintFOp printOp) {
226  auto *context = printOp.getContext();
227  auto whenStmt = dyn_cast<WhenOp>(printOp->getParentOp());
228 
229  // If the parent of printOp is not when, printOp doesn't encode a
230  // verification.
231  if (!whenStmt)
232  return success();
233 
234  // The when blocks we're interested in don't have an else region.
235  if (whenStmt.hasElseRegion())
236  return success();
237 
238  // The when blocks we're interested in contain a `PrintFOp` and an optional
239  // `StopOp` with the same clock and condition as the print.
240  Block &thenBlock = whenStmt.getThenBlock();
241  auto opIt = std::next(printOp->getIterator());
242  auto opEnd = thenBlock.end();
243 
244  // optional `stop(clock, enable, ...)`
245  //
246  // FIXME: Currently, we can't detetct stopOp in the following IR:
247  // when invCond:
248  // printf(io.clock, UInt<1>(1), "assert: ..")
249  // stop(io.clock, UInt<1>(1), 1)
250  // It is because `io.clock` will create another subfield op so StopOp is not
251  // the next operation. Also, we will have to modify `stopOp.clock() !=
252  // printOp.clock()` below since they are not CSEd.
253  if (opIt != opEnd) {
254  auto stopOp = dyn_cast<StopOp>(*opIt++);
255  if (!stopOp || opIt != opEnd || stopOp.getClock() != printOp.getClock() ||
256  stopOp.getCond() != printOp.getCond())
257  return success();
258  stopOp.erase();
259  }
260 
261  // Detect if we're dealing with a verification statement, and what flavor of
262  // statement it is.
263  auto fmt = printOp.getFormatString();
264  VerifFlavor flavor;
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:"))
272  flavor = VerifFlavor::Assert;
273  else if (fmt.consume_front("assume:"))
274  flavor = VerifFlavor::Assume;
275  else if (fmt.consume_front("cover:"))
276  flavor = VerifFlavor::Cover;
277  else if (fmt.consume_front("assertNotX:"))
278  flavor = VerifFlavor::AssertNotX;
279  else if (fmt.startswith("Assertion failed"))
280  flavor = VerifFlavor::ChiselAssert;
281  else
282  return success();
283 
284  // Check if the condition of the `WhenOp` is a trivial inversion operation,
285  // and remove any immediately preceding verification ops that ensure this
286  // condition. This caters to the following pattern emitted by Chisel:
287  //
288  // assert(clock, cond, enable, ...)
289  // node N = eq(cond, UInt<1>(0))
290  // when N:
291  // printf(clock, enable, ...)
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();
301  return false;
302  };
303  if (isConst0(eqOp.getLhs()))
304  flippedCond = eqOp.getRhs();
305  else if (isConst0(eqOp.getRhs()))
306  flippedCond = eqOp.getLhs();
307  else
308  flippedCond = {};
309  } else {
310  flippedCond = {};
311  }
312 
313  // If we have found such a condition, erase any verification ops that use it
314  // and that match the op we are about to assemble. This is necessary since the
315  // `printf` op actually carries all the information we need for the assert,
316  // while the actual `assert` has none of it. This makes me sad.
317  if (flippedCond) {
318  // Use a set to catch cases where a verification op is a double user of the
319  // flipped condition.
320  SmallPtrSet<Operation *, 1> opsToErase;
321  for (const auto &user : flippedCond.getUsers()) {
322  TypeSwitch<Operation *>(user).Case<AssertOp, AssumeOp, CoverOp>(
323  [&](auto op) {
324  if (op.getClock() == printOp.getClock() &&
325  op.getEnable() == printOp.getCond() &&
326  op.getPredicate() == flippedCond && !op.getIsConcurrent())
327  opsToErase.insert(op);
328  });
329  }
330  for (auto op : opsToErase)
331  op->erase();
332  }
333 
334  // A recursive function to move all the dependency in `printOp` operands.
335  std::function<void(Operation *)> moveOperationsToParent = [&](Operation *op) {
336  // If operation is not defined in when, it's ok.
337  if (!op || op->getBlock() != &whenStmt.getThenBlock())
338  return;
339 
340  llvm::for_each(op->getOperands(), [&](Value value) {
341  moveOperationsToParent(value.getDefiningOp());
342  });
343 
344  // `op` might be already moved to parent op by the previous recursive calls,
345  // so check again.
346  if (op->getBlock() != &whenStmt.getThenBlock())
347  return;
348 
349  op->moveBefore(whenStmt);
350  };
351 
352  // Move all operands in printOp to the parent block.
353  llvm::for_each(printOp->getOperands(), [&](Value value) {
354  moveOperationsToParent(value.getDefiningOp());
355  });
356 
357  ImplicitLocOpBuilder builder(whenStmt.getLoc(), whenStmt);
358  builder.setInsertionPointAfter(whenStmt);
359  // CAREFUL: Since the assertions are encoded as "when something wrong, then
360  // print" an error message, we're actually asserting that something is *not*
361  // going wrong.
362  //
363  // In code:
364  //
365  // when somethingGoingWrong:
366  // printf("oops")
367  //
368  // Actually expresses:
369  //
370  // assert(not(somethingGoingWrong), "oops")
371  //
372  // So you'll find quite a few inversions of the when condition below to
373  // represent this.
374 
375  // TODO: None of the following ops preserve interpolated operands in the
376  // format string. SV allows this, and we might want to extend the
377  // `firrtl.{assert,assume,cover}` operations to deal with this.
378 
379  switch (flavor) {
380  // Handle the case of property verification encoded as `<assert>:<msg>` or
381  // `<assert>:<label>:<msg>`.
382  case VerifFlavor::Assert:
383  case VerifFlavor::Assume:
384  case VerifFlavor::Cover:
386  // Extract label and message from the format string.
387  StringRef label;
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);
393  }
394 
395  // AssertNotX has the special format `assertNotX:%d:msg`, where the `%d`
396  // would theoretically interpolate the value being check for X, but in
397  // practice the Scala impl of ExtractTestCode just discards that `%d` label
398  // and replaces it with `notX`. Also prepare the condition to be checked
399  // here.
400  Value predicate = whenStmt.getCondition();
401  if (flavor != VerifFlavor::Cover)
402  predicate = builder.create<NotPrimOp>(predicate);
403  if (flavor == VerifFlavor::AssertNotX) {
404  label = "notX";
405  if (printOp.getSubstitutions().size() != 1) {
406  printOp.emitError("printf-encoded assertNotX requires one operand");
407  return failure();
408  }
409  // Construct a `!whenCond | (value !== 1'bx)` predicate.
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);
415  }
416 
417  // CAVEAT: The Scala impl of ExtractTestCode explicitly sets `emitSVA` to
418  // false for these flavors of verification operations. I think it's a bad
419  // idea to decide at parse time if something becomes an SVA or a print+fatal
420  // process, so I'm not doing this here. If we ever come across this need, we
421  // may want to annotate the operation with an attribute to indicate that it
422  // wants to explicitly *not* be an SVA.
423 
424  // TODO: Sanitize the label by replacing whitespace with "_" as done in the
425  // Scala impl of ExtractTestCode.
426  ValueRange args;
427  if (printOp.getSubstitutions().size())
428  args = printOp.getSubstitutions().drop_front();
429  if (args.size())
430  printOp.emitWarning()
431  << "printf-encoded assertion has format string arguments which may "
432  "cause lint warnings";
433  if (flavor == VerifFlavor::Assert || flavor == VerifFlavor::AssertNotX)
434  builder.create<AssertOp>(printOp.getClock(), predicate, printOp.getCond(),
435  message, args, label, true);
436  else if (flavor == VerifFlavor::Assume)
437  builder.create<AssumeOp>(printOp.getClock(), predicate, printOp.getCond(),
438  message, args, label, true);
439  else // VerifFlavor::Cover
440  builder.create<CoverOp>(printOp.getClock(), predicate, printOp.getCond(),
441  message, args, label, true);
442  printOp.erase();
443  break;
444  }
445 
446  // Handle the case of builtin Chisel assertions.
448  auto op = builder.create<AssertOp>(
449  printOp.getClock(), builder.create<NotPrimOp>(whenStmt.getCondition()),
450  printOp.getCond(), fmt, printOp.getSubstitutions(), "chisel3_builtin",
451  true);
452  op->setAttr("format", StringAttr::get(context, "ifElseFatal"));
453  printOp.erase();
454  break;
455  }
456 
457  // Handle the SiFive verification library asserts/assumes, which contain
458  // additional configuration attributes for the verification op, serialized
459  // to JSON and embedded in the print message within `<extraction-summary>`
460  // XML tags.
464  // Isolate the JSON text in the `<extraction-summary>` XML tag.
465  StringRef prefix, exStr, suffix;
466  std::tie(prefix, exStr) = fmt.split("<extraction-summary>");
467  std::tie(exStr, suffix) = exStr.split("</extraction-summary>");
468 
469  // The extraction summary is necessary for this kind of assertion, so we
470  // throw an error if it is missing.
471  if (exStr.empty()) {
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";
480  return failure();
481  }
482 
483  // Parse the extraction summary, which contains additional parameters for
484  // the assertion.
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")
489  .attachNote()
490  << a.message();
491  });
492  return failure();
493  }
494 
495  // The extraction summary must be an object.
496  auto exObj = ex->getAsObject();
497  if (!exObj) {
498  printOp.emitError("extraction summary must be a JSON object");
499  return failure();
500  }
501 
502  // Extract and apply any predicate modifier.
503  PredicateModifier predMod;
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)) {
508  predMod = *pm;
509  return success();
510  }
511  return failure();
512  });
513  });
514  }))
515  return failure();
516 
517  Value predicate = whenStmt.getCondition();
518  predicate = builder.create<NotPrimOp>(
519  predicate); // assertion triggers when predicate fails
520  switch (predMod) {
522  // Leave the predicate unmodified.
523  break;
525  // Construct a `predicate | (^predicate === 1'bx)`.
526  Value orX = builder.create<XorRPrimOp>(predicate);
527  orX = builder.create<VerbatimExprOp>(UIntType::get(context, 1),
528  "{{0}} === 1'bx", orX);
529  predicate = builder.create<OrPrimOp>(predicate, orX);
530  break;
531  }
532 
533  // Extract the preprocessor macro names that should guard this assertion.
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) {
540  if (auto guard = parseConditionalCompileToggle(ex)) {
541  guards.push_back(
542  StringAttr::get(builder.getContext(), *guard));
543  return success();
544  }
545  return failure();
546  });
547  });
548  });
549  }))
550  return failure();
551 
552  // Extract label additions and the message.
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);
559  return success();
560  });
561  });
562  }))
563  return failure();
564 
565  StringRef message = fmt;
566  if (parseJson(printOp.getLoc(), exObj, [&](const auto &ex) {
567  return ex.withStringField("baseMsg", [&](const auto &ex) {
568  message = ex.value;
569  return success();
570  });
571  }))
572  return failure();
573 
574  // Assertions carry an additional `format` field.
575  std::optional<StringRef> format;
576  if (flavor == VerifFlavor::VerifLibAssert) {
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)) {
581  format = *f;
582  return success();
583  }
584  return failure();
585  });
586  });
587  }))
588  return failure();
589  }
590 
591  // Build the verification op itself.
592  Operation *op;
593  // TODO: The "ifElseFatal" variant isn't actually a concurrent assertion,
594  // but downstream logic assumes that isConcurrent is set.
595  if (flavor == VerifFlavor::VerifLibAssert)
596  op = builder.create<AssertOp>(printOp.getClock(), predicate,
597  printOp.getCond(), message,
598  printOp.getSubstitutions(), label, true);
599  else if (flavor == VerifFlavor::VerifLibAssume)
600  op = builder.create<AssumeOp>(printOp.getClock(), predicate,
601  printOp.getCond(), message,
602  printOp.getSubstitutions(), label, true);
603  else // VerifFlavor::VerifLibCover
604  op = builder.create<CoverOp>(printOp.getClock(), predicate,
605  printOp.getCond(), message,
606  printOp.getSubstitutions(), label, true);
607  printOp.erase();
608 
609  // Attach additional attributes extracted from the JSON object.
610  op->setAttr("guards", ArrayAttr::get(context, guards));
611  if (format)
612  op->setAttr("format", StringAttr::get(context, *format));
613 
614  break;
615  }
616  }
617 
618  // Clean up the `WhenOp` if it has become completely empty.
619  if (thenBlock.empty())
620  whenStmt.erase();
621  return success();
622 }
lowerAnnotationsNoRefTypePorts FirtoolPreserveValuesMode value
Definition: Firtool.cpp:95
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.
Builder builder
Direction get(bool isOutput)
Returns an output direction if isOutput is true, otherwise returns an input direction.
Definition: CalyxOps.cpp:53
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...
Definition: DebugAnalysis.h:21