Install SymbiYosys and run your first formal verification jobs

SymbiYosys is a front-end driver program for Yosys-based formal hardware verification flows. The chapters take you from installing it on Linux to checking two RISC-V cores against the RISC-V specification, and to proving that a refactored core still behaves like the original.

Each step shows the commands to type and the output they print. The tutorial covers Linux on x86-64.

Start chapter 1

chapters

designs verified

3 h

to complete

licenses needed

Chapters

Chapter 1

What is SymbiYosys, and how does a proof run?

What SymbiYosys does: the steps from Verilog to a verdict, the bmc, prove and cover modes, the proof engines, the assertions its free front ends accept, and how it compares with commercial tools.

read -formal counter.sv

15 minOpen

Chapter 2

Install SymbiYosys on Linux

Install SymbiYosys, Yosys and eight proof engines on Ubuntu Linux from one pinned OSS CAD Suite release, without sudo, and avoid stale packages, empty downloads, PATH conflicts and Python changes.

Yosys 0.70+190 (git sha1 485b63564, …)

15 minOpen

Chapter 3

Run your first proofs on a counter

Run six SymbiYosys jobs on a modulo-10 counter: a bounded check, a counterexample to an injected bug, a cover trace, a failed induction step, a helper assertion, and IC3/PDR engines.

terminal

$ sby -f counter.sby bug

… failed assertion … counter.sv:39 … step 6

[counter_bug] DONE (FAIL, rc=2)

FAILcount = 10 at step 6

35 minOpen

Chapter 4

Verify the SymbiYosys FIFO example

Run the FIFO example that ships with the OSS CAD Suite: its labelled assertions and covers, task tags and default tasks, and the counterexample produced when the pointer protection is removed.

terminal

$ sby -f fifo.sby nofullskip

… failed assertion fifo.a_count_diff … step 2

[fifo_nofullskip] DONE (FAIL, rc=2)

FAILa_count_diff at step 2

15 minOpen

Chapter 5

Verify the wb2axip skid buffer

Prove ZipCPU's wb2axip skid buffer with SymbiYosys: four parameter combinations from one job file, input rules that switch between assume and assert, and the folder sby resolves file paths from.

terminal

$ sby -f skidbuffer.sby

[skidbuffer_prfc] summary: successful proof by k-induction.

[skidbuffer_cvr] DONE (PASS, rc=0)

PASS4 proofs and 1 cover

15 minOpen

Chapter 6

Verify an AXI-Lite slave against a protocol checker

Prove ZipCPU's easyaxil AXI-Lite slave against the reusable faxil_slave protocol checker with SymbiYosys: six tasks, four configurations, and the induction depth the proof needs.

terminal

$ sby -f easyaxil.sby prfreg cvrreg

[easyaxil_prfreg] summary: successful proof by k-induction.

[easyaxil_cvrreg] DONE (PASS, rc=0)

PASSproved against faxil_slave

15 minOpen

Chapter 7

Verify the NERV RISC-V core with riscv-formal

Verify the NERV RISC-V core with riscv-formal and SymbiYosys: how RVFI works, one instruction check, all 96 checks, and the counterexample produced by a bug injected into the ADD instruction.

terminal

$ sby -f insn_add_ch0.sby

… rvfi_insn_check.sv:177 … step 10

[insn_add_ch0] DONE (FAIL, rc=0)

FAILinjected ADD bug found

30 minOpen

Chapter 8

Find PicoRV32's built-in test bugs with riscv-formal

Run riscv-formal on the PicoRV32 RISC-V core, switch on its built-in test bugs one at a time, and see which check catches a register-file bug and which catches a bug in the core's RVFI reports.

terminal

$ sby -f reg_ch0.sby

… rvfi_reg_check.sv:42 … step 25

[reg_ch0] DONE (FAIL, rc=0)

FAILtest bug 001 found

25 minOpen

Chapter 9

Check a refactored design for equivalence with EQY

Check that a refactored RISC-V core still behaves like the original with EQY, the Yosys equivalence checker: find an injected shifter bug, prove the fix, and compare RTL with a synthesized netlist.

terminal

$ eqy -f nerv_change_fail.eqy

… Failed to prove equivalence of partition nerv.next_rd

[nerv_change_fail] DONE (FAIL, rc=2)

FAILshifter bug found in 1 of 44 partitions

20 minOpen

Chapter 10

Read the results and fix common errors

How to read a SymbiYosys run: the DONE line and its return codes, the work folder, viewing and replaying traces, and the cause and fix for each error that appears in this tutorial.

terminal

[counter_prove_weak] … returned pass for basecase

[counter_prove_weak] … returned FAIL for induction

[counter_prove_weak] DONE (UNKNOWN, rc=4)

UNKNOWNnot a bug report

15 minOpen