Hi! I need to detect if some pulse_x occurs within some number of clock cycles of another pulse_y., They are separate signals. pulse_x can be before or after pulse_y, so as long as it occurs within some max relative to pulse_y. Any idea on how one could use SVAs to check for this?
Thanks for your response. Here is some more information. Yes, they are synchronous. We can even assume that they are single cycle pulses. They are pseudo periodic in the sense that their nominal period is the same but there is a bit of jitter.
So, lets say the nominal period is 1024 cycles. That can vary by +/- 5 or so but on average is 1024. Relative to pulse_y, pulse_x should arrive within, say, 20 cycles - either before or after but not both. In other words, if I took a snapshot of pulse_y in time and looked back 20 cycles and looked ahead 20 cycles, I should find a pulse_x. If there isn’t one, it is detected as a failure.
Iff I am reading the assertion above correctly, one of them might fail even when the circuit is doing the right thing.
Note: it is perfectly acceptable for the two pulses to occur at the same time (since it is within +/- 20 cycles). Hope this helps understanding the requirement better.
In reply to Soofster:
9/08/2021
I updated this model to correct a few mistakes.
Alas, experts do make mistakes, we’re human too :)
// Key assertions (abbreviated to show the concepts)
//y -1--------------------------1--------------------------1--------------------------1----
//x -1-----------------------1-------------------------------1------------------------1----
sequence x_to_y_edp; @(posedge clk) (x ##[0:max] y); endsequence
p_y2x_before: y |-> x_to_y_edp.triggered); // property for reuse only
p_ytox_after: y |-> ##[0:max] x); // property for reuse only
ap_y2x_x2y: (p_y2x_before or p_ytox_after); // check within range
ap_no_x2x: (x |-> not(x ##0 !y[*0:max] ##1 y ##[1:max] x or
x ##1 !y[*1:max] ##1 y ##[0:max] x));
ap_no2x_between_2ys: (y |-> not( (y ##0 x[->2] ##1 1[*1:$] or
y ##1 x[->2] ##1 1[*0:$]) intersect
##1 y[->1]));
/* Hi! I need to detect if some pulse_x occurs within some number of clock cycles of another pulse_y.,
They are separate signals. pulse_x can be before or after pulse_y, so as long as it occurs within
some max relative to pulse_y. Any idea on how one could use SVAs to check for this?
pulse_x: _________^____________________________^____________________^___________________________________^________^______
pulse_y: _____________^____________________^________________________^___________________^___________________________^___
...............................................................................................................
failure ...........................................................<...................................>............... (for example)
Thanks for your response. Yes, they are synchronous. We can even assume that they are single cycle pulses.
They are pseudo periodic in the sense that their nominal period is the same but there is a bit of jitter.
So, lets say the nominal period is 1024 cycles. That can vary by +/- 5 or so but on average is 1024.
Relative to pulse_y, pulse_x should arrive within, say, 20 cycles - either before or after but not both.
In other words, if I took a snapshot of pulse_y in time and looked back 20 cycles and looked ahead 20 cycles,
I should find a pulse_x. If there isn't one, it is detected as a failure.
Iff I am reading the assertion above correctly, one of them might fail even when the circuit is doing the right thing.
Note: it is perfectly acceptable for the two pulses to occur at the same time
(since it is within +/- 20 cycles). Hope this helps understanding the requirement better. */
// If x occurred, then y within 1024-20 cycles.
// If y then x within 20 cycles
// if x then no x until y plus 20 cycels after y
module m;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, x, y, err;
let max=12; let cycles=123;
int delay;
event e0, e1, e2, e_beforex, erandom;
initial forever #10 clk = !clk;
//let period=1024;
// y--------112---123y
// ------------xxxxxxx // zones where x can occur before y
let xl_legal_2y=cycles+1-max; // 124-12= 112
sequence x_to_y_edp; // for use in x to y endpoints
@(posedge clk) (x ##[0:max] y); //
endsequence
always @(x_to_y_edp.triggered) -> e_beforex; // for debug
// x <-- 0 to max ...> y
property p_y2x_before;
(@ (posedge clk) @(posedge clk) y |-> x_to_y_edp.triggered);
endproperty
ap_y2x_before: assert property(p_y2x_before); // for debug ONLY
// y <-- 0 to 20 ...> x
property p_ytox_after;
(@ (posedge clk) @(posedge clk) y |-> ##[0:max] x);
endproperty
ap_ytox_after: assert property(p_ytox_after); // for debug ONLY
ap_y2x_x2y: assert property( p_y2x_before or p_ytox_after); // KEEP THIS
//-- NO ...x <---1 to max ...> y <---1 to max ...> x
//>>>ap_no_x2x0: assert property(@ (posedge clk) x |-> not(x ##1 !y[*1:max] ##1 y ##[1:max] x));
ap_no_x2x: assert property(@(posedge clk) x |->
not(x ##0 !y[*0:max] ##1 y ##[1:max] x or
x ##1 !y[*1:max] ##1 y ##[0:max] x));
ap_no2x_between_2ys: assert property(@(posedge clk) y |->
not( (y ##0 x[->2] ##1 1[*1:$] or y ##1 x[->2] ##1 1[*0:$]) intersect
##1 y[->1]));
initial forever begin
y <=1'b1;
-> e0;
@(posedge clk)
y <=1'b0;
repeat(cycles) @(posedge clk);
end
initial begin
// good conditions
repeat(3) begin // NO jitter
x <=1'b1;
-> e1;
@(posedge clk)
x <=1'b0;
repeat(cycles) @(posedge clk);
end
repeat(3) begin // NO jitter
x <=1'b1;
-> e1;
@(posedge clk)
x <=1'b0;
repeat(8) @(posedge clk);
x <=1'b1;
-> e1; ->e1;
@(posedge clk)
x <=1'b0;
@(posedge y);
end
// Jitter after 10 cycles
repeat(3) begin // NO jitter
repeat(3) @(posedge clk) ;
x <=1'b1;
-> e1;
@(posedge clk)
x <=1'b0;
repeat(cycles-10) @(posedge clk);
end
// x 2 x
@(posedge y);
repeat(cycles-1) @(posedge clk);
repeat(2) begin // NO jitter
repeat(1) @(posedge clk) ;
x <=1'b1;
-> e1;
@(posedge clk)
x <=1'b0; ->e1;
end
repeat(2) begin // NO jitter
@(posedge clk) ;
x <=1'b1;
-> e1;
@(posedge clk)
x <=1'b0;
repeat(cycles-8) @(posedge clk);
x <=1'b1;
-> e1;
@(posedge clk)
x <=1'b0;
@(posedge y) repeat(4) @(posedge clk);
x <=1'b1;
-> e1;
@(posedge clk)
x <=1'b0;
end
// Jitter before by 10
repeat(3) begin // NO jitter
repeat(cycles-10) @(posedge clk) ;
x <=1'b1;
-> e1;
@(posedge clk)
x <=1'b0;
repeat(10) @(posedge clk);
end
// random
-> erandom;
repeat (200) begin
if (!randomize(delay, err) with {
delay >115 && delay < 135;
err dist {1'b1 := 1, 1'b0 := 9};
}) `uvm_error("MYERR", "This is a randomize error");
repeat(delay) @(posedge clk);
-> e1;
x <=1'b1;
@(posedge clk)
x <=1'b0;
if(err==1) begin
repeat(4) @(posedge clk);
-> e2;
x <=1'b1;
@(posedge clk)
x <=1'b0;
repeat(20) @(posedge clk);
-> e2;
x <=1'b1;
@(posedge clk)
x <=1'b0;
end
end
$finish;
end
endmodule
