diff --git a/rtl/ibex_fetch_fifo.sv b/rtl/ibex_fetch_fifo.sv index 5c52e817..530fa44b 100644 --- a/rtl/ibex_fetch_fifo.sv +++ b/rtl/ibex_fetch_fifo.sv @@ -216,11 +216,6 @@ module ibex_fetch_fifo ( // Assertions // //////////////// `ifndef VERILATOR - // Code changes required to support > 2 outstanding requests - assert property ( - @(posedge clk_i) disable iff (!rst_ni) - (NUM_REQS <= 2) ); - assert property ( @(posedge clk_i) disable iff (!rst_ni) (in_valid_i) |-> ((valid_q[DEPTH-1] == 1'b0) || (clear_i == 1'b1)) ); diff --git a/rtl/ibex_prefetch_buffer.sv b/rtl/ibex_prefetch_buffer.sv index 8a817e74..649ec223 100644 --- a/rtl/ibex_prefetch_buffer.sv +++ b/rtl/ibex_prefetch_buffer.sv @@ -213,4 +213,15 @@ module ibex_prefetch_buffer ( assign instr_req_o = valid_req; assign instr_addr_o = instr_addr_w_aligned; + //////////////// + // Assertions // + //////////////// + +`ifndef VERILATOR + // Code changes required to support > 2 outstanding requests + assert property ( + @(posedge clk_i) disable iff (!rst_ni) + (NUM_REQS <= 2) ); +`endif + endmodule