Skip to content

Commit 1e8fc08

Browse files
Xelef2000Xelef2000
committed
fixed asserts
1 parent f946c05 commit 1e8fc08

File tree

4 files changed

+93
-33
lines changed

4 files changed

+93
-33
lines changed

‎rtl/common_cells/fifo_v3.sv‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -140,13 +140,16 @@ module fifo_v3 #(
140140
end
141141

142142
`ifndef COMMON_CELLS_ASSERTS_OFF
143+
`ifndef SYNTHESIS
143144
`ASSERT_INIT(depth_0, DEPTH > 0, "DEPTH must be greater than 0.")
144-
145-
`ASSERT(full_write, full_o |-> ~push_i, clk_i, !rst_ni,
146-
"Trying to push new data although the FIFO is full.")
147-
148-
`ASSERT(empty_read, empty_o |-> ~pop_i, clk_i, !rst_ni,
149-
"Trying to pop data although the FIFO is empty.")
145+
`ASSERT(full_write, full_o |-> ~push_i, clk_i, !rst_ni, "Trying to push new data although the FIFO is full.")
146+
`ASSERT(empty_read, empty_o |-> ~pop_i, clk_i, !rst_ni, "Trying to pop data although the FIFO is empty.")
147+
`else
148+
`ASSERT_INIT(depth_0, DEPTH > 0)
149+
`ASSERT(full_write, full_o |-> ~push_i, clk_i, !rst_ni)
150+
`ASSERT(empty_read, empty_o |-> ~pop_i, clk_i, !rst_ni)
151+
`endif
150152
`endif
151153

154+
152155
endmodule // fifo_v3

‎rtl/common_cells/lzc.sv‎

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -41,10 +41,18 @@ module lzc #(
4141

4242
localparam int unsigned NumLevels = $clog2(WIDTH);
4343

44+
45+
4446
`ifndef COMMON_CELLS_ASSERTS_OFF
45-
`ASSERT_INIT(width_0, WIDTH > 0, "input must be at least one bit wide")
47+
`ifndef SYNTHESIS
48+
`ASSERT_INIT(width_0, WIDTH > 0, "input must be at least one bit wide")
49+
`else
50+
`ASSERT_INIT(width_0, WIDTH > 0)
51+
`endif
4652
`endif
4753

54+
55+
4856
logic [WIDTH-1:0][NumLevels-1:0] index_lut;
4957
logic [2**NumLevels-1:0] sel_nodes;
5058
logic [2**NumLevels-1:0][NumLevels-1:0] index_nodes;
@@ -99,8 +107,14 @@ module lzc #(
99107

100108
end : gen_lzc
101109

110+
102111
`ifndef COMMON_CELLS_ASSERTS_OFF
103-
`ASSERT_INIT(width_0, WIDTH >= 1, "The WIDTH must at least be one bit wide!")
112+
`ifndef SYNTHESIS
113+
`ASSERT_INIT(width_0, WIDTH >= 1, "The WIDTH must at least be one bit wide!")
114+
`else
115+
`ASSERT_INIT(width_0, WIDTH >= 1)
116+
`endif
104117
`endif
105118

119+
106120
endmodule : lzc

‎rtl/common_cells/rr_arb_tree.sv‎

Lines changed: 61 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -160,18 +160,36 @@ module rr_arb_tree #(
160160
end
161161
end
162162
end
163-
163+
164164
`ifndef COMMON_CELLS_ASSERTS_OFF
165-
`ASSERT(lock, req_o && (!gnt_i && !flush_i) |=> idx_o == $past(idx_o),
166-
clk_i, !rst_ni || flush_i,
167-
"Lock implies same arbiter decision in next cycle if output is not ready.")
168-
169-
logic [NumIn-1:0] req_tmp;
170-
assign req_tmp = req_q & req_i;
171-
`ASSUME(lock_req, lock_d |=> req_tmp == req_q, clk_i, !rst_ni || flush_i,
172-
"It is disallowed to deassert unserved request signals when LockIn is enabled.")
165+
`ifndef SYNTHESIS
166+
`ASSERT(lock,
167+
req_o && (!gnt_i && !flush_i) |=> idx_o == $past(idx_o),
168+
clk_i, !rst_ni || flush_i,
169+
"Lock implies same arbiter decision in next cycle if output is not ready.")
170+
171+
logic [NumIn-1:0] req_tmp;
172+
assign req_tmp = req_q & req_i;
173+
174+
`ASSUME(lock_req,
175+
lock_d |=> req_tmp == req_q,
176+
clk_i, !rst_ni || flush_i,
177+
"It is disallowed to deassert unserved request signals when LockIn is enabled.")
178+
`else
179+
`ASSERT(lock,
180+
req_o && (!gnt_i && !flush_i) |=> idx_o == $past(idx_o),
181+
clk_i, !rst_ni || flush_i)
182+
183+
logic [NumIn-1:0] req_tmp;
184+
assign req_tmp = req_q & req_i;
185+
186+
`ASSUME(lock_req,
187+
lock_d |=> req_tmp == req_q,
188+
clk_i, !rst_ni || flush_i)
189+
`endif
173190
`endif
174191

