Add L2 fills and a stream prefetcher to the coherent home

README.md

@@ -172,7 +172,8 @@ every supported extension and privilege mode.
   load queue. The L1D holds 32-byte sectors in I, S or M states, with eight
   read slots and up to eight misses in flight to the L2, seven of them for
   loads. The L2's coherence home orders
-  the L1s, page-table walks and DMA by sector and has four fills. Low BRAM
+  the L1s, page-table walks and DMA by sector, has eight fills, and prefetches
+  data and instruction streams into the L2. Low BRAM
   uses an 8 KiB instruction cache and L0 data reads with write-through stores.
   DMA is coherent with the data caches.
 - 256 KiB of on-chip BRAM and 1 GiB of cached DDR4, with the same

ROADMAP.md

@@ -39,10 +39,11 @@ freed as soon as its result is staged for the common data bus, before the
 load retires, so returned loads stay observable until they retire. A store
 acquires M before it writes. Probe data and acknowledgements must keep making
 progress when every queue is full. In simulation, memory-bound code in DDR
-runs slower through the home than through the previous hierarchy: the L1D
-sends its store acquisitions one at a time, the home has four fills, and it
-has no stream prefetcher yet. Other paths also take more cycles than
-before. The L1D completes one cached store at a time, hits included. The
+runs slower through the home than through the previous hierarchy, even with
+the home's eight fills and its stream prefetcher: the L1D sends its store
+acquisitions one at a time, and its read slots hold one load each, so a
+sequential stream keeps few misses in flight. Other paths also take more
+cycles than before. The L1D completes one cached store at a time, hits included. The
 probe for an instruction or page-table read downgrades a Modified sector to
 Shared, so the next store to it acquires it again. An instruction refill
 or page-table read from the L2 takes about 25 cycles, against 10 to 16
@@ -132,10 +133,11 @@ model of `cpu_top` and `soc_top` that CI compares with a CoreMark trace from
 the RTL. Its sweep of the previous hierarchy showed that a second memory
 channel needs about 16 reads in flight to use its bandwidth. In the coherent
 path, `L1D_NUM_MSHR` sets the L1D's request endpoints, eight on X3, so up to
-seven load misses go to a home with four fills; `L2_NUM_MSHR` and the L2
-prefetch parameters have no effect on the CPU. Measuring 8, 12 and 16 L2
-misses in flight in the RTL therefore needs more fills in the home, and a
-prefetcher in the home could supply further concurrent requests.
+seven load misses go to the home. `L2_NUM_MSHR` sets the home's fills, eight
+on X3, and the home's stream prefetcher adds up to four requests of its own.
+With four fills and no prefetcher, the demand side never had more than four
+L2 misses in flight in the programs measured in simulation, so more fills
+pay only together with the prefetcher.
 
 ## Verification
 

boards/README.md

@@ -10,9 +10,10 @@ and the [VCU118 guide](vcu118/README.md) for its board integration and usage.
 
 The X3 has eight L1D read slots and eight L1D request endpoints, so up to
 seven load misses and one store or LR acquisition are in flight to the L2 at
-once, and eight load queue entries. Its L2 coherence home has four fills, each with
-an initiating request and room for two more read waiters, and two writeback
-slots.
+once, and eight load queue entries. Its L2 coherence home has eight fills, each with
+an initiating request and room for two more read waiters, two writeback
+slots, and a stream prefetcher that reads ahead of the hart's data and
+instruction miss streams.
 
 ## Architecture Overview
 

boards/xilinx_frost_subsystem.sv

@@ -33,7 +33,7 @@ module xilinx_frost_subsystem #(
     parameter int unsigned L1I_CACHE_BYTES = 16 * 1024,
     // L2 line size (see frost.sv); the DDR AXI data width follows it.
     parameter int unsigned L2_LINE_BYTES = 64,
-    parameter int unsigned L2_NUM_MSHR = 4,
+    parameter int unsigned L2_NUM_MSHR = 8,
     parameter int unsigned L2_PREFETCH_INFLIGHT = 4,
     // Optional boot-hang UART classifier. Leave off for interactive testing.
     parameter int unsigned ENABLE_HANG_TRIAGE = 0,

formal/README.md

