Your First Formal Run

This article walks through a complete formal run in ChipVerify Lab: a small counter, one assumption, two assertions, the settings of the formal panel, and the log that the tool prints. By the end you can run a formal check on your own design and tell what the result means.

9 min read | Beginner to Intermediate

What You'll Learn

• Write the properties for a small counter in SVA and in the form the lab reads
• Set the top module, solver engine and depth in the formal panel
• Read the SymbiYosys log of a passing run step by step
• Explain what a pass at a given depth does and does not promise

The Design: A Saturating Counter

A saturating counter counts up while its enable is high and stops at a maximum value instead of wrapping around to 0. Counters like this are used to count retries, errors or idle cycles, where a wrap would turn a large count into a small one. This one stops at 12:

module sat_counter (input clk, input rst, input en, output reg [3:0] q);
  always @(posedge clk)
    if (rst)                    q <= 4'd0;
    else if (en && q != 4'd12)  q <= q + 4'd1;
endmodule

The register q has 4 bits, so it could hold any value from 0 to 15. The design is supposed to keep it at 12 or below. That is exactly the kind of rule a formal tool can check for every input sequence.

The Properties in SVA

Two rules describe the counter:

• The count is never larger than 12.
• Once the count is 12, it stays at 12 until the next reset.

In SystemVerilog Assertions they read:

a_max:  assert property (@(posedge clk) disable iff (rst) q <= 4'd12);
a_stay: assert property (@(posedge clk) disable iff (rst) (q == 4'd12) |=> (q == 4'd12));

The first line is the same pattern as in the first article of this tutorial. The second one introduces the operator |=>, read as "then, in the next cycle". If q is 12 in one cycle, it must be 12 in the next cycle too. Chapter 3 explains this operator, called implication, in detail.

A commercial formal tool reads these two lines directly. The open-source engine of the lab needs the same rules in a different form.

The Same Rules in the Form the Lab Reads

The lab reads the design with Yosys, which does not accept assert property, disable iff or |=>. It accepts plain assert and assume statements inside always blocks, and the function $past, which gives the value of a signal one clock cycle earlier. Here is the counter with its properties in that form:

module sat_counter (input clk, input rst, input en, output reg [3:0] q);
  always @(posedge clk)
    if (rst)                    q <= 4'd0;
    else if (en && q != 4'd12)  q <= q + 4'd1;

`ifdef FORMAL
  reg init = 1'b1;                                 // 1 only in the first cycle
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);              // start from a reset

  // a_max: never above 12
  always @(posedge clk) if (!init) assert (q <= 4'd12);

  // a_stay: once at 12 it stays at 12 (until a reset)
  always @(posedge clk)
    if (!init && !$past(rst) && $past(q) == 4'd12 && !rst)
      assert (q == 4'd12);
`endif
endmodule

Line by line:

• `ifdef FORMAL: the formal tool defines the macro FORMAL when it reads the file, so this section is seen by the formal tool and ignored by simulators and synthesis.
• init is a helper register that is 1 in the first cycle and 0 forever after.
• assume (rst) in the first cycle tells the tool to start from a reset. Without it the tool may start the register at any value, including 15, and report a failure that cannot happen in a real chip that is reset at power-up.
• assert (q <= 4'd12) is the rule a_max, checked at every clock edge after the first.
• The second assertion uses $past to look one cycle back: if the counter was 12 and no reset happened, it is still 12. This is what |=> does in SVA.

The ifdef FORMAL and the formal wrapper article explains these lines in more detail, and shows how to keep the properties in a separate file.

The Formal Panel

Open the design in ChipVerify Lab and select the Formal panel. A formal run follows these steps:

The panel has these settings:

• Design Files: the files that are read, in order. Submodules come before the modules that use them. Testbench files are left out automatically.
• Top Module: the module to check, here sat_counter.
• Solver Engine: Bitwuzla, Z3 or Boolector. Bitwuzla is the default and the best first choice.
• BMC Depth: the number of clock cycles the tool examines, up to 10 on the free tier and up to 100 with PRO.
• Run Formal Verification: starts the run. The log appears in the console.

Leave the engine at Bitwuzla, set the depth to 10, and run.

Reading the Log of a Passing Run

The lab runs SymbiYosys, which prints a log like this one, shortened:

SBY [run] engine_0: ##   0:00:00  Solver: bitwuzla
SBY [run] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY [run] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY [run] engine_0: ##   0:00:00  Checking assumptions in step 1..
SBY [run] engine_0: ##   0:00:00  Checking assertions in step 1..
...
SBY [run] engine_0: ##   0:00:00  Checking assertions in step 9..
SBY [run] summary: engine_0 (smtbmc bitwuzla) returned pass
SBY [run] DONE (PASS, rc=0)

Each "step" is one clock cycle. For every step the tool first checks that the assumptions can still be met, then asks the solver whether any assertion can fail in that step. Step 0 is the first cycle, the reset cycle. With a depth of 10 the tool checks steps 0 to 9 and then stops. The lab then prints its own summary: PASS, "No counterexample found within the specified depth."

What a Pass Means Here

The words "within the specified depth" matter. This run proves that no input sequence of up to 10 cycles, starting from reset, can break either assertion. It does not say anything about cycle 11 or later.

For this counter that is a real limitation. The counter needs 13 cycles to climb from 0 to 12 (one reset cycle, then 12 counts), so a depth of 10 never even reaches the value 12. The second assertion is never really tested: its condition, "the counter was 12", never comes true within 10 cycles.

With PRO the depth can be raised to 20, which covers the climb and several cycles at 12. That run also passes on the lab engine. It is a much stronger result, because now both rules have been checked in the situation they are about. Chapter 5 shows how to choose a depth, and Chapter 6 shows how to prove a rule for any number of cycles.

When Something Goes Wrong Before the Check

Not every run ends in PASS or FAIL. If the design does not compile, the log shows an error from Yosys and the lab reports ERROR. The most common one for beginners is the concurrent SVA form, which the lab front end rejects with a syntax error at the @. The lab then suggests the form shown above. A run can also hit the time limit of 300 seconds, usually because the depth is too large for the design. Lower the depth and try again.

Running It in ChipVerify Lab

The example below contains the counter and both assertions, ready to run. Try it at depth 10. With PRO, try depth 20 as well and compare how long the two runs take.

Common Mistakes