e68d8a6cd6
Fix two frontend bugs: possibility for fetch to be blocked at CIR whilst also not going to FIFO (fixed by making those signals the complement of each other) and typo in the shift value for shifting into a CIR with 32 bits of contents, which is only reachable via a CIR-locked branch to an unaligned address.
2022-06-13 01:23:32 +01:00
23b4dbe7f3
Redesign fetch queue: 2x32 + 3x16 -> 6x16.
...
Should make it easier to support finer-grained flushing,
and handle predicted branches cleanly.
2022-06-12 02:44:08 +01:00
d5a202e4a5
Add standalone frontend formal tb
2022-06-11 20:14:24 +01:00
cd3125b6e5
Add new bus signals on instruction_fetch_match/tb.v
2022-05-27 21:48:45 +01:00
4946248dc4
RVFI monitor: blank out instructions which experienced an instruction fetch fault.
...
(previous monitor logic was ok when fetch faults weren't implemented.
If the blanked instruction has side effects, these will break other test
properties, which we would detect.)
2022-04-12 13:38:19 +01:00
8a61fe5243
Fix RVFI monitor assuming rs2 data is equivalent to store data
...
(this used to be true, but was re-plumbed when optimising A extension implementation)
2022-04-12 13:27:53 +01:00
9e27db0884
Connect or tie off missing ports on RVFI wrapper
2022-04-12 13:27:03 +01:00
0a369efc06
Add single-port bus compliance. Fix adapter not re-arbitrating following an ERROR response, causing a squashed younger load-store to remain presented to the bus.
2021-12-18 15:41:05 +00:00
1b0e205f87
Fix bad AMO asserts. Fix hwdata instability during stalled AMO write dphase, which meant AMOs were fundamentally broken following yesterday's datapath origami
2021-12-18 14:51:46 +00:00
52d58fdee4
Add keep wires for debug port on bus compliance tb
2021-12-11 12:06:10 +00:00
449348f459
Fix bug where an IRQ can fire during load/store dphase, followed by dphase bus exception.
...
Result was that the exception would sample the IRQ vector PC rather than the load/store instruction PC.
Fix by fencing off on in-flight dphases before asserting the IRQ. This adds a cycle of jitter
to IRQs, but is required for correct operation without adding a full exception-gathering pipeline.
2021-12-07 19:24:53 +00:00
dbc331dbb4
Add exclusives bus properties
2021-12-07 05:47:25 +00:00
93be227d8a
Add (currently failing) trap entry property. Fails when an IRQ arrives during a load/store data phase which subsequently excepts.
2021-12-06 20:12:23 +00:00
12205f12c7
Add instruction fetch match check
2021-05-30 11:22:36 +01:00
16dc905dce
Add simple formal bus properties check
2021-05-30 10:19:42 +01:00
2330b84b73
Use .f for riscv-formal tb dependencies, small reshuffling of directories
2021-05-30 09:44:57 +01:00
089bcc7c43
Typo
2021-05-29 23:24:18 +01:00
90acfdcbe8
Organise test directory into formal and sim
2021-05-23 07:42:35 +01:00
Luke Wren