192+
175193
always_ff @(posedge clk_i or negedge rst_ni) begin : p_req_regs
176194
if (!rst_ni) begin
177195
req_q <= '0;
@@ -293,27 +311,48 @@ module rr_arb_tree #(
293311
//////////////////////////////////////////////////////////////
294312
end
295313
end
296-
314+
297315
`ifndef COMMON_CELLS_ASSERTS_OFF
298-
`ASSERT_INIT(numin_0, NumIn, "Input must be at least one element wide.")
299-
`ASSERT_INIT(lockin_and_extprio, !(LockIn && ExtPrio),
300-
"Cannot use LockIn feature together with external ExtPrio.")
316+
`ifndef SYNTHESIS
317+
`ASSERT_INIT(numin_0, NumIn, "Input must be at least one element wide.")
318+
`ASSERT_INIT(lockin_and_extprio, !(LockIn && ExtPrio),
319+
"Cannot use LockIn feature together with external ExtPrio.")
320+
321+
`ASSERT(hot_one, $onehot0(gnt_o), clk_i, !rst_ni || flush_i,
322+
"Grant signal must be hot1 or zero.")
323+
324+
`ASSERT(gnt0, |gnt_o |-> gnt_i, clk_i, !rst_ni || flush_i,
325+
"Grant out implies grant in.")
301326

302-
`ASSERT(hot_one, $onehot0(gnt_o), clk_i, !rst_ni || flush_i,
303-
"Grant signal must be hot1 or zero.")
327+
`ASSERT(gnt1, req_o |-> gnt_i |-> |gnt_o, clk_i, !rst_ni || flush_i,
328+
"Req out and grant in implies grant out.")
304329

305-
`ASSERT(gnt0, |gnt_o |-> gnt_i, clk_i, !rst_ni || flush_i, "Grant out implies grant in.")
330+
`ASSERT(gnt_idx, req_o |-> gnt_i |-> gnt_o[idx_o], clk_i, !rst_ni || flush_i,
331+
"Idx_o / gnt_o do not match.")
306332

307-
`ASSERT(gnt1, req_o |-> gnt_i |-> |gnt_o, clk_i, !rst_ni || flush_i,
308-
"Req out and grant in implies grant out.")
333+
`ASSERT(req0, |req_i |-> req_o, clk_i, !rst_ni || flush_i,
334+
"Req in implies req out.")
309335

310-
`ASSERT(gnt_idx, req_o |-> gnt_i |-> gnt_o[idx_o], clk_i, !rst_ni || flush_i,
311-
"Idx_o / gnt_o do not match.")
336+
`ASSERT(req1, req_o |-> |req_i, clk_i, !rst_ni || flush_i,
337+
"Req out implies req in.")
338+
`else
339+
`ASSERT_INIT(numin_0, NumIn)
340+
`ASSERT_INIT(lockin_and_extprio, !(LockIn && ExtPrio))
312341

313-
`ASSERT(req0, |req_i |-> req_o, clk_i, !rst_ni || flush_i, "Req in implies req out.")
342+
`ASSERT(hot_one, $onehot0(gnt_o), clk_i, !rst_ni || flush_i)
314343

315-
`ASSERT(req1, req_o |-> |req_i, clk_i, !rst_ni || flush_i, "Req out implies req in.")
344+
`ASSERT(gnt0, |gnt_o |-> gnt_i, clk_i, !rst_ni || flush_i)
345+
346+
`ASSERT(gnt1, req_o |-> gnt_i |-> |gnt_o, clk_i, !rst_ni || flush_i)
347+
348+
`ASSERT(gnt_idx, req_o |-> gnt_i |-> gnt_o[idx_o], clk_i, !rst_ni || flush_i)
349+
350+
`ASSERT(req0, |req_i |-> req_o, clk_i, !rst_ni || flush_i)
351+
352+
`ASSERT(req1, req_o |-> |req_i, clk_i, !rst_ni || flush_i)
353+
`endif
316354
`endif
355+
317356
end
318357

319358
endmodule : rr_arb_tree

‎rtl/common_cells/spill_register_flushable.sv‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -95,9 +95,13 @@ module spill_register_flushable #(
9595
// We empty the spill register before the slice register.
9696
assign data_o = b_full_q ? b_data_q : a_data_q;
9797

98-
`ifndef COMMON_CELLS_ASSERTS_OFF
99-
`ASSERT(flush_valid, flush_i |-> ~valid_i, clk_i, !rst_ni,
98+
`ifndef COMMON_CELLS_ASSERTS_OFF
99+
`ifndef SYNTHESIS
100+
`ASSERT(flush_valid, flush_i |-> ~valid_i, clk_i, !rst_ni,
100101
"Trying to flush and feed the spill register simultaneously. You will lose data!")
101-
`endif
102+
`else
103+
`ASSERT(flush_valid, flush_i |-> ~valid_i, clk_i, !rst_ni)
104+
`endif
105+
`endif
102106
end
103107
endmodule

0 commit comments

Comments
 (0)