Assertion#

Assertions are primarily used to validate the behavior of a design. An assertion is a check embedded in design or bound to a design unit during the simulation. Warnings or errors are generated on the failure of a specific condition or sequence of events.
“The values of variables used in assertions are sampled in the Preponed region of a time slot, and the assertions are evaluated during the Observed region.”

Advantages of using Assertions

• Checks design specifications and reports errors or warnings in case of failure.
• It improves debugging time. For example, a bug due to an illegal state transition can propagate to the output.
• Can be used in formal verification.

There are two kinds of assertions:

• Immediate Assertions
• Concurrent Assertions

Immediate Assertion#

The immediate assertion statement is a test of an expression performed when the statement is executed in the procedural code. If the expression evaluates to X, Z or 0, then it is interpreted as being false and the assertion is said to fail. Otherwise, the expression is interpreted as being true and the assertion is said to pass.

Syntax:

label: assert(expression) action_block;

Example:

condition1:assert (A==0 && B==0) $display(" %0t, A=0 and B=0, assertion failed" ,$time);

• The action_block is executed immediately after the evaluation of the assert expression.
• The action_block specifies what actions are taken upon success or failure of the assertion.

action_block

• The pass statement is executed if the expression evaluates to true.

• The statement associated with else is called a fail statement and is executed if the expression evaluates to false.

• Both pass and fail statements are optional.

• Since the assertion is a statement that something must be true, the failure of an assertion shall have a severity associated with it. By default, the severity of an assertion failure is an error.

• Other severity levels can be specified by including one of the following severity system tasks in the fail statement:

1. $fatal - It generates a run-time fatal assertion error, which terminates the simulation with an error code.

2. $error - It is a simple SystemVerilog construct that emits an error severity message.

3. $warning - It is a run-time warning, which can be suppressed in a tool-specific manner.

4. $info - It indicates that the assertion failure carries no specific severity.

• If an assertion fails and no else clause is specified, the tool shall, by default call $error.

Below are the different forms of immediate assertion syntax with and without optional items

1. With Pass and Fail statement; Fail verbosity info

       assert(expression)   
       $display(“expression evaluates to true”); 
       else   
       $info(“expression evaluates to false”);  

2. Only With Pass statement

       assert(expression)  
       $display(“expression evaluates to true”); 

3. With Pass and Fail statement; Fail verbosity fatal

       assert(expression) $display(“expression evaluates to true”);  
       else 
       $fatal(“expression evaluates to false”);  

4. Only With Fail statement; Multiple statements in Faile condition and Fail verbosity fatal

       assert(expression)  
       else begin  
        …….  
        …….  
       $fatal(“expression evaluates to false”);  
       end 

5. Only With Fail statement; Fail verbosity warning

       assert(expression)  
       else 
       $warning(“expression evaluates to false”);

6. With Label and Fail statement; Fail verbosity warning

       label: assert(expression)   
       else 
       $warning(“expression evaluates to false”);  

Example:

code snippet

       always @(posedge clk) 
       begin 
       assert (A==0 && B==0) $display("%0t, A=0 and B=0, assertion failed\n",$time);
  
       else assert (A==0 && B==1) $display("%0t, A=0 and B=1, assertion failed\n",$time);
  
       else assert (A==1 && B==0) $display("%0t, A=1 and B=0, assertion failed\n",$time);
  
       else assert (A==1 && B==1) $display("%0t, A=1 and B=1,assertion Success\n",$time);
  
       else $display("%0t fail\n",$time);
       end

Below figure shows the Output of Immediate assertion

Here there are four conditions, i.e 00,01,10,11 and the condition will be success when A and B both are high, so at that condition assertion is success and for other condition it is considered as failure.

Concurrent Assertion#

• An assertion that checks the sequence of events spread over multiple clock cycles is called a concurrent assertion.
• They execute in parallel with other always blocks concurrently, hence it is known as a concurrent assertion.
• Unlike immediate assertion, the concurrent assertion is evaluated only at clock tick. Thus, it is a clock-based evaluation model and an expression used in the concurrent assertion is always tied to a clock definition.
• The Keyword differentiates the immediate assertion from the concurrent assertion is “property.”

Following are the steps to create assertions:

SVA Building block#

Step 1: Create Boolean expressions
Step 2: Create sequence expressions
Step 3: Create property
Step 4: Assert property

1.Boolean expressions

The functionality is represented by the combination of multiple logical events. These events could be simple Boolean expressions.

2.Sequence

• In any design model, the functionality is represented by the combination of multiple logical events.
• These events could be simple Boolean expression that get evaluated on the same clock edge or could be events that evaluate over a period of time involving multiple clock cycles.
• Systemverilog asserion provides a key word to represent these events called “sequence”.
• The basic syntax of a sequence is given below,

Syntax

sequence name_of_sequence;  
<test expression> 
endsequence  

3.Property

• A number of sequences can be combined logically or sequentially to create more complex sequences.
• Systemverilog asserion provides a keyword to represent these complex sequential behaviors called “property”.

Syntax

property name_of_property;
  <test expression> or  
  <complex sequence expressions>
endproperty  

4.Assert

The property is the one that is verified during a simulation. It has to be asserted to take effect during a simulation. SVA provides a keyword called “assert” to check the property.

Syntax

assertion_ name: assert property( property_name );

Example:

