[gHashTag]

Closes #12202. Refs #9367 (WASM-on-AX7203 tracker). Epic: see Trinity-S-AI-DNA/trinity-fpga#917. Stacked on #12061 (lane/wasm-control-flow-12010), which is stacked on #12060; retarget to master after those merge.

What

Before this PR the board cell could run arithmetic and control flow over a stack and nothing could be stored. This PR gives specs/fpga/wasm_board_ax7203.t27 one 64 KiB linear memory page (var mem : [MEM_BYTES]u8, MEM_BYTES = 65536) and ten memory opcodes:

• i32.load (0x28), i32.load8_s/u (0x2C/0x2D), i32.load16_s/u (0x2E/0x2F), i32.store (0x36), i32.store8 (0x3A), i32.store16 (0x3B), memory.size (0x3F), memory.grow (0x40).
• Little-endian; a 2- or 4-byte access is a byte-per-step microsequence (mem_run) with one read site and one write site, both addressed by the register mem_addr; the extra steps spend no fuel.
• The memarg is two LEB128 values (align ignored, offset kept); a fifth continuation byte answers ERR_LEB; scan_class steps over the memarg, so a branch that skips a load with a two-byte offset ending in 0x0B lands correctly.
• An access of width w traps with ERR_MEM = 10 (RESP_BADOP on the wire) when base + offset > 65536 - w, before any byte is written; no wrap, and the next request works.
• load8_s/load16_s sign-extend, load8_u/load16_u zero-extend; store8/store16 leave every other byte alone.
• memory.size pushes 1; memory.grow pushes 0xFFFFFFFF for every delta (it grows nothing; a documented deviation from the WASM spec).

Ten new cell tests (42 in all), placed before the P2..P4 page-load tests, which stay last (shared code[], see the spec header). cell_runs grows from 45 to 55 bytes. In specs/fpga/wasm_opcodes.t27, fn executed_beyond_alu grows from 21 to 31 bytes and the executed-bytes law is re-pinned for 55 (24 ALU + 31); no row is added and no pinned const changes, the eight memory rows keep interp_ok = false because the live interpreter has no memory. Both seals re-saved from a master-built t27c.

Measured (commands as run, 2026-10-25, master-built t27c, iverilog 12.0, yosys 0.67)

