From bd49eb7829fdcf5f3e9379ace9de028411fb9cf9 Mon Sep 17 00:00:00 2001 From: Will Dietz Date: Fri, 17 May 2024 09:19:41 -0500 Subject: [PATCH 1/7] [NFC] Touchup 80-col violations in commments. --- lib/Conversion/LoopScheduleToCalyx/LoopScheduleToCalyx.cpp | 4 ++-- lib/Conversion/SCFToCalyx/SCFToCalyx.cpp | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/Conversion/LoopScheduleToCalyx/LoopScheduleToCalyx.cpp b/lib/Conversion/LoopScheduleToCalyx/LoopScheduleToCalyx.cpp index e9e60d5da8a9..164d187c7b6d 100644 --- a/lib/Conversion/LoopScheduleToCalyx/LoopScheduleToCalyx.cpp +++ b/lib/Conversion/LoopScheduleToCalyx/LoopScheduleToCalyx.cpp @@ -1630,9 +1630,9 @@ void LoopScheduleToCalyxPass::runOnOperation() { return; } - //===----------------------------------------------------------------------===// + //===--------------------------------------------------------------------===// // Cleanup patterns - //===----------------------------------------------------------------------===// + //===--------------------------------------------------------------------===// RewritePatternSet cleanupPatterns(&getContext()); cleanupPatterns.add(&getContext()); diff --git a/lib/Conversion/SCFToCalyx/SCFToCalyx.cpp b/lib/Conversion/SCFToCalyx/SCFToCalyx.cpp index 588185dab5f0..e208a502efc9 100644 --- a/lib/Conversion/SCFToCalyx/SCFToCalyx.cpp +++ b/lib/Conversion/SCFToCalyx/SCFToCalyx.cpp @@ -1831,9 +1831,9 @@ void SCFToCalyxPass::runOnOperation() { return; } - //===----------------------------------------------------------------------===// + //===--------------------------------------------------------------------===// // Cleanup patterns - //===----------------------------------------------------------------------===// + //===--------------------------------------------------------------------===// RewritePatternSet cleanupPatterns(&getContext()); cleanupPatterns.add(&getContext()); From 5b41f2d8f86bd0ad33c3da9cc079233d2d166d60 Mon Sep 17 00:00:00 2001 From: Will Dietz Date: Fri, 17 May 2024 09:21:55 -0500 Subject: [PATCH 2/7] [NFC] tools: remove unused iostream header. --- tools/arcilator/arcilator.cpp | 1 - tools/hlstool/hlstool.cpp | 2 -- tools/ibistool/ibistool.cpp | 2 -- 3 files changed, 5 deletions(-) diff --git a/tools/arcilator/arcilator.cpp b/tools/arcilator/arcilator.cpp index 0b6c43a9a4f4..1348e5a979cf 100644 --- a/tools/arcilator/arcilator.cpp +++ b/tools/arcilator/arcilator.cpp @@ -62,7 +62,6 @@ #include "llvm/Support/TargetSelect.h" #include "llvm/Support/ToolOutputFile.h" -#include #include using namespace mlir; diff --git a/tools/hlstool/hlstool.cpp b/tools/hlstool/hlstool.cpp index c7397ab62e54..a5571c2c954d 100644 --- a/tools/hlstool/hlstool.cpp +++ b/tools/hlstool/hlstool.cpp @@ -57,8 +57,6 @@ #include "circt/Support/Version.h" #include "circt/Transforms/Passes.h" -#include - using namespace llvm; using namespace mlir; using namespace circt; diff --git a/tools/ibistool/ibistool.cpp b/tools/ibistool/ibistool.cpp index 463dcc640102..21d587dd26a0 100644 --- a/tools/ibistool/ibistool.cpp +++ b/tools/ibistool/ibistool.cpp @@ -59,8 +59,6 @@ #include "circt/Support/Version.h" #include "circt/Transforms/Passes.h" -#include - using namespace llvm; using namespace mlir; using namespace circt; From 5e2ad89fda1e040ba29249fd5ac84befb9741da3 Mon Sep 17 00:00:00 2001 From: Will Dietz Date: Fri, 17 May 2024 13:21:10 -0500 Subject: [PATCH 3/7] [FIRRTL][Import] Remove support for printf-encoded verif. (#7030) Retain logic to recognize (but not parse or diagnose) printf's of the various "flavors" previously supported so that we can reject designs that rely on this removed support (emit error). --- lib/Dialect/FIRRTL/Import/FIRAnnotations.h | 7 +- lib/Dialect/FIRRTL/Import/FIRParser.cpp | 38 +- .../FIRRTL/Import/FIRParserAsserts.cpp | 579 +----------------- .../FIRRTL/SFCTests/complex-asserts.fir | 103 +--- .../FIRRTL/SFCTests/complex-assumes.fir | 28 +- test/Dialect/FIRRTL/when-encoded-verif.fir | 91 +-- 6 files changed, 47 insertions(+), 799 deletions(-) diff --git a/lib/Dialect/FIRRTL/Import/FIRAnnotations.h b/lib/Dialect/FIRRTL/Import/FIRAnnotations.h index 2f1232459a94..0639af4c701f 100644 --- a/lib/Dialect/FIRRTL/Import/FIRAnnotations.h +++ b/lib/Dialect/FIRRTL/Import/FIRAnnotations.h @@ -39,10 +39,9 @@ bool fromOMIRJSON(llvm::json::Value &value, SmallVectorImpl &annotations, llvm::json::Path path, MLIRContext *context); -/// Handle verif intent captured in printf + when's. Returns failure if any -/// encountered, otherwise bool indicates whether the printf was encoding verif -/// intent. Mutates the IR, and will delete the PrintFOp when returns true. -FailureOr foldWhenEncodedVerifOp(PrintFOp printOp); +/// Classifier for legacy verif intent captured in printf + when's. Returns +/// true if the printf encodes verif intent, false otherwise. +bool isRecognizedPrintfEncodedVerif(PrintFOp printOp); } // namespace firrtl } // namespace circt diff --git a/lib/Dialect/FIRRTL/Import/FIRParser.cpp b/lib/Dialect/FIRRTL/Import/FIRParser.cpp index 62b3f5f55156..769230514ee5 100644 --- a/lib/Dialect/FIRRTL/Import/FIRParser.cpp +++ b/lib/Dialect/FIRRTL/Import/FIRParser.cpp @@ -5390,38 +5390,30 @@ FIRCircuitParser::parseModuleBody(const SymbolTable &circuitSymTbl, if (failed(result)) return result; - // Convert print-encoded verifications after parsing. - + // Scan for printf-encoded verif's to error on their use, no longer supported. { - // Gather PrintFOps and then process to avoid walking while mutating. - SmallVector buffer; - deferredModule.moduleOp.walk( - [&buffer](PrintFOp printFOp) { buffer.push_back(printFOp); }); - size_t numVerifPrintfs = 0; std::optional printfLoc; - for (auto printFOp : buffer) { - auto loc = printFOp.getLoc(); - auto result = circt::firrtl::foldWhenEncodedVerifOp(printFOp); - if (failed(result)) - return failure(); - if (*result) { - ++numVerifPrintfs; - if (!printfLoc) - printfLoc = loc; - } - } + + deferredModule.moduleOp.walk([&](PrintFOp printFOp) { + if (!circt::firrtl::isRecognizedPrintfEncodedVerif(printFOp)) + return; + ++numVerifPrintfs; + if (!printfLoc) + printfLoc = printFOp.getLoc(); + }); + if (numVerifPrintfs > 0) { auto diag = - mlir::emitWarning(deferredModule.moduleOp.getLoc(), - "module contains ") + mlir::emitError(deferredModule.moduleOp.getLoc(), "module contains ") << numVerifPrintfs - << " printf-encoded verification operation(s), which are deprecated " - "and will be removed in the future"; + << " printf-encoded verification operation(s), which are no longer " + "supported."; diag.attachNote(*printfLoc) - << "example printf here, will just be a printf in the future"; + << "example printf here, this is now just a printf and nothing more"; diag.attachNote() << "For more information, see " "https://github.com/llvm/circt/issues/6970"; + return diag; } } diff --git a/lib/Dialect/FIRRTL/Import/FIRParserAsserts.cpp b/lib/Dialect/FIRRTL/Import/FIRParserAsserts.cpp index d78510a304e3..ccb1c76b4ebc 100644 --- a/lib/Dialect/FIRRTL/Import/FIRParserAsserts.cpp +++ b/lib/Dialect/FIRRTL/Import/FIRParserAsserts.cpp @@ -9,211 +9,23 @@ // This file implements handling of printf-encoded verification operations // embedded in when blocks. // +// While no longer supported, this file retains enough to classify printf +// operations so that we may error on their unsupported use. +// //===----------------------------------------------------------------------===// #include "FIRAnnotations.h" #include "circt/Dialect/FIRRTL/FIRRTLOps.h" #include "circt/Support/LLVM.h" #include "mlir/IR/ImplicitLocOpBuilder.h" -#include "llvm/ADT/APSInt.h" -#include "llvm/ADT/SmallPtrSet.h" #include "llvm/ADT/TypeSwitch.h" -#include "llvm/Support/JSON.h" using namespace circt; using namespace firrtl; -namespace json = llvm::json; - -namespace { -/// Helper class to destructure parsed JSON and emit appropriate error messages. -/// This class should be treated with the same care as a Twine; it should never -/// be assigned to a local variable and should only be passed by constant -/// reference parameters. -template -class ExtractionSummaryCursor { - - // Allow ExtractionSummaryCursor to construct other instances. - template - friend class ExtractionSummaryCursor; - - // This is a friend function since we have no public contructors. - template - friend ParseResult parseJson(Location loc, const T &jsonValue, FnType fn); - - // Private constructor and destructor. - ExtractionSummaryCursor(Location loc, Twine path, JsonType value) - : loc(loc), path(path), value(value) {} - ~ExtractionSummaryCursor() = default; - - // Deleted constructors. - ExtractionSummaryCursor(const ExtractionSummaryCursor &) = delete; - ExtractionSummaryCursor &operator=(const ExtractionSummaryCursor &) = delete; - -public: - Location loc; - Twine path; - JsonType value; - - /// Report an error about the current path. - InFlightDiagnostic emitError() const { - auto diag = mlir::emitError(loc, "extraction summary "); - if (!path.isTriviallyEmpty()) - diag << "field `" << path << "` "; - return diag; - } - - /// Access a field in an object. - ParseResult withField(StringRef field, - llvm::function_ref &)> - fn, - bool optional = false) const { - auto fieldValue = value->get(field); - if (!fieldValue) { - if (optional) - return success(); - emitError() << "missing `" << field << "` field"; - return failure(); - } - return fn({loc, path.isTriviallyEmpty() ? field : path + "." + field, - fieldValue}); - } - - /// Access a JSON value as an object. - ParseResult withObject(llvm::function_ref &)> - fn) const { - auto obj = value->getAsObject(); - if (!obj) { - emitError() << "must be an object"; - return failure(); - } - return fn({loc, path, obj}); - } - - /// Access a JSON value as a string. - ParseResult withString(llvm::function_ref &)> - fn) const { - auto str = value->getAsString(); - if (!str) { - emitError() << "must be a string"; - return failure(); - } - return fn({loc, path, *str}); - } - - /// Access a JSON value as an array. - ParseResult withArray(llvm::function_ref &)> - fn) const { - auto array = value->getAsArray(); - if (!array) { - emitError() << "must be an array"; - return failure(); - } - for (size_t i = 0, e = array->size(); i < e; ++i) - if (fn({loc, path + "[" + Twine(i) + "]", &(*array)[i]})) - return failure(); - return success(); - } - - /// Access an object field as an object. - ParseResult - withObjectField(StringRef field, - llvm::function_ref &)> - fn, - bool optional = false) const { - return withField( - field, [&](const auto &cursor) { return cursor.withObject(fn); }, - optional); - } - - /// Access an object field as a string. - ParseResult withStringField(StringRef field, - llvm::function_ref &)> - fn, - bool optional = false) const { - return withField( - field, [&](const auto &cursor) { return cursor.withString(fn); }, - optional); - } - - /// Access an object field as an array. - ParseResult - withArrayField(StringRef field, - llvm::function_ref &)> - fn, - bool optional = true) const { - return withField( - field, [&](const auto &cursor) { return cursor.withArray(fn); }, - optional); - } -}; - -/// Convenience function to create a `ExtractionSummaryCursor`. -template -ParseResult parseJson(Location loc, const JsonType &jsonValue, FnType fn) { - return fn(ExtractionSummaryCursor{loc, {}, jsonValue}); -} -} // namespace - -/// A flavor of when-printf-encoded verification statement. -enum class VerifFlavor { - VerifLibAssert, // contains "[verif-library-assert]" - VerifLibAssume, // contains "[verif-library-assume]" - VerifLibCover, // contains "[verif-library-cover]" - Assert, // begins with "assert:" - Assume, // begins with "assume:" - Cover, // begins with "cover:" - ChiselAssert, // begins with "Assertion failed" - AssertNotX // begins with "assertNotX:" -}; - -/// A modifier for an assertion predicate. -enum class PredicateModifier { NoMod, TrueOrIsX }; - -/// Parse a conditional compile toggle (e.g. "unrOnly") into the corresponding -/// preprocessor guard macro name (e.g. "USE_UNR_ONLY_CONSTRAINTS"), or report -/// an error. -static std::optional -parseConditionalCompileToggle(const ExtractionSummaryCursor &ex) { - if (ex.value == "formalOnly") - return {"USE_FORMAL_ONLY_CONSTRAINTS"}; - else if (ex.value == "unrOnly") - return {"USE_UNR_ONLY_CONSTRAINTS"}; - ex.emitError() << "must be `formalOnly` or `unrOnly`"; - return std::nullopt; -} - -/// Parse a string into a `PredicateModifier`. -static std::optional -parsePredicateModifier(const ExtractionSummaryCursor &ex) { - if (ex.value == "noMod") - return PredicateModifier::NoMod; - else if (ex.value == "trueOrIsX") - return PredicateModifier::TrueOrIsX; - ex.emitError() << "must be `noMod` or `trueOrIsX`"; - return std::nullopt; -} - -/// Check that an assertion "format" is one of the admissible values, or report -/// an error. -static std::optional -parseAssertionFormat(const ExtractionSummaryCursor &ex) { - if (ex.value == "sva" || ex.value == "ifElseFatal") - return ex.value; - ex.emitError() << "must be `sva` or `ifElseFatal`"; - return std::nullopt; -} - /// Chisel has a tendency to emit complex assert/assume/cover statements encoded /// as print operations with special formatting and metadata embedded in the -/// message literal. These always reside in a when block of the following form: +/// message literal. One variant looks like: /// /// when invCond: /// printf(clock, UInt<1>(1), "...[verif-library-assert]...") @@ -222,8 +34,11 @@ parseAssertionFormat(const ExtractionSummaryCursor &ex) { /// Depending on the nature the verification operation, the `stop` may be /// optional. The Scala implementation simply removes all `stop`s that have the /// same condition as the printf. -FailureOr circt::firrtl::foldWhenEncodedVerifOp(PrintFOp printOp) { - auto *context = printOp.getContext(); +/// +/// This is no longer supported. +/// This method retains enough support to accurately detect when this is used +/// and returns whether this is a recognized (legacy) printf+when-encoded verif. +bool circt::firrtl::isRecognizedPrintfEncodedVerif(PrintFOp printOp) { auto whenStmt = dyn_cast(printOp->getParentOp()); // If the parent of printOp is not when, printOp doesn't encode a @@ -241,382 +56,26 @@ FailureOr circt::firrtl::foldWhenEncodedVerifOp(PrintFOp printOp) { auto opIt = std::next(printOp->getIterator()); auto opEnd = thenBlock.end(); - // Detect if we're dealing with a verification statement, and what flavor of - // statement it is. + // Detect if we're dealing with a verification statement. auto fmt = printOp.getFormatString(); - VerifFlavor flavor; - if (fmt.contains("[verif-library-assert]")) - flavor = VerifFlavor::VerifLibAssert; - else if (fmt.contains("[verif-library-assume]")) - flavor = VerifFlavor::VerifLibAssume; - else if (fmt.contains("[verif-library-cover]")) - flavor = VerifFlavor::VerifLibCover; - else if (fmt.consume_front("assert:")) - flavor = VerifFlavor::Assert; - else if (fmt.consume_front("assume:")) - flavor = VerifFlavor::Assume; - else if (fmt.consume_front("cover:")) - flavor = VerifFlavor::Cover; - else if (fmt.consume_front("assertNotX:")) - flavor = VerifFlavor::AssertNotX; - else if (fmt.starts_with("Assertion failed")) - flavor = VerifFlavor::ChiselAssert; - else + if (!(fmt.contains("[verif-library-assert]") || + fmt.contains("[verif-library-assume]") || + fmt.contains("[verif-library-cover]") || fmt.starts_with("assert:") || + fmt.starts_with("assume:") || fmt.starts_with("cover:") || + fmt.starts_with("assertNotX:") || fmt.starts_with("Assertion failed"))) return false; // optional `stop(clock, enable, ...)` // - // FIXME: Currently, we can't detetct stopOp in the following IR: - // when invCond: - // printf(io.clock, UInt<1>(1), "assert: ..") - // stop(io.clock, UInt<1>(1), 1) - // It is because `io.clock` will create another subfield op so StopOp is not - // the next operation. Also, we will have to modify `stopOp.clock() != - // printOp.clock()` below since they are not CSEd. + // NOTE: This code is retained as-is from when these were fully supported, + // to maintain the classification portion. Previously this code would then + // delete the "stop" operation, which it no longer does. if (opIt != opEnd) { auto stopOp = dyn_cast(*opIt++); if (!stopOp || opIt != opEnd || stopOp.getClock() != printOp.getClock() || stopOp.getCond() != printOp.getCond()) return false; - stopOp.erase(); - } - - // Check if the condition of the `WhenOp` is a trivial inversion operation, - // and remove any immediately preceding verification ops that ensure this - // condition. This caters to the following pattern emitted by Chisel: - // - // assert(clock, cond, enable, ...) - // node N = eq(cond, UInt<1>(0)) - // when N: - // printf(clock, enable, ...) - Value flippedCond = whenStmt.getCondition(); - if (auto node = flippedCond.getDefiningOp()) - flippedCond = node.getInput(); - if (auto notOp = flippedCond.getDefiningOp()) { - flippedCond = notOp.getInput(); - } else if (auto eqOp = flippedCond.getDefiningOp()) { - auto isConst0 = [](Value v) { - if (auto constOp = v.getDefiningOp()) - return constOp.getValue().isZero(); - return false; - }; - if (isConst0(eqOp.getLhs())) - flippedCond = eqOp.getRhs(); - else if (isConst0(eqOp.getRhs())) - flippedCond = eqOp.getLhs(); - else - flippedCond = {}; - } else { - flippedCond = {}; - } - - // If we have found such a condition, erase any verification ops that use it - // and that match the op we are about to assemble. This is necessary since the - // `printf` op actually carries all the information we need for the assert, - // while the actual `assert` has none of it. This makes me sad. - if (flippedCond) { - // Use a set to catch cases where a verification op is a double user of the - // flipped condition. - SmallPtrSet opsToErase; - for (const auto &user : flippedCond.getUsers()) { - TypeSwitch(user).Case( - [&](auto op) { - if (op.getClock() == printOp.getClock() && - op.getEnable() == printOp.getCond() && - op.getPredicate() == flippedCond && !op.getIsConcurrent()) - opsToErase.insert(op); - }); - } - for (auto op : opsToErase) - op->erase(); - } - - // A recursive function to move all the dependency in `printOp` operands. - std::function moveOperationsToParent = [&](Operation *op) { - // If operation is not defined in when, it's ok. - if (!op || op->getBlock() != &whenStmt.getThenBlock()) - return; - - llvm::for_each(op->getOperands(), [&](Value value) { - moveOperationsToParent(value.getDefiningOp()); - }); - - // `op` might be already moved to parent op by the previous recursive calls, - // so check again. - if (op->getBlock() != &whenStmt.getThenBlock()) - return; - - op->moveBefore(whenStmt); - }; - - // Move all operands in printOp to the parent block. - llvm::for_each(printOp->getOperands(), [&](Value value) { - moveOperationsToParent(value.getDefiningOp()); - }); - - ImplicitLocOpBuilder builder(whenStmt.getLoc(), whenStmt); - builder.setInsertionPointAfter(whenStmt); - // CAREFUL: Since the assertions are encoded as "when something wrong, then - // print" an error message, we're actually asserting that something is *not* - // going wrong. - // - // In code: - // - // when somethingGoingWrong: - // printf("oops") - // - // Actually expresses: - // - // assert(not(somethingGoingWrong), "oops") - // - // So you'll find quite a few inversions of the when condition below to - // represent this. - - // TODO: None of the following ops preserve interpolated operands in the - // format string. SV allows this, and we might want to extend the - // `firrtl.{assert,assume,cover}` operations to deal with this. - - switch (flavor) { - // Handle the case of property verification encoded as `:` or - // `: