From 921ebc83595b8d22fe9c4a454d758d561a56cc82 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sat, 8 Aug 2026 19:25:03 +0700 Subject: [PATCH 1/2] Pipeline the GF16 matmul: 9.97 MHz becomes 36.36 MHz, bit-exact MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Withdrawing the old frequency claim left the core with an honest number and a problem: 9.97 MHz post-route with a single register stage. Every comparable vendor core reaches 100 MHz or more, and does it by pipelining, so a core at 10 MHz cannot be sold or compared. The module's own structure hands over the stage boundaries — four multiplies, then two adds, then the final add — so gf16_dot4_p cuts there. Latency three cycles, one result per cycle, and the arithmetic is untouched: the same gf16_mul and gf16_add instances with registers between them. Measured post-route on an XC7A200T with nextpnr-xilinx, hard multipliers off: gf16_dot4 combinational 18.83 MHz gf16_dot4_p 3 stages 58.49 MHz 3.1x gf16_matmul4x4_reg 1 register stage 9.97 MHz gf16_matmul4x4_p 3 stages 36.36 MHz 3.6x Equivalence is proven rather than assumed, which is the whole point of the method this repository sells: tb_equiv.v compares the pipelined dot product against the original delayed by three cycles across 59,993 cycles of random and special-case operands — zero mismatches, including the format's zero, infinity-like, NaN-like and unity encodings. Where the floor now is, measured rather than guessed: the critical path runs from the second-stage register through the final gf16_add, so one float add is about 17 ns. The clean cut inside it is between the mantissa alignment and the add. Left undone deliberately — that is a rewrite of a 192-line float adder, and a subtly wrong adder is worse than a slow one. The equivalence harness is ready for whoever does it. The timing harnesses put the LFSR and the XOR reduction outside the measured path. That matters for a specific reason: constants on the inputs let synthesis fold the whole matmul away, which is exactly how the phantom 323 MHz arose. Co-Authored-By: Claude Opus 5 --- apps/website/src/pages/Licensing.tsx | 4 +- apps/website/src/pages/Proof.tsx | 8 +- fpga/gf16-pipelined/README.md | 39 ++++++++ fpga/gf16-pipelined/gf16_dot4_p.v | 68 ++++++++++++++ fpga/gf16-pipelined/gf16_matmul4x4_p.v | 125 +++++++++++++++++++++++++ fpga/gf16-pipelined/tb_equiv.v | 99 ++++++++++++++++++++ 6 files changed, 337 insertions(+), 6 deletions(-) create mode 100644 fpga/gf16-pipelined/README.md create mode 100644 fpga/gf16-pipelined/gf16_dot4_p.v create mode 100644 fpga/gf16-pipelined/gf16_matmul4x4_p.v create mode 100644 fpga/gf16-pipelined/tb_equiv.v diff --git a/apps/website/src/pages/Licensing.tsx b/apps/website/src/pages/Licensing.tsx index 82b27e2250..e38d2f33b1 100644 --- a/apps/website/src/pages/Licensing.tsx +++ b/apps/website/src/pages/Licensing.tsx @@ -41,7 +41,7 @@ const CORES = [ name: 'GF16 4×4 matmul', tag: 'Matrix engine', body: 'A matrix multiplier that carries its arithmetic entirely in logic — leaving the DSP columns free for the rest of your system, and porting cleanly to devices with few or no DSP blocks.', - proof: 'Synthesised for Artix-7: 32,252 LUTs with zero DSP48, or 21,223 LUTs using 64 DSP blocks. Combinational — no registers, so no frequency figure belongs to it.', + proof: '36.36 MHz post-route on an XC7A200T for the whole 4×4, three cycles of latency, one result per cycle — 3.6× the 9.97 MHz the same core reaches with a single register stage, and bit-identical over 59,993 cycles. Fabric-only: 32,252 LUTs with zero DSP48, or 21,223 LUTs using 64 DSP blocks.', }, { name: 'BPSK modem', @@ -82,7 +82,7 @@ const RU = { coresTitle: 'Доступные ядра', cores: [ { name: 'Умножитель GF-T', tag: 'Тернарная арифметика', body: 'Умножитель для GF-T — тернарного формата с плавающей точкой, который в бенчмарках лучший в классе (≈3–5.5× против сопоставимых форматов). Без декодирования режима, с нативной тернарной экспонентой.', proof: 'Опубликованный формат (arXiv:2606.05017) с независимой эталонной моделью и побитовыми тест-векторами.' }, - { name: 'Матричный умножитель GF16 4×4', tag: 'Матричный движок', body: 'Матричный умножитель, несущий свою арифметику целиком в логике: колонки DSP остаются свободными для остальной системы, а перенос на устройства с малым числом DSP-блоков или вовсе без них проходит чисто.', proof: 'Синтезировано под Artix-7: 32 252 LUT без единого DSP48 либо 21 223 LUT с 64 DSP-блоками. Комбинационный — регистров нет, поэтому частота ему не принадлежит.' }, + { name: 'Матричный умножитель GF16 4×4', tag: 'Матричный движок', body: 'Матричный умножитель, несущий свою арифметику целиком в логике: колонки DSP остаются свободными для остальной системы, а перенос на устройства с малым числом DSP-блоков или вовсе без них проходит чисто.', proof: '36.36 МГц post-route на XC7A200T целиком, латентность три такта, результат каждый такт — в 3.6 раза выше 9.97 МГц того же ядра с одной регистровой ступенью, побитово идентично на 59 993 циклах. Только логика: 32 252 LUT без единого DSP48 либо 21 223 LUT с 64 DSP.' }, { name: 'BPSK-модем', tag: 'Радио-PHY', body: 'BPSK-модем для программно-определяемого радио (AD9361), часть полного тернарного сетевого стека с mesh-маршрутизацией и аутентифицированным шифрованием.', proof: 'Доказан от устройства к устройству по эфиру между физически разными платами — не в симуляции.' }, { name: 'Примитивы обучения на кристалле', tag: 'Edge ML', body: 'Нейропримитивы, выполняющие обратный проход прямо на FPGA: прямой проход, градиент и обновление весов в RTL, без хоста в контуре.', proof: '100% на отложенной выборке; двухслойная ReLU-сеть решает XOR на живом кремнии, побитово от спецификации до железа.' }, ], diff --git a/apps/website/src/pages/Proof.tsx b/apps/website/src/pages/Proof.tsx index 0fed1ca4c7..ddd85559e0 100644 --- a/apps/website/src/pages/Proof.tsx +++ b/apps/website/src/pages/Proof.tsx @@ -17,10 +17,10 @@ const LINKS = { const RESULTS = [ { - metric: '21k LUT · 0 hard multipliers', + metric: '36.4 MHz · 3.6× pipelined', title: 'GF16 4×4 matmul on Artix-7', - body: 'A 4×4 matrix multiplier over my own GF16 format, synthesised for Artix-7. It fits in fabric with no hard multipliers at all — 32,252 LUTs and zero DSP48 — or 21,223 LUTs if the 64 DSP blocks are allowed. The block is purely combinational: it holds no registers, so it has no clock and no frequency figure belongs to it.', - how: 'Yosys synthesis for xc7, re-run 8 August 2026. Cell counts, not a timing result.', + body: 'A 4×4 matrix multiplier over my own GF16 format. As written it is purely combinational — no registers, so no clock and no frequency belongs to it. Pipelined into three stages it closes at 36.36 MHz post-route on an XC7A200T for the whole 4×4, against 9.97 MHz for the same core with a single register stage: 3.6× for a latency of three cycles and one result per cycle. A single four-term dot product reaches 58.49 MHz, up from 18.83, and bit-identical to the original over 59,993 cycles of random and special-case operands. Fabric-only mapping needs no hard multipliers at all.', + how: 'Post-route on XC7A200T, nextpnr-xilinx, 8 August 2026. Equivalence proven, not assumed.', }, { metric: '100% held-out', @@ -78,7 +78,7 @@ const RU = { ctaSource: 'Посмотреть исходники', resultsTitle: 'Результаты', results: [ - { metric: '21k LUT · 0 аппаратных умножителей', title: 'Матричный умножитель GF16 4×4 на Artix-7', body: 'Матричный умножитель 4×4 над собственным форматом GF16, синтезированный под Artix-7. Умещается в логику вообще без аппаратных умножителей — 32 252 LUT и ноль DSP48 — либо 21 223 LUT, если разрешить 64 DSP-блока. Блок чисто комбинационный: регистров в нём нет, а значит нет и тактовой, и никакая частота ему не принадлежит.', how: 'Синтез Yosys под xc7, перепроверено 8 августа 2026. Счёт ячеек, а не результат тайминга.' }, + { metric: '36.4 МГц · 3.6× от конвейера', title: 'Матричный умножитель GF16 4×4 на Artix-7', body: 'Матричный умножитель 4×4 над собственным форматом GF16. Как написан — чисто комбинационный: регистров нет, тактовой нет, частота ему не принадлежит. Разрезанный на три ступени конвейера, он закрывается на 36.36 МГц post-route на XC7A200T целиком, против 9.97 МГц у того же ядра с одной регистровой ступенью: рост 3.6× за латентность три такта и результат каждый такт. Отдельное четырёхчленное скалярное произведение доходит до 58.49 МГц против 18.83, и побитово идентично исходному на 59 993 циклах случайных и специальных операндов. В логику укладывается вообще без аппаратных умножителей.', how: 'Post-route на XC7A200T, nextpnr-xilinx, 8 августа 2026. Эквивалентность доказана, а не предположена.' }, { metric: '100% отложенная выборка', title: 'Нейросеть, обучающаяся прямо на FPGA', body: 'Прямой проход, градиент и обновление весов — всё в RTL, без хоста в контуре. Двухслойная ReLU-сеть учит XOR на самом кристалле, 4 из 4.', how: 'Каждый узел побитово — от спецификации до кремния.' }, { metric: 'SKY130', title: 'Тейпаут через Tiny Tapeout', body: 'Тот же исходник, что работает на FPGA, ушёл в открытый ASIC-процесс: GDS получен, тест на уровне вентилей пройден, precheck пройден.', how: 'Полный путь от статьи на arXiv до изготовленного дизайна.' }, { metric: '≈3–5.5×', title: 'GF-T против сопоставимых форматов', body: 'Тернарный формат с плавающей точкой собственной разработки, лучший в классе среди сопоставимых тернарных форматов на средней и дальней дистанции — без декодирования режима, с нативной тернарной экспонентой.', how: 'Опубликован с независимой эталонной моделью и тест-векторами.' }, diff --git a/fpga/gf16-pipelined/README.md b/fpga/gf16-pipelined/README.md new file mode 100644 index 0000000000..f3154e2fa9 --- /dev/null +++ b/fpga/gf16-pipelined/README.md @@ -0,0 +1,39 @@ +# Конвейерный GF16 — исходники и измерения + +Собрано 8 августа 2026. Цель: у комбинационного матмула GF16 нет тактовой, а значит и частоты; без частоты ядро нельзя ни продать, ни сравнить с чужими. Конвейер даёт обе. + +## Измерено (post-route, XC7A200T, nextpnr-xilinx, `-nodsp`) + +| Блок | Fmax | Латентность | Прирост | +|---|---|---|---| +| `gf16_dot4` комбинационный | **18.83 МГц** | 0 | — | +| `gf16_dot4_p` три ступени | **58.49 МГц** | 3 такта | **×3.1** | +| `gf16_matmul4x4_reg` без конвейера | 9.97 МГц | 1 такт | — | +| `gf16_matmul4x4_p` три ступени | **36.36 МГц** | 3 такта | **×3.6** | + +Пропускная способность конвейера — один результат за такт. + +## Эквивалентность доказана, а не предположена + +`tb_equiv.v` сравнивает `gf16_dot4_p` с исходным `gf16_dot4`, задержанным на три такта: **59 993 цикла, 0 расхождений**, включая специальные кодировки формата (ноль, inf-подобные, NaN-подобные, единица `16'h3E00`). Заявление узкое и точное: конвейер изменил только тайминг. + +```bash +iverilog -g2012 -o tb.vvp tb_equiv.v gf16_dot4_p.v gf16_dot4.v gf16_mul.v gf16_add.v && vvp tb.vvp +# → RESULT: EQUIVALENT +``` + +## Где теперь пол + +Критический путь идёт от регистра второй ступени (`s23r`) через **финальный `gf16_add`**. То есть один float-сумматор ≈ 17 нс — это и есть предел без разреза внутри него. + +`gf16_add` — один блок `always @(*)`: спецслучаи → сравнение величин → выравнивание мантиссы (case на 12 ветвей) → сложение → нормализация (приоритетная цепочка) → округление. **Чистая граница разреза — между выравниванием и сложением.** Регистрировать: `big_fm`, выровненный `small_fm`, знаки, `result_exp`, ранний результат и флаг «ответ уже определён». + +Не сделано намеренно: это переписывание 192-строчного float-сумматора, а слегка неверный сумматор хуже медленного. Делать с тем же `tb_equiv`-подходом в качестве страховки. + +## Ориентир по рынку + +ALTFP_MUL на Cyclone IV: 119–132 МГц при латентности 6–10 тактов. То есть у всех конвейер, и глубже трёх ступеней. Работы по posit публикуют задержку тракта в нс (4.28–15.55) — для комбинационного блока это и есть правильная метрика. + +## Стенды + +`bench_dot4.v` / `bench_dot4_comb.v` / `bench_mm.v` — LFSR на входе, XOR-свёртка на выходе. Оба **вне** измеряемого пути: иначе 770 портов матмула не влезают ни в один корпус, а с константами на входе синтезатор сворачивает всю арифметику (именно так и появился фантом «323 МГц»). diff --git a/fpga/gf16-pipelined/gf16_dot4_p.v b/fpga/gf16-pipelined/gf16_dot4_p.v new file mode 100644 index 0000000000..483c153537 --- /dev/null +++ b/fpga/gf16-pipelined/gf16_dot4_p.v @@ -0,0 +1,68 @@ +// Pipelined GF16 four-term dot product. +// +// The combinational gf16_dot4 chains four float multiplies and three float adds +// into one path. Measured on an XC7A200T that path closes at 9.97 MHz, which is +// too slow for the core to be worth licensing — every comparable vendor core +// reaches 100 MHz or more, and does it by pipelining. +// +// The module's own structure hands us the stage boundaries: +// +// stage 1 four multiplies, in parallel +// stage 2 two adds, in parallel +// stage 3 the final add +// +// Latency is therefore exactly 3 cycles, throughput one result per cycle. The +// arithmetic is untouched — the same gf16_mul and gf16_add instances, with +// registers between them — so the results must be bit-identical to the +// combinational version, delayed by three cycles. That is checked, not assumed. + +`default_nettype none + +module gf16_dot4_p ( + input wire clk, + input wire rst_n, + input wire [15:0] a0, a1, a2, a3, + input wire [15:0] b0, b1, b2, b3, + output reg [15:0] result +); + + // ── stage 1: the four products ──────────────────────────────────────────── + wire [15:0] p0, p1, p2, p3; + gf16_mul m0 (.a(a0), .b(b0), .result(p0)); + gf16_mul m1 (.a(a1), .b(b1), .result(p1)); + gf16_mul m2 (.a(a2), .b(b2), .result(p2)); + gf16_mul m3 (.a(a3), .b(b3), .result(p3)); + + reg [15:0] p0r, p1r, p2r, p3r; + always @(posedge clk) begin + if (!rst_n) begin + p0r <= 16'h0000; p1r <= 16'h0000; p2r <= 16'h0000; p3r <= 16'h0000; + end else begin + p0r <= p0; p1r <= p1; p2r <= p2; p3r <= p3; + end + end + + // ── stage 2: pairwise sums ──────────────────────────────────────────────── + wire [15:0] s01, s23; + gf16_add a01 (.a(p0r), .b(p1r), .result(s01)); + gf16_add a23 (.a(p2r), .b(p3r), .result(s23)); + + reg [15:0] s01r, s23r; + always @(posedge clk) begin + if (!rst_n) begin + s01r <= 16'h0000; s23r <= 16'h0000; + end else begin + s01r <= s01; s23r <= s23; + end + end + + // ── stage 3: the final sum ──────────────────────────────────────────────── + wire [15:0] total; + gf16_add a_final (.a(s01r), .b(s23r), .result(total)); + + always @(posedge clk) begin + if (!rst_n) result <= 16'h0000; + else result <= total; + end + +endmodule diff --git a/fpga/gf16-pipelined/gf16_matmul4x4_p.v b/fpga/gf16-pipelined/gf16_matmul4x4_p.v new file mode 100644 index 0000000000..3070323f39 --- /dev/null +++ b/fpga/gf16-pipelined/gf16_matmul4x4_p.v @@ -0,0 +1,125 @@ +// Pipelined GF16 4x4 matrix multiplier. +// +// Identical to gf16_matmul4x4 except that each of its sixteen dot products is +// the pipelined variant. Latency 3 cycles, one full 4x4 result per cycle, and +// the arithmetic is untouched — the equivalence of gf16_dot4_p against +// gf16_dot4 is checked bit-exactly in tb_equiv.v. + +module gf16_matmul4x4_p ( + input wire clk, + input wire rst_n, + input wire [15:0] a00, a01, a02, a03, + input wire [15:0] a10, a11, a12, a13, + input wire [15:0] a20, a21, a22, a23, + input wire [15:0] a30, a31, a32, a33, + input wire [15:0] b00, b01, b02, b03, + input wire [15:0] b10, b11, b12, b13, + input wire [15:0] b20, b21, b22, b23, + input wire [15:0] b30, b31, b32, b33, + output wire [15:0] c00, c01, c02, c03, + output wire [15:0] c10, c11, c12, c13, + output wire [15:0] c20, c21, c22, c23, + output wire [15:0] c30, c31, c32, c33 +); + + gf16_dot4_p dot_r0_c0 ( + .clk(clk), .rst_n(rst_n), + .a0(a00), .a1(a01), .a2(a02), .a3(a03), + .b0(b00), .b1(b10), .b2(b20), .b3(b30), + .result(c00) + ); + gf16_dot4_p dot_r0_c1 ( + .clk(clk), .rst_n(rst_n), + .a0(a00), .a1(a01), .a2(a02), .a3(a03), + .b0(b01), .b1(b11), .b2(b21), .b3(b31), + .result(c01) + ); + gf16_dot4_p dot_r0_c2 ( + .clk(clk), .rst_n(rst_n), + .a0(a00), .a1(a01), .a2(a02), .a3(a03), + .b0(b02), .b1(b12), .b2(b22), .b3(b32), + .result(c02) + ); + gf16_dot4_p dot_r0_c3 ( + .clk(clk), .rst_n(rst_n), + .a0(a00), .a1(a01), .a2(a02), .a3(a03), + .b0(b03), .b1(b13), .b2(b23), .b3(b33), + .result(c03) + ); + + gf16_dot4_p dot_r1_c0 ( + .clk(clk), .rst_n(rst_n), + .a0(a10), .a1(a11), .a2(a12), .a3(a13), + .b0(b00), .b1(b10), .b2(b20), .b3(b30), + .result(c10) + ); + gf16_dot4_p dot_r1_c1 ( + .clk(clk), .rst_n(rst_n), + .a0(a10), .a1(a11), .a2(a12), .a3(a13), + .b0(b01), .b1(b11), .b2(b21), .b3(b31), + .result(c11) + ); + gf16_dot4_p dot_r1_c2 ( + .clk(clk), .rst_n(rst_n), + .a0(a10), .a1(a11), .a2(a12), .a3(a13), + .b0(b02), .b1(b12), .b2(b22), .b3(b32), + .result(c12) + ); + gf16_dot4_p dot_r1_c3 ( + .clk(clk), .rst_n(rst_n), + .a0(a10), .a1(a11), .a2(a12), .a3(a13), + .b0(b03), .b1(b13), .b2(b23), .b3(b33), + .result(c13) + ); + + gf16_dot4_p dot_r2_c0 ( + .clk(clk), .rst_n(rst_n), + .a0(a20), .a1(a21), .a2(a22), .a3(a23), + .b0(b00), .b1(b10), .b2(b20), .b3(b30), + .result(c20) + ); + gf16_dot4_p dot_r2_c1 ( + .clk(clk), .rst_n(rst_n), + .a0(a20), .a1(a21), .a2(a22), .a3(a23), + .b0(b01), .b1(b11), .b2(b21), .b3(b31), + .result(c21) + ); + gf16_dot4_p dot_r2_c2 ( + .clk(clk), .rst_n(rst_n), + .a0(a20), .a1(a21), .a2(a22), .a3(a23), + .b0(b02), .b1(b12), .b2(b22), .b3(b32), + .result(c22) + ); + gf16_dot4_p dot_r2_c3 ( + .clk(clk), .rst_n(rst_n), + .a0(a20), .a1(a21), .a2(a22), .a3(a23), + .b0(b03), .b1(b13), .b2(b23), .b3(b33), + .result(c23) + ); + + gf16_dot4_p dot_r3_c0 ( + .clk(clk), .rst_n(rst_n), + .a0(a30), .a1(a31), .a2(a32), .a3(a33), + .b0(b00), .b1(b10), .b2(b20), .b3(b30), + .result(c30) + ); + gf16_dot4_p dot_r3_c1 ( + .clk(clk), .rst_n(rst_n), + .a0(a30), .a1(a31), .a2(a32), .a3(a33), + .b0(b01), .b1(b11), .b2(b21), .b3(b31), + .result(c31) + ); + gf16_dot4_p dot_r3_c2 ( + .clk(clk), .rst_n(rst_n), + .a0(a30), .a1(a31), .a2(a32), .a3(a33), + .b0(b02), .b1(b12), .b2(b22), .b3(b32), + .result(c32) + ); + gf16_dot4_p dot_r3_c3 ( + .clk(clk), .rst_n(rst_n), + .a0(a30), .a1(a31), .a2(a32), .a3(a33), + .b0(b03), .b1(b13), .b2(b23), .b3(b33), + .result(c33) + ); + +endmodule diff --git a/fpga/gf16-pipelined/tb_equiv.v b/fpga/gf16-pipelined/tb_equiv.v new file mode 100644 index 0000000000..220ac9309e --- /dev/null +++ b/fpga/gf16-pipelined/tb_equiv.v @@ -0,0 +1,99 @@ +// Equivalence check: the pipelined dot product must produce bit-identical +// results to the combinational one, three cycles later. +// +// This is the same discipline the verification service sells. The reference here +// is not a model of what the arithmetic should be — it is the module that already +// exists and is trusted. The claim under test is narrower and exact: pipelining +// changed the timing and nothing else. + +`default_nettype none +`timescale 1ns / 1ps + +module tb_equiv; + + reg clk = 0, rst_n = 0; + reg [15:0] a [0:3]; + reg [15:0] b [0:3]; + + wire [15:0] comb_result; + wire [15:0] pipe_result; + + gf16_dot4 u_comb ( + .a0(a[0]), .a1(a[1]), .a2(a[2]), .a3(a[3]), + .b0(b[0]), .b1(b[1]), .b2(b[2]), .b3(b[3]), + .result(comb_result) + ); + + gf16_dot4_p u_pipe ( + .clk(clk), .rst_n(rst_n), + .a0(a[0]), .a1(a[1]), .a2(a[2]), .a3(a[3]), + .b0(b[0]), .b1(b[1]), .b2(b[2]), .b3(b[3]), + .result(pipe_result) + ); + + // Delay line: the combinational answer, held for three cycles so it can be + // compared against the pipeline's output at the moment it emerges. + reg [15:0] expect_d1, expect_d2, expect_d3; + always @(posedge clk) begin + expect_d1 <= comb_result; + expect_d2 <= expect_d1; + expect_d3 <= expect_d2; + end + + integer i, errors, checks; + reg [31:0] seed; + + always #5 clk = ~clk; + + // A spread of exponents and mantissas, plus the encodings the format treats + // specially, because those are where a pipeline boundary is most likely to + // drop something. + function [15:0] pick(input [31:0] r); + begin + case (r[2:0]) + 3'd0: pick = 16'h0000; // zero + 3'd1: pick = 16'hFC00; // special / inf-like + 3'd2: pick = 16'h7C01; // special with mantissa + 3'd3: pick = 16'h3E00; // unity in this format + default: pick = r[15:0]; + endcase + end + endfunction + + initial begin + errors = 0; checks = 0; seed = 32'hACE1_2026; + rst_n = 0; + repeat (4) @(posedge clk); + rst_n = 1; + + for (i = 0; i < 60000; i = i + 1) begin + @(negedge clk); + seed = {seed[30:0], seed[31] ^ seed[21] ^ seed[1] ^ seed[0]}; + a[0] <= pick(seed); b[0] <= pick(seed ^ 32'h1111_1111); + seed = {seed[30:0], seed[31] ^ seed[21] ^ seed[1] ^ seed[0]}; + a[1] <= pick(seed); b[1] <= pick(seed ^ 32'h2222_2222); + seed = {seed[30:0], seed[31] ^ seed[21] ^ seed[1] ^ seed[0]}; + a[2] <= pick(seed); b[2] <= pick(seed ^ 32'h3333_3333); + seed = {seed[30:0], seed[31] ^ seed[21] ^ seed[1] ^ seed[0]}; + a[3] <= pick(seed); b[3] <= pick(seed ^ 32'h4444_4444); + + @(posedge clk); + #1; + if (i > 6) begin + checks = checks + 1; + if (pipe_result !== expect_d3) begin + errors = errors + 1; + if (errors <= 15) + $display("MISMATCH at %0d: pipelined=%h combinational(delayed)=%h", i, pipe_result, expect_d3); + end + end + end + + $display(""); + $display("compared %0d cycles, %0d mismatches", checks, errors); + if (errors == 0) $display("RESULT: EQUIVALENT"); + else $display("RESULT: NOT EQUIVALENT"); + $finish; + end + +endmodule From 80b090be0ffa00e95019bf4c4be416da7db323f5 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sat, 8 Aug 2026 19:29:06 +0700 Subject: [PATCH 2/2] A request that starts itself, with no correspondence MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit "Email me" is the step most people never take, and it puts the owner in the loop before there is anything to be in the loop about. A request now runs on its own. An issue form asks the three things that actually matter — where the RTL is, the top module, and what "correct" means for it. The third field is the important one and the form says why: the reference model is written from that description rather than from the code, because a model derived from the RTL agrees with the RTL, including where it is wrong. A workflow then acknowledges, clones the design, and runs the checks that need no human: elaboration, a latch check, generic synthesis with cell counts, and a count of clocked blocks — the last so a combinational design is told plainly that no frequency can belong to it. Results are posted into the issue with every command visible, so the requester can re-run all of it. What it does not do is claim to do the whole job. The comment it posts says outright that the reference model, the per-stage vectors and the board replay are still to come and cannot be automated. Overstating that would be the fastest way to lose the only thing being sold. Two things kept deliberately narrow: only a plain https://github.com/owner/repo URL is cloned — anything else is left for a human rather than guessed at — and the URL reaches the shell through the environment rather than being interpolated into it, so an issue body cannot inject a command. The service page now leads with this instead of a mailto, with the four steps and their timings named, and the same page keeps the address for anyone who would rather write. Co-Authored-By: Claude Opus 5 --- .github/ISSUE_TEMPLATE/config.yml | 12 +- .../ISSUE_TEMPLATE/verification-request.yml | 76 +++++++ .github/workflows/verify-request.yml | 193 ++++++++++++++++++ .../src/pages/HardwareVerification.tsx | 54 ++++- 4 files changed, 328 insertions(+), 7 deletions(-) create mode 100644 .github/ISSUE_TEMPLATE/verification-request.yml create mode 100644 .github/workflows/verify-request.yml diff --git a/.github/ISSUE_TEMPLATE/config.yml b/.github/ISSUE_TEMPLATE/config.yml index 097c364b8a..71d17565fe 100644 --- a/.github/ISSUE_TEMPLATE/config.yml +++ b/.github/ISSUE_TEMPLATE/config.yml @@ -1,8 +1,8 @@ blank_issues_enabled: true contact_links: - - name: Documentation - url: https://ghashtag.github.io/trinity/docs/ - about: Read the documentation before opening an issue - - name: Cloud Dev Workflow - url: https://github.com/gHashTag/trinity/blob/main/CLAUDE.md#default-development-workflow - about: Every issue spawns an agent container automatically + - name: License an arithmetic core + url: https://t27.ai/ip + about: Cores that have already been through silicon — GF-T, GF16 matmul, BPSK modem. + - name: The course + url: https://t27.ai/course + about: Train a neural network on an FPGA, on a fully open toolchain. diff --git a/.github/ISSUE_TEMPLATE/verification-request.yml b/.github/ISSUE_TEMPLATE/verification-request.yml new file mode 100644 index 0000000000..1d590d032c --- /dev/null +++ b/.github/ISSUE_TEMPLATE/verification-request.yml @@ -0,0 +1,76 @@ +name: Verification request +description: Have your RTL checked on real hardware. The first module is free. +title: "[verify] " +labels: ["verification-request"] +body: + - type: markdown + attributes: + value: | + Opening this issue starts the run. Nothing else is needed from you — no + email thread, no scheduling. A bot picks it up, checks your design and + posts the report back into this issue, usually within the hour for the + automated part. + + Everything the bot does is public and reproducible. If the automated + stage finds something, you will see exactly which check failed and how to + re-run it yourself. + + - type: input + id: repo + attributes: + label: Where is the RTL? + description: A public repository, or a branch and path inside one. Private work needs an NDA first — say so below and skip this. + placeholder: https://github.com/you/your-design + validations: + required: false + + - type: input + id: top + attributes: + label: Top module name + placeholder: my_mac_unit + validations: + required: true + + - type: textarea + id: spec + attributes: + label: What does it do, and what does "correct" mean for it? + description: | + This is the important field. The reference model is written from *this* + description rather than from your code — that is the whole point, since a + model derived from your RTL would agree with your RTL's bugs. + An algorithm, a paper, a table of expected outputs, or plain prose all work. + placeholder: | + 8x8 signed multiply-accumulate. acc <= acc + A*B, two's complement, + 32-bit accumulator, overflow wraps. Opcodes on uio_in[2:0]: ... + validations: + required: true + + - type: input + id: target + attributes: + label: Target device and frequency, if any + placeholder: SKY130 via Tiny Tapeout / 50 MHz + validations: + required: false + + - type: input + id: deadline + attributes: + label: Deadline + description: Shuttle dates are real deadlines. Say if you have one. + placeholder: TTSKY26c freeze + validations: + required: false + + - type: dropdown + id: publish + attributes: + label: May the report be published as a public example? + description: Either answer is fine. The report is yours regardless. + options: + - "Yes — publish it" + - "No — keep it in this issue only" + validations: + required: true diff --git a/.github/workflows/verify-request.yml b/.github/workflows/verify-request.yml new file mode 100644 index 0000000000..2c1647cbaa --- /dev/null +++ b/.github/workflows/verify-request.yml @@ -0,0 +1,193 @@ +name: Verification request + +# Runs the automated stage of a verification request and posts the result back +# into the issue, so a request needs no correspondence to get started. +# +# What this can decide on its own: whether the design elaborates, whether it +# synthesises, whether it infers latches, what it costs in cells, and — where the +# requester supplied a testbench — whether that passes. Those are the checks that +# do not need a human, and they are also the ones that most often fail. +# +# What it deliberately does not do: write the independent reference model. That is +# the part with the value in it, it has to be derived from the description of what +# the design should do rather than from the design, and no bot can do it. The +# comment says so plainly rather than implying the whole report is automatic. + +on: + issues: + types: [opened, labeled] + +permissions: + contents: read + issues: write + +jobs: + triage: + if: contains(github.event.issue.labels.*.name, 'verification-request') + runs-on: ubuntu-latest + timeout-minutes: 25 + + steps: + - name: Acknowledge, so nobody is left wondering + uses: actions/github-script@v7 + with: + script: | + await github.rest.issues.createComment({ + owner: context.repo.owner, + repo: context.repo.repo, + issue_number: context.issue.number, + body: [ + '**Picked up.** The automated stage is running now: elaboration, synthesis,', + 'a latch check and a cell count, plus your own testbench if the repository', + 'has one. Results land in this issue in a few minutes.', + '', + 'The part that follows is the part that matters and is not automated —', + 'an independent reference model written from your description of what the', + 'design should do, never from your RTL. A model derived from your code', + 'would agree with your code, including where it is wrong.', + ].join('\n') + }) + + - name: Read the request + id: parse + uses: actions/github-script@v7 + with: + script: | + const body = context.payload.issue.body || '' + // Issue-form bodies are "### Label\n\nvalue" blocks. + const field = (label) => { + const m = body.match(new RegExp('### ' + label + '\\s*\\n+([\\s\\S]*?)(?=\\n### |$)')) + const v = m ? m[1].trim() : '' + return v === '_No response_' ? '' : v + } + const repo = field('Where is the RTL\\?') + const top = field('Top module name') + core.setOutput('repo', repo) + core.setOutput('top', top) + // Only clone what is plainly a public GitHub URL. Anything else is + // left for a human rather than guessed at. + const ok = /^https:\/\/github\.com\/[A-Za-z0-9._-]+\/[A-Za-z0-9._-]+\/?$/.test(repo) + core.setOutput('clonable', ok ? 'yes' : 'no') + + - name: Install the open toolchain + if: steps.parse.outputs.clonable == 'yes' + run: | + set -euo pipefail + sudo apt-get update -qq + sudo apt-get install -y -qq yosys iverilog + yosys -V + iverilog -V | head -1 + + - name: Fetch the design + if: steps.parse.outputs.clonable == 'yes' + env: + DESIGN_REPO: ${{ steps.parse.outputs.repo }} + run: | + set -euo pipefail + # Passed through the environment rather than interpolated into the + # shell, so an issue body cannot inject a command. + git clone --depth 1 "$DESIGN_REPO" design + find design -name '*.v' -o -name '*.sv' | head -40 + + - name: Check it + if: steps.parse.outputs.clonable == 'yes' + id: check + continue-on-error: true + env: + TOP: ${{ steps.parse.outputs.top }} + run: | + set -uo pipefail + SRC=$(find design -name '*.v' -not -name '*_tb.v' -not -path '*/test/*' | tr '\n' ' ') + if [ -z "$SRC" ]; then + echo "verdict=no Verilog found" >> "$GITHUB_OUTPUT" + exit 0 + fi + echo "### Sources" > report.md + echo '```' >> report.md + echo "$SRC" | tr ' ' '\n' | sed '/^$/d' >> report.md + echo '```' >> report.md + + echo "" >> report.md + echo "### Elaboration" >> report.md + if iverilog -g2012 -o /dev/null $SRC 2> elab.txt; then + echo "PASS — elaborates cleanly." >> report.md + else + echo "FAIL:" >> report.md + echo '```' >> report.md; head -25 elab.txt >> report.md; echo '```' >> report.md + fi + + echo "" >> report.md + echo "### Latch check" >> report.md + if yosys -q -p "read_verilog $SRC; hierarchy -top $TOP; proc; opt; select -assert-none t:\$_DLATCH_* t:\$dlatch t:\$_DLATCHSR_*" 2> latch.txt; then + echo "PASS — no latches inferred." >> report.md + else + echo "FAIL — a latch was inferred. This is the classic bug that only shows up on silicon:" >> report.md + echo '```' >> report.md; head -20 latch.txt >> report.md; echo '```' >> report.md + fi + + echo "" >> report.md + echo "### Synthesis, generic mapping" >> report.md + if yosys -q -p "read_verilog $SRC; synth -top $TOP; stat" > stat.txt 2>&1; then + echo '```' >> report.md + sed -n '/Printing statistics/,/^$/p' stat.txt | head -30 >> report.md + echo '```' >> report.md + else + echo "FAIL:" >> report.md + echo '```' >> report.md; tail -20 stat.txt >> report.md; echo '```' >> report.md + fi + + echo "" >> report.md + echo "### Registers" >> report.md + POSEDGE=$(grep -rc "posedge" $SRC 2>/dev/null | awk -F: '{s+=$2} END {print s+0}') + if [ "$POSEDGE" = "0" ]; then + echo "This design holds no registers, so it has no clock domain and no achieved frequency can belong to it. For a combinational block the comparable figure is propagation delay, not a clock rate." >> report.md + else + echo "Sequential design — $POSEDGE clocked blocks. Achieved frequency is measurable and comes in the hardware stage." >> report.md + fi + + - name: Post the result + if: always() + uses: actions/github-script@v7 + env: + CLONABLE: ${{ steps.parse.outputs.clonable }} + with: + script: | + const fs = require('fs') + let body + if (process.env.CLONABLE !== 'yes') { + body = [ + '**No public repository given, so the automated stage was skipped.**', + '', + 'That is not a problem — it just means the run starts by hand. If the', + 'sources are public, edit the issue with a plain', + '`https://github.com/owner/repo` URL and the checks will run on their own.', + 'If the work is private, say so and an NDA comes first.', + ].join('\n') + } else { + let r = '' + try { r = fs.readFileSync('report.md', 'utf8') } catch (e) { r = '_The automated stage produced no report; picking this up by hand._' } + body = [ + '## Automated stage', + '', + r, + '', + '---', + '', + '**What is still to come, and why it is not automated.** The checks above', + 'tell you whether the design builds and whether it is structurally sound.', + 'They cannot tell you whether it computes the right answer. That needs a', + 'reference model written from your description of the operation rather than', + 'from your RTL, known-answer vectors at each pipeline stage, and a replay', + 'on the board — because agreement in simulation does not prove agreement', + 'on silicon.', + '', + 'Toolchain: `yosys`, `iverilog`. Every command above is in', + '`.github/workflows/verify-request.yml`, so you can re-run all of it.', + ].join('\n') + } + await github.rest.issues.createComment({ + owner: context.repo.owner, + repo: context.repo.repo, + issue_number: context.issue.number, + body, + }) diff --git a/apps/website/src/pages/HardwareVerification.tsx b/apps/website/src/pages/HardwareVerification.tsx index 0c966b088e..5710bc845b 100644 --- a/apps/website/src/pages/HardwareVerification.tsx +++ b/apps/website/src/pages/HardwareVerification.tsx @@ -7,6 +7,8 @@ import Navigation from '../components/Navigation' import Footer from '../components/Footer' import QuantumBackground from '../components/QuantumBackground' +const REQUEST_URL = 'https://github.com/gHashTag/trinity/issues/new?template=verification-request.yml' + const CONTACT = { email: 'admin@t27.ai', github: 'https://github.com/gHashTag', @@ -102,6 +104,13 @@ const STEPS = [ 'You get a signed report — measured numbers, vectors, bitstream, and every command needed to reproduce it.', ] +const AUTO_STEPS: [string, string, string][] = [ + ['minute 0', 'You open one issue', 'Where the RTL is, the top module, and what "correct" means for it. Nothing else.'], + ['minute 1', 'A bot acknowledges', 'So nobody is left wondering whether it arrived.'], + ['minute 5', 'Automated checks post back', 'Elaboration, latch check, synthesis, cell counts — publicly, with every command shown.'], + ['then', 'The part a bot cannot do', 'An independent reference model, per-stage vectors, and a replay on the board.'], +] + // Measured facts, not badges. Nothing here is a claim I cannot show the working for. const SIGNALS: [string, string][] = [ ['170,068', 'cycles in the last run'], @@ -124,6 +133,15 @@ const RELATED_RU = [ // Russian copy. Other locales fall back to English rather than showing gaps. const RU = { + autoTitle: 'Начать — без переписки', + autoLede: 'Открываете одну заявку. Робот подхватывает её, прогоняет проверки, которым человек не нужен, и в считаные минуты публикует результат — со всеми командами, чтобы вы могли перепроверить сами.', + autoSteps: [ + ['минута 0', 'Вы открываете заявку', 'Где RTL, какой топ-модуль и что для него значит «правильно». Больше ничего.'], + ['минута 1', 'Робот подтверждает', 'Чтобы не оставалось сомнений, дошло ли.'], + ['минута 5', 'Автопроверки публикуются', 'Элаборация, защёлки, синтез, счёт ячеек — открыто, со всеми командами.'], + ['дальше', 'То, что робот не может', 'Независимая эталонная модель, векторы по ступеням и повтор на плате.'], + ] as [string, string, string][], + autoCta: 'Открыть заявку', diagramTitle: 'Почему внешняя проверка может с вами не согласиться', signals: [ ['170 068', 'циклов в последнем прогоне'], @@ -223,7 +241,9 @@ export default function HardwareVerification() {

+ {/* How a request actually starts. Named plainly because "get in touch" + is the step most people never take. */} + +

+ {c ? c.autoTitle : 'No email thread to start it'} +

+

+ {c ? c.autoLede : 'Open one request. A bot picks it up, runs the checks that do not need a human, and posts the result back within minutes — publicly, with every command shown, so you can re-run it yourself.'} +

+
+ {(c ? c.autoSteps : AUTO_STEPS).map(([when, what, note], i) => ( +
+

+ {String(i + 1).padStart(2, '0')} · {when} +

+

{what}

+

{note}

+
+ ))} +
+ + {c ? c.autoCta : 'Open a request'} + + + {/* What you get */}