github-mirrors/ibex
1
0
Fork 0
mirror of https://github.com/lowRISC/ibex.git synced 2025-04-22 04:47:25 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

Change format of assertions and add display output

Browse source
This commit is contained in:
Pirmin Vogel 2019-06-24 19:14:10 +01:00 • committed by Philipp Wagner
parent b3c6c7ddbf
commit 37d9322785
2 changed files with 14 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

8
rtl/ibex_if_stage.sv
View file

@ -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 (

14
rtl/ibex_load_store_unit.sv
View file

@ -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 (