System verilog assertion - If b is asserted in the current cycle, a must have been present anywhere between 1 - 3 cycles earlier than b.

Problem Statement:

1. A and B are 2 pulses.

If B is asserted, A must have been asserted anywhere between 1 and 3 cycles in the past.

Solution :

We cannot use $past, as the problem requires the check to be range bound.

One way around is to use an intermediate signal ( vector).

Let us try using an vector to accommodate the length of duration to be under check.

In our case, it is between 1 and 3.

Therefore , let us take an intermediate signal arr, ranging from 3:0.

Each bit position corresponds to 1 cycle.

Code snippet will be something like this:

always @(posedge clk) arr = {[arr[2:0],a};

Code for assertion :

  property check;
    @(posedge clk) (b==1) |-> $countones(arr[3:1])>=1; // omit arr[0] as this is represents the time at which 'b' is set to 1
  endproperty: check

  a_check: assert property (check);

One more way to do it is the use of sequence.triggered.

As per LRM, triggered is a method, which checks if the operand sequence has reached its end point at that point in time.

Using this, we can write a sequence and check whether it reached its endpoint before $rose(b).

sequence s_1;

  @(posedge clk) $rose(a) ##[1:3]  1;

endsequence: s_1

property test_1;

  @(posedge clk) $rose(b) |-> s_1.triggered;

endproperty: test_1

Notes:

Now the sequence s_1, checks for $rose(a) between 1 and 3 cycles.

property test_1 checks if the s_1.triggered is reached to its endpoint at $rose(a).

Code with stimulus :

module top;
  bit a;
  bit b;
  bit [3:0] arr;

  bit clk;

  initial  begin
    $timeformat(-9,3,"ns",8);
    clk <= 0;
    forever #5 clk = !clk;
  end

  initial
    $monitor("%0t - A -%0d B -%0d Arr:%0b",$time,a,b,arr);

  initial begin
    repeat(1) @(posedge clk);
    a = 1;
    repeat(1) @(posedge clk);
    a = 0;

    repeat(2) @(posedge clk); // Check should pass, as 'a' is asserted 3 cycles before 'b'.
    b = 1;
    repeat(1) @(posedge clk);
    b = 0;
  
    repeat(3) @(posedge clk); // Check should fail, as 'a' is not present in the previous 3 cycles
    b = 1;
    repeat(1) @(posedge clk);
    b = 0;
   
    repeat(1) @(posedge clk); // Check should fail, as 'a' and 'b' are asserted in the same cycle.
    a = 1; b = 1;
    repeat(1) @(posedge clk);
    a = 0; b = 0;

    repeat(4) @(posedge clk);
    $finish;
  end

  always @(posedge clk) begin
    arr <= { arr[2:0], a };
  end

  property check;
    @(posedge clk) (b==1) |-> $countones(arr[3:1])>=1; // omit arr[0] as this is represents the time at which 'b' is set to 1
  endproperty: check

  a_check: assert property (check);
endmodule

Result :

Compiler version L-2016.06; Runtime version L-2016.06;  Jul 29 04:18 2020
0ns - A -0 B -0 Arr:0
5ns - A -1 B -0 Arr:1
15ns - A -0 B -0 Arr:10
25ns - A -0 B -0 Arr:100
35ns - A -0 B -1 Arr:1000
45ns - A -0 B -0 Arr:0
75ns - A -0 B -1 Arr:0
"assertion_past_value.sv", 51: top.a_check: started at 85000ps failed at 85000ps
        Offending '($countones(arr[3:1]) >= 1)'
85ns - A -0 B -0 Arr:0
95ns - A -1 B -1 Arr:1
"assertion_past_value.sv", 51: top.a_check: started at 105000ps failed at 105000ps
        Offending '($countones(arr[3:1]) >= 1)'
105ns - A -0 B -0 Arr:10
115ns - A -0 B -0 Arr:100
125ns - A -0 B -0 Arr:1000
135ns - A -0 B -0 Arr:0
$finish called from file "assertion_past_value.sv", line 40.
$finish at simulation time    145ns