Skip to content

feat(spec): BitNet×GF-T inference neuron + signed GF-T dot4 (Refs #1764) - #1795

Merged
gHashTag merged 1 commit into
masterfrom
feat/gft-bitnet-neuron-signed-dot4
Aug 6, 2026
Merged

gHashTag merged 1 commit into
masterfrom
feat/gft-bitnet-neuron-signed-dot4

Conversation

@gHashTag

@gHashTag gHashTag commented Aug 6, 2026

Copy link
Copy Markdown
Owner

Refs #1764

Two spec-first increments fusing the project's two threads (BitNet ternary + GF-T format), both bit-exact to the ideal oracle gft16_ref.py and synthesizable. No compiler change (uses on_comb).

BitNet×GF-T neuron — specs/ternary/gft_bitnet_neuron.t27

A neuron with ternary weights {-1,0,+1} and real-valued GF-T16 activations — the actual BitNet inference pattern with wide dynamic range. Each trit weight selects +a / 0 / -a of its GF-T activation; the four signed contributions are summed in signed GF-T (RNE, zero-aware).

  • Bit-exact to the oracle over 3000 vectors (tree-consistent adds).
  • yosys synth_xilinx → 9763 LUT + 1320 CARRY4 (synthesizes to Artix-7).

Signed GF-T dot4 — specs/ternary/gft_signed_dot4.t27

A signed GF-T16 4-term MAC (real-valued matmul tile with negatives + cancellation), bit-exact to the oracle balanced tree over 3000 vectors.

Synthesis finding

A bounded while loop inside a Verilog function is not yosys-synthesizable ("Function can only be called with constant arguments"). The signed subtract's left-normalization was rewritten as a flat unrolled sequence (12 conditional shifts, ≥ the ~9 max) — functionally identical (re-verified 3000 vectors), now synthesizable. Bitstream/place-and-route (nextpnr) remains owner-gated (not installed locally).

1535 unit tests pass.

🤖 Generated with Claude Code

specs/ternary/gft_bitnet_neuron.t27: the BitNet x GF-T inference
primitive -- a neuron with ternary weights {-1,0,+1} and real-valued
GF-T16 activations. Each trit weight selects +a / 0 / -a of its GF-T
activation; the four signed contributions are summed in signed GF-T
(round-to-nearest-even, zero-aware). Fuses the two project threads.
Bit-exact to the oracle over 3000 vectors; yosys synth_xilinx ->
9763 LUT + 1320 CARRY4 (synthesizes to Artix-7).

specs/ternary/gft_signed_dot4.t27: a signed GF-T16 4-term MAC (real-
valued matmul tile with negatives + cancellation), bit-exact to the
oracle balanced tree over 3000 vectors.

Synthesis finding: a bounded `while` loop inside a Verilog function is
NOT yosys-synthesizable; the signed subtract's left-normalization was
rewritten flat (12 conditional shifts), re-verified 3000 vectors.
Bitstream (nextpnr) remains owner-gated.

No compiler change (uses on_comb); 1535 unit tests pass.

Refs #1764

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

github-actions Bot commented Aug 6, 2026

Copy link
Copy Markdown
Contributor

📓 NotebookLM Notebook linked to this PR

This notebook contains session context, decisions, and artifacts for this work.

@github-actions

github-actions Bot commented Aug 6, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-08-06 14:24:07 UTC

Summary

Status Count
Total Open PRs 3
PRs with Failing Checks 1
PRs with All Checks Green 2
READY 1
FAILING 1
PENDING 0

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=de57378ec0e2 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@gHashTag
gHashTag merged commit 5b57518 into master Aug 6, 2026
20 of 22 checks passed
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