ibex/formal
Tom Roberts 8db89a9dfc [rtl] Add branch prediction signals to icache
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>
2020-12-02 15:10:48 +00:00
..
data_ind_timing [formal] Add check for multdiv cycle consumption 2020-09-16 16:30:20 +01:00
icache [rtl] Add branch prediction signals to icache 2020-12-02 15:10:48 +00:00
riscv-formal Move riscv-formal code into formal/riscv-formal 2020-07-02 15:19:11 +01:00
.gitignore [formal] Create Ibex Verilog source 2020-05-25 16:47:25 +01:00