From 71354430be2b8e2f80bafc58261bd5d86885ede6 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Thu, 6 Aug 2026 20:49:01 +0700 Subject: [PATCH] feat(gen-verilog): land spec-first data ports + BitNet & GF-T hardware stack Now that master is unblocked (#1790), land the spec-first hardware work from 11 improvement cycles. Compiler: opt-in data ports -- `on_clock` var state exposed as `output reg`; `on_clock`/`on_comb` params become `input` data ports; `on_comb` return drives an `output wire result`. Seal-neutral (gated on on_clock/on_comb fn names, so existing specs are byte-identical). Specs (each iverilog + yosys + oracle cross-checked): - BitNet, synthesizes to Artix-7: comb_ternary_dot, comb_bitnet_neuron (a full neuron, ~319 LUT), comb_bitnet_layer, stream_ternary_mac (32 FDCE), clocked_counter. docs/SYNTH_REPORT.md. - GF-T, bit-exact to the AX7203 silicon: gft_dot2/dot4/dot8/layer2. - GF-T RNE, bit-exact to the ideal oracle (more accurate than the truncating silicon): gft_mul_rne, gft_add_rne, gft_dot2_rne. Verified: 1535 unit tests pass; all 12 spec tests green on master's compiler; FROZEN_HASH resealed; new-spec seals regenerated. Refs #1764 Co-Authored-By: Claude Opus 4.8 --- .trinity/seals/ternary_ClockedCounter.json | 6 +- .trinity/seals/ternary_CombBitnetLayer.json | 11 + .trinity/seals/ternary_CombBitnetNeuron.json | 11 + .trinity/seals/ternary_CombTernaryDot.json | 11 + .trinity/seals/ternary_GftAddRne.json | 11 + .trinity/seals/ternary_GftDot2.json | 11 + .trinity/seals/ternary_GftDot2Rne.json | 11 + .trinity/seals/ternary_GftDot4.json | 11 + .trinity/seals/ternary_GftDot8.json | 11 + .trinity/seals/ternary_GftLayer2.json | 11 + .trinity/seals/ternary_GftMulRne.json | 11 + .trinity/seals/ternary_StreamTernaryMac.json | 11 + bootstrap/src/compiler.rs | 125 +++++++- bootstrap/stage0/FROZEN_HASH | 2 +- bootstrap/tests/clocked_counter.rs | 34 +++ bootstrap/tests/comb_bitnet_layer.rs | 145 +++++++++ bootstrap/tests/comb_bitnet_neuron.rs | 143 +++++++++ bootstrap/tests/comb_ternary_dot.rs | 155 ++++++++++ bootstrap/tests/gft_add_rne.rs | 107 +++++++ bootstrap/tests/gft_add_rne_vectors.txt | 300 +++++++++++++++++++ bootstrap/tests/gft_dot2.rs | 224 ++++++++++++++ bootstrap/tests/gft_dot2_rne.rs | 108 +++++++ bootstrap/tests/gft_dot2_rne_vectors.txt | 300 +++++++++++++++++++ bootstrap/tests/gft_dot4.rs | 195 ++++++++++++ bootstrap/tests/gft_dot8.rs | 202 +++++++++++++ bootstrap/tests/gft_layer2.rs | 191 ++++++++++++ bootstrap/tests/gft_mul_rne.rs | 119 ++++++++ bootstrap/tests/gft_mul_rne_vectors.txt | 300 +++++++++++++++++++ bootstrap/tests/stream_ternary_mac.rs | 170 +++++++++++ docs/NOW.md | 17 ++ docs/SYNTH_REPORT.md | 58 ++++ specs/ternary/clocked_counter.t27 | 7 + specs/ternary/comb_bitnet_layer.t27 | 62 ++++ specs/ternary/comb_bitnet_neuron.t27 | 53 ++++ specs/ternary/comb_ternary_dot.t27 | 43 +++ specs/ternary/gft_add_rne.t27 | 66 ++++ specs/ternary/gft_dot2.t27 | 75 +++++ specs/ternary/gft_dot2_rne.t27 | 84 ++++++ specs/ternary/gft_dot4.t27 | 73 +++++ specs/ternary/gft_dot8.t27 | 76 +++++ specs/ternary/gft_layer2.t27 | 76 +++++ specs/ternary/gft_mul_rne.t27 | 55 ++++ specs/ternary/stream_ternary_mac.t27 | 52 ++++ 43 files changed, 3734 insertions(+), 10 deletions(-) create mode 100644 .trinity/seals/ternary_CombBitnetLayer.json create mode 100644 .trinity/seals/ternary_CombBitnetNeuron.json create mode 100644 .trinity/seals/ternary_CombTernaryDot.json create mode 100644 .trinity/seals/ternary_GftAddRne.json create mode 100644 .trinity/seals/ternary_GftDot2.json create mode 100644 .trinity/seals/ternary_GftDot2Rne.json create mode 100644 .trinity/seals/ternary_GftDot4.json create mode 100644 .trinity/seals/ternary_GftDot8.json create mode 100644 .trinity/seals/ternary_GftLayer2.json create mode 100644 .trinity/seals/ternary_GftMulRne.json create mode 100644 .trinity/seals/ternary_StreamTernaryMac.json create mode 100644 bootstrap/tests/comb_bitnet_layer.rs create mode 100644 bootstrap/tests/comb_bitnet_neuron.rs create mode 100644 bootstrap/tests/comb_ternary_dot.rs create mode 100644 bootstrap/tests/gft_add_rne.rs create mode 100644 bootstrap/tests/gft_add_rne_vectors.txt create mode 100644 bootstrap/tests/gft_dot2.rs create mode 100644 bootstrap/tests/gft_dot2_rne.rs create mode 100644 bootstrap/tests/gft_dot2_rne_vectors.txt create mode 100644 bootstrap/tests/gft_dot4.rs create mode 100644 bootstrap/tests/gft_dot8.rs create mode 100644 bootstrap/tests/gft_layer2.rs create mode 100644 bootstrap/tests/gft_mul_rne.rs create mode 100644 bootstrap/tests/gft_mul_rne_vectors.txt create mode 100644 bootstrap/tests/stream_ternary_mac.rs create mode 100644 docs/SYNTH_REPORT.md create mode 100644 specs/ternary/comb_bitnet_layer.t27 create mode 100644 specs/ternary/comb_bitnet_neuron.t27 create mode 100644 specs/ternary/comb_ternary_dot.t27 create mode 100644 specs/ternary/gft_add_rne.t27 create mode 100644 specs/ternary/gft_dot2.t27 create mode 100644 specs/ternary/gft_dot2_rne.t27 create mode 100644 specs/ternary/gft_dot4.t27 create mode 100644 specs/ternary/gft_dot8.t27 create mode 100644 specs/ternary/gft_layer2.t27 create mode 100644 specs/ternary/gft_mul_rne.t27 create mode 100644 specs/ternary/stream_ternary_mac.t27 diff --git a/.trinity/seals/ternary_ClockedCounter.json b/.trinity/seals/ternary_ClockedCounter.json index c438de61d2..8f17f272d5 100644 --- a/.trinity/seals/ternary_ClockedCounter.json +++ b/.trinity/seals/ternary_ClockedCounter.json @@ -1,11 +1,11 @@ { "gen_hash_c": "sha256:27383948b87cfb14a1fe5b5188e45317648d51530c9fe657090d5c6d8011b318", "gen_hash_rust": "sha256:ad02e62fbac89c519bd4b82b2ec3b8a5a24f76a0426f582ba831ecc965b462ac", - "gen_hash_verilog": "sha256:980820ea0014f837f8fb8c021390947973dec556dfb6ef925c6b6810bce0905b", + "gen_hash_verilog": "sha256:742baa2af5542beb3dd9bdaabf60865eb8324ed71cf707ec25ee685d7af62dd4", "gen_hash_zig": "sha256:b4847252ab51690dc65b288a7f7d95840a4aa31ff87ee8b9b2d0c268273c13d0", "module": "ClockedCounter", "ring": 12, - "sealed_at": "2026-08-06T10:43:39Z", - "spec_hash": "sha256:0bdf30370bf761b681d0745630e46dcab0e8f7cf7b59242041ac815a48f09d80", + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:12a5bb8e6d0975bfd72b3520ac83e9adaa6f52371be8ef101ef5fd39b8fcbf6f", "spec_path": "specs/ternary/clocked_counter.t27" } \ No newline at end of file diff --git a/.trinity/seals/ternary_CombBitnetLayer.json b/.trinity/seals/ternary_CombBitnetLayer.json new file mode 100644 index 0000000000..eebd985687 --- /dev/null +++ b/.trinity/seals/ternary_CombBitnetLayer.json @@ -0,0 +1,11 @@ +{ + "gen_hash_c": "sha256:095e6072c93b91f7e343bc517ddfb8063d263ebc78e44ea70b3ec3a40eaddf58", + "gen_hash_rust": "sha256:b3b29fdd87187b06ca8f5e5b93e15676bda76e2f5236322f3f713713e6d2e793", + "gen_hash_verilog": "sha256:e4faca797bec20c0727d344c20df3af8cac748004f86f5da17903b4f6ba32e1e", + "gen_hash_zig": "sha256:cd371cffeb09a87c3fb7bb60d04d3515c1e8d1de9385071fc5a002e92f65f4a9", + "module": "CombBitnetLayer", + "ring": 12, + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:105570e1b9856293381a0dd3a7365177b880aaf561e8659f5d50e240a593b5be", + "spec_path": "specs/ternary/comb_bitnet_layer.t27" +} \ No newline at end of file diff --git a/.trinity/seals/ternary_CombBitnetNeuron.json b/.trinity/seals/ternary_CombBitnetNeuron.json new file mode 100644 index 0000000000..059ecae445 --- /dev/null +++ b/.trinity/seals/ternary_CombBitnetNeuron.json @@ -0,0 +1,11 @@ +{ + "gen_hash_c": "sha256:335a4d8f9a1b96197475cc2e0ddcb3ed47a6c4edd7ae2b7222696fb579bfacbb", + "gen_hash_rust": "sha256:6aac52806028636740c4dd181f13cccc1c2bcadce38e097483feeb3766c35446", + "gen_hash_verilog": "sha256:bb061aa2c56bdf386892b89ee8f13e44d73d32eca928f7eec7d3850b588e20bc", + "gen_hash_zig": "sha256:8545d117bb4a1a5a2cd71fb2234ef14fd7b1ad0bfd34ba2ee76e5bf65af984b5", + "module": "CombBitnetNeuron", + "ring": 12, + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:85e9e5f9206e17a924e9ae7f2a7c79a62cce17f06327cf1abdf424efaba6cf41", + "spec_path": "specs/ternary/comb_bitnet_neuron.t27" +} \ No newline at end of file diff --git a/.trinity/seals/ternary_CombTernaryDot.json b/.trinity/seals/ternary_CombTernaryDot.json new file mode 100644 index 0000000000..f59dbaeecf --- /dev/null +++ b/.trinity/seals/ternary_CombTernaryDot.json @@ -0,0 +1,11 @@ +{ + "gen_hash_c": "sha256:fd30c50e9bed7a74880a3b911641d1c8869385fc6ad4a14668ebe0d647b80f3d", + "gen_hash_rust": "sha256:747428b2be42fbd2cc4c14d172e56a2323dc1f1766b1ec688c437a7c39d6f5c2", + "gen_hash_verilog": "sha256:3936e13b234c20b7dc7daf2332adb4e27afeef049ebeaaa392a4c4b4facf6244", + "gen_hash_zig": "sha256:a06c6c9a385a07db9123a69f5b423966aacbac91a7d226744361a2c1b27d5bc1", + "module": "CombTernaryDot", + "ring": 12, + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:1cb1bf87cd3f9cb92778ec47f85d079c6514ad532a7f8ee777481dd031ba4651", + "spec_path": "specs/ternary/comb_ternary_dot.t27" +} \ No newline at end of file diff --git a/.trinity/seals/ternary_GftAddRne.json b/.trinity/seals/ternary_GftAddRne.json new file mode 100644 index 0000000000..770a2b3b2b --- /dev/null +++ b/.trinity/seals/ternary_GftAddRne.json @@ -0,0 +1,11 @@ +{ + "gen_hash_c": "sha256:30292b82d55be23fa5952775ceb0dbded3c6f051dc929f937c7e6dfe3909ab77", + "gen_hash_rust": "sha256:bb4c89d4ddddc8892a470ccd47025767e7b66de5dc4ec00fff056e273f8977d4", + "gen_hash_verilog": "sha256:88b310292720be7be01e98c15ae63615547d39646e758de51867612fb14268cc", + "gen_hash_zig": "sha256:c4e780d9cc0139bff7a2b73b4f6ad5bab6103205d8655b4b911ed4695224d44d", + "module": "GftAddRne", + "ring": 12, + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:e900a1f93f9d85ab1c55a4492f61134eee0720787e2cc59a88890e6120a7ee87", + "spec_path": "specs/ternary/gft_add_rne.t27" +} \ No newline at end of file diff --git a/.trinity/seals/ternary_GftDot2.json b/.trinity/seals/ternary_GftDot2.json new file mode 100644 index 0000000000..507cd8f776 --- /dev/null +++ b/.trinity/seals/ternary_GftDot2.json @@ -0,0 +1,11 @@ +{ + "gen_hash_c": "sha256:9072ef283a9f55147e7fb63f581b53262d520f110ab9d78ac61169a90ab7a5d0", + "gen_hash_rust": "sha256:99b540c4468bd1e8eefc039dfbeabfbd9d7af347ede035242c7a224bb6b3112e", + "gen_hash_verilog": "sha256:14682c77fe6fdec9656828145c2b41e23e30a78524bd9c9fde370424f5ba7276", + "gen_hash_zig": "sha256:b654810ab7356b4b170a6405d1b904ee9c8e4d20efcc98004b430ae7d291022e", + "module": "GftDot2", + "ring": 12, + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:b99c892c8a0fdcd11528ddd0ca8d52d8646e0c9b1ce420ae16610e8ede3de5c4", + "spec_path": "specs/ternary/gft_dot2.t27" +} \ No newline at end of file diff --git a/.trinity/seals/ternary_GftDot2Rne.json b/.trinity/seals/ternary_GftDot2Rne.json new file mode 100644 index 0000000000..f3c443f211 --- /dev/null +++ b/.trinity/seals/ternary_GftDot2Rne.json @@ -0,0 +1,11 @@ +{ + "gen_hash_c": "sha256:e6dc470045a17a719de37b6b59ffea70be28dd306b109ba8e1a5356638157409", + "gen_hash_rust": "sha256:d83583ec1d4a03405e2f88e6b67b4fcc1281de2b215a12bf43e9788002133b1a", + "gen_hash_verilog": "sha256:73abfbc1ed5cc595f6677c120dcd05b2c5aa0f4b832060f95f6810b29a96da39", + "gen_hash_zig": "sha256:146a0646e204d523da04197b83989202071cf60c73addfb68291407fc9c131ae", + "module": "GftDot2Rne", + "ring": 12, + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:be0e54b47c9cef2d0f3338635e692dfc3afe66258a0b9c9fdbb95cce022309d8", + "spec_path": "specs/ternary/gft_dot2_rne.t27" +} \ No newline at end of file diff --git a/.trinity/seals/ternary_GftDot4.json b/.trinity/seals/ternary_GftDot4.json new file mode 100644 index 0000000000..35ec2faa23 --- /dev/null +++ b/.trinity/seals/ternary_GftDot4.json @@ -0,0 +1,11 @@ +{ + "gen_hash_c": "sha256:bf46c20be049d23ad8a43674b919d9a3f5f7ae4921e678f753824331d5764c94", + "gen_hash_rust": "sha256:7f94ab7756a758d4cc6869dce46ad17b084d64a9b89620b4dcd6f7610f40ca1f", + "gen_hash_verilog": "sha256:686c9dbf0b86f11498309f986825f59650c6f690b18b3ad9646c691fb4ed8e04", + "gen_hash_zig": "sha256:c764491d15be4c5df0810cf9b59d2dca43d68059f4e3d54a7bf441e3065f8b03", + "module": "GftDot4", + "ring": 12, + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:4e80040a11ab6ae72d46b8d4487959caa396ddde34d00ebe15ecef1f4bbbb9ed", + "spec_path": "specs/ternary/gft_dot4.t27" +} \ No newline at end of file diff --git a/.trinity/seals/ternary_GftDot8.json b/.trinity/seals/ternary_GftDot8.json new file mode 100644 index 0000000000..2a66049fb0 --- /dev/null +++ b/.trinity/seals/ternary_GftDot8.json @@ -0,0 +1,11 @@ +{ + "gen_hash_c": "sha256:06ba4cad93adba5600c3a3c4d4d97d6347b88cb5e03c5a4a70451c26ba92e012", + "gen_hash_rust": "sha256:5b35b84c39af10f82ac9988c180306a9bd85ae393b06647c9bced6117a2fcc06", + "gen_hash_verilog": "sha256:f8bf84c8a793d9a39bfc2c37be27c8a9fe48c176cbcada92ff8c7d7af2e4e28c", + "gen_hash_zig": "sha256:4d8a3ad5d803c92076d0666838f1f2ec2fbc837662a157714cba8e868b6ef6d6", + "module": "GftDot8", + "ring": 12, + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:2d9ab503fe27887ed2f276cca7e093e3e017547d591f875a457a69bd58647f01", + "spec_path": "specs/ternary/gft_dot8.t27" +} \ No newline at end of file diff --git a/.trinity/seals/ternary_GftLayer2.json b/.trinity/seals/ternary_GftLayer2.json new file mode 100644 index 0000000000..25ea4c92a7 --- /dev/null +++ b/.trinity/seals/ternary_GftLayer2.json @@ -0,0 +1,11 @@ +{ + "gen_hash_c": "sha256:aeff0798c4375a3611554e7435f2f4f8f4a3f01e4da5fd1e6fd8657dd1b43027", + "gen_hash_rust": "sha256:77c1337c41161123a28bca8fc3cb85a521181702c62b78b6c79293b1a01e10be", + "gen_hash_verilog": "sha256:93baf008efbdc1215d2f887945ef2980b76a5f61c4f0e411830948b1a971d969", + "gen_hash_zig": "sha256:0ec32b741911475de3160677c669ecb818c192f52933959e8753663b77859123", + "module": "GftLayer2", + "ring": 12, + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:35a33a43c6ba2669c285f757c838ae44d8cd5028598ff7912370383a41ee7133", + "spec_path": "specs/ternary/gft_layer2.t27" +} \ No newline at end of file diff --git a/.trinity/seals/ternary_GftMulRne.json b/.trinity/seals/ternary_GftMulRne.json new file mode 100644 index 0000000000..c6392d9fe8 --- /dev/null +++ b/.trinity/seals/ternary_GftMulRne.json @@ -0,0 +1,11 @@ +{ + "gen_hash_c": "sha256:c5dc68c01c9f66810431684dad2ed0dfe6db9267d06afa6e79dbf437aaccc062", + "gen_hash_rust": "sha256:bb1b28ae1841154247b3e794bd359fcdc92c840ed1bf636ca994a24cb4e891d3", + "gen_hash_verilog": "sha256:feee808883e376fdbabeb5fc51639497d91cf0bc2b704adec4383d0e53d81dab", + "gen_hash_zig": "sha256:aff1d546b1386dcfa7ff370d481636c1817382fbf87efd50bac2f21ce6db9c14", + "module": "GftMulRne", + "ring": 12, + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:d16bedfa83646e9e9df60e17c51928fabe4240cb5ca15ac682369f4dcc9fd9a6", + "spec_path": "specs/ternary/gft_mul_rne.t27" +} \ No newline at end of file diff --git a/.trinity/seals/ternary_StreamTernaryMac.json b/.trinity/seals/ternary_StreamTernaryMac.json new file mode 100644 index 0000000000..9788bee114 --- /dev/null +++ b/.trinity/seals/ternary_StreamTernaryMac.json @@ -0,0 +1,11 @@ +{ + "gen_hash_c": "sha256:f553ebdccd96b21d0ee140c3ede653ad4b13d8b3ee84af5f35743c130b7b5d63", + "gen_hash_rust": "sha256:0f6c4b2bb6cffb751322bc797df1701ac6c5048523dadb22282e2b550e1e395f", + "gen_hash_verilog": "sha256:48a0e07aae8a39a3dd62a323312143cef6efa160ae7da28c6031bf7a7e41685f", + "gen_hash_zig": "sha256:6f659088bd546472e7e3db64ea64ac431a5ab30d7800d04e564b639916e99326", + "module": "StreamTernaryMac", + "ring": 12, + "sealed_at": "2026-08-06T13:47:37Z", + "spec_hash": "sha256:f46c60b0ba669110f8cf4a169987c7c2e794b317bd6889f0e90e40cfcb158632", + "spec_path": "specs/ternary/stream_ternary_mac.t27" +} \ No newline at end of file diff --git a/bootstrap/src/compiler.rs b/bootstrap/src/compiler.rs index b432e2d2e0..c75ccfca03 100644 --- a/bootstrap/src/compiler.rs +++ b/bootstrap/src/compiler.rs @@ -4067,6 +4067,10 @@ pub struct VerilogCodegen { // assignment (`<=`) instead of a blocking one, so a clocked `fn on_clock` // body lowers to correct sequential logic inside an `always @(posedge clk)`. clocked_nonblocking: bool, + // Scalar module-level `var`s exposed as `output reg` data ports (only in a + // clocked module -- one with an `on_clock` fn). Their body `reg` declaration + // is suppressed because the ANSI port header already declares them. + exposed_output_vars: std::collections::HashSet, // Width of the parameters of the function currently being lowered, keyed by // parameter name. Populated in `gen_verilog_fn`. Used by `ExprCast` lowering // to skip a redundant truncation mask when the operand is a parameter that is @@ -4146,6 +4150,7 @@ impl VerilogCodegen { current_fn_return_type: String::new(), hoist_fn_locals: false, clocked_nonblocking: false, + exposed_output_vars: std::collections::HashSet::new(), param_widths: std::collections::HashMap::new(), struct_decls: std::collections::HashMap::new(), local_types: std::collections::HashMap::new(), @@ -5487,6 +5492,7 @@ impl VerilogCodegen { current_fn_return_type: String::new(), hoist_fn_locals: false, clocked_nonblocking: false, + exposed_output_vars: std::collections::HashSet::new(), param_widths: self.param_widths.clone(), struct_decls: self.struct_decls.clone(), local_types: self.local_types.clone(), @@ -5655,6 +5661,7 @@ impl VerilogCodegen { current_fn_return_type: String::new(), hoist_fn_locals: false, clocked_nonblocking: false, + exposed_output_vars: std::collections::HashSet::new(), param_widths: self.param_widths.clone(), struct_decls: self.struct_decls.clone(), local_types: self.local_types.clone(), @@ -6187,6 +6194,52 @@ impl VerilogCodegen { // Emit top-level module let mod_name = self.module_name.clone(); + // #1764: in a clocked module (an `on_clock` fn is present) the registered + // scalar `var`s ARE the module's observable state. Expose each as an + // `output reg` data port so the design synthesizes to real flip-flops + // instead of being dead-code-eliminated (yosys DCEs a port-less design to + // zero cells). Gated on `on_clock`, so non-clocked specs -- and every + // existing spec -- keep the byte-identical `(clk,rst_n,en,ready)` header. + let has_on_clock = functions.iter().any(|f| f.name == "on_clock"); + self.exposed_output_vars.clear(); + let mut exposed_ports: Vec<(String, usize, bool)> = Vec::new(); + if has_on_clock { + for c in &consts { + let is_scalar = Self::parse_array_type(&c.extra_type).is_none() + && !Self::is_primitive_array_type(&c.extra_type) + && !self.struct_decls.contains_key(&c.extra_type); + if c.extra_mutable && is_scalar { + let w = Self::type_to_width(&c.extra_type) as usize; + let signed = Self::type_is_signed(&c.extra_type); + exposed_ports.push((c.name.clone(), w, signed)); + self.exposed_output_vars.insert(c.name.clone()); + } + } + } + // #1764: the parameters of `on_clock` (streaming) or `on_comb` + // (combinational) become INPUT data ports, so a spec can consume data fed + // in on real ports (`fn on_clock(x: i16) {...}` -> `input signed [15:0] x`). + // Only present when such a fn takes params -> existing specs unchanged. + let mut input_ports: Vec<(String, u32, bool)> = Vec::new(); + if let Some(oc) = functions.iter().find(|f| f.name == "on_clock" || f.name == "on_comb") { + for (pname, ptype) in &oc.params { + let w = Self::type_to_width(ptype); + let signed = Self::type_is_signed(ptype); + input_ports.push((pname.clone(), w, signed)); + } + } + // `on_comb` is the combinational counterpart of `on_clock`: its return is a + // continuously-driven `output wire result` (`assign result = on_comb(...)`), + // so a purely combinational spec (dot27, an adder, a whole MLP) synthesizes + // to real LUTs instead of being dead-code-eliminated. Only when defined. + let comb_result: Option<(u32, bool, Vec)> = + functions.iter().find(|f| f.name == "on_comb").map(|f| { + let w = Self::type_to_width(&f.extra_return_type); + let signed = Self::type_is_signed(&f.extra_return_type); + let params: Vec = f.params.iter().map(|(p, _)| p.clone()).collect(); + (w, signed, params) + }); + self.write_line(&format!("module {} (", mod_name)); self.indent(); self.write_indent(); @@ -6195,8 +6248,46 @@ impl VerilogCodegen { self.write_line("input wire rst_n,"); self.write_indent(); self.write_line("input wire en,"); + for (name, w, signed) in &input_ports { + let range = Self::range_decl(*w); + let signed_str = if *signed { "signed " } else { "" }; + self.write_indent(); + if range.is_empty() { + self.write_line(&format!("input wire {}{},", signed_str, name)); + } else { + self.write_line(&format!("input wire {}{} {},", signed_str, range, name)); + } + } self.write_indent(); - self.write_line("output wire ready"); + let n_extra_out = exposed_ports.len() + if comb_result.is_some() { 1 } else { 0 }; + if n_extra_out == 0 { + self.write_line("output wire ready"); + } else { + self.write_line("output wire ready,"); + let mut emitted = 0; + for (name, w, signed) in &exposed_ports { + let range = Self::range_decl(*w as u32); + let signed_str = if *signed { "signed " } else { "" }; + emitted += 1; + let comma = if emitted < n_extra_out { "," } else { "" }; + self.write_indent(); + if range.is_empty() { + self.write_line(&format!("output reg {}{}{}", signed_str, name, comma)); + } else { + self.write_line(&format!("output reg {}{} {}{}", signed_str, range, name, comma)); + } + } + if let Some((w, signed, _)) = &comb_result { + let range = Self::range_decl(*w); + let signed_str = if *signed { "signed " } else { "" }; + self.write_indent(); + if range.is_empty() { + self.write_line(&format!("output wire {}result", signed_str)); + } else { + self.write_line(&format!("output wire {}{} result", signed_str, range)); + } + } + } self.dedent(); self.write_line(");"); self.write_line(""); @@ -6329,6 +6420,13 @@ impl VerilogCodegen { for f in &clocked { self.gen_verilog_clocked_fn(f, &consts); } + // `on_comb`: continuously drive the `result` output port from the + // combinational function of the input data ports. + if let Some((_, _, params)) = &comb_result { + self.write_line(""); + self.write_indent(); + self.write_line(&format!("assign result = on_comb({});", params.join(", "))); + } // Section: Module-level statements (e.g. calls to array-param functions) if !module_stmts.is_empty() { @@ -7112,11 +7210,17 @@ impl VerilogCodegen { self.write_line("end"); } } else { - self.write(&format!( - "reg {}{}{};", - signed_str, range_str, safe_name - )); - self.write_line(""); + // An exposed output-reg var is already declared in the ANSI port + // header; emit only its power-on initializer here. + if self.exposed_output_vars.contains(&node.name) { + self.write_line(&format!("// {} exposed as output reg port", node.name)); + } else { + self.write(&format!( + "reg {}{}{};", + signed_str, range_str, safe_name + )); + self.write_line(""); + } if !node.children.is_empty() { self.write_indent(); self.write_line("initial begin"); @@ -7390,6 +7494,14 @@ impl VerilogCodegen { self.current_fn_name = node.name.clone(); self.local_types.clear(); self.param_types.clear(); + self.param_widths.clear(); + // `on_clock` params are streaming input data ports; register their widths + // and types so body references (casts, width-aware ops) resolve. + for (pname, ptype) in &node.params { + self.param_widths + .insert(pname.clone(), self.packed_width(ptype) as usize); + self.param_types.insert(pname.clone(), ptype.clone()); + } // Mirror gen_verilog_fn: cache any body-local variable types. for stmt in &node.children { if stmt.kind == NodeKind::StmtLocal && !stmt.name.is_empty() { @@ -7438,6 +7550,7 @@ impl VerilogCodegen { self.current_fn_name.clear(); self.local_types.clear(); self.param_types.clear(); + self.param_widths.clear(); } /// Emit a Verilog function body statement list, rewriting the diff --git a/bootstrap/stage0/FROZEN_HASH b/bootstrap/stage0/FROZEN_HASH index 356f391521..a27803db31 100644 --- a/bootstrap/stage0/FROZEN_HASH +++ b/bootstrap/stage0/FROZEN_HASH @@ -1 +1 @@ -6607d41cbc98f18867814aad647587ba3d3c4d50b134c16a9683c4137c82752c +de57378ec0e294016ced91ad6976f19f73cf71ae3cf4db93f210bf754bdc9c6f diff --git a/bootstrap/tests/clocked_counter.rs b/bootstrap/tests/clocked_counter.rs index c214411895..31158d4d8f 100644 --- a/bootstrap/tests/clocked_counter.rs +++ b/bootstrap/tests/clocked_counter.rs @@ -103,6 +103,40 @@ fn spec_first_on_clock_registers_state() { "clocked var was not updated with a nonblocking assignment:\n{}", verilog ); + // The registered state must be exposed as a data output port -- otherwise a + // synthesizer dead-code-eliminates the whole design to zero cells (nothing + // observable drives an output). This is the difference between a simulation + // artifact and real hardware. + assert!( + verilog.contains("output reg [7:0] count"), + "clocked var `count` was not exposed as an output data port:\n{}", + verilog + ); + + // If yosys is available, prove the design synthesizes to REAL Artix-7 + // hardware -- the 8-bit register must map to flip-flops, not vanish. + if tool_available("yosys") { + let dir = scratch_dir("synth"); + fs::create_dir_all(&dir).expect("create synth dir"); + fs::write(dir.join("cc.v"), &gen.stdout).expect("write cc.v"); + let synth = Command::new("yosys") + .arg("-p") + .arg(format!( + "read_verilog -sv {}; synth_xilinx -top ClockedCounter; stat", + dir.join("cc.v").to_str().unwrap() + )) + .output() + .expect("invoke yosys"); + let s = String::from_utf8_lossy(&synth.stdout).into_owned() + + &String::from_utf8_lossy(&synth.stderr); + let _ = fs::remove_dir_all(&dir); + assert!(synth.status.success(), "yosys synth_xilinx failed:\n{}", s); + assert!( + s.contains("FDCE") || s.contains("FDRE") || s.contains("FDPE") || s.contains("FDSE"), + "synth produced no flip-flops -- the register was optimized away:\n{}", + s + ); + } if !tool_available("iverilog") || !tool_available("vvp") { eprintln!("SKIP: iverilog/vvp not on PATH; skipping clocked simulation"); diff --git a/bootstrap/tests/comb_bitnet_layer.rs b/bootstrap/tests/comb_bitnet_layer.rs new file mode 100644 index 0000000000..b4f9f4d3b4 --- /dev/null +++ b/bootstrap/tests/comb_bitnet_layer.rs @@ -0,0 +1,145 @@ +// ============================================================================ +// Check for the spec-first combinational BitNet LAYER (specs/ternary/ +// comb_bitnet_layer.t27, #1764): four neurons over a shared 27-trit activation, +// each with its own fixed weight vector, trits packed 2 bits each into the +// `result` output. Verifies the activation input port + packed output port; that +// (with yosys) it synthesizes to real Artix-7 LUTs with NO flip-flops; and that +// (with iverilog) the packed layer output matches the hand-computed responses +// to the canonical all-P / all-N / all-Z activations. +// ============================================================================ + +use std::env; +use std::fs; +use std::path::PathBuf; +use std::process::Command; + +fn t27c() -> &'static str { + env!("CARGO_BIN_EXE_t27c") +} + +fn spec_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("..") + .join("specs") + .join("ternary") + .join("comb_bitnet_layer.t27") +} + +fn scratch_dir(label: &str) -> PathBuf { + let dir = env::temp_dir().join(format!("t27_layer_{}_{}", std::process::id(), label)); + if dir.exists() { + let _ = fs::remove_dir_all(&dir); + } + dir +} + +fn tool_available(tool: &str) -> bool { + Command::new(tool) + .arg("-V") + .output() + .map(|o| o.status.success()) + .unwrap_or(false) +} + +// Weights = all+1, all-1, all0, all+1. Response to canonical activations: +// a=all+1 -> dots +27,-27,0,+27 -> P,N,Z,P -> 2|0<<2|1<<4|2<<6 = 146 +// a=all-1 -> dots -27,+27,0,-27 -> N,P,Z,N -> 0|2<<2|1<<4|0<<6 = 24 +// a=all0 -> all dots 0 -> Z,Z,Z,Z -> 1|1<<2|1<<4|1<<6 = 85 +const TESTBENCH: &str = r#"`timescale 1ns/1ps +module tb; + reg [63:0] a; wire [7:0] result; integer fails; + CombBitnetLayer dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.a(a),.ready(),.result(result)); + task chk(input [63:0] av,input integer exp); begin + a=av;#1; + if(result!==exp)begin fails=fails+1;$display("FAIL a=%h result=%0d exp=%0d",av,result,exp);end + end endtask + initial begin + fails=0; + chk(64'd12009599006321322,146); + chk(64'd0,24); + chk(64'd6004799503160661,85); + if(fails==0)$display("ALL_PASS");else $display("FAILED %0d",fails); + $finish; + end +endmodule +"#; + +#[test] +fn spec_first_combinational_bitnet_layer() { + let gen = Command::new(t27c()) + .arg("gen-verilog") + .arg(spec_path()) + .output() + .expect("invoke gen-verilog"); + assert!( + gen.status.success(), + "gen-verilog of comb_bitnet_layer.t27 failed:\n{}", + String::from_utf8_lossy(&gen.stderr) + ); + let verilog = String::from_utf8_lossy(&gen.stdout).into_owned(); + + assert!( + verilog.contains("input wire [63:0] a"), + "layer activation did not become an input data port:\n{}", + verilog + ); + assert!( + verilog.contains("output wire [7:0] result") + && verilog.contains("assign result = on_comb(a);"), + "layer output is not driven on the result port:\n{}", + verilog + ); + + if tool_available("yosys") { + let dir = scratch_dir("synth"); + fs::create_dir_all(&dir).expect("create synth dir"); + fs::write(dir.join("l.v"), &gen.stdout).expect("write l.v"); + let synth = Command::new("yosys") + .arg("-p") + .arg(format!( + "read_verilog -sv {}; synth_xilinx -top CombBitnetLayer; stat", + dir.join("l.v").to_str().unwrap() + )) + .output() + .expect("invoke yosys"); + let s = String::from_utf8_lossy(&synth.stdout).into_owned() + + &String::from_utf8_lossy(&synth.stderr); + let _ = fs::remove_dir_all(&dir); + assert!(synth.status.success(), "yosys synth_xilinx failed:\n{}", s); + assert!(s.contains("LUT"), "layer produced no LUTs:\n{}", s); + } + + if !tool_available("iverilog") || !tool_available("vvp") { + eprintln!("SKIP: iverilog/vvp not on PATH; skipping layer simulation"); + return; + } + + let dir = scratch_dir("chk"); + fs::create_dir_all(&dir).expect("create scratch dir"); + fs::write(dir.join("l.v"), &gen.stdout).expect("write l.v"); + fs::write(dir.join("tb.v"), TESTBENCH).expect("write tb.v"); + + let vvp_path = dir.join("sim.vvp"); + let compile = Command::new("iverilog") + .args(["-g2012", "-o", vvp_path.to_str().unwrap()]) + .arg(dir.join("l.v")) + .arg(dir.join("tb.v")) + .output() + .expect("invoke iverilog"); + assert!( + compile.status.success(), + "iverilog compile failed:\n{}", + String::from_utf8_lossy(&compile.stderr) + ); + + let run = Command::new("vvp").arg(&vvp_path).output().expect("invoke vvp"); + let stdout = String::from_utf8_lossy(&run.stdout).into_owned(); + let _ = fs::remove_dir_all(&dir); + + assert!( + stdout.contains("ALL_PASS"), + "layer did not produce the expected packed trit outputs:\n{}", + stdout + ); + assert!(!stdout.contains("FAIL"), "layer mismatch:\n{}", stdout); +} diff --git a/bootstrap/tests/comb_bitnet_neuron.rs b/bootstrap/tests/comb_bitnet_neuron.rs new file mode 100644 index 0000000000..26e89fab2c --- /dev/null +++ b/bootstrap/tests/comb_bitnet_neuron.rs @@ -0,0 +1,143 @@ +// ============================================================================ +// Check for the spec-first combinational BitNet NEURON (specs/ternary/ +// comb_bitnet_neuron.t27, #1764): `on_comb(a, b) = quantize(dot27(a, b))` -- +// a full neuron over one 27-trit chunk (weighted ternary sum -> sign) in a +// single combinational module. Verifies input ports a, b + output port result; +// that (with yosys) it synthesizes to real Artix-7 LUTs with NO flip-flops; and +// that (with iverilog) result == quantize(dot27(a,b)) for known trit vectors. +// ============================================================================ + +use std::env; +use std::fs; +use std::path::PathBuf; +use std::process::Command; + +fn t27c() -> &'static str { + env!("CARGO_BIN_EXE_t27c") +} + +fn spec_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("..") + .join("specs") + .join("ternary") + .join("comb_bitnet_neuron.t27") +} + +fn scratch_dir(label: &str) -> PathBuf { + let dir = env::temp_dir().join(format!("t27_neuron_{}_{}", std::process::id(), label)); + if dir.exists() { + let _ = fs::remove_dir_all(&dir); + } + dir +} + +fn tool_available(tool: &str) -> bool { + Command::new(tool) + .arg("-V") + .output() + .map(|o| o.status.success()) + .unwrap_or(false) +} + +// result = quantize(dot27(a,b)): +sum -> P(2), -sum -> N(0), 0 -> Z(1). +const TESTBENCH: &str = r#"`timescale 1ns/1ps +module tb; + reg [63:0] a,b; wire [7:0] result; integer fails; + CombBitnetNeuron dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.a(a),.b(b),.ready(),.result(result)); + task chk(input [63:0] av,input [63:0] bv,input integer exp); begin + a=av;b=bv;#1; + if(result!==exp)begin fails=fails+1;$display("FAIL a=%h b=%h r=%0d exp=%0d",av,bv,result,exp);end + end endtask + initial begin + fails=0; + chk(64'd0,64'd0,2); + chk(64'd12009599006321322,64'd12009599006321322,2); + chk(64'd0,64'd12009599006321322,0); + chk(64'd6004799503160661,64'd6004799503160661,1); + if(fails==0)$display("ALL_PASS");else $display("FAILED %0d",fails); + $finish; + end +endmodule +"#; + +#[test] +fn spec_first_combinational_bitnet_neuron() { + let gen = Command::new(t27c()) + .arg("gen-verilog") + .arg(spec_path()) + .output() + .expect("invoke gen-verilog"); + assert!( + gen.status.success(), + "gen-verilog of comb_bitnet_neuron.t27 failed:\n{}", + String::from_utf8_lossy(&gen.stderr) + ); + let verilog = String::from_utf8_lossy(&gen.stdout).into_owned(); + + assert!( + verilog.contains("input wire [63:0] a") && verilog.contains("input wire [63:0] b"), + "neuron inputs did not become data ports:\n{}", + verilog + ); + assert!( + verilog.contains("output wire [7:0] result") + && verilog.contains("assign result = on_comb(a, b);"), + "neuron activation is not driven on the result output port:\n{}", + verilog + ); + + // Synthesizes to real combinational Artix-7 fabric: LUTs, and NO flip-flops. + if tool_available("yosys") { + let dir = scratch_dir("synth"); + fs::create_dir_all(&dir).expect("create synth dir"); + fs::write(dir.join("n.v"), &gen.stdout).expect("write n.v"); + let synth = Command::new("yosys") + .arg("-p") + .arg(format!( + "read_verilog -sv {}; synth_xilinx -top CombBitnetNeuron; stat", + dir.join("n.v").to_str().unwrap() + )) + .output() + .expect("invoke yosys"); + let s = String::from_utf8_lossy(&synth.stdout).into_owned() + + &String::from_utf8_lossy(&synth.stderr); + let _ = fs::remove_dir_all(&dir); + assert!(synth.status.success(), "yosys synth_xilinx failed:\n{}", s); + assert!(s.contains("LUT"), "neuron produced no LUTs:\n{}", s); + } + + if !tool_available("iverilog") || !tool_available("vvp") { + eprintln!("SKIP: iverilog/vvp not on PATH; skipping neuron simulation"); + return; + } + + let dir = scratch_dir("chk"); + fs::create_dir_all(&dir).expect("create scratch dir"); + fs::write(dir.join("n.v"), &gen.stdout).expect("write n.v"); + fs::write(dir.join("tb.v"), TESTBENCH).expect("write tb.v"); + + let vvp_path = dir.join("sim.vvp"); + let compile = Command::new("iverilog") + .args(["-g2012", "-o", vvp_path.to_str().unwrap()]) + .arg(dir.join("n.v")) + .arg(dir.join("tb.v")) + .output() + .expect("invoke iverilog"); + assert!( + compile.status.success(), + "iverilog compile failed:\n{}", + String::from_utf8_lossy(&compile.stderr) + ); + + let run = Command::new("vvp").arg(&vvp_path).output().expect("invoke vvp"); + let stdout = String::from_utf8_lossy(&run.stdout).into_owned(); + let _ = fs::remove_dir_all(&dir); + + assert!( + stdout.contains("ALL_PASS"), + "neuron did not compute quantize(dot27(a,b)):\n{}", + stdout + ); + assert!(!stdout.contains("FAIL"), "neuron mismatch:\n{}", stdout); +} diff --git a/bootstrap/tests/comb_ternary_dot.rs b/bootstrap/tests/comb_ternary_dot.rs new file mode 100644 index 0000000000..4e0b90c8a5 --- /dev/null +++ b/bootstrap/tests/comb_ternary_dot.rs @@ -0,0 +1,155 @@ +// ============================================================================ +// Check for the spec-first COMBINATIONAL data interface (specs/ternary/ +// comb_ternary_dot.t27, `on_comb`, #1764). `on_comb`'s params become input +// data ports and its return is a continuously-driven `output wire result` +// (`assign result = on_comb(...)`), so a purely combinational spec synthesizes +// to real LUTs instead of being dead-code-eliminated to zero cells. +// +// Here `on_comb` is the bit-exact 27-trit dot product. Verifies the generated +// module has input ports a, b and an output port `result`; that (with yosys) it +// synthesizes to real Artix-7 LUTs; and that (with iverilog) `result` equals the +// dot product for known trit vectors. Skips the tool legs when tools are absent. +// ============================================================================ + +use std::env; +use std::fs; +use std::path::PathBuf; +use std::process::Command; + +fn t27c() -> &'static str { + env!("CARGO_BIN_EXE_t27c") +} + +fn spec_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("..") + .join("specs") + .join("ternary") + .join("comb_ternary_dot.t27") +} + +fn scratch_dir(label: &str) -> PathBuf { + let dir = env::temp_dir().join(format!("t27_cdot_{}_{}", std::process::id(), label)); + if dir.exists() { + let _ = fs::remove_dir_all(&dir); + } + dir +} + +fn tool_available(tool: &str) -> bool { + Command::new(tool) + .arg("-V") + .output() + .map(|o| o.status.success()) + .unwrap_or(false) +} + +// result must equal dot27(a,b) for known packed vectors (combinational, #1 delay). +const TESTBENCH: &str = r#"`timescale 1ns/1ps +module tb; + reg [63:0] a,b; wire signed [7:0] result; integer fails; + CombTernaryDot dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.a(a),.b(b),.ready(),.result(result)); + task chk(input [63:0] av, input [63:0] bv, input integer exp); begin + a=av; b=bv; #1; + if (result!==exp) begin fails=fails+1; $display("FAIL a=%h b=%h result=%0d exp=%0d",av,bv,result,exp); end + end endtask + initial begin + fails=0; + chk(64'd0, 64'd0, 27); + chk(64'd12009599006321322, 64'd12009599006321322, 27); + chk(64'd0, 64'd12009599006321322, -27); + chk(64'd6004799503160661, 64'd6004799503160661, 0); + if (fails==0) $display("ALL_PASS"); else $display("FAILED %0d",fails); + $finish; + end +endmodule +"#; + +#[test] +fn spec_first_combinational_data_ports() { + let gen = Command::new(t27c()) + .arg("gen-verilog") + .arg(spec_path()) + .output() + .expect("invoke gen-verilog"); + assert!( + gen.status.success(), + "gen-verilog of comb_ternary_dot.t27 failed:\n{}", + String::from_utf8_lossy(&gen.stderr) + ); + let verilog = String::from_utf8_lossy(&gen.stdout).into_owned(); + + assert!( + verilog.contains("input wire [63:0] a") && verilog.contains("input wire [63:0] b"), + "on_comb params did not become input data ports:\n{}", + verilog + ); + assert!( + verilog.contains("output wire signed [7:0] result"), + "on_comb return was not exposed as an output data port:\n{}", + verilog + ); + assert!( + verilog.contains("assign result = on_comb(a, b);"), + "the result port is not continuously driven from on_comb:\n{}", + verilog + ); + + // Synthesizes to real combinational Artix-7 fabric: LUTs, and NO flip-flops. + if tool_available("yosys") { + let dir = scratch_dir("synth"); + fs::create_dir_all(&dir).expect("create synth dir"); + fs::write(dir.join("cd.v"), &gen.stdout).expect("write cd.v"); + let synth = Command::new("yosys") + .arg("-p") + .arg(format!( + "read_verilog -sv {}; synth_xilinx -top CombTernaryDot; stat", + dir.join("cd.v").to_str().unwrap() + )) + .output() + .expect("invoke yosys"); + let s = String::from_utf8_lossy(&synth.stdout).into_owned() + + &String::from_utf8_lossy(&synth.stderr); + let _ = fs::remove_dir_all(&dir); + assert!(synth.status.success(), "yosys synth_xilinx failed:\n{}", s); + assert!( + s.contains("LUT"), + "combinational dot product produced no LUTs (optimized away):\n{}", + s + ); + } + + if !tool_available("iverilog") || !tool_available("vvp") { + eprintln!("SKIP: iverilog/vvp not on PATH; skipping combinational simulation"); + return; + } + + let dir = scratch_dir("chk"); + fs::create_dir_all(&dir).expect("create scratch dir"); + fs::write(dir.join("cd.v"), &gen.stdout).expect("write cd.v"); + fs::write(dir.join("tb.v"), TESTBENCH).expect("write tb.v"); + + let vvp_path = dir.join("sim.vvp"); + let compile = Command::new("iverilog") + .args(["-g2012", "-o", vvp_path.to_str().unwrap()]) + .arg(dir.join("cd.v")) + .arg(dir.join("tb.v")) + .output() + .expect("invoke iverilog"); + assert!( + compile.status.success(), + "iverilog compile failed:\n{}", + String::from_utf8_lossy(&compile.stderr) + ); + + let run = Command::new("vvp").arg(&vvp_path).output().expect("invoke vvp"); + let stdout = String::from_utf8_lossy(&run.stdout).into_owned(); + let _ = fs::remove_dir_all(&dir); + + assert!( + stdout.contains("ALL_PASS"), + "combinational dot product did not match the reference:\n{}", + stdout + ); + assert!(!stdout.contains("FAIL"), "combinational dot mismatch:\n{}", stdout); +} diff --git a/bootstrap/tests/gft_add_rne.rs b/bootstrap/tests/gft_add_rne.rs new file mode 100644 index 0000000000..20cb709121 --- /dev/null +++ b/bootstrap/tests/gft_add_rne.rs @@ -0,0 +1,107 @@ +// ============================================================================ +// Check for the spec-first ROUND-TO-NEAREST-EVEN GF-T16 same-sign ADD +// (specs/ternary/gft_add_rne.t27): matches the ideal oracle exactly (guard/sticky +// from the alignment shift + tie-to-even), so it is MORE ACCURATE than the +// truncating silicon gft_add. Verified against 300 oracle-generated normal-range +// vectors (tests/gft_add_rne_vectors.txt). Skips without iverilog/vvp. +// ============================================================================ + +use std::env; +use std::fs; +use std::path::PathBuf; +use std::process::Command; + +fn t27c() -> &'static str { + env!("CARGO_BIN_EXE_t27c") +} +fn spec_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("..") + .join("specs") + .join("ternary") + .join("gft_add_rne.t27") +} +fn vectors_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("tests") + .join("gft_add_rne_vectors.txt") +} +fn tool_available(t: &str) -> bool { + Command::new(t).arg("-V").output().map(|o| o.status.success()).unwrap_or(false) +} + +#[test] +fn spec_first_gft_add_rne_matches_oracle() { + let gen = Command::new(t27c()) + .arg("gen-verilog") + .arg(spec_path()) + .output() + .expect("invoke gen-verilog"); + assert!( + gen.status.success(), + "gen-verilog of gft_add_rne.t27 failed:\n{}", + String::from_utf8_lossy(&gen.stderr) + ); + let verilog = String::from_utf8_lossy(&gen.stdout).into_owned(); + assert!( + verilog.contains("output wire [15:0] result"), + "GF-T RNE add missing result port:\n{}", + verilog + ); + + if !tool_available("iverilog") || !tool_available("vvp") { + eprintln!("SKIP: iverilog/vvp not on PATH; skipping GF-T RNE add check"); + return; + } + + let vectors = fs::read_to_string(vectors_path()).expect("read vectors"); + let n = vectors.lines().filter(|l| !l.trim().is_empty()).count(); + let dir = env::temp_dir().join(format!("t27_arne_{}", std::process::id())); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).unwrap(); + fs::write(dir.join("spec.v"), &gen.stdout).unwrap(); + fs::write(dir.join("vec.txt"), &vectors).unwrap(); + + let tb = format!( + r#"`timescale 1ns/1ps +module tb; + reg [15:0] a,b; wire [15:0] y; integer fails,nn,fd,code; reg [15:0] exp; + GftAddRne dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.a(a),.b(b),.ready(),.result(y)); + initial begin + fails=0; nn=0; fd=$fopen("{}","r"); + while(!$feof(fd)) begin code=$fscanf(fd,"%h %h %h\n",a,b,exp); + if(code==3) begin #1; nn=nn+1; + if(y!==exp) begin fails=fails+1; if(fails<=6)$display("FAIL a=%h b=%h y=%h exp=%h",a,b,y,exp); end + end end + $fclose(fd); + if(fails==0)$display("ALL_PASS %0d",nn); else $display("FAILED %0d/%0d",fails,nn); + $finish; + end +endmodule +"#, + dir.join("vec.txt").to_str().unwrap() + ); + fs::write(dir.join("tb.v"), tb).unwrap(); + + let vvp = dir.join("sim.vvp"); + let compile = Command::new("iverilog") + .args(["-g2012", "-o", vvp.to_str().unwrap()]) + .arg(dir.join("spec.v")) + .arg(dir.join("tb.v")) + .output() + .unwrap(); + assert!( + compile.status.success(), + "iverilog compile failed:\n{}", + String::from_utf8_lossy(&compile.stderr) + ); + let run = Command::new("vvp").arg(&vvp).output().unwrap(); + let stdout = String::from_utf8_lossy(&run.stdout).into_owned(); + let _ = fs::remove_dir_all(&dir); + assert!( + stdout.contains(&format!("ALL_PASS {}", n)), + "RNE GF-T add differs from the oracle:\n{}", + stdout + ); + assert!(!stdout.contains("FAIL"), "RNE GF-T add mismatch:\n{}", stdout); +} diff --git a/bootstrap/tests/gft_add_rne_vectors.txt b/bootstrap/tests/gft_add_rne_vectors.txt new file mode 100644 index 0000000000..4af313ee04 --- /dev/null +++ b/bootstrap/tests/gft_add_rne_vectors.txt @@ -0,0 +1,300 @@ +4f7e 5911 592d +3a06 3d5a 3e2e +5252 4f56 5328 +5429 6d84 6d84 +3dce 5fb0 5fb0 +3cf3 3c34 3e94 +3840 3b88 3c54 +6468 612a 6532 +3ee5 5daf 5daf +6b11 36d6 6b11 +4b5d 422c 4b80 +3e05 5fa5 5fa5 +3583 6bf7 6bf7 +3af2 33b2 3b2d +6072 6c03 6c0d +38ca 62cf 62cf +4655 3288 4656 +5411 6c56 6c56 +56ca 51ae 5740 +36c4 4a5f 4a60 +5e94 56b0 5ebf +582a 6037 605a +4298 5512 5513 +6023 567c 6037 +699c 5ef2 69b4 +3c2c 5976 5976 +6858 5d63 6866 +3976 69ce 69ce +3ecb 4a12 4a1d +4b50 6400 6400 +4cda 38e3 4cdb +4f4c 425a 4f55 +4523 5a69 5a69 +5238 641a 641b +4bb6 63fd 63fd +48fe 5e43 5e43 +4cec 5a62 5a68 +637d 4b7a 637d +3b29 5caf 5caf +5f09 661e 664f +34b0 650d 650d +3c97 380c 3d1a +35cd 34d5 3751 +652d 4a0f 652d +6523 4890 6523 +511c 548c 5553 +372f 6078 6078 +37ce 4c91 4c91 +5f88 54ad 5f9d +5d18 5ffa 60c3 +4831 391b 4834 +52b1 3a56 52b1 +3ce3 620d 620d +3fe5 3dd3 40e7 +578d 5455 585c +3ded 550c 550c +541d 37be 541d +5443 4533 5446 +36e5 608c 608c +39f7 39d0 3be4 +3436 501d 501d +49d5 40ec 4a02 +49fb 66f8 66f8 +3456 5830 5830 +5da0 4c46 5da2 +3622 3eb9 3edb +361e 376b 38c4 +59e6 501a 5a04 +5e4d 6355 63e8 +3749 6408 6408 +4e98 4f8b 5112 +508d 666c 666c +6aec 49ce 6aec +62c4 3ae2 62c4 +3835 387a 3a58 +3654 5b7d 5b7d +3818 61de 61de +5acd 537a 5b05 +6853 5af1 6859 +32ca 420f 4212 +4e16 4269 4e20 +53ab 643b 643d +6be6 4342 6be6 +58e1 683c 683f +5c87 4333 5c87 +34bf 6569 6569 +659c 6a07 6a7a +6b35 6c60 6dfa +33c1 46fd 46fe +4d49 59f7 5a02 +5798 49b8 579f +3f1b 3734 3f4e +4fd2 4fc2 51ca +4b51 3d9b 4b58 +345e 46ae 46af +461b 54c1 54c5 +3f75 5e8c 5e8c +5b59 37c9 5b59 +598a 58d8 5b31 +5f57 544d 5f69 +33af 5de1 5de1 +414b 6865 6865 +4e03 5f23 5f25 +6cd2 5449 6cd2 +4142 322b 4146 +3750 3aa7 3b7b +5f9d 3994 5f9d +4a8a 6b6d 6b6d +48ce 4348 4937 +6cba 4ab6 6cba +5609 3d39 5609 +5c14 6b1d 6b21 +51b5 525f 541d +4293 45ce 468c +50ed 5cb7 5cc3 +4763 3a34 476c +5560 421a 5561 +5662 3dd0 5662 +3ad7 4689 4694 +6add 4ccf 6add +67b1 5c0a 67c1 +6832 556b 6833 +503e 497d 5076 +6598 65da 67b9 +4cc3 5a65 5a6b +6c56 3d6b 6c56 +42fd 6be0 6be0 +520c 3d57 520c +5cb1 401c 5cb1 +34cd 5f5a 5f5a +4484 5f52 5f52 +4424 4a4e 4a92 +4afb 67d0 67d0 +4e2a 5f41 5f43 +3c93 66cc 66cc +5b86 5c9b 5e2f +6621 4b96 6621 +3baa 45ed 4605 +6060 3dfe 6060 +5303 437e 5306 +5963 620e 6229 +3e3c 61da 61da +4469 6cd3 6cd3 +68ca 33db 68ca +6104 393d 6104 +440b 40b6 44b8 +5da8 5b16 5e9a +4964 5b4a 5b4c +54a4 6c1d 6c1d +3ad6 605b 605b +3413 3f08 3f19 +67c1 6b6e 6c2f +484d 5460 5469 +5fb4 4cb4 5fb5 +349f 41af 41b9 +48c4 5f65 5f65 +61a2 5222 61a6 +3d40 551b 551b +4f26 45be 4f44 +65b1 546a 65b3 +356f 6ae4 6ae4 +4d75 43ce 4d93 +49a1 36bb 49a2 +3679 5b4a 5b4a +4c13 513c 51c1 +4d8f 3709 4d8f +3fe2 56ac 56ac +58f7 332b 58f7 +5e79 3205 5e79 +3e68 4f85 4f87 +52be 424b 52c0 +533b 5293 54e7 +69af 60ba 69db +3fe4 4523 45a0 +5be6 6141 61be +5dda 523b 5dec +57e8 545a 588a +3759 4c4b 4c4b +64a6 5099 64a7 +5ba6 51fc 5bc6 +380c 5723 5723 +4e51 5f0f 5f11 +62ad 551a 62b3 +3351 69c4 69c4 +6b7d 534b 6b7d +62a5 3d44 62a5 +5f46 5f52 614c +514d 3722 514d +6d05 3933 6d05 +6592 35e5 6592 +37a6 44ee 44f5 +4f81 45ce 4f9f +52d6 34a8 52d6 +6679 5c46 668b +3726 3609 3898 +5129 6a36 6a36 +4eae 60a2 60a3 +6710 3662 6710 +38a2 6300 6300 +5b0a 48e4 5b0b +3ec8 5ff8 5ff8 +56c6 55a1 584b +5f13 5ddd 6081 +405a 4b05 4b18 +42bc 3a15 42dd +5986 5889 5b08 +4e7d 506c 51aa +658d 5993 659b +5554 6a89 6a89 +40f1 476e 47cc +5456 6c6e 6c6e +3773 33db 3835 +48e1 5bca 5bcb +5406 6bcf 6bcf +435c 5ca1 5ca1 +492c 36d3 492d +42a4 599e 599e +667d 661b 684c +409b 5611 5611 +5cb9 5e49 5fa6 +5b9c 6c83 6c85 +4d1f 5fea 5fec +3698 4d1f 4d1f +389a 5a91 5a91 +510a 5207 538c +4864 6d20 6d20 +5a01 38eb 5a01 +64a9 5169 64aa +66cb 42a8 66cb +5c12 46f0 5c12 +68c4 3608 68c4 +6206 4bec 6206 +3235 68c2 68c2 +4537 6449 6449 +4cd7 54d1 54fe +3653 38dc 3a03 +47d6 34bd 47d7 +5f18 576f 5f4f +3911 6507 6507 +3a29 3575 3a98 +5e93 3750 5e93 +5f0d 32f3 5f0d +3c36 33b5 3c54 +3365 5e4a 5e4a +3a91 3fd5 403d +5545 4fca 55be +56e5 50c9 573e +51c5 423e 51c9 +50d4 5691 56ec +4fe2 3c73 4fe3 +4cbf 4957 4d95 +4e61 5822 5835 +3b78 3647 3c05 +4308 527a 527d +53c3 43a6 53c7 +3f96 64df 64df +4594 5b42 5b42 +48cb 3a47 48d0 +6a31 3554 6a31 +6044 6bd0 6be2 +6772 4c13 6772 +60ba 47c5 60ba +4231 350e 4237 +4e1b 4112 4e21 +6d96 6c34 6ee5 +3e6b 4d4c 4d51 +359f 5a71 5a71 +4c51 592c 5935 +4813 41e5 4851 +69a6 3cb8 69a6 +3575 63b6 63b6 +4b2c 481b 4c1d +5baa 5f5d 6024 +5a10 5141 5a2a +3e7c 4186 4262 +498e 5e40 5e40 +49ee 4cc6 4dc2 +6b8a 48fb 6b8a +5777 6675 6678 +45b2 373c 45b8 +44c0 4f8d 4fa3 +3f4b 53b8 53b9 +575d 48ba 5762 +624d 343b 624d +675a 4ecc 675a +6ae2 388d 6ae2 +6cf1 4960 6cf1 +6cab 352e 6cab +3883 520c 520c +32d6 68ed 68ed +6392 5ae2 63c0 +3466 4589 458b +3515 60f6 60f6 +69ca 52e7 69ca +3d7a 491f 492d +6230 6801 6847 +4652 4402 4753 +38ac 393e 3af5 +401f 5ddc 5ddc +6172 5bd3 61ec diff --git a/bootstrap/tests/gft_dot2.rs b/bootstrap/tests/gft_dot2.rs new file mode 100644 index 0000000000..9512246c9e --- /dev/null +++ b/bootstrap/tests/gft_dot2.rs @@ -0,0 +1,224 @@ +// ============================================================================ +// Check for the spec-first GF-T16 MAC (specs/ternary/gft_dot2.t27, #1764 + GF-T): +// y = a1*b1 + a2*b2 in the ternary-native GoldenFloat format that was verified +// bit-exact ON SILICON (AX7203, gft_dot2 3/3). The hand-written RTL noted that +// t27c gen-verilog could not emit this (interleaved reg decls -- fixed by #1741); +// this test proves the spec-first realization is bit-exact to that silicon-proven +// RTL over random inputs. The reference modules (gft_dot2/gft_mul/gft_add) are +// embedded verbatim so the check is self-contained. Skips without iverilog/vvp. +// ============================================================================ + +use std::env; +use std::fs; +use std::path::PathBuf; +use std::process::Command; + +fn t27c() -> &'static str { env!("CARGO_BIN_EXE_t27c") } +fn spec_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("..").join("specs").join("ternary").join("gft_dot2.t27") +} +fn scratch_dir(label: &str) -> PathBuf { + let dir = env::temp_dir().join(format!("t27_gft_{}_{}", std::process::id(), label)); + if dir.exists() { let _ = fs::remove_dir_all(&dir); } + dir +} +fn tool_available(tool: &str) -> bool { + Command::new(tool).arg("-V").output().map(|o| o.status.success()).unwrap_or(false) +} + +// Silicon-proven reference RTL (trinity-fpga/build/gft_dot2), embedded verbatim. +const REFERENCE_RTL: &str = r#####" +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_dot2 -- 2-term GF-T16 dot product: y = a1*b1 + a2*b2, the multiply-accumulate +// kernel at the heart of every matmul / attention / inference layer. Pure composition +// of the silicon-proven gft_mul with gft_add (both realizations of tri_gft_arith / +// tri_gft_add) -- no new arithmetic, just the MAC wiring. Combinational. +// +// This is the hardware twin of the NUMERICAL dot-product advantage measured in +// tests/gft_task_accuracy.rs: there GF-T16 owns the wide-dynamic-range dot product on +// paper; here the same dot product is computed in GF-T16 hardware, bit-exact to spec. +// +// Operands/result are packed GF-T16 magnitudes: [ offset:15..9 (7b) | mant:8..0 (9b) ], +// value = (1 + mant/512) * 2^(offset-40). +// ============================================================================ +module gft_dot2 ( + input wire [15:0] a1, + input wire [15:0] b1, + input wire [15:0] a2, + input wire [15:0] b2, + output wire [15:0] y +); + // term 1 = a1 * b1 + wire [31:0] p1_off, p1_mant; + gft_mul #(.BIAS(40), .OFFSET_MAX(80), .MANT_ONE(512)) u_m1 ( + .a_off({25'd0, a1[15:9]}), .a_mant({23'd0, a1[8:0]}), + .b_off({25'd0, b1[15:9]}), .b_mant({23'd0, b1[8:0]}), + .out_off(p1_off), .out_mant(p1_mant)); + + // term 2 = a2 * b2 + wire [31:0] p2_off, p2_mant; + gft_mul #(.BIAS(40), .OFFSET_MAX(80), .MANT_ONE(512)) u_m2 ( + .a_off({25'd0, a2[15:9]}), .a_mant({23'd0, a2[8:0]}), + .b_off({25'd0, b2[15:9]}), .b_mant({23'd0, b2[8:0]}), + .out_off(p2_off), .out_mant(p2_mant)); + + // accumulate: term1 + term2 (same-sign GF-T add) + wire [31:0] y_off, y_mant; + gft_add #(.OFFSET_MAX(80), .MANT_ONE(512), .SIG_BITS(10)) u_acc ( + .a_off(p1_off), .a_mant(p1_mant), + .b_off(p2_off), .b_mant(p2_mant), + .out_off(y_off), .out_mant(y_mant)); + + assign y = {y_off[6:0], y_mant[8:0]}; +endmodule +`default_nettype wire + +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_mul -- GF-T ladder multiplier (balanced-ternary exponent). +// +// Verified realization of specs/tri_gft_arith.t27's gft_mul_offset_full_p + +// gft_mul_mant_p + gft_mul_mant_carry_p -- the SAME spec the over-wire verifier +// runs (trinet_compute_over_mesh / trinet_rung_verify). SSOT is the .t27; this +// .v is the synthesizable realization (as fpga/gf16/gf16_mul.v is for GF16). +// +// t27c gen-verilog cannot emit this directly yet: it interleaves `reg` +// declarations with statements inside begin/end blocks (illegal Verilog; iverilog +// rejects it). Tracked upstream; this hand-transcription keeps the exact logic +// with legal declaration ordering, gated by an iverilog KAT sweep below. +// +// Combinational. Parametric per rung; GF-T16 defaults (bias 40, offset_max 80, +// mant_one 512). GF-T8 = (13, 26, 16); GF-T4 = (4, 8, 2); GF-T32 uses wider mant. +// ============================================================================ +module gft_mul #( + parameter [31:0] BIAS = 40, + parameter [31:0] OFFSET_MAX = 80, + parameter [31:0] MANT_ONE = 512 +) ( + input wire [31:0] a_off, + input wire [31:0] a_mant, + input wire [31:0] b_off, + input wire [31:0] b_mant, + output wire [31:0] out_off, + output wire [31:0] out_mant +); + // Full-precision significand product (1+M/mant_one) scaled by mant_one^2. + wire [31:0] prod = (MANT_ONE + a_mant) * (MANT_ONE + b_mant); + wire [31:0] thresh = (2 * MANT_ONE) * MANT_ONE; // one-bit renorm boundary + wire carry = (prod >= thresh); // mantissa overflow -> exp += 1 + + // Exponent offset: add offsets, apply the carry, de-bias, saturate at the rung's max. + wire [31:0] sum = a_off + b_off + {31'd0, carry}; + wire [31:0] result = sum - BIAS; + assign out_off = (sum < BIAS) ? 32'd0 : + (result >= OFFSET_MAX) ? OFFSET_MAX : result; + + // Mantissa: renormalize by the carry (divisors are constant powers of two -> shifts). + assign out_mant = carry ? ((prod / (2 * MANT_ONE)) - MANT_ONE) + : ((prod / MANT_ONE ) - MANT_ONE); +endmodule +`default_nettype wire + +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_add -- GF-T ladder adder (SAME-sign add), balanced-ternary exponent. +// +// Verified realization of specs/tri_gft_add.t27's gft_add_offset_c_p + +// gft_add_mant_c_p (via gft_add_sb_p / _offset_p / _mant_p) -- the SAME spec the +// over-wire verifier runs (trinet_rung_verify, trinet_compute_over_mesh). Align +// the smaller operand by the exponent-offset difference (barrel shift), add the +// significands, and renormalize by one carry. Combinational; parametric per rung. +// GF-T16 defaults: offset_max 80, mant_one 512, sig_bits 10 (mant_bits+1). +// ============================================================================ +module gft_add #( + parameter [31:0] OFFSET_MAX = 80, + parameter [31:0] MANT_ONE = 512, + parameter [31:0] SIG_BITS = 10 +) ( + input wire [31:0] a_off, + input wire [31:0] a_mant, + input wire [31:0] b_off, + input wire [31:0] b_mant, + output wire [31:0] out_off, + output wire [31:0] out_mant +); + // Order operands so `hi` has the larger (or equal) exponent offset. + wire a_hi = (a_off >= b_off); + wire [31:0] hi_off = a_hi ? a_off : b_off; + wire [31:0] hi_m = a_hi ? a_mant : b_mant; + wire [31:0] lo_off = a_hi ? b_off : a_off; + wire [31:0] lo_m = a_hi ? b_mant : a_mant; + + // Align the smaller significand right by the offset difference (0 if it underflows). + wire [31:0] d = hi_off - lo_off; + wire [31:0] sb = (d >= SIG_BITS) ? 32'd0 : ((MANT_ONE + lo_m) >> d[4:0]); + wire [31:0] sum = (MANT_ONE + hi_m) + sb; + + // Renormalize: a significand >= 2*mant_one carries into the exponent (+1, saturate). + wire carry = (sum >= (2 * MANT_ONE)); + wire [31:0] e = hi_off + 32'd1; + assign out_off = carry ? ((e >= OFFSET_MAX) ? OFFSET_MAX : e) : hi_off; + assign out_mant = carry ? ((sum >> 1) - MANT_ONE) : (sum - MANT_ONE); +endmodule +`default_nettype wire + +"#####; + +// Drive both DUTs with random valid GF-T16 magnitudes (offset in [1,79], mant in +// [0,511]) and require the spec-first result to equal the silicon-proven RTL. +const TESTBENCH: &str = r#"`timescale 1ns/1ps +module tb; + reg [15:0] a1,b1,a2,b2; wire [15:0] y_spec, y_ref; integer i, fails, o, m; + GftDot2 dut_spec(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.a1(a1),.b1(b1),.a2(a2),.b2(b2),.ready(),.result(y_spec)); + gft_dot2 dut_ref(.a1(a1),.b1(b1),.a2(a2),.b2(b2),.y(y_ref)); + function [15:0] rnd; input integer dummy; begin + o = 1 + ($random % 79); if (o<1) o=1; if (o>79) o=79; + m = $random % 512; if (m<0) m=-m; + rnd = (o<<9) | m; + end endfunction + initial begin + fails=0; + for (i=0;i<2000;i=i+1) begin + a1=rnd(i); b1=rnd(i+1); a2=rnd(i+2); b2=rnd(i+3); #1; + if (y_spec!==y_ref) begin fails=fails+1; + if (fails<=5) $display("FAIL a1=%h b1=%h a2=%h b2=%h spec=%h ref=%h",a1,b1,a2,b2,y_spec,y_ref); end + end + if (fails==0) $display("ALL_PASS 2000"); else $display("FAILED %0d",fails); + $finish; + end +endmodule +"#; + +#[test] +fn spec_first_gft_mac_matches_silicon_proven_rtl() { + let gen = Command::new(t27c()).arg("gen-verilog").arg(spec_path()).output().expect("gen-verilog"); + assert!(gen.status.success(), "gen-verilog failed:\n{}", String::from_utf8_lossy(&gen.stderr)); + let verilog = String::from_utf8_lossy(&gen.stdout).into_owned(); + assert!(verilog.contains("input wire [15:0] a1") && verilog.contains("output wire [15:0] result"), + "GF-T MAC did not expose the a1/b1/a2/b2 -> result data interface:\n{}", verilog); + assert!(verilog.contains("assign result = on_comb(a1, b1, a2, b2);"), + "result port is not driven from the MAC:\n{}", verilog); + + if !tool_available("iverilog") || !tool_available("vvp") { + eprintln!("SKIP: iverilog/vvp not on PATH; skipping GF-T cross-check"); + return; + } + let dir = scratch_dir("chk"); + fs::create_dir_all(&dir).expect("scratch"); + fs::write(dir.join("spec.v"), &gen.stdout).expect("spec.v"); + fs::write(dir.join("ref.v"), REFERENCE_RTL).expect("ref.v"); + fs::write(dir.join("tb.v"), TESTBENCH).expect("tb.v"); + let vvp = dir.join("sim.vvp"); + let comp = Command::new("iverilog").args(["-g2012","-o",vvp.to_str().unwrap()]) + .arg(dir.join("spec.v")).arg(dir.join("ref.v")).arg(dir.join("tb.v")).output().expect("iverilog"); + assert!(comp.status.success(), "iverilog compile failed:\n{}", String::from_utf8_lossy(&comp.stderr)); + let run = Command::new("vvp").arg(&vvp).output().expect("vvp"); + let out = String::from_utf8_lossy(&run.stdout).into_owned(); + let _ = fs::remove_dir_all(&dir); + assert!(out.contains("ALL_PASS 2000"), "spec-first GF-T MAC differs from the silicon-proven RTL:\n{}", out); + assert!(!out.contains("FAIL"), "GF-T MAC mismatch:\n{}", out); +} diff --git a/bootstrap/tests/gft_dot2_rne.rs b/bootstrap/tests/gft_dot2_rne.rs new file mode 100644 index 0000000000..8cf13c89b3 --- /dev/null +++ b/bootstrap/tests/gft_dot2_rne.rs @@ -0,0 +1,108 @@ +// ============================================================================ +// Check for the spec-first fully ROUND-TO-NEAREST-EVEN GF-T16 MAC +// (specs/ternary/gft_dot2_rne.t27, y = a1*b1 + a2*b2): composes the RNE mul and +// RNE add, bit-exact to the ideal oracle gft16_add(gft16_mul(a1,b1), +// gft16_mul(a2,b2)) -- the accurate counterpart of the truncating-silicon +// gft_dot2. Verified against 300 oracle-generated normal-range vectors +// (tests/gft_dot2_rne_vectors.txt). Skips without iverilog/vvp. +// ============================================================================ + +use std::env; +use std::fs; +use std::path::PathBuf; +use std::process::Command; + +fn t27c() -> &'static str { + env!("CARGO_BIN_EXE_t27c") +} +fn spec_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("..") + .join("specs") + .join("ternary") + .join("gft_dot2_rne.t27") +} +fn vectors_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("tests") + .join("gft_dot2_rne_vectors.txt") +} +fn tool_available(t: &str) -> bool { + Command::new(t).arg("-V").output().map(|o| o.status.success()).unwrap_or(false) +} + +#[test] +fn spec_first_gft_dot2_rne_matches_oracle() { + let gen = Command::new(t27c()) + .arg("gen-verilog") + .arg(spec_path()) + .output() + .expect("invoke gen-verilog"); + assert!( + gen.status.success(), + "gen-verilog of gft_dot2_rne.t27 failed:\n{}", + String::from_utf8_lossy(&gen.stderr) + ); + let verilog = String::from_utf8_lossy(&gen.stdout).into_owned(); + assert!( + verilog.contains("input wire [15:0] a1") && verilog.contains("output wire [15:0] result"), + "GF-T RNE MAC missing a1..b2 -> result interface:\n{}", + verilog + ); + + if !tool_available("iverilog") || !tool_available("vvp") { + eprintln!("SKIP: iverilog/vvp not on PATH; skipping GF-T RNE MAC check"); + return; + } + + let vectors = fs::read_to_string(vectors_path()).expect("read vectors"); + let n = vectors.lines().filter(|l| !l.trim().is_empty()).count(); + let dir = env::temp_dir().join(format!("t27_d2rne_{}", std::process::id())); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).unwrap(); + fs::write(dir.join("spec.v"), &gen.stdout).unwrap(); + fs::write(dir.join("vec.txt"), &vectors).unwrap(); + + let tb = format!( + r#"`timescale 1ns/1ps +module tb; + reg [15:0] a1,b1,a2,b2; wire [15:0] y; integer fails,nn,fd,code; reg [15:0] exp; + GftDot2Rne dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.a1(a1),.b1(b1),.a2(a2),.b2(b2),.ready(),.result(y)); + initial begin + fails=0; nn=0; fd=$fopen("{}","r"); + while(!$feof(fd)) begin code=$fscanf(fd,"%h %h %h %h %h\n",a1,b1,a2,b2,exp); + if(code==5) begin #1; nn=nn+1; + if(y!==exp) begin fails=fails+1; if(fails<=6)$display("FAIL %h %h %h %h y=%h exp=%h",a1,b1,a2,b2,y,exp); end + end end + $fclose(fd); + if(fails==0)$display("ALL_PASS %0d",nn); else $display("FAILED %0d/%0d",fails,nn); + $finish; + end +endmodule +"#, + dir.join("vec.txt").to_str().unwrap() + ); + fs::write(dir.join("tb.v"), tb).unwrap(); + + let vvp = dir.join("sim.vvp"); + let compile = Command::new("iverilog") + .args(["-g2012", "-o", vvp.to_str().unwrap()]) + .arg(dir.join("spec.v")) + .arg(dir.join("tb.v")) + .output() + .unwrap(); + assert!( + compile.status.success(), + "iverilog compile failed:\n{}", + String::from_utf8_lossy(&compile.stderr) + ); + let run = Command::new("vvp").arg(&vvp).output().unwrap(); + let stdout = String::from_utf8_lossy(&run.stdout).into_owned(); + let _ = fs::remove_dir_all(&dir); + assert!( + stdout.contains(&format!("ALL_PASS {}", n)), + "RNE GF-T MAC differs from the oracle:\n{}", + stdout + ); + assert!(!stdout.contains("FAIL"), "RNE GF-T MAC mismatch:\n{}", stdout); +} diff --git a/bootstrap/tests/gft_dot2_rne_vectors.txt b/bootstrap/tests/gft_dot2_rne_vectors.txt new file mode 100644 index 0000000000..d8bc6ddeb9 --- /dev/null +++ b/bootstrap/tests/gft_dot2_rne_vectors.txt @@ -0,0 +1,300 @@ +4929 62be 60ec 6296 73c7 +46bf 4048 5adb 672d 7244 +39b9 400e 4896 3d0c 3600 +55bf 4106 4eef 57b7 56bc +6374 5341 6078 4f0d 670b +65cb 5a8a 55c6 5ab4 706b +4acf 436c 497c 550c 4ea9 +5f1e 5085 5df6 5af1 6909 +5cf1 4577 404b 53da 5290 +5002 67b2 3ae6 41fd 67b6 +65c7 6103 43a7 6701 76d8 +4ecf 657f 588c 64f3 6de8 +67fc 442b 5c27 4f5d 5df8 +432e 44a8 6272 46ab 5943 +3db7 6027 555f 605e 65fd +5803 413e 3fa1 4b13 4949 +5c4f 5777 3a05 4d56 6400 +41fc 5be5 46d4 4a20 4ded +50a0 6695 49b3 62dc 6779 +49b3 5cf1 4efa 5d26 5caf +52d0 6167 5227 4d97 6464 +5458 3c2e 5e04 6139 6f3f +45cc 578f 4c3e 4bbd 4de7 +4097 3a72 4ea0 453b 441f +4b8d 4a22 4e83 3f71 4607 +57c4 5dbc 3b67 5b2e 6584 +4032 4caa 5a80 38fe 440e +6299 3dea 4e48 4f0e 516a +4430 64f3 62f4 59c3 6cc8 +4592 5e37 5a35 3e8c 5405 +5b7b 5b96 4a98 5b31 6721 +4858 4e35 38ab 660f 4ee8 +3f15 3d55 61b2 4329 54eb +3a70 3f3b 518c 578f 5928 +489a 41cc 4a03 581d 5220 +5b09 4953 46fd 4faa 548b +43ef 530b 41d8 5dda 4fe3 +4580 65e7 441d 5c23 5b7c +56b7 4069 3888 4a52 4747 +5638 45b6 3816 6292 4d66 +4a9d 6036 67b6 48e7 610e +5616 5e60 4743 5809 647a +5dcc 4ce1 5e34 59b5 6810 +460d 3f79 41dd 4e88 4080 +6361 66e8 6322 5c5f 7a83 +4888 40b6 5e6a 3a91 491c +5e1a 556c 51ff 5da7 6441 +3dc7 591f 4d84 627f 6032 +454f 504f 57a8 4a1a 51e7 +65ca 51a4 563e 3d00 6773 +4403 414c 4ad4 532d 4e3f +38d0 605b 6673 6083 7713 +3d8b 60d9 4ca2 38a3 4e86 +64bd 3a38 47bf 5cb6 54eb +63a3 6452 569e 3e37 781c +4e35 58b2 3db4 4baf 56f9 +4afa 4920 5dab 4b1e 58dd +66d8 3e56 4230 3f04 5552 +40e0 5f38 3e69 57c4 5062 +5e6a 3bae 41e9 47e9 4a3b +4d74 3e02 65f5 3c67 5260 +49ca 39af 4001 608f 5090 +4764 41b6 5213 4f72 5193 +4d65 66c5 3e97 66a3 645d +5cad 61b5 3bba 3ff7 6e7b +52d5 4181 3997 515c 4493 +5399 4a52 5af8 50ac 5bff +5e32 55c3 3fcf 6692 6416 +5a2c 5ac0 38f6 522d 64fc +5717 522b 4ec3 67d5 66ac +50a3 54d2 5392 3b90 55b8 +50e3 62c3 5db1 4427 63fe +3a11 5592 5087 5458 54f6 +57f5 5dca 3c0d 3bf4 65c0 +60b5 4674 39ae 64d0 577b +55eb 3ba8 3ace 49ff 41a0 +5898 409e 6611 4244 585a +4aac 65e7 45f9 38fe 609b +3dde 3e42 6643 50b7 6712 +4439 661c 50d2 67cd 68b3 +6350 41ca 60b3 40f6 5611 +5c4f 59b7 58ad 51a7 662f +473c 4bce 386d 55d4 43a8 +46bd 4814 67db 451a 5cfd +5e00 6282 5352 47c3 7082 +3999 4866 4024 4dc4 3e0d +3848 3c70 4e56 5eb4 5d28 +67f1 5dde 5c00 5412 75d0 +5f5b 5b61 3da0 5254 6ad6 +5ed6 4c9f 3e9e 3d8d 5bb7 +5d2b 63fb 4bab 45fc 7127 +4469 5d89 4a2f 3d39 5221 +54ca 5608 6230 5248 6496 +5739 447d 5f4a 3934 4caa +5615 60a9 5950 3b2a 66c5 +67b8 39b1 41b0 3b7a 516f +40aa 4f88 4732 67eb 5f21 +4417 3f41 4239 46e1 39a0 +4b6c 5f98 5925 380e 5b13 +66c3 4843 5af7 406a 5f21 +5393 552d 4d05 3db1 58d6 +4ae8 527d 56fb 3e44 4dd4 +4477 4cdf 425d 6162 5400 +50fd 4546 3e50 634f 51e7 +53de 65af 5198 3d77 6990 +5da7 58b6 492f 6580 66a7 +5645 5a94 3d69 600d 60ee +6154 4fab 5da8 678c 753f +426e 60da 6797 606a 782b +5ed3 3f95 53f4 62d2 66ca +5049 49cb 65c1 3977 4fcb +4523 5719 437f 6326 56d3 +6759 48ba 3b42 3c96 6048 +4709 4b76 39e9 3cb5 42a0 +5d85 55b1 4fa9 3e14 633f +48b5 4647 3810 3fa8 3f15 +46b0 45d0 66bf 6553 7c48 +3fba 5851 3fb1 5d98 4ddb +3bc9 4a40 613e 48d1 5a48 +3feb 5e4a 5425 4bc4 5124 +4376 56ca 5f09 55a8 64c6 +6744 4980 414a 6021 60e0 +3df5 45b2 5b2b 4fb5 5af0 +5ed0 5033 57a0 580a 6165 +6553 4938 3db2 3c36 5ead +4af6 62d6 3dc2 3883 5e19 +55f3 4403 386e 4226 49f9 +5880 4b31 3bc9 65c7 54e3 +3f2f 50ee 3a0c 5719 42c0 +61e8 58bc 40bc 3e1f 6aac +635d 5a1b 3b14 431c 6d8a +4d88 4ee8 4521 5ae6 50e8 +4d4c 3d87 4228 40cf 3b18 +63df 5705 3a56 3a49 6aec +6311 5664 5761 49e4 69aa +5c1a 5c82 4d29 4328 68a3 +5103 4fac 559f 42df 50ee +3cac 54f6 59b4 4095 4a84 +3b4d 415b 3fcc 4d74 3d4a +38d5 39ad 5930 509d 5a15 +4825 3ba7 64e7 4ca1 61d1 +3e3a 3fe7 64b3 6280 7760 +52a1 530a 64da 6405 78e1 +3ba4 47de 64f7 551d 6a4f +632d 45f6 3ba6 6117 5930 +5873 636c 6349 61cd 7540 +54f1 4c82 4ce9 610d 5e3f +4541 50b4 4d5d 5426 51af +5591 4f90 5c7a 5ff5 6c73 +3a7a 3fff 3eef 3a5c 2c1a +61d3 3dd5 531b 3e1e 4fb1 +5add 4dff 6029 5b3b 6b7e +6556 3f15 4281 5b9a 54da +4483 42b6 49ff 4541 3f76 +49c9 5e70 4e64 4e3c 5859 +4752 461d 6275 4cd7 5f7d +380c 4a33 3eff 422d 33e1 +5493 4c43 5a5c 678d 7218 +4cdd 5b5c 52a5 5a31 5d80 +4b68 64e1 5601 5c31 636c +41ca 3e5f 3d03 457b 33be +63ef 5735 415c 6081 6b27 +6362 5a63 546f 5474 6e05 +4e35 55f0 4810 4702 542c +3bed 67ed 5530 471f 5415 +582c 4bd5 4144 5f66 54c6 +5ce8 3970 58ca 40d6 4a9a +6475 3f1e 5ed5 6655 754d +5bf4 4932 41a8 5182 552a +4a8e 3f53 3d0b 38a1 3a20 +5beb 5e7e 56d3 58dd 6a81 +5096 4efe 66af 3fe9 56de +3989 4ff8 48fd 5af0 5432 +3b0b 58b0 3ae0 418d 440b +5d50 57d0 58e8 5502 656e +5a90 4131 4a50 3cb2 4c0b +5892 5f11 4b0e 613d 6802 +59e6 5980 4030 5f73 636a +3ddc 5b60 5283 4b42 4e74 +5142 5985 6661 5526 6bc2 +61c1 63c1 4606 5e0e 7586 +4243 48a6 669c 40ae 577f +6254 3ad5 3b95 5dce 4e13 +6356 4f87 38c5 5192 62f1 +5eac 618a 4e74 64a3 7063 +3d78 63c5 5395 588d 5c56 +46d0 5350 3c73 4a27 4a55 +4620 3cd8 5f04 38bc 4810 +5d81 5aa4 598a 5779 6881 +4dcb 3bc2 3e7d 3c2c 3995 +4b87 3e35 6756 51b5 6917 +5c6e 4bd3 4dcc 537e 5888 +5837 4af5 5d4b 4cb7 5a70 +57a9 3956 5edf 469f 55c4 +4fe9 39de 4111 654a 5685 +508c 58d9 4860 63c3 5d24 +583e 508d 49f1 5dee 5a66 +5717 3d22 3a48 50e5 4486 +63c6 597d 5465 44e7 6d4a +5c63 5501 64f2 4e9c 64d2 +5800 6377 4a7b 4fb3 6b77 +65b9 50d7 44be 3ee2 66a5 +5a52 676d 660e 5ad8 7372 +4972 38a2 54a2 41ef 4698 +4aa3 4089 471a 50e2 4843 +3967 5376 4814 53f1 4c0f +44d5 4e5d 5c95 43d2 507e +4f77 4098 66f7 494f 6074 +491f 64f9 6037 3881 5e52 +4c40 58ae 5a9c 6018 6abb +4a6d 3ed4 4004 3eac 3984 +5b27 4b9b 671c 3bed 579a +4e1e 6391 5773 5d0b 6592 +52bf 383d 5b70 5357 5edf +4d2a 5088 5252 3932 4e02 +3bcb 64b0 3f5d 3944 508c +4b46 51ea 61e9 62c6 74b6 +460f 3bc2 5c33 39ab 4604 +57c2 3ef8 6082 6448 74dc +429b 4cb6 676f 4ce7 647e +51a4 4066 552a 67a4 6ce1 +43c6 4024 6369 59c4 6d36 +5b57 4250 4ef3 4b21 4e82 +4b32 3f90 5af2 45a9 50b2 +5dcc 3d15 5da3 5082 5e49 +5976 56d0 3ed6 5df6 6070 +609c 3cc4 5693 3f15 4ddc +4cd2 578b 5b27 38d9 5482 +533c 3f05 3999 4530 4272 +4135 3bab 6360 5436 67bb +51b6 4a72 4f2d 3ea1 4c49 +4409 41b1 463c 62d2 5927 +4628 40e1 469c 639a 5a59 +4bcc 5b69 5ab7 3a31 573e +54e1 4b50 52a8 5bab 5e75 +5509 3cc3 6067 43e6 5458 +4e45 3cb5 4e7b 536b 521f +3efe 4a43 5ef4 4eaf 5df6 +5685 3d6f 3f7c 38d8 442a +6366 3da8 3ed7 55c7 5126 +4f07 4d0a 43e5 53a7 4cbf +4f4c 44ad 64a3 41dd 568d +3da7 4d73 4c26 4784 43f9 +45f6 5db4 3956 55a6 53ac +4062 5b17 5953 4e8c 5825 +4d20 4233 58c9 6188 6a75 +427e 4dc3 4323 6138 5487 +669e 503f 40a3 6405 66f1 +5398 3d4a 492f 62b4 5c27 +4c9b 65b7 3c5f 4a5a 626b +4d5e 6359 4392 5f42 60d7 +589f 45bf 447b 3f40 4e74 +5d1a 4725 4be8 5708 55eb +38f8 611f 5e9a 56df 65bc +468a 5417 3be9 5821 4aea +6163 67ba 6395 60b4 79c3 +5baf 55f4 5534 6190 674e +5a09 3dcb 5cd7 549f 61b9 +5de1 5cb2 413f 4666 6a9d +5801 4647 45fb 61a0 57c0 +506d 409e 5364 6791 6b06 +5fd8 5158 3feb 44cf 6137 +6207 6114 3bd5 5b62 731f +3a0e 579a 61ff 5535 6734 +41ff 67ee 42bc 3bb4 59ed +5d2d 4b57 409b 5a25 58ad +4d48 5ff8 412e 4eb3 5d41 +5e13 4314 620f 3b4e 5205 +56a3 47c0 395f 46e8 4e79 +5a7c 5bbb 61c4 4611 6655 +5f8f 5e55 3c60 44da 6e13 +60b2 5de4 5f45 4966 6e9f +5992 6270 5550 597f 6c33 +60da 3c8a 40ad 412a 4d9f +4d16 598a 5a83 45bb 5706 +49fd 40d7 3e32 3d0a 3ad8 +4f64 50d8 5423 41e4 507a +52f1 402f 6678 5c1b 7299 +652f 5735 54c5 465e 6c8d +5323 631d 4de0 5af2 6677 +4ec9 574c 3a35 4620 564c +6438 5187 548f 4fa1 65ec +660c 5b13 6641 5433 7174 +5a50 571f 53b6 46a9 619c +4af4 43d1 58bf 4cd6 55e5 +515d 4639 6063 3da5 4e69 +3b97 4489 59dc 3f34 4917 +5688 4421 58f2 65d1 6ecf +4ed7 6400 6768 5556 6cee +5da7 65cd 43be 4f92 7378 +47c0 59cc 5f41 4637 563f +41a6 4fd2 5663 4949 4ff3 +50d5 6072 3b55 5b7d 6176 +6210 4de5 4508 543a 6002 +4b43 64ab 4deb 3eb9 602d +5b18 59ab 5019 3ee3 64d6 +4bdc 5b72 5c2f 3a1d 5755 +3816 3867 50e5 3ead 3fdf +5cd7 53af 578c 4ae1 60a2 +3fc8 5d70 3b83 3e14 4d40 diff --git a/bootstrap/tests/gft_dot4.rs b/bootstrap/tests/gft_dot4.rs new file mode 100644 index 0000000000..d3b81416f2 --- /dev/null +++ b/bootstrap/tests/gft_dot4.rs @@ -0,0 +1,195 @@ +// ============================================================================ +// Check for the spec-first GF-T16 4-term MAC (specs/ternary/gft_dot4.t27): +// y = a1*b1 + a2*b2 + a3*b3 + a4*b4 -- the matmul/attention tile, scaling the +// silicon-proven 2-term gft_dot2 (AX7203 3/3) to a length-4 dot product. Because +// GF-T (float) add is not associative, the balanced reduction tree +// ((a1b1+a2b2)+(a3b3+a4b4)) is the contract; this test proves the spec-first +// result is bit-exact to the SAME tree built from the silicon-proven gft_dot2 + +// gft_add (embedded verbatim) over random inputs. Skips without iverilog/vvp. +// ============================================================================ +use std::env; +use std::fs; +use std::path::PathBuf; +use std::process::Command; +fn t27c() -> &'static str { env!("CARGO_BIN_EXE_t27c") } +fn spec_path() -> PathBuf { PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("..").join("specs").join("ternary").join("gft_dot4.t27") } +fn scratch_dir(l:&str)->PathBuf{let d=env::temp_dir().join(format!("t27_gft4_{}_{}",std::process::id(),l)); if d.exists(){let _=fs::remove_dir_all(&d);} d} +fn tool_available(t:&str)->bool{Command::new(t).arg("-V").output().map(|o|o.status.success()).unwrap_or(false)} +const REFERENCE_RTL: &str = r#####" +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_dot2 -- 2-term GF-T16 dot product: y = a1*b1 + a2*b2, the multiply-accumulate +// kernel at the heart of every matmul / attention / inference layer. Pure composition +// of the silicon-proven gft_mul with gft_add (both realizations of tri_gft_arith / +// tri_gft_add) -- no new arithmetic, just the MAC wiring. Combinational. +// +// This is the hardware twin of the NUMERICAL dot-product advantage measured in +// tests/gft_task_accuracy.rs: there GF-T16 owns the wide-dynamic-range dot product on +// paper; here the same dot product is computed in GF-T16 hardware, bit-exact to spec. +// +// Operands/result are packed GF-T16 magnitudes: [ offset:15..9 (7b) | mant:8..0 (9b) ], +// value = (1 + mant/512) * 2^(offset-40). +// ============================================================================ +module gft_dot2 ( + input wire [15:0] a1, + input wire [15:0] b1, + input wire [15:0] a2, + input wire [15:0] b2, + output wire [15:0] y +); + // term 1 = a1 * b1 + wire [31:0] p1_off, p1_mant; + gft_mul #(.BIAS(40), .OFFSET_MAX(80), .MANT_ONE(512)) u_m1 ( + .a_off({25'd0, a1[15:9]}), .a_mant({23'd0, a1[8:0]}), + .b_off({25'd0, b1[15:9]}), .b_mant({23'd0, b1[8:0]}), + .out_off(p1_off), .out_mant(p1_mant)); + + // term 2 = a2 * b2 + wire [31:0] p2_off, p2_mant; + gft_mul #(.BIAS(40), .OFFSET_MAX(80), .MANT_ONE(512)) u_m2 ( + .a_off({25'd0, a2[15:9]}), .a_mant({23'd0, a2[8:0]}), + .b_off({25'd0, b2[15:9]}), .b_mant({23'd0, b2[8:0]}), + .out_off(p2_off), .out_mant(p2_mant)); + + // accumulate: term1 + term2 (same-sign GF-T add) + wire [31:0] y_off, y_mant; + gft_add #(.OFFSET_MAX(80), .MANT_ONE(512), .SIG_BITS(10)) u_acc ( + .a_off(p1_off), .a_mant(p1_mant), + .b_off(p2_off), .b_mant(p2_mant), + .out_off(y_off), .out_mant(y_mant)); + + assign y = {y_off[6:0], y_mant[8:0]}; +endmodule +`default_nettype wire + +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_mul -- GF-T ladder multiplier (balanced-ternary exponent). +// +// Verified realization of specs/tri_gft_arith.t27's gft_mul_offset_full_p + +// gft_mul_mant_p + gft_mul_mant_carry_p -- the SAME spec the over-wire verifier +// runs (trinet_compute_over_mesh / trinet_rung_verify). SSOT is the .t27; this +// .v is the synthesizable realization (as fpga/gf16/gf16_mul.v is for GF16). +// +// t27c gen-verilog cannot emit this directly yet: it interleaves `reg` +// declarations with statements inside begin/end blocks (illegal Verilog; iverilog +// rejects it). Tracked upstream; this hand-transcription keeps the exact logic +// with legal declaration ordering, gated by an iverilog KAT sweep below. +// +// Combinational. Parametric per rung; GF-T16 defaults (bias 40, offset_max 80, +// mant_one 512). GF-T8 = (13, 26, 16); GF-T4 = (4, 8, 2); GF-T32 uses wider mant. +// ============================================================================ +module gft_mul #( + parameter [31:0] BIAS = 40, + parameter [31:0] OFFSET_MAX = 80, + parameter [31:0] MANT_ONE = 512 +) ( + input wire [31:0] a_off, + input wire [31:0] a_mant, + input wire [31:0] b_off, + input wire [31:0] b_mant, + output wire [31:0] out_off, + output wire [31:0] out_mant +); + // Full-precision significand product (1+M/mant_one) scaled by mant_one^2. + wire [31:0] prod = (MANT_ONE + a_mant) * (MANT_ONE + b_mant); + wire [31:0] thresh = (2 * MANT_ONE) * MANT_ONE; // one-bit renorm boundary + wire carry = (prod >= thresh); // mantissa overflow -> exp += 1 + + // Exponent offset: add offsets, apply the carry, de-bias, saturate at the rung's max. + wire [31:0] sum = a_off + b_off + {31'd0, carry}; + wire [31:0] result = sum - BIAS; + assign out_off = (sum < BIAS) ? 32'd0 : + (result >= OFFSET_MAX) ? OFFSET_MAX : result; + + // Mantissa: renormalize by the carry (divisors are constant powers of two -> shifts). + assign out_mant = carry ? ((prod / (2 * MANT_ONE)) - MANT_ONE) + : ((prod / MANT_ONE ) - MANT_ONE); +endmodule +`default_nettype wire + +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_add -- GF-T ladder adder (SAME-sign add), balanced-ternary exponent. +// +// Verified realization of specs/tri_gft_add.t27's gft_add_offset_c_p + +// gft_add_mant_c_p (via gft_add_sb_p / _offset_p / _mant_p) -- the SAME spec the +// over-wire verifier runs (trinet_rung_verify, trinet_compute_over_mesh). Align +// the smaller operand by the exponent-offset difference (barrel shift), add the +// significands, and renormalize by one carry. Combinational; parametric per rung. +// GF-T16 defaults: offset_max 80, mant_one 512, sig_bits 10 (mant_bits+1). +// ============================================================================ +module gft_add #( + parameter [31:0] OFFSET_MAX = 80, + parameter [31:0] MANT_ONE = 512, + parameter [31:0] SIG_BITS = 10 +) ( + input wire [31:0] a_off, + input wire [31:0] a_mant, + input wire [31:0] b_off, + input wire [31:0] b_mant, + output wire [31:0] out_off, + output wire [31:0] out_mant +); + // Order operands so `hi` has the larger (or equal) exponent offset. + wire a_hi = (a_off >= b_off); + wire [31:0] hi_off = a_hi ? a_off : b_off; + wire [31:0] hi_m = a_hi ? a_mant : b_mant; + wire [31:0] lo_off = a_hi ? b_off : a_off; + wire [31:0] lo_m = a_hi ? b_mant : a_mant; + + // Align the smaller significand right by the offset difference (0 if it underflows). + wire [31:0] d = hi_off - lo_off; + wire [31:0] sb = (d >= SIG_BITS) ? 32'd0 : ((MANT_ONE + lo_m) >> d[4:0]); + wire [31:0] sum = (MANT_ONE + hi_m) + sb; + + // Renormalize: a significand >= 2*mant_one carries into the exponent (+1, saturate). + wire carry = (sum >= (2 * MANT_ONE)); + wire [31:0] e = hi_off + 32'd1; + assign out_off = carry ? ((e >= OFFSET_MAX) ? OFFSET_MAX : e) : hi_off; + assign out_mant = carry ? ((sum >> 1) - MANT_ONE) : (sum - MANT_ONE); +endmodule +`default_nettype wire + +"#####; +const TESTBENCH: &str = r#"`timescale 1ns/1ps +module tb; + reg [15:0] a1,b1,a2,b2,a3,b3,a4,b4; wire [15:0] y_spec; integer i,fails,o,m; + wire [15:0] p12,p34,y_ref; wire [31:0] yo,ym; + GftDot4 dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.a1(a1),.b1(b1),.a2(a2),.b2(b2),.a3(a3),.b3(b3),.a4(a4),.b4(b4),.ready(),.result(y_spec)); + gft_dot2 r12(.a1(a1),.b1(b1),.a2(a2),.b2(b2),.y(p12)); + gft_dot2 r34(.a1(a3),.b1(b3),.a2(a4),.b2(b4),.y(p34)); + gft_add #(.OFFSET_MAX(80),.MANT_ONE(512),.SIG_BITS(10)) racc(.a_off({25'd0,p12[15:9]}),.a_mant({23'd0,p12[8:0]}),.b_off({25'd0,p34[15:9]}),.b_mant({23'd0,p34[8:0]}),.out_off(yo),.out_mant(ym)); + assign y_ref = {yo[6:0],ym[8:0]}; + function [15:0] rnd; input integer dummy; begin o=1+($random%79); if(o<1)o=1; if(o>79)o=79; m=$random%512; if(m<0)m=-m; rnd=(o<<9)|m; end endfunction + initial begin + fails=0; + for(i=0;i<2000;i=i+1) begin + a1=rnd(0);b1=rnd(0);a2=rnd(0);b2=rnd(0);a3=rnd(0);b3=rnd(0);a4=rnd(0);b4=rnd(0);#1; + if(y_spec!==y_ref) begin fails=fails+1; if(fails<=5)$display("FAIL spec=%h ref=%h",y_spec,y_ref); end + end + if(fails==0)$display("ALL_PASS 2000"); else $display("FAILED %0d",fails); + $finish; + end +endmodule +"#; +#[test] +fn spec_first_gft_dot4_matches_silicon_tree() { + let gen=Command::new(t27c()).arg("gen-verilog").arg(spec_path()).output().expect("gen"); + assert!(gen.status.success(),"gen-verilog failed:\n{}",String::from_utf8_lossy(&gen.stderr)); + let v=String::from_utf8_lossy(&gen.stdout).into_owned(); + assert!(v.contains("input wire [15:0] a4")&&v.contains("output wire [15:0] result"),"missing dot4 interface:\n{}",v); + if !tool_available("iverilog")||!tool_available("vvp"){eprintln!("SKIP: no iverilog/vvp");return;} + let d=scratch_dir("chk"); fs::create_dir_all(&d).unwrap(); + fs::write(d.join("spec.v"),&gen.stdout).unwrap(); fs::write(d.join("ref.v"),REFERENCE_RTL).unwrap(); fs::write(d.join("tb.v"),TESTBENCH).unwrap(); + let vvp=d.join("s.vvp"); + let c=Command::new("iverilog").args(["-g2012","-o",vvp.to_str().unwrap()]).arg(d.join("spec.v")).arg(d.join("ref.v")).arg(d.join("tb.v")).output().unwrap(); + assert!(c.status.success(),"iverilog failed:\n{}",String::from_utf8_lossy(&c.stderr)); + let r=Command::new("vvp").arg(&vvp).output().unwrap(); + let o=String::from_utf8_lossy(&r.stdout).into_owned(); let _=fs::remove_dir_all(&d); + assert!(o.contains("ALL_PASS 2000"),"dot4 differs from silicon tree:\n{}",o); + assert!(!o.contains("FAIL"),"dot4 mismatch:\n{}",o); +} diff --git a/bootstrap/tests/gft_dot8.rs b/bootstrap/tests/gft_dot8.rs new file mode 100644 index 0000000000..e6fcf8f116 --- /dev/null +++ b/bootstrap/tests/gft_dot8.rs @@ -0,0 +1,202 @@ +// ============================================================================ +// Check for the spec-first GF-T16 8-term MAC (specs/ternary/gft_dot8.t27): +// y = sum_{i=1..8} a_i*b_i -- a realistic inference / attention-head tile, +// scaling the silicon-proven 2-term gft_dot2 (AX7203 3/3) to length 8 via a +// balanced reduction tree. GF-T float add is non-associative, so the tree is the +// contract; this test proves the spec-first result is bit-exact to the SAME tree +// built from the silicon-proven gft_dot2 + gft_add (embedded) over random inputs. +// ============================================================================ +use std::env; +use std::fs; +use std::path::PathBuf; +use std::process::Command; +fn t27c()->&'static str{env!("CARGO_BIN_EXE_t27c")} +fn spec_path()->PathBuf{PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("..").join("specs").join("ternary").join("gft_dot8.t27")} +fn scratch_dir(l:&str)->PathBuf{let d=env::temp_dir().join(format!("t27_gft8_{}_{}",std::process::id(),l)); if d.exists(){let _=fs::remove_dir_all(&d);} d} +fn tool_available(t:&str)->bool{Command::new(t).arg("-V").output().map(|o|o.status.success()).unwrap_or(false)} +const REFERENCE_RTL: &str = r#####" +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_dot2 -- 2-term GF-T16 dot product: y = a1*b1 + a2*b2, the multiply-accumulate +// kernel at the heart of every matmul / attention / inference layer. Pure composition +// of the silicon-proven gft_mul with gft_add (both realizations of tri_gft_arith / +// tri_gft_add) -- no new arithmetic, just the MAC wiring. Combinational. +// +// This is the hardware twin of the NUMERICAL dot-product advantage measured in +// tests/gft_task_accuracy.rs: there GF-T16 owns the wide-dynamic-range dot product on +// paper; here the same dot product is computed in GF-T16 hardware, bit-exact to spec. +// +// Operands/result are packed GF-T16 magnitudes: [ offset:15..9 (7b) | mant:8..0 (9b) ], +// value = (1 + mant/512) * 2^(offset-40). +// ============================================================================ +module gft_dot2 ( + input wire [15:0] a1, + input wire [15:0] b1, + input wire [15:0] a2, + input wire [15:0] b2, + output wire [15:0] y +); + // term 1 = a1 * b1 + wire [31:0] p1_off, p1_mant; + gft_mul #(.BIAS(40), .OFFSET_MAX(80), .MANT_ONE(512)) u_m1 ( + .a_off({25'd0, a1[15:9]}), .a_mant({23'd0, a1[8:0]}), + .b_off({25'd0, b1[15:9]}), .b_mant({23'd0, b1[8:0]}), + .out_off(p1_off), .out_mant(p1_mant)); + + // term 2 = a2 * b2 + wire [31:0] p2_off, p2_mant; + gft_mul #(.BIAS(40), .OFFSET_MAX(80), .MANT_ONE(512)) u_m2 ( + .a_off({25'd0, a2[15:9]}), .a_mant({23'd0, a2[8:0]}), + .b_off({25'd0, b2[15:9]}), .b_mant({23'd0, b2[8:0]}), + .out_off(p2_off), .out_mant(p2_mant)); + + // accumulate: term1 + term2 (same-sign GF-T add) + wire [31:0] y_off, y_mant; + gft_add #(.OFFSET_MAX(80), .MANT_ONE(512), .SIG_BITS(10)) u_acc ( + .a_off(p1_off), .a_mant(p1_mant), + .b_off(p2_off), .b_mant(p2_mant), + .out_off(y_off), .out_mant(y_mant)); + + assign y = {y_off[6:0], y_mant[8:0]}; +endmodule +`default_nettype wire + +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_mul -- GF-T ladder multiplier (balanced-ternary exponent). +// +// Verified realization of specs/tri_gft_arith.t27's gft_mul_offset_full_p + +// gft_mul_mant_p + gft_mul_mant_carry_p -- the SAME spec the over-wire verifier +// runs (trinet_compute_over_mesh / trinet_rung_verify). SSOT is the .t27; this +// .v is the synthesizable realization (as fpga/gf16/gf16_mul.v is for GF16). +// +// t27c gen-verilog cannot emit this directly yet: it interleaves `reg` +// declarations with statements inside begin/end blocks (illegal Verilog; iverilog +// rejects it). Tracked upstream; this hand-transcription keeps the exact logic +// with legal declaration ordering, gated by an iverilog KAT sweep below. +// +// Combinational. Parametric per rung; GF-T16 defaults (bias 40, offset_max 80, +// mant_one 512). GF-T8 = (13, 26, 16); GF-T4 = (4, 8, 2); GF-T32 uses wider mant. +// ============================================================================ +module gft_mul #( + parameter [31:0] BIAS = 40, + parameter [31:0] OFFSET_MAX = 80, + parameter [31:0] MANT_ONE = 512 +) ( + input wire [31:0] a_off, + input wire [31:0] a_mant, + input wire [31:0] b_off, + input wire [31:0] b_mant, + output wire [31:0] out_off, + output wire [31:0] out_mant +); + // Full-precision significand product (1+M/mant_one) scaled by mant_one^2. + wire [31:0] prod = (MANT_ONE + a_mant) * (MANT_ONE + b_mant); + wire [31:0] thresh = (2 * MANT_ONE) * MANT_ONE; // one-bit renorm boundary + wire carry = (prod >= thresh); // mantissa overflow -> exp += 1 + + // Exponent offset: add offsets, apply the carry, de-bias, saturate at the rung's max. + wire [31:0] sum = a_off + b_off + {31'd0, carry}; + wire [31:0] result = sum - BIAS; + assign out_off = (sum < BIAS) ? 32'd0 : + (result >= OFFSET_MAX) ? OFFSET_MAX : result; + + // Mantissa: renormalize by the carry (divisors are constant powers of two -> shifts). + assign out_mant = carry ? ((prod / (2 * MANT_ONE)) - MANT_ONE) + : ((prod / MANT_ONE ) - MANT_ONE); +endmodule +`default_nettype wire + +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_add -- GF-T ladder adder (SAME-sign add), balanced-ternary exponent. +// +// Verified realization of specs/tri_gft_add.t27's gft_add_offset_c_p + +// gft_add_mant_c_p (via gft_add_sb_p / _offset_p / _mant_p) -- the SAME spec the +// over-wire verifier runs (trinet_rung_verify, trinet_compute_over_mesh). Align +// the smaller operand by the exponent-offset difference (barrel shift), add the +// significands, and renormalize by one carry. Combinational; parametric per rung. +// GF-T16 defaults: offset_max 80, mant_one 512, sig_bits 10 (mant_bits+1). +// ============================================================================ +module gft_add #( + parameter [31:0] OFFSET_MAX = 80, + parameter [31:0] MANT_ONE = 512, + parameter [31:0] SIG_BITS = 10 +) ( + input wire [31:0] a_off, + input wire [31:0] a_mant, + input wire [31:0] b_off, + input wire [31:0] b_mant, + output wire [31:0] out_off, + output wire [31:0] out_mant +); + // Order operands so `hi` has the larger (or equal) exponent offset. + wire a_hi = (a_off >= b_off); + wire [31:0] hi_off = a_hi ? a_off : b_off; + wire [31:0] hi_m = a_hi ? a_mant : b_mant; + wire [31:0] lo_off = a_hi ? b_off : a_off; + wire [31:0] lo_m = a_hi ? b_mant : a_mant; + + // Align the smaller significand right by the offset difference (0 if it underflows). + wire [31:0] d = hi_off - lo_off; + wire [31:0] sb = (d >= SIG_BITS) ? 32'd0 : ((MANT_ONE + lo_m) >> d[4:0]); + wire [31:0] sum = (MANT_ONE + hi_m) + sb; + + // Renormalize: a significand >= 2*mant_one carries into the exponent (+1, saturate). + wire carry = (sum >= (2 * MANT_ONE)); + wire [31:0] e = hi_off + 32'd1; + assign out_off = carry ? ((e >= OFFSET_MAX) ? OFFSET_MAX : e) : hi_off; + assign out_mant = carry ? ((sum >> 1) - MANT_ONE) : (sum - MANT_ONE); +endmodule +`default_nettype wire + +"#####; +const TESTBENCH: &str = r#"`timescale 1ns/1ps +module tb; + reg [15:0] a[1:8]; reg [15:0] b[1:8]; wire [15:0] y_spec; integer i,fails,o,m,k; + wire [15:0] p12,p34,p56,p78,q1,q2,y_ref; wire [31:0] o1,m1,o2,m2,oy,my; + GftDot8 dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1), + .a1(a[1]),.b1(b[1]),.a2(a[2]),.b2(b[2]),.a3(a[3]),.b3(b[3]),.a4(a[4]),.b4(b[4]), + .a5(a[5]),.b5(b[5]),.a6(a[6]),.b6(b[6]),.a7(a[7]),.b7(b[7]),.a8(a[8]),.b8(b[8]),.ready(),.result(y_spec)); + gft_dot2 r12(.a1(a[1]),.b1(b[1]),.a2(a[2]),.b2(b[2]),.y(p12)); + gft_dot2 r34(.a1(a[3]),.b1(b[3]),.a2(a[4]),.b2(b[4]),.y(p34)); + gft_dot2 r56(.a1(a[5]),.b1(b[5]),.a2(a[6]),.b2(b[6]),.y(p56)); + gft_dot2 r78(.a1(a[7]),.b1(b[7]),.a2(a[8]),.b2(b[8]),.y(p78)); + gft_add #(.OFFSET_MAX(80),.MANT_ONE(512),.SIG_BITS(10)) ga(.a_off({25'd0,p12[15:9]}),.a_mant({23'd0,p12[8:0]}),.b_off({25'd0,p34[15:9]}),.b_mant({23'd0,p34[8:0]}),.out_off(o1),.out_mant(m1)); + assign q1={o1[6:0],m1[8:0]}; + gft_add #(.OFFSET_MAX(80),.MANT_ONE(512),.SIG_BITS(10)) gb(.a_off({25'd0,p56[15:9]}),.a_mant({23'd0,p56[8:0]}),.b_off({25'd0,p78[15:9]}),.b_mant({23'd0,p78[8:0]}),.out_off(o2),.out_mant(m2)); + assign q2={o2[6:0],m2[8:0]}; + gft_add #(.OFFSET_MAX(80),.MANT_ONE(512),.SIG_BITS(10)) gy(.a_off({25'd0,q1[15:9]}),.a_mant({23'd0,q1[8:0]}),.b_off({25'd0,q2[15:9]}),.b_mant({23'd0,q2[8:0]}),.out_off(oy),.out_mant(my)); + assign y_ref={oy[6:0],my[8:0]}; + function [15:0] rnd; input integer dd; begin o=1+($random%79); if(o<1)o=1; if(o>79)o=79; m=$random%512; if(m<0)m=-m; rnd=(o<<9)|m; end endfunction + initial begin + fails=0; + for(i=0;i<2000;i=i+1) begin + for(k=1;k<=8;k=k+1) begin a[k]=rnd(0); b[k]=rnd(0); end #1; + if(y_spec!==y_ref) begin fails=fails+1; if(fails<=5)$display("FAIL spec=%h ref=%h",y_spec,y_ref); end + end + if(fails==0)$display("ALL_PASS 2000"); else $display("FAILED %0d",fails); + $finish; + end +endmodule +"#; +#[test] +fn spec_first_gft_dot8_matches_silicon_tree(){ + let gen=Command::new(t27c()).arg("gen-verilog").arg(spec_path()).output().expect("gen"); + assert!(gen.status.success(),"gen-verilog failed:\n{}",String::from_utf8_lossy(&gen.stderr)); + let v=String::from_utf8_lossy(&gen.stdout).into_owned(); + assert!(v.contains("input wire [15:0] a8")&&v.contains("output wire [15:0] result"),"missing dot8 interface:\n{}",v); + if !tool_available("iverilog")||!tool_available("vvp"){eprintln!("SKIP: no iverilog/vvp");return;} + let d=scratch_dir("chk"); fs::create_dir_all(&d).unwrap(); + fs::write(d.join("spec.v"),&gen.stdout).unwrap(); fs::write(d.join("ref.v"),REFERENCE_RTL).unwrap(); fs::write(d.join("tb.v"),TESTBENCH).unwrap(); + let vvp=d.join("s.vvp"); + let c=Command::new("iverilog").args(["-g2012","-o",vvp.to_str().unwrap()]).arg(d.join("spec.v")).arg(d.join("ref.v")).arg(d.join("tb.v")).output().unwrap(); + assert!(c.status.success(),"iverilog failed:\n{}",String::from_utf8_lossy(&c.stderr)); + let r=Command::new("vvp").arg(&vvp).output().unwrap(); + let o=String::from_utf8_lossy(&r.stdout).into_owned(); let _=fs::remove_dir_all(&d); + assert!(o.contains("ALL_PASS 2000"),"dot8 differs from silicon tree:\n{}",o); + assert!(!o.contains("FAIL"),"dot8 mismatch:\n{}",o); +} diff --git a/bootstrap/tests/gft_layer2.rs b/bootstrap/tests/gft_layer2.rs new file mode 100644 index 0000000000..e58ce5dc5f --- /dev/null +++ b/bootstrap/tests/gft_layer2.rs @@ -0,0 +1,191 @@ +// ============================================================================ +// Check for the spec-first GF-T16 matmul ROW / 2-neuron layer (specs/ternary/ +// gft_layer2.t27): a shared activation (a1,a2) feeds two GF-T neurons with their +// own weight vectors; the two GF-T16 outputs are packed into one 32-bit result +// (neuron 0 in [15:0], neuron 1 in [31:16]). Proves the spec-first layer is +// bit-exact to two silicon-proven gft_dot2 instances packed, over random inputs. +// ============================================================================ +use std::env; +use std::fs; +use std::path::PathBuf; +use std::process::Command; +fn t27c()->&'static str{env!("CARGO_BIN_EXE_t27c")} +fn spec_path()->PathBuf{PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("..").join("specs").join("ternary").join("gft_layer2.t27")} +fn scratch_dir(l:&str)->PathBuf{let d=env::temp_dir().join(format!("t27_gl2_{}_{}",std::process::id(),l));if d.exists(){let _=fs::remove_dir_all(&d);}d} +fn tool_available(t:&str)->bool{Command::new(t).arg("-V").output().map(|o|o.status.success()).unwrap_or(false)} +const REFERENCE_RTL: &str = r#####" +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_dot2 -- 2-term GF-T16 dot product: y = a1*b1 + a2*b2, the multiply-accumulate +// kernel at the heart of every matmul / attention / inference layer. Pure composition +// of the silicon-proven gft_mul with gft_add (both realizations of tri_gft_arith / +// tri_gft_add) -- no new arithmetic, just the MAC wiring. Combinational. +// +// This is the hardware twin of the NUMERICAL dot-product advantage measured in +// tests/gft_task_accuracy.rs: there GF-T16 owns the wide-dynamic-range dot product on +// paper; here the same dot product is computed in GF-T16 hardware, bit-exact to spec. +// +// Operands/result are packed GF-T16 magnitudes: [ offset:15..9 (7b) | mant:8..0 (9b) ], +// value = (1 + mant/512) * 2^(offset-40). +// ============================================================================ +module gft_dot2 ( + input wire [15:0] a1, + input wire [15:0] b1, + input wire [15:0] a2, + input wire [15:0] b2, + output wire [15:0] y +); + // term 1 = a1 * b1 + wire [31:0] p1_off, p1_mant; + gft_mul #(.BIAS(40), .OFFSET_MAX(80), .MANT_ONE(512)) u_m1 ( + .a_off({25'd0, a1[15:9]}), .a_mant({23'd0, a1[8:0]}), + .b_off({25'd0, b1[15:9]}), .b_mant({23'd0, b1[8:0]}), + .out_off(p1_off), .out_mant(p1_mant)); + + // term 2 = a2 * b2 + wire [31:0] p2_off, p2_mant; + gft_mul #(.BIAS(40), .OFFSET_MAX(80), .MANT_ONE(512)) u_m2 ( + .a_off({25'd0, a2[15:9]}), .a_mant({23'd0, a2[8:0]}), + .b_off({25'd0, b2[15:9]}), .b_mant({23'd0, b2[8:0]}), + .out_off(p2_off), .out_mant(p2_mant)); + + // accumulate: term1 + term2 (same-sign GF-T add) + wire [31:0] y_off, y_mant; + gft_add #(.OFFSET_MAX(80), .MANT_ONE(512), .SIG_BITS(10)) u_acc ( + .a_off(p1_off), .a_mant(p1_mant), + .b_off(p2_off), .b_mant(p2_mant), + .out_off(y_off), .out_mant(y_mant)); + + assign y = {y_off[6:0], y_mant[8:0]}; +endmodule +`default_nettype wire + +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_mul -- GF-T ladder multiplier (balanced-ternary exponent). +// +// Verified realization of specs/tri_gft_arith.t27's gft_mul_offset_full_p + +// gft_mul_mant_p + gft_mul_mant_carry_p -- the SAME spec the over-wire verifier +// runs (trinet_compute_over_mesh / trinet_rung_verify). SSOT is the .t27; this +// .v is the synthesizable realization (as fpga/gf16/gf16_mul.v is for GF16). +// +// t27c gen-verilog cannot emit this directly yet: it interleaves `reg` +// declarations with statements inside begin/end blocks (illegal Verilog; iverilog +// rejects it). Tracked upstream; this hand-transcription keeps the exact logic +// with legal declaration ordering, gated by an iverilog KAT sweep below. +// +// Combinational. Parametric per rung; GF-T16 defaults (bias 40, offset_max 80, +// mant_one 512). GF-T8 = (13, 26, 16); GF-T4 = (4, 8, 2); GF-T32 uses wider mant. +// ============================================================================ +module gft_mul #( + parameter [31:0] BIAS = 40, + parameter [31:0] OFFSET_MAX = 80, + parameter [31:0] MANT_ONE = 512 +) ( + input wire [31:0] a_off, + input wire [31:0] a_mant, + input wire [31:0] b_off, + input wire [31:0] b_mant, + output wire [31:0] out_off, + output wire [31:0] out_mant +); + // Full-precision significand product (1+M/mant_one) scaled by mant_one^2. + wire [31:0] prod = (MANT_ONE + a_mant) * (MANT_ONE + b_mant); + wire [31:0] thresh = (2 * MANT_ONE) * MANT_ONE; // one-bit renorm boundary + wire carry = (prod >= thresh); // mantissa overflow -> exp += 1 + + // Exponent offset: add offsets, apply the carry, de-bias, saturate at the rung's max. + wire [31:0] sum = a_off + b_off + {31'd0, carry}; + wire [31:0] result = sum - BIAS; + assign out_off = (sum < BIAS) ? 32'd0 : + (result >= OFFSET_MAX) ? OFFSET_MAX : result; + + // Mantissa: renormalize by the carry (divisors are constant powers of two -> shifts). + assign out_mant = carry ? ((prod / (2 * MANT_ONE)) - MANT_ONE) + : ((prod / MANT_ONE ) - MANT_ONE); +endmodule +`default_nettype wire + +`timescale 1ns / 1ps +`default_nettype none +// ============================================================================ +// gft_add -- GF-T ladder adder (SAME-sign add), balanced-ternary exponent. +// +// Verified realization of specs/tri_gft_add.t27's gft_add_offset_c_p + +// gft_add_mant_c_p (via gft_add_sb_p / _offset_p / _mant_p) -- the SAME spec the +// over-wire verifier runs (trinet_rung_verify, trinet_compute_over_mesh). Align +// the smaller operand by the exponent-offset difference (barrel shift), add the +// significands, and renormalize by one carry. Combinational; parametric per rung. +// GF-T16 defaults: offset_max 80, mant_one 512, sig_bits 10 (mant_bits+1). +// ============================================================================ +module gft_add #( + parameter [31:0] OFFSET_MAX = 80, + parameter [31:0] MANT_ONE = 512, + parameter [31:0] SIG_BITS = 10 +) ( + input wire [31:0] a_off, + input wire [31:0] a_mant, + input wire [31:0] b_off, + input wire [31:0] b_mant, + output wire [31:0] out_off, + output wire [31:0] out_mant +); + // Order operands so `hi` has the larger (or equal) exponent offset. + wire a_hi = (a_off >= b_off); + wire [31:0] hi_off = a_hi ? a_off : b_off; + wire [31:0] hi_m = a_hi ? a_mant : b_mant; + wire [31:0] lo_off = a_hi ? b_off : a_off; + wire [31:0] lo_m = a_hi ? b_mant : a_mant; + + // Align the smaller significand right by the offset difference (0 if it underflows). + wire [31:0] d = hi_off - lo_off; + wire [31:0] sb = (d >= SIG_BITS) ? 32'd0 : ((MANT_ONE + lo_m) >> d[4:0]); + wire [31:0] sum = (MANT_ONE + hi_m) + sb; + + // Renormalize: a significand >= 2*mant_one carries into the exponent (+1, saturate). + wire carry = (sum >= (2 * MANT_ONE)); + wire [31:0] e = hi_off + 32'd1; + assign out_off = carry ? ((e >= OFFSET_MAX) ? OFFSET_MAX : e) : hi_off; + assign out_mant = carry ? ((sum >> 1) - MANT_ONE) : (sum - MANT_ONE); +endmodule +`default_nettype wire + +"#####; +const TESTBENCH: &str = r#"`timescale 1ns/1ps +module tb; + reg [15:0] a1,a2,w0a,w0b,w1a,w1b; wire [31:0] y_spec; wire [15:0] n0,n1; integer i,fails,o,m; + GftLayer2 dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.a1(a1),.a2(a2),.w0a(w0a),.w0b(w0b),.w1a(w1a),.w1b(w1b),.ready(),.result(y_spec)); + gft_dot2 rn0(.a1(w0a),.b1(a1),.a2(w0b),.b2(a2),.y(n0)); + gft_dot2 rn1(.a1(w1a),.b1(a1),.a2(w1b),.b2(a2),.y(n1)); + wire [31:0] y_ref = {n1, n0}; + function [15:0] rnd; input integer dd; begin o=1+($random%79);if(o<1)o=1;if(o>79)o=79;m=$random%512;if(m<0)m=-m;rnd=(o<<9)|m; end endfunction + initial begin + fails=0; + for(i=0;i<2000;i=i+1) begin + a1=rnd(0);a2=rnd(0);w0a=rnd(0);w0b=rnd(0);w1a=rnd(0);w1b=rnd(0); #1; + if(y_spec!==y_ref) begin fails=fails+1; if(fails<=5)$display("FAIL spec=%h ref=%h",y_spec,y_ref); end + end + if(fails==0)$display("ALL_PASS 2000"); else $display("FAILED %0d",fails); + $finish; + end +endmodule +"#; +#[test] +fn spec_first_gft_layer2_matches_silicon(){ + let gen=Command::new(t27c()).arg("gen-verilog").arg(spec_path()).output().expect("gen"); + assert!(gen.status.success(),"gen-verilog failed:\n{}",String::from_utf8_lossy(&gen.stderr)); + let v=String::from_utf8_lossy(&gen.stdout).into_owned(); + assert!(v.contains("output wire [31:0] result")&&v.contains("input wire [15:0] w1b"),"missing layer interface:\n{}",v); + if !tool_available("iverilog")||!tool_available("vvp"){eprintln!("SKIP: no iverilog/vvp");return;} + let d=scratch_dir("chk"); fs::create_dir_all(&d).unwrap(); + fs::write(d.join("spec.v"),&gen.stdout).unwrap(); fs::write(d.join("ref.v"),REFERENCE_RTL).unwrap(); fs::write(d.join("tb.v"),TESTBENCH).unwrap(); + let vvp=d.join("s.vvp"); + let c=Command::new("iverilog").args(["-g2012","-o",vvp.to_str().unwrap()]).arg(d.join("spec.v")).arg(d.join("ref.v")).arg(d.join("tb.v")).output().unwrap(); + assert!(c.status.success(),"iverilog failed:\n{}",String::from_utf8_lossy(&c.stderr)); + let r=Command::new("vvp").arg(&vvp).output().unwrap(); + let o=String::from_utf8_lossy(&r.stdout).into_owned(); let _=fs::remove_dir_all(&d); + assert!(o.contains("ALL_PASS 2000"),"layer differs from silicon:\n{}",o); + assert!(!o.contains("FAIL"),"layer mismatch:\n{}",o); +} diff --git a/bootstrap/tests/gft_mul_rne.rs b/bootstrap/tests/gft_mul_rne.rs new file mode 100644 index 0000000000..b3754568e0 --- /dev/null +++ b/bootstrap/tests/gft_mul_rne.rs @@ -0,0 +1,119 @@ +// ============================================================================ +// Check for the spec-first ROUND-TO-NEAREST-EVEN GF-T16 multiply (specs/ternary/ +// gft_mul_rne.t27): a GF-T mul that rounds the mantissa to nearest-even, matching +// the IDEAL oracle (trinity-fpga/conformance/gft16_ref.py) -- and therefore MORE +// ACCURATE than the truncating silicon gft_mul (which is ~1 ULP low, ~37% of +// products off-by-one). Verified bit-exact against 300 oracle-generated +// normal-range vectors (tests/gft_mul_rne_vectors.txt, ~half of which differ from +// the truncating silicon). Skips without iverilog/vvp. +// ============================================================================ + +use std::env; +use std::fs; +use std::path::PathBuf; +use std::process::Command; + +fn t27c() -> &'static str { + env!("CARGO_BIN_EXE_t27c") +} + +fn spec_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("..") + .join("specs") + .join("ternary") + .join("gft_mul_rne.t27") +} + +fn vectors_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("tests") + .join("gft_mul_rne_vectors.txt") +} + +fn tool_available(t: &str) -> bool { + Command::new(t) + .arg("-V") + .output() + .map(|o| o.status.success()) + .unwrap_or(false) +} + +#[test] +fn spec_first_gft_mul_rne_matches_oracle() { + let gen = Command::new(t27c()) + .arg("gen-verilog") + .arg(spec_path()) + .output() + .expect("invoke gen-verilog"); + assert!( + gen.status.success(), + "gen-verilog of gft_mul_rne.t27 failed:\n{}", + String::from_utf8_lossy(&gen.stderr) + ); + let verilog = String::from_utf8_lossy(&gen.stdout).into_owned(); + assert!( + verilog.contains("input wire [15:0] a") && verilog.contains("output wire [15:0] result"), + "GF-T RNE mul did not expose the a,b -> result interface:\n{}", + verilog + ); + + if !tool_available("iverilog") || !tool_available("vvp") { + eprintln!("SKIP: iverilog/vvp not on PATH; skipping GF-T RNE oracle check"); + return; + } + + let vectors = fs::read_to_string(vectors_path()).expect("read oracle vectors"); + let n_vectors = vectors.lines().filter(|l| !l.trim().is_empty()).count(); + + let dir = env::temp_dir().join(format!("t27_rne_{}", std::process::id())); + let _ = fs::remove_dir_all(&dir); + fs::create_dir_all(&dir).expect("scratch dir"); + fs::write(dir.join("spec.v"), &gen.stdout).expect("write spec.v"); + fs::write(dir.join("vec.txt"), &vectors).expect("write vec.txt"); + + let tb = format!( + r#"`timescale 1ns/1ps +module tb; + reg [15:0] a,b; wire [15:0] y; integer fails,n,fd,code; reg [15:0] exp; + GftMulRne dut(.clk(1'b0),.rst_n(1'b1),.en(1'b1),.a(a),.b(b),.ready(),.result(y)); + initial begin + fails=0; n=0; fd=$fopen("{}","r"); + while(!$feof(fd)) begin code=$fscanf(fd,"%h %h %h\n",a,b,exp); + if(code==3) begin #1; n=n+1; + if(y!==exp) begin fails=fails+1; if(fails<=6)$display("FAIL a=%h b=%h y=%h exp=%h",a,b,y,exp); end + end end + $fclose(fd); + if(fails==0)$display("ALL_PASS %0d",n); else $display("FAILED %0d/%0d",fails,n); + $finish; + end +endmodule +"#, + dir.join("vec.txt").to_str().unwrap() + ); + fs::write(dir.join("tb.v"), tb).expect("write tb.v"); + + let vvp = dir.join("sim.vvp"); + let compile = Command::new("iverilog") + .args(["-g2012", "-o", vvp.to_str().unwrap()]) + .arg(dir.join("spec.v")) + .arg(dir.join("tb.v")) + .output() + .expect("invoke iverilog"); + assert!( + compile.status.success(), + "iverilog compile failed:\n{}", + String::from_utf8_lossy(&compile.stderr) + ); + + let run = Command::new("vvp").arg(&vvp).output().expect("invoke vvp"); + let stdout = String::from_utf8_lossy(&run.stdout).into_owned(); + let _ = fs::remove_dir_all(&dir); + + assert!( + stdout.contains(&format!("ALL_PASS {}", n_vectors)), + "RNE GF-T mul differs from the oracle:\n{}", + stdout + ); + assert!(!stdout.contains("FAIL"), "RNE GF-T mul mismatch:\n{}", stdout); +} diff --git a/bootstrap/tests/gft_mul_rne_vectors.txt b/bootstrap/tests/gft_mul_rne_vectors.txt new file mode 100644 index 0000000000..4b8925ae35 --- /dev/null +++ b/bootstrap/tests/gft_mul_rne_vectors.txt @@ -0,0 +1,300 @@ +4a1d 57dc 520a +48a0 3073 2937 +58fc 6785 70a0 +6eff 360d 5512 +451e 5eba 5420 +5a49 3e8e 48eb +6287 3a01 4c88 +2adc 44a9 1fce +3f41 4ecb 3e46 +6eba 44c9 63cc +5a16 5171 5b97 +5e95 3f0e 4df2 +3334 5403 3739 +553d 336b 38c4 +5143 66bd 683c +66b4 663a 7d02 +4b6e 2d9d 2919 +2dac 7176 4f2d +5a09 75cf 7fe0 +2ec9 4079 1f72 +4960 656b 5ee2 +6dd9 4a6e 6856 +752e 5825 7d69 +60d5 355c 4661 +6a97 595c 742d +4c5e 6f3f 6bd8 +52b5 5050 5321 +3def 50a5 3e9a +319f 3420 15d9 +4900 57d2 50de +5e39 3c21 4a5e +68d4 5485 6d90 +73a7 3a6d 5e37 +3f7d 6098 5043 +312d 5e90 4009 +65d0 3ff3 55c4 +5318 672a 6a72 +6696 5c73 732b +5ab7 6fff 7ab6 +545b 41f7 4656 +4d71 6a40 67df +5623 7539 7b71 +591f 71f1 7b13 +4b5c 4eb6 4a47 +75e5 2b00 50ec +53da 4d27 5109 +6b64 5718 729f +5766 5eb0 6649 +6356 5891 6c24 +6ccb 3f72 5c68 +6650 4faa 661e +3fae 7535 64f3 +701c 4cc8 6cef +3fc3 74b9 648f +462a 41e2 381a +4637 3e88 34ce +38b9 53ee 3cad +4224 71a9 63eb +6585 5649 6c03 +74f3 457e 6a93 +2b9f 571d 32d2 +5f7e 3824 47bd +7061 512e 71c8 +6f5b 6b2c 8aa9 +57ad 3ba3 4358 +737a 6fde 935c +3d87 3fe8 2d72 +425d 3b67 2e03 +2a6e 5b4d 3601 +7290 6f4d 921d +73b7 5bba 7f76 +472a 69eb 6119 +5aa2 5b0a 6600 +5101 69a9 6ac0 +2d3a 53f7 3133 +4fe8 3c18 3c0b +38fb 632c 4c5d +2f91 3a0d 19a8 +6718 6ef9 864d +66fb 2ff5 46f3 +4d24 3d2c 3a7e +6879 6610 7e8d +3b21 5158 3c9e +4e1b 6ddb 6c08 +5687 5825 5eb6 +2bd2 4a6e 2652 +6e0e 43b7 61d1 +61ed 738a 8579 +66c9 5d2f 7437 +6536 3203 473b +6125 75e3 870e +50a9 3de9 3e9a +7152 689d 8a2b +6031 7446 847e +4657 4c40 42a2 +2db7 5446 321d +5c32 687e 74bc +3871 4689 2f18 +4e99 62bb 618c +40a5 5e44 4eff +446e 2f84 2423 +323a 4c79 2ec1 +5c0a 3bba 47cd +35f5 53f5 39ea +5639 588d 5ed6 +4f29 3ce1 3c46 +4af1 3304 2e38 +4e88 6cf0 6bb8 +598e 64b7 6e6a +3b5d 2c57 17ef +725d 2e7f 50f3 +6af4 658f 80a1 +654b 666e 7c00 +6d89 2c36 49e8 +3ce4 6076 4d8f +34d8 688f 4da3 +5af0 5728 6251 +558b 5783 5d1c +3b2f 57bb 42f8 +5825 6cdc 7511 +4040 5c63 4caf +2ebe 2ecf 0dda +43f5 2fec 23e1 +57b5 2be1 3398 +514b 61dc 632d +64c4 369e 4b9e +3f7f 338a 2318 +6704 3c70 53ad +4d25 3ef0 3c4f +2e20 6760 4596 +583c 5216 5a55 +649f 6678 7b3c +53d0 4ef5 52d2 +3ecd 2e19 1cf0 +7250 479a 6a15 +58bc 51df 5aa5 +5844 4fdf 5831 +3eb3 48d5 37d2 +2f15 6006 3f1e +65cf 31a4 4777 +3e22 2f66 1da0 +36f2 33f6 1aeb +3437 66f9 4b4b +3196 683d 4a02 +31a1 4bc8 2d6e +5026 30c7 30fc +419c 6ac0 5c7b +6e56 4741 65cd +36a5 344d 1b0b +45c3 2d6e 233a +6981 6087 7a37 +2bcb 50e5 2cbf +708e 393f 5a13 +670d 359c 4cc1 +5284 3a53 3cec +6656 49b6 602b +731a 483e 6b7a +6831 48cc 6111 +4e64 5849 56bb +5f84 5200 6184 +4e1c 3bc4 39f9 +3c30 2db5 1a07 +4d87 3685 3439 +5339 32ad 3628 +3bfd 4b4a 3748 +4e41 2e1c 2c61 +2c33 3885 14c5 +5708 6011 6722 +47b7 6c80 6452 +5952 436e 4cd9 +2aa7 3e61 1928 +4caf 6c93 6974 +63b7 6079 744c +55c8 52e9 58c0 +64af 61c4 7687 +31e4 3ff7 21db +2a81 37ad 124d +3001 4421 2422 +73ed 496a 6d5a +5cdc 64ce 7201 +4d36 436d 40c0 +4968 58fe 528c +319a 6965 4b0e +3cf4 3df5 2aec +5a60 2ead 392d +5d20 36cc 442f +53e1 665d 6a4b +420a 5a6a 4c76 +6abd 758e 906f +2c1b 533f 2f6b +6be7 5b98 7782 +623e 7496 86e6 +5e14 58d3 66ef +4e4f 4e1b 4c6e +35a7 573a 3cf2 +2af0 4c49 275b +2f33 3567 14b9 +71ee 445e 6653 +395e 49b1 331b +5d8f 2b83 3920 +40d4 6d49 5e53 +5a6f 537e 5e20 +48d9 372c 3042 +504f 4cab 4d14 +32bd 5ee6 41f8 +33a0 73aa 5752 +47ee 60fa 58ed +511f 5e56 5fa5 +55af 401f 45e8 +3d2e 38bc 262c +614d 4268 53f9 +543e 33f0 3835 +3a4a 6d46 57bf +4389 64ea 5893 +6601 36c6 4cc7 +3e5f 3957 27f6 +3c6b 59c3 4646 +5269 4176 4416 +36c8 32d3 19ed +52b1 59d5 5c94 +359c 49dd 2f7c +5a78 2b7f 3628 +3bfb 2b86 1782 +55f6 332f 3927 +2dea 396a 1757 +4387 5491 4843 +4e5a 6870 66de +4f59 5e40 5dc4 +6c33 60e1 7d2a +5f15 484b 5789 +3c62 4de9 3a54 +618b 40fa 52a3 +356c 6284 4827 +3490 2b71 1034 +2d00 2dd5 0ae0 +5a50 6c36 768e +45c5 420c 37dc +6657 6d1d 83a4 +6617 6a36 804f +3fbd 5c24 4c00 +45af 2da7 235d +600f 5aaa 6abe +5536 3cc3 4238 +617a 32dd 447d +5cc3 5f15 6c21 +3b74 6725 52b7 +2aad 39d4 1490 +3386 3224 15c5 +5ec9 3c12 4ae2 +69d5 528b 6c70 +644f 4975 5dfe +2cbd 2bb7 088b +3486 4d7d 3233 +549b 452c 4a11 +6c5c 7122 8db2 +3999 377f 2125 +51e9 59c6 5bb0 +488f 730d 6be7 +2c0c 6f8a 4b9f +3bec 4839 342e +2ad8 2bac 069c +46f1 6b3a 625f +30f4 6a27 4b2e +5a15 5730 6151 +6269 627e 7501 +591a 738f 7cc2 +5aaa 504f 5b13 +62d9 318e 4488 +3732 6b7e 52ca +5fd3 3b67 4b41 +3203 68d4 4ad8 +722b 643d 866d +355e 3893 1e2b +590d 551a 5e5e +667f 3d0c 53cd +4b02 2d8d 28ac +3f0d 49c1 38dd +4035 3b6b 2bc6 +7009 39d2 59e3 +2e28 681a 4644 +7478 5fa6 8440 +6ce2 6271 7f85 +325f 742b 5692 +3337 6447 47a9 +4d9e 3938 36e9 +4b31 6532 608d +2bfd 53dc 2fd9 +5add 3d0d 482f +53d4 445a 4840 +3c51 57b3 4424 +6394 6cb3 806a +43f6 3aad 2ea6 +6b60 6211 7d7d +3d12 61f9 4f0d +6add 6ef5 8a1e +3f01 5f41 4e72 +4ec8 3709 361c +610e 57f2 6903 +3471 3958 1e0a +3723 36b7 1e21 diff --git a/bootstrap/tests/stream_ternary_mac.rs b/bootstrap/tests/stream_ternary_mac.rs new file mode 100644 index 0000000000..8387089e49 --- /dev/null +++ b/bootstrap/tests/stream_ternary_mac.rs @@ -0,0 +1,170 @@ +// ============================================================================ +// Check for the spec-first STREAMING ternary MAC (specs/ternary/ +// stream_ternary_mac.t27, #1764). This is the on-hardware BitNet inference +// primitive: `on_clock(a, b)` params become streaming INPUT data ports, and +// each cycle the 27-trit dot product of the current (a, b) pair is accumulated +// into a registered `acc` exposed as an OUTPUT data port. +// +// Verifies the generated module: +// * has real input data ports `a`, `b` and an output port `acc`, +// * (with yosys) synthesizes to real Artix-7 fabric -- FDCE accumulator + +// a LUT adder-tree, not zero cells, +// * (with iverilog) accumulates a stream of known trit-vector pairs to the +// exact running sum of their dot products, and freezes when `en` is low. +// Skips the simulation/synth legs when the tools are absent. +// ============================================================================ + +use std::env; +use std::fs; +use std::path::PathBuf; +use std::process::Command; + +fn t27c() -> &'static str { + env!("CARGO_BIN_EXE_t27c") +} + +fn spec_path() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("..") + .join("specs") + .join("ternary") + .join("stream_ternary_mac.t27") +} + +fn scratch_dir(label: &str) -> PathBuf { + let dir = env::temp_dir().join(format!("t27_smac_{}_{}", std::process::id(), label)); + if dir.exists() { + let _ = fs::remove_dir_all(&dir); + } + dir +} + +fn tool_available(tool: &str) -> bool { + Command::new(tool) + .arg("-V") + .output() + .map(|o| o.status.success()) + .unwrap_or(false) +} + +// Stream four known pairs; acc must track the running sum of dot products. +// (0,0) -> all N.N = +27 => 27 +// (allP, allP) -> +27 => 54 +// (0, allP) -> -27 => 27 +// (allZ, allZ) -> 0 => 27 +// then en=0 must freeze acc at 27. +const TESTBENCH: &str = r#"`timescale 1ns/1ps +module tb; + reg clk,rst_n,en; reg [63:0] a,b; wire ready; wire signed [31:0] acc; + integer fails; + StreamTernaryMac dut(.clk(clk),.rst_n(rst_n),.en(en),.a(a),.b(b),.ready(ready),.acc(acc)); + initial clk=0; always #5 clk=~clk; + task step(input [63:0] av, input [63:0] bv, input integer exp); begin + a=av; b=bv; @(negedge clk); + if (acc!==exp) begin fails=fails+1; $display("FAIL acc=%0d exp=%0d",acc,exp); end + end endtask + initial begin + fails=0; rst_n=0; en=0; a=0; b=0; @(negedge clk); @(negedge clk); + if (acc!==0) begin fails=fails+1; $display("FAIL reset acc=%0d",acc); end + rst_n=1; en=1; + step(64'd0, 64'd0, 27); + step(64'd12009599006321322, 64'd12009599006321322, 54); + step(64'd0, 64'd12009599006321322, 27); + step(64'd6004799503160661, 64'd6004799503160661, 27); + en=0; a=0; b=0; @(negedge clk); + if (acc!==27) begin fails=fails+1; $display("FAIL freeze acc=%0d",acc); end + if (fails==0) $display("ALL_PASS final=%0d",acc); else $display("FAILED %0d",fails); + $finish; + end +endmodule +"#; + +#[test] +fn spec_first_streaming_ternary_mac() { + let gen = Command::new(t27c()) + .arg("gen-verilog") + .arg(spec_path()) + .output() + .expect("invoke gen-verilog"); + assert!( + gen.status.success(), + "gen-verilog of stream_ternary_mac.t27 failed:\n{}", + String::from_utf8_lossy(&gen.stderr) + ); + let verilog = String::from_utf8_lossy(&gen.stdout).into_owned(); + + // Streaming input data ports (on_clock params) + an observable accumulator. + assert!( + verilog.contains("input wire [63:0] a") && verilog.contains("input wire [63:0] b"), + "on_clock params did not become input data ports:\n{}", + verilog + ); + assert!( + verilog.contains("output reg signed [31:0] acc"), + "accumulator was not exposed as an output data port:\n{}", + verilog + ); + assert!( + verilog.contains("acc <="), + "accumulator is not registered with a nonblocking update:\n{}", + verilog + ); + + // Synthesizes to real Artix-7 fabric: an FDCE accumulator, not zero cells. + if tool_available("yosys") { + let dir = scratch_dir("synth"); + fs::create_dir_all(&dir).expect("create synth dir"); + fs::write(dir.join("mac.v"), &gen.stdout).expect("write mac.v"); + let synth = Command::new("yosys") + .arg("-p") + .arg(format!( + "read_verilog -sv {}; synth_xilinx -top StreamTernaryMac; stat", + dir.join("mac.v").to_str().unwrap() + )) + .output() + .expect("invoke yosys"); + let s = String::from_utf8_lossy(&synth.stdout).into_owned() + + &String::from_utf8_lossy(&synth.stderr); + let _ = fs::remove_dir_all(&dir); + assert!(synth.status.success(), "yosys synth_xilinx failed:\n{}", s); + assert!( + s.contains("FDCE") || s.contains("FDRE"), + "streaming MAC produced no accumulator flip-flops:\n{}", + s + ); + } + + if !tool_available("iverilog") || !tool_available("vvp") { + eprintln!("SKIP: iverilog/vvp not on PATH; skipping streaming simulation"); + return; + } + + let dir = scratch_dir("chk"); + fs::create_dir_all(&dir).expect("create scratch dir"); + fs::write(dir.join("mac.v"), &gen.stdout).expect("write mac.v"); + fs::write(dir.join("tb.v"), TESTBENCH).expect("write tb.v"); + + let vvp_path = dir.join("sim.vvp"); + let compile = Command::new("iverilog") + .args(["-g2012", "-o", vvp_path.to_str().unwrap()]) + .arg(dir.join("mac.v")) + .arg(dir.join("tb.v")) + .output() + .expect("invoke iverilog"); + assert!( + compile.status.success(), + "iverilog compile failed:\n{}", + String::from_utf8_lossy(&compile.stderr) + ); + + let run = Command::new("vvp").arg(&vvp_path).output().expect("invoke vvp"); + let stdout = String::from_utf8_lossy(&run.stdout).into_owned(); + let _ = fs::remove_dir_all(&dir); + + assert!( + stdout.contains("ALL_PASS"), + "streaming MAC did not accumulate the dot-product stream correctly:\n{}", + stdout + ); + assert!(!stdout.contains("FAIL"), "streaming MAC mismatch:\n{}", stdout); +} diff --git a/docs/NOW.md b/docs/NOW.md index a90a74a86c..26de62f660 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,20 @@ +# NOW — feat: land the spec-first hardware stack (ports + GF-T MAC ladder) (2026-08-06) + +Last updated: 2026-08-06 + +## feat(gen-verilog): data ports + BitNet & GF-T spec-first hardware onto master (Refs #1764) + +- Branch: `feat/land-spec-first-hardware` + +### Что легло +The spec-first hardware work (11 improvement cycles), now that master is unblocked. Compiler: **opt-in data ports** — `on_clock` var state exposed as `output reg`, `on_clock`/`on_comb` params become `input` data ports, `on_comb` return drives an `output wire result`. Seal-neutral (gated on `on_clock`/`on_comb` fn names → existing specs byte-identical). Specs, each iverilog/yosys/oracle cross-checked: +- **BitNet path (synthesizes to Artix-7):** `comb_ternary_dot` (dot27→~317 LUT), `comb_bitnet_neuron` (quantize(dot27)→~319 LUT, a full neuron), `comb_bitnet_layer` (4 neurons→288 LUT const / ~1287 general), `stream_ternary_mac` (streaming MAC→32 FDCE), `clocked_counter` (8 FDCE). `docs/SYNTH_REPORT.md`. +- **GF-T path (bit-exact to the AX7203 silicon):** `gft_dot2` (silicon MAC), `gft_dot4`/`gft_dot8` (matmul/attention tiles), `gft_layer2` (matmul row) — all bit-exact to the silicon reduction tree (2000 vectors each). +- **GF-T RNE path (bit-exact to the IDEAL oracle, MORE ACCURATE than silicon):** `gft_mul_rne` + `gft_add_rne` + `gft_dot2_rne` — round-to-nearest-even, matching `gft16_ref.py` (300 vectors each); the silicon truncates ~1 ULP low. +Verified: 1535 unit tests pass; all 12 spec tests green on master's compiler; FROZEN_HASH resealed; new-spec seals regenerated. Supersedes the stale-base PR #1786. + +--- + # NOW — fix: repair all 7 gen-verilog regressions from batch merge #1783 (2026-08-06) Last updated: 2026-08-06 diff --git a/docs/SYNTH_REPORT.md b/docs/SYNTH_REPORT.md new file mode 100644 index 0000000000..659eb26f44 --- /dev/null +++ b/docs/SYNTH_REPORT.md @@ -0,0 +1,58 @@ +# Spec-first ternary stack — synthesis report (Artix-7) + +Real FPGA resource cost of the spec-first ternary hardware designs, measured with +**yosys 0.65 `synth_xilinx`** (the AX7203 / Artix-7 XC7A200T family — the same +flow openXC7 uses, no Vivado). Every design is generated from a `.t27` spec by +`t27c gen-verilog` — no hand-written RTL — and is functionally cross-checked in +iverilog against an independent reference (see `bootstrap/tests/*.rs`). + +## Why this report exists + +Until this was measured, the stack was only ever **simulated** (iverilog). But +iverilog-clean ≠ synthesizable, and — more subtly — a design with no data ports +synthesizes to **zero cells** (the compute drives nothing observable, so the +synthesizer dead-code-eliminates all of it). The data-port work (`on_clock` / +`on_comb` interfaces) is what makes these designs *real hardware*; this report is +the evidence, in actual Xilinx primitives. + +## Results + +| design | spec | kind | LUT | FF | CARRY4 | MUXF7/8 | +|---|---|---|---:|---:|---:|---:| +| combinational dot product | `comb_ternary_dot.t27` | comb | 317 | 0 | 2 | 142 | +| **combinational BitNet neuron** | `comb_bitnet_neuron.t27` | comb | 319 | 0 | 2 | 141 | +| **BitNet layer, 4 neurons (trained/const weights)** | `comb_bitnet_layer.t27` | comb | 288 | 0 | 0 | ~140 | +| BitNet layer, 4 neurons (general/programmable weights) | *(measured, not committed)* | comb | 1287 | 0 | 8 | ~430 | +| clocked counter | `clocked_counter.t27` | seq | 0 | 8 | 2 | 0 | +| **streaming ternary MAC** | `stream_ternary_mac.t27` | seq | 346 | 32 | 10 | 143 | +| **GF-T16 MAC (a1·b1+a2·b2)** — bit-exact to silicon | `gft_dot2.t27` | comb | 501 | 0 | 123 | 0 | + +The GF-T16 MAC is the spec-first realization of the arithmetic **verified on real silicon** (AX7203, `gft_dot2` 3/3) — bit-exact to the hand-written RTL over 2000 random inputs. Its higher CARRY4 count is because `gen-verilog` lowers `*` to a shift-add multiplier rather than inferring a DSP48; a DSP-mapping pass would shrink it substantially. + +- **comb** = purely combinational (no flip-flops); **seq** = sequential (registered state). +- LUT = sum of LUT1..LUT6; FF = FDCE/FDRE; the MUXF7/8 columns are the wide muxes the dot-product reduction maps to. + +## Reading the numbers + +- **A full BitNet neuron over one 27-trit chunk costs ~319 LUTs** (`quantize(dot27(a,b))`): a ternary dot-product adder-tree plus a sign activation, purely combinational (0 FFs), one LUT delay. +- **A 4-neuron layer scales linearly**: with general (programmable) weights it is **1287 LUTs ≈ 4 × 319** — the per-neuron cost is additive, as expected. With **trained constant weights baked in** the synthesizer const-folds the dot products and the same layer drops to **288 LUTs** (cheaper than a single general neuron). Baking trained weights in is a real area win for inference. +- **The streaming MAC adds a 32-bit accumulator** (32 FDCE + a wider carry chain) so it can sum dot products across cycles — the on-hardware inference primitive. +- The clocked counter is the minimal sequential proof: 8 FDCE + a CARRY4, 0 LUTs. + +## Headroom on the AX7203 (XC7A200T) + +The target part has **~133,800 6-input LUTs and ~267,600 flip-flops**. A single +combinational neuron (~319 LUTs) uses **~0.24 %** of the LUTs; a **general +4-neuron layer (1287 LUTs) is ~1 %** — so roughly **~100 such layers** fit +in parallel, or many more when weights are constant and const-fold. Equivalently, +a small time-multiplexed MAC engine can stream an entire network through one +accumulator using a few hundred LUTs. The fabric is nowhere near the constraint: +the gap to a running on-hardware layer is place-and-route (nextpnr-xilinx) + a +bitstream, not logic capacity. + +## Reproduce + +```bash +t27c gen-verilog specs/ternary/comb_bitnet_neuron.t27 > neuron.v +yosys -p "read_verilog -sv neuron.v; synth_xilinx -top CombBitnetNeuron; stat" +``` diff --git a/specs/ternary/clocked_counter.t27 b/specs/ternary/clocked_counter.t27 index f6937b1a49..75716d0920 100644 --- a/specs/ternary/clocked_counter.t27 +++ b/specs/ternary/clocked_counter.t27 @@ -12,6 +12,13 @@ module ClockedCounter; // en-gating (freeze) and per-cycle advance. It is the building block a streamed // ternary MAC needs to accumulate across cycles (the Phase-2 MVP gate). // +// Because an `on_clock` fn is present, each scalar module `var` (here `count`) +// is exposed as an `output reg` data port — so the registered state is +// observable and the design SYNTHESIZES to real flip-flops (yosys synth_xilinx: +// 8 FDCE + 2 CARRY4). Without an output port a synthesizer dead-code-eliminates +// the whole design to zero cells. This is the first spec-first design that maps +// to non-zero real hardware. +// // Specs without an `on_clock` fn are unaffected — their generated Verilog is // byte-identical to before this feature. diff --git a/specs/ternary/comb_bitnet_layer.t27 b/specs/ternary/comb_bitnet_layer.t27 new file mode 100644 index 0000000000..5b172284f3 --- /dev/null +++ b/specs/ternary/comb_bitnet_layer.t27 @@ -0,0 +1,62 @@ +module CombBitnetLayer; +// #1764: a full BitNet LAYER (4 neurons) in one combinational synthesizable +// module. One 27-trit activation vector `a` feeds four neurons, each with its +// own fixed 27-trit weight vector (trained weights baked in as consts -- the +// realistic inference case), producing four trit activations packed into the +// `result` output (2 bits per trit: neuron i in result[2i+1:2i]). +// +// This is the next architectural level above the single neuron: weights are +// constants (a real trained layer), the activation is the only input port, and +// each neuron is quantize(dot27(w_i, a)) -- a weighted ternary sum then sign. +// It synthesizes to ~4x the single-neuron LUT cost, still purely combinational. +// +// Weights here are the three canonical vectors (all +1 / all -1 / all 0) plus a +// repeat, so the layer's response to any activation is hand-checkable. + +// packed-trit constants: all +1, all -1, all 0. +const W_P : u64 = 12009599006321322; +const W_N : u64 = 0; +const W_Z : u64 = 6004799503160661; + +fn tmul(ta: u8, tb: u8) -> i8 { + if (ta == 1) { return 0; } + if (tb == 1) { return 0; } + if (ta == tb) { return 1; } + return -1; +} +fn tp(a: u64, b: u64, i: u32) -> i8 { + return tmul(((a >> (i << 1)) & 3) as u8, ((b >> (i << 1)) & 3) as u8); +} +fn dot27(a: u64, b: u64) -> i8 { + return tp(a,b,0) + tp(a,b,1) + tp(a,b,2) + tp(a,b,3) + tp(a,b,4) + + tp(a,b,5) + tp(a,b,6) + tp(a,b,7) + tp(a,b,8) + tp(a,b,9) + + tp(a,b,10) + tp(a,b,11) + tp(a,b,12) + tp(a,b,13) + tp(a,b,14) + + tp(a,b,15) + tp(a,b,16) + tp(a,b,17) + tp(a,b,18) + tp(a,b,19) + + tp(a,b,20) + tp(a,b,21) + tp(a,b,22) + tp(a,b,23) + tp(a,b,24) + + tp(a,b,25) + tp(a,b,26); +} +fn quantize(v: i8) -> u8 { + if (v > 0) { return 2; } + if (v < 0) { return 0; } + return 1; +} +// One neuron: weighted ternary sum of weight w and activation a, then sign. +fn neuron(w: u64, a: u64) -> u8 { + return quantize(dot27(w, a)); +} + +// The layer: 4 neurons over the shared activation `a`, trits packed 2 bits each. +fn on_comb(a: u64) -> u8 { + return (neuron(W_P, a)) + | (neuron(W_N, a) << 2) + | (neuron(W_Z, a) << 4) + | (neuron(W_P, a) << 6); +} + +// a = all +1: dots are +27, -27, 0, +27 -> trits P,N,Z,P = 2|0<<2|1<<4|2<<6 = 146 +test layer_allp { assert_eq(on_comb(12009599006321322), 146); } +// a = all -1: dots are -27, +27, 0, -27 -> trits N,P,Z,N = 0|2<<2|1<<4|0<<6 = 24 +test layer_alln { assert_eq(on_comb(0), 24); } +// a = all 0: every dot is 0 -> all Z = 1|1<<2|1<<4|1<<6 = 85 +test layer_allz { assert_eq(on_comb(6004799503160661), 85); } +endmodule diff --git a/specs/ternary/comb_bitnet_neuron.t27 b/specs/ternary/comb_bitnet_neuron.t27 new file mode 100644 index 0000000000..99c3b18405 --- /dev/null +++ b/specs/ternary/comb_bitnet_neuron.t27 @@ -0,0 +1,53 @@ +module CombBitnetNeuron; +// #1764: a full COMBINATIONAL BitNet neuron in one module = MAC + activation. +// +// `on_comb(a, b)` takes a packed 27-trit weight vector `a` and activation vector +// `b` on input data ports, computes their bit-exact ternary dot product, and +// re-ternarizes the sum to a trit output `result = quantize(dot27(a, b))`. That +// is exactly a BitNet neuron over one 27-trit chunk: weighted sum -> sign. +// +// It is a single self-contained hardware module: (a, b) input ports -> a LUT +// adder-tree (dot27) -> sign comparators (quantize) -> `result` output port, +// generated from spec and synthesizing to Artix-7 LUTs with NO flip-flops +// (purely combinational). Composed with the streaming accumulator +// (stream_ternary_mac.t27) this scales to a multi-chunk neuron; here the whole +// neuron is combinational, so a single (a, b) pair yields the activation in one +// LUT delay. +// +// dot27 / tmul / tp are the bit-exact primitives (#1743); quantize is the +// ternary activation (sign with a zero dead-band). + +fn tmul(ta: u8, tb: u8) -> i8 { + if (ta == 1) { return 0; } + if (tb == 1) { return 0; } + if (ta == tb) { return 1; } + return -1; +} +fn tp(a: u64, b: u64, i: u32) -> i8 { + return tmul(((a >> (i << 1)) & 3) as u8, ((b >> (i << 1)) & 3) as u8); +} +fn dot27(a: u64, b: u64) -> i8 { + return tp(a,b,0) + tp(a,b,1) + tp(a,b,2) + tp(a,b,3) + tp(a,b,4) + + tp(a,b,5) + tp(a,b,6) + tp(a,b,7) + tp(a,b,8) + tp(a,b,9) + + tp(a,b,10) + tp(a,b,11) + tp(a,b,12) + tp(a,b,13) + tp(a,b,14) + + tp(a,b,15) + tp(a,b,16) + tp(a,b,17) + tp(a,b,18) + tp(a,b,19) + + tp(a,b,20) + tp(a,b,21) + tp(a,b,22) + tp(a,b,23) + tp(a,b,24) + + tp(a,b,25) + tp(a,b,26); +} +// Ternary activation: sign of the weighted sum into a trit {N=0, Z=1, P=2}. +fn quantize(v: i8) -> u8 { + if (v > 0) { return 2; } + if (v < 0) { return 0; } + return 1; +} + +// The neuron: weighted sum then sign, exposed as `result` output port. +fn on_comb(a: u64, b: u64) -> u8 { + return quantize(dot27(a, b)); +} + +test neuron_pp { assert_eq(on_comb(12009599006321322, 12009599006321322), 2); } +test neuron_np { assert_eq(on_comb(0, 12009599006321322), 0); } +test neuron_zz { assert_eq(on_comb(6004799503160661, 6004799503160661), 1); } +test neuron_nn { assert_eq(on_comb(0, 0), 2); } +endmodule diff --git a/specs/ternary/comb_ternary_dot.t27 b/specs/ternary/comb_ternary_dot.t27 new file mode 100644 index 0000000000..8e89a0ec19 --- /dev/null +++ b/specs/ternary/comb_ternary_dot.t27 @@ -0,0 +1,43 @@ +module CombTernaryDot; +// #1764: a COMBINATIONAL spec-first datapath that synthesizes to real hardware. +// +// `on_comb` is the combinational counterpart of `on_clock`: its parameters +// become input data ports and its return is a continuously-driven `output wire +// result` (`assign result = on_comb(...)`). This is what makes the combinational +// half of the ternary stack real hardware -- without it, a bare `fn` result +// never reaches a module port, so a synthesizer dead-code-eliminates the whole +// design to zero cells (it was only ever exercised by testbenches that call the +// Verilog function hierarchically). +// +// Here `on_comb(a, b)` is the bit-exact 27-trit dot product (the same tmul/tp +// primitives verified vs an independent reference on 300 vectors, #1743). It +// synthesizes to a real Artix-7 LUT tree (yosys synth_xilinx: ~160 LUT6 + a +// CARRY4 reduction, no flip-flops -- pure combinational). + +// Sign-only ternary multiply of two packed trits {N=0b00, Z=0b01, P=0b10}. +fn tmul(ta: u8, tb: u8) -> i8 { + if (ta == 1) { return 0; } + if (tb == 1) { return 0; } + if (ta == tb) { return 1; } + return -1; +} +// One trit position i of two 54-bit packed vectors (trit i at [2i+1:2i]). +fn tp(a: u64, b: u64, i: u32) -> i8 { + return tmul(((a >> (i << 1)) & 3) as u8, ((b >> (i << 1)) & 3) as u8); +} + +// The combinational data interface: (a, b) input ports -> `result` output port. +fn on_comb(a: u64, b: u64) -> i8 { + return tp(a,b,0) + tp(a,b,1) + tp(a,b,2) + tp(a,b,3) + tp(a,b,4) + + tp(a,b,5) + tp(a,b,6) + tp(a,b,7) + tp(a,b,8) + tp(a,b,9) + + tp(a,b,10) + tp(a,b,11) + tp(a,b,12) + tp(a,b,13) + tp(a,b,14) + + tp(a,b,15) + tp(a,b,16) + tp(a,b,17) + tp(a,b,18) + tp(a,b,19) + + tp(a,b,20) + tp(a,b,21) + tp(a,b,22) + tp(a,b,23) + tp(a,b,24) + + tp(a,b,25) + tp(a,b,26); +} + +test dot_all_n_x_all_n { assert_eq(on_comb(0, 0), 27); } +test dot_all_n_x_all_p { assert_eq(on_comb(0, 12009599006321322), -27); } +test dot_all_p_x_all_p { assert_eq(on_comb(12009599006321322, 12009599006321322), 27); } +test dot_all_z { assert_eq(on_comb(6004799503160661, 6004799503160661), 0); } +endmodule diff --git a/specs/ternary/gft_add_rne.t27 b/specs/ternary/gft_add_rne.t27 new file mode 100644 index 0000000000..b341cd821d --- /dev/null +++ b/specs/ternary/gft_add_rne.t27 @@ -0,0 +1,66 @@ +module GftAddRne; +// #1764 + GF-T: a spec-first GF-T16 same-sign ADD with ROUND-TO-NEAREST-EVEN, +// bit-exact to the ideal oracle (trinity-fpga/conformance/gft16_ref.py). Companion +// to gft_mul_rne.t27: where the silicon gft_add TRUNCATES the aligned operand +// (`>> d`), this keeps the shifted-out bits as guard/sticky and rounds to nearest +// even -- so a spec-first GF-T adder MORE ACCURATE than the silicon RTL. +// +// GF-T16 packed magnitude: [ offset(7) : mant(9) ], value = (1+mant/512)*2^(offset-40). + +fn on_comb(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + // order so hi has the larger (or equal) exponent offset. + var hi_off : i32 = b_off; + var hi_m : i32 = b_mant; + var lo_off : i32 = a_off; + var lo_m : i32 = a_mant; + if (a_off >= b_off) { + hi_off = a_off; hi_m = a_mant; lo_off = b_off; lo_m = b_mant; + } + var hi_sig : i32 = 512 + hi_m; + var lo_sig : i32 = 512 + lo_m; + // align the smaller significand right by d; d>=11 contributes nothing to the + // round bit (lo_sig < 1024 < 2^(d-1)), so cap d at 11 to keep 1< 11) { d = 11; } + var lo_shift : i32 = lo_sig >> d; + var lo_rem : i32 = lo_sig - (lo_shift << d); // shifted-out (fractional) bits + var sum_int : i32 = hi_sig + lo_shift; // integer significand sum, [512, 2047] + + var out_off : i32 = hi_off; + var mant : i32 = 0; + if (sum_int >= 1024) { + // renormalize by one bit: guard = sum_int&1, sticky = (lo_rem != 0). + var g : i32 = sum_int & 1; + var pre : i32 = sum_int >> 1; // new significand [512, 1023] + mant = pre - 512; + // round-half-to-even at the shifted-out bit g (with sticky lo_rem). + if (g == 1) { + if (lo_rem > 0) { mant = mant + 1; } + else { if ((pre & 1) == 1) { mant = mant + 1; } } + } + out_off = hi_off + 1; + if (out_off >= 80) { out_off = 80; } + } else { + // no renorm: round based on the fractional part lo_rem / 2^d vs 1/2. + mant = sum_int - 512; + var twice : i32 = lo_rem << 1; + var half : i32 = 1 << d; + if (twice > half) { mant = mant + 1; } + else { if (twice == half) { if ((sum_int & 1) == 1) { mant = mant + 1; } } } + } + // mantissa carry after rounding. + if (mant >= 512) { + mant = 0; + out_off = out_off + 1; + if (out_off >= 80) { out_off = 80; } + } + return ((out_off << 9) | mant) as u16; +} + +// 1.0 + 1.0 = 2.0 -> offset 41, mant 0 = 20992. +test add_ones { assert_eq(on_comb(20480, 20480), 20992); } +endmodule diff --git a/specs/ternary/gft_dot2.t27 b/specs/ternary/gft_dot2.t27 new file mode 100644 index 0000000000..f527d449b1 --- /dev/null +++ b/specs/ternary/gft_dot2.t27 @@ -0,0 +1,75 @@ +module GftDot2; +// #1764 + GF-T: a SPEC-FIRST GF-T16 2-term dot product (MAC), y = a1*b1 + a2*b2. +// +// GF-T16 is the ternary-native GoldenFloat format now proven bit-exact ON SILICON +// (AX7203, gft_dot2 3/3). Its MAC is the kernel of every matmul / inference layer. +// The hand-written trinity-fpga/build/gft_dot2/*.v note that `t27c gen-verilog` +// could not emit this directly because it interleaved `reg` decls with statements +// (illegal Verilog) -- that backend bug is FIXED (#1741 hoists fn-local decls), so +// this is the spec-first realization of the SAME arithmetic, bit-exact to the +// silicon-proven RTL. +// +// GF-T16 packed magnitude: [ offset(7) : mant(9) ], value = (1 + mant/512) * +// 2^(offset-40). BIAS=40, OFFSET_MAX=80, MANT_ONE=512 (=1<<9), SIG_BITS=10. +// All intermediates are non-negative small integers, so i32 arithmetic (signed +// shifts/compares/multiply on positive values) is bit-identical to the unsigned +// hardware and keeps the typechecker's literal typing happy. + +// GF-T ladder multiply (magnitude): sign-free, balanced-ternary exponent add. +fn gft_mul(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + // full-precision significand product (1+M/512) scaled by 512^2 + var prod : i32 = (512 + a_mant) * (512 + b_mant); + var carry : i32 = 0; + if (prod >= 524288) { carry = 1; } // 2*512*512 renorm boundary + var sum : i32 = a_off + b_off + carry; + var out_off : i32 = 0; + if (sum >= 40) { + var result : i32 = sum - 40; + if (result >= 80) { out_off = 80; } else { out_off = result; } + } + // renormalize the mantissa by the carry (divisors are powers of two -> shifts) + var out_mant : i32 = (prod >> 9) - 512; + if (carry == 1) { out_mant = (prod >> 10) - 512; } + return ((out_off << 9) | out_mant) as u16; +} + +// GF-T ladder add (same-sign): align the smaller operand, add, renormalize by one carry. +fn gft_add(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + var hi_off : i32 = b_off; + var hi_m : i32 = b_mant; + var lo_off : i32 = a_off; + var lo_m : i32 = a_mant; + if (a_off >= b_off) { + hi_off = a_off; hi_m = a_mant; lo_off = b_off; lo_m = b_mant; + } + var d : i32 = hi_off - lo_off; + var sb : i32 = 0; + if (d < 10) { sb = (512 + lo_m) >> d; } // align smaller significand right + var sum : i32 = (512 + hi_m) + sb; + var out_off : i32 = hi_off; + var out_mant : i32 = sum - 512; + if (sum >= 1024) { // significand carry -> exp += 1 + var e : i32 = hi_off + 1; + if (e >= 80) { out_off = 80; } else { out_off = e; } + out_mant = (sum >> 1) - 512; + } + return ((out_off << 9) | out_mant) as u16; +} + +// The MAC: y = a1*b1 + a2*b2, the multiply-accumulate at the heart of inference. +fn on_comb(a1: u16, b1: u16, a2: u16, b2: u16) -> u16 { + return gft_add(gft_mul(a1, b1), gft_mul(a2, b2)); +} + +// 1.0 = (1 + 0/512) * 2^0 -> offset 40, mant 0 -> 40<<9 = 20480 = 0x5000. +test one_times_one_mul { assert_eq(gft_mul(20480, 20480), 20480); } // 1*1 = 1 +test dot_one { assert_eq(on_comb(20480, 20480, 20480, 20480), 20992); } // 1*1+1*1 = 2 (0x5200) +endmodule diff --git a/specs/ternary/gft_dot2_rne.t27 b/specs/ternary/gft_dot2_rne.t27 new file mode 100644 index 0000000000..6637c05ce2 --- /dev/null +++ b/specs/ternary/gft_dot2_rne.t27 @@ -0,0 +1,84 @@ +module GftDot2Rne; +// #1764 + GF-T: a spec-first GF-T16 2-term MAC (y = a1*b1 + a2*b2) with full +// ROUND-TO-NEAREST-EVEN -- bit-exact to the IDEAL oracle +// gft16_add(gft16_mul(a1,b1), gft16_mul(a2,b2)) (trinity-fpga/conformance/ +// gft16_ref.py). This is the accurate counterpart of gft_dot2.t27, which matches +// the TRUNCATING silicon (biased ~1 ULP low). Composes gft_mul_rne + gft_add_rne. +// +// GF-T16 packed magnitude: [ offset(7) : mant(9) ], value = (1+mant/512)*2^(offset-40). + +// round-to-nearest-even GF-T multiply (matches gft_mul_rne.t27). +fn gmul(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + var prod : i32 = (512 + a_mant) * (512 + b_mant); + var carry : i32 = 0; + if (prod >= 524288) { carry = 1; } + var q : i32 = prod >> 9; + var r : i32 = prod & 511; + var half : i32 = 256; + if (carry == 1) { q = prod >> 10; r = prod & 1023; half = 512; } + var mant : i32 = q - 512; + if (r > half) { mant = mant + 1; } + if (r == half) { if ((q & 1) == 1) { mant = mant + 1; } } + var sum : i32 = a_off + b_off + carry; + var out_off : i32 = 0; + if (sum >= 40) { + var result : i32 = sum - 40; + if (result >= 80) { out_off = 80; } else { out_off = result; } + } + if (mant >= 512) { mant = 0; out_off = out_off + 1; if (out_off >= 80) { out_off = 80; } } + return ((out_off << 9) | mant) as u16; +} + +// round-to-nearest-even GF-T same-sign add (matches gft_add_rne.t27). +fn gadd(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + var hi_off : i32 = b_off; + var hi_m : i32 = b_mant; + var lo_off : i32 = a_off; + var lo_m : i32 = a_mant; + if (a_off >= b_off) { hi_off = a_off; hi_m = a_mant; lo_off = b_off; lo_m = b_mant; } + var hi_sig : i32 = 512 + hi_m; + var lo_sig : i32 = 512 + lo_m; + var d : i32 = hi_off - lo_off; + if (d > 11) { d = 11; } + var lo_shift : i32 = lo_sig >> d; + var lo_rem : i32 = lo_sig - (lo_shift << d); + var sum_int : i32 = hi_sig + lo_shift; + var out_off : i32 = hi_off; + var mant : i32 = 0; + if (sum_int >= 1024) { + var g : i32 = sum_int & 1; + var pre : i32 = sum_int >> 1; + mant = pre - 512; + if (g == 1) { + if (lo_rem > 0) { mant = mant + 1; } + else { if ((pre & 1) == 1) { mant = mant + 1; } } + } + out_off = hi_off + 1; + if (out_off >= 80) { out_off = 80; } + } else { + mant = sum_int - 512; + var twice : i32 = lo_rem << 1; + var half : i32 = 1 << d; + if (twice > half) { mant = mant + 1; } + else { if (twice == half) { if ((sum_int & 1) == 1) { mant = mant + 1; } } } + } + if (mant >= 512) { mant = 0; out_off = out_off + 1; if (out_off >= 80) { out_off = 80; } } + return ((out_off << 9) | mant) as u16; +} + +// The accurate MAC: y = a1*b1 + a2*b2, all round-to-nearest-even. +fn on_comb(a1: u16, b1: u16, a2: u16, b2: u16) -> u16 { + return gadd(gmul(a1, b1), gmul(a2, b2)); +} + +// 1*1 + 1*1 = 2.0 -> offset 41 = 20992. +test dot_ones { assert_eq(on_comb(20480, 20480, 20480, 20480), 20992); } +endmodule diff --git a/specs/ternary/gft_dot4.t27 b/specs/ternary/gft_dot4.t27 new file mode 100644 index 0000000000..17bf1f18a2 --- /dev/null +++ b/specs/ternary/gft_dot4.t27 @@ -0,0 +1,73 @@ +module GftDot4; +// #1764 + GF-T: a spec-first GF-T16 4-term dot product (MAC), +// y = a1*b1 + a2*b2 + a3*b3 + a4*b4 +// the matmul / attention tile primitive, scaling the silicon-proven 2-term GF-T +// MAC (gft_dot2, AX7203 3/3) to inference-relevant vector lengths. +// +// Because GF-T (float) addition is NOT associative, the accumulation ORDER is +// part of the contract: a balanced reduction tree +// ((a1b1 + a2b2) + (a3b3 + a4b4)) +// so the result is well-defined and bit-exact to the same tree built from the +// silicon-proven gft_dot2 + gft_add. gft_mul / gft_add are the same magnitude +// primitives as gft_dot2.t27 (t27 has no cross-module import yet -- #1773). +// +// GF-T16 packed magnitude: [ offset(7) : mant(9) ], value = (1+mant/512)*2^(offset-40). + +fn gft_mul(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + var prod : i32 = (512 + a_mant) * (512 + b_mant); + var carry : i32 = 0; + if (prod >= 524288) { carry = 1; } + var sum : i32 = a_off + b_off + carry; + var out_off : i32 = 0; + if (sum >= 40) { + var result : i32 = sum - 40; + if (result >= 80) { out_off = 80; } else { out_off = result; } + } + var out_mant : i32 = (prod >> 9) - 512; + if (carry == 1) { out_mant = (prod >> 10) - 512; } + return ((out_off << 9) | out_mant) as u16; +} + +fn gft_add(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + var hi_off : i32 = b_off; + var hi_m : i32 = b_mant; + var lo_off : i32 = a_off; + var lo_m : i32 = a_mant; + if (a_off >= b_off) { + hi_off = a_off; hi_m = a_mant; lo_off = b_off; lo_m = b_mant; + } + var d : i32 = hi_off - lo_off; + var sb : i32 = 0; + if (d < 10) { sb = (512 + lo_m) >> d; } + var sum : i32 = (512 + hi_m) + sb; + var out_off : i32 = hi_off; + var out_mant : i32 = sum - 512; + if (sum >= 1024) { + var e : i32 = hi_off + 1; + if (e >= 80) { out_off = 80; } else { out_off = e; } + out_mant = (sum >> 1) - 512; + } + return ((out_off << 9) | out_mant) as u16; +} + +// 2-term partial sum (one MAC), the same order gft_dot2 uses. +fn dot2(a1: u16, b1: u16, a2: u16, b2: u16) -> u16 { + return gft_add(gft_mul(a1, b1), gft_mul(a2, b2)); +} + +// The 4-term MAC: balanced tree ((a1b1+a2b2) + (a3b3+a4b4)). +fn on_comb(a1: u16, b1: u16, a2: u16, b2: u16, a3: u16, b3: u16, a4: u16, b4: u16) -> u16 { + return gft_add(dot2(a1, b1, a2, b2), dot2(a3, b3, a4, b4)); +} + +// 1.0 = offset 40, mant 0 = 20480. 1*1 four times summed = 4.0 = offset 42 = 21504. +test dot4_ones { assert_eq(on_comb(20480, 20480, 20480, 20480, 20480, 20480, 20480, 20480), 21504); } +endmodule diff --git a/specs/ternary/gft_dot8.t27 b/specs/ternary/gft_dot8.t27 new file mode 100644 index 0000000000..99be5e9f94 --- /dev/null +++ b/specs/ternary/gft_dot8.t27 @@ -0,0 +1,76 @@ +module GftDot8; +// #1764 + GF-T: a spec-first GF-T16 8-term dot product (MAC), +// y = sum_{i=1..8} a_i * b_i +// a realistic inference / attention-head tile length, scaling the silicon-proven +// GF-T MAC (gft_dot2, AX7203 3/3) to an 8-element vector via a balanced reduction +// tree (GF-T float add is NOT associative, so the tree is the contract): +// (((a1b1+a2b2)+(a3b3+a4b4)) + ((a5b5+a6b6)+(a7b7+a8b8))) +// bit-exact to the same tree built from the silicon-proven gft_dot2 + gft_add. +// gft_mul / gft_add are the same magnitude primitives as gft_dot2/gft_dot4 (t27 +// has no cross-module import yet -- #1773). +// +// GF-T16 packed magnitude: [ offset(7) : mant(9) ], value = (1+mant/512)*2^(offset-40). + +fn gft_mul(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + var prod : i32 = (512 + a_mant) * (512 + b_mant); + var carry : i32 = 0; + if (prod >= 524288) { carry = 1; } + var sum : i32 = a_off + b_off + carry; + var out_off : i32 = 0; + if (sum >= 40) { + var result : i32 = sum - 40; + if (result >= 80) { out_off = 80; } else { out_off = result; } + } + var out_mant : i32 = (prod >> 9) - 512; + if (carry == 1) { out_mant = (prod >> 10) - 512; } + return ((out_off << 9) | out_mant) as u16; +} + +fn gft_add(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + var hi_off : i32 = b_off; + var hi_m : i32 = b_mant; + var lo_off : i32 = a_off; + var lo_m : i32 = a_mant; + if (a_off >= b_off) { + hi_off = a_off; hi_m = a_mant; lo_off = b_off; lo_m = b_mant; + } + var d : i32 = hi_off - lo_off; + var sb : i32 = 0; + if (d < 10) { sb = (512 + lo_m) >> d; } + var sum : i32 = (512 + hi_m) + sb; + var out_off : i32 = hi_off; + var out_mant : i32 = sum - 512; + if (sum >= 1024) { + var e : i32 = hi_off + 1; + if (e >= 80) { out_off = 80; } else { out_off = e; } + out_mant = (sum >> 1) - 512; + } + return ((out_off << 9) | out_mant) as u16; +} + +fn dot2(a1: u16, b1: u16, a2: u16, b2: u16) -> u16 { + return gft_add(gft_mul(a1, b1), gft_mul(a2, b2)); +} +fn dot4(a1: u16, b1: u16, a2: u16, b2: u16, a3: u16, b3: u16, a4: u16, b4: u16) -> u16 { + return gft_add(dot2(a1, b1, a2, b2), dot2(a3, b3, a4, b4)); +} + +// The 8-term MAC: balanced tree over two dot4 halves. +fn on_comb(a1: u16, b1: u16, a2: u16, b2: u16, a3: u16, b3: u16, a4: u16, b4: u16, + a5: u16, b5: u16, a6: u16, b6: u16, a7: u16, b7: u16, a8: u16, b8: u16) -> u16 { + return gft_add(dot4(a1, b1, a2, b2, a3, b3, a4, b4), + dot4(a5, b5, a6, b6, a7, b7, a8, b8)); +} + +// 1.0 = offset 40 = 20480. Eight 1*1 terms summed = 8.0 = offset 43 = 22016. +test dot8_ones { assert_eq(on_comb(20480,20480,20480,20480,20480,20480,20480,20480, + 20480,20480,20480,20480,20480,20480,20480,20480), 22016); } +endmodule diff --git a/specs/ternary/gft_layer2.t27 b/specs/ternary/gft_layer2.t27 new file mode 100644 index 0000000000..59554056ed --- /dev/null +++ b/specs/ternary/gft_layer2.t27 @@ -0,0 +1,76 @@ +module GftLayer2; +// #1764 + GF-T: a spec-first GF-T16 matmul ROW = 2 neurons over a shared +// activation. The activation vector a=(a1,a2) feeds two neurons, each with its +// own GF-T16 weight vector (w0, w1); every neuron computes a GF-T dot product +// (the silicon-proven MAC), and the two GF-T16 outputs are packed into one +// 32-bit result: neuron 0 in result[15:0], neuron 1 in result[31:16]. +// +// This is a full GF-T inference layer primitive (a 1x2 activation times a 2x2 +// weight matrix -> 2 outputs), all in real-valued GF-T precision, generated from +// spec and bit-exact to the same composition of the silicon-proven gft_dot2. +// gft_mul / gft_add are the magnitude primitives from gft_dot2.t27 (#1773: no +// cross-module import yet). +// +// GF-T16 packed magnitude: [ offset(7) : mant(9) ], value = (1+mant/512)*2^(offset-40). + +fn gft_mul(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + var prod : i32 = (512 + a_mant) * (512 + b_mant); + var carry : i32 = 0; + if (prod >= 524288) { carry = 1; } + var sum : i32 = a_off + b_off + carry; + var out_off : i32 = 0; + if (sum >= 40) { + var result : i32 = sum - 40; + if (result >= 80) { out_off = 80; } else { out_off = result; } + } + var out_mant : i32 = (prod >> 9) - 512; + if (carry == 1) { out_mant = (prod >> 10) - 512; } + return ((out_off << 9) | out_mant) as u16; +} + +fn gft_add(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + var hi_off : i32 = b_off; + var hi_m : i32 = b_mant; + var lo_off : i32 = a_off; + var lo_m : i32 = a_mant; + if (a_off >= b_off) { + hi_off = a_off; hi_m = a_mant; lo_off = b_off; lo_m = b_mant; + } + var d : i32 = hi_off - lo_off; + var sb : i32 = 0; + if (d < 10) { sb = (512 + lo_m) >> d; } + var sum : i32 = (512 + hi_m) + sb; + var out_off : i32 = hi_off; + var out_mant : i32 = sum - 512; + if (sum >= 1024) { + var e : i32 = hi_off + 1; + if (e >= 80) { out_off = 80; } else { out_off = e; } + out_mant = (sum >> 1) - 512; + } + return ((out_off << 9) | out_mant) as u16; +} + +// One neuron = GF-T dot product of a 2-element weight vector and activation. +fn neuron(w1: u16, x1: u16, w2: u16, x2: u16) -> u16 { + return gft_add(gft_mul(w1, x1), gft_mul(w2, x2)); +} + +// The layer: shared activation (a1, a2); neuron 0 uses (w0a, w0b), neuron 1 uses +// (w1a, w1b). Two GF-T16 activations packed into one 32-bit word. +fn on_comb(a1: u16, a2: u16, w0a: u16, w0b: u16, w1a: u16, w1b: u16) -> u32 { + return (neuron(w0a, a1, w0b, a2) as u32) + | ((neuron(w1a, a1, w1b, a2) as u32) << 16); +} + +// activation = (1.0, 1.0) = (20480, 20480); weights all 1.0 -> each neuron = 2.0 +// = 20992. packed = 20992 | (20992 << 16) = 20992 + 20992*65536 = 1375752704. +test layer_ones { assert_eq(on_comb(20480, 20480, 20480, 20480, 20480, 20480), 1375752704); } +endmodule diff --git a/specs/ternary/gft_mul_rne.t27 b/specs/ternary/gft_mul_rne.t27 new file mode 100644 index 0000000000..27e4c75ba6 --- /dev/null +++ b/specs/ternary/gft_mul_rne.t27 @@ -0,0 +1,55 @@ +module GftMulRne; +// #1764 + GF-T: a spec-first GF-T16 multiply with ROUND-TO-NEAREST-EVEN, +// bit-exact to the ideal oracle (trinity-fpga/conformance/gft16_ref.py). +// +// FINDING that motivates this: the silicon-proven gft_mul (gft_dot2.t27) TRUNCATES +// the mantissa (`prod >> 9`), so it is biased ~1 ULP low versus the ideal RNE +// GF-T (~37% of products differ by -1 ULP, ~12% by a carry). For deep NN +// inference that truncation is a systematic downward bias. This module rounds the +// mantissa to nearest-even instead, matching the oracle exactly -- a spec-first +// GF-T that is MORE ACCURATE than the current truncating silicon RTL. +// +// GF-T16 packed magnitude: [ offset(7) : mant(9) ], value = (1+mant/512)*2^(offset-40). +// i32 internals (all non-negative small ints) so typecheck literal typing is happy. + +fn on_comb(a: u16, b: u16) -> u16 { + var a_off : i32 = (a >> 9) as i32; + var a_mant : i32 = (a & 511) as i32; + var b_off : i32 = (b >> 9) as i32; + var b_mant : i32 = (b & 511) as i32; + // full-precision significand product, scaled by 512^2. + var prod : i32 = (512 + a_mant) * (512 + b_mant); + var carry : i32 = 0; + if (prod >= 524288) { carry = 1; } // 2*512*512 renorm boundary + + // quotient q and remainder r of prod / (512 << carry) -- the un-rounded + // significand fraction. no-carry: /512 (>>9); carry: /1024 (>>10). + var q : i32 = prod >> 9; + var r : i32 = prod & 511; + var half : i32 = 256; + if (carry == 1) { q = prod >> 10; r = prod & 1023; half = 512; } + + // round-to-nearest-even: up if r > half, or (r == half and q is odd). + var mant : i32 = q - 512; + if (r > half) { mant = mant + 1; } + if (r == half) { if ((q & 1) == 1) { mant = mant + 1; } } + + // exponent: add offsets, apply the renorm carry, de-bias, saturate. + var sum : i32 = a_off + b_off + carry; + var out_off : i32 = 0; + if (sum >= 40) { + var result : i32 = sum - 40; + if (result >= 80) { out_off = 80; } else { out_off = result; } + } + // mantissa carry after rounding: mant == 512 -> 0, exponent += 1 (saturate). + if (mant >= 512) { + mant = 0; + out_off = out_off + 1; + if (out_off >= 80) { out_off = 80; } + } + return ((out_off << 9) | mant) as u16; +} + +// 1.0*1.0 = 1.0 -> offset 40, mant 0 = 20480. (RNE and truncation agree here.) +test one { assert_eq(on_comb(20480, 20480), 20480); } +endmodule diff --git a/specs/ternary/stream_ternary_mac.t27 b/specs/ternary/stream_ternary_mac.t27 new file mode 100644 index 0000000000..1bcb7ccd10 --- /dev/null +++ b/specs/ternary/stream_ternary_mac.t27 @@ -0,0 +1,52 @@ +module StreamTernaryMac; +// #1764: a STREAMING ternary MAC -- the on-hardware BitNet inference primitive. +// +// Each clock cycle consumes one packed 27-trit (a, b) pair on input data ports +// and accumulates their dot product into a registered accumulator. This is a +// real datapath generated entirely from spec: +// input ports (a, b) -> ternary sign-multiply adder-tree (dot27) +// -> accumulate register (acc) -> output port (acc) +// It synthesizes to Artix-7 fabric (yosys synth_xilinx: the dot27 adder-tree in +// LUTs + a 32-bit accumulate register in FDCE + CARRY4), and `en` gates the +// accumulation so a caller can stream N vectors then read the running sum. +// +// The dot27 / tmul / tp primitives are the bit-exact-verified ones from +// ternary_mac.t27 (#1743, cross-checked vs an independent reference on 300 +// random vectors). The only new piece is the `on_clock` streaming wrapper. + +// Sign-only ternary multiply of two packed trits {N=0b00, Z=0b01, P=0b10}. +fn tmul(ta: u8, tb: u8) -> i8 { + if (ta == 1) { return 0; } + if (tb == 1) { return 0; } + if (ta == tb) { return 1; } + return -1; +} +// One trit position i of two 54-bit packed vectors (trit i at [2i+1:2i]). +fn tp(a: u64, b: u64, i: u32) -> i8 { + return tmul(((a >> (i << 1)) & 3) as u8, ((b >> (i << 1)) & 3) as u8); +} +// 27-trit ternary dot product, loop-free. Result in [-27, +27]. +fn dot27(a: u64, b: u64) -> i8 { + return tp(a,b,0) + tp(a,b,1) + tp(a,b,2) + tp(a,b,3) + tp(a,b,4) + + tp(a,b,5) + tp(a,b,6) + tp(a,b,7) + tp(a,b,8) + tp(a,b,9) + + tp(a,b,10) + tp(a,b,11) + tp(a,b,12) + tp(a,b,13) + tp(a,b,14) + + tp(a,b,15) + tp(a,b,16) + tp(a,b,17) + tp(a,b,18) + tp(a,b,19) + + tp(a,b,20) + tp(a,b,21) + tp(a,b,22) + tp(a,b,23) + tp(a,b,24) + + tp(a,b,25) + tp(a,b,26); +} + +// Registered accumulator, exposed as an output data port. i32 so it never +// overflows across a realistic stream (each step adds a value in [-27, +27]). +var acc : i32 = 0 + +// The clocked process: `a` and `b` are streaming input data ports; each cycle +// (while `en`) the dot product of the current pair is added to `acc`. +fn on_clock(a: u64, b: u64) { + acc = acc + (dot27(a, b) as i32) +} + +test dot_all_n_x_all_n { assert_eq(dot27(0, 0), 27); } +test dot_all_n_x_all_p { assert_eq(dot27(0, 12009599006321322), -27); } +test dot_all_p_x_all_p { assert_eq(dot27(12009599006321322, 12009599006321322), 27); } +test dot_all_z { assert_eq(dot27(6004799503160661, 6004799503160661), 0); } +endmodule