Proofs in Practice

The previous articles explained induction and strengthening on small examples. This article is about doing it in a real flow: how to set up a proof in SymbiYosys, which engines to use, what to do when the step will not pass, how to run both halves of a proof in ChipVerify Lab, and when to stop trying and report a bounded result instead.

9 min read | Intermediate

What You'll Learn

• Write a SymbiYosys configuration for a prove-mode run
• Choose between k-induction and the PDR engine
• Run the base case and the induction step in the lab with one switch
• Decide when to stop and how to report a proof that does not close

Prove Mode in SymbiYosys

A SymbiYosys run is described by a small .sby file. The lab writes one for you with mode bmc. A proof uses mode prove:

[options]
mode prove
depth 4

[engines]
smtbmc bitwuzla

[script]
read -formal design.sv
prep -top lockstep

[files]
design.sv

With the smtbmc engine, prove mode runs k-induction: a base case and an induction step, each of depth 4 here. The result is one of three statuses:

• PASS, "successful proof by k-induction": proven for every cycle.
• FAIL: the base case found a real counterexample from reset.
• UNKNOWN: the base case passed but the step failed. The step trace is in engine_0/trace_induct.vcd, next to the normal trace.vcd.

Engines That Find Helpers Themselves

k-induction needs you to supply the helper invariants. A second family of engines finds them automatically: IC3, also called PDR (property directed reachability). It builds up the missing relations between registers step by step, guided by the property. SymbiYosys offers it as abc pdr:

[engines]
abc pdr

On the lockstep counters, abc pdr proves done_a == done_b without the helper a == b, and it proves q != 11 for the decimal counter without the range helper:

SBY [run] summary: engine_0 (abc pdr) returned PASS
SBY [run] summary: engine_0 did not produce any traces
SBY [run] DONE (PASS, rc=0)

PDR is the workhorse of commercial tools for exactly this reason. It is not magic: on large designs it can run for a long time, and when it fails to converge you are back to helpers. A good practice is to run several engines in parallel, k-induction with your helpers and PDR, and take the first proof. The lab panel offers the BMC engines only, so PDR results appear in this tutorial as tool output.

Running It in ChipVerify Lab

Both halves of a proof can run in the lab as bounded checks. A switch in the file selects which one:

`ifdef FORMAL
// `define INDUCTION_STEP      // uncomment to run the induction step instead of the base case
`ifndef INDUCTION_STEP
  // base case: an ordinary bounded check from reset (depth >= K)
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) assert (done_a == done_b);
  always @(*) if (!init) assert (a == b);                 // helper invariant
`else
  // induction step with K = 1: start anywhere, properties hold in step 0, check step 1 (depth 2)
  always @(*) assume (!rst);
  reg [7:0] step = 8'd0;
  always @(posedge clk) step <= step + 8'd1;
  always @(*) if (step < 8'd1) assume (done_a == done_b && a == b);
  always @(*) if (step == 8'd1) assert (done_a == done_b && a == b);
`endif
`endif

Run it once as it is (the base case), and once with the `define line uncommented (the step). If both pass, the property is proven. The recipe works for any design: list every property and helper in both halves, use the same K in the step as the base case depth requires, and keep the step free of the reset assumption.

When the Step Will Not Pass

Strengthening can take many rounds on a real design. Some guidelines:

• Try a larger k once. If the failure needs only a few cycles of unreachable behavior, a modest k may be enough. If it keeps failing, stop raising it.
• Try PDR. If it proves the property, you are done.
• Add helpers one at a time, from the start state of each step trace, as the strengthening invariants article shows.
• Simplify the design for the proof: scale parameters down, cut out logic the property does not need. Chapter 8 covers these.
• Set a budget. If the proof does not close within it, report the property as bounded, with the depth, the covers that show the depth is meaningful, and a note on the open proof.

Common Mistakes