formalff - prepare FFs for formal¶
yosys> help formalff¶
formalff [options] [selection]
This pass transforms clocked flip-flops to prepare a design for formal verification. If a design contains latches and/or multiple different clocks run the async2sync or clk2fflogic passes before using this pass.
Replace all clocked flip-flops with $ff cells that use the implicit global clock. This assumes, without checking, that the design uses a single global clock. If that is not the case, the clk2fflogic pass should be used instead.
Replace uninitialized bits of $ff cells with $anyinit cells. An $anyinit cell behaves exactly like an $ff cell with an undefined initialization value. The difference is that $anyinit inhibits don't-care optimizations and is used to track solver-provided values in witness traces. If combined with -clk2ff this also affects newly created $ff cells.
Replaces $anyinit cells with uninitialized $ff cells. This performs the reverse of -ff2anyinit and can be used, before running a backend pass (or similar) that is not yet aware of $anyinit cells. Note that after running -anyinit2ff, in general, performing don't-care optimizations is not sound in a formal verification setting.
Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for -anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit.
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.
Propagates the 'replaced_by_gclk' attribute set by clk2ff upwards through the design hierarchy towards the toplevel inputs. This option works on the whole design and ignores the selection.
Add assumptions that constrain wires with the 'replaced_by_gclk' attribute to the value they would have before an active clock edge.