Labs & tool setup

Every lesson's example code is a real file you can download and run. This page explains how to run them with free open-source tools or with a commercial formal tool, and lists every file.

What a lab folder contains

File	Purpose
`<design>.sv`	The RTL under test (sometimes with a deliberate bug — read the lesson).
`<design>_fv.sv`	The formal wrapper: instantiates the design, leaves its inputs free and holds assumptions, assertions and covers.
`<design>.sby`	A SymbiYosys run script with a `prove` task and a `cover` task.

Option A — open-source flow (SymbiYosys)

Download the latest OSS CAD Suite build for your OS from the YosysHQ oss-cad-suite-build releases on GitHub and extract it.
Activate it in your shell: source oss-cad-suite/environment (Linux/macOS) or run start.bat (Windows).

Put the example files of one lab in a folder and run:

shell

sby -f rr_arbiter.sby          # runs all tasks (prove and cover)
sby -f rr_arbiter.sby cover    # just the cover task

Each task creates a folder such as rr_arbiter_prove/. The summary says PASS or FAIL; counterexamples and cover traces are written as .vcd files under engine_*/. Open them with GTKWave (included in the suite).

Rewriting a concurrent property for the plain open-source front end

translation pattern

// Standard SVA (as used in the lessons)
a_req_gnt: assert property (@(posedge clk) disable iff (rst) req |=> gnt);

// Equivalent immediate-assertion style accepted by every Yosys build
logic past_valid = 1'b0;
always_ff @(posedge clk) past_valid <= 1'b1;

always_ff @(posedge clk)
  if (past_valid && !rst && !$past(rst) && $past(req))
    a_req_gnt_imm: assert (gnt);

Option B — commercial formal tools

Commercial FPV tools read the .sv files directly. A typical script looks like the pseudo-Tcl below; command names differ by vendor, so treat it as a checklist rather than exact syntax.

generic FPV script

# generic FPV script (adapt to your tool's command names)
analyze   -sv rr_arbiter.sv rr_arbiter_fv.sv
elaborate -top rr_arbiter_fv
clock     clk
reset     rst              ;# or: rely on the 'initial assume (rst)' in the wrapper
prove     -all
report

Every example file

Chapter	Files
Chapter 1: Welcome to Formal Verification	`credit_counter.sv` `credit_counter_fv.sv` `credit_counter.sby`
Chapter 2: How Formal Engines Think	`door_unlock_miter.sv` `phase_seq.sv` `decade_counter.sv` `decade_counter_fv.sv`
Chapter 3: SystemVerilog Assertions Essentials	`rr_arbiter.sv` `rr_arbiter_fv.sv` `rr_arbiter.sby`
Chapter 4: Formal Property Verification (FPV) Basics	`periodic_timer.sv` `fpv_timer.tcl` `periodic_timer_fv.sv` `periodic_timer.sby`
Chapter 5: Exploring New RTL with Formal	`lift_ctrl.sv` `lift_ctrl_fv.sv` `lift_ctrl.sby`
Chapter 6: FPV for Bug Hunting and Signoff	`sync_fifo.sv` `sync_fifo_fv.sv` `sync_fifo.sby`
Chapter 7: Formal Apps for Everyday Problems	`pinmux.sv` `conn_spec.csv` `gen_conn.py` `pinmux_conn_fv.sv` `csr_block.sv` `csr_block_fv.sv` `vr_checker.sv`
Chapter 8: Formal Equivalence Verification	`prio_enc_v1.sv` `prio_enc_v2.sv` `prio_enc_eq.sv` `adder_retime.sv` `adder_seq_eq.sv`
Chapter 9: When Proofs Lie: Avoiding False Positives	`updown.sv` `updown_fv.sv`
Chapter 10: Taming Complexity	`watchdog.sv` `watchdog_fv.sv`
Chapter 11: Formal Signoff on Real Projects	`fv_plan_template.md` `formal-ci.yml`
Chapter 12: Your Formal-Aware Workflow	`gray_counter.sv` `gray_counter_fv.sv` `pulse_stretch.sv` `pulse_stretch_fv.sv`

All example files are also included in the examples/ folder of the site source.

Was this page helpful?

Tip: select any text on the page before clicking Report and it will be quoted in your report.