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.