A property that calls itself

A named property is recursive when its body instantiates itself, directly or through another property (16.12.17). Each instance checks the current tick and, after a time advance, starts a fresh instance with new arguments. The arguments are how state moves from one cycle to the next.

1
2
3
4
5
6
7
8

// snippet: two recursive properties from IEEE 1800-2012, 16.12.17
property prop_always(p);
  p and (1'b1 |=> prop_always(p));          // p now, and the same again next tick
endproperty

property prop_weak_until(p, q);
  q or (p and (1'b1 |=> prop_weak_until(p, q)));
endproperty

prop_always(p) means always p. prop_weak_until(p, q) means p holds at every tick up to, but not including, the first tick where q holds, and q need never hold: that is p until q. Both have built-in operators, so recursion adds nothing here. It earns its place when the next instance needs different arguments.

The four restrictions

Restriction 4 is the one people hit. To pass n - 1 or exp + 1 to the next instance, declare those formals local input. A local input formal is a local variable initialised from the actual argument when the instance starts.

When recursion beats repetition

Repetition operators repeat a fixed shape. Recursion repeats a shape whose parameters change: a beat count that goes down, an expected value that goes up, a phase that alternates. Take a stream that, after start, must deliver len beats with data d0, d0+1, d0+2 and so on, while valid may drop for any number of cycles between beats.

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

// not-run: Verilator 5.048 reports "Unsupported: Recursive property call"; Icarus 13 has no concurrent assertions
property p_beats(local input int unsigned left, local input logic [7:0] e);
  (left == 0)                                                    // done: true
  or (!valid and (1'b1 |=> p_beats(left, e)))                    // stall: same state next tick
  or (valid and (data == e) and (1'b1 |=> p_beats(left - 1, e + 8'd1)));
endproperty

property p_ramp;
  int unsigned n;
  logic [7:0]  e;
  (start, n = len, e = d0) |=> p_beats(n, e);   // capture len and d0 at the start tick
endproperty

a_ramp: assert property (@(posedge clk) disable iff (!rst_n) p_ramp);

The local variables in p_ramp capture len and d0 on the start tick. Passing len straight into p_beats(len, d0) after |=> would bind the values seen one tick later, which is a different property if the inputs move.

The repetition version needs a local variable updated inside a repeated subsequence, plus a separate count to end it, for example (start, n = len, e = d0) |=> ((!valid[*0:$] ##1 valid && data == e, e++, n--) [*1:$]) ... with an extra condition to stop at n == 0. It is harder to read and easy to get wrong. The recursive version is three cases, one per line.

Trace: how the instances unfold

len = 3, d0 = 0x40, start at t0, stall at t1 and t2

  tick  valid data   instance active          which case holds
  t1     0     --    p_beats(3, 0x40)         stall: start p_beats(3, 0x40) at t2
  t2     0     --    p_beats(3, 0x40)         stall: start p_beats(3, 0x40) at t3
  t3     1    0x40   p_beats(3, 0x40)         beat ok: start p_beats(2, 0x41) at t4
  t4     1    0x41   p_beats(2, 0x41)         beat ok: start p_beats(1, 0x42) at t5
  t5     1    0x42   p_beats(1, 0x42)         beat ok: start p_beats(0, 0x43) at t6
  t6     -     --    p_beats(0, 0x43)         left == 0: PASS

  Mutant: data at t4 is 0x42 -> the beat case is false, the stall case is
  false (valid is 1), left != 0 -> p_beats(2, 0x41) FAILS at t4.

This property is weak: it fails only at a tick that shows a violation. If the simulation ends during a long stall, the attempt has not failed. A lost stream therefore needs its own bound, such as a cover or a maximum-gap rule.

An equivalent check that runs

The bench below checks the same rule two ways. First, auxiliary state: a counter and an expected value updated in an always_ff, and a one-cycle assertion that data matches while beats are owed. Second, a recursive function that follows p_beats line for line over the recorded trace of sampled values. The bench requires both to report zero failures on 143 random bursts with 229 stall cycles.

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

// Ramp source: start loads len and d0, then sends len beats d0, d0+1, ...
// hold pauses the stream: valid drops and the next value waits.
module ramp_src (
  input  logic       clk,
  input  logic       rst_n,
  input  logic       start,
  input  logic [3:0] len,
  input  logic [7:0] d0,
  input  logic       hold,
  output logic       valid,
  output logic [7:0] data
);
  logic [3:0] left;
  logic [7:0] nxt;
  always_ff @(posedge clk) begin
    if (!rst_n) begin
      left  <= 0;
      valid <= 0;
      data  <= 0;
    end else if (start && left == 0) begin
      left  <= len;
      nxt   <= d0;
      valid <= 0;
    end else if (left != 0 && !hold) begin
      valid <= 1;
      data  <= nxt;
      nxt   <= nxt + 1;
      left  <= left - 1;
    end else begin
      valid <= 0;
    end
  end
endmodule

The aux version is valid only because a new start cannot arrive during a burst; the DUT ignores it. The recursive property has no such limit, because every start launches its own instance with its own arguments. With overlapping transactions, aux code needs one tracker per transaction in flight, which is the trade-off the next lessons build on.

To see it fail, change the DUT so that the first beat after a stall skips a value (data <= hold_q ? nxt + 1 : nxt, where hold_q is hold delayed by one cycle). The aux assertion fires on 152 beats and the recursive model rejects 108 bursts.

Related topics

• Previous: Abort Operators

• Next: let and Property Libraries

• nexttime, always, s_eventually, until (Part 4)

• Repetition: [*], [->], [=] (Part 4)