github-mirrors/cve2
1
0
Fork 0
mirror of https://github.com/openhwgroup/cve2.git synced 2025-04-23 21:47:20 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

[rtl] Add new assertions

Browse source 
Signed-off-by: Pirmin Vogel <vogelpi@lowrisc.org>
This commit is contained in:
Pirmin Vogel 2019-11-14 12:44:32 +01:00
parent 40e3db5f23
commit aefbcdceb3
2 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
rtl/ibex_fetch_fifo.sv
View file

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

10
rtl/ibex_if_stage.sv
View file

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