code snippet

       sequence seq;
       @(posedge clk) (A==1 && B==1);
       endsequence

       property ppt;
       seq;
       endproperty

       assert property (ppt) 
       $display(" %0t, A=1 and B=1, assertion success",$time);
       else 
       $display("%0t, A=%0b and B=%0b,assertion failure", $time,A,B);

Below figure shows the Output of Concurrent assertion

Here there are four conditions, i.e 00,01,10,11 and the condition will be success when A and B both are high, so at that condition, assertion is success and for other condition it is considered as failure.

SVA(System Verilog Assertion) Sequence#

The expressions expand over more than one clock cycle is called a sequence. Sequences are build over SystemVerilog boolean expressions. If an expression checks properly, then the sequence is to be matched. The expressions evaluate over a period of time that may involve one or more clock cycles.

A property may involve checking of one or more sequential behaviours beginning at various times. An attempted evaluation of a sequence is a search for a match of the sequence beginning at a particular clock tick. To determine whether such a match exists, appropriate Boolean expressions are evaluated beginning at the particular clock tick and continuing at each successive clock tick until either a match is found or it is deduced that no match can exist.

Syntax

     sequence <sequence_name>;
     <test expression>;  
     endsequence     

1.The sequence with timing relationship
2.The sequence with a logical expression
3.Multiple sequences
4.The sequence with Formal Argument

1.The Sequence with Timing Relationship#

In SVA, clock cycle delays are represented by x “##” sign. For example, ##5 means 5 clock cycles.

Syntax:

      sequence seq_name;
      variable_1  ##<delay_value>  variable_2 ;
      endsequence  

code snippet:

      sequence seqA;
      x ##5 y ;
      endsequence  

      property prop;
      @(posedge clk) seqA;
      endproperty  

     time_a1:assert property(prop)  $info("assertion passed");  else $error("assertion failed");

Below sequence checks for the signal “x” being high on a given positive edge of the clock. If signal “x” is high on any given positive edge of the clock and signal “y” should be high after 5 clock cycles . The assertion passed , otherwise assertion fails.

2.The sequence with a logical expression#

Syntax:

      sequence seq_name;
      variable_1 <logical_operator> variable_2;
      endsequence  

code Snippet:

      sequence seqB;
      x && y;
      endsequence  

      property prop;
      @(posedge clk) seqB;
      endproperty  
  
      time_a1:assert property(prop)  $info("assertion passed");  else $error("assertion failed");

The above sequence, seqB checks that on every positive edge of the clock, both signals “X” and “Y” are high, then assertion will pass. If one of the signals are low, the assertion will fail.

3.Multiple sequences#

Multiple sequences are evaluating and checking two or more sequences using operators, delay, clock etc…
Here, two sequences ‘seqA’ and ‘seqB’ are shown below:

code snippet:

      sequence seqA;
      x ##5 y ;
      endsequence  

 
      sequence seqB;
      x && y;
      endsequence  

      property prop;
      @(posedge clk) seqA |-> seqB;
      endproperty     

      time_a1:assert property(prop)  $info("assertion passed");  else $error("assertion failed");

• In seqA, x ##5 y shows the timimg relationship between ‘x’ and ‘y’ having five clock ticks.
• In seqB, x && y shows logical relationship between ‘x’ and ‘y’ having logical AND operator.
• Inside property(prop), we use overlapped implication operator (|->) to evaluate the two sequences.
• In seqA, if x is high, then after 5 clock ticks , the y will be evaluated and it should be high.
• In seqB, if x and y are both high ,then the seqB is evaluated .
• Inside the property ‘seqA |-> seqB ’ which indicates if seqA is true, the seqB will be evaluated at the same cycle using overlapped implication operator .If it is true, the assertion will be passed otherwise it fails.

output

The figure below shows that the output of sequence in assertions.

Waveform

Explanation

In concurrent assertions, the assertions are evaluated only at the clock posedge. And effect of input conditions only reflect at the next posedge. The output shows that in seqA, x=1 at 30ns and after 5 clock cycles, y=1 at 50ns.In seqB, both x and y are high after 50ns. The assertions will be passed after 50ns to 62ns.

4.The sequence with Formal Argument#

Sequences can have formal arguments in order to make sequences reusable. Formal argument can be represented by two types:

1. Typed ( With Datatypes)
2. Untyped (Without datatypes)

Code Snippet:

       sequence notype_seq (X,Y);
         X && Y;
       endsequence

       sequence withtype_seq (bit X, bit Y);
         X && Y;
       endsequence

       property a_b_notype_prop(a,b);
         @ (posedge clk) a |-> notype_seq(a,b);
       endproperty

       property c_d_type_prop(bit c, bit d);
         @ (posedge clk) c |-> withtype_seq(c,d);
       endproperty

       a_b_notype_assert : assert property (a_b_notype_prop(a,b))
                           $info("assertion passed");
                           else
                             $error("assertion failed");
       c_d_type_assert   : assert property (c_d_type_prop(c,d))
                           $info("assertion passed");
                           else
                             $error("assertion failed");  

Explanation

The formal argument in SV Assertions example is shown above. In sequence_1 with using untyped formal argument, they were declared variables without data types. In sequence_2, using typed formal argument includes variables with datatypes eg:(bit X, bit Y).Using overlapping implication operator, two property blocks works under initial condition. Using assert property the input conditions were evaluated.
In the assertion_1 and assertion_2 if both argument is 1 then assertion is pass otherwise fail because in the both sequence we perform And operation.
In the a_b_notype_property if a=1 and in the c_d_type_property if c=1 then check notype sequence and withtype sequence.

