Hi, I am new to SVA’s though I have written few assertions but found this one to be a little tricky. Please excuse me in case its a simple assertion.
Please check the above image for the requirement:
only 1 pass scenario exists since signal_2 is expected to be exactly same as signal_1 but a delayed version;
fail (there can be many other fail scenarios in the picture i just mentioned 1 such case).
Thanks in advance
In reply to gumpena@usc.edu:
Keep in mind that an assertion is a statement or directive that a given property is required to hold. Assertions can be expressed in many ways, including regular code.
In SystemVerilog, that can be done in SVA or other plain SystemVerilog options.
Your requirement to verify that a wave of any shape, the duration of highs and lows of s1 are the same as s2, but delayed.
It’s too complex to do in SVA, but you can use the task method, as explained in my paper
SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
Below is an untested method where I measure that the duration in cycles of s1 pulse in high level is the same as s2 (delayed) also staying a 1 for that duration.
You need to do the same for when the signals are in the low state, the t_fell() task.
task automatic t_rise();
int s1_r1r1; // S1 rise to rise
int s2_r1r1; // S2 rise to rise
s1_r1r1=0;
fork
begin // record wave for s1
while (s1==1) begin
@(posedge clk)
s1_r1r1++; // compute #cycles s1==1
end
end
begin
while (s2==1) @(posedge clk); // wait for s2 to rise
s2_r1r1=0;
while (s2==1) begin
@(posedge clk)
s2_r1r1++; // compute #cycles s1==1
end
end
join
label: assert (s1_r1r1==s2_r1r1)
else $error("s1 high pulse != s2 high pulse ");
endtask
always @(posedge clk) begin
if($rose(s1)) t_rise();
if($fell(s1)) t_fell();
end
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
In reply to ben@SystemVerilog.us:
Another approach is to first compute the initial delay between S1 and S2 and store that in a variable. Using the package sva_delay_repeat_range_pkg;
(item 2 in my signature).
// v is first computed. Assertions disabled
$rose(S1) |-> q_dynamic_delay(v) ##0 $rose(S2);
$fell(S1) |-> q_dynamic_delay(v) ##0 $fell(S2);
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
Hi Ben,
Thanks a ton for your prompt response, after going through the 2 solutions you mentioned above I came up with the below 2 scenarios (image attached: if not able to view here is the link Imgur: The magic of the Internet).
Though I have not tested the 2 approaches you mentioned. I suspect case 1 will return pseudo pass with approach 1 and case 2 is interesting to try with approach 2. However thanks a lot i can build upon the idea you gave and give this a try.
In reply to gumpena@usc.edu:
Need to add
initial begin
@(posedge clk);
while (!rose(S1) || !$fell(S1)) begin
assert(!rose(S2) || !$fell(S2))
else $error("S1 pulse wih no s2 pulse ");
@(posedge clk);
end
end
Ben systemverilog.us
In reply to gumpena@usc.edu:
Is your delay between sig1 and sig2 constant? If so, how about:
$rose(sig_2) |=> $past(sig_1, 3)
Similarly for $fell - also you may need to tweak the delays a bit (I didn’t test it).
Good Luck
Srini
www.verifworks.com
Thanks Ben for the Solution,
@Srini The delay is not constant that is the reason I could not think of any SVA.
In reply to gumpena@usc.edu:
You can get a partial check through some modeling code:
bit s1_seen;
always_ff @(posedge clk) begin : glue_logic
if ($rose(sig_1) begin
s1_seen <= 1'b1;
end
if ($rose(sig_2) begin
s1_seen <= 1'b0;
end
end : glue_logic
// Now a property..
$rose(sig_2) |-> s1_seen;
I term this as weak as it does not take care of all scenarios, but towards that direction.
HTH
Srini