SystemVerilog Assertions :

Assertions are a useful way to verify the behavior of the design. Assertions can be written whenever we expect certain signal behavior to be True or False. Assertions help designers to protect against bad inputs & also assist in faster Debug. Assertions are critical component in achieving Formal Proof of the Design.

In general Assertions are classified into two categories:
1. Concurrent Assertions
2. Immediate Assertions

1. Immediate Assertions: These type of Assertions check the properties that hold True or False all the time i.e Clock independent. For Ex. :

P1 :  if (req.opcode != reserved)
      $error ("opcode Error seen");
assert property (P1);


P2 : assert property (!Read && !Write);

2. Concurrent Assertions: These type of assertions are clock based and therefore property is checked only @posedge or @negedge of the clock. These Assertions are more popular in most of the Synchronous Designs. For Ex. :

P1: assert property @(posedge clk) disable iff(!rst) (req |=> grant);

sequence s1;
 (valid == 1b1);
endsequence

sequence s2:
  ##[1:3] (data != '0);
endsequence

P2: assert property @(posedge clk) disable iff(!rst) (s1 |-> s2);

Since Assertions cannot be synthesized it is necessary to guard them with `ifdef and `endif. Alternately, Assertions are grouped into a dedicated package and the package is selectively added depending on the type of compilation. However, adding it into a package makes difficult to debug as source code is isolated.

Lets take a look at different examples of Assertion Operators:

1. $fell() : Event fell in between 2 consecutive cycles.
// clk enable is 0 after 1 cycle whenever valid is 0.
P1: assert property @(posedge clk) (~val) |-> ##1 $fell(clk_en);




2. $change() : Event changed in between 2 consecutive cycles.
// FSM State changes between 2 cycles whenever ack is received.
P2: assert property @(posedge clk) (~ack) |-> ##[1:2] $change(state);




3. $stable() : Event is stable in between 2 consecutive cycles.
// counter is stable whenever wren is 0.
P3: assert property @(posedge clk) (~wren) |->  $stable(count);




4. $onehot() : Event is onehot encoded.
// FSM State is onehot encoded
P4: assert property @(posedge clk) $onehot(fsm_state);




5. $onehot0() : Event is at the most onehot or it could be all 0s.
// Mux select is onehot encoded at most or could be 0.
P5: assert property @(posedge clk) $onehot0(mux_sel);




6. $rose() : Event rose in between 2 consecutive cycles.
// Grant is seen after 1 cycle whenever request is asserted.
P6: assert property @(posedge clk) (req) |=> $rose(grant);




7. $past() : Event was True in previous cycle.
// If grant was seen then request was seen previously.
P7: assert property @(posedge clk) (grant) |-> $past(req);




8.  ##N : One Event was followed by another event in N cycles. // see 1 for example.
   


    
9. ##[M:N] : One Event was followed by another event in between M to N cycles. // see 2 for example




10. [*N] : Event was repeated for at least N consecutive cycles.  
// whenever stall is asserted ack is low for 3 consecutive cycles
P10: assert property @(posedge clk) (stall) |-> (~ack)[*3];



       
11. if (cond) prop1 else prop2 : If condition (cond) is satisfied then
Property (prop1) is True otherwise property (prop2) is True.
P11: assert property @(posedge clk) if (fifo_empty) (!read_en) else (read_en);




12. Ev1 |-> Ev2 : Whenever Event (Ev1) is True then Event (Ev2) is also True. // see 1 for example




13. Ev1 |=> Ev2: Whenever Event (Ev1) is True then Event (Ev2) is also True 
starting next cycle. // see 6 for example




14. $isunknown() : Check if Event/Signal is X or Z.
// opcode should not be X or Z.  
P14: assert property @(posedge clk) $isunknown(opcode);




15. $countones() : Count the number of 1s in the Signal/Event.
//For a 3-bit Mux-sel, assert select values should be less than 6
P15 : assert property @(posedge clk) ($countones(mux_sel) < 3'h6);




16. k[*M:N] : Event (k) is expected to be repeated between M and N Cycles
 // Power off should result in valid out to be off in between 3 to 5 cycles.  
 P16: assert property @(posedge clk) (pwr_off) |-> (~valid_out)[*3:5];




17. k[->N] : Match the Nth cycle of the Event (k).
//whenever write val is asserted write is seen at 8th cycle.
P17: assert property @(posedge clk) (in_wr) |-> (~write_valid)[->8];




18. k[->M:N] : Match the event (k) is True from M to N Cycle.
//whenever read val is asserted read is seen between 8 to 10 cycles.
P18: assert property @(posedge clk) (in_rd) |-> (~rd_valid)[->8:10];




19. ##[0:$] or ##[*] : Open-ended, Event is True eventually or 
by end of simulation.
// Arbiter will grant request eventually if no stall and request is high.
P18: assert property @(posedge clk) (req & ~no_stall) |-> ##[1:$] grant;

Sequence is also used as a part of Assertions whenever there are a series of events that need to happen in order for the event to hold False or True. Here’s an example of sequence:

sequence req_active;
   //request is de-asserted and seen to be asserted in between 1 to 3 cycles
  (!req)  ##[1:3] $rose(req); 
endsequence

sequence stall_inactive;
 // Stall signal is held 0 to 3 consecutive cycles and then rose on 4th cycle
 (~stall)[*3] ##1 $rose(stall);
endsequence

// whenever sequence req_active is True then sequence stall_active is True.
assert property @(posedge clk) disable iff (~rst) (req_active |-> stall_active);

Its important to note that Assertions should not be more complex than necessary. If the Assertion is complicated then the conditions can be split into multiple Assertions for simplicity and Debug. Also, Assertions also act as useful way to determine if there is an X-prop issue in the logic. This can be simply checked by adding an assertion on control signals to check whether they are driven to known values i.e !$unknown(sig)