From ef30e1f20a2a09985370c71aa6972d24bffeca4f Mon Sep 17 00:00:00 2001 From: Amelia Dobis Date: Thu, 20 Jun 2024 11:24:37 -0700 Subject: [PATCH] [FIRRTL][Verif][LTL] Replace `ltl.disable` with an enable folded into `verif.assert` (#7150) This PR gets rid of the `ltl.disable` op and intrinsic in favor of having an enable operand on the verif assert like ops. This made it trivial to fix an incorrect when condition folding for `AssertProperty`. Most of the PR relates to fixing the chaos that was caused by removing `ltl.disable`. --- .../circt/Dialect/FIRRTL/FIRRTLExpressions.td | 1 - .../circt/Dialect/FIRRTL/FIRRTLIntrinsics.h | 3 +- .../circt/Dialect/FIRRTL/FIRRTLStatements.td | 2 +- include/circt/Dialect/FIRRTL/FIRRTLVisitors.h | 6 +- include/circt/Dialect/LTL/LTLOps.td | 82 +----- include/circt/Dialect/LTL/LTLVisitors.h | 3 +- include/circt/Dialect/Verif/VerifOps.td | 16 +- .../ExportVerilog/ExportVerilog.cpp | 106 ++++---- lib/Conversion/FIRRTLToHW/LowerToHW.cpp | 26 +- lib/Conversion/HWToBTOR2/HWToBTOR2.cpp | 245 ++++++++++++------ lib/Conversion/LTLToCore/LTLToCore.cpp | 125 +-------- lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp | 32 ++- lib/Dialect/FIRRTL/Transforms/ExpandWhens.cpp | 32 ++- lib/Dialect/LTL/LTLFolds.cpp | 12 - lib/Dialect/Verif/Transforms/CMakeLists.txt | 1 + .../Transforms/VerifyClockedAssertLike.cpp | 9 +- lib/Dialect/Verif/VerifOps.cpp | 49 ++++ .../ExportVerilog/prepare-for-emission.mlir | 22 +- test/Conversion/ExportVerilog/verif.mlir | 55 ++-- test/Conversion/FIRRTLToHW/intrinsics.mlir | 3 - test/Conversion/HWToBTOR2/init.mlir | 5 +- test/Conversion/LTLToCore/assertproperty.mlir | 36 +-- test/Dialect/FIRRTL/expand-whens.mlir | 89 ++++--- test/Dialect/FIRRTL/lower-intrinsics.mlir | 2 - test/Dialect/LTL/basic.mlir | 2 - test/Dialect/LTL/canonicalization.mlir | 10 - test/Dialect/Verif/canonicalization.mlir | 21 ++ test/Dialect/Verif/verify.mlir | 38 +-- test/firtool/btor2-assertproperty.fir | 44 ++-- test/firtool/extract-test-code.fir | 9 +- 30 files changed, 499 insertions(+), 587 deletions(-) diff --git a/include/circt/Dialect/FIRRTL/FIRRTLExpressions.td b/include/circt/Dialect/FIRRTL/FIRRTLExpressions.td index c430a649dc..f435e86ef7 100644 --- a/include/circt/Dialect/FIRRTL/FIRRTLExpressions.td +++ b/include/circt/Dialect/FIRRTL/FIRRTLExpressions.td @@ -1474,6 +1474,5 @@ def LTLClockIntrinsicOp : LTLIntrinsicOp<"clock"> { $input `,` $clock attr-dict `:` functional-type(operands, results) }]; } -def LTLDisableIntrinsicOp : BinaryLTLIntrinsicOp<"disable">; #endif // CIRCT_DIALECT_FIRRTL_FIRRTLEXPRESSIONS_TD diff --git a/include/circt/Dialect/FIRRTL/FIRRTLIntrinsics.h b/include/circt/Dialect/FIRRTL/FIRRTLIntrinsics.h index d604e6f79e..0cf27ce231 100644 --- a/include/circt/Dialect/FIRRTL/FIRRTLIntrinsics.h +++ b/include/circt/Dialect/FIRRTL/FIRRTLIntrinsics.h @@ -34,7 +34,8 @@ struct GenericIntrinsic { // Input checking //===--------------------------------------------------------------------===// - ParseResult hasNInputs(unsigned n); + ParseResult hasNInputs(unsigned n, unsigned c); + unsigned getNumInputs(); template ParseResult checkInputType(unsigned n, const Twine &msg, C &&call) { diff --git a/include/circt/Dialect/FIRRTL/FIRRTLStatements.td b/include/circt/Dialect/FIRRTL/FIRRTLStatements.td index 66e5b7f381..649801ad03 100644 --- a/include/circt/Dialect/FIRRTL/FIRRTLStatements.td +++ b/include/circt/Dialect/FIRRTL/FIRRTLStatements.td @@ -357,7 +357,7 @@ class VerifIntrinsicOp traits = []> : FIRRTLOp<"int.verif." # mnemonic, traits> { let summary = "FIRRTL variant of `verif." # mnemonic # "`"; let description = "See `verif." # mnemonic # "` op in the Verif dialect."; - let arguments = (ins UInt1Type:$property, OptionalAttr:$label); + let arguments = (ins UInt1Type:$property, Optional:$enable, OptionalAttr:$label); let assemblyFormat = [{ operands attr-dict `:` type(operands) }]; diff --git a/include/circt/Dialect/FIRRTL/FIRRTLVisitors.h b/include/circt/Dialect/FIRRTL/FIRRTLVisitors.h index 5289cd9bba..03a2466d2b 100644 --- a/include/circt/Dialect/FIRRTL/FIRRTLVisitors.h +++ b/include/circt/Dialect/FIRRTL/FIRRTLVisitors.h @@ -55,9 +55,8 @@ public: LTLRepeatIntrinsicOp, LTLGoToRepeatIntrinsicOp, LTLNonConsecutiveRepeatIntrinsicOp, LTLNotIntrinsicOp, LTLImplicationIntrinsicOp, LTLUntilIntrinsicOp, - LTLEventuallyIntrinsicOp, LTLClockIntrinsicOp, - LTLDisableIntrinsicOp, Mux2CellIntrinsicOp, Mux4CellIntrinsicOp, - HasBeenResetIntrinsicOp, + LTLEventuallyIntrinsicOp, LTLClockIntrinsicOp, Mux2CellIntrinsicOp, + Mux4CellIntrinsicOp, HasBeenResetIntrinsicOp, // Miscellaneous. BitsPrimOp, HeadPrimOp, MuxPrimOp, PadPrimOp, ShlPrimOp, ShrPrimOp, TailPrimOp, VerbatimExprOp, HWStructCastOp, BitCastOp, RefSendOp, @@ -186,7 +185,6 @@ public: HANDLE(LTLUntilIntrinsicOp, Unhandled); HANDLE(LTLEventuallyIntrinsicOp, Unhandled); HANDLE(LTLClockIntrinsicOp, Unhandled); - HANDLE(LTLDisableIntrinsicOp, Unhandled); HANDLE(Mux4CellIntrinsicOp, Unhandled); HANDLE(Mux2CellIntrinsicOp, Unhandled); HANDLE(HasBeenResetIntrinsicOp, Unhandled); diff --git a/include/circt/Dialect/LTL/LTLOps.td b/include/circt/Dialect/LTL/LTLOps.td index 743ab51d6e..1938a7f3b2 100644 --- a/include/circt/Dialect/LTL/LTLOps.td +++ b/include/circt/Dialect/LTL/LTLOps.td @@ -160,10 +160,7 @@ def ConcatOp : LTLOp<"concat", [Pure]> { }]; } -def RepeatOp : LTLOp<"repeat", [ - Pure, - PredOpTrait<"'base' must be >= 0", CPred<"$base >= 0">> -]> { +def RepeatOp : LTLOp<"repeat", [Pure]> { let arguments = (ins LTLAnySequenceType:$input, I64Attr:$base, @@ -188,11 +185,7 @@ def RepeatOp : LTLOp<"repeat", [ }]; } -def GoToRepeatOp : LTLOp<"goto_repeat", [ - Pure, - PredOpTrait<"'base' must be >= 0", CPred<"$base >= 0">>, - PredOpTrait<"'more' must be >= 0", CPred<"$more >= 0">> -]> { +def GoToRepeatOp : LTLOp<"goto_repeat", [Pure]> { let arguments = (ins LTLAnySequenceType:$input, I64Attr:$base, @@ -214,11 +207,7 @@ def GoToRepeatOp : LTLOp<"goto_repeat", [ }]; } -def NonConsecutiveRepeatOp : LTLOp<"non_consecutive_repeat", [ - Pure, - PredOpTrait<"'base' must be >= 0", CPred<"$base >= 0">>, - PredOpTrait<"'more' must be >= 0", CPred<"$more >= 0">> -]> { +def NonConsecutiveRepeatOp : LTLOp<"non_consecutive_repeat", [Pure]> { let arguments = (ins LTLAnySequenceType:$input, I64Attr:$base, @@ -356,69 +345,4 @@ def ClockOp : LTLOp<"clock", [ }]; } -def DisableOp : LTLOp<"disable", [Pure]> { - let arguments = (ins LTLAnyPropertyType:$input, I1:$condition); - let results = (outs LTLPropertyType:$result); - let assemblyFormat = [{ - $input `if` $condition attr-dict `:` type($input) - }]; - let hasFolder = 1; - - let summary = "Disable the evaluation of a property based on a condition."; - let description = [{ - Creates a new property which evaluates the given `$input` property only if - the given disable `$condition` is false throughout the entire evaluation. If - the `$condition` is true at any point in time during the evaluation of - `$input`, the resulting property is disabled. - - The disabling is "infectious". If a property is disabled, it also implicitly - disables all properties that use it. Consider the following example: - ``` - %0 = ltl.disable %prop if %cond - %1 = ltl.or %0, %otherProp - ``` - If the property `%0` is disabled, the derived property `%1` is also - disabled. - - As a result, it is always legal to canonicalize the IR into a form where - there is only one `ltl.disable` operation at the root of a property - expression. - - Note that a property being disabled based on a condition is different from a - property that trivially evaluates to true if the condition does not hold. - The former ensures that a property is only checked when a certain condition - is true, but the number of cases in which the property holds or doesn't hold - remains unchanged. The latter adds additional cases where the property - holds, which can offer a solver unintended ways to make assertions or - coverage proofs derived from the property pass. For example: - - ``` - %p0 = ltl.or %prop, %cond - %p1 = ltl.disable %prop if %cond - ``` - - `$cond` being true would disable the evaluation of `%p0` and would make - `%p1` evaluate to true. These are subtly different. If used in an assertion - during simulation, `$cond` would adequately disable triggering of the - assertion in both cases. However, if used in a formal verification setting - where proofs for `%p0` and `%p1` always holding or never holding are sought, - a solver might use `%cond = true` to trivially make `%p0` hold, which is not - possible for `%p1`. Consider the following more concrete example: - - ``` - %p2 = ltl.or %protocolCorrectProperty, %reset - %p3 = ltl.disable %protocolCorrectProperty if %reset - verif.cover %p2 - verif.cover %p3 - ``` - - The intent is to formally prove coverage for `%protocolCorrectProperty` - while the circuit is in regular operation (i.e., out of reset). A formal - solver would trivially prove coverage for `%p2` by assigning - `%reset = true`, but would have to actually prove coverage for the - underlying `%protocolCorrectProperty` for `%p3`. The latter is almost always - the intended behavior. - }]; -} - #endif // CIRCT_DIALECT_LTL_LTLOPS_TD diff --git a/include/circt/Dialect/LTL/LTLVisitors.h b/include/circt/Dialect/LTL/LTLVisitors.h index ae365a8463..b5f673195d 100644 --- a/include/circt/Dialect/LTL/LTLVisitors.h +++ b/include/circt/Dialect/LTL/LTLVisitors.h @@ -22,7 +22,7 @@ public: auto *thisCast = static_cast(this); return TypeSwitch(op) .template Case( [&](auto op) -> ResultType { return thisCast->visitLTL(op, args...); @@ -59,7 +59,6 @@ public: HANDLE(UntilOp, Unhandled); HANDLE(EventuallyOp, Unhandled); HANDLE(ClockOp, Unhandled); - HANDLE(DisableOp, Unhandled); HANDLE(IntersectOp, Unhandled); HANDLE(NonConsecutiveRepeatOp, Unhandled); HANDLE(GoToRepeatOp, Unhandled); diff --git a/include/circt/Dialect/Verif/VerifOps.td b/include/circt/Dialect/Verif/VerifOps.td index fd101e964b..9e202b2513 100644 --- a/include/circt/Dialect/Verif/VerifOps.td +++ b/include/circt/Dialect/Verif/VerifOps.td @@ -28,11 +28,13 @@ class VerifOp traits = []> : class AssertLikeOp traits = []> : VerifOp { - let arguments = (ins LTLAnyPropertyType:$property, + let arguments = (ins LTLAnyPropertyType:$property, Optional:$enable, OptionalAttr:$label); let assemblyFormat = [{ - $property (`label` $label^)? attr-dict `:` type($property) + $property (`if` $enable^)? (`label` $label^)? attr-dict `:` type($property) }]; + + let hasCanonicalizeMethod = true; } def AssertOp : AssertLikeOp<"assert"> { @@ -64,11 +66,11 @@ def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge", class ClockedAssertLikeOp traits = []> : VerifOp { let arguments = (ins LTLAnyPropertyType:$property, - I1:$disable, ClockEdgeAttr:$edge, I1:$clock, + Optional:$enable, OptionalAttr:$label); let assemblyFormat = [{ - $property `disable` $disable `clock` $edge $clock + $property (`if` $enable^)? `,` $edge $clock (`label` $label^)? attr-dict `:` type($property) }]; } @@ -76,7 +78,7 @@ class ClockedAssertLikeOp traits = []> : def ClockedAssertOp : ClockedAssertLikeOp<"clocked_assert"> { let summary = [{ Assert that a property holds, checked on a given clock's - ticks and disabled if a given condition holds. Only supports + ticks and enabled if a given condition holds. Only supports a single clock and a single disable. }]; } @@ -84,7 +86,7 @@ def ClockedAssertOp : ClockedAssertLikeOp<"clocked_assert"> { def ClockedAssumeOp : ClockedAssertLikeOp<"clocked_assume"> { let summary = [{ Assume that a property holds, checked on a given clock's - ticks and disabled if a given condition holds. Only supports + ticks and enabled if a given condition holds. Only supports a single clock and a single disable. }]; } @@ -92,7 +94,7 @@ def ClockedAssumeOp : ClockedAssertLikeOp<"clocked_assume"> { def ClockedCoverOp : ClockedAssertLikeOp<"clocked_cover"> { let summary = [{ Cover on the holding of a property, checked on a given clock's - ticks and disabled if a given condition holds. Only supports + ticks and enabled if a given condition holds. Only supports a single clock and a single disable. }]; } diff --git a/lib/Conversion/ExportVerilog/ExportVerilog.cpp b/lib/Conversion/ExportVerilog/ExportVerilog.cpp index 3135a29391..896294d625 100644 --- a/lib/Conversion/ExportVerilog/ExportVerilog.cpp +++ b/lib/Conversion/ExportVerilog/ExportVerilog.cpp @@ -779,9 +779,6 @@ static bool isExpressionUnableToInline(Operation *op, // Helper to determine if the use will be part of "event control", // based on what the operation using it is and as which operand. auto usedInExprControl = [user, &use]() { - // "disable iff" condition must be a name. - if (auto disableOp = dyn_cast(user)) - return disableOp.getCondition() == use.get(); // LTL Clock up's clock operand must be a name. if (auto clockOp = dyn_cast(user)) return clockOp.getClock() == use.get(); @@ -3453,15 +3450,15 @@ public: assert(state.pp.getListener() == &state.saver); } - /// Emit the specified value as an SVA property or sequence. This is the entry - /// point to print an entire tree of property or sequence expressions in one - /// go. - void emitProperty( - Value property, + /// Emit the specified value as an SVA property or sequence with an enable + /// signal. This is the entry point to print an entire tree of property or + /// sequence expressions in one go. + void emitEnabledProperty( + Value property, Value enable, PropertyPrecedence parenthesizeIfLooserThan = PropertyPrecedence::Lowest); // Emits a property that is directly associated to a single clock and a single - // disable. Note that it is illegal to nest disable or clock operations in the + // enable. Note that it is illegal to nest clock operations in the // property itself here. void emitClockedProperty( Value property, Value clock, ltl::ClockEdge edge, Value disable, @@ -3490,7 +3487,6 @@ private: EmittedProperty visitLTL(ltl::UntilOp op); EmittedProperty visitLTL(ltl::EventuallyOp op); EmittedProperty visitLTL(ltl::ClockOp op); - EmittedProperty visitLTL(ltl::DisableOp op); void emitLTLConcat(ValueRange inputs); @@ -3513,10 +3509,20 @@ private: }; } // end anonymous namespace -void PropertyEmitter::emitProperty( - Value property, PropertyPrecedence parenthesizeIfLooserThan) { +void PropertyEmitter::emitEnabledProperty( + Value property, Value enable, PropertyPrecedence parenthesizeIfLooserThan) { assert(localTokens.empty()); - // Wrap to this column. + + // If the property is tied to an enable, emit that. + if (enable) { + ps << "disable iff" << PP::nbsp << "(~("; + ps.scopedBox(PP::ibox2, [&] { + emitNestedProperty(enable, PropertyPrecedence::Unary); + ps << "))"; + }); + ps << PP::space; + } + ps.scopedBox(PP::ibox0, [&] { emitNestedProperty(property, parenthesizeIfLooserThan); }); // If we are not using an external token buffer provided through the @@ -3527,7 +3533,7 @@ void PropertyEmitter::emitProperty( } void PropertyEmitter::emitClockedProperty( - Value property, Value clock, ltl::ClockEdge edge, Value disable, + Value property, Value clock, ltl::ClockEdge edge, Value enable, PropertyPrecedence parenthesizeIfLooserThan) { assert(localTokens.empty()); // Wrap to this column. @@ -3538,12 +3544,15 @@ void PropertyEmitter::emitClockedProperty( ps << ")"; }); - ps << PP::space; - ps << "disable iff" << PP::nbsp << "("; - ps.scopedBox(PP::ibox2, [&] { - emitNestedProperty(disable, PropertyPrecedence::Lowest); - ps << ")"; - }); + // If the property is tied to an enable, emit that. + if (enable) { + ps << PP::space; + ps << "disable iff" << PP::nbsp << "(~("; + ps.scopedBox(PP::ibox2, [&] { + emitNestedProperty(enable, PropertyPrecedence::Lowest); + ps << "))"; + }); + } ps << PP::space; ps.scopedBox(PP::ibox0, @@ -3786,17 +3795,6 @@ EmittedProperty PropertyEmitter::visitLTL(ltl::ClockOp op) { return {PropertyPrecedence::Clocking}; } -EmittedProperty PropertyEmitter::visitLTL(ltl::DisableOp op) { - ps << "disable iff" << PP::nbsp << "("; - ps.scopedBox(PP::ibox2, [&] { - emitNestedProperty(op.getCondition(), PropertyPrecedence::Lowest); - ps << ")"; - }); - ps << PP::space; - emitNestedProperty(op.getInput(), PropertyPrecedence::Clocking); - return {PropertyPrecedence::Clocking}; -} - // NOLINTEND(misc-no-recursion) //===----------------------------------------------------------------------===// @@ -4010,16 +4008,15 @@ private: const SmallPtrSetImpl &locationOps, StringRef multiLineComment = StringRef()); - LogicalResult emitVerifAssertLike(Operation *op, Value property, + LogicalResult emitVerifAssertLike(Operation *op, Value property, Value enable, PPExtString opName); LogicalResult visitVerif(verif::AssertOp op); LogicalResult visitVerif(verif::AssumeOp op); LogicalResult visitVerif(verif::CoverOp op); LogicalResult emitVerifClockedAssertLike(Operation *op, Value property, - Value disable, Value clock, - verif::ClockEdge edge, - PPExtString opName); + Value clock, verif::ClockEdge edge, + Value enable, PPExtString opName); LogicalResult visitVerif(verif::ClockedAssertOp op); LogicalResult visitVerif(verif::ClockedAssumeOp op); LogicalResult visitVerif(verif::ClockedCoverOp op); @@ -4887,6 +4884,7 @@ LogicalResult StmtEmitter::visitSV(CoverConcurrentOp op) { /// Emit an assert-like operation from the `verif` dialect. This covers /// `verif.assert`, `verif.assume`, and `verif.cover`. LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property, + Value enable, PPExtString opName) { if (hasSVAttributes(op)) emitError(op, "SV attributes emission is unimplemented for the op"); @@ -4899,8 +4897,9 @@ LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property, // See IEEE 1800-2017 section 16.14.5 "Using concurrent assertion statements // outside procedural code" and 16.14.6 "Embedding concurrent assertions in // procedural code". + Operation *parent = op->getParentOp(); bool isTemporal = !property.getType().isSignlessInteger(1); - bool isProcedural = op->getParentOp()->hasTrait(); + bool isProcedural = parent->hasTrait(); bool emitAsImmediate = !isTemporal && isProcedural; startStatement(); @@ -4915,7 +4914,7 @@ LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property, else ps << opName << PP::nbsp << "property" << PP::nbsp << "("; ps.scopedBox(PP::ibox2, [&]() { - PropertyEmitter(emitter, ops).emitProperty(property); + PropertyEmitter(emitter, ops).emitEnabledProperty(property, enable); ps << ");"; }); }); @@ -4926,22 +4925,26 @@ LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property, } LogicalResult StmtEmitter::visitVerif(verif::AssertOp op) { - return emitVerifAssertLike(op, op.getProperty(), PPExtString("assert")); + return emitVerifAssertLike(op, op.getProperty(), op.getEnable(), + PPExtString("assert")); } LogicalResult StmtEmitter::visitVerif(verif::AssumeOp op) { - return emitVerifAssertLike(op, op.getProperty(), PPExtString("assume")); + return emitVerifAssertLike(op, op.getProperty(), op.getEnable(), + PPExtString("assume")); } LogicalResult StmtEmitter::visitVerif(verif::CoverOp op) { - return emitVerifAssertLike(op, op.getProperty(), PPExtString("cover")); + return emitVerifAssertLike(op, op.getProperty(), op.getEnable(), + PPExtString("cover")); } /// Emit an assert-like operation from the `verif` dialect. This covers /// `verif.clocked_assert`, `verif.clocked_assume`, and `verif.clocked_cover`. -LogicalResult StmtEmitter::emitVerifClockedAssertLike( - Operation *op, Value property, Value disable, Value clock, - verif::ClockEdge edge, PPExtString opName) { +LogicalResult +StmtEmitter::emitVerifClockedAssertLike(Operation *op, Value property, + Value clock, verif::ClockEdge edge, + Value enable, PPExtString opName) { if (hasSVAttributes(op)) emitError(op, "SV attributes emission is unimplemented for the op"); @@ -4953,8 +4956,9 @@ LogicalResult StmtEmitter::emitVerifClockedAssertLike( // See IEEE 1800-2017 section 16.14.5 "Using concurrent assertion statements // outside procedural code" and 16.14.6 "Embedding concurrent assertions in // procedural code". + Operation *parent = op->getParentOp(); bool isTemporal = !property.getType().isSignlessInteger(1); - bool isProcedural = op->getParentOp()->hasTrait(); + bool isProcedural = parent->hasTrait(); bool emitAsImmediate = !isTemporal && isProcedural; startStatement(); @@ -4971,7 +4975,7 @@ LogicalResult StmtEmitter::emitVerifClockedAssertLike( ps.scopedBox(PP::ibox2, [&]() { PropertyEmitter(emitter, ops) .emitClockedProperty(property, clock, verifToltlClockEdge(edge), - disable); + enable); ps << ");"; }); }); @@ -4983,20 +4987,20 @@ LogicalResult StmtEmitter::emitVerifClockedAssertLike( // FIXME: emit property assertion wrapped in a clock and disabled LogicalResult StmtEmitter::visitVerif(verif::ClockedAssertOp op) { - return emitVerifClockedAssertLike(op, op.getProperty(), op.getDisable(), - op.getClock(), op.getEdge(), + return emitVerifClockedAssertLike(op, op.getProperty(), op.getClock(), + op.getEdge(), op.getEnable(), PPExtString("assert")); } LogicalResult StmtEmitter::visitVerif(verif::ClockedAssumeOp op) { - return emitVerifClockedAssertLike(op, op.getProperty(), op.getDisable(), - op.getClock(), op.getEdge(), + return emitVerifClockedAssertLike(op, op.getProperty(), op.getClock(), + op.getEdge(), op.getEnable(), PPExtString("assume")); } LogicalResult StmtEmitter::visitVerif(verif::ClockedCoverOp op) { - return emitVerifClockedAssertLike(op, op.getProperty(), op.getDisable(), - op.getClock(), op.getEdge(), + return emitVerifClockedAssertLike(op, op.getProperty(), op.getClock(), + op.getEdge(), op.getEnable(), PPExtString("cover")); } diff --git a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp index 8d34c4bfd4..9048c130a0 100644 --- a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp +++ b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp @@ -1632,7 +1632,9 @@ struct FIRRTLLowering : public FIRRTLVisitor { LogicalResult visitExpr(LTLUntilIntrinsicOp op); LogicalResult visitExpr(LTLEventuallyIntrinsicOp op); LogicalResult visitExpr(LTLClockIntrinsicOp op); - LogicalResult visitExpr(LTLDisableIntrinsicOp op); + + template + LogicalResult lowerVerifIntrinsicOp(IntrinsicOp op); LogicalResult visitStmt(VerifAssertIntrinsicOp op); LogicalResult visitStmt(VerifAssumeIntrinsicOp op); LogicalResult visitStmt(VerifCoverIntrinsicOp op); @@ -3791,28 +3793,24 @@ LogicalResult FIRRTLLowering::visitExpr(LTLClockIntrinsicOp op) { getLoweredNonClockValue(op.getClock())); } -LogicalResult FIRRTLLowering::visitExpr(LTLDisableIntrinsicOp op) { - return setLoweringToLTL( - op, - ValueRange{getLoweredValue(op.getLhs()), getLoweredValue(op.getRhs())}); +template +LogicalResult FIRRTLLowering::lowerVerifIntrinsicOp(IntrinsicOp op) { + auto property = getLoweredValue(op.getProperty()); + auto enable = op.getEnable() ? getLoweredValue(op.getEnable()) : Value(); + builder.create(property, enable, op.getLabelAttr()); + return success(); } LogicalResult FIRRTLLowering::visitStmt(VerifAssertIntrinsicOp op) { - builder.create(getLoweredValue(op.getProperty()), - op.getLabelAttr()); - return success(); + return lowerVerifIntrinsicOp(op); } LogicalResult FIRRTLLowering::visitStmt(VerifAssumeIntrinsicOp op) { - builder.create(getLoweredValue(op.getProperty()), - op.getLabelAttr()); - return success(); + return lowerVerifIntrinsicOp(op); } LogicalResult FIRRTLLowering::visitStmt(VerifCoverIntrinsicOp op) { - builder.create(getLoweredValue(op.getProperty()), - op.getLabelAttr()); - return success(); + return lowerVerifIntrinsicOp(op); } LogicalResult FIRRTLLowering::visitExpr(HasBeenResetIntrinsicOp op) { diff --git a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp index 3da496eee3..357f17eec2 100644 --- a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp +++ b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp @@ -26,6 +26,9 @@ #include "circt/Dialect/SV/SVVisitors.h" #include "circt/Dialect/Seq/SeqDialect.h" #include "circt/Dialect/Seq/SeqOps.h" +#include "circt/Dialect/Verif/VerifDialect.h" +#include "circt/Dialect/Verif/VerifOps.h" +#include "circt/Dialect/Verif/VerifVisitors.h" #include "mlir/Pass/Pass.h" #include "llvm/ADT/MapVector.h" #include "llvm/ADT/TypeSwitch.h" @@ -46,7 +49,8 @@ struct ConvertHWToBTOR2Pass : public circt::impl::ConvertHWToBTOR2Base, public comb::CombinationalVisitor, public sv::Visitor, - public hw::TypeOpVisitor { + public hw::TypeOpVisitor, + public verif::Visitor { public: ConvertHWToBTOR2Pass(raw_ostream &os) : os(os) {} // Executes the pass @@ -218,8 +222,8 @@ private: // Generates a constant declaration given a value, a width and a name. void genConst(int64_t value, size_t width, Operation *op) { - // For now we're going to assume that the name isn't taken, given that hw is - // already in SSA form + // For now we're going to assume that the name isn't taken, given that hw + // is already in SSA form size_t opLID = getOpLID(op); // Retrieve the lid associated with the sort (sid) @@ -258,15 +262,15 @@ private: size_t sid = sortToLIDMap.at(width); size_t initValLID = getOpLID(initVal); - // Build and emit the string (the lid here doesn't need to be associated to - // an op as it won't be used) + // Build and emit the string (the lid here doesn't need to be associated + // to an op as it won't be used) os << lid++ << " " << "init" << " " << sid << " " << regLID << " " << initValLID << "\n"; } - // Generates a binary operation instruction given an op name, two operands and - // a result width. + // Generates a binary operation instruction given an op name, two operands + // and a result width. void genBinOp(StringRef inst, Operation *binop, Value op1, Value op2, size_t width) { // Set the LID for this operation @@ -320,18 +324,48 @@ private: os << opLID << " " << inst << " " << sid << " " << op0LID << "\n"; } - // Generates a constant declaration given a value, a width and a name + // Generates a constant declaration given a value, a width and a name and + // returns the LID associated to it void genUnaryOp(Operation *srcop, Value op0, StringRef inst, size_t width) { genUnaryOp(srcop, op0.getDefiningOp(), inst, width); } + // Generates a constant declaration given a operand lid, a width and a name + size_t genUnaryOp(size_t op0LID, StringRef inst, size_t width) { + // Register the source operation with the current line id + size_t curLid = lid++; + + // Retrieve the lid associated with the sort (sid) + size_t sid = sortToLIDMap.at(width); + + os << curLid << " " << inst << " " << sid << " " << op0LID << "\n"; + return curLid; + } + + // Generates a constant declaration given a value, a width and a name + size_t genUnaryOp(Operation *op0, StringRef inst, size_t width) { + return genUnaryOp(getOpLID(op0), inst, width); + } + + // Generates a constant declaration given a value, a width and a name and + // returns the LID associated to it + size_t genUnaryOp(Value op0, StringRef inst, size_t width) { + return genUnaryOp(getOpLID(op0), inst, width); + } + // Generate a btor2 assertion given an assertion operation // Note that a predicate inversion must have already been generated at this // point void genBad(Operation *assertop) { // Start by finding the expression lid size_t assertLID = getOpLID(assertop); + genBad(assertLID); + } + // Generate a btor2 assertion given an assertion operation's LID + // Note that a predicate inversion must have already been generated at this + // point + void genBad(size_t assertLID) { // Build and return the btor2 string // Also update the lid as this instruction is not associated to an mlir op os << lid++ << " " @@ -386,26 +420,29 @@ private: } // Generate a logical implication given a lhs and a rhs - void genImplies(Operation *srcop, Value lhs, Value rhs) { + size_t genImplies(Operation *srcop, Value lhs, Value rhs) { // Retrieve LIDs for the lhs and rhs size_t lhsLID = getOpLID(lhs); size_t rhsLID = getOpLID(rhs); - genImplies(srcop, lhsLID, rhsLID); + return genImplies(srcop, lhsLID, rhsLID); } // Generate a logical implication given a lhs and a rhs - void genImplies(Operation *srcop, size_t lhsLID, size_t rhsLID) { + size_t genImplies(Operation *srcop, size_t lhsLID, size_t rhsLID) { // Register the source operation with the current line id size_t opLID = getOpLID(srcop); + return genImplies(opLID, lhsLID, rhsLID); + } + size_t genImplies(size_t opLID, size_t lhsLID, size_t rhsLID) { // Retrieve the lid associated with the sort (sid) size_t sid = sortToLIDMap.at(1); - // Build and emit the implies operation os << opLID << " " << "implies" << " " << sid << " " << lhsLID << " " << rhsLID << "\n"; + return opLID; } // Generates a state instruction given a width and a name @@ -422,8 +459,8 @@ private: << " " << sid << " " << name << "\n"; } - // Generates a next instruction, given a width, a state LID, and a next value - // LID + // Generates a next instruction, given a width, a state LID, and a next + // value LID void genNext(Value next, Operation *reg, int64_t width) { // Retrieve the lid associated with the sort (sid) size_t sid = sortToLIDMap.at(width); @@ -445,13 +482,13 @@ private: // Start by figuring out what sort needs to be generated int64_t width = hw::getBitWidth(type); - // Sanity check: getBitWidth can technically return -1 it is a type with no - // width (like a clock). This shouldn't be allowed as width is required to - // generate a sort + // Sanity check: getBitWidth can technically return -1 it is a type with + // no width (like a clock). This shouldn't be allowed as width is required + // to generate a sort assert(width != noWidth); - // Generate the sort regardles of resulting width (nothing will be added if - // the sort already exists) + // Generate the sort regardles of resulting width (nothing will be added + // if the sort already exists) genSort("bitvec", width); return width; } @@ -506,7 +543,8 @@ private: // with next) size_t resetLID = noLID; if (BlockArgument barg = dyn_cast(reset)) { - // Extract the block argument index and use that to get the line number + // Extract the block argument index and use that to get the line + // number size_t argIdx = barg.getArgNumber(); // Check that the extracted argument is in range before using it @@ -534,9 +572,12 @@ private: // i.e. reg <= reset ? 0 : next genIte(next.getDefiningOp(), resetLID, resetValLID, nextLID, width); } else { - // Assign a new LID to next and perform a sanity check - setOpLID(next.getDefiningOp()); - assert(nextLID != noLID); + // Sanity check: next should have been assigned + if (nextLID == noLID) { + next.getDefiningOp()->emitError( + "Register input does not point to a valid op!"); + return; + } } // Finally generate the next statement @@ -565,8 +606,8 @@ public: // Save lid for later size_t inlid = lid; - // Record the defining operation's line ID (the module itself in the case - // of ports) + // Record the defining operation's line ID (the module itself in the + // case of ports) inputLIDs[port.argNum] = lid; // Increment the lid to keep it unique @@ -605,58 +646,36 @@ public: // Binary operations are all emitted the same way, so we can group them into // a single method. - void visitBinOp(Operation *op, StringRef inst, int64_t w) { + template + void visitBinOp(Op op, StringRef inst) { + // Generete the sort + int64_t w = requireSort(op.getType()); // Start by extracting the operands - Value op1 = op->getOperand(0); - Value op2 = op->getOperand(1); + Value op1 = op.getOperand(0); + Value op2 = op.getOperand(1); // Generate the line genBinOp(inst, op, op1, op2, w); } // Visitors for the binary ops - void visitComb(comb::AddOp op) { - visitBinOp(op, "add", requireSort(op.getType())); - } - void visitComb(comb::SubOp op) { - visitBinOp(op, "sub", requireSort(op.getType())); - } - void visitComb(comb::MulOp op) { - visitBinOp(op, "mul", requireSort(op.getType())); - } - void visitComb(comb::DivSOp op) { - visitBinOp(op, "sdiv", requireSort(op.getType())); - } - void visitComb(comb::DivUOp op) { - visitBinOp(op, "udiv", requireSort(op.getType())); - } - void visitComb(comb::ModSOp op) { - visitBinOp(op, "smod", requireSort(op.getType())); - } - void visitComb(comb::ShlOp op) { - visitBinOp(op, "sll", requireSort(op.getType())); - } - void visitComb(comb::ShrUOp op) { - visitBinOp(op, "srl", requireSort(op.getType())); - } - void visitComb(comb::ShrSOp op) { - visitBinOp(op, "sra", requireSort(op.getType())); - } - void visitComb(comb::AndOp op) { - visitBinOp(op, "and", requireSort(op.getType())); - } - void visitComb(comb::OrOp op) { - visitBinOp(op, "or", requireSort(op.getType())); - } - void visitComb(comb::XorOp op) { - visitBinOp(op, "xor", requireSort(op.getType())); - } - void visitComb(comb::ConcatOp op) { - visitBinOp(op, "concat", requireSort(op.getType())); - } + void visitComb(comb::AddOp op) { visitBinOp(op, "add"); } + void visitComb(comb::SubOp op) { visitBinOp(op, "sub"); } + void visitComb(comb::MulOp op) { visitBinOp(op, "mul"); } + void visitComb(comb::DivSOp op) { visitBinOp(op, "sdiv"); } + void visitComb(comb::DivUOp op) { visitBinOp(op, "udiv"); } + void visitComb(comb::ModSOp op) { visitBinOp(op, "smod"); } + void visitComb(comb::ShlOp op) { visitBinOp(op, "sll"); } + void visitComb(comb::ShrUOp op) { visitBinOp(op, "srl"); } + void visitComb(comb::ShrSOp op) { visitBinOp(op, "sra"); } + void visitComb(comb::AndOp op) { visitBinOp(op, "and"); } + void visitComb(comb::OrOp op) { visitBinOp(op, "or"); } + void visitComb(comb::XorOp op) { visitBinOp(op, "xor"); } + void visitComb(comb::ConcatOp op) { visitBinOp(op, "concat"); } - // Extract ops translate to a slice operation in btor2 in a one-to-one manner + // Extract ops translate to a slice operation in btor2 in a one-to-one + // manner void visitComb(comb::ExtractOp op) { int64_t w = requireSort(op.getType()); @@ -750,7 +769,75 @@ public: void visitSV(Operation *op) { visitInvalidSV(op); } // Once SV Ops are visited, we need to check for seq ops - void visitInvalidSV(Operation *op) { visit(op); } + void visitInvalidSV(Operation *op) { dispatchVerifVisitor(op); } + + template + void visitAssertLike(Op op) { + // Expression is what we will try to invert for our assertion + Value prop = op.getProperty(); + Value en = op.getEnable(); + + // This sort is for assertion inversion and potential implies + genSort("bitvec", 1); + + size_t assertLID = noLID; + // Check for a related enable signal + if (en) { + // Generate the implication + genImplies(op, en, prop); + + // Generate the implies inversion + assertLID = genUnaryOp(op, "not", 1); + } else { + // Generate the expression inversion + assertLID = genUnaryOp(prop.getDefiningOp(), "not", 1); + } + + // Genrate the bad btor2 intruction + genBad(assertLID); + } + + template + void visitAssumeLike(Op op) { + // Expression is what we will try to invert for our assertion + Value prop = op.getProperty(); + Value en = op.getEnable(); + + size_t assumeLID = getOpLID(prop); + // Check for a related enable signal + if (en) { + // This sort is for assertion inversion and potential implies + genSort("bitvec", 1); + // Generate the implication + assumeLID = genImplies(op, en, prop); + } + + // Genrate the bad btor2 intruction + genConstraint(assumeLID); + } + + // Folds the enable signal into the property and converts the result into a + // bad instruction. + void visitVerif(verif::AssertOp op) { visitAssertLike(op); } + void visitVerif(verif::ClockedAssertOp op) { visitAssertLike(op); } + + // Fold the enable into the property and convert the assumption into a + // constraint instruction. + void visitVerif(verif::AssumeOp op) { visitAssumeLike(op); } + void visitVerif(verif::ClockedAssumeOp op) { visitAssumeLike(op); } + + // Cover is not supported in btor2 + void visitVerif(verif::CoverOp op) { + op->emitError("Cover is not supprted in btor2!"); + return signalPassFailure(); + } + + void visitVerif(verif::ClockedCoverOp op) { + op->emitError("Cover is not supprted in btor2!"); + return signalPassFailure(); + } + + void visitInvalidVerif(Operation *op) { visit(op); } // Seq operation visitor, that dispatches to other seq ops // Also handles all remaining operations that should be explicitly ignored @@ -758,7 +845,7 @@ public: // Typeswitch is used here because other seq types will be supported // like all operations relating to memories and CompRegs TypeSwitch(op) - .Case([&](auto expr) { visit(expr); }) + .Case([&](auto expr) { visit(expr); }) .Default([&](auto expr) { visitUnsupportedOp(op); }); } @@ -785,8 +872,13 @@ public: StringRef regName = reg.getName().value(); int64_t w = requireSort(reg.getType()); - // Check for initial values which must be emitted before the state in btor2 + // Check for initial values which must be emitted before the state in + // btor2 Value pov = reg.getPowerOnValue(); + + // Generate state instruction (represents the register declaration) + genState(reg, w, regName); + if (pov) { // Check that the powerOn value is a non-null constant if (!isa_and_nonnull(pov.getDefiningOp())) @@ -798,15 +890,8 @@ public: // Add it to the list of visited operations handledOps.insert(pov.getDefiningOp()); - // Generate state instruction (represents the register declaration) - genState(reg, w, regName); - // Finally generate the init statement genInit(reg, pov, w); - - } else { - // Only generate the state instruction and nothing else - genState(reg, w, regName); } // Record the operation for future `next` instruction generation @@ -860,7 +945,7 @@ void ConvertHWToBTOR2Pass::runOnOperation() { visit(port); } - // Previsit all registers in the module in order to avoid dependency cylcles + // Previsit all registers in the module in order to avoid dependency cycles module.walk([&](Operation *op) { TypeSwitch(op) .Case([&](auto reg) { @@ -910,7 +995,7 @@ void ConvertHWToBTOR2Pass::runOnOperation() { // This is triggered if our operand is already in the worklist and // wasn't handled if (!worklist.insert({defOp, defOp->operand_begin()}).second) { - op->emitError("dependency cycle"); + defOp->emitError("dependency cycle"); return; } } diff --git a/lib/Conversion/LTLToCore/LTLToCore.cpp b/lib/Conversion/LTLToCore/LTLToCore.cpp index e7d0f10492..d4a3d1a8aa 100644 --- a/lib/Conversion/LTLToCore/LTLToCore.cpp +++ b/lib/Conversion/LTLToCore/LTLToCore.cpp @@ -38,68 +38,11 @@ using namespace mlir; using namespace circt; using namespace hw; -static sv::EventControl ltlToSVEventControl(ltl::ClockEdge ce) { - switch (ce) { - case ltl::ClockEdge::Pos: - return sv::EventControl::AtPosEdge; - case ltl::ClockEdge::Neg: - return sv::EventControl::AtNegEdge; - case ltl::ClockEdge::Both: - return sv::EventControl::AtEdge; - } - llvm_unreachable("Unknown event control kind"); -} - //===----------------------------------------------------------------------===// // Conversion patterns //===----------------------------------------------------------------------===// namespace { - -// Custom pattern matchers - -// Matches and records a boolean attribute -struct I1ValueMatcher { - Value *what; - I1ValueMatcher(Value *what) : what(what) {} - bool match(Value op) const { - if (!op.getType().isSignlessInteger(1)) - return false; - *what = op; - return true; - } -}; - -static inline I1ValueMatcher mBool(Value *const val) { - return I1ValueMatcher(val); -} - -// Matches and records an arbitrary op -template -struct BindingRecursivePatternMatcher - : mlir::detail::RecursivePatternMatcher { - - using BaseMatcher = - mlir::detail::RecursivePatternMatcher; - BindingRecursivePatternMatcher(OpType *bop, OperandMatchers... matchers) - : BaseMatcher(matchers...), opBind(bop) {} - - bool match(Operation *op) { - if (BaseMatcher::match(op)) { - *opBind = llvm::cast(op); - return true; - } - return false; - } - - OpType *opBind; -}; - -template -static inline auto mOpWithBind(OpType *op, Matchers... matchers) { - return BindingRecursivePatternMatcher(op, matchers...); -} - struct HasBeenResetOpConversion : OpConversionPattern { using OpConversionPattern::OpConversionPattern; @@ -147,68 +90,6 @@ struct HasBeenResetOpConversion : OpConversionPattern { } }; -struct AssertOpConversionPattern : OpConversionPattern { - using OpConversionPattern::OpConversionPattern; - - Value visit(ltl::DisableOp op, ConversionPatternRewriter &rewriter, - Value operand = nullptr) const { - // Replace the ltl::DisableOp with an OR op as it represents a disabling - // implication: (implies (not condition) input) is equivalent to - // (or (not (not condition)) input) which becomes (or condition input) - return rewriter.replaceOpWithNewOp( - op, op.getCondition(), operand ? operand : op.getInput()); - } - - // Special case : we want to detect the Non-overlapping implication, - // Overlapping Implication or simply AssertProperty patterns and reject - // everything else for now: antecedent : ltl::concatOp || immediate predicate - // consequent : any other non-sequence op - // We want to support a ##n true |-> b and a |-> b - LogicalResult - matchAndRewrite(verif::AssertOp op, OpAdaptor adaptor, - ConversionPatternRewriter &rewriter) const override { - - Value ltlClock, disableCond, disableInput, disableVal; - ltl::ClockOp clockOp; - ltl::DisableOp disableOp; - - // Look for the Assert Property pattern - bool matchedProperty = matchPattern( - op.getProperty(), - mOpWithBind( - &clockOp, - mOpWithBind(&disableOp, mBool(&disableInput), - mBool(&disableCond)), - mBool(<lClock))); - - if (!matchedProperty) - return rewriter.notifyMatchFailure( - op, " verif.assert used outside of an assert property!"); - - // Then visit the disable op - disableVal = visit(disableOp, rewriter, disableInput); - - // Generate the parenting sv.always posedge clock from the ltl - // clock, containing the generated sv.assert - rewriter.create( - clockOp.getLoc(), ltlToSVEventControl(clockOp.getEdge()), ltlClock, - [&] { - // Generate the sv assertion using the input to the - // parenting clock - rewriter.replaceOpWithNewOp( - op, disableVal, - sv::DeferAssertAttr::get(getContext(), - sv::DeferAssert::Immediate), - op.getLabelAttr()); - }); - - // Erase Converted Ops - rewriter.eraseOp(clockOp); - - return success(); - } -}; - } // namespace //===----------------------------------------------------------------------===// @@ -234,7 +115,8 @@ void LowerLTLToCorePass::runOnOperation() { target.addLegalDialect(); target.addLegalDialect(); target.addLegalDialect(); - target.addIllegalDialect(); + target.addLegalDialect(); + target.addIllegalOp(); // Create type converters, mostly just to convert an ltl property to a bool mlir::TypeConverter converter; @@ -269,8 +151,7 @@ void LowerLTLToCorePass::runOnOperation() { // Create the operation rewrite patters RewritePatternSet patterns(&getContext()); - patterns.add( - converter, patterns.getContext()); + patterns.add(converter, patterns.getContext()); // Apply the conversions if (failed( diff --git a/lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp b/lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp index 3005168bf6..f5e07fc168 100644 --- a/lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp +++ b/lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp @@ -18,13 +18,25 @@ using namespace firrtl; // GenericIntrinsic //===----------------------------------------------------------------------===// -ParseResult GenericIntrinsic::hasNInputs(unsigned n) { - if (op.getNumOperands() != n) - return emitError() << " has " << op.getNumOperands() - << " inputs instead of " << n; +// Checks for a number of operands between n and n+c (allows for c optional +// inputs) +ParseResult GenericIntrinsic::hasNInputs(unsigned n, unsigned c = 0U) { + auto numOps = op.getNumOperands(); + unsigned m = n + c; + if (!(n <= numOps && numOps <= m)) { + auto err = emitError() << " has " << numOps << " inputs instead of "; + if (c == 0) + err << n; + else + err << " between " << n << " and " << m; + return failure(); + } return success(); } +// Accessor method for the number of inputs +unsigned GenericIntrinsic::getNumInputs() { return op.getNumOperands(); } + ParseResult GenericIntrinsic::hasNOutputElements(unsigned n) { auto b = getOutputBundle(); if (!b) @@ -447,7 +459,7 @@ public: using IntrinsicConverter::IntrinsicConverter; bool check(GenericIntrinsic gi) override { - return gi.hasNInputs(1) || gi.sizedInput(0, 1) || + return gi.hasNInputs(1, 2) || gi.sizedInput(0, 1) || gi.namedParam("label", true) || gi.hasNParam(0, 1) || gi.hasNoOutput(); } @@ -455,8 +467,14 @@ public: void convert(GenericIntrinsic gi, GenericIntrinsicOpAdaptor adaptor, PatternRewriter &rewriter) override { auto label = gi.getParamValue("label"); + auto operands = adaptor.getOperands(); - rewriter.replaceOpWithNewOp(gi.op, adaptor.getOperands()[0], label); + // Check if an enable was provided + Value enable; + if (gi.getNumInputs() == 2) + enable = operands[1]; + + rewriter.replaceOpWithNewOp(gi.op, operands[0], enable, label); } }; @@ -708,8 +726,6 @@ void FIRRTLIntrinsicLoweringDialectInterface::populateIntrinsicLowerings( "circt.ltl.implication", "circt_ltl_implication"); lowering.add>("circt.ltl.until", "circt_ltl_until"); - lowering.add>( - "circt.ltl.disable", "circt_ltl_disable"); lowering.add>("circt.ltl.not", "circt_ltl_not"); lowering.add>( diff --git a/lib/Dialect/FIRRTL/Transforms/ExpandWhens.cpp b/lib/Dialect/FIRRTL/Transforms/ExpandWhens.cpp index fda0f0ad0a..f785f92c8a 100644 --- a/lib/Dialect/FIRRTL/Transforms/ExpandWhens.cpp +++ b/lib/Dialect/FIRRTL/Transforms/ExpandWhens.cpp @@ -548,15 +548,21 @@ private: condition.getLoc(), condition.getType(), condition, value); } - // Create an implication from the condition to the given value - // This is implemented as (or (not condition) value) to avoid - // the corner case where value is an implication. - Value impliesLTLCondition(Operation *op, Value value) { - OpBuilder builder = OpBuilder(op); - Value notCond = builder.createOrFold( - condition.getLoc(), condition.getType(), condition); - return builder.createOrFold( - condition.getLoc(), condition.getType(), notCond, value); + /// Concurrent and of a property with the current condition. If we are in + /// the outer scope, i.e. not in a WhenOp region, then there is no condition. + Value ltlAndWithCondition(Operation *op, Value value) { + // 'ltl.and' the value with the current condition. + return OpBuilder(op).createOrFold( + condition.getLoc(), condition.getType(), condition, value); + } + + /// Overlapping implication with the condition as its antecedent and a given + /// property as the consequent. If we are in the outer scope, i.e. not in a + /// WhenOp region, then there is no condition. + Value ltlImplicationWithCondition(Operation *op, Value value) { + // 'and' the value with the current condition. + return OpBuilder(op).createOrFold( + condition.getLoc(), condition.getType(), condition, value); } private: @@ -580,15 +586,17 @@ void WhenOpVisitor::visitStmt(StopOp op) { } void WhenOpVisitor::visitStmt(VerifAssertIntrinsicOp op) { - op.getPropertyMutable().assign(impliesLTLCondition(op, op.getProperty())); + op.getPropertyMutable().assign( + ltlImplicationWithCondition(op, op.getProperty())); } void WhenOpVisitor::visitStmt(VerifAssumeIntrinsicOp op) { - op.getPropertyMutable().assign(impliesLTLCondition(op, op.getProperty())); + op.getPropertyMutable().assign( + ltlImplicationWithCondition(op, op.getProperty())); } void WhenOpVisitor::visitStmt(VerifCoverIntrinsicOp op) { - op.getPropertyMutable().assign(impliesLTLCondition(op, op.getProperty())); + op.getPropertyMutable().assign(ltlAndWithCondition(op, op.getProperty())); } void WhenOpVisitor::visitStmt(AssertOp op) { diff --git a/lib/Dialect/LTL/LTLFolds.cpp b/lib/Dialect/LTL/LTLFolds.cpp index 1dc8804ac0..7879401eb0 100644 --- a/lib/Dialect/LTL/LTLFolds.cpp +++ b/lib/Dialect/LTL/LTLFolds.cpp @@ -121,15 +121,3 @@ OpFoldResult GoToRepeatOp::fold(FoldAdaptor adaptor) { OpFoldResult NonConsecutiveRepeatOp::fold(FoldAdaptor adaptor) { return RepeatLikeOp::fold(adaptor.getBase(), adaptor.getMore(), getInput()); } - -//===----------------------------------------------------------------------===// -// DisableOp -//===----------------------------------------------------------------------===// - -OpFoldResult DisableOp::fold(FoldAdaptor adaptor) { - // disable(p, false) -> p - if (isConstantZero(adaptor.getCondition())) - return getInput(); - - return {}; -} diff --git a/lib/Dialect/Verif/Transforms/CMakeLists.txt b/lib/Dialect/Verif/Transforms/CMakeLists.txt index 74c52e6af5..b4aad4e7c5 100644 --- a/lib/Dialect/Verif/Transforms/CMakeLists.txt +++ b/lib/Dialect/Verif/Transforms/CMakeLists.txt @@ -1,6 +1,7 @@ add_circt_dialect_library(CIRCTVerifTransforms PrepareForFormal.cpp VerifyClockedAssertLike.cpp + PrepareForFormal.cpp DEPENDS CIRCTVerifTransformsIncGen diff --git a/lib/Dialect/Verif/Transforms/VerifyClockedAssertLike.cpp b/lib/Dialect/Verif/Transforms/VerifyClockedAssertLike.cpp index 02f6dcfb43..749fc0b75f 100644 --- a/lib/Dialect/Verif/Transforms/VerifyClockedAssertLike.cpp +++ b/lib/Dialect/Verif/Transforms/VerifyClockedAssertLike.cpp @@ -65,7 +65,7 @@ private: if (operandIt == op->operand_end()) { // Check that our property doesn't contain any illegal ops - if (isa(op)) { + if (isa(op)) { op->emitError("Nested clock or disable operations are not " "allowed for clock_assertlike operations."); return; @@ -86,12 +86,7 @@ private: if (!defOp || handledOps.contains(defOp)) continue; - // This is triggered if our operand is already in the worklist and - // wasn't handled - if (!worklist.insert({defOp, defOp->operand_begin()}).second) { - op->emitError("dependency cycle"); - return; - } + worklist.insert({defOp, defOp->operand_begin()}); } // Clear worklist and such diff --git a/lib/Dialect/Verif/VerifOps.cpp b/lib/Dialect/Verif/VerifOps.cpp index e380bc0817..bfdf6fecb7 100644 --- a/lib/Dialect/Verif/VerifOps.cpp +++ b/lib/Dialect/Verif/VerifOps.cpp @@ -23,6 +23,18 @@ using namespace circt; using namespace verif; using namespace mlir; +static ClockEdge ltlToVerifClockEdge(ltl::ClockEdge ce) { + switch (ce) { + case ltl::ClockEdge::Pos: + return ClockEdge::Pos; + case ltl::ClockEdge::Neg: + return ClockEdge::Neg; + case ltl::ClockEdge::Both: + return ClockEdge::Both; + } + llvm_unreachable("Unknown event control kind"); +} + //===----------------------------------------------------------------------===// // HasBeenResetOp //===----------------------------------------------------------------------===// @@ -42,6 +54,43 @@ OpFoldResult HasBeenResetOp::fold(FoldAdaptor adaptor) { return {}; } +//===----------------------------------------------------------------------===// +// AssertLikeOps Canonicalizations +//===----------------------------------------------------------------------===// + +namespace AssertLikeOp { +// assertlike(ltl.clock(prop, clk), en) -> clocked_assertlike(prop, en, clk) +template +static LogicalResult canonicalize(Op op, PatternRewriter &rewriter) { + // If the property is a block argument, then no canonicalization is possible + Value property = op.getProperty(); + auto clockOp = property.getDefiningOp(); + if (!clockOp) + return failure(); + + // Check for clock operand + // If it exists, fold it into a clocked assertlike + rewriter.replaceOpWithNewOp( + op, clockOp.getInput(), ltlToVerifClockEdge(clockOp.getEdge()), + clockOp.getClock(), op.getEnable(), op.getLabelAttr()); + + return success(); +} + +} // namespace AssertLikeOp + +LogicalResult AssertOp::canonicalize(AssertOp op, PatternRewriter &rewriter) { + return AssertLikeOp::canonicalize(op, rewriter); +} + +LogicalResult AssumeOp::canonicalize(AssumeOp op, PatternRewriter &rewriter) { + return AssertLikeOp::canonicalize(op, rewriter); +} + +LogicalResult CoverOp::canonicalize(CoverOp op, PatternRewriter &rewriter) { + return AssertLikeOp::canonicalize(op, rewriter); +} + //===----------------------------------------------------------------------===// // LogicalEquivalenceCheckingOp //===----------------------------------------------------------------------===// diff --git a/test/Conversion/ExportVerilog/prepare-for-emission.mlir b/test/Conversion/ExportVerilog/prepare-for-emission.mlir index 3bfa07c22b..1992b2d8a3 100644 --- a/test/Conversion/ExportVerilog/prepare-for-emission.mlir +++ b/test/Conversion/ExportVerilog/prepare-for-emission.mlir @@ -148,26 +148,6 @@ module attributes {circt.loweringOptions = "disallowExpressionInliningInPorts"} // ----- -module attributes {circt.loweringOptions = "disallowExpressionInliningInPorts"} { - // CHECK-LABEL: @DisableIff( - hw.module @DisableIff(in %clk: i1, in %a: i1, in %b: i1) { - %b_xor_b = comb.xor %b, %b : i1 - - // CHECK: %[[XOR:.+]] = comb.xor - // CHECK: %[[WIRE:.+]] = sv.wire - // CHECK: sv.assign %[[WIRE]], %[[XOR]] - // CHECK: %[[READ:.+]] = sv.read_inout %[[WIRE]] - // CHECK: ltl.disable %{{.+}} if %[[READ]] - %i0 = ltl.implication %a, %b : i1, i1 - %k0 = ltl.clock %i0, posedge %clk : !ltl.property - %k5 = ltl.disable %k0 if %b_xor_b : !ltl.property - - verif.assert %k5: !ltl.property - } -} - -// ----- - module attributes {circt.loweringOptions = "disallowExpressionInliningInPorts"} { // CHECK-LABEL: @ClockExpr( hw.module @ClockExpr(in %clk: i1, in %a: i1, in %b: i1) { @@ -181,7 +161,7 @@ module attributes {circt.loweringOptions = "disallowExpressionInliningInPorts"} %i0 = ltl.implication %a, %b : i1, i1 %k0 = ltl.clock %i0, posedge %clk_xor_b : !ltl.property - verif.assert %k0: !ltl.property + verif.assert %k0 : !ltl.property } } diff --git a/test/Conversion/ExportVerilog/verif.mlir b/test/Conversion/ExportVerilog/verif.mlir index cabe29ed9e..dd3cde019e 100644 --- a/test/Conversion/ExportVerilog/verif.mlir +++ b/test/Conversion/ExportVerilog/verif.mlir @@ -195,21 +195,17 @@ hw.module @Properties(in %clk: i1, in %a: i1, in %b: i1) { // CHECK: assert property (@(posedge clk) a |-> b); // CHECK: assert property (@(posedge clk) a ##1 b |-> (@(negedge b) not a)); - // CHECK: assert property (disable iff (b) not a); - // CHECK: assert property (disable iff (b) @(posedge clk) a |-> b); - // CHECK: assert property (@(posedge clk) disable iff (b) not a); + // CHECK: assert property (disable iff (~(b)) not a); + // CHECK: assert property (disable iff (~(b)) @(posedge clk) not a); %k0 = ltl.clock %i0, posedge %clk : !ltl.property %k1 = ltl.clock %n0, negedge %b : !ltl.property %k2 = ltl.implication %i2, %k1 : !ltl.sequence, !ltl.property %k3 = ltl.clock %k2, posedge %clk : !ltl.property - %k4 = ltl.disable %n0 if %b : !ltl.property - %k5 = ltl.disable %k0 if %b : !ltl.property - %k6 = ltl.clock %k4, posedge %clk : !ltl.property + %k6 = ltl.clock %n0, posedge %clk : !ltl.property verif.assert %k0 : !ltl.property verif.assert %k3 : !ltl.property - verif.assert %k4 : !ltl.property - verif.assert %k5 : !ltl.property - verif.assert %k6 : !ltl.property + verif.assert %n0 if %b : !ltl.property + verif.assert %k6 if %b : !ltl.property } // CHECK-LABEL: module Precedence @@ -267,12 +263,11 @@ hw.module @SystemVerilogSpecExamples(in %clk: i1, in %a: i1, in %b: i1, in %c: i %b3 = ltl.clock %b2, posedge %clk : !ltl.property verif.assert %b3 : !ltl.property - // CHECK: assert property (@(posedge clk) disable iff (e) a |-> not b ##1 c ##1 d); + // CHECK: assert property (disable iff (~(e)) @(posedge clk) a |-> not b ##1 c ##1 d); %c0 = ltl.not %b1 : !ltl.sequence %c1 = ltl.implication %a, %c0 : i1, !ltl.property - %c2 = ltl.disable %c1 if %e : !ltl.property - %c3 = ltl.clock %c2, posedge %clk : !ltl.property - verif.assert %c3 : !ltl.property + %c3 = ltl.clock %c1, posedge %clk : !ltl.property + verif.assert %c3 if %e : !ltl.property // CHECK: assert property (##1 a |-> b); %d0 = ltl.delay %a, 1, 0 : i1 @@ -285,27 +280,25 @@ hw.module @LivenessExample(in %clock: i1, in %reset: i1, in %isLive: i1) { %true = hw.constant true // CHECK: wire _GEN = ~isLive; - // CHECK: assert property (@(posedge clock) disable iff (reset) $fell(reset) & _GEN |-> (s_eventually isLive)); - // CHECK: assume property (@(posedge clock) disable iff (reset) $fell(reset) & _GEN |-> (s_eventually isLive)); + // CHECK: assert property (disable iff (~(reset)) @(posedge clock) $fell(reset) & _GEN |-> (s_eventually isLive)); + // CHECK: assume property (disable iff (~(reset)) @(posedge clock) $fell(reset) & _GEN |-> (s_eventually isLive)); %not_isLive = comb.xor %isLive, %true : i1 %fell_reset = sv.verbatim.expr "$fell({{0}})"(%reset) : (i1) -> i1 %0 = comb.and %fell_reset, %not_isLive : i1 %1 = ltl.eventually %isLive : i1 %2 = ltl.implication %0, %1 : i1, !ltl.property - %3 = ltl.disable %2 if %reset : !ltl.property - %liveness_after_reset = ltl.clock %3, posedge %clock : !ltl.property - verif.assert %liveness_after_reset : !ltl.property - verif.assume %liveness_after_reset : !ltl.property + %liveness_after_reset = ltl.clock %2, posedge %clock : !ltl.property + verif.assert %liveness_after_reset if %reset : !ltl.property + verif.assume %liveness_after_reset if %reset : !ltl.property - // CHECK: assert property (@(posedge clock) disable iff (reset) isLive ##1 _GEN |-> (s_eventually isLive)); - // CHECK: assume property (@(posedge clock) disable iff (reset) isLive ##1 _GEN |-> (s_eventually isLive)); + // CHECK: assert property (disable iff (~(reset)) @(posedge clock) isLive ##1 _GEN |-> (s_eventually isLive)); + // CHECK: assume property (disable iff (~(reset)) @(posedge clock) isLive ##1 _GEN |-> (s_eventually isLive)); %4 = ltl.delay %not_isLive, 1, 0 : i1 %5 = ltl.concat %isLive, %4 : i1, !ltl.sequence %6 = ltl.implication %5, %1 : !ltl.sequence, !ltl.property - %7 = ltl.disable %6 if %reset : !ltl.property - %liveness_after_fall = ltl.clock %7, posedge %clock : !ltl.property - verif.assert %liveness_after_fall : !ltl.property - verif.assume %liveness_after_fall : !ltl.property + %liveness_after_fall = ltl.clock %6, posedge %clock : !ltl.property + verif.assert %liveness_after_fall if %reset : !ltl.property + verif.assume %liveness_after_fall if %reset : !ltl.property } // https://github.com/llvm/circt/issues/5763 @@ -325,12 +318,12 @@ hw.module @ClockedAsserts(in %clk: i1, in %a: i1, in %b: i1) { %true = hw.constant true %n0 = ltl.not %a : i1 - // CHECK: assert property (@(posedge clk) disable iff (b) not a); - verif.clocked_assert %n0 disable %b clock posedge %clk : !ltl.property + // CHECK: assert property (@(posedge clk) disable iff (~(b)) not a); + verif.clocked_assert %n0 if %b, posedge %clk : !ltl.property - // CHECK: assume property (@(posedge clk) disable iff (b) not a); - verif.clocked_assume %n0 disable %b clock posedge %clk : !ltl.property + // CHECK: assume property (@(posedge clk) disable iff (~(b)) not a); + verif.clocked_assume %n0 if %b, posedge %clk : !ltl.property - // CHECK: cover property (@(posedge clk) disable iff (b) not a); - verif.clocked_cover %n0 disable %b clock posedge %clk : !ltl.property + // CHECK: cover property (@(posedge clk) disable iff (~(b)) not a); + verif.clocked_cover %n0 if %b, posedge %clk : !ltl.property } diff --git a/test/Conversion/FIRRTLToHW/intrinsics.mlir b/test/Conversion/FIRRTLToHW/intrinsics.mlir index 06660438fd..f7a649c28c 100644 --- a/test/Conversion/FIRRTLToHW/intrinsics.mlir +++ b/test/Conversion/FIRRTLToHW/intrinsics.mlir @@ -107,9 +107,6 @@ firrtl.circuit "Intrinsics" { // CHECK-NEXT: [[K0:%.+]] = ltl.clock [[I0]], posedge [[CLK]] : !ltl.property %k0 = firrtl.int.ltl.clock %i0, %clk : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> - // CHECK-NEXT: [[D2:%.+]] = ltl.disable [[K0]] if %b : !ltl.property - %d2 = firrtl.int.ltl.disable %k0, %b : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK-NEXT: verif.assert %a : i1 firrtl.int.verif.assert %a : !firrtl.uint<1> // CHECK-NEXT: verif.assert %a label "hello" : i1 diff --git a/test/Conversion/HWToBTOR2/init.mlir b/test/Conversion/HWToBTOR2/init.mlir index 062be0fbc0..9975b4b04d 100644 --- a/test/Conversion/HWToBTOR2/init.mlir +++ b/test/Conversion/HWToBTOR2/init.mlir @@ -4,11 +4,12 @@ module { //CHECK: [[NID0:[0-9]+]] sort bitvec 1 //CHECK: [[NID1:[0-9]+]] input [[NID0]] reset hw.module @test(in %clock : !seq.clock, in %reset : i1) { + // Register states get pregenerated + //CHECK: [[NID2:[0-9]+]] state [[NID0]] reg %0 = seq.from_clock %clock //CHECK: [[NID3:[0-9]+]] constd [[NID0]] 0 %false = hw.constant false - //CHECK: [[NID2:[0-9]+]] state [[NID0]] reg - //CHECK: [[NID9:[0-9]+]] init [[NID0]] [[NID2]] [[NID3]] + //CHECK: [[INIT:[0-9]+]] init [[NID0]] [[NID2]] [[NID3]] %reg = seq.compreg %false, %clock reset %reset, %false powerOn %false : i1 //CHECK: [[NID4:[0-9]+]] eq [[NID0]] [[NID2]] [[NID3]] diff --git a/test/Conversion/LTLToCore/assertproperty.mlir b/test/Conversion/LTLToCore/assertproperty.mlir index 5c4454b922..aac8141796 100644 --- a/test/Conversion/LTLToCore/assertproperty.mlir +++ b/test/Conversion/LTLToCore/assertproperty.mlir @@ -2,35 +2,21 @@ // Tests that an Assert Property high level statement can be converted correctly module { - //CHECK: hw.module @test(in %clock : !seq.clock, in %reset : i1, in %0 "" : i1) - hw.module @test(in %clock : !seq.clock, in %reset : i1, in %8 : i1) { - //CHECK: %1 = seq.from_clock %clock + //CHECK: hw.module @test(in %clock : !seq.clock, in %reset : i1, in %a : i1) + hw.module @test(in %clock : !seq.clock, in %reset : i1, in %a : i1) { + //CHECK: [[CLK:%.+]] = seq.from_clock %clock %0 = seq.from_clock %clock - //CHECK: %true = hw.constant true - %true = hw.constant true //CHECK: %false = hw.constant false - //CHECK: %true_0 = hw.constant true - //CHECK: %2 = comb.or %reset, %hbr : i1 - //CHECK: %hbr = seq.compreg %2, %clock powerOn %false : i1 - %9 = verif.has_been_reset %0, sync %reset + //CHECK: %true = hw.constant true + //CHECK: [[TMP:%.+]] = comb.or %reset, %hbr : i1 + //CHECK: %hbr = seq.compreg [[TMP]], %clock powerOn %false : i1 + %1 = verif.has_been_reset %0, sync %reset - //CHECK: %3 = comb.xor %reset, %true_0 : i1 - //CHECK: %4 = comb.and %hbr, %3 : i1 - //CHECK: %5 = comb.xor bin %4, %true : i1 - %10 = comb.xor bin %9, %true : i1 - - //CHECK: %6 = hw.wire %5 : i1 - %12 = hw.wire %10 : i1 - - //CHECK: %7 = comb.or %6, %0 : i1 - %13 = ltl.disable %8 if %12 : i1 - - //CHECK: sv.always posedge %1 { - //CHECK: sv.assert %7, immediate - //CHECK: } - %14 = ltl.clock %13, posedge %0 : !ltl.property - verif.assert %14 : !ltl.property + //CHECK: [[TMP1:%.+]] = comb.xor %reset, %true : i1 + //CHECK: [[TMP2:%.+]] = comb.and %hbr, [[TMP1]] : i1 + //CHECK: verif.clocked_assert %a if [[TMP2]], posedge [[CLK]] : i1 + verif.clocked_assert %a if %1, posedge %0 : i1 //CHECK: hw.output hw.output diff --git a/test/Dialect/FIRRTL/expand-whens.mlir b/test/Dialect/FIRRTL/expand-whens.mlir index 7f1b67c893..77a750119b 100644 --- a/test/Dialect/FIRRTL/expand-whens.mlir +++ b/test/Dialect/FIRRTL/expand-whens.mlir @@ -637,38 +637,69 @@ firrtl.module @ModuleWithObjectWire(in %in: !firrtl.class<@ClassWithInput(in in: } // Test all verif assert/assume/cover constructs -// CHECK: firrtl.module @verif(in %clock: !firrtl.clock, in %cond: !firrtl.uint<1>, in %prop: !firrtl.uint<1>, in %enable: !firrtl.uint<1>, in %reset: !firrtl.uint<1>) { -firrtl.module @verif( - in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, - in %enable : !firrtl.uint<1>, in %reset : !firrtl.uint<1> +// CHECK-LABEL: firrtl.module @verifassert +firrtl.module @verifassert( + in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, in %prop1 : !firrtl.uint<1>, + in %enable : !firrtl.uint<1>, in %enable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1> ) { firrtl.when %cond : !firrtl.uint<1> { - // CHECK: [[TMP0:%.+]] = firrtl.int.ltl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: [[TMP1:%.+]] = firrtl.int.ltl.or [[TMP0]], %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: firrtl.int.verif.assert [[TMP1]] : !firrtl.uint<1> - firrtl.int.verif.assert %prop : !firrtl.uint<1> - // CHECK: %2 = firrtl.int.ltl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: %3 = firrtl.int.ltl.or %2, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: firrtl.int.verif.assume %3 : !firrtl.uint<1> - firrtl.int.verif.assume %prop : !firrtl.uint<1> - // CHECK: %4 = firrtl.int.ltl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: %5 = firrtl.int.ltl.or %4, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: firrtl.int.verif.cover %5 : !firrtl.uint<1> - firrtl.int.verif.cover %prop : !firrtl.uint<1> + // CHECK: [[TMP2A:%.+]] = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + // CHECK: [[TMP0A:%.+]] = firrtl.int.ltl.implication %cond, [[TMP2A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK: firrtl.int.verif.assert [[TMP0A]], %enable : !firrtl.uint<1>, !firrtl.uint<1> + %clk_prop = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + + firrtl.int.verif.assert %clk_prop, %enable : !firrtl.uint<1>, !firrtl.uint<1> } else { - // CHECK: %6 = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: %7 = firrtl.int.ltl.not %6 : (!firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: %8 = firrtl.int.ltl.or %7, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: firrtl.int.verif.assert %8 : !firrtl.uint<1> - firrtl.int.verif.assert %prop : !firrtl.uint<1> - // CHECK: %9 = firrtl.int.ltl.not %6 : (!firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: %10 = firrtl.int.ltl.or %9, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: firrtl.int.verif.assume %10 : !firrtl.uint<1> - firrtl.int.verif.assume %prop : !firrtl.uint<1> - // CHECK: %11 = firrtl.int.ltl.not %6 : (!firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: %12 = firrtl.int.ltl.or %11, %prop : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK: firrtl.int.verif.cover %12 : !firrtl.uint<1> - firrtl.int.verif.cover %prop : !firrtl.uint<1> + // CHECK: [[TMP3A:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK: [[TMP6A:%.+]] = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + // CHECK: [[TMP4A:%.+]] = firrtl.int.ltl.implication [[TMP3A]], [[TMP6A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK: firrtl.int.verif.assert [[TMP4A]], %enable1 : !firrtl.uint<1>, !firrtl.uint<1> + %clk_prop = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + firrtl.int.verif.assert %clk_prop, %enable1 : !firrtl.uint<1>, !firrtl.uint<1> + } +} + +// CHECK-LABEL: firrtl.module @verifassume +firrtl.module @verifassume( + in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, in %prop1 : !firrtl.uint<1>, + in %enable : !firrtl.uint<1>, in %enable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1> +) { + firrtl.when %cond : !firrtl.uint<1> { + // CHECK: [[TMP2A:%.+]] = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + // CHECK: [[TMP0A:%.+]] = firrtl.int.ltl.implication %cond, [[TMP2A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK: firrtl.int.verif.assume [[TMP0A]], %enable : !firrtl.uint<1>, !firrtl.uint<1> + %clk_prop = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + + firrtl.int.verif.assume %clk_prop, %enable : !firrtl.uint<1>, !firrtl.uint<1> + } else { + // CHECK: [[TMP3A:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK: [[TMP6A:%.+]] = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + // CHECK: [[TMP4A:%.+]] = firrtl.int.ltl.implication [[TMP3A]], [[TMP6A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK: firrtl.int.verif.assume [[TMP4A]], %enable1 : !firrtl.uint<1>, !firrtl.uint<1> + %clk_prop = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + firrtl.int.verif.assume %clk_prop, %enable1 : !firrtl.uint<1>, !firrtl.uint<1> + } +} + +// CHECK-LABEL: firrtl.module @verifcover +firrtl.module @verifcover( + in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, in %prop1 : !firrtl.uint<1>, + in %enable : !firrtl.uint<1>, in %enable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1> +) { + firrtl.when %cond : !firrtl.uint<1> { + // CHECK: [[TMP2A:%.+]] = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + // CHECK: [[TMP0A:%.+]] = firrtl.int.ltl.and %cond, [[TMP2A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK: firrtl.int.verif.cover [[TMP0A]], %enable : !firrtl.uint<1>, !firrtl.uint<1> + %clk_prop = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + + firrtl.int.verif.cover %clk_prop, %enable : !firrtl.uint<1>, !firrtl.uint<1> + } else { + // CHECK: [[TMP3A:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK: [[TMP6A:%.+]] = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + // CHECK: [[TMP4A:%.+]] = firrtl.int.ltl.and [[TMP3A]], [[TMP6A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK: firrtl.int.verif.cover [[TMP4A]], %enable1 : !firrtl.uint<1>, !firrtl.uint<1> + %clk_prop = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> + firrtl.int.verif.cover %clk_prop, %enable1 : !firrtl.uint<1>, !firrtl.uint<1> } } diff --git a/test/Dialect/FIRRTL/lower-intrinsics.mlir b/test/Dialect/FIRRTL/lower-intrinsics.mlir index 0683c0c57b..1962ead766 100644 --- a/test/Dialect/FIRRTL/lower-intrinsics.mlir +++ b/test/Dialect/FIRRTL/lower-intrinsics.mlir @@ -79,8 +79,6 @@ firrtl.circuit "Foo" { // CHECK-NEXT: firrtl.int.ltl.clock %in0, %clk : firrtl.int.generic "circt_ltl_clock" %in0, %clk : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> - // CHECK-NEXT: firrtl.int.ltl.disable %in0, %in1 : - firrtl.int.generic "circt_ltl_disable" %in0, %in1: (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> } // CHECK-LABEL: firrtl.module @Verif( diff --git a/test/Dialect/LTL/basic.mlir b/test/Dialect/LTL/basic.mlir index 7fcdb7ba78..ebaa462047 100644 --- a/test/Dialect/LTL/basic.mlir +++ b/test/Dialect/LTL/basic.mlir @@ -114,5 +114,3 @@ unrealized_conversion_cast %clk0 : !ltl.sequence to index unrealized_conversion_cast %clk1 : !ltl.sequence to index unrealized_conversion_cast %clk2 : !ltl.property to index -// CHECK: ltl.disable {{%.+}} if {{%.+}} : !ltl.property -ltl.disable %p if %true : !ltl.property diff --git a/test/Dialect/LTL/canonicalization.mlir b/test/Dialect/LTL/canonicalization.mlir index 69936c567b..671bd81742 100644 --- a/test/Dialect/LTL/canonicalization.mlir +++ b/test/Dialect/LTL/canonicalization.mlir @@ -128,13 +128,3 @@ func.func @NonConsecutiveRepeatFolds(%arg0: !ltl.sequence) { return } - -// CHECK-LABEL: @ClockingFolds -func.func @ClockingFolds(%arg0: !ltl.property) { - // disable(p, false) -> p - // CHECK-NEXT: call @Prop(%arg0) - %false = hw.constant false - %0 = ltl.disable %arg0 if %false : !ltl.property - call @Prop(%0) : (!ltl.property) -> () - return -} diff --git a/test/Dialect/Verif/canonicalization.mlir b/test/Dialect/Verif/canonicalization.mlir index ca87b2a45a..b84e96e907 100644 --- a/test/Dialect/Verif/canonicalization.mlir +++ b/test/Dialect/Verif/canonicalization.mlir @@ -35,3 +35,24 @@ hw.module @HasBeenReset(in %clock: i1, in %reset: i1) { %constClockS0 = hw.wire %c2 sym @constClockS0 : i1 %constClockS1 = hw.wire %c3 sym @constClockS1 : i1 } + +// CHECK-LABEL: @clockedAssert +hw.module @clockedAssert(in %clock : i1, in %a : i1, in %en : i1) { + // CHECK: verif.clocked_assert %a if %en, posedge %clock : i1 + %clk = ltl.clock %a, posedge %clock : i1 + verif.assert %clk if %en : !ltl.sequence +} + +// CHECK-LABEL: @clockedAssume +hw.module @clockedAssume(in %clock : i1, in %a : i1, in %en : i1) { + // CHECK: verif.clocked_assume %a if %en, posedge %clock : i1 + %clk = ltl.clock %a, posedge %clock : i1 + verif.assume %clk if %en : !ltl.sequence +} + +// CHECK-LABEL: @clockedCover +hw.module @clockedCover(in %clock : i1, in %a : i1, in %en : i1) { + // CHECK: verif.clocked_cover %a if %en, posedge %clock : i1 + %clk = ltl.clock %a, posedge %clock : i1 + verif.cover %clk if %en : !ltl.sequence +} diff --git a/test/Dialect/Verif/verify.mlir b/test/Dialect/Verif/verify.mlir index 7344c1a8fb..ed29a573f4 100644 --- a/test/Dialect/Verif/verify.mlir +++ b/test/Dialect/Verif/verify.mlir @@ -1,33 +1,5 @@ // RUN: circt-opt --verify-clocked-assert-like %s --split-input-file --verify-diagnostics | circt-opt -hw.module @verifyDisables(in %clk: i1, in %a: i1, in %b: i1) { - %n0 = ltl.not %a : i1 - - // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}} - %disabled0 = ltl.disable %n0 if %b : !ltl.property - verif.clocked_assert %disabled0 disable %b clock posedge %clk : !ltl.property -} - -// ----- - -hw.module @verifyDisables1(in %clk: i1, in %a: i1, in %b: i1) { - %n0 = ltl.not %a : i1 - - // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}} - %disabled1 = ltl.disable %n0 if %b : !ltl.property - verif.clocked_assume %disabled1 disable %b clock posedge %clk : !ltl.property -} - -// ----- - -hw.module @verifyDisables2(in %clk: i1, in %a: i1, in %b: i1) { - %n0 = ltl.not %a : i1 - - // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}} - %disabled2 = ltl.disable %n0 if %b : !ltl.property - verif.clocked_cover %disabled2 disable %b clock posedge %clk : !ltl.property -} - // ----- hw.module @verifyClocks(in %clk: i1, in %a: i1, in %b: i1) { @@ -35,7 +7,7 @@ hw.module @verifyClocks(in %clk: i1, in %a: i1, in %b: i1) { // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}} %clocked = ltl.clock %n0, posedge %clk : !ltl.property - verif.clocked_assert %clocked disable %b clock posedge %clk : !ltl.property + verif.clocked_assert %clocked if %b, posedge %clk : !ltl.property } // ----- @@ -45,7 +17,7 @@ hw.module @verifyClocks1(in %clk: i1, in %a: i1, in %b: i1) { // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}} %clocked = ltl.clock %n0, posedge %clk : !ltl.property - verif.clocked_assume %clocked disable %b clock posedge %clk : !ltl.property + verif.clocked_assume %clocked if %b, posedge %clk : !ltl.property } // ----- @@ -55,7 +27,7 @@ hw.module @verifyClocks2(in %clk: i1, in %a: i1, in %b: i1) { // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}} %clocked = ltl.clock %n0, posedge %clk : !ltl.property - verif.clocked_cover %clocked disable %b clock posedge %clk : !ltl.property + verif.clocked_cover %clocked if %b, posedge %clk : !ltl.property } // ----- @@ -70,5 +42,5 @@ hw.module @deeplynested(in %clk: i1, in %a: i1, in %b: i1) { %a1 = ltl.and %b, %i1 : i1, !ltl.property %o1 = ltl.or %b, %a1 : i1, !ltl.property - verif.clocked_assert %o1 disable %b clock posedge %clk : !ltl.property -} \ No newline at end of file + verif.clocked_assert %o1 if %b, posedge %clk : !ltl.property +} diff --git a/test/firtool/btor2-assertproperty.fir b/test/firtool/btor2-assertproperty.fir index 884ab345ad..25bd0a6c37 100644 --- a/test/firtool/btor2-assertproperty.fir +++ b/test/firtool/btor2-assertproperty.fir @@ -17,35 +17,31 @@ circuit Counter : connect count, _count_T_1 node _T_2 = neq(count, UInt<4>(0ha)) node hbr = intrinsic(circt_has_been_reset : UInt<1>, clock, reset) - node disable = eq(hbr, UInt<1>(0h0)) - node ltl_disable = intrinsic(circt_ltl_disable : UInt<1>, _T_2, disable) - node ltl_clock = intrinsic(circt_ltl_clock : UInt<1>, ltl_disable, clock) - intrinsic(circt_verif_assert, ltl_clock) + node ltl_clock = intrinsic(circt_ltl_clock : UInt<1>, _T_2, clock) + intrinsic(circt_verif_assert, ltl_clock, hbr) ; CHECK: 1 sort bitvec 1 ; CHECK: 2 input 1 reset ; CHECK: 3 sort bitvec 32 ; CHECK: 4 state 3 count -; CHECK: 5 constd 1 0 -; CHECK: 6 state 1 hbr -; CHECK: 7 init 1 6 5 +; CHECK: 5 state 1 hbr +; CHECK: 6 constd 1 0 +; CHECK: 7 init 1 5 6 ; CHECK: 8 constd 3 1 ; CHECK: 9 constd 3 10 ; CHECK: 10 constd 3 22 -; CHECK: 11 constd 1 -1 -; CHECK: 12 constd 3 0 -; CHECK: 13 eq 1 4 10 -; CHECK: 14 add 3 4 8 -; CHECK: 15 ite 3 13 12 14 -; CHECK: 16 neq 1 4 9 -; CHECK: 17 constd 1 -1 -; CHECK: 18 or 1 2 6 -; CHECK: 19 xor 1 2 17 -; CHECK: 20 and 1 6 19 -; CHECK: 21 xor 1 20 11 -; CHECK: 22 or 1 21 16 -; CHECK: 23 not 1 22 -; CHECK: 24 bad 23 -; CHECK: 25 ite 3 2 12 15 -; CHECK: 26 next 3 4 25 -; CHECK: 28 next 1 6 27 +; CHECK: 11 constd 3 0 +; CHECK: 12 eq 1 4 10 +; CHECK: 13 add 3 4 8 +; CHECK: 14 ite 3 12 11 13 +; CHECK: 15 neq 1 4 9 +; CHECK: 16 constd 1 -1 +; CHECK: 17 or 1 2 5 +; CHECK: 18 xor 1 2 16 +; CHECK: 19 and 1 5 18 +; CHECK: 20 implies 1 19 15 +; CHECK: 21 not 1 20 +; CHECK: 22 bad 21 +; CHECK: 23 ite 3 2 11 14 +; CHECK: 24 next 3 4 23 +; CHECK: 25 next 1 5 17 diff --git a/test/firtool/extract-test-code.fir b/test/firtool/extract-test-code.fir index 6d16d39311..ca5ce9c57a 100644 --- a/test/firtool/extract-test-code.fir +++ b/test/firtool/extract-test-code.fir @@ -44,13 +44,14 @@ circuit Top: ; CHECK: module Top_assert( ; CHECK-NOT: endmodule - ; CHECK: foo: assert property (cond); + ; CHECK: foo: assert property (disable iff (~(en)) cond); ; CHECK: endmodule public module Top: input clock : Clock - input cond : UInt<1> - output out : UInt<1> + input cond : UInt<1> + input en : UInt<1> + output out : UInt<1> inst instance_extracted of InstanceExtracted connect instance_extracted.clock, clock @@ -61,4 +62,4 @@ circuit Top: connect input_only.clock, clock connect input_only.cond, cond - intrinsic(circt_verif_assert, cond) + intrinsic(circt_verif_assert, cond, en)