[FIRRTL] Add CreateCompanionAssume pass; Decouple UNROnlyAssume generation from AssertOp lowering #6863
Conversation
uenoku
changed the title
uenoku
force-pushed
the
dev/hidetou/unr-only-companion-assume
branch
from
3eba2d5
to
9395e78
Compare
uenoku
force-pushed
the
dev/hidetou/unr-only-companion-assume
branch
2 times, most recently
from
dbd780e
to
7708dc8
Compare
uenoku
changed the title
|
|
||
| // Assertions gain a companion `assume` behind a | ||
| // `USE_PROPERTY_AS_CONSTRAINT` guard. | ||
| if (isAssert) { | ||
| StringAttr assumeLabel; | ||
| if (label) | ||
| assumeLabel = StringAttr::get(builder.getContext(), | ||
| "assume__" + label.getValue()); | ||
|
|
||
| circuitState.addMacroDecl( | ||
| builder.getStringAttr("USE_PROPERTY_AS_CONSTRAINT")); | ||
| addToIfDefBlock("USE_PROPERTY_AS_CONSTRAINT", [&]() { | ||
| if (!isUnrOnlyAssert) { | ||
| builder.create<sv::AssumeConcurrentOp>( | ||
| circt::sv::EventControlAttr::get(builder.getContext(), event), | ||
| clock, predicate, assumeLabel); | ||
| } else { | ||
| 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); | ||
| }); | ||
| } | ||
| }); | ||
| } |
| // If so, use AssumeEdgedPredicateIntrinsicOp. | ||
| if (isUnrOnlyAssert) | ||
| assume = builder.create<firrtl::AssumeEdgedPredicateIntrinsicOp>( | ||
| assertOp.getLoc(), assertOp.getPredicate(), assertOp.getEnable(), |
There was a problem hiding this comment.
Companion assume's -- both kinds -- don't have the message or substitution arguments today, see:
https://github.com/dtzSiFive/firrtl-verif-example/blob/master/assert/conc_true-guard_unr-fmt_%22sva%22-msg_%22message%22-name_%22label%22/output.sv
https://github.com/dtzSiFive/firrtl-verif-example/blob/master/assert/conc_true-guard_no-fmt_%22sva%22-msg_%22message%22-name_%22label%22/output.sv
Does seem nice to have them, just a detail to keep in mind.
There was a problem hiding this comment.
Yeah, thank you for pointing out! For normal assume I think it's totally Ok to have substitutions. For UNROnly assume, probably they are not enabled in the normal simulation but I agree that the behavior is uncertain.
There was a problem hiding this comment.
Great idea to factor out the companion assume business into its own pass, and that there is a dedicated intrinsic to capture the very peculiar flavor of assumes that some formal tools require. Pushes the ugly parts to the boundary and makes for a cleaner flow. 🥳
uenoku
force-pushed
the
dev/hidetou/unr-only-companion-assume
branch
from
7708dc8
to
87fa40c
Compare
This PR separates UNROnlyAssume generation from AssertOp lowering into a dedicate op.
This commit adds:
UnclockedPredicateIntrinsicOp(added in [FIRRTL] Add intrinsic for UNR only assume #6867).The commit is intended not to change semantics of generated verilog. This commit should only introduces cosmetic changes regarding guards(because now they are reused).