System Verilog Assertion State transitions

 Hello All,  today we will understand a unique concept from System Verilog Assertions. when we write down any assertion and run the simulation by asserting the property, it goes through multiple states internally.

we will understand this concept by taking one simple assertion example shown below.

property example();

@posedge(clk) disable iff (rst) a ##1 b |=> c##2 d;

endproperty

Label: assert property (example);

In above property for every positive clock edge we check for 'A' to be 1 followed by 'B' to be 1, this is antecedent. then we have implication operator for next cycle. then 'D' should be 1 , followed by 'D' should be 1 after 2 cycles. this is consequent. Assertion is disabled if rst is enabled.

Below is the diagram for SVA state transition.

A : Inactive to Active: At the beginning assertion will be in inactive state. it looks for first enabling condition to be true. In other sense antecedents first condition should be true to transition to next state which is active. 

In our example assertion, A should be high then assertion changes state from Inactive to Active. 

B: Active to Inactive: When in active state if assertion is incomplete, in other terms if first enabling condition becomes false then state transition from active to Inactive.

In our example assertion, if A goes back to 0 then assertion changes back to Inactive.

C: Active to Pass: When in active state if assertion is disabled state transitions from active to pass. this is also termed as vacuous success.  Another case in which this happens is when simulation completes before all enabling conditions are met.

In our example assertion, when rst is enabled it disables assertion and this state transition occurs. Also when simulation ends without A going to 1.

D: Active to Enable: When all the enabling condition is satisfied or when antecedent is true, then state transitions from active to enable. this is the when first half of the assertion is completed.

In our example assertion, when both a and b are as per the condition , then state transitions from active to enable.

E: Enable to Pass: When consequent is true after implication operator, then state moves from enable to pass.

In our example, when both c and d are true after the implication followed as per the assertion statement, then state transition happens from enable to pass.

F: Enable to Fail: When consequent is false / fails after implication operator, state moves from enable to fail.

In our example, when c is not 1 after implication or when d is not 1 after 2 cycles, state moves from enable to fail

G, H: Both these transition happens directly without any condition. After pass / fail, assertion automatically changes state to Inactive.

Above transition occur independently for each assertion instance. that was about the SVA state change concept, will come up with new topic next time till then keep exploring.