Sampling before the edge

Concurrent assertions never see the value drawn at the clock edge. They sample in the preponed region, the first region of the slot, using the values signals held just before the edge.

The mental model is a flip-flop sampling its D input. A signal changing exactly at the edge contributes its old value at that edge, and the new value only at the next edge. This removes the race with the design's own updates and matches register semantics.

The diagram uses pre-edge sampling, so each slot shows the same values an assertion would use. Watch sig lag req by exactly one slot.

• Slot 0: req 0, sig 0. Settled idle.

• Slot 1: req 1, sig 0. Req changed mid-cycle, and sig updates at this edge, so the pre-edge view still shows 0.

• Slot 2: req 0, sig 1. Sig now shows the slot-1 req.

• Slot 3: req 1, sig 0. Same one-slot lag.

• Slot 4: req 1, sig 1. Req held, so sig caught up.

The rule in one sentence: a concurrent assertion at edge N sees the values stable just before edge N. Outputs produced by edge N itself become visible at edge N plus 1.

Where the clock comes from

Every concurrent assertion needs a clocking event. State it in the property, inherit it from a default clocking block, or rely on inference inside a clocked procedure. Explicit clocks and default clocking are the styles to use.

1
2
3
4
5
6
7
8
9

// snippet
// 1. Explicit clock in the property, always unambiguous
// ap_a: assert property (@(posedge clk) req |-> ##[1:3] ack);
// 2. Default clocking, declared once and inherited by clockless properties
// default clocking cb @(posedge clk); endclocking
// ap_b: assert property (req |-> ##[1:3] ack);
// 3. Inferred from procedural context, legal but legacy style
// always @(posedge clk)
//   ap_d: assert property (req |-> ##1 gnt);

A multiclock property sequences across domains with one clock per piece. The clock switch happens at the join, and the fine print lives in Advanced SVA.

// snippet
// @(posedge clk_a) req_a |=> @(posedge clk_b) ##[1:4] ack_b;
// each piece evaluates on its own clock (full rules in Advanced SVA)

Reset gating with disable iff

disable iff is the property-layer reset gate, and its semantics are asynchronous abort. Whenever the expression is true, every in-flight attempt is killed at once, with no pass and no fail recorded.

The expression uses current values, not sampled values, so a mid-cycle reset pulse still aborts. Aborted attempts simply vanish, which is exactly right across reset: a handshake cut short by reset is neither a failure nor a pass.

1
2
3
4
5
6

// snippet
// the canonical pattern for an active-low asynchronous reset
// property p_req_ack;
//   @(posedge clk) disable iff (!rst_n)
//   req |-> ##[1:3] ack;
// endproperty

For a fully synchronous reset, asynchronous abort is usually still acceptable. When the spec defines behavior in the very cycle reset asserts, gate the antecedent instead, but know that gating alone cannot kill attempts that are already in flight.

1
2
3
4
5
6
7

// snippet
// sampled, clock-aligned gating: new attempts never start during reset,
// but an attempt opened before reset keeps running into it
// property p_sync_gate;
//   @(posedge clk)
//   (rst_n && req) |-> ##[1:3] ack;
// endproperty

Real environments gate more than one reset. A testbench-controlled disable term scopes error injection to one property, a shift register enforces clean cycles after deassertion, and each domain uses its own reset.

1
2
3
4
5
6
7
8
9
10

// snippet
// compound disable: hardware reset or a testbench-controlled quiet window
// property p_gated (sequence s_check);
//   @(posedge clk) disable iff (!rst_n || assertions_off)
//   s_check;
// endproperty
// checking behavior DURING reset: the antecedent is reset itself,
// so this property must NOT carry disable iff on that reset
// ap_quiet_in_reset: assert property (@(posedge clk)
//   !rst_n |-> (!valid && !req));

Common mistakes

When an assertion looks wrong, work the triage in order. Most cases end at step 3, with an edge-aligned transition.

1. Read the exact failing edge from the assertion message, with its label and time.

2. For each signal in the property, ask what it held just before that edge. That is what the assertion used.

3. Suspect signals that change at the failing edge first. The assertion saw their old value.

4. Check the viewer for a sampled or preponed value display if it has one.

5. Only then suspect the property logic itself.

One property gets one reset gate. A current-value disable iff plus a sampled in-expression reset disagree for one cycle around each reset edge, which produces failures that only reproduce with particular reset timing.

Testbench

The bench checks both halves of this lesson on real assertions. A flop's output must equal $past(d) at every edge, and a cover catches the edge where d is already 1 but q still reads 0. Then a request is cut short by reset, watched by the same window rule with and without disable iff.

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

module tb_sampling_reset;
  logic clk = 0;
  always #5 clk = ~clk;
  logic rst_n = 1;
  logic d = 0, q = 0;
  logic req = 0, ack = 0;
  int flop_fails = 0, gated_fails = 0, ungated_fails = 0, saw_old = 0, edges = 0;

  always @(posedge clk) q <= d;                 // a flop: q changes AT the edge

  // Sampled before the edge: q at this edge still holds the old value,
  // so it equals d from the edge before.
  ap_flop: assert property (@(posedge clk) ##1 (q == $past(d))) else flop_fails++;
  // A cover that only matches if the assertion saw q's old value at the edge
  // where d's new value was captured.
  cp_old: cover property (@(posedge clk) d && !q) saw_old++;

  // The same window rule with and without the reset gate.
  ap_gated: assert property (@(posedge clk) disable iff (!rst_n) req |-> ##[1:3] ack) else gated_fails++;
  ap_ungated: assert property (@(posedge clk) req |-> ##[1:3] ack) else ungated_fails++;

  always @(posedge clk) edges++;

  initial begin
    repeat (2) @(negedge clk);
    d = 1;                                      // q follows one edge later
    repeat (2) @(negedge clk);
    d = 0;
    repeat (2) @(negedge clk);
    @(negedge clk); req = 1;                    // a request ...
    @(negedge clk); req = 0; rst_n = 0;         // ... cut short by reset
    repeat (2) @(negedge clk);
    rst_n = 1;
    repeat (4) @(negedge clk);
    $display("flop check: %0d failures over %0d edges; d high while q still low was seen %0d times", flop_fails, edges, saw_old);
    $display("request cut by reset: gated check %0d failures, ungated check %0d failures", gated_fails, ungated_fails);
    if (flop_fails != 0 || saw_old == 0 || gated_fails != 0 || ungated_fails != 1) $fatal(1, "FAIL: sampling or reset verdicts");
    $display("PASS: the assertion saw pre-edge values, and disable iff aborted the attempt that reset cut short");
    $finish;
  end
endmodule

flop check: 0 failures over 14 edges; d high while q still low was seen 1 times
request cut by reset: gated check 0 failures, ungated check 1 failures
PASS: the assertion saw pre-edge values, and disable iff aborted the attempt that reset cut short

Related topics

• Sampled value functions

• Advanced SVA