Automatic Checks

Properties the Code Implies

Some properties need no spec. A case implies its state stays among the listed values. An array implies its index stays in range. A narrower destination implies the sum fits. A tool can write these statements for every such line in a design and run them all.

Two kinds of statement come out. Reachability is a cover: each listed state should be reachable. Safety is an assert: no index, encoding or carry should go wrong. One log holds both verdicts.

Two Verdicts in One Log

Every listed state is reachable in both runs. The extra cover, state > S4, is the one that tells them apart: with the x default it is reached at step 6, with default: state <= S0 it is unreached. One arm changed (F1.3).

The asserts find the other two bugs. The index check fails at reported step 10: eight reads from reset take idx to 8. The carry check fails at step 3, the second add. With all three fixed, the set gives BMC PASS to depth 20 and abc pdr proves it in 496 ms.

Lint Says Could, Formal Says Does

Lint warned about the index on both the buggy and the fixed RTL, because the text is the same: four bits for eight entries. Only the state space shows that the wrap at 9 reaches entry 8. Lint said nothing about the missing arm or the dropped carry.

The limit cuts the other way too. A generated check proves the code agrees with itself. If the spec wanted wrap-around arithmetic, the carry assert is noise; if a state should never be entered, its cover being reached is the bug. Read every generated verdict against the spec.

Asked in Interviews

Try It

cover property (@(posedge clk) !rst && state == S3);
assert property (@(posedge clk) disable iff (rst) state inside {S0, S1, S2, S3, S4});
assert property (@(posedge clk) disable iff (rst) rd |-> idx < 4'd8);
assert property (@(posedge clk) disable iff (rst) acc_en |-> !sum[8]);

  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // generated: state legal, index in range, no dropped carry
  always @(posedge clk) if (!rst) begin
    a_state: assert(state <= S4);
    a_index: assert(!rd || idx < 4'd8);
    a_carry: assert(!acc_en || !sum[8]);
  end

[options]
mode cover
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top lint5
[files]
design.sv

1. Run the covers

   Run as it is: Cover reached, reported step 6. Read which covers the log names and at which step.

2. Fix the default

   Change the default to state <= S0 and run: Cover unreached within 20. Which cover is unreached now, and why is that good news?

3. Run the asserts

   Replace the covers with the three asserts and run with the index bug, then with the overflow bug. Read the step at which each fails.

4. Fix and prove

   With all three fixed, switch to mode prove with abc pdr: Prove PASS (abc pdr).

Check Yourself

module lint5(input clk, rst, go, rd, acc_en, input [1:0] mode, input [7:0] in,
  output reg [7:0] out=0, output reg [7:0] acc=0);
  localparam S0=3'd0, S1=3'd1, S2=3'd2, S3=3'd3, S4=3'd4;
  reg [2:0] state=S0;
  reg [3:0] idx=0;                 // read pointer: four bits for an eight-entry table
  reg [7:0] mem [0:7];
  wire [8:0] sum = acc + in;
  always @(posedge clk)
    if (rst) begin state <= S0; idx <= 0; acc <= 0; out <= 0; end
    else begin
      case (state)
        S0: if (go) state <= S1;
        S1: state <= mode[0] ? S2 : S3;
        S2: state <= S4;
        S3: state <= S4;
        S4: state <= S0;
        default: state <= S0;
      endcase
      if (rd) begin
        out <= mem[idx];
        idx <= (idx == 4'd9) ? 4'd0 : idx + 4'd1;   // bug: wraps at 9, not 7
      end
      if (acc_en) acc <= sum[8] ? 8'hFF : sum[7:0];   // saturates
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // generated: state legal, index in range
  always @(posedge clk) if (!rst) begin
    a_state: assert(state <= S4);
    a_index: assert(!rd || idx < 4'd8);
  end
`endif
endmodule