quick.gif

space2.gif

space2.gif

space2.gif

space2.gif

space2.gif

space2.gif

space2.gif

   

space.gif

   

space.gif

  ../images/main/bullet_green_ball.gif Assertion with OVL

Now that we have seen the code of FIFO and the testbench, let's see the example of using OVL to build assertions for the FIFO. To use OVL, we need to first install the OVL package. Then we need to include the assertion file that we need to use. In our example we are using assert_fifo_index.vlib, we use synopsys translate_off to prevent the synthesis tools from reading the code within synopsys translate_off and synopsys translate_on. We want to do this, as this is simulation code not meant for synthesis. Next we need to enable assertions by `define OVL_ASSERT_ON. There are many other defines that we can use to control the OVL assertion; details of each option can be found in the OVL manual.

   

space.gif

   

space.gif

  ../images/main/bulllet_4dots_orange.gif Assertion in RTL

In the code below, we use the following to get the feel of OVL assertions

   

space.gif

  • assert_fifo_index : Prints error whenever there is overflow or underflow error.
  • assert_always : Prints error whenever a write happens with the fifo full flag set
  • assert_never : Prints error whenever a read happens with the fifo empty flag set
  • assert_increment : Prints error whenever the write pointer increments by a value > 1
   

space.gif

We can set the various parameters for each assertion to get the desired function; for assert_fifo_index, the parameters that need to be set are (for others, refer to OVL documentation):

   

