quick.gif

space2.gif

space2.gif

space2.gif

space2.gif

space2.gif

space2.gif

space2.gif

   

space.gif

   

space.gif

  ../images/main/bullet_star_pink.gif Binary Operators

Binary operators take two operands or two sequence and produce a new sequence. Following are binary sequences operators.

   

space.gif

  • 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 intersect operator is used.
  • or : When one of the both sequence are expected to match. Then or operator is used.
   

space.gif

  ../images/main/4blue_dots_bullets.gif Example : Binary Operators
   

space.gif


  1 //+++++++++++++++++++++++++++++++++++++++++++++++++
  2 //   DUT With assertions
  3 //+++++++++++++++++++++++++++++++++++++++++++++++++
  4 module binary_assertion();
  5 
  6 logic clk = 0;
  7 always  #1  clk ++;
  8 
  9 logic req,gnt,busy;
 10 //=================================================
 11 // Sequence Specification Layer
 12 //=================================================
 13 sequence s1;
 14  $past( ! req,1)  ##1  ($rose(gnt) and $past( ! gnt,1));
 15 endsequence
 16 
 17 sequence s2;
 18  $past( ! req,1)  ##1  $rose(gnt)  ##1  $fell(gnt);
 19 endsequence 
 20 
 21 sequence s3;
 22   req  ##1  gnt  ##1  busy  ##1  ( ! req and  ! gnt and  ! busy);
 23 endsequence
 24 
 25 sequence s4;
 26   req ##[1:3] gnt;
 27 endsequence
 28 //=================================================
 29 // Property Specification Layer
 30 //=================================================
 31 property and_prop;
 32   @ (posedge clk) 
 33     req |-> s1 and s2;
 34 endproperty
 35 
 36 property intersect_prop;
 37   @ (posedge clk) 
 38     req |-> s1 intersect s3;
 39 endproperty
 40 
 41 property or_prop;
 42   @ (posedge clk) 
 43     req |-> s1 or s4;
 44 endproperty
 45 //=================================================
 46 // Assertion Directive Layer
 47 //=================================================
 48 and_assert       : assert property (and_prop);
 49 intersect_assert : assert property (intersect_prop);
 50 or_assert        : assert property (or_prop);
 51 //=================================================
 52 // Generate input vectors
 53 //=================================================
 54 initial begin
 55   req <= 0;gnt <= 0;busy<=0;
 56   repeat(10) @ (posedge clk);
 57   req <= 1;
 58   @( posedge clk);
 59   gnt <= 1;
 60   req <= 0;
 61   @( posedge clk);
 62   busy <= 1;
 63   // Make the assertion fail now
 64   // OR will not fail
 65   req <= 0;gnt <= 0; busy <= 0;
 66   repeat(10) @ (posedge clk);
 67   req <= 1;
 68   repeat (2) @( posedge clk);
 69   req <= 0;
 70   gnt <= 1;
 71   @( posedge clk);
 72   @( posedge clk);
 73   req <= 0;gnt <= 0; busy <= 0;
 74   // Terminate the sim
 75    #30  $finish;
 76 end
 77 
 78 endmodule
You could download file binary_assertion.sv here
   

space.gif

   

space.gif

  ../images/main/4blue_dots_bullets.gif Simulation : Binary Operators
   

space.gif

 Error: Assertion error.
 Time: 23 ns Started: 21 ns  
  intersect_assert File: binary_assertion.sv Line: 46
 Error: Assertion error.
 Time: 47 ns Started: 47 ns  
 and_assert File: binary_assertion.sv Line: 45
 Error: Assertion error.
 Time: 47 ns Started: 45 ns  
 and_assert File: binary_assertion.sv Line: 45
 Error: Assertion error.
 Time: 47 ns Started: 47 ns  
 intersect_assert File: binary_assertion.sv Line: 46
 Error: Assertion error.
 Time: 47 ns Started: 45 ns  
 intersect_assert File: binary_assertion.sv Line: 46
   

