diff --git a/rtl/ibex_if_stage.sv b/rtl/ibex_if_stage.sv index 4ce601a8..2149b479 100644 --- a/rtl/ibex_if_stage.sv +++ b/rtl/ibex_if_stage.sv @@ -259,13 +259,13 @@ module ibex_if_stage #( `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"); + @(posedge clk_i) (boot_addr_i[7:0] == 8'h00) ) else + $error("The provided boot address is not aligned to 256 bytes"); // there should never be a grant when there is no request assert property ( - @(posedge clk_i) (instr_gnt_i) |-> (instr_req_o) ) - else $warning("There was a grant without a request"); + @(posedge clk_i) (instr_gnt_i) |-> (instr_req_o) ) else + $warning("There was a grant without a request"); // assert that the address is word aligned when request is sent assert property ( diff --git a/rtl/ibex_load_store_unit.sv b/rtl/ibex_load_store_unit.sv index ce66d8a7..35b6ae63 100644 --- a/rtl/ibex_load_store_unit.sv +++ b/rtl/ibex_load_store_unit.sv @@ -471,11 +471,15 @@ module ibex_load_store_unit ( // make sure there is no new request when the old one is not yet completely done // i.e. it should not be possible to get a grant without an rvalid for the // last request - assert property ( @(posedge clk_i) - ((ls_fsm_cs == WAIT_RVALID) && (data_gnt_i == 1'b1)) |-> (data_rvalid_i == 1'b1) ); + assert property ( + @(posedge clk_i) + ((ls_fsm_cs == WAIT_RVALID) && (data_gnt_i == 1'b1)) |-> (data_rvalid_i == 1'b1) ) else + $display("Data grant set while LSU keeps waiting for rvalid"); // there should be no rvalid when we are in IDLE - assert property ( @(posedge clk_i) (ls_fsm_cs == IDLE) |-> (data_rvalid_i == 1'b0) ); + assert property ( + @(posedge clk_i) (ls_fsm_cs == IDLE) |-> (data_rvalid_i == 1'b0) ) else + $display("Data rvalid set while LSU idle"); // assert that errors are only sent at the same time as rvalid assert property ( @@ -483,7 +487,9 @@ module ibex_load_store_unit ( $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)) ); + assert property ( + @(posedge clk_i) (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 (