Skip to content

feat(gen-verilog): spec-first ternary designs synthesize to real Artix-7 hardware (on_clock/on_comb data ports) (#1764) - #1786

Closed
gHashTag wants to merge 13 commits into
masterfrom
feat/streaming-ternary-mac-verified
Closed

gHashTag wants to merge 13 commits into
masterfrom
feat/streaming-ternary-mac-verified

Conversation

@gHashTag

@gHashTag gHashTag commented Aug 6, 2026

Copy link
Copy Markdown
Owner

Makes the spec-first ternary stack real, synthesizable FPGA hardware — the on-hardware MVP path for #1764. Self-consistent and buildable (compiler.rs sha == FROZEN_HASH); supersedes the externally-force-pushed, non-compiling branch of #1782.

The problem this solves

The stack was only ever simulated (iverilog). Running yosys synth_xilinx for the first time showed every design synthesized to zero cells: the fixed module interface (clk,rst_n,en,ready) had no data ports, so all compute drove nothing observable and the synthesizer dead-code-eliminated it. iverilog testbenches had been reaching inside the module to call the Verilog functions hierarchically.

What's here (all Refs #1764)

  1. Clocked on_clock process — registered module var state with reset + en gating (always @(posedge clk), nonblocking <=).
  2. Output data ports — a clocked module's scalar vars are exposed as output reg; ClockedCounter → 8 FDCE + 2 CARRY4.
  3. Streaming input ports + a streaming ternary MAC — on_clock params become input data ports; stream_ternary_mac.t27 accumulates bit-exact dot27 across cycles → 32 FDCE + a LUT adder-tree.
  4. on_comb combinational data interface — params → input ports, return → output wire result; makes the combinational half of the stack real hardware (comb_ternary_dot.t27 → ~162 LUT6, no FFs).
  5. Combinational BitNet neuron — comb_bitnet_neuron.t27 = quantize(dot27(a,b)) in one module → ~319 LUT + 2 CARRY4, 0 FF.
  6. docs/SYNTH_REPORT.md — measured Artix-7 cost of every design (a neuron is ~0.24% of the XC7A200T).

Verification

  • Every new module: iverilog cross-check vs an independent reference + yosys synth_xilinx (asserts real FFs/LUTs), in bootstrap/tests/{clocked_counter,stream_ternary_mac,comb_ternary_dot,comb_bitnet_neuron}.rs.
  • Seal-neutral: seal --verify Verilog byte-identical on all existing ternary specs (new interface behavior is gated on on_clock/on_comb fn names). FROZEN_HASH resealed. 1506 unit tests pass.

Notes

  • Branch is off an older master and needs a rebase onto current master: resolve bootstrap/src/compiler.rs by taking master's version + re-applying the additive port edits (a plain merge silently mis-merges that ~30k-line file into non-compiling code — this is what broke feat(gen-verilog): clocked on_clock process — first sequential spec-first design (#1764) #1782's branch).
  • Known follow-up: a single-module streaming neuron (registered y=quantize(acc)) needs a dead_store_elim soundness fix (don't eliminate writes to module vars exposed as output ports) — not seal-neutral, needs a repo-wide reseal sweep (owner decision).

🤖 Generated with Claude Code

gHashTag and others added 7 commits August 6, 2026 17:49
The spec-first path was combinational-only: gen-verilog emitted no
`always @(posedge clk)` and module-level `var` state was never
registered. A function named `on_clock` is now the opt-in clocked
process. Module emission partitions functions into `on_clock` (clocked)
vs the rest (combinational, unchanged) and lowers `on_clock` to
`always @(posedge clk or negedge rst_n)`: on `!rst_n` each scalar
module-level `var` takes its declared init value; while `en` is
asserted the body runs with nonblocking (`<=`) assignments. A new
`clocked_nonblocking` flag routes `StmtAssign` to `<=`, and a new
`gen_verilog_clocked_fn` emits the process.

This is the registered-state building block a streamed ternary MAC
needs to accumulate across cycles -- the first increment toward the
Phase-2 (clocked/streaming) MVP gate.

- specs/ternary/clocked_counter.t27 (+ seal): minimal proof spec.
- tests/clocked_counter.rs: checks the emitted always block + nonblocking
  update, then clocks it in iverilog -- reset, +1/cycle under en,
  en-gated freeze, resume, async re-reset = ALL_PASS.

Seal-neutral: specs without `on_clock` are byte-identical (seal --verify
MATCH on all 10 existing ternary/bitnet specs). FROZEN_HASH resealed.
1506 unit tests + the ternary/bitnet/verilog spec suite pass.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…dware)

