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.

-clk2ff

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.

-ff2anyinit

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.

-anyinit2ff

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.

-fine

Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for
-anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit.

-setundef

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.

-hierarchy

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.

-assume

Add assumptions that constrain wires with the 'replaced_by_gclk'
attribute to the value they would have before an active clock edge.

-declockgate

Detect clock-gating patterns and modify any FFs clocked by the gated
clock to use the ungated clock with the gate signal as clock enable.
This doesn't affect the design's behavior during FV but can enable the
use of formal verification methods that only support a single global
clock.