Throug****hout
The syntax for this sequence is:
expression_or_dist throughout sequence_expr.
The throughout operator specifies that a signal (expression) must hold throughout a sequence.
( b throughout R ) is equivalent to ( b [*0:$] intersect R )
// R is a sequence, b is a variable
initial ap_chk1: assert property (@(TB.cycle)
TB.start[->1] |->
##1 !TB.signal[->1]
##0 (!TB.signal throughout (TB.cycle == 'd21600)[*8])); // (TB.cycle == 'd21600)[->1]) ??
// This is an example, I don't know the requirements for thta R sequence
See my paper on that subject: Reflections on Users’ Experiences with SVA, part 2
I had an issue when I was experimenting with below code. Basically, if i use odd numbers in below equalency check.
(cycle == 'd29)
Assertion will fail. But, will pass for even numbers. eg: 'd28
module m;
int cycle,reset;
bit clk, signal, start;
initial forever #3 clk = !clk;
initial ap_chk1: assert property (@(posedge cycle)
start[->1] |->
strong(##1 !signal[->1]
##0 (!signal throughout (cycle == 'd29)[->1])));
// The intention was to check after "start" rises, "signal" goes low eventually and stays low till cycle count reaches 21600.
always @(posedge clk) begin
if (reset) begin
cycle <= 8'b0;
end else begin
cycle <= cycle + 1; end end
initial begin
$dumpfile("dump.vcd"); $dumpvars;
reset <= 1;
#10;
reset <= 0;
#10;
start <= 1;
#10;
signal <=0;
#10;
repeat(6) @(posedge clk)
#100;
$finish;
end
endmodule
I was wondering if it was an issue with equalency check, so that it checks only LSB. But, using the below code, I saw 19th cycle was only true.
always @(posedge clk) begin
if (cycle == 'd19) begin
$display("true");
end else begin
$display("false"); end end
In reply to Adarsh Santhosh:
You use #10 in your initial and # in your clock generation.
Use the clock instead of the delays in your initial.
Keep everything synchronized to the same clock if the design is synchronous!
What you have is bad style.
initial begin
$dumpfile("dump.vcd"); $dumpvars;
reset <= 1;
repeat(2) @(posedge clk); // #10; // assuming you want about 10
reset <= 0;
repeat(2) @(posedge clk) // #10;
start <= 1;
repeat(2) @(posedge clk)#10;
signal <=0;
repeat(2) @(posedge clk) / #10;
repeat(6) @(posedge clk)
#100;
$finish;
end
endmodule
In reply to ben@SystemVerilog.us:
… I’m using @cycle[0] to do the assertion check and this works for me.
From a paper I am currently writing: “clocking events occurring in the same time step in different regions (e.g., Active, NBA, Reactive) are indistinguishable in concurrent assertions due to sampling of signals”.
Thus, if your @(cycle[0]) occurs in the same time stamp as your clock edge, then the sampled values of the signals are the same as if the asssertion have a lead clock of @(clk) (or whatever edge of the clk).
I think I got your point. But, this cycle count is not derived from any clock.
Its based on pre-fixed no. of cycles and the testbench knows what tasks are to be called in each cycle.
These tasks have hard-coded # delays. Its a TB generated by a design-for-test tool. It takes in timeplate definitions and makes #delays based on that. At the end of the test, the actual clocks are not pulsing. It will be mostly dead cycles(no pulsing).
.
I just needed something close to the end of sim which can be pre-determined. Like a fixed no. of cycles in the test.
In reply to Adarsh24:
SO what is your final assertion?
Also see (1) - EDA Playground
There is a response to a comment made on linkedIn about
“Is cycle incremented somewhere?
What happens if cycle == 21600 is reached before signal goes low? It will keep looking for 21600 either till cycle wraps around again to 21600 which will signal success (is it correct?) Or reach end of simulation and declare failure (if the simulator handles strong correctly).
I think that the assertion should make sure that if 21600 is reached before !signal it is a failure regardless. Or, I may have misread something,”
In reply to Adarsh24:
SO what is your final assertion?
Also see (1) - EDA Playground
There is a response to a comment made on linkedIn about
“Is cycle incremented somewhere?
What happens if cycle == 21600 is reached before signal goes low? It will keep looking for 21600 either till cycle wraps around again to 21600 which will signal success (is it correct?) Or reach end of simulation and declare failure (if the simulator handles strong correctly).
I think that the assertion should make sure that if 21600 is reached before !signal it is a failure regardless. Or, I may have misread something,”
Q: Is cycle incremented somewhere?
A: The cycle is incremented at the end of a task after all the #delays . This task is used at the end of every cycle.
I mentioned task, its actually section of case statement.
Q: What happens if cycle == 21600 is reached before signal goes low? It will keep looking for 21600 either till cycle wraps around again to 21600 which will signal success (is it correct?) Or reach end of simulation and declare failure (if the simulator handles strong correctly).
I think that the assertion should make sure that if 21600 is reached before !signal it is a failure regardless. Or, I may have misread something,"
A: Yes, if the !signal doesnt happen before expected cycle, assertion should fail in the expected cycle. I think the strong & throughout in assertion will provide that check.