Running yosys synth_xilinx on the spec-first ternary stack for the first
time revealed every design synthesized to ZERO logic cells: the fixed
module interface (clk,rst_n,en,ready) has no data ports, so all compute
drives nothing observable and the synthesizer dead-code-eliminates it.
The stack was only ever "verified" via iverilog testbenches that call
the Verilog functions hierarchically from inside the module.

Fix: in a clocked module (an `on_clock` fn is present) each scalar
module-level `var` is exposed as an `output reg` data port, so the
registered state is observable and the design maps to real flip-flops.
Gated on `on_clock`, so non-clocked specs -- and every existing spec,
including the 298 specs/scratch specs that use `pub var` -- keep the
byte-identical (clk,rst_n,en,ready) header.

Measured: ClockedCounter now synthesizes to 8 FDCE + 2 CARRY4 on
Artix-7 (yosys synth_xilinx) -- the first spec-first design that maps
to non-zero real hardware. tests/clocked_counter.rs now asserts the
output port and, when yosys is present, that flip-flops are produced.

Seal-neutral: seal --verify MATCH on all 10 existing ternary specs.
FROZEN_HASH resealed. 1506 unit tests + the spec suite pass.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… MAC

The parameters of a clocked `on_clock` fn now become streaming INPUT
data ports: `fn on_clock(x: i16) { acc = acc + x }` emits
`input signed [15:0] x`, and the always block reads the port each
cycle. Combined with the output-port exposure, a clocked spec is now a
complete datapath -- input ports -> compute -> accumulate register ->
output port. Present only when on_clock takes params, so nullary
on_clock and every existing spec stay byte-identical.

Adds specs/ternary/stream_ternary_mac.t27: a streaming ternary MAC, the
on-hardware BitNet inference primitive. Each cycle consumes a packed
27-trit (a,b) pair and accumulates the bit-exact dot27 (#1743) into a
32-bit acc output register, en-gated. Verified: yosys synth_xilinx ->
32 FDCE + a LUT adder-tree (real Artix-7 fabric); iverilog streams four
known trit-vector pairs and acc tracks the running dot-product sum
(27->54->27->27) exactly, freezing on en=0. In-spec dot27 tests pass.

Seal-neutral: seal --verify MATCH on all existing ternary specs incl.
the nullary clocked_counter. FROZEN_HASH resealed. 1506 unit tests +
the spec suite pass.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ecs -> real hardware)

`on_comb` is the combinational counterpart of `on_clock`: its params
become input data ports and its return is a continuously-driven
`output wire result` (`assign result = on_comb(...)`). This closes the
last synthesizability gap -- the output-port work so far only covered
clocked (on_clock) designs, so the whole combinational half of the
stack (dot27, adders, MLPs) still synthesized to zero cells because a
bare fn result never reaches a module port. Now a combinational spec
is real hardware. Present only when on_comb is defined, so every
existing spec is byte-identical.

Adds specs/ternary/comb_ternary_dot.t27: on_comb(a,b) = the bit-exact
27-trit dot product. Verified: yosys synth_xilinx -> ~162 LUT6 + a
CARRY4 reduction, no flip-flops (pure combinational Artix-7 fabric);
iverilog checks result == dot27(a,b) on known vectors = ALL_PASS.

With the clocked path, the spec-first ternary stack now synthesizes to
real FPGA hardware in both modes: combinational (on_comb -> LUT trees)
and sequential (on_clock -> FDCE + streaming MAC).

Seal-neutral: seal --verify MATCH on all existing ternary specs.
FROZEN_HASH resealed. 1506 unit tests + the spec suite pass.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…s to Artix-7

specs/ternary/comb_bitnet_neuron.t27: a full BitNet neuron over one
27-trit chunk in a single combinational module --
on_comb(a, b) = quantize(dot27(a, b)) (bit-exact ternary dot product ->
sign activation -> trit). Uses the existing on_comb data interface, no
compiler change.

Verified: typecheck 0 err; 4 in-spec tests pass; yosys synth_xilinx ->
~163 LUT6 + a CARRY4 reduction, NO flip-flops (pure combinational
Artix-7 neuron); iverilog checks result == quantize(dot27(a,b)) on
known vectors = ALL_PASS. Seal-neutral; 1506 unit tests pass.

