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. | Â | Example : Let's assume vlib is installed in home directory (/home/deepak) with vlib as name and we are using verilog XL to compile. | verilog +incdir+/home/deepak/vlib syn_fifo_assert.v fifo_tb.v ram_dp_ar_aw.v | 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 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. Remaining messages are OVERFLOW and UNDERFLOW messages. | 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 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. | 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. | Â | Â | Â | |