Same statements, different jobs

A formal tool reads the same SVA as a simulator but uses each directive differently. There is no stimulus: the tool considers every input sequence the assumptions allow.

restrict exists for case splits: prove the ALU with restrict property (@(posedge clk) ctr == '0); for additions in one run and subtraction in another, without simulation flagging tests that use ctr = 1 (the LRM's own example). Verilator 5.048 compiled restrict and ignored it in simulation, as specified.

Safety and liveness

A safety property fails at a finite time: there is a cycle where you can point and say "here it broke". A liveness property says something good eventually happens; on an infinite trace a violation cannot be pinned to any cycle (16.12.15).

The second row catches people. In an assert or assume, a sequence without strong or weak is treated as weak (16.12.1), so ##[1:$] gives no failure if the grant never comes. In cover, the same sequence is strong.

Formal tools prove liveness directly, usually with fairness assumptions on the environment. Simulation cannot. The practical answer is to write both: a bounded version that simulation and bounded proofs can check, and an s_eventually version for the liveness proof.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

// not-run: Verilator 5.048 reports "Unsupported: s_eventually (in property expression)"; Icarus 13 has no concurrent assertions
// Formal harness for the arbiter below.
module rr_arb_formal (input logic clk, rst_n, input logic [3:0] req);
  logic [3:0] gnt;
  rr_arb dut (.*);
  for (genvar i = 0; i < 4; i++) begin : g
    // Environment: a request stays up until granted.
    m_hold: assume property (@(posedge clk) disable iff (!rst_n) req[i] && !gnt[i] |=> req[i]);
    // Liveness: every request is eventually granted.
    a_live: assert property (@(posedge clk) disable iff (!rst_n) req[i] |-> s_eventually gnt[i]);
    // Safety with a deadline: the stronger, design-specific claim.
    a_wait: assert property (@(posedge clk) disable iff (!rst_n) req[i] && !gnt[i] |-> ##[1:3] gnt[i]);
    c_wait: cover  property (@(posedge clk) disable iff (!rst_n) req[i] && !gnt[i] ##1 !gnt[i] ##1 !gnt[i] ##1 gnt[i]);
  end
  // Optional case split for one proof run: only requester 0 and 3 active.
  r_split: restrict property (@(posedge clk) req[2:1] == 2'b00);
endmodule

Habits that make assertions provable

• Synthesizable aux code only. Formal tools read RTL-like code. No classes, $urandom, # delays, fork, queues or DPI in the logic an assertion depends on.

• Assume inputs, assert outputs. An assumption on a DUT output hides bugs. Keep assumptions to the interface the environment drives.

• Cover every assumption's purpose. Too-strong assumptions make proofs vacuous. Covers on interesting states (a grant after a wait, a full FIFO) prove the constrained space still contains them.

• Bound what you can. Deep $past chains, wide counters and long ranges grow the state space. A bounded response window is often easier to prove than unbounded liveness, and it is what the spec usually means.

• Track one symbolic transaction. Instead of a table for every ID, track one ID chosen by the tool and held constant; a proof for an arbitrary ID covers them all.

• Assume-guarantee. The rule a producer's proof asserts on its output is the rule the consumer's proof assumes on its input. A library parameter that switches input-side rules between assert and assume lets one checker serve both.

1
2
3
4
5
6
7
8
9
10
11

// snippet: symbolic ID tracking for the out-of-order responder (previous lesson)
// sym_id is an input of the formal harness; the tool may pick any value, then it stays put.
m_sym:  assume property (@(posedge clk) $stable(sym_id));
logic       tracked;
logic [7:0] exp_d;
always_ff @(posedge clk)
  if (!rst_n)                              tracked <= 0;
  else if (req_valid && req_id == sym_id) begin tracked <= 1; exp_d <= req_data + 8'h11; end
  else if (rsp_valid && rsp_id == sym_id)  tracked <= 0;
a_sym:  assert property (@(posedge clk) disable iff (!rst_n)
          rsp_valid && rsp_id == sym_id |-> tracked && rsp_data == exp_d);

Runnable: the same rules in simulation

The bench checks a round-robin arbiter with the parts of the harness Verilator runs: the assumption (checked, as the LRM requires for simulation), two safety assertions and the bounded-wait assertion. The stimulus obeys the assumption by keeping each pending request until it is granted, which is what a formal tool would do automatically.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

// 4-way round-robin arbiter: one grant per cycle, rotating priority.
module rr_arb (
  input  logic       clk,
  input  logic       rst_n,
  input  logic [3:0] req,
  output logic [3:0] gnt
);
  logic [1:0] last;
  always_comb begin
    gnt = '0;
    for (int k = 1; k <= 4; k++) begin
      automatic logic [1:0] idx = 2'(last + k);
      if (gnt == '0 && req[idx]) gnt[idx] = 1'b1;
    end
  end
  always_ff @(posedge clk) begin
    if (!rst_n) last <= 2'd3;
    else
      for (int i = 0; i < 4; i++) if (gnt[i]) last <= 2'(i);
  end
endmodule

Two mutants. Replace the rotating priority with fixed priority (idx = 2'(k - 1)): requesters 2 and 3 wait too long and the bounded-wait assertion fails 2196 times. Change the stimulus so requester 2 drops a pending request: the assumption reports 132 violations, which is exactly the check that keeps a simulation environment honest about what the formal proof assumes.

Related topics

• Previous: Local Variables for IDs

• Topic hub: Assertion Depth

• assert, assume, cover, restrict and Action Blocks (Part 4)

• Q&A: Vacuity, Debug and Formal (Part 4)

• Next topic: Coverage Modelling