check	result
t27c test-report specs/fpga/wasm_board_ax7203.t27	42 of 42, 0 vacuous
t27c test-report specs/fpga/wasm_opcodes.t27	16 of 16, 1 invariant proved, 0 vacuous
t27c gen-verilog specs/fpga/wasm_board_ax7203.t27	clean, 179665 bytes, empty stderr
iverilog -g2012 -DSIMULATION -o /dev/null wasm_board_ax7203.v	0 error lines (row wasm_board_ax7203 0, unchanged)
iverilog -g2012 -DSIMULATION -o /dev/null wasm_opcodes.v	149 error lines (row wasm_opcodes 149, unchanged)
t27c gen-verilog-for-simulation + sed '/= undefined;/d' (#12179) + iverilog -g2005 + vvp -n	42 PASSED, 0 FAILED, 0 assert failed lines, vvp exit 0
the same vvp run on the first commit 8d7b63311e (before the bounds-check rewrite)	41 PASSED, 1 FAILED (mem_access_past_the_page_traps, 10 asserts)
python3 tools/dupe_scan.py	ok: no new duplicate body, none of the known groups grew
tri seals sync-twins	497 twinned specs consistent, 0 extra files written; no home path in .trinity/seals
git diff --stat lane/wasm-control-flow-12010...HEAD	4 paths: the cell (+908), the table (+36 -16), the two seals

Not measured: nothing was synthesised or flashed. Until a bitstream is loaded with openFPGALoader -c digilent_hs2 on the AX7203 and the UART answers, every run above is a simulation.

The issue's block-RAM criterion: refuted, under its own clause

Issue #12202 asked for the page to infer as block RAM. yosys 0.67 read_verilog on the emitted cell answers Replacing memory \mem with list of registers, and read_verilog + hierarchy ran for more than ten minutes against 5.7 s for the base cell. The page is lowered as 65536 registers inside the single always @(posedge clk or negedge rst_n) block, which no block-RAM template infers. The spec is in the inference shape (one read site, one write site, one address register), the emitter is not; this is not block RAM in this lowering, reported as the issue's refutation clause allows, and filed as #12297. Do not run yosys synthesis on this cell until #12297 lands.

Disclosure: three t27c gen-verilog gaps found here, none fixed here

• gen-verilog: a cast to u64 emits the operand verbatim, so a 33-bit bounds sum wraps in 32 bits (Zig 42/42, vvp 41/42) #12296 (P1): as u64 casts emit the operand verbatim, so the 33-bit bounds sum of the first commit wrapped in 32 bits. The Zig run passed 42 of 42 while the Verilog run failed one test; the second commit rewrites mem_fits as two 32-bit compares that cannot overflow, and both runs now agree. The spec comment at mem_fits says why it has that form.
• gen-verilog: a module-level [N]u8 read and written inside the async-reset always block becomes 65536 registers, not block RAM #12297 (P1): the memory array lands inside the async-reset always block and becomes registers (above).
• gen-verilog: [0] ** 65536 gets an empty initial block, so an unwritten byte reads X in iverilog and 0 in Zig #12298: [0] ** 65536 gets an empty initial begin end, so an unwritten byte reads X in iverilog and 0 in Zig; the new tests store before they load.

Collision: #12181 (spec/wasm-board-p5-float-arith, a pure insertion into the same cell) names its section P5 too; whichever lands second merges the other by hand.

Next on this path (same cell file, so sequential): if/else, call/return, call_indirect, locals and globals on the existing frames (#9367 order), then i64.mul/i64.shr_s for DOOM's FixedMul; the loader of #12278 fills mem from the module's data segments.

🤖 Generated with Claude Code

[tri-claw]

Summary by t27-bees

Checked by the t27 compiler

_{t27c parse, parse-complete and typecheck on each changed .t27 file at 0daf4e6. Nothing was generated, built or run. A pass means the file is well formed, not that it is right.}

• specs/fpga/wasm_board_ax7203.t27: parses and typechecks.
• specs/fpga/wasm_opcodes.t27: parses and typechecks.

Read by the model

This PR adds a 64 KiB linear memory page and ten memory opcodes (load/store variants, memory.size, memory.grow) to the WASM board cell for AX7203. The implementation uses a byte-per-step microsequence for multi-byte accesses, little-endian encoding, LEB128 memarg parsing (align ignored), and bounds checking that traps with ERR_MEM before any write occurs. The page is shaped for block RAM inference but yosys 0.67 lowers it to 65536 registers; gen-verilog emits no initial block, so simulation reads X from unwritten bytes.

Worth a look

• specs/fpga/wasm_board_ax7203.t27:278–280 — The memory page var mem : [MEM_BYTES]u8 = [0] ** MEM_BYTES is declared zero-filled but gen-verilog emits no initial block for it. In simulation, unwritten bytes read as X; tests avoid this by storing before loading, but any synthesis or simulation path that reads before write will see X. The comment acknowledges this as a compiler gap.

• specs/fpga/wasm_board_ax7203.t27:350–365 — mem_fits uses two 32-bit compares (base > lim and off > lim - base) to implement a 33-bit bounds check without overflow. This is correct for w ≤ 4, but the logic depends on lim = MEM_BYTES - w not underflowing (true since MEM_BYTES = 65536 and w ∈ {1,2,4}). A future change to MEM_BYTES or w could break this silently.

• specs/fpga/wasm_board_ax7203.t27:1000–1100 — The mem_run microsequence (states 1–5) parses two LEB128 immediates, checks bounds, then performs byte-wise access. State 1–2 handle LEB parsing with mem_sh tracking shift; a fifth continuation byte in either field triggers ERR_LEB. However, the align field (first LEB) is read and ignored — if its LEB encoding is malformed (e.g., fifth byte with high bits), it still triggers ERR_LEB, which may not match WASM spec where align is allowed to be any valid LEB128.

• specs/fpga/wasm_board_ax7203.t27:1368–1420 — memory.grow pops delta and pushes 0xFFFFFFFF for every delta including 0, a documented deviation from WASM (which returns old size for 0). The test mem_grow_refuses confirms this behavior. If this cell ever interacts with a WASM-compliant host, the semantic mismatch could cause logic errors.

• specs/fpga/wasm_board_ax7203.t27:1880–1885 — The cost comment states "Refuted on synthesis: 10425 yosys LUTs... The page is lowered as 65536 registers... which no block-RAM template infers." This is a known synthesis issue: the single always @(posedge clk or negedge rst_n) block prevents block RAM inference. The PR explicitly does not claim block RAM, but any downstream user expecting BRAM usage will get distributed RAM instead.

---

_{Read: 4 files, +922 -52, the whole diff. Head 0daf4e6. Model: openai-compatible/nvidia/nemotron-3-ultra-550b-a55b. Commands: @t27-bees review | summary | help | pause | resume. Free for every repository.}