Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[firtool] Run LowerFormalToHW pass when emitting SV #7837

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

[firtool] Run LowerFormalToHW pass when emitting SV #7837

wants to merge 1 commit into from

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
    fabianschuiki committed Nov 19, 2024
    Configuration menu
    Copy the full SHA
    816c02b View commit details
    Browse the repository at this point in the history