VLSI Excellence

Nonconsecutive Repetition : - Repeated, Nonconsecutive Boolean expressions can be defined using [=N] - Nonconsecutive - Not necessarily consecutive - Syntax : expr[=N]; expr must occur N times - Example : When A is high then from the same cycle , there must be two cycles of B before C property NONCONSECUTIVE_REPET; @(negedge CLK) A |-> B[=2] ##1 C; endproperty assert property (NONCONSECUTIVE_REPET); Note: In Non Consecutive Repetition Sequence , here there is no restrictions of number of cycles between second B and C. Go-To Repetition : - Syntax : expr[->N] - Go to repetition operator is similar to the Nonconsecutive operator except expr must be true in the last cycle of the sequence - Example : When A is high then from the same cycle , there must be two cycles of B before C , with C immediately following the second B ...

Consecutive Repetition : - Repeated, consecutive sequences can be defined using [*N] - Syntax : SEQ[*N]; SEQ, repeated N times - Example : A is never low for more than 4 cycles property CONSECUTIVE_REPET; @(negedge CLK) !A[*4] |=> A; endproperty assert property (CONSECUTIVE_REPET); Consecutive Repetition with Ranges : - Syntax : SEQ[*min : max] ; SEQ will repeat from min to max times - Example : A is low for 2 to 4 cycles only property CONSECUTIVE_REPET_RANGE; @(negedge CLK) A ##1 ~A |=> !A[*1:3] ##1 A; endproperty assert property (CONSECUTIVE_REPET_RANGE); Consecutive Repetition - Special Range Cases : - Lower bound can be 0 - No minimum number of repetition , sequence may be absent ...

Here, is the flow diagram of how an assertion gets evaluated - Syntax : @(Clocking) disable iff (EXPR) enabling_sequence |=> fulfilling_sequence

System Verilog Sequences : - Temporal properties are described using sequences - Series of Boolean equations - Each cycle separated by ## - Syntax : SEQ_A |-> SEQ_B OR SEQ_A |=> SEQ_B - Properties are either unconditional using instantaneous Boolean expression property UNCONDITIONAL: @(posedge CLK) (COUNT >10); endproperty - OR , conditional using implication operators property CONDITIONAL; @(posedge CLK) A |=> B ##1 C; endproperty - If Enabling Sequence (A) is True, than only Fulfilling Sequence (B ##1 C) will Evaluate. Disabling Properties - - To terminate an assertion when a condition is true - use disable iff (expr) - If expr is true at any point of time, then the property is terminated and it Passes. - Useful for cancelling multicycle sequence properties -...

Problem: Write assertion(s) to verify the behavior of the below circuit - Solution:

$past() : - Returns the value of a signal from previous evaluation cycle - Syntax : $past (A, N) ; Default N = 1 - Example : property PAST1; @(negedge CLK) EN |-> (OP == $past(IP , 2 )); endproperty assert property (PAST1); $stable() : - Returns a Boolean True value if expr has the same value as it did in the previous cycle. - Syntax : $stable(expr) - Example : property STABLE; @(negedge CLK) ~ENAB |=> $stable(DOUT); endproperty assert property (STABLE); $countones() : - Returns the number of 1's in expr - Any value other than 1 is ignored - Syntax : $countones(expr) - Example : property 1HOT_CHK; @(negedge CLK) ($countones(B_VECTOR) == 1); ...

Assertion Overlapping : - Assertions are checked at every evaluation point. - If the start condition is true, a new assertion is triggered. - Many copies of an assertion may be active simultaneously. Example : property A0; @(negedge CLK) REQ |=> ACK; endproperty assert property (A0); Since, the REQ is still high at second negedge of CLK and it triggers an unexpected second assertion. Note: Assertions must be carefully written to avoid unexpected failures from overlapping. How this can be avoid OR how can you code a robust assertion ? - Use built-in functions for detecting value change. - $rose() and $fell() - Useful for making properties edge triggered. - One way to avoid overlapping - $rose(expr) - True if expr has changed value and it is 1 in the current cycle - $fell() - True if expr has changed value and it is 0 in the current cycle - $rose() is true for x-...

