Assertion Basics

System Verilog Assertion:-

Concurrent Assertion:-

Concurrent assertions are the work horses of the assertion notation. They must be clocked, either by specifying a clock edge with the assertion or by deriving a clock edge specification from a surrounding statement. Clocking is the key, because the evaluation of concurrent assertions starts every clock cycle with a new incarnation of a checker.

Example :- assert property @(posedge clk)

  a |=> b ##1 c ;

   endproperty

Concurrent assertions can also occur in sequential code. Here, they derive the synchronization and activation from the surrounding always block.

always_ff @(posedge clk) case (state) s0 : state <= s1; assert property ($past(state) = s4);

Sequence :-

Boolean expression events that evaluate over a period of time involving single/multiple clock cycles. 

Property :-

A number of sequences can be combined logically or sequentially to create more complex sequences. 

Assert :-

The property is the one that is verified during a simulation. It has to be asserted to take effect during a simulation

Operator information :-

•  and : When both sequence are expected to match, and both the sequence start at same time, but are not expected to finish at same time. Then and operator is used.
• intersect : When both sequence are expected to match, and both the sequence start and end at same time. Then intersectoperator is used.
• or : When one of the both sequence are expected to match. Then or operator is used.