EQY Strategies¶
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.
The sat
Strategy¶
The 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.
Yosys’s 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
noapply
option.
Strategy Options¶
depth <int>
The maximal depth to try. The
sat
strategy 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)
Example Configuration¶
[strategy simple]
use sat
depth 10
The sby
Strategy¶
The 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.
The 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
solvers in prove
mode.
Strategy Options¶
engine <engine-config>
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.sby
files. (default value:smtbmc
)depth <int>
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)
timeout <seconds>
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)
xprop <on|off>
Do not use formal x-propagation. Disabling this avoids using the Yosys
xprop
pass, but may prevent proving partitions equivalent when they contain uninitialized state or don’t-care values. (default value: on)
Example Configurations¶
Using the smtbmc
engine with the bitwuzla
solver to perform a depth 10
k-induction equivalence proof:
[strategy induction]
use sby
engine smtbmc bitwuzla
depth 10
Using the abc
engine with the pdr
solver to prove equivalence using the
PDR/IC3 algorithm:
[strategy induction]
use sby
engine abc pdr
The dummy
Strategy¶
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.