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

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

  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

 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

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

  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

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

Copyright © 1998-2014

Deepak Kumar Tala - All rights reserved

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