# proposal/17-memory-model.md · versecafe/strata [View on GitCafe](https://git.cafe/versecafe/strata/blob/5fb00970716bc51374501a76d6d4080f218142c3/proposal/17-memory-model.md) Repository: [versecafe/strata](https://git.cafe/versecafe/strata) Visibility: public Requested revision: 5fb00970716bc51374501a76d6d4080f218142c3 Requested commit: 5fb00970716bc51374501a76d6d4080f218142c3 Commit: 5fb00970716bc51374501a76d6d4080f218142c3 Blob: 221ee7a682e4c73758e5cd426efa899b1f47f427 Size: 17532 bytes [Immutable source](https://git.cafe/versecafe/strata/blob/5fb00970716bc51374501a76d6d4080f218142c3/proposal/17-memory-model.md?format=markdown) ``` # Memory Model What `mem` means: the storage class it adds beyond `reg [T; N]`, its read/write timing, port count, indexing safety, and which compiler stage owns which piece. Principles in force: P-1 (no implicit behavior — a memory read's latency is not folklore), P-3 (meaning survives lowering — the `Memory` architectural node stays recognizable to the CIRCT boundary), P-5 (canonical architectural nodes, not primitive soup), D-030 (representation types), D-037 (width-algebra closure for `DEPTH`). ## Committed design ### 1. `mem` is a storage class over the existing array type, not a new `Type` (D-092) `TypeKind::Array { element, length }` already exists in `strata-hir` (`crates/strata-hir/src/lib.rs`) and is already exercised by two different storage forms in the fixture corpus: `reg gens: [Generation; TXN_ENTRIES] reset(all(0));` (`epoch_soc.strata`) and `mem buf: [T; DEPTH];` (`fifo.strata`, `cdc_bridge.strata`, `epoch_soc.strata`). `strata-check` already type-checks indexed reads against it (`fn index`, `crates/strata-check/src/lib.rs`, ~2836): the base must be `TypeKind::Array`, and the index must equal `Index`. This settles one of the four open questions immediately — **no new `Type` variant is needed.** `[T; N]` is the one array type in the system; `reg` and `mem` are two different storage-class declarators over it, exactly the way `reg`/`mem`/(implicitly) `let` already differ by declarator keyword, not by type. What's missing is downstream of parsing, on every stage from HIR onward: `MemStmt` parses (`crates/strata-syntax/src/parser.rs::mem_stmt`, `mem name: [T; N];`, no `reset(...)` clause — matching every fixture, since memories don't reset per-element) but has no HIR item, no `strata-check` handling, no arch-IR node, and no CIRCT lowering. `07-compiler-architecture.md` §1 already lists `Memory` among the canonical architectural nodes that must survive to the Architectural→Structural boundary; this decision is what finally defines that node's contents. Indexed read/write syntax needs no changes either. `IndexExpr` (`buf[rd_ptr]`) and the `<-` next-cycle write form applied to an indexed target (`buf[wr_ptr] <- item;`) already parse today, reusing the same production as `reg`-array indexing and the existing `reg name <- expr;` update form (D-079) respectively. The fixtures already assume exactly this: `fifo.strata`'s `buf[wr_ptr] <- item;` next to `reg`-style `wr_ptr <- wr_ptr.incr_wrap();`, and `epoch_soc.strata`'s `entries[slot] <- st;`. Nothing new is required at the syntax layer. ### 2. Read semantics: registered by default; no combinational `mem` form in v0 **Decision: `mem` reads are registered — the value at `buf[idx]` reflects the address as sampled at the clock edge, visible one cycle after the read fires, not combinationally in the same cycle.** Rationale: - Real memory primitives are synchronous. Every FPGA block-RAM primitive (Xilinx `RAMB36`/`RAMB18`, Intel M20K/M10K) is clocked on the read side; there is no vendor block-RAM configuration with a purely combinational (unclocked) read. The only combinational-read storage a synthesis tool can produce is LUT-based distributed RAM, which is area-expensive per bit and doesn't scale — it's a flop-array-with-a-mux by another name. - `reg [T; N]` already gives Strata a fully combinational-read array (an actual bank of `seq.firreg`s with a read mux) today, in principle, once `reg`-array indexing is lowered. If `mem` also read combinationally, it would be semantically redundant with `reg [T; N]` — the entire reason to add a second storage class is to reach a construct that maps onto a memory macro rather than a flop bank, and that construct is inherently 1-cycle-latency on read. - D-005 (FPGA-first, ASIC-clean) makes this the load-bearing case: the two examples that motivate this decision — FIFOs deeper than hand-inlined depth-4, and indexed transaction tables — are exactly the designs where flop-array storage stops being viable and BRAM-class storage is the point. **Consequence for the existing corpus.** `fifo.strata`'s current body reads `buf[rd_ptr]` and uses the result (`head`) in the same cycle to drive the FIFO's `Producer` output — a combinational-read assumption. That body will need a one-cycle rework (present the read address a cycle ahead, or add an explicit output/skid stage) once `strata-check` actually enforces `mem` timing. This is expected fallout, not a regression: `mem` currently has zero downstream semantics, so nothing enforces the fixture's assumption today, and it was written before this decision existed. `cdc_bridge.strata`'s two mem accesses (`buf[wr_gray...] <- item` in `'src`, `buf[rd_gray...]` in `'dst`) need the same adjustment; `epoch_soc.strata`'s `TxnTable.lookup` already reads `entries[slot]` in a separate `port` call from the `alloc` write, so it isn't assuming same-cycle round-trip and needs no rework. **Timing vocabulary reuse.** A registered `mem` read is structurally the same shape D-013's `later` modality already exists to type: a value that becomes visible on the next clock edge relative to when it's driven. Rather than inventing a second next-cycle-value mechanism alongside `later`, a `mem` read's result type should be modeled through the same guarded-feedback vocabulary the checker already has for register-adjacent next-cycle values, giving `strata-check` one timing judgment to maintain instead of two. **Both forms eventually.** North star, not v0: a declared combinational-read form for small `mem` instances (effectively a checked alias for "back this with LUTRAM, not BRAM") may be worth adding once there's a real workload that needs zero-latency indexed storage bigger than a hand-written `reg [T; N]` is comfortable expressing. Deferred rather than designed now, per D-003's two-track rule — v0 should not carry a bifurcated read-timing surface until a concrete design needs it. Until then, `reg [T; N]` remains the answer for combinational-read indexed storage. ### 3. Port count: one read port and one write port, usable concurrently **Decision: v0 `mem` supports exactly one read port and one write port, both usable in the same cycle** — i.e. a simple-dual-port memory, the smallest primitive that is not a strictly weaker case of "single-port" (address-shared, read-XOR-write-per-cycle) memory. This floor is not a simplicity choice; it's forced by the flagship fixture. `fifo.strata`'s `Fifo` can push and pop in the same cycle (full-throughput operation — nothing in its contract or body serializes push against pop), which means `buf[wr_ptr] <- item` and `buf[rd_ptr]` (a different address whenever `occupancy < DEPTH`, which the FIFO's own `occupancy_bounded` guarantee establishes) must both be able to fire on one clock edge. A literal single shared port would make the canonical example inexpressible. Simple-dual-port is also the standard FPGA BRAM configuration for exactly this pattern (independent read and write addresses, one clock, no read/write arbitration needed), so it costs nothing beyond what the target already offers. Out of scope for v0: more than one read port or more than one write port (true multi-port memories, e.g. register files needing 2R1W). `MemoryController`'s `const BANKS: Nat1 = 1` parameter in `mem_ctrl.strata` hints at a banking story for exactly this need — banking (N independent single-port or simple-dual-port memories addressed by a bank-select slice) is the cheap way to get effective multi-porting without a new primitive, and is the natural north-star extension rather than a true multi-port `Memory` node. ### 4. Indexed write semantics and bounds: `Index` proves it, no new machinery **Decision: both read and write indices accept any `Index`-typed value, compile-time constant or runtime (register, wire, computed) — no restriction to constant indices, and no separate bounds-check pass.** `Index` (D-030) already means "values in `[0, N)`" by construction; nothing outside that range is representable in the type at all, and `strata-check`'s existing `fn index` helper already requires the index type to equal `Index` (Tier-1 entailment subsumption handles the case where a narrower `Index` is offered where a wider `Index` is expected, per `02-type-system-core.md` §4). Out-of-bounds indexing is therefore not a runtime concern to design a check for — it's a type error at the use site if the index type doesn't unify with the array's length, exactly like `UInt` width checking already works elsewhere in this codebase. The width-algebra closure rule (D-037) covers `DEPTH` itself: it must be `Nat1` (or carry `>= 1`) for the same reason register-depth and FIFO-depth parameters already do (`02-type-system-core.md` §4 point 3), which is why every fixture already spells `const DEPTH: Nat1`. This directly rejects the "compile-time-constant-index-only writes" option that a narrower reading of the FIFO-blocking problem might suggest. `fifo.strata`'s `buf[wr_ptr] <- item;` and `epoch_soc.strata`'s `entries[slot] <- st;` both index with a runtime register value (`wr_ptr`, `slot` from `priority_encode`), not a compile-time constant — restricting v0 writes to constant indices would make the two motivating fixtures uncheckable under this decision while buying no additional safety, since `Index` already proves the bound. There is nothing left for a constant-index restriction to protect. Same-cycle same-address hazard (`mem` read and write on the same index in the same cycle, on the two concurrent ports from §3) is fixed, not user-configurable, in v0: **the read returns the pre-write (old) value** — a `READ_FIRST`-style default, matching a common BRAM configuration and giving deterministic, simulatable behavior without demanding new-value forwarding logic. `fifo.strata`'s own occupancy contract already prevents `rd_ptr == wr_ptr` from mattering on a live push+pop cycle when the FIFO is neither empty nor full, so this default is not observed by the corpus today; a `no_same_address_hazard`-style advisory check is a plausible north-star lint, not a v0 requirement. ### 5. Const generics: `DEPTH` flows through the same `ConstExpr` machinery already in place A `mem`'s length is an ordinary `ConstExpr` inside `TypeKind::Array` — the same representation already used for `reg [T; N]` and for every generic component's `const DEPTH: Nat1` parameter (`Fifo`), and the same body-const-generic resolution that just landed (`f5c2d9e`, "Add expected-type literal inference, body const generics, Local lowering") already resolves `DEPTH` references inside a component body. Nothing mem-specific is needed here: a `mem` declaration's length is checked exactly like an array-typed `reg`'s length is checked, because it's the same `TypeRef::Array` node. ### 6. Pipeline ownership - **`strata-syntax`.** No changes. `MemStmt` (`mem name: [T; N];`) and indexed-read/write expressions already parse correctly and are already exercised by three fixtures. - **`strata-hir`.** Add a `Memory` item (name, `TypeRef` restricted to `TypeKind::Array`, span, no reset expression) structurally paralleling how `RegStmt` becomes a register item today. No change needed to `ExprKind::Index` — it already exists and is shared with `reg`-array indexing. - **`strata-check`.** Three jobs: (a) type-check the `mem` declaration itself (array element type, `Nat1`/positivity obligation on the length per D-037, reject a `reset(...)` clause if one appears); (b) promote the existing `fn index` Ty-computation into a real `CheckedExprKind::Index { base, index }` (today it returns a `Ty` for diagnostics but has no checked-IR representation to hand to lowering — this gap exists for `reg`-array indexing too and should be fixed once, generically); (c) type the *result* of a `mem`-backed index expression as one cycle delayed relative to a `reg`-backed one, via the `later`-modality machinery from §2, and check indexed-write targets (`buf[idx] <- v`) the same way `RegUpdate` targets are resolved today, generalized from a bare name to an indexed target. - **`strata-arch-ir`.** Add `Binding::Memory` alongside the existing `Binding::Register`, and give the `Memory` canonical node (already named in `07-compiler-architecture.md` §1, not yet implemented) real contents: element type, depth, a fixed two-entry port list (one read, one write, per §3) each carrying an address width and the owning clock domain, a read-latency field (fixed at `1` for v0), and no-reset. This is the node's first real definition. - **`strata-circt`.** Lower `Memory` to CIRCT's `seq` dialect. Today this codebase's only sequential-state lowering is register-shaped (`seq.firreg`, `crates/strata-circt/src/lib.rs` ~250); `seq` also carries memory-primitive ops distinct from that register path, which is the natural target given D-032's existing commitment to hw/comb/seq/sv/verif MLIR against a pinned firtool — but the exact op surface needs to be reconfirmed against the pinned firtool version before implementation, the same pin-and-verify discipline D-032 already applies to the rest of the `seq` contract, rather than assumed from memory of the dialect. If that surface turns out unstable or under-maintained (the `pipeline`/`ssp`/`handshake` staleness precedent D-032 already found once), the fallback lowering is explicit: an address-decoded write-enable mux driving `N` `seq.firreg`s for storage, with a registered read-address stage for the 1-cycle latency, plus a vendor `ram_style`-class attribute as an Exit-1 bake hint (D-073) so downstream synthesis still infers block RAM from the resulting structure. Either lowering path is viable for v0; the choice is a research spike, not a design fork — the architectural semantics in §§1-5 don't change based on which one wins. ### 7. v0 scope **In v0:** - `mem name: [T; N];`, no `reset(...)`. - One read port, one write port, concurrently usable (§3). - Registered (1-cycle) reads, modeled through the existing `later` timing vocabulary (§2). - Indexed reads and writes both accept any `Index`-typed index, constant or runtime; boundedness is proved by the index's own type (§4). - Same-address same-cycle read/write hazard fixed to read-old-value (§4). - Single clock domain per `mem` in the general (safe) path. Cross-domain access to a shared `mem` (the `cdc_bridge.strata` pattern: write in `'src`, read in `'dst`) stays legal only inside `unsafe(clock_crossing)` components, mirroring the existing raw-CDC discipline already applied to `sync_ff` — the compiler does not verify cross-domain memory safety beyond that boundary; the component's own contract does (M4). - CIRCT lowering targets `seq` memory ops where confirmed available, else the register-array-plus-mux fallback (§6). **Deferred (north star), and why each is safely deferrable:** - **Combinational `mem` reads.** `reg [T; N]` already covers this case today (§2); no motivating fixture needs a second combinational-read storage form. - **True multi-port memories** (more than one read or one write port). `mem_ctrl.strata`'s `BANKS` parameter suggests banking N v0 memories is the cheap path to effective multi-porting (§3); no fixture needs a single memory with more ports than that. - **Byte-enable / sub-word partial writes.** No fixture in the corpus writes less than a full element; adding masked writes is a strict extension of the port shape in §6 whenever a use case needs it. - **Configurable read-during-write hazard policy.** v0's fixed read-old-value default is unobserved by the current corpus (§4); making it configurable is a later refinement, not a blocking gap. - **First-class dual-clock/async-dual-port memory typing.** `cdc_bridge.strata` needs *a* dual-clock memory today, but only inside an already-`unsafe` component; generalizing the `'src`/`'dst` domain-tagging already in the language into checked per-port `mem` clock typing is real work (it needs to reuse D-014's nominal clock-domain generativity) that nothing outside `unsafe(clock_crossing)` code requires yet. - **Memory initialization from a constant table** (ROM-style `mem` with an initial contents literal, analogous to `reg`'s `reset(v)`). Valuable for decode tables eventually, but no fixture motivating this decision needs it — every existing `mem` is a scratch buffer (FIFO backing store, transaction table), not a ROM. ## North star Combinational-read `mem` as a second declared form once a real workload needs indexed storage bigger than `reg [T; N]` but with zero read latency; multi-port `Memory` nodes (or a first-class banking combinator reusing `BANKS`-style parameters, keeping the primitive itself simple per P-5); byte-enable and masked writes; a checked per-port clock/domain field on `Memory` generalizing the `unsafe(clock_crossing)` `cdc_bridge.strata` pattern into something the type system verifies directly rather than delegating to the component's own contract; initialized/ROM-style memories; a `no_same_address_hazard`-class design lint (D-055's lint tier) for designs that assume the fixed read-old-value default matters to their timing. ## Open problems touching this doc None logged yet. If the `seq`-dialect memory-op research in §6 finds the same kind of staleness D-032 already found in `pipeline`/`ssp`/`handshake`, this decision's lowering recommendation moves from DRAFT to CONTESTED and needs a named entry in [open-problems.md](open-problems.md) rather than a silent rewrite here. ```