Lets have a look at below FSM Design - DATA_VALID is an input signal. DATA_READ is an output signal. Write assertions to verify the state transition from current state and inputs and outputs from current states. ( Hint: Use Implication Operators) Solution :

Same Cycle Implication ( |->) : Only under certain conditions assertions may be valid. exp1 |-> exp2 ; If exp1 is true then exp2 must be true at the same evaluation point. Example : property SameCyImp @(negedge CLK) (REQ && ~ACK) |-> BUSY ; endproperty assert property (SameCyImp); Next Cycle Implication ( |=>) : exp1 |=> exp2; If exp1 is true , then exp2 must be true at the next evaluation point. Example : property NextCyImp @(negedge CLK) (REQ && ~ACK) |=> BUSY; endproperty assert property (NextCyImp); Hope, this blog is helpful to understand the use case of Same Cycle and Next Cycle Implication Operators clearly. Please feel free to like/share/comment and follow VLSI Excellence for m...

Clocked Property Evaluation : Remember - "Objects are sampled before the Clock Edge" Lets have a look at below examples - 1) property EN_1HOT @(EN1 or EN2) (EN1 | EN2) endproperty 2) property EN_1HOT_CLK @(psoedge CLK) (EN1 | EN2) endproperty Now, Lets have a look at the signal waveform below - Important Points: 1) EN_1HOT Property is evaluated whenever there is a change in EN1 or EN2 Signal ( As shown in above waveform) 2) EN_1HOT_CLK Property is evaluated at every Positive Edge of the Clock ( As shown in above waveform) 3) As you observe in the above waveform when a property evaluates, the property expression objects are evaluated before the property clocking expression ( See the point in the above waveform where EN_1HOT Fails ) Hope, this example gives an insight on how the assertion property evaluation takes place. Please like/share/comment and Follow "VLSI Excellence" for more such exciting and interesting Problems !!...

Counterintuitive Clock Behavior in Assertions: It is possible that the properties do not behave as intended. Example : Using the same signal in clocking expression and the property definition assert property (@(posedge clock) clock)) -------- > This assertion always FAILS !!! Explanation : Lest see the circuit diagram below -    If you want to verify the behavior of this circuit using the assertion below - assert property (@(posedge clock) clock)) ----- > This will always FAIL Lets see the waveform of above circuit - "LRM defines regions where the signals are sampled and where they are updated." So here ,At clocking expression @(posedge clock) , the property definition (Clock) is always evaluated to False and hence this assertion always FAILS !!! Note: Objects are sampled before Clock Edge !!! Please like/share/comm...

There are two kind of assertions in System Verilog : 1) Immediate Assertion (Assert) 2) Concurrent Assertion (Assert Property) 1) Immediate Assertion: These are procedural statements (Embedded within a procedural block) and only active within the block. These are similar to the 'if' statement. Example : always @ (negedge clock ) assert !(wr_en && rd_en) ------- > Immediate Assertion Note: wr_en and rd_en should never be 1 together, if so , assertion will results in failure Equivalent Verilog Code for the above mentioned assertion : always @ (negedge clock ) if(wr_en && rd_en) $displey ("Error !!!"); You can code the above assertion in different ways like below - a) assert !(wr_en && rd_en) $display ("All Good ") ; ...

Assertion: What : A check embedded in the code !!! Embedded in functional code, ignored by synthesis !!! Why : 1) To check if - a) A specific condition occurs during the simulation or b) A specific sequence of events occurs 2) Significantly enhance productivity of designers by finding bugs earlier in the design and more easily 3) Assertions monitors and reports - a) Expected design behavior b) Protocols correctness c) Forbidden behavior 4) Reduce debug time by identifying incorrect design behavior when and where it occurs 5) Helps designers to better understand their design Who : Who writes assertions - -----------------------------------------------------Happy Learning--------------------------------------