Regarding of the next cycle implication operator, it defined as if expr1 is true then expr2 must be true at the next evaluation point.
expr1 |=> expr2;
I’m trying to use next cycle implication operator in my example assertion.
timescale 1ns/1ps
module ex3;
reg clk;
reg reset;
reg a;
reg b;
initial begin
reset = 1;
#11;
reset = 0;
end
initial begin
clk = 0;
a= 0;
#13 a = 0;
#0 a = 1;
#2 a = 0;
#2 a = 1;
#2 a = 0;
#2 a = 1;
#2 a = 0;
#2 a = 1;
#2 a = 0;
end
initial begin
b = '0;
#13 b = 0;
#2 b = 0;
#1 b =1;
#3 b =1;
#1 b =1;
#1 b =1;
#1 b =1;
#1 b = 0;
end
always #1 clk = ~clk;
property cycle_delay_repetition_range;
@(posedge clk) disable iff (reset)
~a |=> a;
endproperty
check08 : assert property (cycle_delay_repetition_range);
But I got assert fail. Could you let me know what am I supposed to do to resolve this fail?
In reply to UVM_LOVE:
Your testbench approach needs strong reconsiderations.
I suggest that you read my reply to this question:
Got this question:
Q: I need your advice in getting started with verification with systemverilog. I 've built various projects using Verilog and they was FPGA and ASIC synthesizable. what I need now is a road map that get me started with verification for example SVA , UVM and SV testbenches
A: To better respond to this question I am attaching a file that addresses the build of a verification plan, quick-and dirty partition testing, a reference to my co-author Srinivasan Venkataramanan on UVM, SVA and learning SVA.
I welcome comments from this community.
FIle also at LinkedIn
That link is a pdf file.
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
thanks I update some test initial sequence about ‘a’.
as you see, ‘a’ has to change as ‘1’ after disable period.
then the assertion is working I though. but problem is that assertion check in disable period.
so the assertion fail has propagated to non disable period.
I though that SVA does not sample in the disable period. but I SVA sampled the signal even in the disable period.
would you please let me know more detail about why time 13NS assertion has failed?
What am I supposed to do?
Hi Ben,
Now I’m reading your attached documents, So I think your are trying to tell me about SVA testbench must be conducted on non-blocking domain. so my blocking test sequence in initial statement is wrong.
In reply to UVM_LOVE:
…"SVA testbench must be conducted on non-blocking domain. "
[Ben] Not quite. However, typically, signals are assigned nonblocking and occur in the NBA region. Doing a #10 a=1; with posedge(clk) changing at t is same time when “a” changes can be problematic. It is also not stylist, though it should work; this is because within a time step signals used in an assertin are sampled in the Preponed region with the value just before the time step. What would be better is to do something like
@(posedge clk) a=1; // or a <=1;
Assertion sample signals in the Preponed region
See my paper 3) Understanding Assertion Processing Within a Time Step (Horizons Feb 27, 2023 issue)
This paper goes into detail about how evaluation regions should be handled by a simulator as described in the SystemVerilog LRM; this should give you a better understanding of how assertions work.
// I do the following:
initial begin
$dumpfile("dump.vcd"); $dumpvars;
bit v_a, v_b, v_err;
repeat (200) begin
@(posedge clk);
if (!randomize(v_a, v_b, v_err) with {
a dist {1'b1 := 1, 1'b0 := 1}; // *****CAN USE signal a
// a changes in the Active region ************ OK
v_b dist {1'b1 := 1, 1'b0 := 2};
v_err dist {1'b1 := 1, 1'b0 := 15};
}) `uvm_error("MYERR", "This is a randomize error");
if(v_err==0) b<=v_b; else b<=!v_b;
// b changes in the NBA region ****************
end
$finish;
end
In reply to UVM_LOVE:
Look, I’m not a SVA expert at all, and it’s so embarrassing to even open my mouth when Ben is also responding to you…
But in general I have two basic recommendations:
Add prints that describe the situation when the assert fails:
asset () else $error(“expect that a = … but a = %b, b = %b, time = %t”, a,b,$time);
Write a property with arguments, and send arguments when you assert:
property check(clk,a)
…
endproperty
assert property (c,x) else $error(…);
here c = clk and x = a.
In reply to UVM_LOVE:
Look, I’m not a SVA expert at all, and it’s so embarrassing to even open my mouth when Ben is also responding to you…
But in general I have two basic recommendations:
Add prints that describe the situation when the assert fails:
asset () else $error(“expect that a = … but a = %b, b = %b, time = %t”, a,b,$time);
[Ben] You need the $sampled
asset property () else
$error("expect that a = ... but a = %b, b = %b, time = %t",
$sampled(a),$sampled(b),$realtime);
Write a property with arguments, and send arguments when you assert:
property check(clk,a)…endproperty
assert property (c,x) else $error(…);
here c = clk and x = a.
Unless you see the need for reuse, which is usually rare, I do not use arguments because they make the assertion hard to read. For me, I have to mentally convert the formal arguments to the actual arguments while I am composing or reading an assertion.
Sorry, it gives me mental “fatigue!”
:)
Ben