circt
circt copied to clipboard
llvm
[firtool] Add an option to export SV without SVA
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). As LTLToCore 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?
There are already options for specifying preferred format for verification constructs, e.g., https://github.com/llvm/circt/pull/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 no-sva only controlling the LTL variants is a bit unexpected in conjunction with --verification-flavor options which might indeed produce SVA's (and soon will by default).
WDYT?
Hopefully all this can be unified representationally soon as well! 👍 .
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
no-svaonly controlling the LTL variants is a bit unexpected in conjunction with--verification-flavoroptions which might indeed produce SVA's (and soon will by default).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!