From 2f8ba28db8642bf36e9ea26f2792e059dda3f57f Mon Sep 17 00:00:00 2001 From: Amelia Dobis Date: Fri, 12 Jul 2024 10:34:04 -0700 Subject: [PATCH] [SV] Add Intermediary Assert Op for better enable polarity flip (#7302) This PR introduces a new assert property op to the sv dialect and uses that as an intermediary for property assertion emission. This should solve the issue of the polarity being different in SV and in verif for the enable signals ( enable in verif, disable in sv ). --- include/circt/Dialect/SV/SVDialect.td | 3 +- include/circt/Dialect/SV/SVOps.h | 2 + include/circt/Dialect/SV/SVVerification.td | 54 +++++ include/circt/Dialect/SV/SVVisitors.h | 6 +- .../ExportVerilog/ExportVerilog.cpp | 214 ++++++------------ .../ExportVerilog/LegalizeNames.cpp | 15 +- .../ExportVerilog/PrepareForEmission.cpp | 28 +++ lib/Conversion/VerifToSV/VerifToSV.cpp | 90 +++++++- lib/Dialect/SV/CMakeLists.txt | 1 + lib/Dialect/SV/SVOps.cpp | 30 +++ test/Conversion/ExportVerilog/verif.mlir | 182 ++++++++------- test/firtool/extract-test-code.fir | 3 +- 12 files changed, 383 insertions(+), 245 deletions(-) diff --git a/include/circt/Dialect/SV/SVDialect.td b/include/circt/Dialect/SV/SVDialect.td index 041564099c87..a8f4e2f8eb8a 100644 --- a/include/circt/Dialect/SV/SVDialect.td +++ b/include/circt/Dialect/SV/SVDialect.td @@ -22,7 +22,8 @@ def SVDialect : Dialect { This dialect defines the `sv` dialect, which represents various SystemVerilog-specific constructs in an AST-like representation. }]; - let dependentDialects = ["circt::comb::CombDialect", "circt::hw::HWDialect"]; + let dependentDialects = ["circt::comb::CombDialect", "circt::hw::HWDialect", + "circt::ltl::LTLDialect"]; let useDefaultTypePrinterParser = 1; let useDefaultAttributePrinterParser = 1; diff --git a/include/circt/Dialect/SV/SVOps.h b/include/circt/Dialect/SV/SVOps.h index a8b80a036ddd..91347d1512e1 100644 --- a/include/circt/Dialect/SV/SVOps.h +++ b/include/circt/Dialect/SV/SVOps.h @@ -15,6 +15,8 @@ #include "circt/Dialect/HW/HWAttributes.h" #include "circt/Dialect/HW/HWOps.h" +#include "circt/Dialect/LTL/LTLDialect.h" +#include "circt/Dialect/LTL/LTLTypes.h" #include "circt/Dialect/SV/SVAttributes.h" #include "circt/Dialect/SV/SVDialect.h" #include "circt/Dialect/SV/SVTypes.h" diff --git a/include/circt/Dialect/SV/SVVerification.td b/include/circt/Dialect/SV/SVVerification.td index ee0e6037ef62..c1f8da6aea13 100644 --- a/include/circt/Dialect/SV/SVVerification.td +++ b/include/circt/Dialect/SV/SVVerification.td @@ -10,6 +10,7 @@ // declarations. // //===----------------------------------------------------------------------===// +include "circt/Dialect/LTL/LTLTypes.td" /// Immediate assertions, like `assert`. def ImmediateAssert: I32EnumAttrCase<"Immediate", 0, "immediate">; @@ -159,3 +160,56 @@ def CoverConcurrentOp : ConcurrentVerifOp<"cover.concurrent", section 16.5 of the SystemVerilog 2017 specification. }]; } + + +/// Property Assertions/Assumptions/Cover analogous to SVA property verification ops. +class PropertyVerifOp traits = [AttrSizedOperandSegments]> : + SVOp { + let arguments = (ins + LTLAnyPropertyType:$property, + OptionalAttr:$event, Optional:$clock, + Optional:$disable, + OptionalAttr:$label); + + let assemblyFormat = [{ + $property (`on` $event^)? ($clock^)? (`disable_iff` $disable^)? + (`label` $label^)? attr-dict `:` type($property) + }]; + + let builders = [ + // no clock or event + OpBuilder<(ins "mlir::Value":$property, + "mlir::Value":$disable, + CArg<"StringAttr","StringAttr()">: $label), + [{ build(odsBuilder, odsState, property, EventControlAttr{}, Value(), disable, label); }]> + ]; + + let hasVerifier = true; +} + +def AssertPropertyOp : PropertyVerifOp<"assert_property"> { + let summary = "property assertion -- can be disabled and clocked"; + let description = [{ + Assert that a given SVA-style property holds. This is only checked when + the disable signal is low and a clock event occurs. This is analogous to + the verif.assert operation, but with a flipped enable polarity. + }]; +} + +def AssumePropertyOp : PropertyVerifOp<"assume_property"> { + let summary = "property assumption -- can be disabled and clocked"; + let description = [{ + Assume that a given SVA-style property holds. This is only considered when + the disable signal is low and a clock event occurs. This is analogous to + the verif.assume operation, but with a flipped enable polarity. + }]; +} + +def CoverPropertyOp : PropertyVerifOp<"cover_property"> { + let summary = "property cover point -- can be disabled and clocked"; + let description = [{ + Cover when a given SVA-style property holds. This is only checked when + the disable signal is low and a clock event occurs. This is analogous to + the verif.cover operation, but with a flipped enable polarity. + }]; +} diff --git a/include/circt/Dialect/SV/SVVisitors.h b/include/circt/Dialect/SV/SVVisitors.h index 4fdc1c8f4a50..eeb173751222 100644 --- a/include/circt/Dialect/SV/SVVisitors.h +++ b/include/circt/Dialect/SV/SVVisitors.h @@ -48,7 +48,8 @@ class Visitor { FuncDPIImportOp, // Verification statements. AssertOp, AssumeOp, CoverOp, AssertConcurrentOp, AssumeConcurrentOp, - CoverConcurrentOp, + CoverConcurrentOp, AssertPropertyOp, AssumePropertyOp, + CoverPropertyOp, // Bind Statements BindOp, // Simulator control tasks @@ -154,6 +155,9 @@ class Visitor { HANDLE(AssertConcurrentOp, Unhandled); HANDLE(AssumeConcurrentOp, Unhandled); HANDLE(CoverConcurrentOp, Unhandled); + HANDLE(AssertPropertyOp, Unhandled); + HANDLE(AssumePropertyOp, Unhandled); + HANDLE(CoverPropertyOp, Unhandled); // Bind statements. HANDLE(BindOp, Unhandled); diff --git a/lib/Conversion/ExportVerilog/ExportVerilog.cpp b/lib/Conversion/ExportVerilog/ExportVerilog.cpp index 3d964cd066f4..8ecd406323d3 100644 --- a/lib/Conversion/ExportVerilog/ExportVerilog.cpp +++ b/lib/Conversion/ExportVerilog/ExportVerilog.cpp @@ -74,18 +74,6 @@ using namespace pretty; StringRef circtHeader = "circt_header.svh"; StringRef circtHeaderInclude = "`include \"circt_header.svh\"\n"; -static ltl::ClockEdge verifToltlClockEdge(verif::ClockEdge ce) { - switch (ce) { - case verif::ClockEdge::Pos: - return ltl::ClockEdge::Pos; - case verif::ClockEdge::Neg: - return ltl::ClockEdge::Neg; - case verif::ClockEdge::Both: - return ltl::ClockEdge::Both; - } - llvm_unreachable("Unknown event control kind"); -} - namespace { /// This enum keeps track of the precedence level of various binary operators, /// where a lower number binds tighter. @@ -3450,28 +3438,25 @@ class PropertyEmitter : public EmitterBase, assert(state.pp.getListener() == &state.saver); } - /// 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, + void emitAssertPropertyDisable( + Value property, Value disable, PropertyPrecedence parenthesizeIfLooserThan = PropertyPrecedence::Lowest); - // Emits a property that is directly associated to a single clock and a single - // 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, + void emitAssertPropertyBody( + Value property, Value disable, PropertyPrecedence parenthesizeIfLooserThan = PropertyPrecedence::Lowest); -private: - using ltl::Visitor::visitLTL; - friend class ltl::Visitor; + void emitAssertPropertyBody( + Value property, sv::EventControl event, Value clock, Value disable, + PropertyPrecedence parenthesizeIfLooserThan = PropertyPrecedence::Lowest); +private: /// Emit the specified value as an SVA property or sequence. EmittedProperty emitNestedProperty(Value property, PropertyPrecedence parenthesizeIfLooserThan); + using ltl::Visitor::visitLTL; + friend class ltl::Visitor; EmittedProperty visitUnhandledLTL(Operation *op); EmittedProperty visitLTL(ltl::AndOp op); @@ -3509,22 +3494,36 @@ class PropertyEmitter : public EmitterBase, }; } // end anonymous namespace -void PropertyEmitter::emitEnabledProperty( - Value property, Value enable, PropertyPrecedence parenthesizeIfLooserThan) { - assert(localTokens.empty()); - - // If the property is tied to an enable, emit that. - if (enable) { - ps << "disable iff" << PP::nbsp << "(~("; +// Emits a disable signal and its containing property. +// This function can be called from withing another emission process in which +// case we don't need to check that the local tokens are empty. +void PropertyEmitter::emitAssertPropertyDisable( + Value property, Value disable, + PropertyPrecedence parenthesizeIfLooserThan) { + // If the property is tied to a disable, emit that. + if (disable) { + ps << "disable iff" << PP::nbsp << "("; ps.scopedBox(PP::ibox2, [&] { - emitNestedProperty(enable, PropertyPrecedence::Unary); - ps << "))"; + emitNestedProperty(disable, PropertyPrecedence::Unary); + ps << ")"; }); ps << PP::space; } ps.scopedBox(PP::ibox0, [&] { emitNestedProperty(property, parenthesizeIfLooserThan); }); +} + +// Emits a disable signal and its containing property. +// This function can be called from withing another emission process in which +// case we don't need to check that the local tokens are empty. +void PropertyEmitter::emitAssertPropertyBody( + Value property, Value disable, + PropertyPrecedence parenthesizeIfLooserThan) { + assert(localTokens.empty()); + + emitAssertPropertyDisable(property, disable, parenthesizeIfLooserThan); + // If we are not using an external token buffer provided through the // constructor, but we're using the default `PropertyEmitter`-scoped buffer, // flush it. @@ -3532,31 +3531,22 @@ void PropertyEmitter::emitEnabledProperty( buffer.flush(state.pp); } -void PropertyEmitter::emitClockedProperty( - Value property, Value clock, ltl::ClockEdge edge, Value enable, +void PropertyEmitter::emitAssertPropertyBody( + Value property, sv::EventControl event, Value clock, Value disable, PropertyPrecedence parenthesizeIfLooserThan) { assert(localTokens.empty()); // Wrap to this column. ps << "@("; ps.scopedBox(PP::ibox2, [&] { - ps << PPExtString(stringifyClockEdge(edge)) << PP::space; + ps << PPExtString(stringifyEventControl(event)) << PP::space; emitNestedProperty(clock, PropertyPrecedence::Lowest); ps << ")"; }); + ps << PP::space; - // 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 << "))"; - }); - } + // Emit the rest of the body + emitAssertPropertyDisable(property, disable, parenthesizeIfLooserThan); - ps << PP::space; - ps.scopedBox(PP::ibox0, - [&] { emitNestedProperty(property, parenthesizeIfLooserThan); }); // If we are not using an external token buffer provided through the // constructor, but we're using the default `PropertyEmitter`-scoped buffer, // flush it. @@ -3996,6 +3986,11 @@ class StmtEmitter : public EmitterBase, LogicalResult visitSV(AssertConcurrentOp op); LogicalResult visitSV(AssumeConcurrentOp op); LogicalResult visitSV(CoverConcurrentOp op); + template + LogicalResult emitPropertyAssertion(Op op, PPExtString opName); + LogicalResult visitSV(AssertPropertyOp op); + LogicalResult visitSV(AssumePropertyOp op); + LogicalResult visitSV(CoverPropertyOp op); LogicalResult visitSV(BindOp op); LogicalResult visitSV(InterfaceOp op); @@ -4008,19 +4003,6 @@ class StmtEmitter : public EmitterBase, const SmallPtrSetImpl &locationOps, StringRef multiLineComment = StringRef()); - 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 clock, verif::ClockEdge edge, - Value enable, PPExtString opName); - LogicalResult visitVerif(verif::ClockedAssertOp op); - LogicalResult visitVerif(verif::ClockedAssumeOp op); - LogicalResult visitVerif(verif::ClockedCoverOp op); - LogicalResult visitSV(FuncDPIImportOp op); template LogicalResult emitFunctionCall(CallOp callOp); @@ -4881,11 +4863,10 @@ LogicalResult StmtEmitter::visitSV(CoverConcurrentOp op) { return emitConcurrentAssertion(op, PPExtString("cover")); } -/// 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) { +// Property assertions are what gets emitted if the user want to combine +// concurrent assertions with a disable signal, a clock and an ltl property. +template +LogicalResult StmtEmitter::emitPropertyAssertion(Op op, PPExtString opName) { if (hasSVAttributes(op)) emitError(op, "SV attributes emission is unimplemented for the op"); @@ -4898,6 +4879,7 @@ LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property, // outside procedural code" and 16.14.6 "Embedding concurrent assertions in // procedural code". Operation *parent = op->getParentOp(); + Value property = op.getProperty(); bool isTemporal = !property.getType().isSignlessInteger(1); bool isProcedural = parent->hasTrait(); bool emitAsImmediate = !isTemporal && isProcedural; @@ -4907,77 +4889,28 @@ LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property, ops.insert(op); ps.addCallback({op, true}); ps.scopedBox(PP::ibox2, [&]() { + // Check for a label and emit it if necessary emitAssertionLabel(op); + // Emit the assertion ps.scopedBox(PP::cbox0, [&]() { if (emitAsImmediate) ps << opName << "("; else ps << opName << PP::nbsp << "property" << PP::nbsp << "("; - ps.scopedBox(PP::ibox2, [&]() { - PropertyEmitter(emitter, ops).emitEnabledProperty(property, enable); - ps << ");"; - }); - }); - }); - ps.addCallback({op, false}); - emitLocationInfoAndNewLine(ops); - return success(); -} - -LogicalResult StmtEmitter::visitVerif(verif::AssertOp op) { - return emitVerifAssertLike(op, op.getProperty(), op.getEnable(), - PPExtString("assert")); -} - -LogicalResult StmtEmitter::visitVerif(verif::AssumeOp op) { - return emitVerifAssertLike(op, op.getProperty(), op.getEnable(), - PPExtString("assume")); -} - -LogicalResult StmtEmitter::visitVerif(verif::CoverOp op) { - 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 clock, verif::ClockEdge edge, - Value enable, PPExtString opName) { - if (hasSVAttributes(op)) - emitError(op, "SV attributes emission is unimplemented for the op"); - - // If we are inside a procedural region we have the option of emitting either - // an `assert` or `assert property`. If we are in a non-procedural region, - // e.g., the body of a module, we have to use the concurrent form `assert - // property` (which also supports plain booleans). - // - // 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 = parent->hasTrait(); - bool emitAsImmediate = !isTemporal && isProcedural; - - startStatement(); - SmallPtrSet ops; - ops.insert(op); - ps.addCallback({op, true}); - ps.scopedBox(PP::ibox2, [&]() { - emitAssertionLabel(op); - ps.scopedBox(PP::cbox0, [&]() { - if (emitAsImmediate) - ps << opName << "("; + // Event only exists if the clock exists + Value clock = op.getClock(); + auto event = op.getEvent(); + if (clock) + ps.scopedBox(PP::ibox2, [&]() { + PropertyEmitter(emitter, ops) + .emitAssertPropertyBody(property, *event, clock, op.getDisable()); + }); else - ps << opName << PP::nbsp << "property" << PP::nbsp << "("; - ps.scopedBox(PP::ibox2, [&]() { - PropertyEmitter(emitter, ops) - .emitClockedProperty(property, clock, verifToltlClockEdge(edge), - enable); - ps << ");"; - }); + ps.scopedBox(PP::ibox2, [&]() { + PropertyEmitter(emitter, ops) + .emitAssertPropertyBody(property, op.getDisable()); + }); + ps << ");"; }); }); ps.addCallback({op, false}); @@ -4985,23 +4918,16 @@ StmtEmitter::emitVerifClockedAssertLike(Operation *op, Value property, return success(); } -// FIXME: emit property assertion wrapped in a clock and disabled -LogicalResult StmtEmitter::visitVerif(verif::ClockedAssertOp op) { - return emitVerifClockedAssertLike(op, op.getProperty(), op.getClock(), - op.getEdge(), op.getEnable(), - PPExtString("assert")); +LogicalResult StmtEmitter::visitSV(AssertPropertyOp op) { + return emitPropertyAssertion(op, PPExtString("assert")); } -LogicalResult StmtEmitter::visitVerif(verif::ClockedAssumeOp op) { - return emitVerifClockedAssertLike(op, op.getProperty(), op.getClock(), - op.getEdge(), op.getEnable(), - PPExtString("assume")); +LogicalResult StmtEmitter::visitSV(AssumePropertyOp op) { + return emitPropertyAssertion(op, PPExtString("assume")); } -LogicalResult StmtEmitter::visitVerif(verif::ClockedCoverOp op) { - return emitVerifClockedAssertLike(op, op.getProperty(), op.getClock(), - op.getEdge(), op.getEnable(), - PPExtString("cover")); +LogicalResult StmtEmitter::visitSV(CoverPropertyOp op) { + return emitPropertyAssertion(op, PPExtString("cover")); } LogicalResult StmtEmitter::emitIfDef(Operation *op, MacroIdentAttr cond) { diff --git a/lib/Conversion/ExportVerilog/LegalizeNames.cpp b/lib/Conversion/ExportVerilog/LegalizeNames.cpp index a945a46f0dea..ad9b736d6a01 100644 --- a/lib/Conversion/ExportVerilog/LegalizeNames.cpp +++ b/lib/Conversion/ExportVerilog/LegalizeNames.cpp @@ -207,7 +207,8 @@ static void legalizeModuleLocalNames(HWEmittableModuleLike module, } else if (auto forOp = dyn_cast(op)) { nameEntries.emplace_back(op, forOp.getInductionVarNameAttr()); } else if (isa(op)) { // Notice and renamify the labels on verification statements. if (auto labelAttr = op->getAttrOfType("label")) @@ -217,12 +218,12 @@ static void legalizeModuleLocalNames(HWEmittableModuleLike module, // name from verificaiton kinds. StringRef defaultName = llvm::TypeSwitch(op) - .Case( - [](auto) { return "assert"; }) - .Case( - [](auto) { return "cover"; }) - .Case( - [](auto) { return "assume"; }); + .Case([](auto) { return "assert"; }) + .Case([](auto) { return "cover"; }) + .Case([](auto) { return "assume"; }); nameEntries.emplace_back( op, StringAttr::get(op->getContext(), defaultName)); } diff --git a/lib/Conversion/ExportVerilog/PrepareForEmission.cpp b/lib/Conversion/ExportVerilog/PrepareForEmission.cpp index a8c39405e29c..d8da392cc054 100644 --- a/lib/Conversion/ExportVerilog/PrepareForEmission.cpp +++ b/lib/Conversion/ExportVerilog/PrepareForEmission.cpp @@ -1315,6 +1315,31 @@ static LogicalResult legalizeHWModule(Block &block, return success(); } +// Adds a wire to disable signals to allow for the polarity flip of the +// enable signal to happen legally (diable iff must not contain ~). +static void wireDisableSignals(hw::HWEmittableModuleLike module) { + + module.walk([&](Operation *op) { + TypeSwitch(op) + .Case( + [&](auto assertLike) { + OpBuilder builder(assertLike); + if (auto disable = assertLike.getDisable()) { + Value wdisable = builder.createOrFold( + assertLike.getLoc(), + IntegerType::get(assertLike.getContext(), 1)); + // Assign the wire to the disable and read its value + builder.createOrFold(assertLike.getLoc(), + wdisable, disable); + Value read = builder.createOrFold( + assertLike.getLoc(), wdisable); + assertLike.getDisableMutable().assign(read); + } + }) + .Default([&](auto) {}); + }); +} + // NOLINTNEXTLINE(misc-no-recursion) LogicalResult ExportVerilog::prepareHWModule(hw::HWEmittableModuleLike module, const LoweringOptions &options) { @@ -1332,6 +1357,9 @@ LogicalResult ExportVerilog::prepareHWModule(hw::HWEmittableModuleLike module, EmittedExpressionStateManager expressionStateManager(options); // Spill wires to prettify verilog outputs. prettifyAfterLegalization(*module.getBodyBlock(), expressionStateManager); + + // Make sure that assertions have their disable signals spilled to wires + wireDisableSignals(module); return success(); } diff --git a/lib/Conversion/VerifToSV/VerifToSV.cpp b/lib/Conversion/VerifToSV/VerifToSV.cpp index 620822ac3631..3b31659b3a87 100644 --- a/lib/Conversion/VerifToSV/VerifToSV.cpp +++ b/lib/Conversion/VerifToSV/VerifToSV.cpp @@ -14,6 +14,7 @@ #include "circt/Dialect/Comb/CombOps.h" #include "circt/Dialect/HW/HWOpInterfaces.h" #include "circt/Dialect/HW/HWOps.h" +#include "circt/Dialect/SV/SVDialect.h" #include "circt/Dialect/SV/SVOps.h" #include "circt/Dialect/Verif/VerifOps.h" #include "mlir/Pass/Pass.h" @@ -35,7 +36,6 @@ using namespace verif; //===----------------------------------------------------------------------===// namespace { - struct PrintOpConversionPattern : public OpConversionPattern { using OpConversionPattern::OpConversionPattern; @@ -128,6 +128,78 @@ struct HasBeenResetConversion : public OpConversionPattern { } }; +// Conversion from one event control enum to another +static sv::EventControl verifToSVEventControl(verif::ClockEdge ce) { + switch (ce) { + case verif::ClockEdge::Pos: + return sv::EventControl::AtPosEdge; + case verif::ClockEdge::Neg: + return sv::EventControl::AtNegEdge; + case verif::ClockEdge::Both: + return sv::EventControl::AtEdge; + } + llvm_unreachable("Unknown event control kind"); +} + +// Generic conversion for verif.assert, verif.assume and verif.cover +template +struct VerifAssertLikeConversion : public OpConversionPattern { + using OpConversionPattern::OpConversionPattern; + using OpAdaptor = typename OpConversionPattern::OpAdaptor; + + // Convert the verif.assert like op that uses an enable, into an equivalent + // sv.assert_property op that has the negated enable as its disable. + LogicalResult + matchAndRewrite(Op op, OpAdaptor operands, + ConversionPatternRewriter &rewriter) const override { + // Negate the enable if it exists + Value disable; + if (auto enable = operands.getEnable()) { + Value constOne = rewriter.createOrFold( + op.getLoc(), rewriter.getI1Type(), 1); + disable = + rewriter.createOrFold(op.getLoc(), enable, constOne); + } + + rewriter.replaceOpWithNewOp(op, operands.getProperty(), disable, + operands.getLabelAttr()); + + return success(); + } +}; + +// Generic conversion for verif.clocked_assert, verif.clocked_assume and +// verif.clocked_cover +template +struct VerifClockedAssertLikeConversion : public OpConversionPattern { + using OpConversionPattern::OpConversionPattern; + using OpAdaptor = typename OpConversionPattern::OpAdaptor; + + // Convert the verif.assert like op that uses an enable, into an equivalent + // sv.assert_property op that has the negated enable as its disable. + LogicalResult + matchAndRewrite(Op op, OpAdaptor operands, + ConversionPatternRewriter &rewriter) const override { + // Negate the enable if it exists + Value disable; + if (auto enable = operands.getEnable()) { + Value constOne = rewriter.createOrFold( + op.getLoc(), rewriter.getI1Type(), 1); + disable = + rewriter.createOrFold(op.getLoc(), enable, constOne); + } + // Convert a verif clock edge into an sv event control + auto eventattr = sv::EventControlAttr::get( + op.getContext(), verifToSVEventControl(operands.getEdge())); + + rewriter.replaceOpWithNewOp(op, operands.getProperty(), eventattr, + operands.getClock(), disable, + operands.getLabelAttr()); + + return success(); + } +}; + } // namespace //===----------------------------------------------------------------------===// @@ -147,9 +219,21 @@ void VerifToSVPass::runOnOperation() { ConversionTarget target(context); RewritePatternSet patterns(&context); - target.addIllegalOp(); + target.addIllegalOp(); target.addLegalDialect(); - patterns.add(&context); + patterns.add< + PrintOpConversionPattern, HasBeenResetConversion, + VerifAssertLikeConversion, + VerifAssertLikeConversion, + VerifAssertLikeConversion, + VerifClockedAssertLikeConversion, + VerifClockedAssertLikeConversion, + VerifClockedAssertLikeConversion>( + &context); if (failed(applyPartialConversion(module, target, std::move(patterns)))) signalPassFailure(); diff --git a/lib/Dialect/SV/CMakeLists.txt b/lib/Dialect/SV/CMakeLists.txt index 1aa348e93e28..c07b4407884a 100644 --- a/lib/Dialect/SV/CMakeLists.txt +++ b/lib/Dialect/SV/CMakeLists.txt @@ -16,6 +16,7 @@ add_circt_dialect_library(CIRCTSV LINK_LIBS PUBLIC CIRCTComb CIRCTHW + CIRCTLTL CIRCTSupport MLIRIR ) diff --git a/lib/Dialect/SV/SVOps.cpp b/lib/Dialect/SV/SVOps.cpp index a0f779f2fd38..6929f445c1dd 100644 --- a/lib/Dialect/SV/SVOps.cpp +++ b/lib/Dialect/SV/SVOps.cpp @@ -2433,6 +2433,36 @@ FuncDPIImportOp::verifySymbolUses(SymbolTableCollection &symbolTable) { return success(); } +//===----------------------------------------------------------------------===// +// Assert Property Like ops +//===----------------------------------------------------------------------===// + +namespace AssertPropertyLikeOp { +// Check that a clock is never given without an event +// and that an event is never given with a clock. +static LogicalResult verify(Value clock, bool eventExists, mlir::Location loc) { + if ((!clock && eventExists) || (clock && !eventExists)) + return mlir::emitError( + loc, "Every clock must be associated to an even and vice-versa!"); + return success(); +} +} // namespace AssertPropertyLikeOp + +LogicalResult AssertPropertyOp::verify() { + return AssertPropertyLikeOp::verify(getClock(), getEvent().has_value(), + getLoc()); +} + +LogicalResult AssumePropertyOp::verify() { + return AssertPropertyLikeOp::verify(getClock(), getEvent().has_value(), + getLoc()); +} + +LogicalResult CoverPropertyOp::verify() { + return AssertPropertyLikeOp::verify(getClock(), getEvent().has_value(), + getLoc()); +} + //===----------------------------------------------------------------------===// // TableGen generated logic. //===----------------------------------------------------------------------===// diff --git a/test/Conversion/ExportVerilog/verif.mlir b/test/Conversion/ExportVerilog/verif.mlir index dd3cde019e1f..bcf2e9efefcb 100644 --- a/test/Conversion/ExportVerilog/verif.mlir +++ b/test/Conversion/ExportVerilog/verif.mlir @@ -5,14 +5,14 @@ hw.module @Labels(in %a: i1) { // CHECK: foo1: assert property (a); // CHECK: foo2: assume property (a); // CHECK: foo3: cover property (a); - verif.assert %a {label = "foo1"} : i1 - verif.assume %a {label = "foo2"} : i1 - verif.cover %a {label = "foo3"} : i1 + sv.assert_property %a label "foo1" : i1 + sv.assume_property %a label "foo2" : i1 + sv.cover_property %a label "foo3" : i1 // CHECK: bar: assert property (a); // CHECK: bar_0: assert property (a); - verif.assert %a {label = "bar"} : i1 - verif.assert %a {label = "bar"} : i1 + sv.assert_property %a label "bar" : i1 + sv.assert_property %a label "bar" : i1 } // CHECK-LABEL: module BasicEmissionNonTemporal @@ -22,9 +22,9 @@ hw.module @BasicEmissionNonTemporal(in %a: i1, in %b: i1) { // CHECK: assert property (a); // CHECK: assume property (a & b); // CHECK: cover property (a | b); - verif.assert %a : i1 - verif.assume %0 : i1 - verif.cover %1 : i1 + sv.assert_property %a : i1 + sv.assume_property %0 : i1 + sv.cover_property %1 : i1 // CHECK: initial begin sv.initial { @@ -33,9 +33,9 @@ hw.module @BasicEmissionNonTemporal(in %a: i1, in %b: i1) { // CHECK: assert(a); // CHECK: assume(a ^ b); // CHECK: cover(a & b); - verif.assert %a : i1 - verif.assume %2 : i1 - verif.cover %3 : i1 + sv.assert_property %a : i1 + sv.assume_property %2 : i1 + sv.cover_property %3 : i1 } } @@ -45,18 +45,18 @@ hw.module @BasicEmissionTemporal(in %a: i1) { // CHECK: assert property (not a); // CHECK: assume property (not a); // CHECK: cover property (not a); - verif.assert %p : !ltl.property - verif.assume %p : !ltl.property - verif.cover %p : !ltl.property + sv.assert_property %p : !ltl.property + sv.assume_property %p : !ltl.property + sv.cover_property %p : !ltl.property // CHECK: initial begin sv.initial { // CHECK: assert property (not a); // CHECK: assume property (not a); // CHECK: cover property (not a); - verif.assert %p : !ltl.property - verif.assume %p : !ltl.property - verif.cover %p : !ltl.property + sv.assert_property %p : !ltl.property + sv.assume_property %p : !ltl.property + sv.cover_property %p : !ltl.property } } @@ -64,103 +64,103 @@ hw.module @BasicEmissionTemporal(in %a: i1) { hw.module @Sequences(in %clk: i1, in %a: i1, in %b: i1) { // CHECK: assert property (##0 a); %d0 = ltl.delay %a, 0, 0 : i1 - verif.assert %d0 : !ltl.sequence + sv.assert_property %d0 : !ltl.sequence // CHECK: assert property (##4 a); %d1 = ltl.delay %a, 4, 0 : i1 - verif.assert %d1 : !ltl.sequence + sv.assert_property %d1 : !ltl.sequence // CHECK: assert property (##[5:6] a); %d2 = ltl.delay %a, 5, 1 : i1 - verif.assert %d2 : !ltl.sequence + sv.assert_property %d2 : !ltl.sequence // CHECK: assert property (##[7:$] a); %d3 = ltl.delay %a, 7 : i1 - verif.assert %d3 : !ltl.sequence + sv.assert_property %d3 : !ltl.sequence // CHECK: assert property (##[*] a); %d4 = ltl.delay %a, 0 : i1 - verif.assert %d4 : !ltl.sequence + sv.assert_property %d4 : !ltl.sequence // CHECK: assert property (##[+] a); %d5 = ltl.delay %a, 1 : i1 - verif.assert %d5 : !ltl.sequence + sv.assert_property %d5 : !ltl.sequence // CHECK: assert property (a ##0 a); %c0 = ltl.concat %a, %a : i1, i1 - verif.assert %c0 : !ltl.sequence + sv.assert_property %c0 : !ltl.sequence // CHECK: assert property (a ##4 a); %c1 = ltl.concat %a, %d1 : i1, !ltl.sequence - verif.assert %c1 : !ltl.sequence + sv.assert_property %c1 : !ltl.sequence // CHECK: assert property (a ##4 a ##[5:6] a); %c2 = ltl.concat %a, %d1, %d2 : i1, !ltl.sequence, !ltl.sequence - verif.assert %c2 : !ltl.sequence + sv.assert_property %c2 : !ltl.sequence // CHECK: assert property (##4 a ##[5:6] a ##[7:$] a); %c3 = ltl.concat %d1, %d2, %d3 : !ltl.sequence, !ltl.sequence, !ltl.sequence - verif.assert %c3 : !ltl.sequence + sv.assert_property %c3 : !ltl.sequence // CHECK: assert property (a and b); %g0 = ltl.and %a, %b : i1, i1 - verif.assert %g0 : !ltl.sequence + sv.assert_property %g0 : !ltl.sequence // CHECK: assert property (a ##0 a and a ##4 a); %g1 = ltl.and %c0, %c1 : !ltl.sequence, !ltl.sequence - verif.assert %g1 : !ltl.sequence + sv.assert_property %g1 : !ltl.sequence // CHECK: assert property (a or b); %g2 = ltl.or %a, %b : i1, i1 - verif.assert %g2 : !ltl.sequence + sv.assert_property %g2 : !ltl.sequence // CHECK: assert property (a ##0 a or a ##4 a); %g3 = ltl.or %c0, %c1 : !ltl.sequence, !ltl.sequence - verif.assert %g3 : !ltl.sequence + sv.assert_property %g3 : !ltl.sequence // CHECK: assert property (a[*0]); %r0 = ltl.repeat %a, 0, 0 : i1 - verif.assert %r0 : !ltl.sequence + sv.assert_property %r0 : !ltl.sequence // CHECK: assert property (a[*4]); %r1 = ltl.repeat %a, 4, 0 : i1 - verif.assert %r1 : !ltl.sequence + sv.assert_property %r1 : !ltl.sequence // CHECK: assert property (a[*5:6]); %r2 = ltl.repeat %a, 5, 1 : i1 - verif.assert %r2 : !ltl.sequence + sv.assert_property %r2 : !ltl.sequence // CHECK: assert property (a[*7:$]); %r3 = ltl.repeat %a, 7 : i1 - verif.assert %r3 : !ltl.sequence + sv.assert_property %r3 : !ltl.sequence // CHECK: assert property (a[*]); %r4 = ltl.repeat %a, 0 : i1 - verif.assert %r4 : !ltl.sequence + sv.assert_property %r4 : !ltl.sequence // CHECK: assert property (a[+]); %r5 = ltl.repeat %a, 1 : i1 - verif.assert %r5 : !ltl.sequence + sv.assert_property %r5 : !ltl.sequence // CHECK: assert property (a[->0]); %gtr0 = ltl.goto_repeat %a, 0, 0 : i1 - verif.assert %gtr0 : !ltl.sequence + sv.assert_property %gtr0 : !ltl.sequence // CHECK: assert property (a[->4]); %gtr1 = ltl.goto_repeat %a, 4, 0 : i1 - verif.assert %gtr1 : !ltl.sequence + sv.assert_property %gtr1 : !ltl.sequence // CHECK: assert property (a[->5:6]); %gtr2 = ltl.goto_repeat %a, 5, 1 : i1 - verif.assert %gtr2 : !ltl.sequence + sv.assert_property %gtr2 : !ltl.sequence // CHECK: assert property (a[=0]); %ncr0 = ltl.non_consecutive_repeat %a, 0, 0 : i1 - verif.assert %ncr0 : !ltl.sequence + sv.assert_property %ncr0 : !ltl.sequence // CHECK: assert property (a[=4]); %ncr1 = ltl.non_consecutive_repeat %a, 4, 0 : i1 - verif.assert %ncr1 : !ltl.sequence + sv.assert_property %ncr1 : !ltl.sequence // CHECK: assert property (a[=5:6]); %ncr2 = ltl.non_consecutive_repeat %a, 5, 1 : i1 - verif.assert %ncr2 : !ltl.sequence + sv.assert_property %ncr2 : !ltl.sequence // CHECK: assert property (@(posedge clk) a); %k0 = ltl.clock %a, posedge %clk : i1 - verif.assert %k0 : !ltl.sequence + sv.assert_property %k0 : !ltl.sequence // CHECK: assert property (@(negedge clk) a); %k1 = ltl.clock %a, negedge %clk : i1 - verif.assert %k1 : !ltl.sequence + sv.assert_property %k1 : !ltl.sequence // CHECK: assert property (@(edge clk) a); %k2 = ltl.clock %a, edge %clk : i1 - verif.assert %k2 : !ltl.sequence + sv.assert_property %k2 : !ltl.sequence // CHECK: assert property (@(posedge clk) ##4 a); %k3 = ltl.clock %d1, posedge %clk : !ltl.sequence - verif.assert %k3 : !ltl.sequence + sv.assert_property %k3 : !ltl.sequence // CHECK: assert property (b ##0 (@(posedge clk) a)); %k4 = ltl.concat %b, %k0 : i1, !ltl.sequence - verif.assert %k4 : !ltl.sequence + sv.assert_property %k4 : !ltl.sequence } // CHECK-LABEL: module Properties @@ -169,43 +169,41 @@ hw.module @Properties(in %clk: i1, in %a: i1, in %b: i1) { // CHECK: assert property (not a); %n0 = ltl.not %a : i1 - verif.assert %n0 : !ltl.property + sv.assert_property %n0 : !ltl.property // CHECK: assert property (a |-> b); // CHECK: assert property (a ##1 b |-> not a); // CHECK: assert property (a ##1 b |=> not a); %i0 = ltl.implication %a, %b : i1, i1 - verif.assert %i0 : !ltl.property + sv.assert_property %i0 : !ltl.property %i1 = ltl.delay %b, 1, 0 : i1 %i2 = ltl.concat %a, %i1 : i1, !ltl.sequence %i3 = ltl.implication %i2, %n0 : !ltl.sequence, !ltl.property - verif.assert %i3 : !ltl.property + sv.assert_property %i3 : !ltl.property %i4 = ltl.delay %true, 1, 0 : i1 %i5 = ltl.concat %a, %i1, %i4 : i1, !ltl.sequence, !ltl.sequence %i6 = ltl.implication %i5, %n0 : !ltl.sequence, !ltl.property - verif.assert %i6 : !ltl.property + sv.assert_property %i6 : !ltl.property // CHECK: assert property (a until b); %u0 = ltl.until %a, %b : i1, i1 - verif.assert %u0 : !ltl.property + sv.assert_property %u0 : !ltl.property // CHECK: assert property (s_eventually a); %e0 = ltl.eventually %a : i1 - verif.assert %e0 : !ltl.property + sv.assert_property %e0 : !ltl.property // 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) not a); + // CHECK: wire [[W:.+]] = b; + // CHECK: assert property (@(posedge clk) disable iff ([[W]]) 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 - %k6 = ltl.clock %n0, posedge %clk : !ltl.property - verif.assert %k0 : !ltl.property - verif.assert %k3 : !ltl.property - verif.assert %n0 if %b : !ltl.property - verif.assert %k6 if %b : !ltl.property + sv.assert_property %k0 : !ltl.property + sv.assert_property %k3 : !ltl.property + sv.assert_property %n0 on posedge %clk disable_iff %b: !ltl.property } // CHECK-LABEL: module Precedence @@ -213,33 +211,33 @@ hw.module @Precedence(in %a: i1, in %b: i1) { // CHECK: assert property ((a or b) and b); %a0 = ltl.or %a, %b : i1, i1 %a1 = ltl.and %a0, %b : !ltl.sequence, i1 - verif.assert %a1 : !ltl.sequence + sv.assert_property %a1 : !ltl.sequence // CHECK: assert property (##1 (a or b)); %d0 = ltl.delay %a0, 1, 0 : !ltl.sequence - verif.assert %d0 : !ltl.sequence + sv.assert_property %d0 : !ltl.sequence // CHECK: assert property (not (a or b)); %n0 = ltl.not %a0 : !ltl.sequence - verif.assert %n0 : !ltl.property + sv.assert_property %n0 : !ltl.property // CHECK: assert property (a and (a |-> b)); %i0 = ltl.implication %a, %b : i1, i1 %i1 = ltl.and %a, %i0 : i1, !ltl.property - verif.assert %i1 : !ltl.property + sv.assert_property %i1 : !ltl.property // CHECK: assert property ((s_eventually a) and b); // CHECK: assert property (b and (s_eventually a)); %e0 = ltl.eventually %a : i1 %e1 = ltl.and %e0, %b : !ltl.property, i1 %e2 = ltl.and %b, %e0 : i1, !ltl.property - verif.assert %e1 : !ltl.property - verif.assert %e2 : !ltl.property + sv.assert_property %e1 : !ltl.property + sv.assert_property %e2 : !ltl.property // CHECK: assert property ((a until b) and a); %u0 = ltl.until %a, %b : i1, i1 %u1 = ltl.and %u0, %a : !ltl.property, i1 - verif.assert %u1 : !ltl.property + sv.assert_property %u1 : !ltl.property } // CHECK-LABEL: module SystemVerilogSpecExamples @@ -252,7 +250,7 @@ hw.module @SystemVerilogSpecExamples(in %clk: i1, in %a: i1, in %b: i1, in %c: i %a2 = ltl.concat %a, %a0 : i1, !ltl.sequence %a3 = ltl.concat %c, %a1 : i1, !ltl.sequence %a4 = ltl.concat %a2, %a3 : !ltl.sequence, !ltl.sequence - verif.assert %a4 : !ltl.sequence + sv.assert_property %a4 : !ltl.sequence // Section 16.12.20 "Property examples" @@ -261,18 +259,19 @@ hw.module @SystemVerilogSpecExamples(in %clk: i1, in %a: i1, in %b: i1, in %c: i %b1 = ltl.concat %b, %b0, %a1 : i1, !ltl.sequence, !ltl.sequence %b2 = ltl.implication %a, %b1 : i1, !ltl.sequence %b3 = ltl.clock %b2, posedge %clk : !ltl.property - verif.assert %b3 : !ltl.property + sv.assert_property %b3 : !ltl.property - // CHECK: assert property (disable iff (~(e)) @(posedge clk) a |-> not b ##1 c ##1 d); + // CHECK: wire [[W0:.+]] = e; + // CHECK: assert property (disable iff ([[W0]]) @(posedge clk) a |-> not b ##1 c ##1 d); %c0 = ltl.not %b1 : !ltl.sequence %c1 = ltl.implication %a, %c0 : i1, !ltl.property %c3 = ltl.clock %c1, posedge %clk : !ltl.property - verif.assert %c3 if %e : !ltl.property + sv.assert_property %c3 disable_iff %e : !ltl.property // CHECK: assert property (##1 a |-> b); %d0 = ltl.delay %a, 1, 0 : i1 %d1 = ltl.implication %d0, %b : !ltl.sequence, i1 - verif.assert %d1 : !ltl.property + sv.assert_property %d1 : !ltl.property } // CHECK-LABEL: module LivenessExample @@ -280,25 +279,29 @@ hw.module @LivenessExample(in %clock: i1, in %reset: i1, in %isLive: i1) { %true = hw.constant true // CHECK: wire _GEN = ~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)); + // CHECK: wire [[WR0:.+]] = reset; + // CHECK: assert property (disable iff ([[WR0]]) @(posedge clock) $fell(reset) & _GEN |-> (s_eventually isLive)); + // CHECK: wire [[WR1:.+]] = reset; + // CHECK: assume property (disable iff ([[WR1]]) @(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 %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 + sv.assert_property %liveness_after_reset disable_iff %reset : !ltl.property + sv.assume_property %liveness_after_reset disable_iff %reset : !ltl.property - // 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)); + // CHECK: wire [[WR2:.+]] = reset; + // CHECK: assert property (disable iff ([[WR2]]) @(posedge clock) isLive ##1 _GEN |-> (s_eventually isLive)); + // CHECK: wire [[WR3:.+]] = reset; + // CHECK: assume property (disable iff ([[WR3]]) @(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 %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 + sv.assert_property %liveness_after_fall disable_iff %reset : !ltl.property + sv.assume_property %liveness_after_fall disable_iff %reset : !ltl.property } // https://github.com/llvm/circt/issues/5763 @@ -309,7 +312,7 @@ hw.module @Issue5763(in %a: i3) { %0 = comb.extract %a from 0 : (i3) -> i1 %1 = comb.icmp bin eq %a, %c-1_i3 : i3 %2 = comb.and bin %1, %0 : i1 - verif.assert %2 : i1 + sv.assert_property %2 : i1 } @@ -318,12 +321,15 @@ 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 if %b, posedge %clk : !ltl.property + // CHECK: wire [[WB0:.+]] = b; + // CHECK: assert property (@(posedge clk) disable iff ([[WB0]]) not a); + sv.assert_property %n0 on posedge %clk disable_iff %b : !ltl.property - // CHECK: assume property (@(posedge clk) disable iff (~(b)) not a); - verif.clocked_assume %n0 if %b, posedge %clk : !ltl.property + // CHECK: wire [[WB1:.+]] = b; + // CHECK: assume property (@(posedge clk) disable iff ([[WB1]]) not a); + sv.assume_property %n0 on posedge %clk disable_iff %b : !ltl.property - // CHECK: cover property (@(posedge clk) disable iff (~(b)) not a); - verif.clocked_cover %n0 if %b, posedge %clk : !ltl.property + // CHECK: wire [[WB2:.+]] = b; + // CHECK: cover property (@(posedge clk) disable iff ([[WB2]]) not a); + sv.cover_property %n0 on posedge %clk disable_iff %b: !ltl.property } diff --git a/test/firtool/extract-test-code.fir b/test/firtool/extract-test-code.fir index ca5ce9c57a38..674e5035ecbf 100644 --- a/test/firtool/extract-test-code.fir +++ b/test/firtool/extract-test-code.fir @@ -44,7 +44,8 @@ circuit Top: ; CHECK: module Top_assert( ; CHECK-NOT: endmodule - ; CHECK: foo: assert property (disable iff (~(en)) cond); + ; CHECK: wire _GEN = ~en; + ; CHECK: foo: assert property (disable iff (_GEN) cond); ; CHECK: endmodule public module Top: