These changes correspond to similar changes in the prefetch buffer to
support branch prediction. A registered version of fill_ext_done was
required to prevent a combinational loop from branch_i in to valid_o
out.
Multiplexing priorities for fifo_addr have been swapped to match
fetch_addr_d in the same module and all similar multiplexing in the
icache (prioritize incoming branch_i over branch_mispredict_i). Note
however that it is not expected that these conditions will actually
occur together, and an assertion has been added to check that.
Signed-off-by: Tom Roberts <tomroberts@lowrisc.org>
Remove the SpeculativeRequest parameter, and replace it with a
policy. If the cache is disabled, make the request on the basis that we
definitely won't hit in the cache and so should make the bus request
asap.
Stop fill buffers from fetching complete cache lines when the cache is
disabled. When the core branches into the middle of a line, the lower
words would normally be fetched to complete the line. This is
unnecessary when the cache is disabled since those words will just be
thrown away and the core will stall while they are being fetched.
These two changes make the performance using the disabled icache the
same as using non-icache prefetch buffer.
Signed-off-by: Tom Roberts <tomroberts@lowrisc.org>
The PR that I pushed up to add sby support to
Edalize (https://github.com/olofk/edalize/pull/173) ended up with a
different input format from the one it started with.
That's now merged into master, so this patch updates the Ibex code to
match the final syntax.
This turns out to be quite complicated, because the icache has a lot
of different counters that all track addresses or fill buffer state.
For an inductive proof to go through, you need to make the relations
between them explicit, which takes lots of assertions.
All of the signals defined in the formal_tb are prefixed with 'f_'.
This isn't strictly necessary, but it makes it much easier to see what
came from the design (since we are "bound in", our ports don't have _o
or _i suffixes).
We add a couple of protocol assumptions:
ICache <-> Core:
- Branch target addresses are half-word aligned
- The branch_spec signal is driven if branch is
ICache <-> Memory:
- The bus doesn't respond unless there is an outstanding request
- The bus doesn't grant more than 4 billion outstanding requests(!)
There's also some protocol state tracking:
- f_addr_valid tracks whether the ICache currently has an
architectural address. It goes high with branch_i (which gives the
cache an address) and goes low when the cache completes a
transaction with err_o set (since the data is bad, there's no
notion of a "next address").
- f_reqs_on_bus tracks the number of requests currently outstanding
on the bus. This is used for the ICache <-> Memory assumptions
above. We have some internal assertions that check this equals the
sum of the "ext" counters minus the sum of the "rvd" counters.
With these assumptions, we can prove:
- Once asserted, valid_o stays high until a transaction is completed
by ready_i or until branch_i is asserted (which cancels the
transaction).
- While the transaction is pending, addr_o remains stable.
- While the transaction is pending, err_o remains stable and, if
err_o is asserted, so does err_plus2_o.
- While the transaction is pending, if err_o and err_plus2_o are
high then bottom 16 bits of the returned instruction data imply an
uncompressed instruction.
- While the transaction is pending, if err_o is low then the bottom
16 bits of the returned instruction remain stable.
- While the transaction is pending, if err_o is low and the bottom
16 bits of the returned instruction imply an uncompressed
instruction then the top 16 bits of the returned instruction
remain stable.
To get this working, you need a corresponding patch in Edalize, which
adds SymbiYosys as an EDA tool.
At the moment, this proves a couple of simple bus assertions. Later
patches will add more.
There are currently some rough edges to this flow:
(1) We use a hacky pre_build hook to run sv2v and edit the files in
the work tree. Among other problems, this means that the any
failure messages that come out of sby have bogus line numbers.
(2) Since we haven't yet got bind support in Yosys, we have to
include a fragment from the design itself.
