Jannis Harder c0063288d6 Add the $anyinit cell and the formalff pass ...

These can be used to protect undefined flip-flop initialization values
from optimizations that are not sound for formal verification and can
help mapping all solver-provided values in witness traces for flows that
use different backends simultaneously.

2022-08-16 13:37:30 +02:00

61 KiB

Raw Blame History

View Raw