[Verif] Add pass to lower symbolic values #8422
Conversation
Add the `LowerSymbolicValues` pass which converts `verif.symbolic_value` ops either to a black box instance or to a wire declaration with a `(* anyseq *)` attribute. The former is useful since most formal tools have a way of treating black boxes as internal port boundaries, such that black box output ports behave the same as top-level input ports. The latter is useful for interoperability with Yosys which has a custom Verilog attribute "anyseq" that marks a wire declaration as a symbolic value.
ad5d4fe to
3a045c3
Compare
| @@ -306,6 +306,8 @@ LogicalResult firtool::populateHWToSV(mlir::PassManager &pm, | |||
| const FirtoolOptions &opt) { | |||
| pm.nestAny().addPass(verif::createStripContractsPass()); | |||
| pm.addPass(verif::createLowerFormalToHWPass()); | |||
| pm.addPass( | |||
There was a problem hiding this comment.
Just making sure I understand this right, does opt.shouldExtractTestCode() state that test code should be lowered or should be removed? If it means that it should be lowered, shouldn't this pass only be run if we want to generate "formal verification" SV and symbolic values should be outright removed otherwise?
There was a problem hiding this comment.
ExtractTestCode is a FIRRTL-specific pass that moves assert/assume/cover statements into a separate Verilog file/module that can then be bound into the original location. As long as we create any asserts/assumes/covers before that pass runs, everything should be good 👍
| %3 = verif.symbolic_value : !hw.array<6xi7> | ||
| dbg.variable "x3", %3 : !hw.array<6xi7> | ||
| } | ||
|
|
There was a problem hiding this comment.
Is there also a test for when we should remove symbolic values when lowering to SV?
There was a problem hiding this comment.
Currently there's no mode for the pass that removes symbolic values. I'm not entirely sure how that would look like. Replacing with a constant feels wrong, and otherwise I don't know what we could put there instead of the symbolic value. Do you have any ideas?
Add the
LowerSymbolicValuespass which convertsverif.symbolic_valueops either to a black box instance or to a wire declaration with a(* anyseq *)attribute. The former is useful since most formal tools have a way of treating black boxes as internal port boundaries, such that black box output ports behave the same as top-level input ports. The latter is useful for interoperability with Yosys which has a custom Verilog attribute "anyseq" that marks a wire declaration as a symbolic value.