In reply to Marina.Miao:
.. to what extent I should know about assertions just for time-bound tasks.
I will appreciate it if you can point out the detailed sections of certain SVA book that I should pay close attention to.
The most important concepts that one need to understand about assertions include the following: (section/page references are from my SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- 1.2.1 What is a property? What is an assertion? 
- ATTEMPTS and THREADS, Vacuity : (1.4.3 Assertion states [pg 14..],
An attempt is the start of an evaluation of an assertion. Aside from the book explanation, you should take a look at my paper SVA Alternative for Complex Assertions
There, I explain a model for an assertion using SystemVerilog. Consider the section EMULATING A SIMPLE ASSERTION, also VACUITY:
// SVA assertion
ap_ab_then_c : assert property(@(posedge clk)
$rose(a) ##2 b |-> ##3 c);
// The model for the property
task automatic t_a2b_then_3c();
if($rose(a)) begin : rose_a
repeat(2) @(posedge clk); // can use ##2 instead
if(b) begin : got_b
repeat(3) @(posedge clk);
if(c) `uvm_info (tID,$sformatf("%m : AB_then_C PASS, c= %b", c), UVM_HIGH)
else `uvm_error(tID,$sformatf("%m : AB_then_C FAIL @ c= %b", c))
end : got_b
else return; // vacuous assertion, exit task
end : rose_a
// (file <a href="http://SystemVerilog.us/vf/abc_emul.sv" rel="nofollow">http://SystemVerilog.us/vf/abc_emul.sv</a>)
// Emulating the firing the assertion
always_ff @(posedge clk) begin // emulate the assertion firing
In the assertion @(posedge clk) $rose(a) ##2 b |-> ##3 c); and from the SystemVerilog model you can see the following
- At every (posedge clk), the leading clocking event, the assertion is attempted and fires as a separate automatic and totally independent task, unrealated to any previously fired task. Essentially, it's like a fire an forget, and the fired task has a life of its own. If the antecedent ($rose(a) ##2 b) succeeds, the test for the consequent ( ##3 c) contitues. Else, the assertion becomes vacuous (the return in the task emulation).
- Assertion success (true or vacuous) or failure.
- 1.4.3 Assertion states [pg 14] Those included attenpted, faiked, pass (vacuous or nonvacuous), active, inactive.
- Assertion outcome  Success, faikure, disabled, killed.
- 126.96.36.199 Important concepts on threads and sequences: [pg 28 .]
- Sequence syntax and operators [pg 22 ..] Most importantly, If a multi-threaded sequence is used in an antecedent (e.g., a ##1 b[*1:3] ##1 c |-> d), then all threads must be tested with its consequent for the assertion to terminate as successful.
- Table 3.1 Property Construct Syntax [pg 83 ..]
Of course, other concepts and examples of SVA provide the user a better understanding on how to apply SVA for your specific verification applications, I provide a lot of this throughut the book, particularly in 5 CHECKER, 6.9 CASE STUDY - SYNCHRONOUS FIFO, 7.3 CASE STUDY - FV OF A TRAFFIC LIGHT CONTROLLER, 10 Assertions Dictionary.
For training, consulting, services: contact http://cvcblr.com/home
* SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
* A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
* Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
* Component Design by Example ", 2001 ISBN 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
1) SVA Alternative for Complex Assertions
3) SVA in a UVM Class-based Environment