Appendix: the open-source flow

This lesson is labelled Appendix because it is the one place in the course that names tools. The headers you ran in the course runner map to files and commands here, and the verdicts agree because the engine underneath is the same family.

Why it matters

A course runner is convenient and opaque. Running the flow yourself turns each header into a project file you can read, a command you can rerun and a trace you can open.

Goal: a working local flow that proves, bounds and covers the decade counter. Inputs: a machine with the tools below. Steps: install and check versions, write the project file, run the three tasks, read the verdicts and the trace, map each concept across.

Installing and checking

You need four pieces: a synthesis front end with formal support, a SystemVerilog front-end plugin for the Boolean assertion style of this course, a bounded model checker script with induction support, and a solver. The baseline used here is Yosys 0.70 with its slang plugin, yosys-smtbmc driving Z3 5.1.0, and SymbiYosys 0.70. The cycle traces of the running designs were produced with Icarus Verilog. Check your installed version of each: header support moves with versions.

# not-run: appendix commands, not executed by the course runner
yosys --version        # a 0.70 baseline was used; check your installed version
sby --version          # 0.70 baseline; check your installed version
yosys-smtbmc --help   # lists the bounded, induction and cover options
z3 --version          # 5.1.0 baseline; check your installed version

What the open flow does versus the concept

Worked example: the counter project file

The course header prove 4 on the counter maps to a project file with three tasks, bmc, prove and cover. Modes and depths are set in the options section, one line per task; the engine line names the solver. counter.sv is the counter block of this lesson (below) without its first header line, so it starts at the line that defines the formal region and the front-end option needs no extra define.

# not-run: appendix project file, not executed by the course runner
[tasks]
bmc
prove
cover

[options]
bmc: mode bmc
bmc: depth 4
prove: mode prove
prove: depth 4
cover: mode cover
cover: depth 15

[engines]
smtbmc z3

[script]
plugin -i <path to the front-end plugin>
read_slang counter.sv --top mod10_counter
prep -top mod10_counter

[files]
counter.sv

Run each task and read the output:

# not-run: appendix commands, not executed by the course runner
sby -f counter.sby prove    # base case plus induction step: expect both to pass
sby -f counter.sby bmc      # bounded check only: expect no failure to depth 4
sby -f counter.sby cover    # expect every cover reached: c_nine and c_tc at step 10, c_wrap at step 14

The output names each assertion and cover with its status. A failure prints the failing property label and writes a trace file to read cycle by cycle. A cover not reached within the depth is inconclusive, never unreachable. A failed induction with a passing base case ends as UNKNOWN: file it as inconclusive, never as a pass.

The same header runs in the course, so the mapping is one to one:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

// formal: prove 4 expect pass slang top mod10_counter
`define FORMAL
// mod10_counter: decade counter, counts 0 to 9 and wraps to 0 while en is high, holds while en is low.
// tc is the terminal-count pulse. Synchronous active-high reset. BUG selects a variant (0 is the design
// as specified); HELPER=0 removes the helper assertion.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);
  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate
  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
`endif
endmodule

Vendor-neutral note

Commercial formal tools expose the same concepts under their own menus: task definition, engines, depth, time limit, verdicts, traces and cover mode. The ledger, the bound justifications and the mutation tables transfer unchanged. No commercial tool is named anywhere in this course, including here.

Limits stated honestly

• No true liveness engine ships in this flow: eventuality properties are not expressible, so the course uses bounded response with counters as the runnable substitute.

• Concurrent implication and sequence operators are rejected by the front end used here, which is why every lesson pairs the textbook form with a Boolean history form and runs the latter.

• The default front end rejects hierarchical references and bind; the slang front end accepts both. The reset-pair proofs of stage 2 use hierarchical references and need it; every other listing was written for the selected front end and is not claimed for the other.

• There is no X or Z in the two-state model: unreset registers are arbitrary values, and reset determinism is proved by two-copy comparison, never asserted from an unknown.

Related topics

• Back: Solutions, Ledger and Final Manifest

• Formal Glossary