Assertion execution

SystemVerilog
, , , ,
1

I have this code,

property p1;
   @(posedge core_clk)	g1_g3 |-> g3_g4 ##0 g4_g5 ##0(1,$display("WITH EQ ASSERTION PASSED"));
endproperty
assert property (p1);
 
sequence g1_g3;
    @(posedge core_clk) $fell(g1) ##0 $rose(g3);
endsequence
 
sequence g3_g4;
    @(posedge core_clk) $fell(g3) ##0 $rose(g4);
endsequence
 
sequence g4_g5;
    @(posedge core_clk) $fell(g4) ##0  $rose(g5);
endsequence

I wanted to clarify my understanding of this assertions working. According to me if g1_g3 passes next g3_g4 at the same clk edge will be checked and so on. If g3_g4 fails then assertion will throw an error. Will it attempt to check again or compiler exits?

2

In reply to Annapoornahm:

Implication works each time there is a match on the antecedent(LHS), it proceeds to check the consequent (RHS). The antecedent checks every clock cycle. The consequent only checks on the same cycle as a match for |->, and on the next cycle for |=>.

3

In reply to Annapoornahm:
Your question suggests that you are missing very important concepts in SVA including:
important concepts about attempts and threads.
I explain these concepts in my paper:
Understanding the SVA Engine Using the Fork-Join Model
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.