space.gif

  • severity_level : `OVL_ERROR, This can be set to fatal, warning, and so on.
  • depth of FIFO : This is set to the depth of FIFO.
  • msg : Message that we want to print.
   

space.gif

Details on usage of this assertion could be found from OVL manual. Now to compile we need to pass the +incdir path to the VLIB install directory.

   

space.gif

Example : Let's assume vlib is installed in home directory (/home/deepak) with vlib as name and we are using verilog XL to compile.

   

space.gif

verilog +incdir+/home/deepak/vlib syn_fifo_assert.v fifo_tb.v ram_dp_ar_aw.v

   

space.gif


   1 //=============================================
   2 // Function  : Synchronous (single clock) FIFO
   3 //             With Assertion
   4 // Coder     : Deepak Kumar Tala
   5 // Date      : 1-Nov-2005
   6 //=============================================
   7 // synopsys translate_off
   8 `define OVL_ASSERT_ON
   9 `define OVL_INIT_MSG
  10 `include "assert_fifo_index.vlib"
  11 `include "assert_always.vlib"
  12 `include "assert_never.vlib"
  13 `include "assert_increment.vlib"
  14 // synopsys translate_on
  15 module syn_fifo (
  16 clk      , // Clock input
  17 rst      , // Active high reset
  18 wr_cs    , // Write chip select
  19 rd_cs    , // Read chipe select
  20 data_in  , // Data input
  21 rd_en    , // Read enable
  22 wr_en    , // Write Enable
  23 data_out , // Data Output
  24 empty    , // FIFO empty
  25 full       // FIFO full
  26 );    
  27  
  28 // FIFO constants
  29 parameter DATA_WIDTH = 8;
  30 parameter ADDR_WIDTH = 8;
  31 parameter RAM_DEPTH = (1 << ADDR_WIDTH);
  32 // Port Declarations
  33 input clk ;
  34 input rst ;
  35 input wr_cs ;
  36 input rd_cs ;
  37 input rd_en ;
  38 input wr_en ;
  39 input [DATA_WIDTH-1:0] data_in ;
  40 output full ;
  41 output empty ;
  42 output [DATA_WIDTH-1:0] data_out ;
  43 
  44 //-----------Internal variables-------------------
  45 reg [ADDR_WIDTH-1:0] wr_pointer;
  46 reg [ADDR_WIDTH-1:0] rd_pointer;
  47 reg [ADDR_WIDTH :0] status_cnt;
  48 reg [DATA_WIDTH-1:0] data_out ;
  49 wire [DATA_WIDTH-1:0] data_ram ;
  50 
  51 //-----------Variable assignments---------------
  52 assign full = (status_cnt == (RAM_DEPTH-1));
  53 assign empty = (status_cnt == 0);
  54 
  55 //-----------Code Start---------------------------
  56 always @ (posedge clk or posedge rst)
  57 begin : WRITE_POINTER
  58   if (rst) begin
  59    wr_pointer <= 0;
  60   end else if (wr_cs && wr_en ) begin
  61    wr_pointer <= wr_pointer + 1;
  62   end
  63 end
  64 
  65 always @ (posedge clk or posedge rst)
  66 begin : READ_POINTER
  67   if (rst) begin
  68     rd_pointer <= 0;
  69   end else if (rd_cs && rd_en ) begin
  70     rd_pointer <= rd_pointer + 1;
  71   end
  72 end
  73 
  74 always  @ (posedge clk or posedge rst)
  75 begin : READ_DATA
  76   if (rst) begin
  77     data_out <= 0;
  78   end else if (rd_cs && rd_en ) begin
  79     data_out <= data_ram;
  80   end
  81 end
  82 
  83 always @ (posedge clk or posedge rst)
  84 begin : STATUS_COUNTER
  85   if (rst) begin
  86     status_cnt <= 0;
  87   // Read but no write.
  88   end else if ((rd_cs && rd_en) &&  ! (wr_cs && wr_en) 
  89                 && (status_cnt  ! = 0)) begin
  90     status_cnt <= status_cnt - 1;
  91   // Write but no read.
  92   end else if ((wr_cs && wr_en) &&  ! (rd_cs && rd_en) 
  93                && (status_cnt  ! = RAM_DEPTH)) begin
  94     status_cnt <= status_cnt + 1;
  95   end
  96 end
  97    
  98 ram_dp_ar_aw #(DATA_WIDTH,ADDR_WIDTH) DP_RAM (
  99 .address_0 (wr_pointer) , // address_0 input 
 100 .data_0    (data_in)    , // data_0 bi-directional
 101 .cs_0      (wr_cs)      , // chip select
 102 .we_0      (wr_en)      , // write enable
 103 .oe_0      (1'b0)       , // output enable
 104 .address_1 (rd_pointer) , // address_q input
 105 .data_1    (data_ram)   , // data_1 bi-directional
 106 .cs_1      (rd_cs)      , // chip select
 107 .we_1      (1'b0)       , // Read enable
 108 .oe_1      (rd_en)        // output enable
 109 );  
 110 
 111 // Add assertion here
 112 // synopsys translate_off
 113 // Assertion to check overflow and underflow
 114 assert_fifo_index #(
 115 `OVL_ERROR      , // severity_level
 116 (RAM_DEPTH-1)   , // depth
 117 1               , // push width
 118 1               , // pop width
 119 `OVL_ASSERT     , // property type
 120 "my_module_err" , // msg
 121 `OVL_COVER_NONE , //coverage_level
 122 1) no_over_under_flow (
 123 .clk     (clk),           // Clock
 124 .reset_n (~rst),          // Active low reset
 125 .pop     (rd_cs & rd_en), // FIFO Write
 126 .push    (wr_cs & wr_en)  // FIFO Read
 127 );
 128 
 129 // Assertion to check full and write
 130 assert_always #(
 131 `OVL_ERROR       , // severity_level
 132 `OVL_ASSERT      , // property_type
 133 "fifo_full_write", // msg
 134 `OVL_COVER_NONE    // coverage_level
 135 ) no_full_write (
 136 .clk       (clk),
 137 .reset_n   (~rst),
 138 .test_expr ( ! (full && wr_cs && wr_en))
 139 );
 140 
 141 // Assertion to check empty and read
 142 assert_never #(
 143 `OVL_ERROR       , // severity_level
 144 `OVL_ASSERT      , // property_type
 145 "fifo_empty_read", // msg
 146 `OVL_COVER_NONE    // coverage_level
 147 ) no_empty_read (
 148 .clk       (clk),
 149 .reset_n   (~rst),
 150 .test_expr ((empty && rd_cs && rd_en))
 151 );
 152 
 153 // Assertion to check if write pointer increments by just one
 154 assert_increment #(
 155 `OVL_ERROR            , // severity_level
 156 ADDR_WIDTH            , // width
 157 1                     , // value 
 158 `OVL_ASSERT           , // property_typ 
 159 "Write_Pointer_Error" , // msg 
 160 `OVL_COVER_NONE         // coverage_level
 161 ) write_count ( 
 162 .clk         (clk), 
 163 .reset_n     (~rst),
 164 .test_expr   (wr_pointer)
 165 ); 
 166 // synopsys translate_on
 167 endmodule
You could download file syn_fifo_assert.v here
   

space.gif

  ../images/main/bulllet_4dots_orange.gif Simulator Output

The first OVL message is the init message, used to check if the OVL lib was included and ready. my_module_err is a user defined message that OVL uses in print statements.

   

space.gif

Remaining messages are OVERFLOW and UNDERFLOW messages.

   

space.gif

 OVL_NOTE: `OVL_VERSION: ASSERT_FIFO_INDEX initialized 
 @ fifo_tb.fifo.no_over_under_flow.ovl_init_msg_t Severity: 1, Message: my_module_err
 OVL_NOTE: `OVL_VERSION: ASSERT_ALWAYS initialized 
 @ fifo_tb.fifo.no_full_write.ovl_init_msg_t Severity: 1, Message: fifo_full_write
 OVL_NOTE: `OVL_VERSION: ASSERT_NEVER initialized 
 @ fifo_tb.fifo.no_empty_read.ovl_init_msg_t Severity: 1, Message: fifo_empty_read
 0 wr:0 wr_data:00 rd:0 rd_data:xx
 5 wr:0 wr_data:00 rd:0 rd_data:00
 10 wr:1 wr_data:00 rd:0 rd_data:00
 12 wr:1 wr_data:01 rd:0 rd_data:00
 14 wr:1 wr_data:02 rd:0 rd_data:00
 16 wr:1 wr_data:03 rd:0 rd_data:00
 18 wr:1 wr_data:04 rd:0 rd_data:00
 20 wr:1 wr_data:05 rd:0 rd_data:00
 22 wr:1 wr_data:06 rd:0 rd_data:00
 24 wr:1 wr_data:07 rd:0 rd_data:00
        OVL_ERROR : ASSERT_FIFO_INDEX : my_module_err : OVERFLOW : severity 1 : 
        time 25 : fifo_tb.fifo.no_over_under_flow.ovl_error_t
        OVL_ERROR : ASSERT_ALWAYS : fifo_full_write :  : severity 1 : time 25 : 
        fifo_tb.fifo.no_full_write.ovl_error_t
 26 wr:1 wr_data:08 rd:0 rd_data:00
        OVL_ERROR : ASSERT_FIFO_INDEX : my_module_err : OVERFLOW : severity 1 : 
        time 27 : fifo_tb.fifo.no_over_under_flow.ovl_error_t
 28 wr:1 wr_data:09 rd:0 rd_data:00
        OVL_ERROR : ASSERT_FIFO_INDEX : my_module_err : OVERFLOW : severity 1 : 
        time 29 : fifo_tb.fifo.no_over_under_flow.ovl_error_t
 30 wr:0 wr_data:09 rd:0 rd_data:00
 32 wr:0 wr_data:09 rd:1 rd_data:00
 33 wr:0 wr_data:09 rd:1 rd_data:08
 35 wr:0 wr_data:09 rd:1 rd_data:09
 39 wr:0 wr_data:09 rd:1 rd_data:03
 41 wr:0 wr_data:09 rd:1 rd_data:04
 43 wr:0 wr_data:09 rd:1 rd_data:05
 45 wr:0 wr_data:09 rd:1 rd_data:06
        OVL_ERROR : ASSERT_FIFO_INDEX : my_module_err : UNDERFLOW : severity 1 : 
        time 47 : fifo_tb.fifo.no_over_under_flow.ovl_error_t
 47 wr:0 wr_data:09 rd:1 rd_data:07
        OVL_ERROR : ASSERT_FIFO_INDEX : my_module_err : UNDERFLOW : severity 1 : 
        time 49 : fifo_tb.fifo.no_over_under_flow.ovl_error_t
        OVL_ERROR : ASSERT_NEVER : fifo_empty_read :  : severity 1 : time 49 : 
        fifo_tb.fifo.no_empty_read.ovl_error_t
 49 wr:0 wr_data:09 rd:1 rd_data:08
        OVL_ERROR : ASSERT_FIFO_INDEX : my_module_err : UNDERFLOW : severity 1 : 
        time 51 : fifo_tb.fifo.no_over_under_flow.ovl_error_t
        OVL_ERROR : ASSERT_NEVER : fifo_empty_read :  : severity 1 : time 51 : 
        fifo_tb.fifo.no_empty_read.ovl_error_t
 51 wr:0 wr_data:09 rd:1 rd_data:09
 52 wr:0 wr_data:09 rd:0 rd_data:09
   

