-
Notifications
You must be signed in to change notification settings - Fork 281
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.
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
[firtool] Add an option to export SV without SVA #7081
Conversation
IMO LTLToCore should cause an error if the legalization was not possible. |
There are already options for specifying preferred format for verification constructs, e.g., #6885 . These apply to the non-LTL verification statements, but has similar motivation and use-case: capture verif intent higher-level and the way it's lowered is an option -- usually driven by tool compatibility needs (such as older verilator not supporting SVA's or dealing poorly with many of them). Can we unify these under a single knob for users to indicate what's legal/preferred for emitting verification intent? It's not a perfect fit, but as-is WDYT? Hopefully all this can be unified representationally soon as well! 👍 . |
Oh ok I wasn't aware that those were around for more than just forcing an sva output. In the current form it definitely seems like something I could use to trigger LTLToCore. I'll look into that thanks! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you for iterating on this! I agree what @dtzSiFive said.
The verification lowering is chaotic right now and hopefully we will move forward single representation. We may need to consider verif flavor is ifElseFatal
and None
but I think they should be deprecated anyway soon.
Please add a test tor firtool, but otherwise LGTM :)
Could you please add an e2e test for --verif-flavor=imediate? |
Some simulators like Verilator have very poor support for SVA syntax and will sometimes give a false positives when they are used. This PR adds an option that allows for
LowerLTLToCore
to be run just before SV emission, to allow in some simples for SVA to be omitted in the output (when only disable iff is used on a boolean predicate). AsLTLToCore
evolves, this would also allow for certain properties to be synthesized and such.I'm unsure if LTLToCore should fail loudly if it encounters ltl ops that it doesn't handle or if that should be allowed to slip through and simply still output property assertions but with the disable folded into the property?