space.gif

  ../images/main/bullet_star_pink.gif Match Operators

Match operators take two operands or two sequence and produce a new sequence. Following are match sequences operators.

   

space.gif

first_match

When we want to stop after first match of sequence, we use first_match match operator.

throughout

When we want to check if some condition is valid over period of sequence, then throughout match operator is used.

within

When we want to check containment of one sequence in another sequence, we use within match operator.

   

space.gif

  ../images/main/4blue_dots_bullets.gif Example : Match Operators
   

space.gif


  1 //+++++++++++++++++++++++++++++++++++++++++++++++++
  2 //   DUT With assertions
  3 //+++++++++++++++++++++++++++++++++++++++++++++++++
  4 module match_assertion();
  5 
  6 logic clk = 0;
  7 always  #1  clk ++;
  8 
  9 logic burst_enable, master_busy, slave_busy;
 10 //=================================================
 11 // Property Specification Layer
 12 //=================================================
 13 property first_match_prop;
 14   @ (posedge clk) 
 15     $rose(burst_enable) |=> 
 16       first_match(burst_enable ##[0:4]  ! master_busy);
 17 endproperty
 18        
 19 property throughout_prop;
 20   @ (posedge clk) 
 21     $rose(burst_enable) |-> 
 22       (burst_enable) throughout 
 23           (  ##2  ( ! slave_busy &&  ! master_busy) [*6]);
 24 endproperty
 25 
 26 property within_prop;
 27   @ (posedge clk) 
 28     $rose(burst_enable) |=> 
 29        ( ! slave_busy[*6]) within 
 30            (($fell(master_busy))  ##1   ! master_busy[*7]);
 31 endproperty
 32 //=================================================
 33 // Assertion Directive Layer
 34 //=================================================
 35 within_assert     : assert property (within_prop);
 36 throughout_assert : assert property (throughout_prop);
 37 first_match_assert: assert property (first_match_prop);
 38 //=================================================
 39 // Generate input vectors
 40 //=================================================
 41 initial begin
 42   burst_enable <= 0; master_busy <= 1; slave_busy <= 1;
 43   @ (posedge clk); 
 44   burst_enable <= 1;
 45   @ (posedge clk); 
 46   master_busy <= 0;
 47   @ (posedge clk); 
 48   slave_busy <= 0;
 49   repeat(6) @ (posedge clk);
 50   slave_busy <= 1;
 51   @ (posedge clk); 
 52   burst_enable <= 0;
 53   master_busy <= 1;
 54   // Fail both the assertion
 55   repeat(20) @ (posedge clk);
 56   burst_enable <= 0; master_busy <= 1; slave_busy <= 1;
 57   @ (posedge clk); 
 58   burst_enable <= 1;
 59   @ (posedge clk); 
 60   master_busy <= 0;
 61   @ (posedge clk); 
 62   slave_busy <= 0;
 63   repeat(5) @ (posedge clk);
 64   slave_busy <= 1;
 65   @ (posedge clk); 
 66   burst_enable <= 0;
 67   master_busy <= 1;
 68   // Terminate the sim
 69   repeat(20) @ (posedge clk);
 70   $finish;
 71 end
 72 
 73 endmodule
You could download file match_assertion.sv here
   

space.gif

  ../images/main/4blue_dots_bullets.gif Simulation : Match Operators
   

space.gif

 "match_assertion.sv", 26: within_assert: started at 63s failed at 77s
         Offending '(!slave_busy)'
 "match_assertion.sv", 27: throughout_assert: started at 63s failed at 77s
         Offending '((!slave_busy) && (!master_busy))'
   

space.gif

   

space.gif

   

space.gif

   

space.gif

space2.gif

space2.gif

space2.gif

space2.gif

space2.gif

  

Copyright © 1998-2014

Deepak Kumar Tala - All rights reserved

Do you have any Comment? mail me at:deepak@asic-world.com