@@ -278,14 +278,15 @@ divider runs in the `divider` simulation, against Python integer division.
 | `axil_reg_bridge` | Unbounded AXI4-Lite channel stability, independent AW/W capture, response conservation, reset cancellation, aligned read pairs, and equivalence of write offsets, lane selection and wide-write enables to the SoC register expressions. `prove` uses the NIC bank, `prove_engine` the DMA bank, and `cover` exercises channel skew, partial wide writes, response stalls and reset. Assumes a master that holds each request until accepted |
 | `axi_mux` | Unbounded, with three ports and with `soc_top`'s two: no READY or VALID in reset; a downstream AW or AR handshake is exactly one port's handshake, with that port's payload and its index in the id's top bits; W beats come only from the port of the oldest AW granted whose beats are not all in; B and R reach the port their id names, with that port's READY; and the downstream VALIDs hold until accepted. Assumes masters that hold their requests until accepted and a slave that answers only bursts it accepted |
 | `cache_mshr_payload` | Per-entry MSHR data and byte strobes equal the reference indexed fill and store merge, including fills that coincide with stores, on every byte that can be read, in a 256-byte cache with 8-byte lines |
-| `coherence_home_select` | Combinational equivalence of nineteen-way circular priority with READY preference and three-seat waiter admission against serial reference selectors |
-| `coherence_home_completions` | Unbounded ownership checks for three identities and two result credits, including distinct live identities, same-sector predecessors (released at U, or at a DMA predecessor's result), held G/U payloads, retry credit return and way pins through U. Parked work keeps its identity and predecessors while releasing image credit. READY work has priority over fresh eligible work. Assumes initial reset and legal worker pin/retry, park and wake events. Cover tasks reach a full result pool and independent completion while other work remains live. The IF-pair cover tracks admission order and reaches a younger G before the older G and a younger U before the older U |
-| `coherence_home` | Unbounded control ownership checks cover three completions, two engines and two fill controls over eight sectors with 32-byte lines and sixteen sectors with 64-byte lines, using one way and zero payload data. An independent scoreboard tracks accepted memory IDs through responses. Assumes initial reset, persistent fatal stop and responses for owed IDs. Unbounded victim checks preserve frozen bytes, address ownership and held memory payloads through B. Victim recall controls have distinct reserved slots. Directed cover traces reach delayed success and error responses. Array and engine byte-value properties have separate unbounded proofs |
+| `coherence_home_select` | Combinational equivalence against serial reference selectors of circular priority with READY preference over twenty positions, the last of which picks a slot it is given, and of three-seat waiter admission over twenty-three slots |
+| `coherence_home_completions` | Unbounded ownership checks for three identities and two result credits, including distinct live identities, same-sector predecessors (released at U, or at a DMA predecessor's result; prefetches neither wait nor order), grants that rotate among the result buffers, held G/U payloads, retry credit return and way pins through U. Parked work keeps its identity and predecessors while releasing image credit. READY work has priority over fresh eligible work. The prefetch slots' place in the work rotation offers an eligible slot whenever it can be picked. `coh_completions_pairs_prove` keeps request addresses in an eight-bit window and checks that a prefetch's no-fill flag covers every live demand for its block. The partition tasks keep one of three slots for prefetches, or two of four, and assume the consumer takes a prefetch slot's G when it is presented; with two, the cover reaches the prefetch rotation passing over an offered prefetch slot. Assumes initial reset and legal worker pin/retry, park and wake events, with no prefetch parked, as the composed home proves. Cover tasks reach a full result pool, independent completion while other work remains live, a prefetch dispatched with no fill and a prefetch slot's G. The IF-pair cover tracks admission order and reaches a younger G before the older G and a younger U before the older U |
+| `coherence_home` | Unbounded control ownership checks cover three completions, two engines and two fill controls over eight sectors with 32-byte lines and sixteen sectors with 64-byte lines, using one way and zero payload data. An independent scoreboard tracks accepted memory IDs through responses. Assumes initial reset, persistent fatal stop and responses for owed IDs. Unbounded victim checks preserve frozen bytes, address ownership and held memory payloads through B. Victim recall controls have distinct reserved slots. Directed cover traces reach delayed success and error responses. `coh_home_control_partition_prove` repeats the 32-byte control proof with one of the three completion slots kept for prefetches. Two bounded tasks check every assertion for 14 cycles from reset with four ways and three fill controls, one of them with the registered tag array; k-induction does not close with four ways. In the same configuration, `coh_home_prefetch_cover` reaches a prefetch allocation, a prefetch that allocates nothing for a block a demand holds, a prefetch fill that gains a demand seat or fails, a prefetch held back by the fill reserve, and a prefetch fill that installs; the last two take more than the bounded tasks' 14 cycles. Array and engine byte-value properties have separate unbounded proofs |
 | `coherence_home_engine` | Unbounded byte-value checks in both line geometries select dirty probe data over the resident snapshot and apply DMA byte enables last. Checks held probe, acknowledgement, update and result payloads. Assumes initial reset, legal dispatch and decision events, and responses to launched array operations. Covers coincident dirty reply/data and failed SC completion |
 | `coherence_home_array` | Unbounded watched-byte preservation across independent read and masked-update ports in both RAM forms. Checks held tag decisions, physical-row hazards and bounded service under continuous read/write contention without tag updates. A held tag-only update has bounded service when the response receiver is ready. The block RAM task watches an arbitrary byte; the registered RAM tasks cover each of the 64 byte lanes. Assumes initial reset, legal ways and claims of available tag decisions. Covers overlap on all three ports |
+| `coherence_prefetcher` | Unbounded checks that each prefetch identity follows its D, G, C and U, that D and C hold until taken, that D is a line-aligned Prefetch of a live identity, and that a stream table's request stays in the page of its stream line. Assumes initial reset and a home that sends one GrantAck per accepted D and a U only after the identity's C. `coh_prefetcher_ids_bmc` checks for 20 cycles that each table's read ids return once and to the right table. Covers reach every identity in flight, the tables taking turns, and a held C |
 | `coherence_dma_ingress` | Four or eight independent request lifetimes preserve opaque IDs until the later of the response and U; each request responds once, a read after its G and a write after its U, and a U's slot that has not responded responds on the next cycle. Requests issue in acceptance order; full keys match reordered grants and releases. The composed arbiters assert their sender hold contracts and captured-payload equality. Reset clears all ownership. `coh_dma_ingress_soc_prove` proves eight credits; `coh_dma_ingress_soc_cover` fills the queue, wraps both pointers, drains every credit, and reuses an ID both with and without other requests in flight. Its cover driver uses writes with matching G and U packets; the proof assumes initial reset and aligned requests |
 | `coherence_control` (`coh_reader_*`, `coh_ptw_reader_*`, `coh_ingress_prove`) | IF slots 0 and 1 and the PTW class register one data/error response per G and hold their identity through U. Default readers and source-2 line bridges respond after U. Payloads and reader IDs remain associated under D/C stalls; response debt forbids duplicates. Covers exercise errors, stalled completion tails, fatal stop and reset in each active phase. Assumes initial reset, aligned requests and read-only hart requests. Early readers assume a valid G for their waiting q carries the demand's address, as checked by the home completion target. The maintenance composition asserts this address contract at the bridge without that assumption |
-| `coherence_control` (`coh_arbiter_prove`, `coh_arbiter19_prove`) | Captured payloads equal the selected input at each valid presentation. Selection matches circular priority at three and nineteen inputs. Assumes initial reset and held input payloads until acceptance |
+| `coherence_control` (`coh_arbiter_prove`, `coh_arbiter23_prove`) | Captured payloads equal the selected input at each valid presentation. Selection matches circular priority at three and twenty-three inputs. Assumes initial reset and held input payloads until acceptance |
 | `coherence_endpoints` | Unbounded held-payload, identity lifetime, completion ordering, keyed cancellation, and fatal-data retention properties for the request, home, PutM, and queue endpoints. Assumes initial reset, held service results under backpressure, and masked ordinary W selection after absorption. Cover tasks reach ordinary completion and absorbed cancellation. The wide home task uses 56-bit addresses and 16 fill identities. These are endpoint safety proofs, not a proof of a cache coherence sequencer or arbitration progress |
 | `coherence_control` (`coh_c_payload_prove`, `coh_c_payload_wide_prove`) | Completion payload equality outside reset at 50 and 74 bits with arbitrary phase selections and payloads. No one-hot or peer assumption is imposed. Endpoint tasks separately check phase-selection and channel-valid qualification |
 | `coherence_control` (`coh_atomic_select_prove`, `coh_atomic_select_wide_prove`, `coh_atomic_pair_prove`, `coh_atomic_pair_wide_prove`) | Arbitrary-input atomic source qualification and unbounded equality of guard active state, retired state and active tags at five and nine tag bits. The paired guards assume first-edge reset. Invalid candidate tags are unqualified |

formal/coherence_control.sby

@@ -6,7 +6,7 @@ coh_atomic_pair_wide_prove arm_pair arm_pair_wide
 coh_c_payload_prove payload
 coh_c_payload_wide_prove payload payload_wide
 coh_arbiter_prove arbiter
-coh_arbiter19_prove arbiter large_arbiter
+coh_arbiter23_prove arbiter large_arbiter
 coh_arbiter_held_prove arbiter large_arbiter held_arbiter
 coh_reader_prove reader early
 coh_reader_cover reader early covers
@@ -52,7 +52,7 @@ arm_pair: prep -flatten -top coherent_atomic_select_formal
 payload_wide: chparam -set WIDTH 74 coherence_c_payload
 payload: prep -top coherence_c_payload
 arbiter: chparam -set WIDTH 12 -set PORTS 3 coherence_d_arbiter
-large_arbiter: chparam -set PORTS 19 coherence_d_arbiter
+large_arbiter: chparam -set PORTS 23 coherence_d_arbiter
 held_arbiter: chparam -set HOLD_VALID 1 coherence_d_arbiter
 arbiter: prep -top coherence_d_arbiter
 dma: chparam -set SOURCE 2 -set PORT_CLASS 3 -set ID_BITS 4 coherence_line_bridge

formal/coherence_home.sby

@@ -1,52 +1,68 @@
 [tasks]
-coh_home_control_prove control
-coh_home_control64_prove control wide
+coh_home_control_prove control ctl
+coh_home_control64_prove control ctl wide
+coh_home_control_partition_prove control ctl partition
+coh_home_control4_bmc bmc4 ctl four
+coh_home_control4_ultra_bmc bmc4 ctl four ultra
 coh_home_wb_prove wb unit
 coh_home_victim_cover covers
 coh_home_error_cover covers error
+coh_home_prefetch_cover pfcover ctl four
 
 [options]
 control: mode prove
 control: depth 2
+pfcover: mode cover
+pfcover: depth 20
+bmc4: mode bmc
+bmc4: depth 14
 wb: mode prove
 wb: depth 4
 covers: mode cover
 covers: depth 180
 timeout 180
 control: timeout 600
+bmc4: timeout 1200
+pfcover: timeout 1200
 
 [engines]
 control: smtbmc boolector
+pfcover: smtbmc boolector
+bmc4: smtbmc boolector
 wb: smtbmc boolector
 covers: smtbmc boolector
 
 [script]
 read -formal -sv coherence_seat_select.sv coherence_work_select.sv
 read -sv cache_perf_pkg.sv
 error: verilog_defines -D COHERENCE_HOME_COVER_ERROR
+pfcover: verilog_defines -D COHERENCE_HOME_PREFETCH_COVER
 read -sv coherence_pkg.sv
-control: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_home_endpoint.sv
+ctl: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_home_endpoint.sv
 wb: read -sv coherence_home_endpoint.sv
 covers: read -sv coherence_home_endpoint.sv
-control: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_d_arbiter.sv
+ctl: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_d_arbiter.sv
 wb: read -sv coherence_d_arbiter.sv
 covers: read -sv coherence_d_arbiter.sv
-control: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_home_completions.sv
+ctl: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_home_completions.sv
 wb: read -sv coherence_home_completions.sv
 covers: read -sv coherence_home_completions.sv
-control: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_home.sv coherence_home_control_harness.sv
+ctl: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_home.sv coherence_home_control_harness.sv
 wb: read -formal -sv -D SYNTHESIS -D COHERENCE_HOME_WB_PROOF coherence_home.sv
 covers: read -formal -sv -D COHERENCE_HOME_WB_PROOF -D COHERENCE_HOME_COVER coherence_home.sv coherence_home_harness.sv
 read -sv sdp_block_ram.sv sdp_packed_tag_uram.sv sdp_ram_byte_en.sv
-control: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_home_array.sv
+ctl: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_home_array.sv
 wb: read -sv coherence_home_array.sv
 covers: read -sv coherence_home_array.sv
-control: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_home_engine.sv
+ctl: read -formal -sv -D COHERENCE_HOME_CONTROL coherence_home_engine.sv
 wb: read -sv coherence_home_engine.sv
 covers: read -sv coherence_home_engine.sv
-unit: chparam -set CACHE_BYTES 128 -set WAYS 1 -set ULTRA 0 -set COMPLETIONS 2 -set RESULTS 2 -set FILLS 2 coherence_home
+unit: chparam -set CACHE_BYTES 128 -set WAYS 1 -set ULTRA 0 -set COMPLETIONS 2 -set RESULTS 2 -set FILLS 2 -set PREFETCH_SLOTS 0 coherence_home
 wide: chparam -set LINE_BYTES 64 -set WAYS 1 coherence_home_control_harness
-control: prep -flatten -top coherence_home_control_harness
+four: chparam -set WAYS 4 -set FILLS 3 -set PREFETCH_RESERVE 1 coherence_home_control_harness
+ultra: chparam -set ULTRA 1 -set PREFETCH_RESERVE 0 coherence_home_control_harness
+partition: chparam -set PREFETCH_SLOTS 1 coherence_home_control_harness
+ctl: prep -flatten -top coherence_home_control_harness
 unit: prep -flatten -top coherence_home
 error: chparam -set FAIL_B 1 coherence_home_harness
 covers: prep -flatten -top coherence_home_harness