Skip to content

Commit

Permalink
Rebase and drop message strings for now
Browse files Browse the repository at this point in the history
  • Loading branch information
@uenoku
uenoku committed Mar 28, 2024
1 parent 91ab0f8 commit 87fa40c
Show file tree
Hide file tree
Showing 7 changed files with 41 additions and 32 deletions.
21 changes: 14 additions & 7 deletions lib/Conversion/FIRRTLToHW/LowerToHW.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1621,7 +1621,7 @@ struct FIRRTLLowering : public FIRRTLVisitor<FIRRTLLowering, LogicalResult> {
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);
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -4563,11 +4563,18 @@ LogicalResult FIRRTLLowering::visitStmt(AssumeEdgedPredicateIntrinsicOp op) {
return emitGuards(op.getLoc(), guards, [&]() {
builder.create<sv::AlwaysOp>(
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);
});
});
}
Expand Down
18 changes: 11 additions & 7 deletions lib/Dialect/FIRRTL/Transforms/CreateCompanionAssume.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,8 @@ namespace {
struct CreateCompanionAssumePass
: public CreateCompanionAssumeBase<CreateCompanionAssumePass> {
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<ArrayAttr>("guards");
Expand All @@ -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<firrtl::AssumeEdgedPredicateIntrinsicOp>(
// If UNROnly, use UnclockedAssumeIntrinsicOp.
assume = builder.create<firrtl::UnclockedAssumeIntrinsicOp>(
assertOp.getLoc(), assertOp.getPredicate(), assertOp.getEnable(),
assertOp.getMessage(), assertOp.getSubstitutions(),
assertOp.getName());
emptyMessage, ValueRange{}, assertOp.getName());
else
// Otherwise use concurrent assume.
assume = builder.create<firrtl::AssumeOp>(
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<Attribute> newGuards{
builder.getStringAttr("USE_PROPERTY_AS_CONSTRAINT")};
if (guards)
Expand Down
2 changes: 1 addition & 1 deletion test/Conversion/FIRRTLToHW/lower-to-hw.mlir
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]]
Expand Down
20 changes: 10 additions & 10 deletions test/Dialect/FIRRTL/SFCTests/complex-asserts.fir
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions test/Dialect/FIRRTL/create-companion-assume.mlir
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"]}
}

Expand Down
2 changes: 1 addition & 1 deletion test/Dialect/FIRRTL/lower-intrinsics.mlir
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down
6 changes: 2 additions & 4 deletions test/firtool/chisel_assert.fir
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 87fa40c

Please sign in to comment.