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