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