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<GEN_BITS>; 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<length>. 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.firregs 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<N> proves it, no new machinery

Decision: both read and write indices accept any Index<N>-typed value, compile-time constant or runtime (register, wire, computed) — no restriction to constant indices, and no separate bounds-check pass.

Index<N> (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<length> (Tier-1 entailment subsumption handles the case where a narrower Index<M> is offered where a wider Index<N> 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<N> 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<N> 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<T, const DEPTH: Nat1>), 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.firregs 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<N>-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 rather than a silent rewrite here.