[dv/icache] Add qualifications in protocol checker

The rdata driven by the cache is undefined when there is an error. There
are therefore no requirements on stability.

Signed-off-by: Tom Roberts <tomroberts@lowrisc.org>
This commit is contained in:
Tom Roberts 2020-05-21 14:06:59 +01:00 committed by Tom Roberts
parent 84c5373c27
commit 65b21c6741

View file

@ -91,10 +91,10 @@ interface ibex_icache_core_protocol_checker (
`ASSERT(Err2Stable, unfinished_valid |=> $stable(err_plus2), clk, !rst_n);
`ASSERT(LoRDataStable,
unfinished_valid |=> $stable(rdata[15:0]),
unfinished_valid & ~err |=> $stable(rdata[15:0]),
clk, !rst_n);
`ASSERT(HiRDataStable,
unfinished_valid & (rdata[1:0] == 2'b11) |=> $stable(rdata[31:16]),
unfinished_valid & ~err & (rdata[1:0] == 2'b11) |=> $stable(rdata[31:16]),
clk, !rst_n);
// The err_plus2 signal means "this error was caused by the upper two bytes" and is only read when