[firtool] Run LowerFormalToHW pass when emitting SV #7837
Conversation
Add the `LowerFormalToHW` pass to the HW-to-SV pipeline of firtool. This will make any `verif.formal` ops be emitted as additional top-level modules, which is in line with what circt-test also does. In the future we may want to have additional controls in firtool to disable emission of these formal tests. (But we would likely do this by removing them early in the pipeline to open up new optimization possibilities rather than not emitting them at the final stage.) This creates a small amount of churn in the `directories.fir` test which was sensitive to _any_ kind of folder running, e.g. through the dialect conversion or greedy rewriter framework. The latter one is used by the formal op lowering, and it's probably a good idea to not have tests fail when a very common optimization runs.
| ; MLIR_OUT-DAG: [[OBJ3:%.+]] = om.object @MemorySchema | ||
| ; MLIR_OUT-DAG: om.constant "baz_m_ext" : !om.string | ||
| ; MLIR_OUT-DAG: om.constant #om.integer<3 : ui64> : !om.integer | ||
| ; MLIR_OUT: om.class.fields [[OBJ1]], [[OBJ2]], [[OBJ3]] : !om.class.type<@MemorySchema>, !om.class.type<@MemorySchema>, !om.class.type<@MemorySchema> | ||
|
|
There was a problem hiding this comment.
This is fine. However, this test in appropriately combined directory testing with OM testing. (Apparently, my past self thought the same thing: #5224 (comment))
If it's cleaner, in a follow-on, to either (1) factor this out of this test or (2) just delete this part of the test, then that would be good. @prithayan: Do you have any thoughts here?
There was a problem hiding this comment.
Yeah that would be great! I'll land this for now. Let's see what @prithayan thinks.
There was a problem hiding this comment.
Sorry for the messy lit tests and missing out your original review @seldridge , I think it makes sense to remove the testing from here. I added the om classes just because the original test was checking for the metadata verbatim ops, which will be replaced by the OM. I will take up the task to cleanup the tests.
Add the
LowerFormalToHWpass to the HW-to-SV pipeline of firtool. This will make anyverif.formalops be emitted as additional top-level modules, which is in line with what circt-test also does.In the future we may want to have additional controls in firtool to disable emission of these formal tests. (But we would likely do this by removing them early in the pipeline to open up new optimization possibilities rather than not emitting them at the final stage.)
This creates a small amount of churn in the
directories.firtest which was sensitive to any kind of folder running, e.g. through the dialect conversion or greedy rewriter framework. The latter one is used by the formal op lowering, and it's probably a good idea to not have tests fail when a very common optimization runs.