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;
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
$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
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