3 commits

Author	SHA1	Message	Date
Jannis Harder	95db5a9d38	formalff: New -setundef option ... Find FFs with undefined initialization values for which changing the initialization does not change the observable behavior and initialize them. For -ff2anyinit, this reduces the number of generated $anyinit cells that drive wires with private names.	2022-08-16 13:37:30 +02:00
Jannis Harder	a5e1d3b997	formalff: Set new replaced_by_gclk attribute on removed dff's clks ... This attribute can be used by formal backends to indicate which clocks were mapped to the global clock. Update the btor and smt2 backend which already handle clock inputs to understand this attribute.	2022-08-16 13:37:30 +02:00
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