Commits on Nov 19, 2024

1. [firtool] Run LowerFormalToHW pass when emitting SV …

   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.

   

   fabianschuiki committed Nov 19, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 816c02b
   • Browse repository at this point

   Copy the full SHA

   816c02b View commit details

   Browse the repository at this point in the history