The req/ack contract

The requester raises req and holds it. The responder answers with a one-cycle ack inside a bounded window.

After the ack, req falls and the bus stays quiet for a gap. Each rule polices one phase of that shape.

Watch req hold until ack, then fall; the quiet slots delimit the gap.

• Slot 0: idle: req 0, ack 0.

• Slot 1: req rises; the hold obligation begins.

• Slot 2: req held; the window is still open.

• Slot 3: ack pulses; latency is 2 cycles.

• Slot 4: req released in the next cycle.

• Slot 5: quiet; first gap cycle.

• Slot 6: quiet; second gap cycle.

• Slot 7: the next request may rise.

The checker module

Inside a sequence the checker writes x == 1'b0 instead of !x: Verilator 5.048 rejects a unary ! after ##, although IEEE 1800 allows it.

The listing is one file you can paste into the Code Lab: the checker first, then a small design and a bench that runs legal traffic before planting one bug at a time. Every rule reports through fail(), which counts and prints the report and lets the run go on; Verilator 5.048 stops at the first $error, and production checkers often count the same way.

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
44
45
46
47
48
49
50
51

module req_ack_checker #(
  parameter int ACK_MIN = 1,
  parameter int ACK_MAX = 8,
  parameter int GAP     = 2,
  parameter int REL     = 1
)(
  input logic clk, rst_n,
  input logic req,
  input logic ack
);
  int n_fail = 0, n_min = 0, n_max = 0;
  function automatic void fail(string msg);
    n_fail++;
    $display("[%0t] req_ack_checker: %s", $time, msg);
  endfunction

  // R1: req held until ack
  a_req_hold: assert property (@(posedge clk) disable iff (!rst_n)
    (req && !ack) |-> ##1 req)
    else fail("req dropped before ack");

  // R2: ack arrives inside the window after the request rises
  a_ack_window: assert property (@(posedge clk) disable iff (!rst_n)
    $rose(req) |-> ##[ACK_MIN:ACK_MAX] ack)
    else fail("ack missed window");

  // R3: no ack without a pending request
  a_no_spurious_ack: assert property (@(posedge clk) disable iff (!rst_n)
    ack |-> req)
    else fail("ack with no pending req");

  // R4: ack is a single-cycle pulse
  a_ack_pulse: assert property (@(posedge clk) disable iff (!rst_n)
    ack |-> ##1 (ack == 1'b0))
    else fail("ack wider than one cycle");

  // R5: pulse-ack release within REL cycles
  a_req_release: assert property (@(posedge clk) disable iff (!rst_n)
    (req && ack) |-> ##[1:REL] (req == 1'b0))
    else fail("req not released after ack");

  // R6: the quiet gap starts the cycle after the fall
  a_req_spacing: assert property (@(posedge clk) disable iff (!rst_n)
    $fell(req) |-> ##1 (req == 1'b0) [*GAP])
    else fail("re-request inside gap");

  c_min_lat: cover property (@(posedge clk)
    $rose(req) ##ACK_MIN ack) n_min++;
  c_max_lat: cover property (@(posedge clk)
    $rose(req) ##ACK_MAX ack) n_max++;
endmodule

3 legal transactions: 0 new report(s)
covers: minimum latency hit 1, maximum latency hit 1
[245] req_ack_checker: req dropped before ack
[275] req_ack_checker: ack missed window
req dropped after one cycle (hold, then the window echo): 2 new report(s)
[345] req_ack_checker: ack missed window
ack after 6 cycles against a window of 4: 1 new report(s)
[415] req_ack_checker: ack with no pending req
ack with no request: 1 new report(s)
[495] req_ack_checker: re-request inside gap
re-request after 1 quiet cycle against a gap of 2: 1 new report(s)
PASS: legal traffic hit both covers, and each planted bug was reported by the rule that owns it

The level form req |-> ##[1:N] ack spawns one window thread per held cycle. The edge form $rose(req) spawns exactly one thread per transaction.

In a failure cascade the earliest report is the root cause. An early req drop trips the hold rule first, and the window rule echoes later.

Pulse discipline

Three widths hide under one name. Exact-one is a rise followed by a fall; minimum holds for N cycles; maximum falls within N cycles.

The band form composes a floor with a ceiling. All four are clocked-sample rules, blind to sub-cycle glitches.

1
2
3
4
5
6
7
8
9

// snippet
// a_exact1: assert property (@(posedge clk) disable iff (!rst_n)
//   $rose(kick) |-> ##1 !kick);
// a_min: assert property (@(posedge clk) disable iff (!rst_n)
//   $rose(p) |-> p[*MIN]);
// a_max: assert property (@(posedge clk) disable iff (!rst_n)
//   $rose(p) |-> ##[1:MAX] !p);
// a_band: assert property (@(posedge clk) disable iff (!rst_n)
//   $rose(p) |-> (p[*MIN] ##[1:MAX-MIN+1] !p));

Common mistakes

What the run shows

Three legal transactions give no reports and hit both latency covers. A request dropped after one cycle gives two reports in order: the hold rule first, then the window rule four cycles later. The first report is the root cause, and the second is its echo. A late ack, an ack with no request and a re-request inside the gap each give one report, from the rule that owns that phase.