Composed with the streaming accumulator (stream_ternary_mac) this
scales to a multi-chunk neuron.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Measured yosys synth_xilinx resource cost (Artix-7 XC7A200T) for every
spec-first hardware design: a full combinational BitNet neuron is
~319 LUT + 2 CARRY4 / 0 FF (~0.24% of the 200T), the streaming MAC is
346 LUT + 32 FDCE + 10 CARRY4. Hundreds of parallel neurons fit; the
gap to a running on-hardware layer is place-and-route + bitstream, not
logic capacity. Docs-only.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ix-7

specs/ternary/comb_bitnet_layer.t27: a full BitNet layer = 4 neurons
over a shared 27-trit activation, each quantize(dot27(w_i, a)) with its
own trained (const) weight vector, trits packed 2 bits each into the
result output. The next architectural level above the single neuron;
uses on_comb with a packed return, no compiler change.

Verified: typecheck 0 err; 3 hand-computed in-spec tests pass (packed
responses 146/24/85 to all-P/all-N/all-Z activations); yosys
synth_xilinx -> 288 LUT, 0 FF (const weights const-fold); iverilog
matches = ALL_PASS.

SYNTH_REPORT.md: layer scaling is linear -- a general programmable-
weight 4-neuron layer measures 1287 LUT ~= 4x the 319-LUT neuron, while
the trained/const-weight layer folds to 288 LUT. ~100 general layers
fit on the XC7A200T.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gHashTag and others added 2 commits August 6, 2026 19:19
specs/ternary/gft_dot2.t27: a spec-first GF-T16 2-term dot product
(y = a1*b1 + a2*b2) in the ternary-native GoldenFloat format proven
bit-exact on silicon (AX7203, gft_dot2 3/3). GF-T ladder multiply
(significand product + balanced-ternary exponent add + renorm) and
same-sign add (align + add + renorm), composed via on_comb.

The hand-written trinity-fpga gft_dot2/gft_mul/gft_add RTL documented
that t27c gen-verilog could not emit this because it interleaved reg
declarations with statements (illegal Verilog) -- that is exactly the
backend bug #1741 fixed, so this is the first spec-first GF-T MAC.

Verified: typecheck 0 err; in-spec tests pass; iverilog cross-check
against the embedded silicon-proven reference RTL = ALL_PASS on 2000
random inputs (bit-exact); yosys synth_xilinx -> 501 LUT + 123 CARRY4,
0 FF (combinational; high carry because `*` lowers to a shift-add
multiplier rather than a DSP48).

The spec-first compiler now generates the GF-T MAC that runs on real
silicon -- GF-T is on the spec-first path for the ternary NN work.
Seal-neutral; 1506 unit tests pass. Uses on_comb, no compiler change.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… reduction tree

specs/ternary/gft_dot4.t27: a spec-first GF-T16 4-term dot product
(y = a1*b1+a2*b2+a3*b3+a4*b4), scaling the silicon-proven 2-term GF-T
MAC to a real matmul/attention tile. GF-T float add is non-associative,
so the balanced reduction tree ((a1b1+a2b2)+(a3b3+a4b4)) is the contract.

Verified: typecheck 0 err; in-spec test passes (4.0 = 21504); iverilog
cross-check vs the same tree built from the silicon-proven gft_dot2 +
gft_add = ALL_PASS on 2000 random inputs (bit-exact). Uses on_comb, no
compiler change.

Documented (NOW.md): "DSP inference for *" is intentionally NOT done --
the shift-add __mul_noop is R-SI-1 (multiplier-free RTL by design, the
project keystone). DSP48 would violate it.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gHashTag

gHashTag commented Aug 6, 2026

Copy link
Copy Markdown
Owner Author

Landing status (verified this cycle): good news and a blocker that isn't ours.

  • My cycle-1 clocked construct (on_clock, gen_verilog_clocked_fn, clocked_nonblocking) already landed on master — identical to this branch's version.
  • The rest of this PR applies cleanly onto current master: I extracted the output-ports/input-ports/on_comb compiler delta and git apply --3way'd it onto origin/master (one trivial conflict — master's safe_name vs my node.name in gen_verilog_var, resolved by keeping both), added the additive spec/test/seal files, resealed, and it cargo builds clean. So this work is master-ready.
  • The blocker is a master codegen regression, not this PR: current master's gen-verilog emits a stray `endif with no matching `ifndef SIMULATION (visible even on a plain ternary_mac.t27 — 0 ifdef, 1 endif), which makes yosys reject every design and leaves 7 internal tests red (tests_w457_ram_style, tests_w458, tests_w459, tests_hir_pipeline_parity). This is the W458 guard-emission area that the in-progress repair-verilog-codegen-merge ([GOLD-RING] fix(compiler): restore declarations dropped by batch merge #1783 — master does not compile #1788) is working on.

