When proving partitions equal, EQY can use different strategies. Strategies are
configured using strategy sections in an
.eqy file. This page documents the
currently supported strategies and the corresponding strategy specific options.
See the .eqy file format reference for general information on
how to specify the strategies to use for each partition.
sat strategy uses Yosys’s builtin
sat command in the
-tempinduct mode to perform a k-induction proof (see the Yosys command
reference for more details).
This strategy can be quite fast for small and simple partitions, but is less effective for larger or more complex partitions. Being limited to k-induction means that this strategy is unable to prove some partitions equal.
sat command also lacks support for memories, and therefore this
startegy will not apply to any partitions that contain memory. This is done
automatically and does not require excluding these partitions using the
The maximal depth to try. The
satstrategy will only be able to prove partitions equivalent if the partitions produce equal outputs for the initial depth steps and also produce equal outputs in any step for which the depth preceding steps did so. (default value: 5)
sby strategy uses SBY, the front-end for Yosys-based formal
verification flows. SBY provides a common interface for using different
backend-tools. This makes the
sby stratagy a very versatile strategy and a
good default choice.
sby strategy always uses SBY’s
prove mode. The partitions it can
prove equal and the runtime it takes to do so depend on which engine and solver
are used. See the SBY reference for details on the supported engines and
The SBY engine to use. This can include the solver to be used by the engine as well as engine and solver options. Here
<engine-config>is used verbatim in the generated
.sbyfiles. (default value:
The depth to use for engine configurations that require a depth bound. Ignored by engines that do not take a depth bound. (default value: 5)
Limits the amount of time spent trying to prove a partition equivalent. If the timout is reached before a proof was found, the next strategy is tried. (not enabled by default)
Do not use formal x-propagation. Disabling this avoids using the Yosys
xproppass, but may prevent proving partitions equivalent when they contain uninitialized state or don’t-care values. (default value: on)
smtbmc engine with the
bitwuzla solver to perform a depth 10
k-induction equivalence proof:
engine smtbmc bitwuzla
abc engine with the
pdr solver to prove equivalence using the
engine abc pdr
The dummy strategy does not try to prove partitions equivalent and instead immediately gives up, falling through to the next strategy or failing the equivalence prove if no other strategy remains.