[FIRRTL] Add intrinsic for UNR only assume #6867
Conversation
uenoku
changed the title
|
|
||
| ### circt.assume_edged_predicate | ||
|
|
||
| Generate a SV assume statement whose predicate is used in a sensitivity list of the enclosing always block. |
There was a problem hiding this comment.
No clock, that's right. Interesting!
| `ifdef USE_UNR_ONLY_CONSTRAINTS | ||
| wire _GEN = ~enable | pred; | ||
| always @(edge _GEN) | ||
| assume_label: assume(_GEN) else $error("Conditional compilation example for UNR-only and formal-only assert"); |
There was a problem hiding this comment.
Companion assume's don't have error messages today, but seems reasonable to support on the intrinsic (can use or not when migrating).
Was thinking about implications of not being under a clock in the case when the error has substitution arguments.
There was a problem hiding this comment.
Yeah thank you for pointing out. We add %sampled for concurrent assertions but not for immediate assertions but I'm uncertain we need $sampled for this. I'm fine to drop messages for migration.
Added, thanks! |
uenoku
force-pushed
the
dev/hidetou/unr-only-assume-intr
branch
from
52f5acf
to
8598188
Compare
|
Maybe |
Yeah that sounds great! |
uenoku
force-pushed
the
dev/hidetou/unr-only-assume-intr
branch
from
1f6f448
to
ac45e7c
Compare
…ation from AssertOp lowering (#6863) This PR separates UNROnlyAssume generation from AssertOp lowering into a dedicate op. This commit adds: * LowerToHW support for `UnclockedPredicateIntrinsicOp` (added in #6867). * CreateCompanionAssume pass which explicitly introduces companion assumes to the IR. Normal assume and UnclockedPredicateIntrinsicOp are used based on the guard's content. 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).
This adds UnclockedAssumeIntrinsicOp which generates a SV assume statement whose predicate is used in a sensitivity list of the enclosing always block.