Recommendation: once master's `ifndef/`endif guard emission is repaired and those 7 tests go green, this PR's port edits + specs drop in cleanly (build-verified). I did not push onto the broken base or touch the guard code under active repair.

… + master diagnosis

specs/ternary/gft_dot8.t27: a spec-first GF-T16 8-term dot product
(realistic inference / attention-head tile length), balanced reduction
tree. Verified: typecheck 0 err; in-spec test (8.0 = 22016); iverilog
cross-check vs the same tree from silicon-proven gft_dot2+gft_add =
ALL_PASS on 2000 random inputs (bit-exact). GF-T ladder: dot2->dot4->dot8.

NOW.md documents a master codegen diagnosis: current master is red (7
internal tests + yosys broken) from #1783 batch-merge drops that #1788
only partially repaired. The tests-section emits `// synthesis
translate_off` but closes with `endif (unbalanced -> breaks yosys);
one-line fix = emit `ifndef SIMULATION (verified). 6 other red tests are
distinct dropped features. Not pushed (multi-bug repair + reseal sweep
in an active-repair area = owner decision). The spec-first hardware
delta applies + builds clean on master and lands once those go green.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
gHashTag and others added 3 commits August 6, 2026 19:58
specs/ternary/gft_layer2.t27: a spec-first GF-T16 matmul row = 2 neurons
over a shared activation (1x2 activation x 2x2 weights -> 2 GF-T16
outputs packed into a 32-bit result). A full GF-T inference-layer
primitive in real-valued GF-T precision.

Verified: typecheck 0 err; in-spec test (packed 1375752704); iverilog
cross-check vs two silicon-proven gft_dot2 packed = ALL_PASS on 2000
random inputs (bit-exact). Uses on_comb, no compiler change; 1506 unit
tests pass.

Also this session: diagnosed + partially fixed master's codegen
breakage (3/7 tests, unblocks yosys repo-wide) -- filed issue #1789
with the verified patch; the full multi-feature repair + reseal sweep
is owner-scale.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…oracle

Finding: the silicon-proven GF-T arithmetic (what runs on the AX7203)
TRUNCATES the mantissa, so it is ~1 ULP low vs the ideal RNE oracle
(gft16_ref.py) -- ~37% of products off-by-one-low, ~12% carry-different
(62% mul / 12% add mismatch over 20-50k pairs). A systematic downward
bias for deep NN inference.

specs/ternary/gft_mul_rne.t27: a spec-first GF-T16 multiply that rounds
the mantissa to nearest-even (guard/round + tie-to-even + mantissa-carry
after round), matching the ideal oracle exactly -- a spec-first GF-T
MORE ACCURATE than the truncating silicon. Verified bit-exact against
300 oracle-generated normal-range vectors (~half differ from the
truncating silicon). Edge cases saturate like the silicon.

Signed GF-T (deferred) was investigated: needs an owner semantics
decision (no signed silicon reference; silicon-truncation and oracle-RNE
disagree). Documented, not guessed.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
specs/ternary/gft_add_rne.t27: a GF-T16 same-sign add with round-to-
nearest-even -- keeps the guard/sticky bits the silicon gft_add
truncates (>> d), plus tie-to-even and mantissa-carry-after-round.
Verified bit-exact vs 300 oracle add vectors.

specs/ternary/gft_dot2_rne.t27: the full RNE MAC y = a1*b1 + a2*b2
composing RNE mul + RNE add, bit-exact to the ideal oracle
gft16_add(gft16_mul(a1,b1), gft16_mul(a2,b2)) over 300 normal-range
vectors. The accurate counterpart of gft_dot2.t27 (which matches the
truncating silicon, ~1 ULP low).

With gft_mul_rne.t27 the spec-first stack now has a complete oracle-
accurate GF-T MAC, more accurate than what runs on silicon. Two GF-T
semantics coexist: truncating (silicon SSOT) and RNE (oracle-accurate).
No compiler change; 1506 unit tests pass.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gHashTag

gHashTag commented Aug 6, 2026

Copy link
Copy Markdown
Owner Author

Superseded by #1791, which landed the spec-first hardware stack (data ports + BitNet + GF-T + RNE) onto the now-unblocked master (#1790). All specs re-verified on master's compiler.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant