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

Weaken some checks on cache in ibex_icache_core_protocol_checker

Browse source 
Once the cache has passed an error to the core, we now allow it to
wiggle its valid, addr, rdata, err and err_plus2 lines however it sees
fit until the core issues a new branch.

Since the core isn't allowed to assert ready until then, the values
will not be read and this won't matter.

This was exposed by

  make -C dv/uvm/icache/dv run SEED=1314810947 WAVES=1
This commit is contained in:
Rupert Swarbrick 2020-05-11 16:38:26 +01:00 • committed by Rupert Swarbrick
parent d51d970089
commit 22b0609b4f
2 changed files with 29 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

1
doc/icache.rst
View file

@ -223,6 +223,7 @@ Fetched instructions are returned to the core using ports ``ready_i``, ``valid_o
This interface uses a form of ready/valid handshaking.
A transaction is signalled by ready and valid being high.
If valid goes high, it will remain high and the other output signals will remain stable until the transaction goes through or is cancelled by ``branch_i`` being asserted.
The only exception is after an error is passed to the core. Once that has happened, there is no constraint on the values of ``valid_o``, ``rdata_o``, ``addr_o``, ``err_o`` and ``err_plus2_o`` until the next time ``branch_i`` is asserted.
There is no constraint on the behaviour of ``ready_i``.
The 32-bit wide ``rdata_o`` signal contains instruction data fetched from ``addr_o``.

49
dv/uvm/icache/dv/ibex_icache_core_agent/ibex_icache_core_protocol_checker.sv
View file

@ -46,27 +46,6 @@ interface ibex_icache_core_protocol_checker (
`ASSERT(BranchAddrAligned, branch |-> !branch_addr[0], clk, !rst_n)
// The main instruction interface
//
// This uses a form of ready/valid handshaking, with a special rule that asserting branch_i
// cancels a transaction (so the cache can assert valid, but de-assert it if the core asserts
// branch_i).
//
// Note that the lower 16 bits of rdata must be stable, but the upper bits may change if this is a
// compressed instruction (which is the case if the bottom 2 bits are not 2'b11): the upper bits
// are then ignored by the core.
//
// There's no requirement on the core to hold ready until valid.
`ASSERT(ValidUntilReady, valid & ~(ready | branch) |=> valid, clk, !rst_n);
`ASSERT(AddrStable, valid & ~(ready | branch) |=> $stable(addr), clk, !rst_n);
`ASSERT(ErrStable, valid & ~(ready | branch) |=> $stable(err), clk, !rst_n);
`ASSERT(Err2Stable, valid & ~(ready | branch) |=> $stable(err_plus2), clk, !rst_n);
`ASSERT(LoRDataStable,
valid & ~(ready | branch) |=> $stable(rdata[15:0]),
clk, !rst_n);
`ASSERT(HiRDataStable,
valid & ~(ready | branch) & (rdata[1:0] == 2'b11) |=> $stable(rdata[15:0]),
clk, !rst_n);
// The core is never allowed to make a fetch from the cache when the PC is not known. To set the
// PC, it must issue a branch. Obviously, that means the core must branch before the first fetch
@ -90,6 +69,34 @@ interface ibex_icache_core_protocol_checker (
`ASSERT(NoFetchWithoutAddr, ready |-> (branch | has_addr), clk, !rst_n)
// This uses a form of ready/valid handshaking, with two special rules.
//
// 1. Asserting branch_i cancels a transaction (so the cache can assert valid, but de-assert it
// if the core asserts branch_i).
//
// 2. After signalling an error to the core (when has_addr is false), the cache can do whatever
// it likes: the core may not re-assert ready until it asserts branch.
//
// Note that the lower 16 bits of rdata must be stable, but the upper bits may change if this is a
// compressed instruction (which is the case if the bottom 2 bits are not 2'b11): the upper bits
// are then ignored by the core.
//
// There's no requirement on the core to hold ready until valid.
logic unfinished_valid;
assign unfinished_valid = has_addr & valid & ~(ready | branch);
`ASSERT(ValidUntilReady, unfinished_valid |=> valid, clk, !rst_n);
`ASSERT(AddrStable, unfinished_valid |=> $stable(addr), clk, !rst_n);
`ASSERT(ErrStable, unfinished_valid |=> $stable(err), clk, !rst_n);
`ASSERT(Err2Stable, unfinished_valid |=> $stable(err_plus2), clk, !rst_n);
`ASSERT(LoRDataStable,
unfinished_valid |=> $stable(rdata[15:0]),
clk, !rst_n);
`ASSERT(HiRDataStable,
unfinished_valid & (rdata[1:0] == 2'b11) |=> $stable(rdata[15:0]),
clk, !rst_n);
// The err_plus2 signal means "this error was caused by the upper two bytes" and is only read when
// both valid and err are true. It should never be set for compressed instructions (for them, the
// contents of the upper two bytes are ignored).