space.gif

  ../images/main/bulllet_4dots_orange.gif OVL Assertion List

Below is the list of OVL assertions that are commonly used; you can always refer to the document that comes with the OVL library to get more information and a complete list of assertions available.

   

space.gif

Assertion

Description

assert_always

The assert_always assertion checker checks the single-bit expression test_expr at each rising edge of clk to verify whether it evaluates to TRUE.

assert_always_on_edge

The assert_always_on_edge assertion checker checks the single-bit expression sampling_event for a particular type of transition.

assert_change

The assert_change assertion checker checks the expression start_event at each rising edge of clk to determine if it should check for a change in the value of test_expr. If start_event is sampled TRUE, the checker evaluates test_expr and re-evaluates test_expr at each of the subsequent num_cks rising edges of clk. If the value of test_expr has not been sampled changed from its start value by the last of the num_cks cycles, the assertion fails.

assert_cycle_sequence

The assert_cycle_sequence assertion checker checks the expression event_sequence at the rising edges of clk to identify whether or not the bits in event_sequence assert sequentially on successive rising edges of clk.

assert_decrement

The assert_decrement assertion checker checks the expression test_expr at each rising edge of clk to determine if its value has changed from the one at the previous rising edge of clk. If so, the checker verifies that the new value equals the previous one decremented by value. The checker allows the value of test_expr to wrap, if the total change equals the decrement value.

