In reply to Adarsh Santhosh:
Requirements The start and end are starting and ending sections of simulation.
And, the signal TB.a is high between start and end with TB.clk pulsing.
There are better ways to express your requirements.
module m;
bit clk, start, done, a;
// The start and done are starting and ending sections of simulation.
// And, the signal TB.a is high between start and done with TB.clk pulsing.
//
// 1) PREFERRED PROPERTY STATEMENT BECAUSE:
// * ap_preferred has ONE attempt
// * Upon a start, "a" remains hi until done
initial ap_preferred: assert property(@(posedge clk)
start[->1] |=> strong(a[*1:$] intersect done[->1] ));
// Also OK
initial ap_preferred_OK: assert property(@(posedge clk)
start[->1] |=> a s_until done);
// ALso OK
initial ap_preferred_with_OK: assert property(@(posedge clk)
start[->1] |=> a s_until_with done);
// 2) Assertion with unnecssary multiple threads and
// issues with the disable
property Test1;
@(posedge clk) disable iff (start || done)
a |=> always(a);
endproperty
ap_TEST1: assert property(Test1);
// ap_TEST1 is disable when start and done occurs
// ap_TEST1 has an attempt at every clocking event.
// If a==1, then a new thread is started, and every started thread
// checks that a==1 at every clock. Thus, if you have 100 clocks
// you end up with 100 separate threads, and each threads checks that
// taht a==1. Consider the checks
// cycle 1 2 3 4 5 .... 100
// Thread1 a a a a a .... a
// thread2 a a a a .....a
// thread3 a a a .....a
// thread 100 a
// If you insist on using the always
// Syntax
// $past ( expression1 [, [number_of_ticks] [, [expression2] [, [clocking_event]]] ] )
property Test_better;
@(posedge clk) disable iff ($past(done, 1, 1, @(posedge clk)))
start[->1] |=> always(a);
endproperty
initial ap_TEST_better: assert property(Test_better);
initial forever #10 clk=!clk;
initial begin
repeat(10) @(posedge clk);
$finish;
end
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
https://verificationacademy.com/verification-horizons/march-2022-volume-18-issue-1/reflections-on-users-experiences-with-systemverilog-assertions-sva
- 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/