Output

Waveform

Explanation

At 25ns a=1 so it will check notype_seq and there a=1 and b=0 so at 25ns a_b_notype_assert is failed and c=0 so it will not check withtype_seq.
At 35ns a=1 so it will check notype_seq and there a=1 and b=1 so at 35ns a_b_notype_assert is passed and c=1 so it will check nontype_seq and there c=1 and d=1 so at 35ns c_d_type_assert is passed
At 45ns a=1 so it will check notype_seq and there a=1 and b=0 so at 45ns a_b_notype_assert is failed and c=1 so it will check nontype_seq and there c=1 and d=1 so at 45ns c_d_type_assert is passed
At 55ns a=1 so it will check notype_seq and there a=1 and b=1 so at 55ns a_b_notype_assert is passed and c=1 so it will check nontype_seq and there c=1 and d=0 so at 55ns c_d_type_assert is failed

Variable Delay in sequence#

• static delay

The static delay means that using ’ ## ’ operator inside the the sequence. It is same as the sequence with timing relationship.

Syntax:

variable_1  ## delay_value  variable_2;  

Example:

a ##5 b;    

• Variable delay

The variable delay works as loops. It is the main advantage over static delay.

     parameter_delay = 2;
    
     sequence delay_sequence(variable_delay);
     int delay;
     (1,delay=variable_delay) ##0 first_match((1,delay=delay-1) [*0:$] ##0 delay <=0);
     endsequence
     
     a_1: assert property(@(posedge clk) a |-> delay_sequence(parameter_delay) |-> b)
     $info("assertion passed"); else $error("assertion failed");

Explanation

• The above program shows the example of variable delay in assertions. Inside the program we assign parameter delay as ‘2’. This parameter_delay is copied to variable_delay, the variable value will be decremented on each clk cycle and checks for the value of ‘delay’ equals to ‘0’ . The sequence delay_sequence has a variable parameter_delay which is passed from the property. That is actually assigned to variable_delay, which is in turn assigned to the local variable delay.

• ‘*0’ is called an empty match. For example a[*0:$] |-> b means a [*0] or a [*1] or a [*2] .. a [$]

• To avoid unexpected behaviours because of multiple matches or cause an assertion to never succeed because all threads of antecedent must be tested for property to succeed. The ‘first_match’ operator matches only the first of possibly multiple matches for an evaluation attempt and causes all the subsequent matches to be discarded.

Output

Waveform

parameter delay -2

Explanation

The output shows that, inside the program we assign parameter delay as ‘2’. First we take a = 1 at 5ns,after 2 clock cycles at 15ns b is not high. So the assertion is failed. Between 15ns to 25ns, a and b are same and assertion will not taken because ‘first match’ avoids duplication. Between 25ns to 35ns,the effect of input a and b is high, so it will pass the assertion. In addition to, between 45ns to 55ns the assertion is passed.

Implication Operator#

• If we want the sequence to be checked only after “a” is high, this can be achieved by using the implication operator. The implication is equivalent to an if-then structure.

• The left-hand side of the implication is called the “antecedent” and the right-hand side is called the “consequent.”

• It can be used only with property definitions not used with sequences.

• There are two types of implication operators:

1. Overlapped implication (|->)
2. Non-overlapped implication (|=>)

1.Overlapped Implication#

• It is denoted by |->.
• If there is a match on the antecedent, then the consequent expression is evaluated in the same clock cycle.

Syntax:-

<Antecedent> |-> <Consequent>

Example:-

    property p;
       @(posedge clk) a |-> b;
    endproperty  
    a: assert property(p);  

In the above example when “a” is high on the positive edge of clock cycle then “b” will be evaluated and based on that assertion will be passed or fail.

