From 40e3db5f23e015db6633f6f489eb190da7c20233 Mon Sep 17 00:00:00 2001 From: Pirmin Vogel Date: Wed, 13 Nov 2019 18:44:50 +0100 Subject: [PATCH] [rtl] Rework assertions This commit modifies the assertions to not fire as long as the reset is active. Also, it updates some assertions. This resolves lowRISC/ibex#274. Signed-off-by: Pirmin Vogel --- rtl/ibex_fetch_fifo.sv | 7 ++++--- rtl/ibex_id_stage.sv | 33 ++++++++++++++++----------------- rtl/ibex_if_stage.sv | 16 ++++++++-------- rtl/ibex_load_store_unit.sv | 34 +++++++++++++++++----------------- 4 files changed, 45 insertions(+), 45 deletions(-) diff --git a/rtl/ibex_fetch_fifo.sv b/rtl/ibex_fetch_fifo.sv index e2e5639a..c30f7798 100644 --- a/rtl/ibex_fetch_fifo.sv +++ b/rtl/ibex_fetch_fifo.sv @@ -220,8 +220,9 @@ module ibex_fetch_fifo #( // Assertions // //////////////// `ifndef VERILATOR - assert property ( - @(posedge clk_i) disable iff (!rst_ni) - (in_valid_i) |-> ((valid_q[DEPTH-1] == 1'b0) || (clear_i == 1'b1)) ); + // 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 + $display("Must not push when FIFO full"); `endif endmodule diff --git a/rtl/ibex_id_stage.sv b/rtl/ibex_id_stage.sv index 322bd27c..fdf854ad 100644 --- a/rtl/ibex_id_stage.sv +++ b/rtl/ibex_id_stage.sv @@ -608,28 +608,27 @@ module ibex_id_stage #( //////////////// `ifndef VERILATOR - // make sure that branch decision is valid when jumping - assert property ( - @(posedge clk_i) (branch_decision_i !== 1'bx || branch_in_dec == 1'b0) ) else - $display("Branch decision is X"); + // branch decision must be valid when jumping + assert property (@(posedge clk_i) disable iff (!rst_ni) + (branch_decision_i !== 1'bx || !branch_in_dec)) else + $display("Branch decision is X"); `ifdef CHECK_MISALIGNED - assert property ( - @(posedge clk_i) (~lsu_addr_incr_req_i) ) else - $display("Misaligned memory access at %x",pc_id_i); + assert property (@(posedge clk_i) disable iff (!rst_ni) + (!lsu_addr_incr_req_i)) else + $display("Misaligned memory access at %x",pc_id_i); `endif - // the instruction delivered to the ID stage should always be valid - assert property ( - @(posedge clk_i) (instr_valid_i & ~(illegal_c_insn_i | instr_fetch_err_i)) |-> - (!$isunknown(instr_rdata_i)) ) else - $display("Instruction is valid, but has at least one X"); - - // make sure multicycles enable signals are unique - assert property ( - @(posedge clk_i) ~(data_req_dec & multdiv_en_dec)) else - $display("Multicycles enable signals are not unique"); + // instruction delivered to ID stage must always be valid + assert property (@(posedge clk_i) disable iff (!rst_ni) + (instr_valid_i && !(illegal_c_insn_i || instr_fetch_err_i)) |-> + (!$isunknown(instr_rdata_i))) else + $display("Instruction is valid, but has at least one X"); + // multicycle enable signals must be unique + assert property (@(posedge clk_i) disable iff (!rst_ni) + ($onehot0({data_req_dec, multdiv_en_dec, branch_in_dec, jump_in_dec}))) else + $display("Multicycle enable signals are not unique"); `endif endmodule diff --git a/rtl/ibex_if_stage.sv b/rtl/ibex_if_stage.sv index f3a58f71..91abcb25 100644 --- a/rtl/ibex_if_stage.sv +++ b/rtl/ibex_if_stage.sv @@ -256,15 +256,15 @@ module ibex_if_stage #( // Assertions // //////////////// `ifndef VERILATOR - // the boot address needs to be aligned to 256 bytes - assert property ( - @(posedge clk_i) (boot_addr_i[7:0] == 8'h00) ) else - $error("The provided boot address is not aligned to 256 bytes"); + // boot address must be aligned to 256 bytes + assert property (@(posedge clk_i) disable iff (!rst_ni) + (boot_addr_i[7:0] == 8'h00)) else + $error("Provided boot address not aligned to 256 bytes"); - // assert that the address is word aligned when request is sent - assert property ( - @(posedge clk_i) (instr_req_o) |-> (instr_addr_o[1:0] == 2'b00) ) else - $display("Instruction address not word aligned"); + // 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 + $display("Instruction address not word aligned"); `endif endmodule diff --git a/rtl/ibex_load_store_unit.sv b/rtl/ibex_load_store_unit.sv index d823938e..b33f3fc3 100644 --- a/rtl/ibex_load_store_unit.sv +++ b/rtl/ibex_load_store_unit.sv @@ -483,25 +483,25 @@ module ibex_load_store_unit ( //////////////// `ifndef VERILATOR - // there should not be an rvalid unless the FSM is handlling it - assert property ( - @(posedge clk_i) (data_rvalid_i) |-> ((ls_fsm_cs == WAIT_RVALID) || - (ls_fsm_cs == WAIT_RVALID_MIS) || (ls_fsm_cs == WAIT_RVALID_DONE)) ) else - $display("Data response valid received without expecting it"); + // there must not be an rvalid unless the FSM is handlling it + assert property (@(posedge clk_i) disable iff (!rst_ni) + (data_rvalid_i) |-> ((ls_fsm_cs == WAIT_RVALID) || + (ls_fsm_cs == WAIT_RVALID_MIS) || (ls_fsm_cs == WAIT_RVALID_DONE))) else + $display("Data response valid received without expecting it"); - // assert that errors are only sent at the same time as rvalid - assert property ( - @(posedge clk_i) (data_err_i) |-> (data_rvalid_i) ) else - $display("Data error not sent with rvalid"); + // errors must only be sent together with rvalid + assert property (@(posedge clk_i) disable iff (!rst_ni) + (data_err_i) |-> (data_rvalid_i)) else + $display("Data error not sent with rvalid"); - // assert that the address does not contain X when request is sent - assert property ( - @(posedge clk_i) (data_req_o) |-> (!$isunknown(data_addr_o)) ) else - $display("Data address not valid"); + // address must not contain X when request is sent + assert property (@(posedge clk_i) disable iff (!rst_ni) + (data_req_o) |-> (!$isunknown(data_addr_o))) else + $display("Data address not valid"); - // assert that the address is word aligned when request is sent - assert property ( - @(posedge clk_i) (data_req_o) |-> (data_addr_o[1:0] == 2'b00) ) else - $display("Data address not word aligned"); + // address must be word aligned when request is sent + assert property (@(posedge clk_i) disable iff (!rst_ni) + (data_req_o) |-> (data_addr_o[1:0] == 2'b00)) else + $display("Data address not word aligned"); `endif endmodule