# 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.