System Verilog Assertions - Nonconsecutive Repetition

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






property GOTO_REPET;

@(negedge CLK) A |-> B[->2] ##1 C;

endproperty

assert property (GOTO_REPET);


Note: Last occurrence of B must be followed immediately by C


Hope, this blog post is helpful in understanding the tiny difference between these two operators while coding System Verilog Assertions.


Please like/share/comment and follow VLSI Excellence for such more interesting blog posts.


Happy Learning !!!

Read More

System Verilog Assertions - Consecutive Repetition

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

- Example :

A ##1 B[*0:2] ##1C;

- Possible Sequences - (A##1 C), (A ##1B ##1 C), (A ##1 B ##1 B ##1 C)

- Lower bound can be infinity ($)

- No maximum number of repetition , sequence might never end

- Example :

A[*2:$] ##1 B

- Possible Sequences - (A ##1 A ##1 B) , (A ##1 A ##1 A ---)



--------------------------------------------------Happy Learning-----------------------------------------

Read More

System Verilog Assertions - How it Works !!!

Here, is the flow diagram of how an assertion gets evaluated -


Syntax : @(Clocking) disable iff (EXPR) enabling_sequence |=> fulfilling_sequence

Read More

System Verilog Assertions - Sequences

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

- Example :

property ABORT;

@(negedge CLK) disable iff (RST)

A |=> B ##1 C ##1 D;

endproperty

assert property (ABORT);






--------------------------------------------------------Happy Learning----------------------------------

Read More

System Verilog Assertions - Example Problem

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









Solution:

Read More

System Verilog Assertions - Useful Built-in Functions

$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);

endproperty

assert property (1HOT_CHK);

$isunknown() :

- Returns a Boolean True if any bit in expr is 'x' or 'z'

- Syntax : $isunknown(expr)

- Example :

property CHK_UNKNOWN;

@(negedge CLK) (~EN |=> $isunknown(B_VECTOR));

endproperty

assert property (CHK_UNKNOWN);

- When EN is low, check that any bits of B_VECTOR is driven as 'x' OR 'z'

$onehot() :

- Returns a Boolean True only if exactly one bit in expr is 1

- Syntax : $onehot(expr)

- Example :

property ONEHOT;

@(negedge CLK) ($onehot(B_VECTOR));

end property

assert property (ONEHOT);

$onehot0() :

- Returns a Boolean True only if, at most, 1 bit in expr is 1

- Syntax : #onehot0(expr)

- Example :

property ONEHOT0;

@(negedge CLK) ($onehot0(B_VECTOR));

endproperty

assert property (ONEHOT0);





$rose() :

- Click Here

$fell() :

- Click Here


Hope, this blog post is helpful in understanding the useful System Verilog built-in functions.

Please do like/share/comment and follow VLSI Problems for such more interesting blog posts.

Happy Learning !!!

Read More

System Verilog Assertions - Assertion Overlapping

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->1 and z->1 changes

Example :

property ET;

@(negedge CLK) $rose(REQ) |=> ACK;

endproperty

assert property (ET);







Here, at second negedge of CLK , a new assertion is not getting triggered since there is no change in REQ.


Hope, this blog is helpful to understand assertion overlapping, their cons and how they can be avoided.


Please like/share/comment and follow VLSI Excellence for more such interesting blog posts.

Thanks !!!

-----------------------------------------------------Happy Learning -------------------------------------

Read More

System Verilog Assertions - Example Problem

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 :

Read More

System Verilog Assertions - Implication Operators

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 more such interesting blog posts.

Thanks !!!




-------------------------------------------------------------Happy Learning------------------------------

Read More

System Verilog Assertions - Clocked Property Evaluation

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 !!! Thanks.


------------------------------------------------------Happy Learning-------------------------------------

Read More

System Verilog Assertions - Counterintuitive Clock Behavior

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/comment and Follow 'VLSI Excellence' !!!

----------------------------------------------------- Happy Learning-------------------------------------

Read More

System Verilog Assertions - Simple Boolean Assertions

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 ") ;

else $display (" Error ");

b) You may only display the filing condition -

assert !(wr_rn && rd_en) else $display ("Error");

2) Concurrent Assertion: Concurrent assertions are used to specify functional property of design(A general behavior attribute used to characterize a design). They are not procedural codes and evaluated as a separate thread.

Examples of design behavior -

a) The read and write signal should never be asserted together

b) A request should be followed by an acknowledgement

1) assert property !(wr && rd)

2) assert property (@(posedge clock) Req |=> ACK )

Example: Signals wr_en and rd_en are never both high at the negedge of clock

rw_chk : assert property (@(negedge clock) !(wr_en && rd_en))

@(negedge clock) is the temporal condition for the clock expression. The design behavior is only checked on this condition

Important Notes:

1) Properties are often built using sequences

2) Concurrent assertions are checked throughout the simulation

3) Concurrent assertions usually appears outside any procedural blocks , interfaces and programs (Sometimes they may also be used as statements in initial or always block , A concurrent assertion inside initial block is only tested on first clock tick). Immediate assertions are defined within a procedural block (always or initial)

4) An immediate assertion describes a logic behavior at an instant of time while a concurrent assertion detects a behavior over a period of time


------------------------------------------------Happy Learning-------------------------------------------

Read More

System Verilog Assertions - What & Why & Who

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--------------------------------------

Read More