Repository navigation
Add L2 fills and a stream prefetcher to the coherent home - #147
Merged
Merged
Conversation
…home The home had four fills and no prefetcher, so streaming code waited on one demand miss after another. Give the home L2_NUM_MSHR fills (1 to 16, eight by default, as the X3 already sets) and a prefetcher at source 3. coherence_prefetcher watches the hart requests the home accepts, from a registered copy of its D acceptance: a data table of four streams sees GetS, GetM and LoadReserved, an instruction table of two streams sees ReadOnce.IF refills. It owns four prefetch identities, presents each request from a D register, takes every source-3 G when it arrives, and loads new requests only while the home reports room for a prefetch fill. l2_stream_prefetcher gains the load enable this needs. The home looks a Prefetch up once and answers GrantAck. A resident line takes no pin, probe, read or update. An absent line gets a fill with no seat only if more than a quarter of the fills stay free, two ways of the set are available, a valid victim finds two free write-back slots, and no hart or DMA request for the block was live before the prefetch's dispatch; otherwise the prefetch completes having done nothing. A prefetch never retries, joins or waits for a fill, its engine protects no victim, it hands its sector on at its result, and it never makes a PutM wait. Demand readers take the seats of a prefetch fill and wake at its install. completion_count becomes 11*H+12: the completion table keeps four slots for the prefetch identities, so neither kind waits for the other's capacity. Those slots capture their G without G readiness, which the cluster holds set for source 3. W readiness reads one registered reduction of the fill and write-back blocks, so its depth does not grow with the fill count. Checks: the home, completion table, endpoint, cluster and stream table benches; DDR hello_world, CoreMark and ddr_bench; lint.
The completion table picked the next grant among its slots and then looked up the slot's result buffer, so the pick and its payload grew with the slot count. Rotate the grants over the eight result buffers instead: each buffer marks a ready result, the pick selects the buffer's payload directly, and the payload's tid names the slot. Rotation stays fair, now in buffer order. A prefetch changes nothing a client sees, so it no longer takes a place in the per-sector order: it neither waits for earlier requests of its sector nor holds later ones back, and the order matrix covers only the hart and DMA slots. DMA results still hand their sector on. The prefetcher takes every source-3 U when it arrives, as it takes G, and returns a table's read id only for the matching identity. Its D register loads only when empty, so its load does not wait on D readiness. The put selection no longer waits for the stop condition, which W readiness already includes, and the no-fill flag is set afresh at admission. Add the invariants the home proofs need for prefetches: a live slot holds a legal request, every tag owner is the lookup in service, the lookup's prefetch flags belong to its owner, a busy engine serves its slot's opcode, a looking-up engine has no error, and prefetches are never parked, woken or seated. The stream table proves that a request stays in the page of its stream line. Checks: the home (both line sizes), completion table and cluster benches; the completion table proofs, with and without the full address range.
The home bench takes every source-3 G when it is presented, as the prefetcher does, and its take_grant leaves those grants alone. New home cases: a Prefetch fills an absent line with no seat and leaves a resident one without a read, probe or pin; a demand read waits on a Prefetch's fill; Prefetches keep the fill reserve, the last available way and, for a valid victim, the last write-back slot; a failed Prefetch fill frees and reports the error to a joined read; Prefetches beside DMA writes and reads change no bytes; a PutM proceeds beside live Prefetches of its sector; and a demand miss replaces a line while Prefetches of every way of its set are live. The completion table bench fills both slot partitions, checks the no-fill flag against live demands of the block, and checks that a Prefetch neither waits for nor orders its sector and never holds a PutM. The cluster bench runs Prefetches through the agent port, which now carries sources 2 and 3, beside lines the L1D holds Modified. The single-hart endpoint bench recognizes the 23-slot layout. Checks: the home benches at both line sizes, the completion table, cluster (one and three L1D endpoints), endpoint and stream table benches.
The completion table proof gains a task that keeps request addresses in an eight-bit window and checks the pairwise no-fill invariant, and partition tasks with one of three slots kept for prefetches, assuming the consumer takes that slot's G when presented. The selector and arbiter proofs move from 19 to 23 inputs, the table's slot count. The home's control harness takes the fill count, the fill reserve and the tag array form as parameters. Two bounded tasks check every home assertion for 14 cycles from reset with four ways and three fills, one of them with the registered tag array; k-induction does not close with four ways. A cover task in the same configuration reaches a prefetch allocation, a prefetch that allocates nothing for a block a demand holds, prefetch fills that gain a demand seat, fail and install, and a prefetch held back by the fill reserve. coherence_prefetcher.sby proves the prefetcher's identity lifetimes, held D and C, line-aligned requests and page-bounded table requests against a home that sends one GrantAck per accepted D and a U only after C, checks the tables' read ids for 20 cycles, and covers every identity in flight, the tables taking turns and a held C. Checks: all registered tasks of coherence_home, coherence_home_completions, coherence_home_engine, coherence_home_array, coherence_home_select, coherence_control, coherence_endpoints, coherent_hart_cache and coherence_prefetcher pass.
The cache README describes how an idle grant register takes the next waiting result in rotation over the result buffers, and lists the prefetch cases of the home and cluster benches and the stream table's disabled case; the tests README lists them too. The home bench case of prefetches beside DMA writes and reads is renamed for what it checks, since prefetches no longer order other requests.
The completion table's result buffer lifetime and readiness, and each slot's result and buffer ownership flags, now take G readiness as their last term. Kept nodes hold each next state without the grant, and the presented grant's slot and buffer come from decodes of the grant registers instead of the endpoints' G valid and the slot's buffer index. An assertion ties the slot decode to the endpoints' G valid. The buffer lifetime reference check applies outside reset, since the grant registers meet the invariants the decodes rely on only after reset. The table's behavior is unchanged: the completion table bench runs the same cycles.
The work selector ranked all 23 completion slots. It now ranks twenty positions: one for each hart or DMA slot, and one after them for the four prefetch slots. That position offers a prefetch slot registered on the previous cycle, chosen in rotation among the prefetch slots and leaving out the slot being dispatched and any slot parked on that edge, so every selector input is a register. A selection needs an idle selector, which follows a dispatch by a cycle, so the offered slot is eligible whenever it can be picked; a simulation and proof assertion checks this. coherence_work_select's last input can now yield a given slot number in place of its index. A prefetch reaches an engine a cycle later than before, and at most one prefetch is picked per turn of the rotation; hart and DMA slots keep their order. The home parks no prefetch, so the prefetch position is never READY; the standalone completion-table proof now assumes this, as the composed home proof asserts. The selector proof runs the twenty-position form with a coded last input. coh_home_control_partition_prove repeats the composed home control proof with one of its three completion slots kept for prefetches.
D readiness was the OR, over the 23 completion endpoints, of each idle endpoint's admission check, which since the prefetch partition includes the endpoint's class. It now takes the same checks once from the request (legal identity and opcode, epoch, source and alignment) beside the duplicate check and the free-slot summary of the request's partition. The existing assertion that D readiness equals the chosen free endpoint's own readiness holds the two forms equal. Checks on this commit and the two before it: the completion table proofs, the selector proofs and every coherence_home task including the new partition task pass; the completion table, home (both line sizes) and cluster benches pass, with and without three L1D request endpoints, and so does DDR hello_world.
coh_completions_partition2_prove runs the completion table proof with four slots, two of them kept for prefetches, so the prefetch slots' rotation behind their shared place in the work rotation is under proof; it passes in about 190 s. Its cover task reaches the rotation passing over an offered prefetch slot. The other tasks keep three slots.
The prefetch work offer left out a prefetch slot parked on the same edge, which made the registered choice depend on the home's park decision. The home parks no prefetch, which its composed proof asserts and the standalone completion-table proof assumes, so the offer now reads only registers: the slots' eligibility and the current selection. Behavior is unchanged.
A prefetch slot holds only Prefetches, and a Prefetch never takes a fill seat, so each fill's seat selector now sees a constant zero for the prefetch slots instead of their waiting offers. The selectors rank only the hart and DMA slots, and the prefetch slots are never parked or woken by construction. Behavior is unchanged.
U readiness depends on the clients' own comparisons with the presented release. The completion table's predecessor matrix, handed flags and READY flags now take it as their last term: kept nodes hold each next state without a release on the edge (admission of a new request, DMA handoff, dispatch and wake included), and the release clears its column or slot last. READY state moves to a per-slot block for this. Behavior is unchanged. Checks on this commit and the two before it: all coherence_home_completions tasks pass; the completion table, home (both line sizes) and cluster benches, with and without three L1D request endpoints, and DDR hello_world pass with the same simulated times as before.
The held put address, which the put-blocking comparisons and the completion table's sector checks read one cycle ahead, took the incoming W's address only while W was valid. An idle put selection now offers the incoming W's address whatever W's validity: a W that is not valid leaves no put selected on the next cycle, and W readiness and the put sector checks use these comparisons only for a selected or just-accepted put. The fill and write-back owners reduce as one vector. The reference checks of the held address apply when it is the selected put's. W readiness is unchanged.
A result's match selected its slot's state, identity and address by the result's tid and compared them once. Each slot now compares the result with its own tid, state, identity and address, and the slot matches reduce through kept nodes of at most six; a DMA result's handed flag is set from its slot's match. Result acceptance is unchanged.
Each candidate of the work selector's four priority classes is now a kept node, one LUT of the slot's inputs, so the group summaries and priorities above it form a fixed tree. Selection is unchanged.
Each completion slot's result match is now two kept terms, the address comparison and the tid, state and identity comparison, which meet in one node, so the identity terms do not follow the address comparison. Result acceptance is unchanged.
Each completion slot's issue, error, wake error, count and pin flags now join READY in a per-slot block whose next states hold every other event of the edge and apply the slot's release last; a wake, a count and a pin on the release edge take effect over it, as before. Behavior is unchanged.
A release fired from the endpoints' U valid and the release arbiter's reset-gated U readiness. The completion table now forms it from the kept release candidates, which already exclude reset since an endpoint offers U only outside reset, and U readiness directly; the predecessor clear flags select their release case by U readiness alone, as reset sets them. An assertion ties the release to the arbiter's handshake. Behavior is unchanged. Checks on this commit and the five before it: all coherence_home_completions and coherence_home tasks pass; the completion table, home (both line sizes) and cluster benches, with and without three L1D request endpoints, and DDR hello_world pass with the same simulated times.
The overview gives the home's eight fills and its prefetching of data and instruction streams. The roadmap no longer lists four fills and a missing stream prefetcher among the costs of the coherent path, and its memory system paragraph gives the home's fill count and the prefetcher's requests in place of the plan to add them.
Preserve confirmed instruction streams for refills within their backward distance window. Other observations can allocate entries and train forward streams; data-stream allocation uses the default policy. Give demand and PutM lookups priority over unselected prefetches at the home tag arbiter. Preserve selected requests through backpressure. Exercise distance boundaries, page-offset carry, response identity, held tag requests and finite contention. Verify the prefetcher, home, completion and selection proofs, cache benches and lint checks.
Keep instruction entries within a page-bounded window of twice the prefetch distance. Preserve tentative entries and confirm them on a successor observation. Allow farther-back refills to replace entries. Use round-robin tag selection in the home. Share page and offset comparisons in the instruction filter. Cover tentative entries, window boundaries, page-end refills, held request identities and data-table behavior. Verify coherence proofs, cache benches, lint, fast Python tests and synthesis checks.
Capture the LR set decision and reservation clear decision separately from held validity. Combine their registered values with clear priority to preserve the reservation on the same response edge and across commit-time branch recovery. Check the full reservation recurrence, reset, recovery and clear priority in the local proof. Exercise clears on the LR response edge and the following two edges in the load-queue bench. Validation: both load-queue benches pass 93 cases, the coherent LQ cut proof passes, and lint and fast Python tests pass.
Reduce pending offers through the arbiter's held one-hot selection. Captured-valid arbiters use their held valid bit. Selection, payload, priority and acceptance cycles are unchanged. Assert the live offer against the indexed reference beside the held selection invariant. Document the read-offer selection in the cache README. Validation: lint and the three-port, twenty-three-port and held-valid arbiter proofs pass.
Project the ROB tag and writeback hint for each prepared CDB-validity case, then select the live case. Selection priority, issue permission and capture cycles are unchanged. Compare both fields with the direct expressions in local and runtime assertions. Enable writeback-hint tracking in the integer control proof and document the metadata selection. Validation: all five control proofs, the hint-enabled integer proof, 42 reservation-station cases, two shift cases, lint and fast Python checks pass.
Compute lookup-history and wait-flag updates for both allocation-valid values before selecting the live value. Keep allocation clear priority, wait attachment priority and synchronous reset on their original edges. Endpoint payload capture and performance-event sampling are unchanged. Assert the registered flag recurrences and describe the allocation priority in the cache README. Validation: eleven L1D cases, twenty-nine cluster and reader cases, lint and fast Python checks pass.
Reduce masked live offers within four-port groups, then combine their outputs. Keep each group boundary explicit and use zero group values for captured-valid arbiters. Selection, payload, priority and handshake cycles are unchanged. Describe the grouped selection in the cache README. Validation: three-port, twenty-three-port and held-valid arbiter proofs, 115 cache bench cases, lint and fast Python checks pass.
Describe the configured home fills and stream prefetching alongside streaming DMA placement in the cache module table and architecture diagram.
Exercise a streaming miss while way zero is pinned and a prefetch fill owns another way. Check progress in an unrelated set, completion after release, way-zero placement, and a streaming hit on the prefetched line. Describe the coherent home's prefetch configuration and counter events in the performance model and counter reference. Checks: both home line-size benches and lint.
Make the sized cast the explicit operand of the complement. The streaming mask leaves way zero eligible and excludes every higher way. The mask is zero for a one-way home. Checks: four-way home control BMC, both home line-size benches, and lint.
Store the primary opcode in a two-write register bank when effective operand capture is enabled. The issue mask reads the opcode while the grouped RAMs supply the other payload fields. Compare split storage with the full payload RAM, assert mask/index identity for prepared selectors, and exercise primary issue through stalls, row reuse and flushes in the shift-amount bench. Verified with the storage and selector proofs, reservation-station benches, randomized startup, lint and fast Python tests.
Collaborator
|
Could you check the latencies used by default for the DDR runs in the sim, I think these are overly lower than reality for a Soc level DDR, (even if the whole path is sync with no CDC - which for most designs won't be) |
Collaborator
Author
|
By default, the simulation's DDR model answers 30 CPU cycles after a request reaches the SoC's DDR port ( That is low for a slower SoC fabric with a clock crossing, or for DRAM a hundred or more cycles away. Next steps:
Results will follow here. |
adambagley
added a commit
that referenced
this pull request
Nov 5, 2026
…ip ci] The primary opcode store from #147 is a coherent_rs_payload_store, whose registers start at zero. With it in the bmc8 and bmc16 configurations, rs_issue_clear's check that the design has no initial-state constraints failed. The proof already holds whatever the payload RAMs return, initial contents included, so the payload stores are now treated the same way: their file is not read and their instances are deleted, which leaves their outputs free. All five rs_issue_clear tasks pass.
Collaborator
Author
|
Follow-up on the DDR model latency. Calibration. Fitting ddr_bench's latency-bound kernels (sequential, random, chase, copy, write) on hardware against the simulation puts the X3's DDR at about 80 cycles of model latency at the X3's CPU clock. The default of 30 is low, so we'll look at raising it. This PR's change with a higher latency (cycles, ddr_bench in simulation):
random_read, record_read and chase are unchanged, within about 1%. |
Collaborator
|
This will give a better baseline regards balancing level of outstanding needed to keep pipeline humming along...
My soc has an async cdc around the cpu-top for dvfs so even more latency :(. But hoping can recover through adaptive clock/power to chase the actual silicon speed and corner at current junction temp...
DFS on fpga may even give a few more mhz, waiting on the build..
…________________________________
From: Adam Bagley ***@***.***>
Sent: Thursday, 05 November 2026 18:03:53
To: twosigma/frost ***@***.***>
Cc: John Goodacre ***@***.***>; Comment ***@***.***>
Subject: Re: [twosigma/frost] Add L2 fills and a stream prefetcher to the coherent home (PR #147)
[https://avatars.githubusercontent.com/u/123022216?s=20&v=4]adambagley left a comment (twosigma/frost#147) [github.com]<https://urldefense.com/v3/__https://github.com/twosigma/frost/pull/147*issuecomment-6665413030__;Iw!!PDiH4ENfjr2_Jw!GkEC0VwWud9toQZMWqMdPqdpjtlSfYQ1kHxTWFBn0jkGRRkVmC7GGLNhZf0dDsizutPkdKHPrpzJUyWWvkzDcmDRbnQscq-zwYw$>
Follow-up on the DDR model latency.
Calibration. Fitting ddr_bench's latency-bound kernels (sequential, random, chase, copy, write) on hardware against the simulation puts the X3's DDR at about 80 cycles of model latency at the X3's CPU clock. The default of 30 is low, so we'll look at raising it.
This PR's change with a higher latency (cycles, ddr_bench in simulation):
Kernel or program Latency 30 Latency 100 Latency 200
seq_read -21.8% -46.3% -62.1%
stride_read -19.3% -33.2% -34.9%
copy -19.2% -34.2% -45.8%
write -22.3% -38.9% -51.5%
streams_read -8.2% -13.3% -23.1%
DDR CoreMark -1.3% -3.2% -5.7%
random_read, record_read and chase are unchanged, within about 1%.
—
Reply to this email directly, view it on GitHub [github.com]<https://urldefense.com/v3/__https://github.com/twosigma/frost/pull/147?email_source=notifications&email_token=BUPXPLAOB75ZIWYSLM73G335XS6ITA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTMNRWGU2DCMZQGMYKM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJLDGN5XXIZLSL5RWY2LDNM*issuecomment-6665413030__;Iw!!PDiH4ENfjr2_Jw!GkEC0VwWud9toQZMWqMdPqdpjtlSfYQ1kHxTWFBn0jkGRRkVmC7GGLNhZf0dDsizutPkdKHPrpzJUyWWvkzDcmDRbnQsfiq1XuI$>, or unsubscribe [github.com]<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/BUPXPLEEJ4UIJSZBLARYZAD5XS6ITAVCNFSNUABGKJSXA33TNF2G64TZHMYTCMRZGMZDIMJUGM5US43TOVSTWNRSGI2DKMZYHEZDNILWAI__;!!PDiH4ENfjr2_Jw!GkEC0VwWud9toQZMWqMdPqdpjtlSfYQ1kHxTWFBn0jkGRRkVmC7GGLNhZf0dDsizutPkdKHPrpzJUyWWvkzDcmDRbnQsMm9lxig$>.
You are receiving this because you commented.Message ID: ***@***.***>
|
adambagley
added a commit
that referenced
this pull request
Nov 5, 2026
#147's simulation check compared the primary opcode store with a reference RAM on every issue while reset was deasserted. With a random start, the first clock edge can arrive before the testbench drives reset, with random issue state, so the check fired at time zero and riscv-torture failed every test under main's CI random-start seed. The check now also waits for reset_seen_q, as the other simulation checks in this file do. Synthesis and formal builds do not include it.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The coherent home gets
L2_NUM_MSHRfills, eight by default, with a quarter kept for demand misses. It also gets a stream prefetcher at its own source:The branch also regroups several select and readiness terms in the home, the completion table and the reservation stations, without changing behavior. It parenthesizes the streaming way mask cast, which Yosys parsed differently from the other tools.
README.md, ROADMAP.md and the cache README describe the home's fills and prefetcher.
Against main, in simulation:
The completion-table, home, prefetcher, reservation and selector proofs pass. So do the home, cluster and endpoint benches, TestRIG, the program set, lint and the fast tests.
Supersedes #135.