Enhance YosysVerificSettings by introducing a vector to track applied SystemVerilog file extensions, ensuring stale mappings are removed before adding new extensions. Implement an apply_all method to apply all settings to Verific APIs after a reset, improving settings management and consistency.
Introduce a new structure for managing Yosys-Verific settings, allowing users to get, set, and reset options related to Verific integration. Implement options for ignoring translate pragmas and specifying file extensions for SystemVerilog. Update command-line interface to support these settings, including help documentation for usage examples.
This option allows you to process a design that includes unsupported
SVA. Unsupported SVA gets imported as formal cells using 'x inputs and
with the `unsupported_sva` attribute set. This allows you to get a
complete list of defined properties or to check only a supported subset
of properties. To ensure no properties are unintentionally skipped for
actual verification, even in cases where `-sva-continue-on-error` is
used by default to read and inspect a design, `hierarchy -simcheck` and
`hierarchy -smtcheck` (run by SBY) now ensure that no `unsupported_sva`
property cells remain in the design.
The implementation for the implication operator in cover mode actually
implements the followed-by operator, so we can re-use it unchanged.
It is not always the correct behavior for the implication operator in
cover mode, but a) it will only cause false positives not miss anything
so if the behavior is unexpected it will be visible in the produced
traces, b) it is unlikely to make a difference for most properties one
would practically use in cover mode, c) at least one other widely used
SVA implementations behaves the same way and d) it's not clear whether
we can fix this without rewriting most of verificsva.cc
