Hello, first of all, thanks for your help, I am struggeling with this property.
I have a enable signal to activate the property. After that I want to count how many times an event 1 happens until another event 2 happens and then compare the counter with the reference.
The number of times event_1 happens before event_2 is random. Event_1 is a $fell(signal) condition.
In reply to salinerojj:
A very long long time ago when I was learning VHDL i used to ask a lot of questions.
Finally, a colleague gave me a good advice:
“Try a test code with the simulator; chances are that the simulator knows about the syntax much better than you”.
With this advice I did this because your code did not look right.
module m;
event event_1, event_2;
bit clk, enable;
int counter_reference=10;
property TEST(counter_reference);
int count;
@(posedge clk) enable |->
(event_1[=0:$],count=count+1) until event_2 ##0 count == counter_reference; // line 8
endproperty
ap_TEST: assert property(TEST(reference));
endmodule
Compiling module m
** Error: testbench.sv(8): (vlog-2110) Illegal reference to event "event_1".
** Error: testbench.sv(8): Illegal event value in SVA expression.
** Error: testbench.sv(8): Match items can not be attached to a sequence which admits empty match.
** Error: testbench.sv(8): (vlog-2110) Illegal reference to event "event_2".
** Error: testbench.sv(8): Illegal event value in SVA expression.
** Error: testbench.sv(8): Local variable count referenced in expression before getting initialized.
** Error (suppressible): testbench.sv(10): (vlog-1957) The sva directive is not sensitive to a clock. Unclocked directives are not supported.
** Error: testbench.sv(8): Local variable count referenced in expression before getting initialized.
Try something the following
module m;
event event_1, event_2;
bit clk, enable, a1, a2;
int reference=10;
task automatic count_events(int c);
bit done;
int count;
fork
while(done==0) @(event_1) count++;
while(done==0) @(event_2) done=1;
join
a_test: assert(count == c);
endtask
ap_test: assert property(@(posedge clk) enable |->
(1, count_events(reference)));
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
2) Free books:
* Component Design by Example https://rb.gy/9tcbhl
* Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
* A Pragmatic Approach to VMM Adoption
http://SystemVerilog.us/vf/VMM/VMM_pdf_release070506.zip
http://SystemVerilog.us/vf/VMM/VMM_code_release_071806.tar
3) Papers:
Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
Reflections on Users’ Experiences with SVA, part 1
https://verificationacademy.com/verification-horizons/march-2022-volume-18-issue-1/reflections-on-users-experiences-with-systemverilog-assertions-sva
Reflections on Users’ Experiences with SVA, part 2
https://verificationacademy.com/verification-horizons/july-2022-volume-18-issue-2/reflections-on-users-experiences-with-sva-part-2
SUPPORT LOGIC AND THE ALWAYS PROPERTY
http://systemverilog.us/vf/support_logic_always.pdf
SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/
Well, nicely explained. I got a few observations from this thread. I hope these are right.
In the questions event_1, event_2 are not signals . They are triggering controllers. So
the assertion wouldn’t be that simple and we cannot use repetition operators.
To solve such questions, we have to implement functions and implicitly count them. And
within the function, we can make an assertion one more time. Maybe there is a concept
called a nested assertion.
Now what if that event_1 and event_2 were signals? In that case, we could use the
following way.
module m;
bit event_1, event_2;
bit clk, enable;
int counter_reference=10;
property TEST;
int count=0;
@(posedge clk) enable |->
first_match((event_1,count++)[->0:$]) until event_2 |-> count == counter_reference; //
line 8
endproperty
ap_TEST: assert property(TEST);
endmodule
Immediate assertion can be inserted anywhere, in an always, always_comb, always_ff, task, function, or in a block (e.g. module m; bit a, b; assert(a && b); endmodule)
Ben
In reply to salinerojj:
You are correct that the go-to repetition operator only accepts boolean values.
But I don’t see a sequence with the goto in the code.
BTW, the 2nd implication is not needed and not recommended.
Since the until is a property operator, I changed the code to intersect
see Reflections on Users’ Experiences with SVA - Part II
module m;
bit event_1, event_2;
bit clk, enable;
int counter_reference=10;
property TEST;
int count=0;
@(posedge clk) enable |->
((event_1,count++)[->0:$] intersect event_2[->1]) ##0
count == counter_reference;
endproperty
ap_TEST: assert property(TEST);
endmodule
Hello Sir,
I have used the Second implication just for checking whether the nested implication works or not.
“until” operator, I used it because I knew that it is being added in the latest LRM and can be used instead of intersecting.
And one more thing is that my code. Is it actually wrong? Because I am not having any error messages on eda playground.
property_expr |-> property_expr IS ILLEGAL
// USING the -lca with VCS
Error-[SE] Syntax error
Following verilog source has syntax error :
“testbench.sv”, 8: token is ‘until’
first_match((event_1,count++)[->0:$]) until event_2 |-> count ==
counter_reference; // line 8
^
1 warning
1 error
CPU time: .212 seconds to compile
Exit code expected: 0, received: 1