Three jobs

Each construct answers a different question about the same interface.

• assert checks design obligations and flags violations.

• cover tracks whether important scenarios are reachable/exercised.

• assume constrains environment behavior, mainly in formal contexts.

• Avoid over-constraining assumptions that exclude real bug traces.

1
2
3
4
5
6
7
8

// snippet
cover property (@(posedge clk) disable iff (!rst_n)
  req); // exact antecedent exercise/reachability
cover property (@(posedge clk) disable iff (!rst_n)
  req ##1 grant);

assume property (@(posedge clk) disable iff (!rst_n)
  !(req && cancel));

The first cover names the exact antecedent req; the second asks for the stricter one-cycle answer sequence. The assume states one environment rule: cancel never rides with a request.

One trace, three readings

All three constructs read the same signals. The trace below has two requests, answered after two cycles and after one, and one cancel on an idle cycle.

Each slot is one clock cycle, numbered from 0; read each construct against the slots it names.

• Assert req |-> ##[1:3] grant: the request in slot 1 is answered in slot 3 (two cycles) and the one in slot 5 in slot 6 (one cycle). Both are inside the window, so nothing is reported.

• Cover req: hits in slots 1 and 5, so the assertion was exercised, not passed vacuously.

• Cover req ##1 grant: misses for the slot 1 request (no grant in slot 2) and hits in slot 6. One hit is enough to mark the scenario covered.

• Assume !(req && cancel): cancel is high only in slot 4, where req is low, so the stimulus kept its promise. In formal, the tool would never even try a trace with both high.

Strong promises hide bugs

An assume removes traces instead of checking them. When it states design behavior rather than environment behavior, it removes the failing trace and the bug survives review.

1
2
3
4
5
6
7

// snippet
// Good: a rule about the environment (inputs only).
assume property (@(posedge clk) disable iff (!rst_n)
  !(req && cancel));
// Bad: a rule about the design under test. It assumes the grant the proof should check.
assume property (@(posedge clk) disable iff (!rst_n)
  req |-> ##1 grant);

Keep assumes to input rules such as the cancel rule above. Grant timing stays an assert, where a violation is evidence.

Common mistakes

Testbench

Three responders answer the same stimulus with one-, two-, and three-cycle latency. Cover counters record each latency, one monitor per responder checks the window, and the cancel input exercises the environment rule.

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

// A responder with latency D: grant is high exactly D cycles after a req
// pulse, as sampled on the clock.
module grant_resp #(parameter [2:0] D = 2) (
  input  logic clk, rst_n, req,
  output logic grant
);
  logic [2:0] cnt;
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) cnt <= 3'd0;
    else if (req) cnt <= D;
    else if (cnt != 3'd0) cnt <= cnt - 3'd1;
  end
  assign grant = (cnt == 3'd1);
endmodule

// Plain-RTL form of: req |-> ##[1:3] grant.
// Each pending bit records one request age; overlapping windows are preserved.
module grant_window_mon (
  input  logic clk, rst_n, req, grant,
  output logic violation
);
  logic [2:0] pending;
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin pending <= 3'd0; violation <= 1'b0; end
    else begin
      violation <= pending[2] && (grant !== 1'b1);
      if (grant === 1'b1) pending <= {2'b00, req};
      else               pending <= {pending[1:0], req};
    end
  end
endmodule

• Result: 180 matched sampled grants in each age bin, with all pending requests drained. Changing all responders to D=2 would produce 540 age-2 hits and fail the bin checks.

• Expected checks: zero window violations and zero cycles with req and cancel together.

Related topics

• Immediate vs concurrent assertions

• Common RTL property templates