diff --git a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp index 183644f6ead..c96556a82bf 100644 --- a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp +++ b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp @@ -1621,7 +1621,7 @@ struct FIRRTLLowering : public FIRRTLVisitor { LogicalResult visitStmt(VerifAssumeIntrinsicOp op); LogicalResult visitStmt(VerifCoverIntrinsicOp op); LogicalResult visitExpr(HasBeenResetIntrinsicOp op); - LogicalResult visitStmt(AssumeEdgedPredicateIntrinsicOp op); + LogicalResult visitStmt(UnclockedAssumeIntrinsicOp op); // Other Operations LogicalResult visitExpr(BitsPrimOp op); @@ -4530,7 +4530,7 @@ LogicalResult FIRRTLLowering::visitStmt(CoverOp op) { } // Lower an UNR only assume to a specific style of SV assume. -LogicalResult FIRRTLLowering::visitStmt(AssumeEdgedPredicateIntrinsicOp op) { +LogicalResult FIRRTLLowering::visitStmt(UnclockedAssumeIntrinsicOp op) { // TODO : Need to figure out if there is a cleaner way to get the string which // indicates the assert is UNR only. Or better - not rely on this at all - // ideally there should have been some other attribute which indicated that @@ -4563,11 +4563,18 @@ LogicalResult FIRRTLLowering::visitStmt(AssumeEdgedPredicateIntrinsicOp op) { return emitGuards(op.getLoc(), guards, [&]() { builder.create( ArrayRef(sv::EventControl::AtEdge), ArrayRef(predicate), [&]() { - buildImmediateVerifOp( - builder, "assume", predicate, - circt::sv::DeferAssertAttr::get( - builder.getContext(), circt::sv::DeferAssert::Immediate), - assumeLabel, op.getMessageAttr(), messageOps); + if (op.getMessageAttr().getValue().empty()) + buildImmediateVerifOp( + builder, "assume", predicate, + circt::sv::DeferAssertAttr::get( + builder.getContext(), circt::sv::DeferAssert::Immediate), + assumeLabel); + else + buildImmediateVerifOp( + builder, "assume", predicate, + circt::sv::DeferAssertAttr::get( + builder.getContext(), circt::sv::DeferAssert::Immediate), + assumeLabel, op.getMessageAttr(), messageOps); }); }); } diff --git a/lib/Dialect/FIRRTL/Transforms/CreateCompanionAssume.cpp b/lib/Dialect/FIRRTL/Transforms/CreateCompanionAssume.cpp index 31a2132c0df..cfd99b023ba 100644 --- a/lib/Dialect/FIRRTL/Transforms/CreateCompanionAssume.cpp +++ b/lib/Dialect/FIRRTL/Transforms/CreateCompanionAssume.cpp @@ -22,7 +22,8 @@ namespace { struct CreateCompanionAssumePass : public CreateCompanionAssumeBase { void runOnOperation() override { - getOperation().walk([](firrtl::AssertOp assertOp) { + StringAttr emptyMessage = StringAttr::get(&getContext(), ""); + getOperation().walk([&](firrtl::AssertOp assertOp) { OpBuilder builder(assertOp); builder.setInsertionPointAfter(assertOp); auto guards = assertOp->getAttrOfType("guards"); @@ -37,19 +38,22 @@ struct CreateCompanionAssumePass }); } - // If so, use AssumeEdgedPredicateIntrinsicOp. + // TODO: Currently messages are dropped to preserve the old behaivor. Copy + // messages once it works well with UNR tools. if (isUnrOnlyAssert) - assume = builder.create( + // If UNROnly, use UnclockedAssumeIntrinsicOp. + assume = builder.create( assertOp.getLoc(), assertOp.getPredicate(), assertOp.getEnable(), - assertOp.getMessage(), assertOp.getSubstitutions(), - assertOp.getName()); + emptyMessage, ValueRange{}, assertOp.getName()); else // Otherwise use concurrent assume. assume = builder.create( assertOp.getLoc(), assertOp.getClock(), assertOp.getPredicate(), - assertOp.getEnable(), assertOp.getMessage(), - assertOp.getSubstitutions(), assertOp.getName(), + assertOp.getEnable(), emptyMessage, ValueRange{}, + assertOp.getName(), /*isConcurrent=*/true); + + // Add a guard "USE_PROPERTY_AS_CONSTRAINT" to companion assumes. SmallVector newGuards{ builder.getStringAttr("USE_PROPERTY_AS_CONSTRAINT")}; if (guards) diff --git a/test/Conversion/FIRRTLToHW/lower-to-hw.mlir b/test/Conversion/FIRRTLToHW/lower-to-hw.mlir index cb25dfb7331..c84bae5c839 100644 --- a/test/Conversion/FIRRTLToHW/lower-to-hw.mlir +++ b/test/Conversion/FIRRTLToHW/lower-to-hw.mlir @@ -407,7 +407,7 @@ firrtl.circuit "Simple" attributes {annotations = [{class = firrtl.assume %clock, %aCond, %aEn, "assert0" : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1> {guards = ["USE_PROPERTY_AS_CONSTRAINT"], isConcurrent = true} firrtl.assume %clock, %aCond, %aEn, "assert0" : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1> {name = "assert_0", guards = ["USE_PROPERTY_AS_CONSTRAINT"], isConcurrent = true} firrtl.assume %clock, %aCond, %aEn, "assert0"(%value) : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1>, !firrtl.uint<42> {guards = ["USE_PROPERTY_AS_CONSTRAINT"], isConcurrent = true} - firrtl.int.assume.edged_predicate %bCond, %bEn, "assume0"(%value) : !firrtl.uint<1>, !firrtl.uint<1>, !firrtl.uint<42> {name = "assume_unr", guards = ["USE_PROPERTY_AS_CONSTRAINT", "USE_UNR_ONLY_CONSTRAINTS"]} + firrtl.int.unclocked_assume %bCond, %bEn, "assume0"(%value) : !firrtl.uint<1>, !firrtl.uint<1>, !firrtl.uint<42> {name = "assume_unr", guards = ["USE_PROPERTY_AS_CONSTRAINT", "USE_UNR_ONLY_CONSTRAINTS"]} // CHECK-NEXT: [[CLOCK:%.+]] = seq.from_clock %clock // CHECK-NEXT: [[TRUE:%.+]] = hw.constant true // CHECK-NEXT: [[TMP1:%.+]] = comb.xor bin %aEn, [[TRUE]] diff --git a/test/Dialect/FIRRTL/SFCTests/complex-asserts.fir b/test/Dialect/FIRRTL/SFCTests/complex-asserts.fir index 305916eb72b..92c6f01e9c5 100644 --- a/test/Dialect/FIRRTL/SFCTests/complex-asserts.fir +++ b/test/Dialect/FIRRTL/SFCTests/complex-asserts.fir @@ -147,25 +147,25 @@ circuit Foo: ; The companion assumes get bunched up in an ifdef block. ; CHECK-NEXT: `ifdef USE_PROPERTY_AS_CONSTRAINT - ; CHECK-NEXT: assume__verif_library: assume property (@(posedge clock) ~enable | [[GEN]]) else $error("Assertion failed (verification library): "); - ; CHECK-NEXT: assume__verif_library_0: assume property (@(posedge clock) ~enable | [[GEN_0]]) else $error("Assertion failed (verification library): sum =/= 1.U"); - ; CHECK-NEXT: assume__verif_library_1: assume property (@(posedge clock) ~[[GEN_2]] | [[GEN_1]]) else $error("Assertion failed (verification library): Assert with when"); - ; CHECK-NEXT: assume__verif_library_2: assume property (@(posedge clock) ~enable | [[GEN_3]]) else $error("Assertion failed (verification library): expected sum === 2.U but got %d", $sampled(sum)); - ; CHECK-NEXT: assume__verif_library_3: assume property (@(posedge clock) [[GEN_4]]) else $error("Assertion failed (verification library): SVA assert example, sum was %d", $sampled(sum)); - ; CHECK-NEXT: assume__verif_library_hello_world: assume property (@(posedge clock) [[GEN_5]]) else $error("Assertion failed (verification library): Custom label example"); - ; CHECK-NEXT: assume__verif_library_4: assume property (@(posedge clock) [[GEN_6]]) else $error("Assertion failed (verification library): X-passing assert example"); + ; CHECK-NEXT: assume__verif_library: assume property (@(posedge clock) ~enable | [[GEN]]); + ; CHECK-NEXT: assume__verif_library_0: assume property (@(posedge clock) ~enable | [[GEN_0]]); + ; CHECK-NEXT: assume__verif_library_1: assume property (@(posedge clock) ~[[GEN_2]] | [[GEN_1]]); + ; CHECK-NEXT: assume__verif_library_2: assume property (@(posedge clock) ~enable | [[GEN_3]]); + ; CHECK-NEXT: assume__verif_library_3: assume property (@(posedge clock) [[GEN_4]]); + ; CHECK-NEXT: assume__verif_library_hello_world: assume property (@(posedge clock) [[GEN_5]]); + ; CHECK-NEXT: assume__verif_library_4: assume property (@(posedge clock) [[GEN_6]]); ; CHECK-NEXT: `ifdef USE_UNR_ONLY_CONSTRAINTS ; CHECK-NEXT: wire [[GEN_10:.+]] = ~enable | [[GEN_8]]; ; CHECK-NEXT: always @(edge [[GEN_7]]) - ; CHECK-NEXT: assume__verif_library_5: assume([[GEN_7]]) else $error("Assertion failed (verification library): Conditional compilation example for UNR-only assert"); + ; CHECK-NEXT: assume__verif_library_5: assume([[GEN_7]]); ; CHECK-NEXT: always @(edge [[GEN_10]]) - ; CHECK-NEXT: assume__verif_library_6: assume([[GEN_10]]) else $error("Assertion failed (verification library): Conditional compilation example with if-else-fatal style assert"); + ; CHECK-NEXT: assume__verif_library_6: assume([[GEN_10]]); ; CHECK-NEXT: `endif // USE_UNR_ONLY_CONSTRAINTS ; CHECK-NEXT: `ifdef USE_FORMAL_ONLY_CONSTRAINTS ; CHECK-NEXT: `ifdef USE_UNR_ONLY_CONSTRAINTS ; CHECK-NEXT: wire [[GEN_11:.+]] = ~enable | [[GEN_9]]; ; CHECK-NEXT: always @(edge [[GEN_11]]) - ; CHECK-NEXT: assume__verif_library_7: assume([[GEN_11]]) else $error("Assertion failed (verification library): Conditional compilation example for UNR-only and formal-only assert"); + ; CHECK-NEXT: assume__verif_library_7: assume([[GEN_11]]); ; CHECK-NEXT: `endif // USE_UNR_ONLY_CONSTRAINTS ; CHECK-NEXT: `endif // USE_FORMAL_ONLY_CONSTRAINTS ; CHECK-NEXT: `endif diff --git a/test/Dialect/FIRRTL/create-companion-assume.mlir b/test/Dialect/FIRRTL/create-companion-assume.mlir index a038bf34c7a..90c9b4ecd8d 100644 --- a/test/Dialect/FIRRTL/create-companion-assume.mlir +++ b/test/Dialect/FIRRTL/create-companion-assume.mlir @@ -7,12 +7,12 @@ firrtl.module @Assert(in %clock: !firrtl.clock, in %pred: !firrtl.uint<1>, in % in %value: !firrtl.uint<42>) { firrtl.assert %clock, %pred, %en, "assert0"(%value) : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1>, !firrtl.uint<42> {guards=["Foo"]} // CHECK: firrtl.assert - // CHECK-NEXT: firrtl.assume %clock, %pred, %en, "assert0"(%value) : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1>, !firrtl.uint<42> + // CHECK-NEXT: firrtl.assume %clock, %pred, %en, "" : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1> // CHECK-SAME: {eventControl = 0 : i32, guards = ["USE_PROPERTY_AS_CONSTRAINT", "Foo"], isConcurrent = true} firrtl.assert %clock, %pred, %en, "assert0"(%value) : !firrtl.clock, !firrtl.uint<1>, !firrtl.uint<1>, !firrtl.uint<42> {guards=["USE_UNR_ONLY_CONSTRAINTS"]} // CHECK: firrtl.assert - // CHECK-NEXT: firrtl.int.assume.edged_predicate %pred, %en, "assert0"(%value) : !firrtl.uint<1>, !firrtl.uint<1>, !firrtl.uint<42> + // CHECK-NEXT: firrtl.int.unclocked_assume %pred, %en, "" : !firrtl.uint<1>, !firrtl.uint<1> // CHECK-SAME: {guards = ["USE_PROPERTY_AS_CONSTRAINT", "USE_UNR_ONLY_CONSTRAINTS"]} } diff --git a/test/Dialect/FIRRTL/lower-intrinsics.mlir b/test/Dialect/FIRRTL/lower-intrinsics.mlir index 1c4f71cb377..4d04486fd03 100644 --- a/test/Dialect/FIRRTL/lower-intrinsics.mlir +++ b/test/Dialect/FIRRTL/lower-intrinsics.mlir @@ -303,7 +303,7 @@ firrtl.circuit "Foo" { // CHECK: firrtl.int.unclocked_assume %{{.+}}, %{{.+}}, "text: %d"( // CHECK-SAME: guards = ["MACRO_GUARD", "ASDF"] // CHECK-SAME: name = "label for unr" - %unr_predicate, %unr_enable, %unr_val = firrtl.instance unr interesting_name @AssumeEdgedPredicate(in predicate: !firrtl.uint<1>, in enable: !firrtl.uint<1>, in val: !firrtl.uint<1>) + %unr_predicate, %unr_enable, %unr_val = firrtl.instance unr interesting_name @UnclockedAssume(in predicate: !firrtl.uint<1>, in enable: !firrtl.uint<1>, in val: !firrtl.uint<1>) firrtl.strictconnect %unr_predicate, %cond : !firrtl.uint<1> firrtl.strictconnect %unr_enable, %enable : !firrtl.uint<1> firrtl.strictconnect %unr_val, %enable : !firrtl.uint<1> diff --git a/test/firtool/chisel_assert.fir b/test/firtool/chisel_assert.fir index 8b91397bdf0..2ed81fd4df9 100644 --- a/test/firtool/chisel_assert.fir +++ b/test/firtool/chisel_assert.fir @@ -85,11 +85,9 @@ circuit ChiselVerif: ; CHECK-NEXT: `ifdef MACRO_GUARD ; CHECK-NEXT: `ifdef ASDF ; CHECK-NEXT: assume__label_for_assert_with_format_string: - ; CHECK-NEXT: assume property (@(posedge clock) [[GEN]]) - ; CHECK-NEXT: else $error("message: %d", $sampled(cond)); + ; CHECK-NEXT: assume property (@(posedge clock) [[GEN]]); ; CHECK-NEXT: assume__label_for_ifelsefatal_assert: - ; CHECK-NEXT: assume property (@(posedge clock) [[GEN]]) - ; CHECK-NEXT: else $error("ief: %d", $sampled(enable)); + ; CHECK-SAME: assume property (@(posedge clock) [[GEN]]); ; CHECK-NEXT: `endif ; CHECK-NEXT: `endif ; CHECK-NEXT:`endif