abstract - replace signals with abstract values during formal verification

yosys> help abstract

abstract [mode] [options] [selection]

Perform abstraction of signals within the design. Abstraction replaces a signal
with an unconstrained abstract value that can take an arbitrary concrete value
during formal verification. The mode and options control when a signal should
be abstracted and how it should affect FFs present in the design.

Modes:
    -state
        The selected FFs will be modified to load a new abstract value on every
        active clock edge, async reset or async load. This is independent of any
        clock enable that may be present on the FF cell. Conditional abstraction
        is supported with the -enable/-enabeln options. If present, the condition
        is sampled at the same time as the FF would smaple the correspnding data
        or async-data input whose value will be replaced with an abstract value.

        The selection can be used to specify which state bits to abstract. For
        each selected wire, any state bits that the wire is driven by will be
        abstracted. For a selected FF cell, all of its state is abstracted.
        Individual bits of a single wire can be abtracted using the -slice and
        -rtlilslice options.

-init

The selected FFs will be modified to have an abstract initial value.
The -enable/-enablen options are not supported in this mode.

The selection is used in the same way as it is for the -state mode.

-value

The drivers of the selected signals will be replaced with an abstract
value. In this mode, the abstract value can change at any time and is
not synchronized to any clock or other signal. Conditional abstraction
is supported with the -enable/-enablen options. The condition will
combinationally select between the original driver and the abstract
value.

The selection can be used to specify which output bits of which drivers
to abtract. For a selected cell, all its output bits will be abstracted.
For a selected wire, every output bit that is driving the wire will be
abstracted. Individual bits of a single wire can be abstracted using the
-slice and -rtlilslice options.

-enable <wire-name>

-enablen <wire-name>

Perform conditional abstraction with a named single bit wire as
condition. For -enable the wire is used as an active-high condition and
for -enablen as an active-low condition. See the description of the
-state and -value modes for details on how the condition affects the
abstractions performed by either mode. This option is not supported in
the -init mode.

-slice <lhs>:<rhs>

-slice <index>

-rtlilslice <lhs>:<rhs>

-rtlilslice <index>

Limit the abstraction to a slice of a single selected wire. The targeted
bits of the wire can be given as an inclusive range of indices or as a
single index. When using the -slice option, the indices are interpreted
following the source level declaration of the wire. This means the
-slice option will respect declarations with a non-zero-based index range
or with reversed bitorder. The -rtlilslice options will always use
zero-based indexing where index 0 corresponds to the least significant
bit of the wire.