From aefbcdceb327a7af47e8c9af710a5110aab5a0eb Mon Sep 17 00:00:00 2001 From: Pirmin Vogel Date: Thu, 14 Nov 2019 12:44:32 +0100 Subject: [PATCH] [rtl] Add new assertions Signed-off-by: Pirmin Vogel --- rtl/ibex_fetch_fifo.sv | 5 +++++ rtl/ibex_if_stage.sv | 10 ++++++++++ 2 files changed, 15 insertions(+) diff --git a/rtl/ibex_fetch_fifo.sv b/rtl/ibex_fetch_fifo.sv index c30f7798..a2c3ac15 100644 --- a/rtl/ibex_fetch_fifo.sv +++ b/rtl/ibex_fetch_fifo.sv @@ -220,6 +220,11 @@ module ibex_fetch_fifo #( // Assertions // //////////////// `ifndef VERILATOR + // must not push and pop simultaneously when FIFO full + assert property (@(posedge clk_i) disable iff (!rst_ni) + (in_valid_i && pop_fifo) |-> (!valid_q[DEPTH-1] || clear_i)) else + $display("Simultaneous pushing and popping not supported when FIFO full"); + // must not push to FIFO when full assert property (@(posedge clk_i) disable iff (!rst_ni) (in_valid_i) |-> (!valid_q[DEPTH-1] || clear_i)) else diff --git a/rtl/ibex_if_stage.sv b/rtl/ibex_if_stage.sv index 91abcb25..8c2b3e65 100644 --- a/rtl/ibex_if_stage.sv +++ b/rtl/ibex_if_stage.sv @@ -261,6 +261,16 @@ module ibex_if_stage #( (boot_addr_i[7:0] == 8'h00)) else $error("Provided boot address not aligned to 256 bytes"); + // errors must only be sent together with rvalid + assert property (@(posedge clk_i) disable iff (!rst_ni) + (instr_err_i) |-> (instr_rvalid_i)) else + $display("Instruction error not sent with rvalid"); + + // address must not contain X when request is sent + assert property (@(posedge clk_i) disable iff (!rst_ni) + (instr_req_o) |-> (!$isunknown(instr_addr_o))) else + $display("Instruction address not valid"); + // address must be word aligned when request is sent assert property (@(posedge clk_i) disable iff (!rst_ni) (instr_req_o) |-> (instr_addr_o[1:0] == 2'b00)) else