assert_even_parity

The assert_even_parity assertion checker checks the expression test_expr at each rising edge of clk to verify the expression evaluates to a value that has even parity. A value has even parity if it is 0 or if the number of bits set to 1 is even.

assert_fifo_index

The assert_fifo_index assertion checker tracks the numbers of pushes (writes) and pops (reads) that occur for a FIFO or queue memory structure. This checker does permit simultaneous pushes/ pops on the queue within the same clock cycle. It ensures the FIFO never overflows (i.e., too many pushes occur without enough pops) and never underflows (i.e., too many pops occur without enough pushes).

assert_increment

The assert_increment assertion checker checks the expression test_expr at each rising edge of clk to determine if its value has changed from the one at the previous rising edge of clk. If so, the checker verifies that the new value equals the previous one incremented by value. The checker allows the value of test_expr to wrap, if the total change equals the increment value.

assert_never

The assert_never assertion checker checks the single-bit expression test_expr at each rising edge of clk to verify the expression does not evaluate to TRUE.

assert_one_hot

The assert_one_hot assertion checker checks the expression test_expr at each rising edge of clk to verify the expression evaluates to a one-hot value. A one-hot value has exactly one bit set to 1.

assert_range

The assert_range assertion checker checks the expression test_expr at each rising edge of clk to verify the expression falls in the range from min to max, inclusive. The assertion fails if test_expr< min or max < test_expr.

assert_one_cold

The assert_one_cold assertion checker checks the expression test_expr at each rising edge of clk to verify the expression evaluates to a one-cold or inactive state value. A one-cold value has exactly one bit set to 0.

   

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