Hi, I had used the below assertion to check a particular sequence.
After “start” goes high, “signal” should go low and stay low till “cycle” = 'd21600.
initial ap_chk1: assert property (@(TB.cycle)
TB.start[->1] |->
##1 !TB.signal[->1]
#-# !TB.signal throughout (TB.cycle == 'd21600));
But, this pic shows unexpected behaviour where the assertion fails at first transition of “cycle” after “signal” goes low.
In reply to Adarsh24:
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
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
In reply to ben@SystemVerilog.us:
Sorry , for the late reply.
I got an error “Expected a verilog expression as operand to throughput operator” pointing to the “##0”.
I had tried,
initial ap_chk1: assert property (@(TB.cycle)
TB.start[->1] |->
##1 !TB.signal[->1]
##0 (!TB.signal throughout (TB.cycle == 'd21600)[->1]));
This is an example, I don’t know the requirements for thta R sequence
The intention was to check after “start” rises, “signal” goes low eventually and stays low till cycle count reaches 21600.
In reply to Adarsh Santhosh:
The following works for me
Edit code - EDA Playground
module m;
int cycle;
bit clk, signal, start=1;
initial forever #5 clk = !clk;
initial ap_chk1: assert property (@(posedge clk) // <------ leading clocking event
start[->1] |->
strong(##1 !signal[->1] // <---- the strong
##0 (!signal throughout (cycle == 'd21600)[->1])));
// The intention was to check after "start" rises, "signal" goes low eventually
// and stays low till cycle count reaches 21600.
initial begin
repeat(6) @(posedge clk)
#100;
$finish;
end
endmoduleA
/*
# ** Note: $finish : testbench.sv(15)
# Time: 605 ns Iteration: 0 Instance: /m
# ** Error: Assertion error.
# Time: 605 ns Started: 5 ns Scope: m.ap_chk1 File: testbench.sv Line: 6
# End time: 14:06:03 on Dec 30,2022, Elapsed time: 0:00:02
# Errors: 1, Warnings: 0 */
In reply to ben@SystemVerilog.us:
Thanks a lot, Ben.
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:
Thanks, Ben for your feedback.
I found the issue.
@posedge of “cycle” would mean the cycle number increases by 2 rather than increment by 1 which i was expecting.
Unfortunately, since i have no other clock at this late stage. I’m using @cycle[0] to do the assertio check and this works for me.
In reply to Adarsh24:
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).
In reply to ben@SystemVerilog.us:
Hi Ben,
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,”
In reply to ben@SystemVerilog.us:
Final would be
initial ap_chk1: assert property (@(cycle[0])
start[->1] |->
strong(##1 !signal[->1]
##0 (!signal throughout (cycle == 'd21600)[->1])));
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.