diff --git a/rtl/ibex_if_stage.sv b/rtl/ibex_if_stage.sv index 875a0e1d..4ce601a8 100644 --- a/rtl/ibex_if_stage.sv +++ b/rtl/ibex_if_stage.sv @@ -266,6 +266,11 @@ module ibex_if_stage #( assert property ( @(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 ( + @(posedge clk_i) (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 8e2a5208..a0d55651 100644 --- a/rtl/ibex_load_store_unit.sv +++ b/rtl/ibex_load_store_unit.sv @@ -482,5 +482,10 @@ module ibex_load_store_unit ( // 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 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"); `endif endmodule