Code snippet:

      module overlapped_assertion;
      bit clk,a,b,valid;
  
      always #5 clk = ~clk; //clock generation
  
      //generating 'a'
      initial begin
        valid=1; a=1; b=1;
       #15 a=1; b=0;
       #10 b=1;
       #12 b=0;
       #10 a=0; b=1;
        valid=0;
       #15 a=1; b=0;
       #100 $finish;
      end
     
      // property definition
      property p;
        @(posedge clk) valid |-> (a ##3 b);
      endproperty
 
     //calling assert property
       a_1: assert property(p)
         $info("pass");
         else
          $info("fail");
 
     endmodule

Output:

The below figure will shows the overlapped implication output. here, at 5ns first posedge comes and at that point valid and a both are high so it will check for b after 3 clock cycles at 35ns b is high so assertion passed if b is not high at that point then assertion is fail and this same process will be followed for other posedges till $finish is called.

Output Waveform:

Overlapped Implication Types:#

The implication with a fixed delay on the consequent#

• Below property checks that, if signal “a” is high on a given positive clock edge, then signal “b” should be high after 2 clock cycles.
• Fixed delay can be denoted as ##n here n will specify the time.

Syntax:-

<Antecedent> |-> ##<value> <Consequent> 

Example:-

property p;  
@(posedge clk) a |-> ##2 b;  
endproperty 
a: assert property(p);

The implication with a sequence as an antecedent#

• Below property checks that, if the sequence seq_1 is true on a given positive edge of the clock, then start checking the seq_2 (“d” should be low, 2 clock cycles after seq_1 is true).

Syntax:-

<Sequence1> |-> <Sequence2>

Example:-

sequence seq_1;  
(a && b) ##1 c; 
endsequence 

sequence seq_2; 
##2 !d;  
endsequence

property p; 
@(posedge clk) seq_1 |-> seq_2; 
endpeoperty
a: assert property(p);

Timing windows in SVA Checkers#

• Below property checks that, if signal “a” is high on a given positive clock edge, then within 1 to 3 clock cycles, the signal “b” should be high.

Syntax

<Antecedent> |-> ##[1:<value>] <Consequent>

Example:-

property p;
@(posedge clk)
a |-> ##[1:3] b; 
endproperty 
a: assert property(p); 

Overlapping timing window#

• Below property checks that, if signal “a” is high on a given positive clock edge, then signal “b” should be high in the same clock cycle or within 4 clock cycles.

Syntax:-

<Antecedent> |-> ##[0:<value>] <Consequent>

Example:-

property p;
@(posedge clk)
a |-> ##[0:3] b;
endproperty
a: assert property(p);

Indefinite timing window#

• The upper limit of the timing window specified in the right-hand side can be defined with a “$” sign which implies that there is no upper bound for timing. This is called the “eventuality” operator. The checker will keep checking for a match until the end of the simulation.
• Below property checks that, if signal “a” is high on a given positive clock edge, then signal “b” will be high eventually starting from the next clock cycle.

Syntax:-

<Antecedent> |-> ##[1:$] <Consequent>

Example:-

property p;
@(posedge clk)
a |-> ##[1:$] b;
endproperty
a: assert property(p);

2.Non-overlapped Implication:#

• The non-overlapped implication is denoted by the symbol |=>.
• If there is a match on the antecedent, then the consequent expression is evaluated in the next clock cycle.

Syntax:-

<Antecedent> |=> <Consequent>

Example :-

property p;
@(posedge clk) a |=>b;
endproperty
a: assert property( p );  

In the above example if signal “a” is high on a given positive clock edge, then signal “b” should be high on the next clock edge.

Code snippet:

      module nonoverlapped_assertion;
      bit clk,a,b,valid;
  
      always #5 clk = ~clk; //clock generation
  
      //generating 'a'
      initial begin
        valid=1; a=1; b=1;
       #15 a=1; b=0;
       #10 b=1;
       #12 b=0;
       #10 a=0; b=1;
        valid=0;
       #15 a=1; b=0;
       #100 $finish;
      end
     
      // property definition
      property p;
        @(posedge clk) valid |=> (a ##3 b);
      endproperty
 
     //calling assert property
       a_1: assert property(p)
         $info("pass");
         else
          $info("fail");
 
     endmodule

Output:

The below figure will shows the nonoverlapped implication output. here, at 5ns first posedge comes and at that point valid is high after one clock cycle at 15ns a is high so it will check for b after 3 clock cycles at 45ns b is low so assertion failed if b is high at that point assertion is pass and this same process will be followed for other posedges till $finish is called.

Output Waveform:

Repetition Operators:#

Consecutive repetition#

property p;
@(posedge clk) a |-> ##1 b ##1 b ##1 b;
endproperty 
a: assert property(p);

The above property checks that, if the signal “a” is high on given posedge of the clock, the signal “b” should be high for 3 consecutive clock cycles.

The Consecutive repetition operator is used to specify that a signal or a sequence will match continuously for the number of clocks specified.

Syntax:

signal [*n] or sequence [*n]

“n” is the number of repetitions.

with repetition operator above sequence can be re-written as,

property p;  
@(posedge clk) a |-> ##1 b[*3] ##1 c;  
endproperty 

a: assert property(p);

Example:

    module consecutive_repetition;     
      bit clk,a,b;   
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin  
       a=0; b=0;  
       #15 a=1; b=0;  //15  
       #10 a=0; b=1;  //25  
       #10 a=0; b=1;  //35  
       #10 a=0; b=1;  //45  
       #10 a=1; b=1;  //55  
       #10 a=0; b=1;  //65  
       #10 a=0; b=1;  //75  
       #10 a=0; b=0;  //85  
       #10 a=1; b=0;  //95  
       #10 a=0; b=0;  //105  
       #10 a=1; b=1;  //115  
       #10 a=0; b=1;  //125  
       #10 a=0; b=1;  //135  
       #10 a=0; b=0;  //145  
       #10 a=0; b=0;  //155  
       #10;  
       $finish;  
     end  
   
     //property definition  
     property p;  
       @(posedge clk) a |-> ##1 b[*3];  
     endproperty  

     //calling assert property  
     a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
   
    endmodule   

Output:

In below figure,At 25ns a=1, and after 1 clock-cycle(##1) b =1 for 3 consecutive clock cycle.Hence, $info displayed as pass at 55ns. At 65ns a=1, but after 1 clock-cycle b=1 for only 2 cosecutive times. Hence $info displayed fail at 95ns. At 105ns a=1, but b=0 after 1 clock-cycle.Hence $info displayed pass at 115ns.

Waveform Output:

go to repetition#

The go-to repetition operator is used to specify that a signal will match the number of times specified not necessarily on continuous clock cycles.

Syntax:

signal [->n]    

property p;  
  @(posedge clk) a |-> ##1 b[->3] ##1 c;  
endproperty 

a: assert property(p);

The above property checks that, if the signal “a” is high on given posedge of the clock, the signal “b” should be high for 3 clock cycles followed by “c” should be high after ”b” is high for the third time.

Example:

    module goto_repetition;  
     bit clk,a,b,c;   
 
     always #5 clk = ~clk; //clock generation  
   
     initial begin  
       a=0; b=0;  
       #15 a=1; b=0; c=0; //15  
       #10 a=0; b=1; c=0; //25  
       #10 a=0; b=1; c=0; //35  
       #10 a=0; b=0; c=0; //45  
       #10 a=0; b=1; c=0; //55  
       #10 a=0; b=0; c=0; //65  
       #10 a=0; b=0; c=0; //75  
       #10 a=1; b=0; c=0; //85  
       #10 a=0; b=1; c=0; //95  
       #10 a=0; b=0; c=0; //105  
       #10 a=0; b=1; c=0; //115  
       #10 a=0; b=0; c=0; //125  
       #10 a=0; b=1; c=0; //135  
       #10 a=0; b=0; c=1; //145  
       #10 a=0; b=0; c=0; //155  
       #10;  
       $finish;  
     end  
 
     //property definition  
     property p;  
       @(posedge clk) a |-> b[->3] ##1 c;  
     endproperty  
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  

     endmodule  

Output:

In below figure, at 25ns a=1, b can be 1 on any clock-cycle for 3 times, not necesserily on consecutive clock-cycle and c=1 after 1 clock-cycle follwed by b, but c=0 at 75ns. Hence, $info displayed fail at 75ns. At 95ns a=1, and b=1 for 3 times then c=1 after 1 clock-cycle(##1) i.e at 155ns. Hence, $info displayed pass at 155ns.

Waveform Output:

Nonconsecutive repetition#

This is very similar to “go to” repetition except that it does not require that the last match on the signal repetition happens in the clock cycle before the end of the entire sequence matching.

Syntax:

signal [=n] 

Only expressions are allowed to repeat in “go to” and “nonconsecutive” repetitions. Sequences are not allowed.

Example:

    module nonconsecutive_repetition;  
     bit clk,a,b,c;   
 
     always #5 clk = ~clk; //clock generation  
   
     initial begin  
       a=0; b=0;  
       #15 a=1; b=0; c=0; //15  
       #10 a=0; b=1; c=0; //25  
       #10 a=0; b=1; c=0; //35  
       #10 a=0; b=0; c=0; //45  
       #10 a=0; b=1; c=0; //55  
       #10 a=0; b=0; c=0; //65  
       #10 a=0; b=0; c=1; //75  
       #10 a=0; b=0; c=0; //85  
       #10 a=1; b=1; c=0; //95  
       #10 a=0; b=0; c=0; //105  
       #10 a=0; b=1; c=0; //115  
       #10 a=0; b=0; c=0; //125  
       #10 a=0; b=1; c=0; //135  
       #10 a=0; b=0; c=1; //145  
       #10 a=0; b=0; c=0; //155  
       #10;  
       $finish;  
     end  
 
     //property definition  
     property p;  
       @(posedge clk) a |-> b[=3] ##1 c;  
     endproperty  
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  

     endmodule  

Output:

In below figure, at 25ns a=1, b=1 for 3rd time at 65ns(not necessarily on consecutive clock-cycle) and c can be 1 at any clock-cycle after 1 clock-cycle(##1) delay.Hence, $info displayed Pass at 85ns. At 105ns a=1 and b=1 for 3rd time at 145ns and c=1 at 155ns.Hence $info displayed Pass at 155ns.

Waveform Output:

SVA Methods#

$rose#

Syntax:

$rose(boolean expression or signal name)

returns true if the least significant bit of the expression changed to 1. Otherwise, it returns false.

property p;    
@(posedge clk) $rose(a)  
endproperty   

property p checks that the signal “a” transitions to a value of 1 on every positive edge of the clock. If the transition does not occur, the assertion will fail.

Example:

    module rose;  
     bit clk,a,b;    
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin  
       a=0; b=0;  
       #15 a=1; b=0;  //15  
       #10 a=0; b=0;  //25  
       #10 a=1; b=1;  //35  
       #10 a=0; b=0;  //45  
       #10 a=1; b=1;  //55  
       #10 a=0; b=0;  //65  
       #10 a=1; b=1;  //75  
       #10 a=1; b=1;  //85  
       #10 a=1; b=0;  //95  
       #10 a=0; b=0;  //105  
       #10 a=1; b=0;  //115  
       #10 a=0; b=0;  //125  
       #10 a=1; b=0;  //135  
       #10 a=1; b=0;  //145  
       #10;  
       $finish;  
     end  
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $rose(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule  

Output:

In below figure, a=1 at 25ns but b=0 as it was before.Hence, $info displayed Fail at 25ns. At 45ns a=1 and b transitioned to 1 (previously b=0 at 35ns, it will check previous cycle). Hence, $info displayed Pass at 45ns. At 65ns a=1 and b transitioned to 1 (previously b=0 at 55ns). Hence, $info displayed Pass at 65ns. At 95ns a=1 but b stable 1 its not transitioned. Hence, $info displayed failed at 95ns.

Waveform Output:

$fell#

Syntax:

$fell(boolean expression or signal name)

returns true if the least significant bit of the expression changed to 0. Otherwise, it returns false.

property p;
  @(posedge clk) $fell(a);  
endproperty 

property p checks that the signal “a” transitions to a value of 0 on every positive edge of the clock. If the transition does not occur, the assertion will fail.

Example:

    module fell;  
     bit clk,a,b;   
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=0;
       #15 a=1; b=0;  //15
       #10 a=0; b=1;  //25
       #10 a=1; b=0;  //35
       #10 a=0; b=0;  //45
       #10 a=1; b=1;  //55
       #10 a=0; b=0;  //65
       #10 a=1; b=1;  //75
       #10 a=1; b=0;  //85
       #10 a=1; b=0;  //95
       #10 a=0; b=0;  //105
       #10 a=1; b=0;  //115
       #10 a=0; b=0;  //125
       #10 a=1; b=0;  //135
       #10 a=1; b=0;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $fell(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule  

Output:

In below figure, a=1 at 25ns but b=0 its stable(check previous cycle at 15ns b=0) it is not transitioned.Hence $info displayed as Fail at 25ns. At 45ns a=1 and b transitioned from 1 to 0 (previously b=1 at 35ns).Hence, $info displayed as Pass at 45ns.

Waveform Output:

$stable#

Syntax:

$stable(boolean expression or signal name) 

returns true if the value of the expression did not change. Otherwise, it returns false.

property p;    
  @(posedge clk) $stable(a);   
endproperty     

property p checks that the signal “a” is stable on every positive edge of the clock. If there is any transition occurs, the assertion will fail

Example:

    module stable;  
     bit clk,a,b;    
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=0;
       #15 a=1; b=0;  //15
       #10 a=0; b=0;  //25
       #10 a=1; b=1;  //35
       #10 a=0; b=0;  //45
       #10 a=1; b=1;  //55
       #10 a=0; b=0;  //65
       #10 a=1; b=1;  //75
       #10 a=1; b=1;  //85
       #10 a=1; b=0;  //95
       #10 a=0; b=0;  //105
       #10 a=1; b=0;  //115
       #10 a=0; b=1;  //125
       #10 a=1; b=0;  //135
       #10 a=1; b=0;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $stable(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule  

Output:

In below figure, a=1 at 25ns and b=0 as it was in previous cycle, it is stable.Hence, $info displayed Pass at 25ns. At 45ns a=1 but b transitioned from 0 to 1.Hence, $info displayed as Fail at 45ns.

Waveform Output:

$past#

Syntax:

$past(signal_name, number of clock cycles)

provides the value of the signal from the previous clock cycle.

Below Property checks that, in the given positive clock edge, if the “b” is high, then 2 cycles before that, a was high.

property p;   
  @(posedge clk) b |-> ($past(a,2) == 1);  
endproperty 
a: assert property(p);    

Example:

    module past;  
     bit clk,a,b;  
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=0;
       #15 a=1; b=1;  //15
       #10 a=0; b=0;  //25
       #10 a=1; b=1;  //35
       #10 a=0; b=0;  //45
       #10 a=1; b=1;  //55
       #10 a=0; b=0;  //65
       #10 a=1; b=1;  //75
       #10 a=1; b=1;  //85
       #10 a=1; b=0;  //95
       #10 a=0; b=0;  //105
       #10 a=1; b=0;  //115
       #10 a=0; b=0;  //125
       #10 a=1; b=0;  //135
       #10 a=1; b=0;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> ($past(b,2) == 1);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule  

Output:

In below figure, a=1 at 25ns,but b was not 1 in 2 clock-cycles before that. Hence, $info displayed as Fail at 25ns. At 45ns a=1 and 2 clock-cycles before that b=1 i.e at 25ns. Hence, $info displayed Pass at 45.

Waveform Output:

Built-in system functions#

$onehot(expression)#

• checks that only one bit of the expression can be high on any given clock edge.

Syntax:

a_1: assert property( @(posedge clk) $onehot(state) );

Assert statement a_1 checks that the bit vector “state” is one-hot.

Example:

    module onehot;  
     bit clk,a;  
     logic [4:0] b;  
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=5'b00000;
       #15 a=1; b=5'b00100;  //15
       #10 a=0; b=5'b01000;  //25
       #10 a=1; b=5'b01000;  //35
       #10 a=0; b=5'b01000;  //45
       #10 a=1; b=5'b10000;  //55
       #10 a=0; b=5'b10000;  //65
       #10 a=1; b=5'b11000;  //75
       #10 a=0; b=5'b01100;  //85
       #10 a=1; b=5'b01100;  //95
       #10 a=0; b=5'b01000;  //105
       #10 a=1; b=5'b11100;  //115
       #10 a=0; b=5'b01000;  //125
       #10 a=1; b=5'b00000;  //135
       #10 a=1; b=5'b00100;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $onehot(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule  

Output:

In below figure, a=1 at 25ns and only one bit of b is high(i.e b=00100). Hence, $info displayed Pass at 25ns. At 85ns a=1 but two bits of b are high(i.e b=11000). Hence, $info displayed as Fail at 85ns.

Waveform Output:

$onehot0(expression)#

• checks only one bit of the expression can be high or none of the bits can be high on any given clock edge.

Syntax:

a_1: assert property( @(posedge clk) $onehot0(state) );

Assert statement a_1 checks that the bit vector “state” is zero one-hot.

Example:

    module onehot0;  
     bit clk,a;  
     logic [4:0] b;  
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=5'b00000;
       #15 a=1; b=5'b00100;  //15
       #10 a=0; b=5'b01000;  //25
       #10 a=1; b=5'b01000;  //35
       #10 a=0; b=5'b01000;  //45
       #10 a=1; b=5'b10000;  //55
       #10 a=0; b=5'b10000;  //65
       #10 a=1; b=5'b11000;  //75
       #10 a=0; b=5'b01100;  //85
       #10 a=1; b=5'b01100;  //95
       #10 a=0; b=5'b01000;  //105
       #10 a=1; b=5'b11100;  //115
       #10 a=0; b=5'b01000;  //125
       #10 a=1; b=5'b00000;  //135
       #10 a=1; b=5'b00100;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $onehot0(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule  

Output:

In below figure, a=1 at 25ns and only one bit of b is high (which is allowed in $onehot0). Hence, $info displayed Pass at 25ns. At 85ns a=1 but two bits of b are high, i.e b=11000 (which is not allowed in $onehot0). Hnece, $info displayed as Fail at 85ns.

Waveform Output:

$isunknown(expression)#

• checks if any bit of the expression is X or Z.

Syntax:

a_1: assert property( @(posedge clk) $isunknown(bus) ) ;

Assert statement a_1 checks if any bit of the vector “bus” is X or Z.

Example:

    module isunknown;  
     bit clk,a;  
     logic [4:0] b;  
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=5'b00000;
       #15 a=1; b=5'b001x0;  //15
       #10 a=0; b=5'b01000;  //25
       #10 a=1; b=5'b010z0;  //35
       #10 a=0; b=5'b01000;  //45
       #10 a=1; b=5'b10xz0;  //55
       #10 a=0; b=5'b10000;  //65
       #10 a=1; b=5'bxxxxx;  //75
       #10 a=0; b=5'b01100;  //85
       #10 a=1; b=5'bzzzzz;  //95
       #10 a=0; b=5'b01000;  //105
       #10 a=1; b=5'b10100;  //115
       #10 a=0; b=5'b01000;  //125
       #10 a=1; b=5'b10000;  //135
       #10 a=1; b=5'b00100;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $isunknown(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule  

Output:

In below figure, a=1 at 25ns and one bit of b is unknown(i.e 1x0). Hence, $info displayed Pass at 25ns. At 125ns a=1 but none of the bits of b are unkown (i.e 10100). Hence, $info displayed Fail at 125ns.

Waveform Output:

$countones(expression)#

• counts the number of bits that are high in a vector.

Syntax:

a_1: assert property( @(posedge clk) $countones(bus)> 1 ); 

Assert statement a_1 checks that the number of ones in the vector “bus” is greater than one.

Example:

    module countones;  
     bit clk,a;  
     logic [4:0] b;  
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=5'b00000;
       #15 a=1; b=5'b001x0;  //15
       #10 a=0; b=5'b01000;  //25
       #10 a=1; b=5'b11011;  //35
       #10 a=0; b=5'b01000;  //45
       #10 a=1; b=5'b10xz0;  //55
       #10 a=0; b=5'b10000;  //65
       #10 a=1; b=5'bxxxxx;  //75
       #10 a=0; b=5'b01100;  //85
       #10 a=1; b=5'bzzzzz;  //95
       #10 a=0; b=5'b01000;  //105
       #10 a=1; b=5'b11110;  //115
       #10 a=0; b=5'b01000;  //125
       #10 a=1; b=5'b10000;  //135
       #10 a=1; b=5'b00100;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> ($countones(b) == 1);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule  

Output:

in below figure, a=1 at 25ns and only one of the bits of b is 1 (i.e 1x0). Hence, $info displayed pass at 25ns. At 125 a=1 and more then one bits of b is 1 (i.e 11110). Hence, $info displayed fail at 125ns.

Waveform Output:

Disable iff#

In some design conditions, we don’t want to proceed with the check if some condition is true. this can be achieved by using disable iff. Disable iff disables the property if the expression it is checking is active. This is normally used for reset checking and if reset is active, then property is disabled.
Below property(p) checks that, if reset is disable and the signal “a” & “b” is high on given posedge of the clock the property is asserted, During this entire sequence, if reset is detected high at any point, the checker will stop. property is deasserted.
Syntax:

property p; 
 @(posedge clk) 
  disable iff (condition); 
endproperty`  

Example:

    property p;  
    @(posedge clk)  
    disable iff (reset) (a&&b);  
    endproperty  

The above example we use reset as the checker. The disable iff is used only inside the property. if reset is deasserted i.e ‘0’ then the property is enabled, the assertion output is obtained. if reset is asserted then the property is disabled, then the assertion output is not obtained/displayed

code snippet

      //Design module
       module andgate(  
        input A,  
        input B,  
       output Y,  
       input clk,  
       input rst);  
      assign Y = A&&B;  
      endmodule:andgate  

Testbench Code:

     `//module AND_gate_tb;
       module AND_Gate;
         reg A;
         reg B;
         reg clk;
         wire Y;
         reg rst;

        //Design instantiation
        andgate inst(.A(A), .B(B), .Y(Y), .clk(clk), .rst(rst));

        always #5 clk = ~clk;
        initial
        begin
        rst <=1; //reset is asserted
        clk<=1;
        A<=0;
        B<=0;

        #10
       A<=0;
       B<=1;
 
 
       #12
       rst <=0;//reset is deasserted
       A<=1;
       B<=0;

       #10
        A<=1;
        B<=1;

       #30 $finish;
        end
      //-------------------------------------------------------
      // Disable iff is used to disable the property when the
      // reset is active. Assertion output is disable whether it
      // failure or pass.It is used when we don't want to check 
      // some conditions
      //-------------------------------------------------------
      property p;
      @(posedge clk) disable iff(rst)//disable if reset is assereted
      A&&B;
       endproperty

      assert property (p) $display("time=%0t,A=%0b and B=%0b, assertion success\n",$time,A,B);
      else $display("time=%0t, A=%0b and B=%0b,assertion failure\n", $time,A,B);
      initial
      begin
      $dumpfile("waveform.vcd");
      $dumpvars();
      end
      endmodule:AND_Gate

output:

In the below figure reset is a checker if rst=0, the property is enabled and gives the assertion output while at 40ns rst=1, the property is disabled and the assertion output is not checked. The disable iff is used when we do not want to check some output of assertion.

ended#

The keyword “ended” is attached to the sequence name, while using more than one sequence in the program, the ending point of the sequences can be used as a synchronization point

Below in the code snippet, Here in the code we used two sequences seq1 and seq2. The sequence one as the variable d, and sequence two as the variable ‘k’. The two sequences is declare in the property with the implication operator along with the 4 clock cycle delay. Now, by using ended “keyword” with the sequence.Example: seq1 -> ##4 seq2. The seq1 is antecedent and seq2 is consequent. if antecedent is executed i.e the seq1. Then only the consequent part is executed i.e is seq2. In code, the seq1 variable‘d’ is high at posedge of clk, then from the next posedge of clk the seq2 is evaluated then the assertion is passed if ‘k’ at the 4 clock cycle of delay.

code snippet

      `module assertion_ex;
       bit clk,d,k;

       always #5 clk = ~clk; //clock generation

      //generating 'a'
      initial
      begin
      d=1;
      #57  k=1;
      #10 d=0;
      #15 k=0;
      #10 d=1;
      #10 k=0;
      #10 d=1;
      #10 k=1;
      #200;
      $finish;
      end

      //sequence 1
      sequence seq_1;
      @(posedge clk)
       d;
      endsequence
  
     //sequence 2
     sequence seq_2;
      @(posedge clk)
      ##4 k;
      endsequence

     property p;
     @(posedge clk) seq_1.ended |-> ##4 seq_2.ended;
    endproperty

    a_1: assert property(p)$info("passed");
    else $info("failed");

      initial
      begin
      $dumpfile("waveform.vcd");
      $dumpvars();
      end
      endmodule:assertion_ex

output:
Here, at 5ns d=1, the seq1 is executed from next cycle seq2 execute, it will check for 4cycle cycle from the ending cycle of seq1. here seq2 check the value ‘k’ until 45ns, at 45ns the ‘k’ value is low, then the assertion is failed. At 25ns the seq1 as the variable ’d’ it value is ‘high’, then it will start executing seq2 from next cycle, the seq2 as the variable k, it will check whether the ‘k’ is high at 4 cycle. it is high in the 4clock cycle so at 65n, the assertion is passed.

output Waveform:

Without using ended keywordEx:seq1 |-> ##4 seq2 in this example, While without using ended. The below same code the assertion will pass after 125ns. The seq variable‘d’ is high at 45ns then the seq2 is evaluated after the 4 clock cycle delay due to ##4. The variable ‘k’ is then evaluated as the seq2 as the expression ##4 k; if ‘k’ value is high at 4 clock cycle then the assertion is passed. In this case it will take 9 clock cycle to pass assertion where by using the ended keyword the assertion Is passed for 5 clock cycle.

code snippet

      `module assertion_ex;
       bit clk,d,k;

       always #5 clk = ~clk; //clock generation

      //generating 'a'
      initial
      begin
      d=1;
      #57  k=1;
      #10 d=0;
      #15 k=0;
      #10 d=1;
      #10 k=0;
      #10 d=1;
      #10 k=1;
      #200;
      $finish;
      end

      //sequence 1
      sequence seq_1;
      @(posedge clk)
       d;
      endsequence
  
     //sequence 2
     sequence seq_2;
      @(posedge clk)
      ##4 k;
      endsequence

     property p;
     @(posedge clk) seq_1 |-> ##4 seq_2;
    endproperty

    a_1: assert property(p)$info("passed");
    else $info("failed");

      initial
      begin
      $dumpfile("waveform.vcd");
      $dumpvars();
      end
      endmodule:assertion_ex

output:
Here, at 45ns d=1, the seq1 as variable ’d’ it is high at 45ns, then seq1 is executed, then now seq2 will start execute the variable ‘k’ after the 4clock cycle, it will start to check the value of ‘k’,after the 4clock cycle of seq2, then seq2 variable ‘k’ is chck the value at 4th clcok cycle. if it is high it pass the assertion. Total it take 9 clock cycle to execute the seq2 value, at 125ns it will pass the assertion.

output waveform: