---
title: "Formal proofs and equivalence"
---

# Formal proofs and equivalence

SymbiYosys proofs and covers in the Testing view, counterexamples in the waveform viewer, equivalence checking of a synthesised netlist against the RTL or of two designs with eqy, and property templates.

Formal work uses SymbiYosys (`sby`) and YosysHQ eqy, both installed by you and run as separate programs. Everything on this page is **verified on Linux** with SymbiYosys and eqy. Nothing is verified on Windows. Concurrent SVA and PSL need a commercial front end and are not supported.

## Run proofs and covers

Each SymbiYosys (`.sby`) file of the project appears in the Testing view under **HDL Formal**, with its tasks. `formal` in `hdl.json` lists the files as globs; by default every `.sby` file of the project. Tasks a file writes with Python are listed through `sby --dumptasks`; the default tasks run when the file is run.

A run uses the installed `sby` and its solvers, writes to the build folder, and follows sby's live JSON stream:

- each assert and cover appears under its task at the line that states it;
- an assert is shown as proven, passed to the task's depth (bounded model check), or failing at a step, and an induction failure is told apart from a counterexample;
- a cover is shown as reached at a step;
- a task that does not finish shows SymbiYosys's error.

Counterexample and cover traces are linked from the result and open in the [waveform viewer](https://neuralinverse.com/docs/modules/hdl/waveforms/).

## Check equivalence

| Command | What it proves |
|---|---|
| **Check Synthesized Netlist Against RTL** | That an open-flow target's netlist (iCE40, ECP5, Gowin, AMD 7-series through openXC7) is equivalent to the RTL. It uses the last build's netlist, or a fresh synthesis when the build is older than the sources |
| **Check Equivalence of Two Designs...** | That two sets of sources are equivalent, for example two revisions |

The Editor writes the `.eqy` file (with the `sat` and `sby` strategies) to `<build>/equivalence/` and runs eqy. Against a synthesised netlist, the check leaves unmatched the names the netlist keeps on undriven nets, and optimises the RTL's registers as synthesis does (`opt_dff`), so a correct design with uninitialised registers and state machines is proven equivalent.

An **HDL Equivalence** entry in the Testing view shows each partition as equivalent, different or not proven; a different partition's counterexample opens in the waveform viewer. Your project's own `.eqy` files are listed and run too.

Known limits found on the example design:

- On the Artix-7 (openXC7) netlist, 410 of 888 partitions were proved; on 311 the SymbiYosys strategy stops at the FIFO's memory, which Yosys 0.33 cannot model there, so the check is not proved.
- The ECP5 check cannot run: Yosys 0.33 has no simulation model for its multiplier.
- Equivalence covers open-flow netlists only; Vivado and Quartus netlists are not checked.

## Property templates

In Verilog and SystemVerilog files, typing `formal-` offers asserts, assumes and covers in a form Yosys reads: `$past`, `$stable`, `$rose`, `$fell` and `$onehot`, reset handling under `` `ifdef FORMAL ``, valid/ready stability and FIFO bounds.

![Formal property templates offered while writing assertions in a properties module](https://neuralinverse.com/docs-images/modules/hdl/formal-property-templates.webp)