From 8b335471bda5da2090b0dc2de3fa17d44fd12185 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 20:05:08 +0700 Subject: [PATCH 1/8] fpga(ax7203): ternary mat-vec over real tern-tc-9m weights in DDR3, UART receipt (Closes #10461) Cell 26 of specs/igla/own_model.t27 (epic #10024), the compute step on top of the DDR3 read path of #10248. - specs/fpga/ddr3_ternary_matvec.t27: the board spec. It receives the 20,480 bytes of blocks.0.attn.k.weight (tern-tc-9m, sha256 3102abdf...ce9c, offset 10,589,476) on UART RX P20, packs them into 640 beats of 256 bits, writes them to DDR3, reads them back one beat at a time and steps through their trits one per clock: y_r = sum_c w_rc * x_c, x_c = int8(37c + 11), wrapping 32 bits. Receipt on N15: T27 TERN N= S= C= Y= E= F= L= PASS|FAIL. - specs/fpga/tern9m_l0_k_weights.t27: the same bytes as 2,560 u64 words made with od, and the tests that compute S_EXPECT and Y_EXPECT from them with the board spec's own fold and trit_term; the FF-as-+1 mutant and a one-byte change both miss. - Tests on the Railway lab: 9/9 and 5/5, 0 vacuous. A copy of the board spec with the FF trit read as +1 fails its own test. Co-Authored-By: Claude Opus 5.5 --- .../seals/fpga_FpgaDdr3TernaryMatvec.json | 28 + .trinity/seals/fpga_FpgaTern9mL0KWeights.json | 33 + specs/fpga/ddr3_ternary_matvec.t27 | 1161 +++++++++++++++++ specs/fpga/tern9m_l0_k_weights.t27 | 781 +++++++++++ 4 files changed, 2003 insertions(+) create mode 100644 .trinity/seals/fpga_FpgaDdr3TernaryMatvec.json create mode 100644 .trinity/seals/fpga_FpgaTern9mL0KWeights.json create mode 100644 specs/fpga/ddr3_ternary_matvec.t27 create mode 100644 specs/fpga/tern9m_l0_k_weights.t27 diff --git a/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json b/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json new file mode 100644 index 0000000000..84141a9937 --- /dev/null +++ b/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+a86b691b1", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:a97c2a9d6b4b710cf14aabd9b615d84097b7f0e556e27efb8f87a0ff58f25723", + "gen_hash_rust": "sha256:e4ceee52757003ee74d3cbbcd80038a6385e0bbe19c438857c9033e93512a41b", + "gen_hash_verilog": "sha256:240ad78d4c69b08dc52089c56c8423d9df62e9ed2f70e807985a278f4108345d", + "gen_hash_zig": "sha256:9cc18b3a4e948e1015c2301bc1d93f220865aaedd2ff1140c51612cdbeae5bde", + "module": "FpgaDdr3TernaryMatvec", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-18T13:03:19Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:11fbcc214ab20edaded49ece8dd1714f55f2195f7f1147cb6e49ad7025658eca", + "spec_path": "specs/fpga/ddr3_ternary_matvec.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 9, + "total": 9, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +}warning: Config as Code (railway.json / railway.toml) is deprecated. Prefer Infrastructure as Code (.railway/railway.ts). Run `railway config migrate` or see https://docs.railway.com/infrastructure-as-code#migrating-from-config-as-code diff --git a/.trinity/seals/fpga_FpgaTern9mL0KWeights.json b/.trinity/seals/fpga_FpgaTern9mL0KWeights.json new file mode 100644 index 0000000000..cd25b554f2 --- /dev/null +++ b/.trinity/seals/fpga_FpgaTern9mL0KWeights.json @@ -0,0 +1,33 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+a86b691b1", + "closure": [ + { + "spec": "specs/fpga/ddr3_ternary_matvec.t27", + "spec_hash": "sha256:11fbcc214ab20edaded49ece8dd1714f55f2195f7f1147cb6e49ad7025658eca" + } + ], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:35613d884051da0f0460bb7a715b0dfcd488767db707c78e5f03c556342e8f77", + "gen_hash_rust": "sha256:81255bea491747e968ad3a570ee76bf15c7417e8d8f03587f1319ce2f99d16d6", + "gen_hash_verilog": "sha256:dce0d2d14e0273bb91945f477f1c9fcd66466a570dea68c22ff8822fb972e805", + "gen_hash_zig": "sha256:1bb4a6177c70132b5c5b585008698c4282e3b0cbfb9b6a3697fdc8786b9aaccf", + "module": "FpgaTern9mL0KWeights", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-18T13:03:37Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:31241d2b9351e8d3c35f1b5ecfcfedd11c674afb82836f8137e7658b2f672a8d", + "spec_path": "specs/fpga/tern9m_l0_k_weights.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 5, + "total": 5, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +}warning: Config as Code (railway.json / railway.toml) is deprecated. Prefer Infrastructure as Code (.railway/railway.ts). Run `railway config migrate` or see https://docs.railway.com/infrastructure-as-code#migrating-from-config-as-code diff --git a/specs/fpga/ddr3_ternary_matvec.t27 b/specs/fpga/ddr3_ternary_matvec.t27 new file mode 100644 index 0000000000..ae8179cf1a --- /dev/null +++ b/specs/fpga/ddr3_ternary_matvec.t27 @@ -0,0 +1,1161 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/fpga/ddr3_ternary_matvec.t27 -- a ternary mat-vec on the AX7203 over real weights held in its DDR3 +; Cell 26 of specs/igla/own_model.t27 ("Full model on FPGA, DDR3"), epic gHashTag/t27#10024, issue +; gHashTag/t27#10461. specs/fpga/ddr3_head_bandwidth.t27 measured the read path (#10248); this file is the +; compute step on top of it: weights in DDR3, a product computed from them, a receipt that can be checked. +; - +; THE WEIGHTS. blocks.0.attn.k.weight of tern-tc-9m: 64 rows of 320 trits, one int8 in {-1, 0, +1} each, +; 20,480 bytes at offset 10,589,476 of c_infer/model.bin (Hugging Face playra/tern-tc-9m, 16,953,800 bytes, +; sha256 3102abdf35057924e077a86db4fdac726e4fe1f6574df47f39a638ba99a3ce9c). Its head (wte) is tied and f32, +; not ternary, so the first ternary projection of the same checkpoint is the tensor used. The bytes, as +; 2,560 little-endian u64 words, and the tests that compute S_EXPECT and Y_EXPECT from them, are +; specs/fpga/tern9m_l0_k_weights.t27. The per-tensor scale (0.07064503) is not applied: y is the integer +; product, as a ternary layer computes it before its one multiply. +; - +; THE RUN. Wait for the core's init_done. Receive the 20,480 bytes on the UART (115200 baud, 8N1, P20), pack +; them low byte first into 640 beats of 32 bytes (row r is beats 10r .. 10r+9) and write beat i to address i +; of the native port. The write checksum S folds each beat as it is packed. Then read the 640 beats back +; from DDR3, one at a time: fold each into the read checksum C, and step through its 32 trits one per clock, +; y_r = sum over c of w_rc * x_c in wrapping 32-bit arithmetic, where x_c is the int8 (37 c + 11) mod 256 +; read as two's complement (XV0, XSTEP). At the end of each row y_r is folded into Y. A byte that is not +; 00, 01 or FF counts in E (and adds 0); a UART frame whose stop bit is low counts in F. +; PASS is: 640 beats, S = S_EXPECT, C = S, Y = Y_EXPECT, E = 0 and F = 0. Anything else is FAIL. +; - +; THE RECEIPT. 115200 baud on N15, one line, sent again and again once the run is over: +; T27 TERN N=<16 hex> S=<16 hex> C=<16 hex> Y=<16 hex> E=<16 hex> F=<16 hex> L=<16 hex> PASS +; N beats computed, S write checksum, C read checksum, Y output checksum, E bad trits, F bad frames, L the +; line's number. Until the run is over the UART is the core's BIOS, which prints its calibration; the +; core's own RX is tied idle, so the upload reaches only this design. +; LEDs (active low): B13 init_done, C13 init_error, D14 PASS, D15 a heartbeat of the 100 MHz clock. +; The button T6 (active low) resets the core and so starts the run again. +; - +; THE HOST. Plain commands only: `stty -f 115200 cs8 -cstopb -parenb raw`, then `dd if=model.bin +; bs=20480 skip=10589476 count=1 iflag=skip_bytes` (or `bs=1 skip=10589476 count=20480`) into the port, and +; `cat` of the port for the receipt. +; - +; WHAT A PASS SAYS. These 20,480 bytes of a published checkpoint went into this board's DDR3, came back out +; unchanged, and the board's own ternary datapath computed from them the same 64 outputs the spec's test +; computes, checksum for checksum. WHAT IT DOES NOT SAY. Nothing about the full model: one projection of one +; layer, an input vector that is a fixed pattern and not an activation, no scale, no attention, no rate. +; ASCII only, English only. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module FpgaDdr3TernaryMatvec; + +pub const KIND : str = "board-cell"; +pub const ID : str = "fpga/ddr3_ternary_matvec"; +pub const EPIC : str = "gHashTag/t27#10024"; +pub const BOARD : str = "ALINX AX7203"; +pub const PART : str = "xc7a200tfbg484-2"; + +; --- the run ------------------------------------------------------------------------------------ +pub const W_FILE_SHA256 : str = "3102abdf35057924e077a86db4fdac726e4fe1f6574df47f39a638ba99a3ce9c"; +pub const W_TENSOR : str = "blocks.0.attn.k.weight"; +pub const W_OFFSET : u64 = 10589476; +pub const W_BYTES : u64 = 20480; +pub const W_ROWS : u32 = 64; +pub const W_COLS : u32 = 320; +pub const BEAT_BYTES : u64 = 32; +pub const W_BEATS : u32 = 640; +pub const BEATS_PER_ROW : u32 = 10; +/// x_c = (XSTEP * c + XV0) mod 256, read as an int8. +pub const XV0 : u8 = 11; +pub const XSTEP : u8 = 37; +/// What the board must report. Both were read off the failing assert_eq of specs/fpga/tern9m_l0_k_weights.t27 +/// run with 0 here (t27c test-report on the Railway lab, 2026-10-18), and that spec's tests now hold them: S is +/// s_of over the pinned bytes, Y is y_of over them. The receipt prints them as S=4B58160720ABB863 and +/// Y=9A50D884522C233D. +pub const S_EXPECT : u64 = 0x4B58160720ABB863; +pub const Y_EXPECT : u64 = 0x9A50D884522C233D; + +pub const V_PASS : u8 = 0; +pub const V_FAIL : u8 = 3; + +pub const ST_WAIT : u8 = 0; +pub const ST_LOAD : u8 = 1; +pub const ST_READ : u8 = 2; +pub const ST_JUDGE : u8 = 3; +pub const ST_REPORT : u8 = 4; + +pub const BAUD_DIV : u16 = 868; +pub const LINE_SEGS : u8 = 9; + +; --- the arithmetic ----------------------------------------------------------------------------- + +/// The checksum after one more beat (the fold of specs/fpga/ddr3_head_bandwidth.t27): rotate the sum left by +/// one, then xor in the four lanes, lane k rotated left by 16 * k. +pub fn fold(sum: u64, l0: u64, l1: u64, l2: u64, l3: u64) -> u64 { + return ((sum << 1) | (sum >> 63)) ^ l0 ^ ((l1 << 16) | (l1 >> 48)) ^ ((l2 << 32) | (l2 >> 32)) ^ ((l3 << 48) | (l3 >> 16)); +} + +/// An int8, held as its u8 bits, sign-extended to 32 bits. +pub fn sext8(v: u8) -> u32 { + if (v >= 128) { return (v as u32) | 0xFFFFFF00; } + return v as u32; +} + +/// What a weight byte adds to a row sum, for the input x held as the u8 bits xv: +x for 01, -x for FF, 0 for +/// 00 and for any byte that is not a trit. +pub fn trit_term(b: u8, xv: u8) -> u32 { + if (b == 1) { return sext8(xv); } + if (b == 255) { return (0xFFFFFFFF - sext8(xv)) +% 1; } + return 0; +} + +/// Is the byte one of the three trits 00, 01, FF. +pub fn is_trit(b: u8) -> bool { + return b == 0 or b == 1 or b == 255; +} + +/// The verdict of the run. +pub fn verdict_of(n: u32, s: u64, c: u64, y: u64, e: u32, f: u32, s_want: u64, y_want: u64, n_want: u32) -> u8 { + if (n == n_want and s == s_want and c == s and y == y_want and e == 0 and f == 0) { return V_PASS; } + return V_FAIL; +} + +/// How many clocks the receiver waits before its next sample: half a bit before the start bit's middle, +/// a whole bit before every later one. +pub fn rx_wait(bit: u8, div: u16) -> u16 { + if (bit == 0) { return div >> 1; } + return div; +} + +/// The level of bit k (0 start, 1..8 data low bit first, 9 stop) of the UART frame of `b`. +pub fn frame_bit(b: u8, k: u32) -> bool { + if (k == 0) { return false; } + if (k >= 9) { return true; } + var v : u8 = b; + var j : u32 = 1; + while (j < k) { + v = v >> 1; + j = j + 1; + } + return (v & 1) == 1; +} + +; --- the receipt -------------------------------------------------------------------------------- + +/// The ASCII digit of a nibble, 0-9 A-F. +pub fn hex_digit(n: u8) -> u8 { + if ((n & 15) < 10) { return 48 + (n & 15); } + return 55 + (n & 15); +} + +/// The key letter of field s (1..7): N S C Y E F L. +pub fn key_of(s: u8) -> u8 { + if (s == 1) { return 78; } + if (s == 2) { return 83; } + if (s == 3) { return 67; } + if (s == 4) { return 89; } + if (s == 5) { return 69; } + if (s == 6) { return 70; } + return 76; +} + +/// Character p of "T27 TERN". +pub fn prefix_char(p: u8) -> u8 { + if (p == 0) { return 84; } + if (p == 1) { return 50; } + if (p == 2) { return 55; } + if (p == 3) { return 32; } + if (p == 4) { return 84; } + if (p == 5) { return 69; } + if (p == 6) { return 82; } + return 78; +} + +/// Character p of " PASS\r\n" or " FAIL\r\n". +pub fn verdict_char(v: u8, p: u8) -> u8 { + if (p == 0) { return 32; } + if (p == 5) { return 13; } + if (p == 6) { return 10; } + if (v == V_PASS) { + if (p == 1) { return 80; } + if (p == 2) { return 65; } + return 83; + } + if (p == 1) { return 70; } + if (p == 2) { return 65; } + if (p == 3) { return 73; } + return 76; +} + +/// The character at segment s, position p; `fsr` holds the field being written, its next nibble on top. +pub fn line_char(s: u8, p: u8, fsr: u64, v: u8) -> u8 { + if (s == 0) { return prefix_char(p); } + if (s == LINE_SEGS - 1) { return verdict_char(v, p); } + if (p == 0) { return 32; } + if (p == 1) { return key_of(s); } + if (p == 2) { return 61; } + return hex_digit((fsr >> 60) as u8); +} + +/// The last position of segment s. +pub fn seg_last(s: u8) -> u8 { + if (s == 0) { return 7; } + if (s == LINE_SEGS - 1) { return 6; } + return 18; +} + +/// A UART frame, sent low bit first: a start bit 0, the 8 data bits, a stop bit 1. +pub fn frame(ch: u8) -> u16 { + return ((ch as u16) << 1) | 512; +} + +/// A byte of the test stream: trits in an uneven order, and a 02 where `bad` says so. +pub fn test_byte(k: u32, bad: u32) -> u8 { + if (k == bad) { return 2; } + const m : u32 = (k * 7 + k / 5) % 3; + if (m == 0) { return 0; } + if (m == 1) { return 1; } + return 255; +} + +; --- the board ---------------------------------------------------------------------------------- + +/// A differential input buffer (the 200 MHz oscillator on R4/T4). +pub struct IbufdsOut { O: bool } +pub fn IBUFDS(I: bool, IB: bool) -> IbufdsOut {} + +/// The outputs of the LiteDRAM core, as named in its generated Verilog. +pub struct LitedramOut { ddram_a__0: bool, ddram_a__1: bool, ddram_a__2: bool, ddram_a__3: bool, ddram_a__4: bool, ddram_a__5: bool, ddram_a__6: bool, ddram_a__7: bool, ddram_a__8: bool, ddram_a__9: bool, ddram_a__10: bool, ddram_a__11: bool, ddram_a__12: bool, ddram_a__13: bool, ddram_a__14: bool, ddram_ba__0: bool, ddram_ba__1: bool, ddram_ba__2: bool, ddram_dm__0: bool, ddram_dm__1: bool, ddram_dm__2: bool, ddram_dm__3: bool, ddram_cas_n: bool, ddram_cke: bool, ddram_clk_n: bool, ddram_clk_p: bool, ddram_cs_n: bool, ddram_odt: bool, ddram_ras_n: bool, ddram_reset_n: bool, ddram_we_n: bool, init_done: bool, init_error: bool, pll_locked: bool, uart_tx: bool, user_clk: bool, user_port_native_0_cmd_ready: bool, user_port_native_0_rdata_data__0: u64, user_port_native_0_rdata_data__1: u64, user_port_native_0_rdata_data__2: u64, user_port_native_0_rdata_data__3: u64, user_port_native_0_rdata_valid: bool, user_port_native_0_wdata_ready: bool, user_rst: bool } + +/// The LiteDRAM core: a DDR3 controller with its PHY and PLL, a 256-bit native user port, and a BIOS on the UART +/// that calibrates the PHY before it raises init_done. +pub fn litedram_core(clk_: bool, rst: bool, uart_rx_: bool, user_port_native_0_cmd_addr: u25, user_port_native_0_cmd_valid: bool, user_port_native_0_cmd_we: bool, user_port_native_0_rdata_ready: bool, user_port_native_0_wdata_data__0: u64, user_port_native_0_wdata_data__1: u64, user_port_native_0_wdata_data__2: u64, user_port_native_0_wdata_data__3: u64, user_port_native_0_wdata_valid: bool, user_port_native_0_wdata_we: u32, ddram_dq__0: bool, ddram_dq__1: bool, ddram_dq__2: bool, ddram_dq__3: bool, ddram_dq__4: bool, ddram_dq__5: bool, ddram_dq__6: bool, ddram_dq__7: bool, ddram_dq__8: bool, ddram_dq__9: bool, ddram_dq__10: bool, ddram_dq__11: bool, ddram_dq__12: bool, ddram_dq__13: bool, ddram_dq__14: bool, ddram_dq__15: bool, ddram_dq__16: bool, ddram_dq__17: bool, ddram_dq__18: bool, ddram_dq__19: bool, ddram_dq__20: bool, ddram_dq__21: bool, ddram_dq__22: bool, ddram_dq__23: bool, ddram_dq__24: bool, ddram_dq__25: bool, ddram_dq__26: bool, ddram_dq__27: bool, ddram_dq__28: bool, ddram_dq__29: bool, ddram_dq__30: bool, ddram_dq__31: bool, ddram_dqs_n__0: bool, ddram_dqs_n__1: bool, ddram_dqs_n__2: bool, ddram_dqs_n__3: bool, ddram_dqs_p__0: bool, ddram_dqs_p__1: bool, ddram_dqs_p__2: bool, ddram_dqs_p__3: bool) -> LitedramOut {} + +; --- the pins in -------------------------------------------------------------------------------- +; uart_rx is the on_clock parameter of that name, so it is a port of this module read at the clock; the +; core's own RX is tied idle (true) and never sees the upload. +const clk200_p : bool = undefined; +const clk200_p_LOC : str = "R4"; +const clk200_p_IOSTANDARD : str = "DIFF_SSTL15"; +const clk200_n : bool = undefined; +const clk200_n_LOC : str = "T4"; +const clk200_n_IOSTANDARD : str = "DIFF_SSTL15"; +const cpu_reset_n : bool = undefined; +const cpu_reset_n_LOC : str = "T6"; +const cpu_reset_n_IOSTANDARD : str = "LVCMOS15"; +const uart_rx_LOC : str = "P20"; +const uart_rx_IOSTANDARD : str = "LVCMOS33"; + +; --- the clock, the core and its reset ---------------------------------------------------------- +const clkbuf : IbufdsOut = IBUFDS(clk200_p, clk200_n); +const clkbuf_O_PERIOD_PS : u32 = 5000; + +const core : LitedramOut = litedram_core(clkbuf.O, !cpu_reset_n, true, ca as u25, cv, cwe, true, wb0, wb1, wb2, wb3, wv, 0xFFFFFFFF, ddram_dq_0, ddram_dq_1, ddram_dq_2, ddram_dq_3, ddram_dq_4, ddram_dq_5, ddram_dq_6, ddram_dq_7, ddram_dq_8, ddram_dq_9, ddram_dq_10, ddram_dq_11, ddram_dq_12, ddram_dq_13, ddram_dq_14, ddram_dq_15, ddram_dq_16, ddram_dq_17, ddram_dq_18, ddram_dq_19, ddram_dq_20, ddram_dq_21, ddram_dq_22, ddram_dq_23, ddram_dq_24, ddram_dq_25, ddram_dq_26, ddram_dq_27, ddram_dq_28, ddram_dq_29, ddram_dq_30, ddram_dq_31, ddram_dqs_n_0, ddram_dqs_n_1, ddram_dqs_n_2, ddram_dqs_n_3, ddram_dqs_p_0, ddram_dqs_p_1, ddram_dqs_p_2, ddram_dqs_p_3); +const core_user_clk_PERIOD_PS : u32 = 10000; + +const clk : bool = core.user_clk; +const rst_n : bool = !core.user_rst; +const en : bool = true; + +; --- the pins out ------------------------------------------------------------------------------- +pub var uart_tx : bool = true; +const uart_tx_LOC : str = "N15"; +const uart_tx_IOSTANDARD : str = "LVCMOS33"; +pub const led_0 : bool = !core.init_done; +const led_0_LOC : str = "B13"; +const led_0_IOSTANDARD : str = "LVCMOS33"; +pub const led_1 : bool = !core.init_error; +const led_1_LOC : str = "C13"; +const led_1_IOSTANDARD : str = "LVCMOS33"; +pub var led_2 : bool = true; +const led_2_LOC : str = "D14"; +const led_2_IOSTANDARD : str = "LVCMOS33"; +pub var led_3 : bool = false; +const led_3_LOC : str = "D15"; +const led_3_IOSTANDARD : str = "LVCMOS33"; + +; --- the DDR3 pins: outputs of the core, then the bidirectional data and strobes ------------------ +pub const ddram_a_0 : bool = core.ddram_a__0; +const ddram_a_0_LOC : str = "AA4"; +const ddram_a_0_IOSTANDARD : str = "SSTL15"; +const ddram_a_0_SLEW : str = "FAST"; +pub const ddram_a_1 : bool = core.ddram_a__1; +const ddram_a_1_LOC : str = "AB2"; +const ddram_a_1_IOSTANDARD : str = "SSTL15"; +const ddram_a_1_SLEW : str = "FAST"; +pub const ddram_a_2 : bool = core.ddram_a__2; +const ddram_a_2_LOC : str = "AA5"; +const ddram_a_2_IOSTANDARD : str = "SSTL15"; +const ddram_a_2_SLEW : str = "FAST"; +pub const ddram_a_3 : bool = core.ddram_a__3; +const ddram_a_3_LOC : str = "AB5"; +const ddram_a_3_IOSTANDARD : str = "SSTL15"; +const ddram_a_3_SLEW : str = "FAST"; +pub const ddram_a_4 : bool = core.ddram_a__4; +const ddram_a_4_LOC : str = "AB1"; +const ddram_a_4_IOSTANDARD : str = "SSTL15"; +const ddram_a_4_SLEW : str = "FAST"; +pub const ddram_a_5 : bool = core.ddram_a__5; +const ddram_a_5_LOC : str = "U3"; +const ddram_a_5_IOSTANDARD : str = "SSTL15"; +const ddram_a_5_SLEW : str = "FAST"; +pub const ddram_a_6 : bool = core.ddram_a__6; +const ddram_a_6_LOC : str = "W1"; +const ddram_a_6_IOSTANDARD : str = "SSTL15"; +const ddram_a_6_SLEW : str = "FAST"; +pub const ddram_a_7 : bool = core.ddram_a__7; +const ddram_a_7_LOC : str = "T1"; +const ddram_a_7_IOSTANDARD : str = "SSTL15"; +const ddram_a_7_SLEW : str = "FAST"; +pub const ddram_a_8 : bool = core.ddram_a__8; +const ddram_a_8_LOC : str = "V2"; +const ddram_a_8_IOSTANDARD : str = "SSTL15"; +const ddram_a_8_SLEW : str = "FAST"; +pub const ddram_a_9 : bool = core.ddram_a__9; +const ddram_a_9_LOC : str = "U2"; +const ddram_a_9_IOSTANDARD : str = "SSTL15"; +const ddram_a_9_SLEW : str = "FAST"; +pub const ddram_a_10 : bool = core.ddram_a__10; +const ddram_a_10_LOC : str = "Y1"; +const ddram_a_10_IOSTANDARD : str = "SSTL15"; +const ddram_a_10_SLEW : str = "FAST"; +pub const ddram_a_11 : bool = core.ddram_a__11; +const ddram_a_11_LOC : str = "W2"; +const ddram_a_11_IOSTANDARD : str = "SSTL15"; +const ddram_a_11_SLEW : str = "FAST"; +pub const ddram_a_12 : bool = core.ddram_a__12; +const ddram_a_12_LOC : str = "Y2"; +const ddram_a_12_IOSTANDARD : str = "SSTL15"; +const ddram_a_12_SLEW : str = "FAST"; +pub const ddram_a_13 : bool = core.ddram_a__13; +const ddram_a_13_LOC : str = "U1"; +const ddram_a_13_IOSTANDARD : str = "SSTL15"; +const ddram_a_13_SLEW : str = "FAST"; +pub const ddram_a_14 : bool = core.ddram_a__14; +const ddram_a_14_LOC : str = "V3"; +const ddram_a_14_IOSTANDARD : str = "SSTL15"; +const ddram_a_14_SLEW : str = "FAST"; +pub const ddram_ba_0 : bool = core.ddram_ba__0; +const ddram_ba_0_LOC : str = "AA3"; +const ddram_ba_0_IOSTANDARD : str = "SSTL15"; +const ddram_ba_0_SLEW : str = "FAST"; +pub const ddram_ba_1 : bool = core.ddram_ba__1; +const ddram_ba_1_LOC : str = "Y3"; +const ddram_ba_1_IOSTANDARD : str = "SSTL15"; +const ddram_ba_1_SLEW : str = "FAST"; +pub const ddram_ba_2 : bool = core.ddram_ba__2; +const ddram_ba_2_LOC : str = "Y4"; +const ddram_ba_2_IOSTANDARD : str = "SSTL15"; +const ddram_ba_2_SLEW : str = "FAST"; +pub const ddram_ras_n : bool = core.ddram_ras_n; +const ddram_ras_n_LOC : str = "V4"; +const ddram_ras_n_IOSTANDARD : str = "SSTL15"; +const ddram_ras_n_SLEW : str = "FAST"; +pub const ddram_cas_n : bool = core.ddram_cas_n; +const ddram_cas_n_LOC : str = "W4"; +const ddram_cas_n_IOSTANDARD : str = "SSTL15"; +const ddram_cas_n_SLEW : str = "FAST"; +pub const ddram_we_n : bool = core.ddram_we_n; +const ddram_we_n_LOC : str = "AA1"; +const ddram_we_n_IOSTANDARD : str = "SSTL15"; +const ddram_we_n_SLEW : str = "FAST"; +pub const ddram_cs_n : bool = core.ddram_cs_n; +const ddram_cs_n_LOC : str = "AB3"; +const ddram_cs_n_IOSTANDARD : str = "SSTL15"; +const ddram_cs_n_SLEW : str = "FAST"; +pub const ddram_cke : bool = core.ddram_cke; +const ddram_cke_LOC : str = "T5"; +const ddram_cke_IOSTANDARD : str = "SSTL15"; +const ddram_cke_SLEW : str = "FAST"; +pub const ddram_odt : bool = core.ddram_odt; +const ddram_odt_LOC : str = "U5"; +const ddram_odt_IOSTANDARD : str = "SSTL15"; +const ddram_odt_SLEW : str = "FAST"; +pub const ddram_reset_n : bool = core.ddram_reset_n; +const ddram_reset_n_LOC : str = "W6"; +const ddram_reset_n_IOSTANDARD : str = "LVCMOS15"; +const ddram_reset_n_SLEW : str = "FAST"; +pub const ddram_clk_p : bool = core.ddram_clk_p; +const ddram_clk_p_LOC : str = "R3"; +const ddram_clk_p_IOSTANDARD : str = "DIFF_SSTL15"; +const ddram_clk_p_SLEW : str = "FAST"; +pub const ddram_clk_n : bool = core.ddram_clk_n; +const ddram_clk_n_LOC : str = "R2"; +const ddram_clk_n_IOSTANDARD : str = "DIFF_SSTL15"; +const ddram_clk_n_SLEW : str = "FAST"; +pub const ddram_dm_0 : bool = core.ddram_dm__0; +const ddram_dm_0_LOC : str = "D2"; +const ddram_dm_0_IOSTANDARD : str = "SSTL15"; +const ddram_dm_0_SLEW : str = "FAST"; +pub const ddram_dm_1 : bool = core.ddram_dm__1; +const ddram_dm_1_LOC : str = "G2"; +const ddram_dm_1_IOSTANDARD : str = "SSTL15"; +const ddram_dm_1_SLEW : str = "FAST"; +pub const ddram_dm_2 : bool = core.ddram_dm__2; +const ddram_dm_2_LOC : str = "M2"; +const ddram_dm_2_IOSTANDARD : str = "SSTL15"; +const ddram_dm_2_SLEW : str = "FAST"; +pub const ddram_dm_3 : bool = core.ddram_dm__3; +const ddram_dm_3_LOC : str = "M5"; +const ddram_dm_3_IOSTANDARD : str = "SSTL15"; +const ddram_dm_3_SLEW : str = "FAST"; + +pub const ddram_dq_0 : bool = undefined; +const ddram_dq_0_LOC : str = "C2"; +const ddram_dq_0_IOSTANDARD : str = "SSTL15"; +const ddram_dq_0_SLEW : str = "FAST"; +const ddram_dq_0_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_1 : bool = undefined; +const ddram_dq_1_LOC : str = "G1"; +const ddram_dq_1_IOSTANDARD : str = "SSTL15"; +const ddram_dq_1_SLEW : str = "FAST"; +const ddram_dq_1_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_2 : bool = undefined; +const ddram_dq_2_LOC : str = "A1"; +const ddram_dq_2_IOSTANDARD : str = "SSTL15"; +const ddram_dq_2_SLEW : str = "FAST"; +const ddram_dq_2_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_3 : bool = undefined; +const ddram_dq_3_LOC : str = "F3"; +const ddram_dq_3_IOSTANDARD : str = "SSTL15"; +const ddram_dq_3_SLEW : str = "FAST"; +const ddram_dq_3_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_4 : bool = undefined; +const ddram_dq_4_LOC : str = "B2"; +const ddram_dq_4_IOSTANDARD : str = "SSTL15"; +const ddram_dq_4_SLEW : str = "FAST"; +const ddram_dq_4_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_5 : bool = undefined; +const ddram_dq_5_LOC : str = "F1"; +const ddram_dq_5_IOSTANDARD : str = "SSTL15"; +const ddram_dq_5_SLEW : str = "FAST"; +const ddram_dq_5_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_6 : bool = undefined; +const ddram_dq_6_LOC : str = "B1"; +const ddram_dq_6_IOSTANDARD : str = "SSTL15"; +const ddram_dq_6_SLEW : str = "FAST"; +const ddram_dq_6_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_7 : bool = undefined; +const ddram_dq_7_LOC : str = "E2"; +const ddram_dq_7_IOSTANDARD : str = "SSTL15"; +const ddram_dq_7_SLEW : str = "FAST"; +const ddram_dq_7_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_8 : bool = undefined; +const ddram_dq_8_LOC : str = "H3"; +const ddram_dq_8_IOSTANDARD : str = "SSTL15"; +const ddram_dq_8_SLEW : str = "FAST"; +const ddram_dq_8_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_9 : bool = undefined; +const ddram_dq_9_LOC : str = "G3"; +const ddram_dq_9_IOSTANDARD : str = "SSTL15"; +const ddram_dq_9_SLEW : str = "FAST"; +const ddram_dq_9_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_10 : bool = undefined; +const ddram_dq_10_LOC : str = "H2"; +const ddram_dq_10_IOSTANDARD : str = "SSTL15"; +const ddram_dq_10_SLEW : str = "FAST"; +const ddram_dq_10_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_11 : bool = undefined; +const ddram_dq_11_LOC : str = "H5"; +const ddram_dq_11_IOSTANDARD : str = "SSTL15"; +const ddram_dq_11_SLEW : str = "FAST"; +const ddram_dq_11_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_12 : bool = undefined; +const ddram_dq_12_LOC : str = "J1"; +const ddram_dq_12_IOSTANDARD : str = "SSTL15"; +const ddram_dq_12_SLEW : str = "FAST"; +const ddram_dq_12_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_13 : bool = undefined; +const ddram_dq_13_LOC : str = "J5"; +const ddram_dq_13_IOSTANDARD : str = "SSTL15"; +const ddram_dq_13_SLEW : str = "FAST"; +const ddram_dq_13_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_14 : bool = undefined; +const ddram_dq_14_LOC : str = "K1"; +const ddram_dq_14_IOSTANDARD : str = "SSTL15"; +const ddram_dq_14_SLEW : str = "FAST"; +const ddram_dq_14_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_15 : bool = undefined; +const ddram_dq_15_LOC : str = "H4"; +const ddram_dq_15_IOSTANDARD : str = "SSTL15"; +const ddram_dq_15_SLEW : str = "FAST"; +const ddram_dq_15_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_16 : bool = undefined; +const ddram_dq_16_LOC : str = "L4"; +const ddram_dq_16_IOSTANDARD : str = "SSTL15"; +const ddram_dq_16_SLEW : str = "FAST"; +const ddram_dq_16_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_17 : bool = undefined; +const ddram_dq_17_LOC : str = "M3"; +const ddram_dq_17_IOSTANDARD : str = "SSTL15"; +const ddram_dq_17_SLEW : str = "FAST"; +const ddram_dq_17_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_18 : bool = undefined; +const ddram_dq_18_LOC : str = "L3"; +const ddram_dq_18_IOSTANDARD : str = "SSTL15"; +const ddram_dq_18_SLEW : str = "FAST"; +const ddram_dq_18_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_19 : bool = undefined; +const ddram_dq_19_LOC : str = "J6"; +const ddram_dq_19_IOSTANDARD : str = "SSTL15"; +const ddram_dq_19_SLEW : str = "FAST"; +const ddram_dq_19_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_20 : bool = undefined; +const ddram_dq_20_LOC : str = "K3"; +const ddram_dq_20_IOSTANDARD : str = "SSTL15"; +const ddram_dq_20_SLEW : str = "FAST"; +const ddram_dq_20_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_21 : bool = undefined; +const ddram_dq_21_LOC : str = "K6"; +const ddram_dq_21_IOSTANDARD : str = "SSTL15"; +const ddram_dq_21_SLEW : str = "FAST"; +const ddram_dq_21_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_22 : bool = undefined; +const ddram_dq_22_LOC : str = "J4"; +const ddram_dq_22_IOSTANDARD : str = "SSTL15"; +const ddram_dq_22_SLEW : str = "FAST"; +const ddram_dq_22_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_23 : bool = undefined; +const ddram_dq_23_LOC : str = "L5"; +const ddram_dq_23_IOSTANDARD : str = "SSTL15"; +const ddram_dq_23_SLEW : str = "FAST"; +const ddram_dq_23_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_24 : bool = undefined; +const ddram_dq_24_LOC : str = "P1"; +const ddram_dq_24_IOSTANDARD : str = "SSTL15"; +const ddram_dq_24_SLEW : str = "FAST"; +const ddram_dq_24_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_25 : bool = undefined; +const ddram_dq_25_LOC : str = "N4"; +const ddram_dq_25_IOSTANDARD : str = "SSTL15"; +const ddram_dq_25_SLEW : str = "FAST"; +const ddram_dq_25_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_26 : bool = undefined; +const ddram_dq_26_LOC : str = "R1"; +const ddram_dq_26_IOSTANDARD : str = "SSTL15"; +const ddram_dq_26_SLEW : str = "FAST"; +const ddram_dq_26_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_27 : bool = undefined; +const ddram_dq_27_LOC : str = "N2"; +const ddram_dq_27_IOSTANDARD : str = "SSTL15"; +const ddram_dq_27_SLEW : str = "FAST"; +const ddram_dq_27_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_28 : bool = undefined; +const ddram_dq_28_LOC : str = "M6"; +const ddram_dq_28_IOSTANDARD : str = "SSTL15"; +const ddram_dq_28_SLEW : str = "FAST"; +const ddram_dq_28_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_29 : bool = undefined; +const ddram_dq_29_LOC : str = "N5"; +const ddram_dq_29_IOSTANDARD : str = "SSTL15"; +const ddram_dq_29_SLEW : str = "FAST"; +const ddram_dq_29_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_30 : bool = undefined; +const ddram_dq_30_LOC : str = "P6"; +const ddram_dq_30_IOSTANDARD : str = "SSTL15"; +const ddram_dq_30_SLEW : str = "FAST"; +const ddram_dq_30_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dq_31 : bool = undefined; +const ddram_dq_31_LOC : str = "P2"; +const ddram_dq_31_IOSTANDARD : str = "SSTL15"; +const ddram_dq_31_SLEW : str = "FAST"; +const ddram_dq_31_IN_TERM : str = "UNTUNED_SPLIT_50"; +pub const ddram_dqs_p_0 : bool = undefined; +const ddram_dqs_p_0_LOC : str = "E1"; +const ddram_dqs_p_0_IOSTANDARD : str = "DIFF_SSTL15"; +const ddram_dqs_p_0_SLEW : str = "FAST"; +pub const ddram_dqs_p_1 : bool = undefined; +const ddram_dqs_p_1_LOC : str = "K2"; +const ddram_dqs_p_1_IOSTANDARD : str = "DIFF_SSTL15"; +const ddram_dqs_p_1_SLEW : str = "FAST"; +pub const ddram_dqs_p_2 : bool = undefined; +const ddram_dqs_p_2_LOC : str = "M1"; +const ddram_dqs_p_2_IOSTANDARD : str = "DIFF_SSTL15"; +const ddram_dqs_p_2_SLEW : str = "FAST"; +pub const ddram_dqs_p_3 : bool = undefined; +const ddram_dqs_p_3_LOC : str = "P5"; +const ddram_dqs_p_3_IOSTANDARD : str = "DIFF_SSTL15"; +const ddram_dqs_p_3_SLEW : str = "FAST"; +pub const ddram_dqs_n_0 : bool = undefined; +const ddram_dqs_n_0_LOC : str = "D1"; +const ddram_dqs_n_0_IOSTANDARD : str = "DIFF_SSTL15"; +const ddram_dqs_n_0_SLEW : str = "FAST"; +pub const ddram_dqs_n_1 : bool = undefined; +const ddram_dqs_n_1_LOC : str = "J2"; +const ddram_dqs_n_1_IOSTANDARD : str = "DIFF_SSTL15"; +const ddram_dqs_n_1_SLEW : str = "FAST"; +pub const ddram_dqs_n_2 : bool = undefined; +const ddram_dqs_n_2_LOC : str = "L1"; +const ddram_dqs_n_2_IOSTANDARD : str = "DIFF_SSTL15"; +const ddram_dqs_n_2_SLEW : str = "FAST"; +pub const ddram_dqs_n_3 : bool = undefined; +const ddram_dqs_n_3_LOC : str = "P4"; +const ddram_dqs_n_3_IOSTANDARD : str = "DIFF_SSTL15"; +const ddram_dqs_n_3_SLEW : str = "FAST"; + + +; --- the registers ------------------------------------------------------------------------------ +var st : u8 = 0; +var n_beats : u32 = 640; +var s_want : u64 = 0; +var y_want : u64 = 0; +; the native port: address, command, write data +var ca : u32 = 0; +var cv : bool = false; +var cwe : bool = false; +var wv : bool = false; +var wb0 : u64 = 0; +var wb1 : u64 = 0; +var wb2 : u64 = 0; +var wb3 : u64 = 0; +; the load: write phase, beats written, bytes in the beat being packed, a packed beat waiting +var wph : u8 = 0; +var wi : u32 = 0; +var nb : u8 = 0; +var bfull : bool = false; +var wsum : u64 = 0; +; the read and the product: read phase, beats done, the beat being stepped through, its trit, the column +var rph : u8 = 0; +var ri : u32 = 0; +var rb0 : u64 = 0; +var rb1 : u64 = 0; +var rb2 : u64 = 0; +var rb3 : u64 = 0; +var tk : u8 = 0; +var col : u32 = 0; +var xv : u8 = 11; +var acc : u32 = 0; +var ysum : u64 = 0; +var csum : u64 = 0; +var bad : u32 = 0; +var ferr : u32 = 0; +var verdict : u8 = 3; +; the receiver: two flops of synchronizer, then a frame counter +var rx_s1 : bool = true; +var rx_s2 : bool = true; +var rx_busy : bool = false; +var rx_cnt : u16 = 0; +var rx_bit : u8 = 0; +var rx_sh : u8 = 0; +var rx_got : bool = false; +var rx_byte : u8 = 0; +var rx_div : u16 = 868; +; the transmitter +var baud_div : u16 = 868; +var tx_cnt : u16 = 0; +var tx_sh : u16 = 1023; +var tx_left : u8 = 0; +var seg : u8 = 0; +var pos : u8 = 0; +var fsr : u64 = 0; +var lines : u32 = 0; +var hb : u32 = 0; + +/// The value of receipt field s (1..7), N S C Y E F L. +pub fn field(s: u8, n: u32, ws: u64, cs: u64, y: u64, e: u32, f: u32, l: u32) -> u64 { + if (s == 1) { return n as u64; } + if (s == 2) { return ws; } + if (s == 3) { return cs; } + if (s == 4) { return y; } + if (s == 5) { return e as u64; } + if (s == 6) { return f as u64; } + return l as u64; +} + +/// Lane k of beat i of the test stream, low byte first (the reference for the packer and the memory the +/// tests stand in for). +pub fn test_lane(i: u32, k: u32, bad: u32) -> u64 { + var w : u64 = 0; + var j : u32 = 8; + while (j > 0) { + j = j - 1; + w = (w << 8) | (test_byte(i * 32 + k * 8 + j, bad) as u64); + } + return w; +} + +// Every var is read before it is written, so the test's order and the clock edge agree. +fn on_clock(core_init_done: bool, core_init_error: bool, core_user_port_native_0_cmd_ready: bool, core_user_port_native_0_wdata_ready: bool, core_user_port_native_0_rdata_valid: bool, core_user_port_native_0_rdata_data__0: u64, core_user_port_native_0_rdata_data__1: u64, core_user_port_native_0_rdata_data__2: u64, core_user_port_native_0_rdata_data__3: u64, core_uart_tx: bool, uart_rx: bool) { + uart_tx = (st == ST_REPORT and (tx_sh & 1) == 1) or (st != ST_REPORT and core_uart_tx); + led_2 = !(st == ST_REPORT and verdict == V_PASS); + led_3 = ((hb >> 26) & 1) == 1; + hb = hb +% 1; + if (st == ST_WAIT) { + if (core_init_error) { + verdict = V_FAIL; + st = ST_REPORT; + } else if (core_init_done) { + st = ST_LOAD; + } + } else if (st == ST_LOAD) { + if (wph == 0) { + if (wi == n_beats) { + st = ST_READ; + ca = 0; + cv = true; + cwe = false; + rph = 0; + } else if (bfull) { + bfull = false; + ca = wi; + cv = true; + cwe = true; + wph = 1; + } + } else if (wph == 1) { + if (core_user_port_native_0_cmd_ready) { + cv = false; + wv = true; + wph = 2; + } + } else { + if (core_user_port_native_0_wdata_ready) { + wv = false; + wph = 0; + wi = wi + 1; + } + } + if (rx_got) { + if (nb == 31) { + wsum = fold(wsum, (wb0 >> 8) | (wb1 << 56), (wb1 >> 8) | (wb2 << 56), (wb2 >> 8) | (wb3 << 56), (wb3 >> 8) | ((rx_byte as u64) << 56)); + bfull = true; + nb = 0; + } else { + nb = nb + 1; + } + wb0 = (wb0 >> 8) | (wb1 << 56); + wb1 = (wb1 >> 8) | (wb2 << 56); + wb2 = (wb2 >> 8) | (wb3 << 56); + wb3 = (wb3 >> 8) | ((rx_byte as u64) << 56); + } + } else if (st == ST_READ) { + if (rph == 0) { + if (core_user_port_native_0_cmd_ready) { + cv = false; + rph = 1; + } + } else if (rph == 1) { + if (core_user_port_native_0_rdata_valid) { + csum = fold(csum, core_user_port_native_0_rdata_data__0, core_user_port_native_0_rdata_data__1, core_user_port_native_0_rdata_data__2, core_user_port_native_0_rdata_data__3); + rb0 = core_user_port_native_0_rdata_data__0; + rb1 = core_user_port_native_0_rdata_data__1; + rb2 = core_user_port_native_0_rdata_data__2; + rb3 = core_user_port_native_0_rdata_data__3; + tk = 0; + rph = 2; + } + } else if (rph == 2) { + acc = acc +% trit_term((rb0 & 255) as u8, xv); + if (!is_trit((rb0 & 255) as u8)) { bad = bad + 1; } + xv = xv +% XSTEP; + col = col + 1; + rb0 = (rb0 >> 8) | (rb1 << 56); + rb1 = (rb1 >> 8) | (rb2 << 56); + rb2 = (rb2 >> 8) | (rb3 << 56); + rb3 = rb3 >> 8; + if (tk == 31) { + rph = 3; + } else { + tk = tk + 1; + } + } else { + if (col == W_COLS) { + ysum = fold(ysum, acc as u64, 0, 0, 0); + acc = 0; + col = 0; + xv = XV0; + } + if (ri + 1 == n_beats) { + st = ST_JUDGE; + } else { + ca = ri + 1; + cv = true; + rph = 0; + } + ri = ri + 1; + } + } else if (st == ST_JUDGE) { + verdict = verdict_of(ri, wsum, csum, ysum, bad, ferr, s_want, y_want, n_beats); + st = ST_REPORT; + } else { + if (tx_cnt + 1 < baud_div) { + tx_cnt = tx_cnt + 1; + } else { + tx_cnt = 0; + if (tx_left != 0) { + tx_sh = (tx_sh >> 1) | 512; + tx_left = tx_left - 1; + } else { + tx_sh = frame(line_char(seg, pos, fsr, verdict)); + tx_left = 9; + if (pos == seg_last(seg)) { + fsr = field(seg + 1, ri, wsum, csum, ysum, bad, ferr, lines); + pos = 0; + if (seg == LINE_SEGS - 1) { + seg = 0; + lines = lines + 1; + } else { + seg = seg + 1; + } + } else { + if (seg != 0 and seg != LINE_SEGS - 1 and pos >= 3) { fsr = fsr << 4; } + pos = pos + 1; + } + } + } + } + if (rx_busy) { + if (rx_cnt + 1 < rx_wait(rx_bit, rx_div)) { + rx_cnt = rx_cnt + 1; + rx_got = false; + } else { + rx_cnt = 0; + if (rx_bit == 0) { + if (rx_s2) { + rx_busy = false; + } else { + rx_bit = 1; + } + rx_got = false; + } else if (rx_bit < 9) { + if (rx_s2) { + rx_sh = (rx_sh >> 1) | 128; + } else { + rx_sh = rx_sh >> 1; + } + rx_bit = rx_bit + 1; + rx_got = false; + } else { + rx_busy = false; + rx_bit = 0; + if (rx_s2) { + rx_byte = rx_sh; + rx_got = true; + } else { + ferr = ferr + 1; + rx_got = false; + } + } + } + } else { + rx_got = false; + if (!rx_s2) { + rx_busy = true; + rx_cnt = 0; + rx_bit = 0; + } + } + rx_s2 = rx_s1; + rx_s1 = uart_rx; +} + +; --- the tests ---------------------------------------------------------------------------------- + +test the_tensor_is_640_beats_of_32_trits { + var beats : u32 = 0; + var bytes : u64 = 0; + var r : u32 = 0; + while (r < W_ROWS) { + beats = beats + BEATS_PER_ROW; + bytes = bytes + (W_COLS as u64); + r = r + 1; + } + assert_eq(beats, W_BEATS); + assert_eq(bytes, W_BYTES); + assert_eq((beats as u64) * BEAT_BYTES, bytes); + assert_eq((BEATS_PER_ROW as u64) * BEAT_BYTES, W_COLS as u64); + assert_eq(W_OFFSET, 10589476); +} + +test a_trit_adds_plus_x_minus_x_or_nothing { + assert_eq(sext8(11), 11); + assert_eq(sext8(127), 127); + assert_eq(sext8(128), 0xFFFFFF80); + assert_eq(sext8(255), 0xFFFFFFFF); + assert_eq(trit_term(1, 11), 11); + assert_eq(trit_term(255, 11), 0xFFFFFFF5); + assert_eq(trit_term(0, 11), 0); + assert_eq(trit_term(2, 11), 0); + assert_eq(trit_term(1, 200), 0xFFFFFFC8); + assert_eq(trit_term(255, 200), 56); + assert_eq(trit_term(255, 0), 0); + assert_eq(trit_term(1, 11) +% trit_term(255, 11), 0); + assert is_trit(0) and is_trit(1) and is_trit(255); + assert !is_trit(2) and !is_trit(254) and !is_trit(128); +} + +test the_input_is_37c_plus_11_as_an_int8 { + var x : u8 = XV0; + var c : u32 = 0; + var zero_at : u32 = 9999; + while (c < W_COLS) { + assert_eq(x as u32, (37 * c + 11) % 256); + if (x == 0) { zero_at = c; } + x = x +% XSTEP; + c = c + 1; + } + assert_eq(zero_at, 145); +} + +test the_receiver_takes_a_frame_at_mid_bit_and_counts_a_bad_stop { + st = ST_WAIT; + rx_div = 4; + rx_s1 = true; + rx_s2 = true; + rx_busy = false; + rx_got = false; + rx_byte = 0; + ferr = 0; + var got : u32 = 0; + var t : u32 = 0; + while (t < 60) { + on_clock(false, false, false, false, false, 0, 0, 0, 0, true, frame_bit(0xA5, t / 4)); + if (rx_got) { got = got + 1; } + t = t + 1; + } + assert_eq(got, 1); + assert_eq(rx_byte, 0xA5); + assert_eq(ferr, 0); + t = 0; + while (t < 60) { + on_clock(false, false, false, false, false, 0, 0, 0, 0, true, t / 4 < 9 and frame_bit(0x3C, t / 4)); + if (rx_got) { got = got + 1; } + t = t + 1; + } + assert_eq(got, 1); + assert_eq(ferr, 1); + rx_div = 868; +} + +test two_rows_go_in_come_back_and_are_multiplied { + var sref : u64 = 0; + var i : u32 = 0; + while (i < 20) { + sref = fold(sref, test_lane(i, 0, 99999), test_lane(i, 1, 99999), test_lane(i, 2, 99999), test_lane(i, 3, 99999)); + i = i + 1; + } + var yref : u64 = 0; + var r : u32 = 0; + while (r < 2) { + var a : u32 = 0; + var x : u8 = XV0; + var c : u32 = 0; + while (c < W_COLS) { + a = a +% trit_term(test_byte(r * W_COLS + c, 99999), x); + x = x +% XSTEP; + c = c + 1; + } + yref = fold(yref, a as u64, 0, 0, 0); + r = r + 1; + } + st = ST_LOAD; + n_beats = 20; + s_want = sref; + y_want = yref; + ca = 0; + cv = false; + cwe = false; + wv = false; + wb0 = 0; + wb1 = 0; + wb2 = 0; + wb3 = 0; + wph = 0; + wi = 0; + nb = 0; + bfull = false; + wsum = 0; + rph = 0; + ri = 0; + tk = 0; + col = 0; + xv = XV0; + acc = 0; + ysum = 0; + csum = 0; + bad = 0; + ferr = 0; + verdict = V_FAIL; + rx_s1 = true; + rx_s2 = true; + rx_busy = false; + rx_got = false; + rx_div = 4; + var wrote : u32 = 0; + var t : u32 = 0; + while (t < 40000 and st != ST_REPORT) { + if (st == ST_LOAD and wph == 2) { + assert wb0 == test_lane(ca, 0, 99999) and wb1 == test_lane(ca, 1, 99999) and wb2 == test_lane(ca, 2, 99999) and wb3 == test_lane(ca, 3, 99999); + assert cwe; + wrote = wrote + 1; + } + on_clock(true, false, true, true, st == ST_READ and rph == 1, test_lane(ca, 0, 99999), test_lane(ca, 1, 99999), test_lane(ca, 2, 99999), test_lane(ca, 3, 99999), true, t / 48 >= 640 or frame_bit(test_byte(t / 48, 99999), (t % 48) / 4)); + t = t + 1; + } + assert_eq(st, ST_REPORT); + assert_eq(wrote, 20); + assert_eq(ri, 20); + assert_eq(wsum, sref); + assert_eq(csum, wsum); + assert_eq(ysum, yref); + assert_eq(bad, 0); + assert_eq(ferr, 0); + assert_eq(verdict, V_PASS); + assert_eq(col, 0); + rx_div = 868; + n_beats = 640; +} + +test a_byte_that_is_no_trit_is_counted_and_fails { + var sref : u64 = 0; + var i : u32 = 0; + while (i < 10) { + sref = fold(sref, test_lane(i, 0, 17), test_lane(i, 1, 17), test_lane(i, 2, 17), test_lane(i, 3, 17)); + i = i + 1; + } + var a : u32 = 0; + var x : u8 = XV0; + var c : u32 = 0; + while (c < W_COLS) { + a = a +% trit_term(test_byte(c, 17), x); + x = x +% XSTEP; + c = c + 1; + } + st = ST_LOAD; + n_beats = 10; + s_want = sref; + y_want = fold(0, a as u64, 0, 0, 0); + ca = 0; + cv = false; + wv = false; + wph = 0; + wi = 0; + nb = 0; + bfull = false; + wsum = 0; + rph = 0; + ri = 0; + col = 0; + xv = XV0; + acc = 0; + ysum = 0; + csum = 0; + bad = 0; + ferr = 0; + verdict = V_PASS; + rx_s1 = true; + rx_s2 = true; + rx_busy = false; + rx_got = false; + rx_div = 4; + var t : u32 = 0; + while (t < 20000 and st != ST_REPORT) { + on_clock(true, false, true, true, st == ST_READ and rph == 1, test_lane(ca, 0, 17), test_lane(ca, 1, 17), test_lane(ca, 2, 17), test_lane(ca, 3, 17), true, t / 48 >= 320 or frame_bit(test_byte(t / 48, 17), (t % 48) / 4)); + t = t + 1; + } + assert_eq(st, ST_REPORT); + assert_eq(ri, 10); + assert_eq(wsum, sref); + assert_eq(csum, wsum); + assert_eq(ysum, y_want); + assert_eq(bad, 1); + assert_eq(verdict, V_FAIL); + assert_eq(verdict_of(ri, wsum, csum, ysum, 0, 0, s_want, y_want, 10), V_PASS); + assert_eq(verdict_of(ri, wsum, csum ^ 1, ysum, 0, 0, s_want, y_want, 10), V_FAIL); + assert_eq(verdict_of(ri, wsum, csum, ysum ^ 1, 0, 0, s_want, y_want, 10), V_FAIL); + assert_eq(verdict_of(ri, wsum, csum, ysum, 0, 1, s_want, y_want, 10), V_FAIL); + assert_eq(verdict_of(9, wsum, csum, ysum, 0, 0, s_want, y_want, 10), V_FAIL); + rx_div = 868; + n_beats = 640; +} + +test a_failed_calibration_reports_fail { + st = ST_WAIT; + verdict = V_PASS; + on_clock(false, true, false, false, false, 0, 0, 0, 0, true, true); + assert_eq(st, ST_REPORT); + assert_eq(verdict, V_FAIL); +} + +test the_receipt_line_says_what_was_computed { + st = ST_REPORT; + ri = 640; + wsum = 0x0123456789ABCDEF; + csum = 0x0123456789ABCDEF; + ysum = 0xFEDCBA9876543210; + bad = 0; + ferr = 0; + lines = 0; + verdict = V_PASS; + baud_div = 1; + tx_cnt = 0; + tx_sh = 1023; + tx_left = 0; + seg = 0; + pos = 0; + var got : u32 = 0; + var bits : u32 = 0; + var ch : u8 = 0; + var line : u32 = 0; + while (line < 2) { + on_clock(true, false, false, false, false, 0, 0, 0, 0, true, true); + bits = bits + 1; + if (tx_left == 9) { + assert_eq(tx_sh & 1, 0); + assert_eq(tx_sh >> 9, 1); + ch = ((tx_sh >> 1) & 255) as u8; + if (got == 0) { assert_eq(ch, 84); } + if (got == 4) { assert_eq(ch, 84); } + if (got == 7) { assert_eq(ch, 78); } + if (got == 9) { assert_eq(ch, 78); } + if (got == 10) { assert_eq(ch, 61); } + if (got == 24) { assert_eq(ch, 50); } + if (got == 25) { assert_eq(ch, 56); } + if (got == 26) { assert_eq(ch, 48); } + if (got == 28) { assert_eq(ch, 83); } + if (got == 31) { assert_eq(ch, 49); } + if (got == 45) { assert_eq(ch, 70); } + if (got == 47) { assert_eq(ch, 67); } + if (got == 66) { assert_eq(ch, 89); } + if (got == 68) { assert_eq(ch, 70); } + if (got == 83) { assert_eq(ch, 48); } + if (got == 85) { assert_eq(ch, 69); } + if (got == 104) { assert_eq(ch, 70); } + if (got == 123) { assert_eq(ch, 76); } + if (line == 0 and got == 140) { assert_eq(ch, 48); } + if (line == 1 and got == 140) { assert_eq(ch, 49); } + if (got == 142) { assert_eq(ch, 80); } + if (got == 145) { assert_eq(ch, 83); } + if (got == 146) { assert_eq(ch, 13); } + if (ch == 10) { + assert_eq(got, 147); + got = 0; + line = line + 1; + } else { + got = got + 1; + } + } + } + assert_eq(lines, 2); + assert_eq(bits, (2 * 148 - 1) * 10 + 1); + baud_div = 868; +} + +test the_pins_that_read_the_run_are_set_from_its_state { + baud_div = 868; + tx_cnt = 0; + tx_left = 0; + st = ST_WAIT; + verdict = V_PASS; + hb = 0; + tx_sh = 1023; + on_clock(false, false, false, false, false, 0, 0, 0, 0, false, true); + assert_eq(uart_tx, false); + assert_eq(led_2, true); + assert_eq(led_3, false); + on_clock(false, false, false, false, false, 0, 0, 0, 0, true, true); + assert_eq(uart_tx, true); + st = ST_REPORT; + tx_sh = 1022; + hb = 67108864; + on_clock(false, false, false, false, false, 0, 0, 0, 0, true, true); + assert_eq(uart_tx, false); + assert_eq(led_2, false); + assert_eq(led_3, true); + tx_sh = 1023; + on_clock(false, false, false, false, false, 0, 0, 0, 0, false, true); + assert_eq(uart_tx, true); +} diff --git a/specs/fpga/tern9m_l0_k_weights.t27 b/specs/fpga/tern9m_l0_k_weights.t27 new file mode 100644 index 0000000000..6fe9418022 --- /dev/null +++ b/specs/fpga/tern9m_l0_k_weights.t27 @@ -0,0 +1,781 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/fpga/tern9m_l0_k_weights.t27 -- the weights of cell 26: blocks.0.attn.k.weight of tern-tc-9m +; The data of specs/fpga/ddr3_ternary_matvec.t27 (issue gHashTag/t27#10461, epic gHashTag/t27#10024), and the +; tests that compute from it the two values the board must report, with the board spec's own functions. +; - +; SOURCE. c_infer/model.bin of Hugging Face playra/tern-tc-9m, 16,953,800 bytes, sha256 +; 3102abdf35057924e077a86db4fdac726e4fe1f6574df47f39a638ba99a3ce9c. The tensor is 64 rows of 320 int8 trits, +; row-major, 20,480 bytes at offset 10,589,476; the f32 scale after it is not used. +; MADE WITH. `od -An -v -tx8 -j 10589476 -N 20480 model.bin`, one 32-byte beat per line, each word little-endian +; (byte 0 of the beat is the low byte of its first word). Nothing here was typed in by hand. +; THE UPLOAD. The same bytes, in the same order, are what the host sends to the board: +; `dd if=model.bin bs=1 skip=10589476 count=20480`. +; ASCII only, English only. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module FpgaTern9mL0KWeights; + +use fpga::ddr3_ternary_matvec; + +pub const W_WORDS : u32 = 2560; +/// No byte changed (an index past the 20,480 bytes). +pub const NO_FLIP : u32 = 99999999; + +/// The 640 beats of the tensor, four words each. +pub const W : [2560]u64 = [ + 0x10001ffff00ff, 0x100010100ff0100, 0x1ffff000101, 0xff0000ff0100, + 0xff0101000000ffff, 0xffff0001000001, 0x100ff0000000101, 0x1000000ff00ff01, + 0x1000001ff00ff, 0x1ff0100010000, 0x1000100ff01ff00, 0x100000100000001, + 0xffff00ff0100ff00, 0x10000000000, 0xff000100000100, 0x100ff010000, + 0x100ff0100000001, 0xff00ffff00000000, 0x1010000000000, 0xff0001ffff00, + 0x1ffff01ff00ff00, 0x1ff000000, 0x10000ff, 0xffff010000000100, + 0x100000000010000, 0x10101ff010100, 0xff010000ff00, 0xff01010000ff0100, + 0x1ff000001010101, 0x1ff0000ff0100, 0xff00000000000001, 0x10000ff01ff01ff, + 0x10101ff0001, 0xff01000001010101, 0x1000000ff00ff00, 0x100ff0000ff, + 0xff0000ff, 0x1000000010000ff, 0x100ff0100010001, 0x1000000000000, + 0x1000100000000, 0x101000000ff0101, 0x1ff0100ffff0101, 0x1ff00000100ff00, + 0xff00000000000100, 0x1ff00ff00ff0000, 0x10001ff00ff01, 0x1000000000001, + 0x1000100, 0xffffff0001, 0x100000001ff01, 0x10000000000ff01, + 0xff01ff0100ff01, 0x10001000000ff00, 0xffff000100000000, 0xff000001000100, + 0x101000000, 0xff01ff0000000000, 0xff00ff, 0x100ff00000000, + 0x1010000ff000000, 0x1ffff0000ff0000, 0xff0100ffff00ff, 0x10001000000, + 0x100000001010100, 0x101ff000100, 0xff0000010000ff00, 0x10100ffff000000, + 0x10101, 0xff0100ff0100, 0x101000000, 0x100ff0000000000, + 0xff0101000000, 0x10101010001, 0x101000001000001, 0x10000000000ff00, + 0x10000ff0000ff00, 0x10000ff00000000, 0xffff00000000, 0x1000000000000, + 0xff0001ff, 0x1000101ffff0000, 0xffffff0000, 0xff00000101ff0000, + 0xff000100010100ff, 0xff0000ff010000ff, 0xff0000ff0101, 0x100ff0000ffff, + 0xffff01ff01ffff00, 0x100000101000000, 0x1ff0100ff010000, 0x1ff010000ff0000, + 0xffff01ff000000ff, 0xff01ff, 0x1000000000100ff, 0x101010000010100, + 0x100ff0000000001, 0xff00000000000000, 0xff00000000000000, 0x1ff000000000000, + 0x1ff0000ffff00ff, 0x10000ffffff00, 0x100000001000001, 0xff00000000000000, + 0x100ffffff010100, 0xff000101ff0100ff, 0xff000000ffff, 0x100, + 0xff000000010100, 0x100ff0000ff0100, 0x100ff0000, 0x101000101ff0100, + 0xff000000ffff00, 0x100000100ff00, 0xff000000000001, 0xff, + 0x1000100000100ff, 0xff0000000000, 0x101ff01ff000000, 0x1000000000100, + 0x100ff00, 0xff00ffff00010000, 0x100, 0xff01ffff010001, + 0xff0100ff0100, 0x100010001, 0xff01000000ffff, 0xff000101000101, + 0x1000000010000, 0x1000100ff00ff00, 0xff000000ff000001, 0xff0100ff00010000, + 0x100000001ff0001, 0x10000, 0xffff000000ff0001, 0xff0000000000ff, + 0x1010000ff00, 0x1000101ff00ff00, 0x10000000000ff00, 0xff01ff0001000000, + 0xff0000ff01010001, 0x1010100, 0xff0100ff0001ff00, 0xff000000, + 0xff0100000000ff01, 0xff01ffff01, 0xff00ff01000001, 0x1ff00ffff00, + 0xff0100000000ff00, 0xff0000000000ffff, 0x10000010100, 0xff00ff000000, + 0x1000000000001, 0x1ff000100, 0xff0000, 0xff00000000, + 0xff0100ff01ff0001, 0x0, 0xff00ff0001, 0xff010001000000, + 0x10000ffff000000, 0xff000100ff0000, 0x100ff000000, 0x1ff00ff, + 0x1ff0000000000, 0xff00ff, 0xffff00, 0xff0100000001ff00, + 0x100, 0xffff0000010000, 0x0, 0xff0001, + 0xffffff0000ffffff, 0xff0000000000, 0xff0000000001, 0x1010000000000, + 0xff0000ff0000ff, 0xffffff0101ff0000, 0xff00ff0001ff01, 0x100000000000000, + 0xff000101010000, 0x1000000ffff00, 0x1ff010000000001, 0x0, + 0xff0000ff01, 0xff0001ff0000ff, 0x100ff010000ffff, 0xff00, + 0x1010001010000, 0xff0101000100, 0xff01000000ffff00, 0x10000000100, + 0x1ff000000000000, 0xff0001ff01010000, 0x10000000001ff01, 0xff010001000000ff, + 0xff00ffff0000ff, 0xff, 0x10000ff00, 0x100ff000101ff, + 0x1000100ff000000, 0xff000001000000, 0xffffff00ff, 0x1000001000000, + 0xff0000ff00010100, 0x10001ff0000, 0x1ff000000ff00, 0xff00000000ffff00, + 0x101ff0101, 0xff00ff0000000000, 0x10001000001, 0x1ff00ffff01, + 0xff0000ff01010000, 0x1000001ff00ff, 0x101ff01, 0x1000000ff000100, + 0xffff000000, 0xffffff00000000ff, 0xff0000ff0000, 0x1ff00000000, + 0x100010000000000, 0x100000001000000, 0x1000000ff000000, 0x1ff0000000000ff, + 0x10000000001ff00, 0xff000101ff010101, 0x1000000ff, 0x101000000000000, + 0xff01000000010001, 0xff000101000000ff, 0x1000100010001, 0xff00ff000001, + 0xff0000000001ff00, 0x10000010100ff00, 0x1000101ff0000, 0x1000100010000, + 0x1ff0000ff00, 0x10000ff00010000, 0xff000001ff000000, 0x1000000010100, + 0x1ff0101ff000101, 0x100ff0001000001, 0x1010001ff00ff, 0x1000100ff00ffff, + 0x1ff010000ffffff, 0x1010101ffff00, 0xffffffff01000000, 0xff01ff0101ffff00, + 0x100000100000100, 0x10000ff01010000, 0x1010000ff0000, 0xff00ffff00ff00, + 0xffffff00ff000000, 0xff00ff000000ff00, 0x101ff0000000001, 0x1ff01ff00ff01, + 0xffffff00ffff, 0xff01ff01ffff, 0x101010001ff, 0xff0000ffffffff00, + 0xff0100000100, 0x1ff01ff000000, 0x1000000000100ff, 0xff00ff01ff01ff, + 0x100ff0000ff00ff, 0x100ff000101, 0x1000001000000ff, 0xff01ffff0001ff00, + 0x1ff0001ff0100ff, 0xff00ff0000ff0001, 0x101000000000000, 0xff0000ff000000ff, + 0x10001ff000000, 0xff0101ff01000000, 0xff00ffff00ff, 0xff01ff0000ff00, + 0x10000ff000101, 0xffff000001000100, 0x100000101010001, 0xff0000000001ff00, + 0xff01000000000000, 0xffff000100, 0x1000101ff0000, 0x1010001ff01ff, + 0x1ff01ff010000, 0x1010001ff01ffff, 0xff00ffffff000001, 0x1000001ff00, + 0x100ff01010001, 0x101ff00ff00ff01, 0x10001ff00ffffff, 0x1ff01ff, + 0xffff00ff0000, 0x100ff00ff0100, 0xffff00ff00010000, 0x1000000010100, + 0xff010000ff00ff, 0xff00ffff000000, 0xff00ff00000000, 0x1000100ff000100, + 0xff00000001ff01, 0x100000001ffff00, 0xffff0001010101, 0xff00ff0000ff0001, + 0xff0101ff0000ffff, 0xff0001ff000100, 0x101ff010001ffff, 0x100ff010101, + 0x101010101, 0x100010100, 0xff01ff00ff0100, 0xff000000ffff01ff, + 0xff01ff01ffff00, 0xff000100000100ff, 0xff010100ff0000, 0x100ff000000, + 0x10001ff010101ff, 0xff01ffff0000ffff, 0x1ff010100000001, 0x101ffffff010000, + 0x101010100ff, 0xff0000ff000000, 0xff00000000010001, 0x1ff0001ff010001, + 0xff00000000ff0100, 0xff0000010101, 0xffff000100ffff, 0xffff000000000000, + 0x101000100010101, 0xffff00ff00ff, 0x1000100010000, 0xff0000ff00010101, + 0x100ff0001000100, 0x100ff00ff0000ff, 0xffff0000ffff0000, 0x10000ffffff, + 0x100000100ff0101, 0x101ff00ffff, 0x100ff010001ffff, 0xff00000100ff00ff, + 0xff0000000101, 0x100000000ffffff, 0xff0100000101ffff, 0xff00010000010000, + 0x10100010000ff, 0x101ff0100ff01, 0xff010001000001, 0xff0101000100ffff, + 0xff00010000ff00ff, 0x10001ffff, 0x100000100010001, 0xff00ff0000ff, + 0xff0001ff00, 0xff00ff01ffff0000, 0xff0100ff00ff0000, 0x100ffff00000000, + 0xff01000000000001, 0x10000ffff00ff00, 0xffffff00ffff01, 0xff00000101010101, + 0x1ff01ffff000100, 0x100ff01000100, 0x1000100ff000000, 0xff00ff, + 0xff010000ff000100, 0x100000100, 0x1ff0100000100, 0xffff0100000000ff, + 0x101000100, 0xff01ffffff000001, 0x10101000100ff00, 0xffff0000ffffff00, + 0xffff0000000100ff, 0x1010000ffff0100, 0xff00000000000001, 0x101ff0100000101, + 0x1010101ff0001, 0x100ffff00000000, 0x1ff000100000000, 0x101010001ff01, + 0xff01ff01ffff0100, 0x100010001000000, 0x1ff00000001ffff, 0x1ffff01000000ff, + 0xff00010000, 0xff0101ffffff00, 0xffff0100000000, 0xff0000ff010100ff, + 0x101010101010000, 0xff000001ff00ff, 0x1000000010101, 0x101ffffff00, + 0x1000000010000, 0x101ff01, 0x10000000001ff, 0x0, + 0x100ff0000ff00ff, 0xff0001ff0001ffff, 0xff000000, 0x1ffff, + 0xff0101010001ff00, 0x100ffff010001, 0x100000100ff00, 0x1ff0000ff010000, + 0xff0000010000ff00, 0xff000000010101ff, 0xff0000ff, 0xff00ffff000100ff, + 0x10101ff000001, 0x1ff01ff0100, 0xff00ff00ffff01ff, 0xff01ffffffff0101, + 0xff01ff01ff00, 0xffffff00ff00ff01, 0xff01ff0000, 0x1000101ff000001, + 0x1ffffffffffff01, 0x1ff0101000001ff, 0x1ff01010101, 0xff000000010101ff, + 0x100ff000000ff01, 0xff0101000001ffff, 0xff000100ff01ff01, 0xff00ff01ffffff, + 0x1010001010000ff, 0xff0101ff010000ff, 0xffff00ff01ff, 0xff0001000001ff01, + 0x10100000100ff, 0xffff0000ffff01ff, 0x10000ff01010000, 0xff00ff00ffff0001, + 0x1000100ff000101, 0xff0100ff00ff0000, 0xff010000ffff01ff, 0xff0001ff00ffff00, + 0x10001010100ff00, 0xffffffff0101ff, 0x1ff00ff00ff00ff, 0xffff0001ffffff00, + 0xff0000ff00ff00, 0xffff01ff00ff01ff, 0x10101ff00000101, 0x100000001ff00ff, + 0xffffff01ff010001, 0xff00000100ff, 0x101ffff000000ff, 0xffff0000ff01, + 0x1ff00ff01ff0000, 0x10001ff, 0x101ff0000ffffff, 0xff0000ff0000ff00, + 0xffff00ff000101ff, 0xff01ff0000ff, 0xff0001000001ff, 0x1010000010001, + 0x1010100ffff0100, 0xffffffff010000ff, 0x1ff010101000000, 0x1000000ff00, + 0xffffffff00ff00, 0x10101ff01ff0000, 0x1ffff000101ff00, 0xff0001ff00ff00ff, + 0x1ff0000ff010000, 0xffff0000ff000100, 0x1ff0001000000, 0x10000ffff0000, + 0x1ff000000000000, 0x1ffff0101010101, 0xffff0100ffff01, 0x1ff00ff01ff0001, + 0x1ff01000001ff00, 0x1ff01ff00010000, 0x10101ff00ff00, 0x10000000000ff, + 0x100ffff010000ff, 0x10100000101ff00, 0xff00010101ff01ff, 0x1010000000100ff, + 0xff0100ffff00ff, 0x1ff010100, 0xff00000000ff0000, 0x1000100ffffff00, + 0x100010000ff0100, 0x101ff00ff0000ff, 0x100ffff01010001, 0x1000001000100ff, + 0x1ffffff000101ff, 0x101ffffff00ff00, 0x101ff0001ff00ff, 0x1ff00ffff010101, + 0xffff01ff000001, 0x1000001010001ff, 0xff00ff000101ff01, 0x1000100ffff0101, + 0xff010101ffff01ff, 0x1ffff0001000001, 0xff0000010100ff, 0x10001ffffffff, + 0x101ff01ff000000, 0xff000001ff0000, 0x1ff000101ff00ff, 0xff00010000ff, + 0xffff0001ff0101, 0xffffff01ffff01ff, 0x101ff00ff000101, 0xffffff00ff000101, + 0xff01000101ff0000, 0xffffff00000101ff, 0xff0001ff0000ff01, 0xff00ff01ffffff00, + 0x100ff00ffffff01, 0x101010100ff, 0x1ff01000001ffff, 0xffff010100ff0000, + 0xff01ffffffff0000, 0x100010100ffff, 0x10000010101ff01, 0x100ff0000ff01, + 0xff00ff00010001ff, 0xff010000ffff00ff, 0xffff000101ff00, 0x1ff01, + 0xffff0100000101, 0xff00ff000000, 0x100010001ffff00, 0x10000ff00010100, + 0xff01ffff0000ff, 0xff01ff0001ff00, 0xffff0000010100, 0x1ff0000010101ff, + 0x10100ff00000101, 0x101ff00010000, 0x101010100010001, 0xff00ffff010100ff, + 0xff010100ff00, 0xff01010100000001, 0x100ff000000, 0x100ff0000010100, + 0xff01ff00000000, 0xff00ff00ff0001, 0xff0000ff01ff0101, 0x101000000010001, + 0xffffffffff000000, 0xff00ffff01000000, 0x1ffffff0100, 0x100ff01ff000000, + 0xff000000, 0xff000000ff000000, 0xffff01ff, 0x10000000001, + 0xff000001000000, 0x1ff00ffff000000, 0xffff00ff0000ff01, 0xff, + 0x100ff00000100ff, 0x1ff0100ff000101, 0xff00000001, 0x10000000001ff01, + 0xffff01ff01000100, 0xff01ff0000000101, 0xff0000ff000100ff, 0x100ff0100010001, + 0x100ff000000, 0xff00ff010001ff, 0x1ffff0000, 0xffff0101ff0101ff, + 0xffff00ff0000ff01, 0xff0100010001ff, 0xff00000100ff00, 0x100ff01010100, + 0x1ff000000ff01ff, 0xff00000001010000, 0xff000000ff01ff01, 0x101010100ff0001, + 0xff0001ff00000000, 0xff0001010101ff00, 0x101000000000100, 0xff00ff01ff00ff00, + 0x1ff000101ff00, 0xff01ff01ffff01ff, 0xff01010000ff0000, 0xffff0100ff010001, + 0xff0000000100ffff, 0xffff0100ff00, 0xffff01ff01000001, 0xff000100010001ff, + 0xff0000ff000101ff, 0xff01000000ffffff, 0x101ff010000, 0x1ffffff01010000, + 0x101ffff010100ff, 0xff010001ff000000, 0xff0100ff00ff01ff, 0xffffffff010000ff, + 0xffffff0100ffffff, 0xff00ff01ff0100, 0xff00ffff01ff00, 0xffff000101ffff01, + 0x101ff01ffffffff, 0xff000100ff010000, 0x100010000ffffff, 0x100000001ff0000, + 0xff000000ffff0001, 0xff000100ff01ff, 0xffffff0000ffff00, 0xffff000000, + 0x10000ff0000, 0xff01ff01ff000101, 0x100ff00ffff00, 0x1ff0101000000, + 0xff0100000001ff00, 0x100ff01ffff0100, 0xffffff00010001, 0x1000000ffffff00, + 0xff0100ff0101, 0xffff00000000ff, 0x100ff0001000100, 0xff010001ffff00, + 0x1ff0000010100, 0x1ff00ff01ff01ff, 0x10101ff0100ff00, 0x100ff01000001ff, + 0x10000ff01ffff, 0x10000ff01ff00, 0xffffff01000001ff, 0xff0100ffffff00ff, + 0x100ff010000ff, 0xff010100ff, 0x1000001ff000100, 0x10001ff0000ffff, + 0xff0100ffff000001, 0xff01000000010000, 0x1ff01ff000000, 0xff00000001ffff, + 0xffff0001ff0000, 0xff000100000000ff, 0x100000101ff0100, 0x10101ff000101, + 0x10001ff0001ff, 0x100010101ff0101, 0xffff01ff0100ffff, 0x1010101ff0001, + 0x10000ffffff0001, 0xff01000101ff0000, 0xffff01ff000001ff, 0xff000101ff00, + 0x101ffff00010000, 0x1000101ff01ff00, 0xff00ff0000ff0100, 0x100ff01ffff00, + 0xffffffff00010001, 0x100010100000100, 0x1ffff01, 0x1ffff00ff010101, + 0x1ff01ff00000100, 0xffffff010001ff00, 0x1ff000000000100, 0x1000000ff0001, + 0xffffff0101000000, 0x1ffff01ffff0001, 0x10100ff01ff00ff, 0xff00000101000001, + 0x1ff00010100, 0x101ff000101, 0x100ff01ff00ff01, 0xff0000ffff010001, + 0xffffff0100ffff, 0x1ff0000ff00, 0xffffff00ff0000, 0x1ff01ffff00, + 0x100010100, 0xff0001ff01000100, 0x1000101ffffff00, 0xff010101ffff00, + 0x1010100ff000000, 0xff00010000010100, 0x100010100010101, 0xff00ff01ffff, + 0x10000ff010000, 0x1ff0001000100, 0x101000000ff0100, 0x1000000ffff00, + 0x101000100ffffff, 0xff00ff01ff00ff00, 0x100000000000101, 0x10101ff00ff00, + 0x1000000ff01ff00, 0xff0001000000ff, 0x100ff0001ffff00, 0xffffffff00ff01ff, + 0xff00000000010000, 0x10100ff0001, 0x1010001, 0xff00ff000100ff01, + 0xff010100ff01ffff, 0x1000000ffff0001, 0x10001, 0x1ff00010000, + 0x101ff00ffffff, 0xffffff000000, 0xff000000010001, 0x1ff00ff010000, + 0x1ff0001ff00ff01, 0xff00ff000001, 0x1ff0000ff010100, 0xff0001ff000101, + 0x101000000010000, 0xffffff00ff010000, 0x1ff010000010000, 0xff0000ff00ffff01, + 0xff00ff0101ff01ff, 0x10001ff01000000, 0xff00000001ffff00, 0x1ffff01ff0000ff, + 0x1ff0001010000ff, 0x1ff00ffff01, 0xff010101ffff00ff, 0x100ff00000000ff, + 0x1ff0101ff00ff01, 0x1ff0100ff010101, 0xff010001ff0001, 0x101010100ff01ff, + 0xff00ff0000ff, 0x101010000000100, 0xff00ffff00010101, 0xffff01ff00ff01, + 0xffff00010000ff, 0xff01ffffffff0100, 0x101ff01ffff00, 0x1000001ffff0100, + 0xffff00000001ff01, 0x1ff00ffffffff, 0x100ffff00000100, 0x1ffffff010101, + 0x10101ff00ffffff, 0xff01ffffffffffff, 0xff00010101010100, 0x10100ff00ffff00, + 0x1ff0100010000, 0x10101000001ffff, 0x10100010001ffff, 0x10000ff00ff00ff, + 0x100ff01ff01ff01, 0x1ff0001ff000001, 0x100ff010100ff00, 0xff01ffff00ffffff, + 0x101ffff00000001, 0xff00ff0101ff0101, 0x10000000001ff01, 0xff01ff01ff00ff00, + 0xff01ff0000ffff01, 0xff000101010101ff, 0x1000101ffff01, 0xffffffffffff01, + 0xff0100ffff00ff01, 0xffff, 0xffff0100ff0001, 0xff000100ff0000ff, + 0xff00ff000001ff01, 0xff0000010000, 0xff01ffff00010100, 0xffffff0001010000, + 0x1000001ff0101, 0xffff01ff010101, 0x10001010101ffff, 0xffffff0101ff00, + 0xffff01ff0100ffff, 0xffff0000ff01ff01, 0x1ff, 0xff00ff00ff0000ff, + 0x100ff00000001ff, 0x1010000ffff00, 0x1010101ff000001, 0xffff01010000ff01, + 0x1ff00010001, 0x101ff0001ff00, 0xff0001ffff00ff01, 0xff01ffffff00ff00, + 0x100ff0000ff00ff, 0xff010101ff01, 0xff0100ff000000ff, 0x1000000010000, + 0xff01ff0001ff0100, 0x1ff0101ffff00, 0x101ffff000101, 0xff01ff0101000001, + 0xffff01000001ffff, 0x101ff0100ff0000, 0x101ff0000000000, 0xffff010001ffff00, + 0x101ffff010101ff, 0x1ffffffffff0000, 0xff00ff0000ff00ff, 0x1ff0001000100, + 0x1000000ff0100, 0xffffffffff000100, 0x100ff0001ff01, 0xffff010000000000, + 0x101ff0100, 0x10000ff00ffffff, 0x100010101000100, 0xff00000100ff, + 0xff01ff00000101, 0x1ff0101010000ff, 0xff0001000101ff01, 0x1ff00ffffff, + 0x1ffff00ff000100, 0xffffffffff0100ff, 0x100ff01ffff0001, 0x1000100000001, + 0xff00ffff01000100, 0xff0001ff00ff0100, 0x101000101000001, 0xff00010000000000, + 0x101ffff00ff00, 0x100ffff01, 0x1ffffff00000101, 0x100000000ff01, + 0x10101ffffffff01, 0xff0001ff0000ff00, 0x1ff0101000001, 0x10101ff01000000, + 0x10001010101ffff, 0x10100ff01ffff, 0xff00000000000001, 0x1000101ff0001, + 0xff01ff00ff0000, 0x1ff0000ff0100, 0x1ff0001ff0000ff, 0x1ff00000100ff00, + 0xff01000101ff, 0x1000000010000ff, 0x100ff0000ff0001, 0x1010101000001, + 0xff010001ff000101, 0x1000001ff01ff01, 0x100000000ff01ff, 0x101010100ff0100, + 0xff0001010101ff, 0xff00ff0100ff0000, 0xffffffff0101ff01, 0xffff010001ff01, + 0x1ff000101ff0000, 0xffff0101ff01ff00, 0x1ff0000ffff0000, 0x1000101ff0101ff, + 0xff01ffff01ff01, 0xff00010001ff01ff, 0xffff00ffffff00, 0xffffff0101ffff, + 0x1010001ffff01ff, 0xff000101ffff, 0xff010001ffff0000, 0xff0000010101ff00, + 0xff000000010100ff, 0x10101ff0001ff00, 0x100ff01ff010100, 0xff01ff0001000100, + 0x100ff0001010000, 0xffff010101000001, 0xff01ffffff0001ff, 0xff010001ff010000, + 0xff00010001ff01ff, 0x1ff0001ffff01, 0xff010100ff010000, 0x1ff0000ff010101, + 0xff0001ffff000001, 0x101000000ff0000, 0xff000001ff000101, 0xffff0000000101, + 0x1ff01ff0001ffff, 0x10100ffff0001ff, 0xff00ffff00ff01ff, 0x1ffffffffff0000, + 0x1000101ff0100, 0x10001ff00ff0101, 0xffffffff010100ff, 0x1ff010101ff0001, + 0x1ffffff0101ffff, 0xff01ff01ffffff01, 0xff00ffffff01ff00, 0x1ffffff00010001, + 0x1ff010101000101, 0x10101ff00ff00, 0x1ff0100ff01ffff, 0x1010101ffff01ff, + 0xffff00ff01ff00, 0xff01ffff0000ff, 0x1ff0101ff0001ff, 0x1ffff01ff0101ff, + 0x101ffffffff0101, 0xff0101ff0101ff00, 0xff000101ffffff00, 0xffffff010101ff01, + 0xff0001010001ff01, 0x10101ff00010001, 0x1000101ff000101, 0xff010001ff0101ff, + 0x1ff00ff01ffffff, 0xffff000101ff0101, 0xffffffff00ff01ff, 0xff01ff000101, + 0xff010000010001ff, 0xff00ffff01ffff00, 0xffff01ff0001ff01, 0xff0000ff010101, + 0xffff0101ff010001, 0x1010100ff01ffff, 0xff010001010100, 0xffff01ff0000ff00, + 0x1ff01ff0100ffff, 0x1ff0000ffff01ff, 0xff00ffff00ff00ff, 0xff01ff0101ff01ff, + 0x10001ffff0101, 0x100ffffff0101, 0xff01ffff01ff00, 0x1ffff000100ff00, + 0xff01ffff0101ff01, 0x1ffff0000ffff, 0xff00ff010001ff00, 0x1ffffffff010001, + 0x1ff010101ff01ff, 0x10100ff00ff01, 0x1ff010101ffffff, 0x101010100010101, + 0xffffffffff0101ff, 0x1ff01ff0100ffff, 0x1ffff01ff010101, 0x1ffffff000101ff, + 0x10101ff01ff01ff, 0xffff01ff0001ff00, 0xff010001ffff0000, 0xffffff000100ffff, + 0xffffff010101ff01, 0xff0101010001ffff, 0xff01ff01ffffff01, 0xff01ffffff0101ff, + 0xffff01ff0101ffff, 0xffffff000101ff01, 0xffffffffff0000ff, 0xffff0001ff01ff01, + 0xff00000101ff00ff, 0xff01ffff01ff0001, 0xffff01ff00010001, 0x1ff0100ff010100, + 0x1000101ffffff00, 0x10101ffff00ff00, 0x1000100010101ff, 0xff0101ff01ff01, + 0xff000001010100, 0x100ff00ffff0100, 0xffff00ffffff01ff, 0x10101ff010101ff, + 0x1ff0100ff0100, 0xff00ffffff000101, 0xffff01ff00ffff00, 0x1ff010101ffff01, + 0xffff01000100, 0xff01ff0100ff00ff, 0xffffff0100000001, 0xffffff0000010101, + 0xff010101ff0000, 0xff01ff00ff01ff01, 0x101ff0101000100, 0x101ffff010101ff, + 0x10000ff000101ff, 0xffffff0101ff00, 0x1ff000001010101, 0xff01ffff010100, + 0x101000000ff0100, 0xff01010101ffff, 0x1010101ff00ffff, 0xff0001010100ff00, + 0xffffff0101010000, 0x100010001010001, 0x1ff0001ff0000ff, 0xffff000000010000, + 0x1ff01ff010000ff, 0xffff00000100ffff, 0xff01ffffffff0100, 0x101ffff0001ff01, + 0xffffff00ffffffff, 0xffffffff01000001, 0xffff01ff00000000, 0xff000100000100, + 0xffff0100ff01ffff, 0x10000ff00ffff, 0x100000101000101, 0x1ffff0000000101, + 0xffff010000000001, 0x1ff0001ffff0100, 0xffffffff01ff0100, 0x101000101ff0100, + 0x1010001ffffff00, 0x100ff0101ff0101, 0xffff01ff00010100, 0x1ff000100ff0001, + 0xffffffff00ff01ff, 0x1ffff0001ff0100, 0x1ff000101ff0101, 0xff01ff00ffff01ff, + 0xff00ff01ff, 0x101ffff00ff01ff, 0x101ff000001ff, 0xff01ffff010100ff, + 0xff00010001ff0001, 0xff01000001ff0100, 0x1000100ff000001, 0x1ff01ff00ffff00, + 0x1010001ff00, 0xff01ff00ff01, 0xffffff0000ff01, 0x1ff00ffff01ff, + 0x1ffff00ff000001, 0x100ff0100ffffff, 0xffff01ff010001ff, 0x10101ff0000ff01, + 0x1ffffff000001ff, 0xff0001ff, 0x1000000ff00ff01, 0xff0001010101ff00, + 0x10100000000ffff, 0x100ff00ff010101, 0x1010100ff000100, 0x101ffff01ff00ff, + 0x1ff00ffffff, 0x1ffffffff0101, 0x100000001ff, 0xffff0001ffff00, + 0xff01000100ff0001, 0xffffffff0100ff01, 0xff01ff0000000000, 0xff0101ffff00, + 0xffff01000101ffff, 0x1ffff01ff01ff, 0x101000000000001, 0x1ff00ff01ff0100, + 0x1ffff0001ff00, 0xff0100ff00ff, 0x101ff0000ff0101, 0x1010100ff01, + 0x1ff000101010101, 0x10000ffff010100, 0xffff01ffffff00ff, 0xffff00ff00010000, + 0x100ff0001ff00, 0xff0001ffffffffff, 0x101ff010001, 0xff00ffff000101ff, + 0x1000001ff0000, 0xff01ff0100ffff01, 0xffff000100010001, 0xff0100ff0100ff00, + 0x100000101ff01, 0x10100010101, 0x1000001ff01ffff, 0xff0000ff000101, + 0xff0000ffff00ff01, 0x1ff0101010001, 0x100ffff0100ff, 0xff01ff01ffff01, + 0x1ffff01ff, 0xff0000ff01ffffff, 0xffff00ffff00ff01, 0xff0000ffff010100, + 0xff01010100000000, 0xff0101ff000001, 0x1010100000100, 0xffff0100ff000101, + 0x101ffffffff0001, 0x100ff01ff000100, 0xffff01ff00ff0000, 0x1ffff0100ff01, + 0x101ff0001ff0001, 0x101ff0000000001, 0xff0101ff01ff0000, 0xff010101ff00, + 0x10101ffffffffff, 0x10000ffff00ff01, 0xff010001ff0100, 0x1010100000000ff, + 0xff01ff01000100ff, 0x1ff0101ff010000, 0xff01000100ff0101, 0x100ffff010001, + 0xffff0000000101ff, 0xff010000ff000000, 0x101ffff00ffff, 0x101010101, + 0xff0100010101ffff, 0x1ff01ff0101ff, 0x1ff01ff0101, 0x1000101ff010100, + 0x1ff0100010100, 0x1000001ffff00, 0xff0001ff00ff00, 0x100010101ff0000, + 0xff00ff0000ff01, 0x10101000000ffff, 0x100000001010000, 0xff0001ff010100ff, + 0x101ff01ff01ff01, 0x1ff00ffff0001, 0x1ff0000ff0100, 0x10000000100ffff, + 0x1ff01ff01ff, 0xff01ff01000101, 0xff000101ffffff, 0x100ffff00ff00ff, + 0x100ff0101ffff00, 0xffff010100ff01, 0x1ff00ff00ffff, 0x1000100ff010001, + 0xff01000000000100, 0xffffffff0001ffff, 0xff00010100000000, 0x10000ff0001ff, + 0xff000101ff000100, 0x1ffffff01, 0x1000100010001, 0x100ff01ff010001, + 0xff01010000ff01, 0x100010000ff01, 0x1ff0101010000ff, 0xff0101ff010001, + 0xff00ff01ff000100, 0xff00000101ff00, 0x1000100ff00, 0x100ff0100010100, + 0x10001ff010001ff, 0x1ff010101ff00, 0xff00ffffff000101, 0x1ffff000101ff00, + 0xff0000000100ff01, 0x10001ff01, 0xff010001ff010101, 0x1000000000000ff, + 0xffff0101ff010100, 0x1ff00ffff000101, 0xff0000010101, 0xffff01ff010000, + 0x1ffff0001010101, 0xff01ffff00ffff00, 0xff0001010100ffff, 0xff000101ff0100, + 0xff01000101010001, 0x101ff0101ffff, 0x1ffffff01000001, 0x1ffffffff01ff00, + 0x1ff000001ff0100, 0x1000101000101ff, 0xff0101ffffff0000, 0xffff000100ff0001, + 0xffffffff00ff0101, 0x10000ffffff0000, 0xff0101ffff, 0x1000100ff010101, + 0xff01ffff00000100, 0x101ff000001ffff, 0xff01ffffff0000ff, 0xffffffffff0100ff, + 0xffff0100010101, 0x1010101ff010000, 0xff000100ff00ff00, 0xffff0100000001ff, + 0xff0100ffff010101, 0x1ff01ff01ff00ff, 0xff0001ff000100, 0x10001ff010100ff, + 0x101ff0001ffff01, 0xff00ffff0101ffff, 0x10101ffff00ff, 0x101ffff0101ff01, + 0xff01ff00ff01ff01, 0xff0100ff0001ffff, 0x1000100ff000101, 0x10100, + 0xff0000ff00ffff01, 0xffff000100010101, 0xff00010001ff00ff, 0x101010001000000, + 0xff00ff0101ffffff, 0xffffffffff01ff01, 0x101ff00010101, 0xffff0101000001ff, + 0x10100ff00ff0101, 0x10101ffff00ffff, 0x100ff010101ff, 0xff000100010100ff, + 0xff00010101ff00ff, 0x100ffffffff0000, 0xffff00000000ffff, 0x100ff0101ff00ff, + 0xff010001ff0000ff, 0xff00ff01ffff01, 0x1ff00ff0001, 0x1ff01ffff00, + 0xff01ff01000101, 0x101ff00ff00ff00, 0xff00ffff00ff0101, 0x101010000ff0000, + 0xffff0000000001ff, 0x1000100ff0100, 0xffff00ffff00ff, 0xffffff01ffffff01, + 0x10101ff00ff00ff, 0xffff00ff01010100, 0x10000ff00010100, 0x1ffff010100ffff, + 0xffffff01010100ff, 0xff000100ffffffff, 0x1ff01000100ff00, 0xffffff00010001, + 0xffff00010101ff01, 0x10001ff01ff00, 0xffffffff00ffffff, 0xff010100010001, + 0xff0000ff01000001, 0x1ff0000010001, 0x10100ff010100, 0x10101000001ffff, + 0x101000100ff, 0x1ff0000ff000100, 0x1000000ff000100, 0x101010100ff00ff, + 0xff01ff01000100, 0xff000001000001, 0x100ffffffff0000, 0xff01ff01ff01ff01, + 0x100ffff00ff, 0xff01010101ffff00, 0xff00ffff00ff01ff, 0x10001ff01010001, + 0x1000001ff0000ff, 0x1ffff0101ff00, 0xff000101ff0000, 0xffffff01000101ff, + 0xff01ffffffffffff, 0xffffff0100ffffff, 0x10000000001ff01, 0x1ff0000ff00ff01, + 0x100ffffffffff00, 0x10100ff000000ff, 0x10000000101, 0xff0100010101ff01, + 0x10001ffffff01, 0xff0000ff01010001, 0x101000001ff0001, 0x1ff00000001ff01, + 0x10100ff01010101, 0x1000001ff010001, 0x1ffff0100ffff, 0xff0101ffffffffff, + 0x1010101000100, 0xffffff000101ff, 0xff00ff01000100, 0xffff00ff00ffff, + 0x100ff000000ff00, 0xff000101ff, 0xff01000100ffff, 0x100ff01ffff00, + 0x1ffffffff0101, 0xffff000001000001, 0x1ffff0000000000, 0x10001ffff00ff00, + 0x1000000ffff0000, 0xffffffff010101ff, 0x100ff0101ff, 0x10000000101ff, + 0x100ffff0100ffff, 0x1ffff0000, 0x1010000ffff, 0x100010000ff01, + 0xff010001ff000000, 0x10001ff01ff0001, 0x101ffff00ffff01, 0x100ff0100ffff00, + 0x1000000ff, 0x1ff000101, 0xff00000000000001, 0x10001ff01ff, + 0xff01000000000100, 0xff00000000ff0100, 0xff00000000ff00, 0xffff0000ff00, + 0xff01ff01, 0xff00000100ff0100, 0xff0100ff00ffff, 0x100000100ff0000, + 0xffff01ff000000ff, 0xff00000101ff00, 0x10000ff01010100, 0x101ff00000000, + 0xff000000010100, 0xff010101000000, 0xff000000ff000100, 0x1ff00ff00ffff00, + 0x100000000, 0xff00ff0100000001, 0x1ff000001000001, 0x1000001000000, + 0x1ff0000000101, 0x10000000000ff, 0xffffff, 0x1ff010000, + 0x100000000000000, 0x100ff0000010001, 0xff00ffff0000, 0x100000100000100, + 0x1ff000000ff0000, 0x1000000000000, 0xff01010000, 0x100ff000000ff, + 0x100ff0000000100, 0x10001010000ffff, 0x1ff000100ffff00, 0x100000000ff0101, + 0x10000000101ff01, 0xff0000000000, 0xff000001010000ff, 0x1000000ff010001, + 0x101000000ff0000, 0x1000001ff, 0xffffff010000, 0xffff000001000100, + 0x100ff0100010001, 0x1ff, 0xff01000000ffff00, 0xffff00ff0001ff00, + 0x10000000101ff, 0xffff00ff00ff00, 0xffff0100000000, 0xffff000100ffffff, + 0xffff000000000101, 0x100ff01010000, 0x100000000ff, 0xff00000101010000, + 0xff00ff0001000001, 0xff000100ff000000, 0xff000100ff, 0xff00ffff00000000, + 0x100010101ff0100, 0xff01000001000001, 0x101ff00010001, 0xff0000ff00000000, + 0xff0000, 0x10001000000, 0x1ff010001010000, 0xff00000000, + 0x1010001ff0000ff, 0xff00ff00000000ff, 0x100ffff0100, 0x1000000, + 0x100000101ff00ff, 0xff000100000001, 0x1ff01000000, 0xff0001ff00ff0001, + 0xffff00000101ff00, 0xff00000100000001, 0xff01, 0x100, + 0x101000000010001, 0xff0001ff, 0xff01ff00ffff01, 0xff0000ff00000100, + 0xff0100ff00ff00, 0xff00010000000000, 0xffff0001ff0000, 0x1ff0001ff0000, + 0x1000000ff000000, 0xff0001ff0101ff00, 0x1000000, 0x100ff0001000000, + 0xff00ff000100ff, 0xff010001000000, 0xff0000000101, 0x1ff00010100, + 0xff00010100ff00ff, 0xff00010001000000, 0xff0001ffff0101, 0xffff010000ffff, + 0x1000001ffff0100, 0x10100000000ff00, 0xff0100ff00000000, 0xff000000010000, + 0x100000000ff00, 0x1ffff, 0xff000000ff0000ff, 0xff000000010001, + 0xffffffff00ff01ff, 0x100ff00ff00, 0x101000000, 0x100, + 0xffff0000000000, 0x1000100ff0000, 0xffffff, 0x1ff000000000000, + 0x101ff000100, 0x100000100ff0000, 0xff00ff, 0xff, + 0xff00ff0000ff0000, 0x0, 0x1ff0101000000, 0xffffff0000ff0001, + 0x1000101010000, 0x101ff0100ff00ff, 0x1ff000001ff, 0x100000000000000, + 0xffff0000000000ff, 0xff00000001000100, 0xff00000000000000, 0x1000000000000, + 0xff000000ff0101, 0xff00ff0000000000, 0x1ff0100ff0100ff, 0xff00000100ffff00, + 0x100ff0101010001, 0x1000001ff000100, 0x1ffff01010000, 0xff00000001ff00ff, + 0xffffff01010000, 0xff000000, 0x100ff01ff0001ff, 0xff01000100ff00ff, + 0x1ff010100010100, 0xff01010000ff, 0x1, 0x1010001ff00ff, + 0x100000000, 0xff0101ff00010000, 0xff00ff00ff, 0x101ff00ff00, + 0x101000000010000, 0xff00000000, 0x100000100000001, 0xff00000000, + 0x100ff01ff000000, 0xffff000100000000, 0x100000000, 0xffff0001000000, + 0x1ffffffff0101, 0x10000ff0000, 0x10100010000, 0x100ffff00, + 0x1ff0000ff, 0xff00010000000001, 0xff01ff0000000100, 0xffff0000ff00ffff, + 0x101ff00ff01, 0x1ff000000000101, 0x100ffff01, 0xff00ff00ffff00, + 0xff000100010001ff, 0x100000000, 0x10001ff00ff0100, 0x101ff01010000, + 0xff010000ff000000, 0xff000000000101, 0x1010101ffff0000, 0x0, + 0xff000100010000, 0x100010000ff00, 0x10000ff0100, 0xffff00000100ffff, + 0xffffff00, 0x10100ff0000ffff, 0x1ff00, 0xff00000001, + 0x101ff0000010100, 0xff00ff0001000100, 0x101000100010000, 0x10101000001, + 0x1ffff0001, 0xffff010100000001, 0xff0101ff01000001, 0xffff000100ff00ff, + 0x100ff010100ff00, 0x0, 0x10101ff00, 0xff00ff01ff01, + 0xffff000100000100, 0xff010000ff01ff, 0x1000000010100ff, 0xff00010100000001, + 0x100000000, 0x10001ff, 0xff01ffff00ff0000, 0xff00ff0000ffff, + 0x1000000ff0100ff, 0xff01, 0xffff0001, 0xffff000000ffff, + 0xffff010000000101, 0x1010001000000, 0x1000000000000, 0xff00000001000000, + 0xff00ffff01000000, 0x0, 0xff0100ffff00ff00, 0xffff01000000ff00, + 0x10101ff00ff, 0xff00000001000001, 0xff0000ff01010000, 0xff0000ff00000000, + 0xff0001ff00000000, 0x101000001ff00, 0x1ff000000010100, 0xff000000ffff, + 0x100, 0xff00ff000000, 0x10101000000ff, 0x101ff0100, + 0x101000000, 0x100000100010001, 0xff0001ff00000001, 0xff00000000ffff01, + 0xff0000ffffff0100, 0x101010101ff0001, 0xff01ff0100010000, 0xff01ff0000ff00ff, + 0x1ff00010001, 0x100ffffff01ffff, 0x100ffff00ff0001, 0xff01ff0000010000, + 0xff0001000100ffff, 0x10100000000ff00, 0x10100ffff, 0x1ffffff00000001, + 0x10000ff00010000, 0x10001000100, 0x1000100000100ff, 0x101ffff0101ff00, + 0x100000100010100, 0xff00ff0000000101, 0xff0001ffff000100, 0x101ffff00000001, + 0xff0001ff000000, 0x1ff0001010000ff, 0x1ffffffff000101, 0xff00010101ff0001, + 0xff000000ffff0100, 0xff01ff00ff010001, 0x1ff0000000000, 0xffff0000ff010101, + 0xffffff01000101ff, 0x1ffff00ff01ffff, 0xffff000000ff01, 0x101ff01, + 0xffff01ff000000ff, 0x101000000000000, 0x1ff0100000100ff, 0xff00010100000000, + 0xffffff01ff00, 0xff0100ff00, 0x10000ff010000, 0x10000ff0100ffff, + 0x1ff00ffff, 0xff000000000100, 0x100ff00ff00, 0x1ff000001000000, + 0xffff0001ffff, 0xff0000, 0xffff000000, 0xff01000100000000, + 0x1ff000101ff0100, 0xff00000001010100, 0x101000001000001, 0xff00010000000001, + 0xff010000ff00ff00, 0xff00000101ff, 0x10001ff, 0xff00000100, + 0xff, 0xffff0100ff0100, 0x100ffff, 0x100000000010100, + 0xff0000ff00ff01ff, 0x1010000000100, 0x1ff000100ffff00, 0x1000000ff000000, + 0x10000000001ff01, 0xff0001ff010000, 0xff0000000000ff, 0x1ffff, + 0x1000000ff0000, 0xffff000100000101, 0x10000ff000000, 0xff00010000, + 0x100000000000000, 0x10001000000, 0x100010000000000, 0x1ff0000010000, + 0xff0100ff0100ff, 0xff0000ff0000ff, 0x1000000ff, 0x1010100ff0000ff, + 0x10000ffffff00ff, 0x1010101ff0000, 0xff000100ff010100, 0x100ff0000, + 0xff000000ffff0001, 0xffffffff010100, 0xff00ff0101000100, 0x1ffffffff00ff00, + 0xff01ff0101000000, 0x1ff000000ff00, 0x10100010000, 0xffff000000000000, + 0xffffff0001000000, 0x1ffff0101, 0xffffff0000ff, 0x100ffffff00, + 0x10001000100ff01, 0xff00ffff01000000, 0xff0001ff00, 0xffff01ff00ff01, + 0x100ff0100010001, 0x1000101010000, 0x10001ff000000ff, 0x1ff0001000000, + 0x100000000000101, 0xffff00ff000000, 0x1ff0100ff010001, 0xff0100ff00ffffff, + 0x10100ff01ff, 0x100ff0001ff00ff, 0xff000100ffff01, 0x101000101ffff00, + 0x100000000ffff01, 0xff01000101010000, 0x1ff0100ff000000, 0xff000001ff00ff00, + 0xff01000100000101, 0x1000101ff00, 0x1ff0100000001, 0x100ff01010100, + 0xff01ff0000, 0x100010000ff00, 0xff0000ff0001ff01, 0xff0000000001ff01, + 0x10000ff010000, 0x100000000ff, 0xff0000ff, 0xff00000100ff0100, + 0xff00010001ffff, 0x100000100000001, 0xff00ffff0000ffff, 0xffff00ff0100ff, + 0x1000001000101ff, 0xff0000ff01, 0xff010000ff01, 0xffff01ff00ff0000, + 0xffff0000000001ff, 0x10000010001, 0x10100ff000101, 0xff01000000010000, + 0xff00ff01ff00ff01, 0xff0000ff, 0xff00ffff00, 0xff00000000010000, + 0xffff000101ff0000, 0x100ff01, 0xff0001ff00000001, 0x1ffff0000ff00, + 0xff0000ffff01ff00, 0x1000000ffff, 0x1ff00000101ffff, 0xff0100ffff0000, + 0x101000000ff0100, 0xff0000ff0101, 0xff0001ff00000000, 0xff010000ffff00, + 0x101ff0100010000, 0xff00010001010101, 0x101ffff000001, 0xffffffff00ffff00, + 0x10100000001ff, 0xffff000100, 0xff00ff00ffff01, 0xff00ff0001, + 0xffff00ff000100ff, 0xff00ff01ffff00, 0xffff00ff0000ff01, 0xff00000001ff0100, + 0x10001000100ff, 0x10000ff01ffff00, 0x1000001, 0x1010001ff00ff, + 0xff01ffff01ffff01, 0xff01ffff00010000, 0xff00ff01ff010000, 0xffff01010001ff, + 0xff00ff000100ff, 0xffffff00000100, 0x1ffff01ff0000, 0xff0100ffff01ff, + 0xff0100ffffff00, 0xff00ff0000000000, 0xffffff01ff000000, 0xff0000ff0000ff00, + 0x100ff00, 0x101000000000101, 0xffff0100000100ff, 0x101ff01ff000101, + 0x10100ff0001, 0xff000000ffff0100, 0xff000100ff0100ff, 0xff0000ff0101ff, + 0x1ff01ffffff, 0xff01ff000001ff, 0xff00010101000000, 0x1000101ff01ffff, + 0x1ff01010100ff01, 0x100ffff00ff0000, 0xff0001ff00ff00, 0x1010100ff000000, + 0xff00ffffffff00, 0xffff010101010000, 0xffff000001ff0000, 0xffff01ff01ff, + 0x101ff0000000000, 0xff010001ff0000ff, 0x1ff01ffff010000, 0x101ff01010000ff, + 0xffff00ff, 0x1ff0101ffff, 0xffff0101000000, 0x1ffff000001, + 0xff0001ffff010001, 0xff0100010100, 0x10100ff0100ffff, 0x1ff0101010000, + 0xffff0001ff000000, 0x100010101, 0xff0001ff00ff0000, 0x1000001ff010000, + 0xff0001ff00010101, 0xff000100ff00ff00, 0xff0000ffffff00, 0x100000000000100, + 0xffffff010101, 0xffff0101ff0000ff, 0xff01000000ff00ff, 0x1ffff0000010101, + 0xff000001ffff, 0xffffff0100000000, 0xff01ffffff010100, 0xff00ff01010000, + 0xff00ff01ffff00, 0x1000100ff01, 0x1010100ff01ff00, 0xff00ff0101010101, + 0xff00ff00ff00ffff, 0xffff010100010001, 0xff000001ff0000ff, 0xff0001ff01ffff, + 0xffffffffff0000, 0x101ff010001ff00, 0xffffff000000ff, 0xff0001ffffff01, + 0xff0001ff00010000, 0xff00ff0000ff0000, 0x1000000000000ff, 0xff0000ff010100ff, + 0x1ff000000ffffff, 0xff0101ff01010000, 0x1ff000101010100, 0xff00000000, + 0xff00010000000000, 0xffff01ffff000100, 0xff, 0xff01000101ff00, + 0xffff0100010100ff, 0xff0101ffffff0101, 0xff00010000ff01ff, 0x100ff0101010001, + 0xff0000ff01, 0xffff00000000ff, 0xffff0100ffff01, 0xff00000000, + 0xffff00ffffff00, 0x1ffff00ff0001ff, 0x101ffff0001, 0x1ff000101000000, + 0x10000000101, 0x100ff0000ff0101, 0xff01010100ffff00, 0xffff000101ff, + 0x1ff0000000000ff, 0x1010100, 0x1ff01ff01, 0x10000ff00000100, + 0xff010100010000, 0x101ffffff01ff01, 0x100010100010000, 0x101ff0000ff0000, + 0x1ff010100000000, 0xff00ff00010100ff, 0xff0001ff00ff00ff, 0x100010001000000, + 0xff01000000000100, 0x1ffff01000000ff, 0xff00ff0001ff, 0x10001ffff00ff01, + 0xff01000100000101, 0x101ff000000ff, 0xff01000001010000, 0xffff00000100ff00, + 0xff0100000001ff01, 0xffffff0000ff01ff, 0xffff01ff00010101, 0x101000001ff0100, + 0x1ff00010100ff00, 0xffff0001ff, 0x1ff0101000100, 0xff0000000000ff, + 0xff000001ff000100, 0xff010001ff00, 0x1ffff01ff01ff01, 0x1000100ff0101ff, + 0xff0101ff000100ff, 0x1ff000001, 0xff0100000101ff, 0xff0001ffff000000, + 0xff010100ffffff, 0xff00ff01000100ff, 0xff0100ffff01ff00, 0x10000000001ff, + 0xff00000001010001, 0xff0101000101ff01, 0xff01000001ffffff, 0x1ffff00000100ff, + 0x100ffffff010001, 0xff0000ff0100ff00, 0x1ffff0100010000, 0xff0000ff01, + 0xff000000ff0101ff, 0x10000ff0001ff, 0xff00000101ffff00, 0x101010100ff00ff, + 0x1ffff0001010001, 0x100ff00000001, 0x101ff0100, 0xffffff00000000, + 0x10000ff00ff00, 0xff0100ff01000001, 0x1ff00010000ff00, 0xff01ff01ff010101, + 0xff01000000, 0xff00ff0000, 0x100ff0100ffffff, 0x1ff000001ff01ff, + 0x1010000ff0000, 0xff01ff01010001ff, 0x1ff01ff010101ff, 0xff0100ff000100, + 0xffff000001, 0xff01ff01ff000101, 0x1ff0101000100ff, 0x10000ff00, + 0x100ff0000ffff01, 0x1ff0000ff000000, 0x1000001ffff0001, 0xffff0000000101, + 0x100000101010100, 0xff00ff010000ff, 0xff0100ffff0001ff, 0x100ffff00ff01, + 0xff0101000001ff00, 0x10100010101, 0x10000010000ffff, 0xff000001ff0000ff, + 0xffffff01000000, 0xff01ffff010001, 0x100ff0100ff0100, 0x1010101ff01ff00, + 0x101ff01010001ff, 0x1ff0001ff0000ff, 0x100ff0000ff0001, 0x101ffffff010101, + 0x100000101ff0100, 0xff0100ffffffffff, 0x1ff0001ffffff00, 0xff010001ffff01, + 0xff000001ffffffff, 0x1ff01ff0101ffff, 0xffffff0000ff0101, 0xff00ff0100010001, + 0x1010000ff000001, 0x1ff00010000, 0xff010100ffff01, 0x1000101010000, + 0xff010100010101ff, 0x101ff0101ff, 0x100ff00ff01ff, 0xffff00ff0101ff, + 0xff000000ff00ff, 0xffff00ff00ff00ff, 0xff00ffffff0100, 0x10000ff000000, + 0xff01ff00ffff00ff, 0xff0001ff01ff0101, 0xffffff00ffff01, 0xff010000010100, + 0xff0101000100ff00, 0x101010100ff0000, 0xff010100, 0x1ffffff00010100, + 0x10000010000ff, 0x10100ffff0100, 0x101ff010000ff, 0xff01010101000101, + 0x101ffff01, 0xff00ffffffff0001, 0x100ff00ff010000, 0xff0001ff000000, + 0x1000100, 0x1ff000100ff01, 0xff00ff00ff01ff00, 0x1010100010100ff, + 0xff0101ffff00ff, 0x1ff01000000ff, 0xff01ff000100ff00, 0xff00ffff01010001, + 0x10000ff000001, 0x1ff00ffff000001, 0xffff01ffff0101, 0x1ff00000100ff01, + 0x1ff010000ffff00, 0x10101ff0100ff00, 0xff000001000001, 0xffff00000000ffff, + 0x100ff00000000ff, 0xff0100ff000100ff, 0x1ff0101ff000101, 0xffffffff01ff00ff, + 0x101ffffffff00ff, 0xff00000001ff01ff, 0xffff000001ff00ff, 0xff0001ffff010101, + 0x1ff, 0x101000101ffff01, 0x1000001ffffffff, 0x100000001000001, + 0xff00ffff00010001, 0xff00ff00ff0100ff, 0x10001ff01010101, 0xffff00ffff0000ff, + 0x1ffff01ff010000, 0x100ffffffff0100, 0xff0001ff0001ffff, 0xff01000101ffffff, + 0x1ff0100ff000100, 0xff01000100000100, 0xffff0101ff, 0xff000001ffff00, + 0x10100ff01010100, 0x10101000001, 0x1ffff0000000001, 0xff00ffff01, + 0xff00010101ffff, 0x1000100ff0101, 0x1ff000001000000, 0x1010001000101, + 0x10100ff00ff, 0x100ff010001, 0xffff000001ff00ff, 0x10001000000ff00, + 0x100010001ff01ff, 0xff010001ff0000, 0x10001ff010000, 0x1ff0101ff00ff, + 0xff0000ff0000ff01, 0xff01ffff01ffff, 0x1ffff010100, 0x10001ff010100, + 0xff00ff00ff00ff, 0xffff01, 0xff01ffffffff0101, 0x10100000100ffff, + 0xff00000100ffffff, 0xffff01000001, 0xffff010100000001, 0x1ffff00ff010101, + 0x1ff0000ff000001, 0x10100ffff01ffff, 0xffff01ff00ffff, 0xff000001000000, + 0x10001ff000101ff, 0x10001ffff010100, 0x100ff00000100, 0x1ff00ff01ff, + 0x10000ff000000, 0x1ff0100010100, 0x10000ffff010101, 0xff0001ff0000, + 0xff000000ff0000, 0x100ff010000, 0xffff00010001ffff, 0xff00010100ffff00, + 0xff01ffffff000000, 0xff00ff00ffffff, 0x100ff00010101, 0x100ffffff010000, + 0x100000101ff00, 0x10100000001ff00, 0xff01ff0000ff, 0xffff0000, + 0xff000100ffffff00, 0xffff00ffff00ff01, 0x10000ff01ff0100, 0xff00ffff0000ff, + 0xff0000ff0001ffff, 0xffff00010001, 0x101ff0001010100, 0xff01ff01ff01, + 0x10100000000ff, 0xff0000ffffff0001, 0x1000000ffff00ff, 0x1ff010000000100, + 0xff0000010001, 0x1010000ffff0000, 0xff01010000000001, 0xff010000000000, + 0xff000000000000, 0xff0000ffff0100ff, 0xff00ff000100ff, 0xff00ff00000001, + 0xff0100ff01ff01ff, 0xff00ff0001000101, 0xff0101ff0000ff, 0x1010000000101, + 0x10001010101, 0x10000ffffffff00, 0xffffff00000100, 0xff000000000101ff, + 0xff010101010100ff, 0xff00ff00ff010000, 0x101ff0101010001, 0x1000100010001, + 0xff01ffff0100, 0xff010001ffff0000, 0xff010000ff00ff, 0x100, + 0x1ff00000001ff00, 0x100000000000001, 0x100ff0001000000, 0x1ffff010101ff00, + 0x100ffff01ff01ff, 0xffffffff00010000, 0xff000101000100, 0x1ffff, + 0xff000001010100, 0x101ff00010101, 0x1ffff010000ff00, 0xff00ffff00000100, + 0xff00000100ffff, 0xff00010000ffff01, 0xff01ffffffffff01, 0x100000100ffff01, + 0xff01ff00ff00ff00, 0x100000001ff00ff, 0xff0001ff0101ff00, 0x1010001010100, + 0xff0001ff01ff01, 0xff0001ff0100ff, 0xff00ff01ff0100, 0x100010100ff00, + 0xff00ff0001000100, 0x1000101ffffffff, 0xff00ff0100ff0100, 0x10100ff00000100, + 0x1000001010100, 0x100ffff010101, 0xffffff01ff0000, 0xff00ff01010001, + 0xff00ff01010000, 0xff000001ff000100, 0xff00ff01ff000100, 0xff000000ff010001, + 0xffffff00010000, 0x1010100ff00ffff, 0xff000101ff00ff, 0xff0101ff00ff00ff, + 0x10000ff00ffff00, 0x10000010101ff00, 0xffff0000ff010100, 0x1ff01ffff000100, + 0x100000101000100, 0x10100010000, 0x1010101ff010000, 0x1ff010100ffff, + 0xffff0101010000, 0x10101ff01ffff, 0x1ffffffffff0001, 0xffff00ff0101ff, + 0xff00ffff000000, 0xff00ffffff0001, 0xffffff01010100ff, 0x1000001010001, + 0xff01ff01010101ff, 0xffffff0001ff0000, 0xffff0100ff00ffff, 0x10000000001ff01, + 0xff01000100000100, 0x1010001000000, 0xff0101ff010100ff, 0x1ff000000000001, + 0xffffff0101ff, 0xff00ff00000100, 0xff00010100ff01, 0xff010000ffff01ff, + 0x10101000101ff, 0xff0001ff01ff0101, 0xff010001000001, 0xff0000ff0001ff00, + 0xff00ff010100ff00, 0xff01ff010100ff00, 0xffffffff01ff0001, 0x10000ff0001ff01, + 0x10000010001ff01, 0xff01ff01ff01ff01, 0x10001ff0001, 0x10001ff010101ff, + 0xff000000010000ff, 0xffff00ff01ff00ff, 0x1ff000100010100, 0xffff010000010101, + 0x10100ffff000001, 0xff00000000ff00, 0xffffff0000010100, 0xff0100000101ff00, + 0xff000100ff01, 0x10001000000, 0xff0000ff00ffff, 0xff0000ffff01ff01, + 0x10100ff000000, 0xffff000000010001, 0xffff0100ff000000, 0x100ff01000001, + 0x101010101ff0100, 0xffff010001010001, 0x1ff01ff00ff0100, 0x1000001ff010101, + 0xff0001ffff010100, 0x101ffff0000ff00, 0xffff010101010100, 0xffff010000010100, + 0x1ff01ff0001ff00, 0x1ff0101ff000000, 0xff00ffff0100ff00, 0x101ffffffff0000, + 0xff01ff00000001, 0xff00ff00ff0101, 0x10001ffff000001, 0xff01010100ff01, + 0x10001010000ff00, 0xffff0100ff010100, 0x1ff01ffff00ff01, 0xff010100000100, + 0xffff0001ff00, 0x10000ff00ffff00, 0x100ffff00010000, 0xff01000001ffff00, + 0x1010001ff0001, 0x1ff0001010000, 0x101010100ffff01, 0x101ffff000100ff, + 0xff010000010000ff, 0xff0000ff010001ff, 0x100, 0x10100ff00000101, + 0x100ffffff0000, 0xffff000000ffff, 0x1ffffff01ffffff, 0xff010000000001, + 0xff010100ff010000, 0xff00000001010000, 0x10101010101, 0x100ffff0100ff00, + 0x1ff0000ff010101, 0x100010101010100, 0x100ff010000ffff, 0x1010100ff0100, + 0x101010100ff01, 0x1ffff0001010000, 0xffffff0000000001, 0x101ff0100000001, + 0xff00010000ff0001, 0x1000101010001, 0x1ff0001ff0000, 0x1ffff01ff00, + 0xff01ff000100ff, 0x10000ffff0000ff, 0xffffff0101ff0000, 0x1ff0000ff, + 0x100ff0100ff01, 0xff00ff0101ff01ff, 0x1ffff01010000, 0xff0000010001, + 0xff000101ff0100, 0xffffff01ff01, 0xff010000ff01, 0x101010000010100, + 0x1ffffff000000ff, 0xff00000001ff00, 0xff010001010101, 0x1ff0001010000, + 0x1ff00ffff000101, 0x10101010100ff01, 0x101ff0000000101, 0xff000001ffff00, + 0x10101010001, 0x10101000100ffff, 0xff000001ffffffff, 0xffff0001ff01ff00, + 0x10001ff010001ff, 0xff01ffff0101ffff, 0xffffffffff0101ff, 0x1ff0101000101, + 0xff00ffff00ff0000, 0xffff01ff01000100, 0xff00ffff01010000, 0x1000101ff000101, + 0xffff0001ffff0101, 0x10101ff01ffff, 0xff01ffffff000001, 0x1ff01ff0100ff01, + 0x10001ff0100ffff, 0x1010100ff000000, 0x101ffff00ff00ff, 0x1ffff00ff01ff, + 0xff01ff01ffff00ff, 0x10100ff00000001, 0xffff01010001, 0x1ffffff00010001, + 0x1ff0101ffff0100, 0x10101010101, 0x100010001ff00ff, 0x100010100ff00ff, + 0xff010000ff01ff00, 0xffffff01ff0100, 0xff00ffffff010001, 0xffff00ffff01, + 0x101010100ff0101, 0x1ff0100010101, 0x101ffff0001ff01, 0xff000100ffffff00, + 0xffff0000010100ff, 0x100ff01ffff01ff, 0xff00ff010101ff, 0x10101ffff010100, + 0x10100ff00ff0000, 0xffff01ffff00ff, 0xff0100ff010101ff, 0x101ff00ffff00, + 0x1ff01ff010101, 0x101000000010000, 0x1ff010101ffff00, 0x1ff01ff01000100, + 0x10000ff0101ff01, 0x10101ff010100, 0x10000010100ffff, 0x101ffff01ff0100, + 0x10101ff010101ff, 0xffffffff01ff0100, 0xff01000000ff0001, 0x1010100ffff01ff, + 0xff0100010000ff01, 0xff0100010101ff01, 0x1ff01010001ff00, 0xffff0001ff01ff00, + 0x1ff00ff0101ffff, 0x10100ff0101ffff, 0x1ff01ffff0101, 0x10101ff0101ff, + 0xffff000001000100, 0xff00, 0x100000101ff0100, 0xffffffffffff00, + 0x1ff01ff0100ffff, 0x10100ffff010000, 0x1ff000000ff0100, 0xff0100ffff, + 0xffffff0101ff, 0x100ff0100ff00, 0x1ff00ff0100ff00, 0xffff00ff01010000, + 0x101ff0100000000, 0x101010001ff01, 0x10100000001, 0xff01ff0000ff, + 0xff000001ff01ffff, 0xff00ff01ff, 0xffff00ff00ffffff, 0x101010100000101, + 0xff010000ffff0001, 0x10101ff00ff0100, 0x1ff010100ffffff, 0x1ffff00010100ff, + 0x10001ffff0000ff, 0xff0000ff0101, 0xff00ffffff000001, 0x1ffff010100, + 0x10100000000ff, 0xff0100ff010101, 0x1010001ff0100ff, 0xff000100ffffff01, + 0x1ffff01ff00ffff, 0x10100000000ff, 0xff00010000ffffff, 0x101ff0001000000, + 0x10001ff0101ff00, 0x100ff01ffff01, 0xff0000ff00000100, 0xff00010001ff0000, + 0x101000100ffff, 0x10001ffff01, 0x1000100ffffff01, 0xffff, + 0x101010000ff00ff, 0x100ff0000010101, 0x1ffff000000ff00, 0xffffffff000100ff, + 0xff01ff0000ff00ff, 0xff0000000000, 0xffffff0101000100, 0x1ff0000000101ff, + 0xff01000100ffff00, 0xff000001ff000101, 0x1ff010000ffffff, 0xffff0001ff01, + 0x1ffff01ff0101, 0xff01010101ffff01, 0x1ff010101010000, 0xff00ff0100ff00ff, + 0xff01ffff000101ff, 0xff01000001ff01ff, 0xff0100ffff00ffff, 0x1ff000000000100, + 0x10000ffff0100, 0xff0101ff01010001, 0x1000001, 0x1ff000101000101, + 0xff0000ffff000100, 0xffffff000100ff01, 0xff0000000000ff, 0xffffff010001ff01, + 0x1ff0001010000, 0xffff0001ff00ff, 0xff0000ff010001ff, 0x10100ff0001ff01, + 0xff00000100000000, 0xff0000ffffffff00, 0xff00ffff0001ff01, 0x1ff010100010000, + 0x100010100ff00, 0xffffff010101ffff, 0xffff000101ff0001, 0x10000010100, + 0x1ff010101ff0100, 0x10101ff010100, 0xffff000000ffffff, 0xff000101000101ff, + 0x1ff01ff01010001, 0x1ff00ff0000ff, 0xff0001ffff01ff, 0x1ff01ff0101ffff, + 0x101ff010001ff00, 0x1ff00000100ff, 0xff000001ffff00ff, 0xff0001ffff00ffff, + 0xff0100ff0001ff, 0xff01000100ffff, 0x1ff0001ff01, 0xff0101000101ff01, + 0x1ffff0101ff01, 0xffff0101ff, 0xff00ffff01ffffff, 0x10000ff01ff00ff, + 0xff00000100000000, 0xffff010001ff0001, 0x1000000ff0101, 0xff0100ffffff01, + 0x100ff01ffffffff, 0xff01ff0100ff, 0x1ff00ff00ffffff, 0xff00010101ff00ff, + 0x100ff00ff000100, 0x101ff01ffff0100, 0xff00ffff01ff01ff, 0x1ffff000001ffff, + 0x101ffff01010101, 0x1ffff00ffff00, 0x101ffffff0100ff, 0xffff01000100ff01, + 0xff01ff0101010001, 0x1ff000001010000, 0x101ffffffff01ff, 0x1ff010000ff01, + 0x1ff000001ffff, 0xffffff00ff01ff, 0x101010001ff00, 0x1000001ff0000ff, + 0x10001, 0xffff0001ff010000, 0xff01010100ffff00, 0x10100ffff0101, + 0xff00010000ffff00, 0xff01ffff010000ff, 0x1ffff00ff01ff, 0xff0000ff00000100, + 0x1ffff0101ffff01, 0xff01ff00ff, 0x100000101ff00, 0xffffff00ffff00, + 0xff000000ff0101, 0xff00000101000100, 0x101ff000000ffff, 0x1ff01ff01010001, + 0x101000000ff0100, 0xff01ff00ff000100, 0x10001010100ffff, 0xff01ffff00ffff00, + 0xffffff0100, 0x1000000ffff00ff, 0x1000100ffffff, 0x1ff01ff01010000, + 0x1000101ff01, 0x1000100ff0100, 0x1ff0001ff010101, 0x1ffff01ffff0100, + 0x1ff010000010000, 0x10101ffff000101, 0x10000000101ff, 0x1ff0000ff01ff, + 0x101ffffff000001, 0x1ff01ffff01ff01, 0xff00ff00000101ff, 0x101000101ff0001, + 0xff00ffffff00ff00, 0xff000000ff00ff, 0xff0000010000ff, 0xff0000ffffffff01, + 0xff0100ff00000101, 0x1ff0100ff000100, 0xff00ffff0000, 0x10101ff010000, + 0x1ff01ffff000001, 0xffff01010001, 0x100ffff00ff0000, 0x101ff01010001ff, + 0xff0000000001ff00, 0xffff00ff01ff00, 0x1000101000001ff, 0xffff00ff00000001, + 0xff0001ffff010001, 0xff00000100ffff01, 0xff0000ffff0000ff, 0x100ff01ff000001, + 0x1ff0001ff00ff00, 0xff01ffff000000, 0x10001010100ff, 0xffff010001ffff, + 0xff00000100010100, 0x100000001000000, 0x1ffff0000ff00, 0x10101ffff000001, + 0xffff000101000001, 0xff01ffff00, 0x1010001ff000001, 0xff0001ffff000001, + 0x101ff01ff, 0x1ff00ffffff0101, 0x1ff0100ff00ffff, 0xff0100ff, + 0xff010101010000, 0xff0101ffffffff01, 0xff01010001ff01, 0xff00010101ff00, + 0x100ff000000ff00, 0xff01ff01ff000101, 0x1ff0001ff01ff00, 0x1ff01010100ff01, + 0xff00ffffff000001, 0x10100010000ff, 0xff0001ffff0000ff, 0xffff00ffff0001ff, + 0xff01ffff00ffffff, 0x1ff0101000000ff, 0xffff01ff010101ff, 0x101ff00ffffffff, + 0x10101ffff01ff, 0x1ff00ff01ff00ff, 0xff01ff01010101ff, 0x101ff010100ff, + 0x101000100ff0001, 0xff00ff01000001ff, 0xff010001010000, 0xffff010000ffff00, + 0xff01000000ffff, 0xffffff010101ffff, 0x101010101000001, 0x1000100ffff00, + 0xff00ffff01, 0x101000000ff00, 0x1000001ff0000ff, 0x1ff0000ffff00, + 0xff0101ff00ff0100, 0x100ff0100ff0101, 0x10000ffff0100ff, 0xff010001ff010100, + 0xff0000ff010101, 0x1ff0000ff0000, 0x10001010000ff00, 0x1ff0101ffff01, + 0x1010000ffffff01, 0x1ffff0000ff01ff, 0xff00ff0000ff0001, 0x1ff00ffffffff01, + 0x1000001ff010000, 0x100ff0100ffffff, 0x100ff0000ff0000, 0xff0000ff00ff00ff, + 0xff0001ff00ff00ff, 0xffff0101ff010001, 0xff010001ff0001, 0xff010101ffffff00, + 0xffffffff00000101, 0xffffff00ff0100, 0xff01ffff01ffff01, 0x1010001ffff00ff, + 0xff01ff0001ffffff, 0xff00ff0100, 0x101ff00ffff0100, 0x1010001ffff0000, + 0xffff0000ff000101, 0x100010001ffffff, 0xff00ff01ff0100ff, 0x1ff01ff01ffff, + 0x1ff0101ff010101, 0x1ffff010100ff, 0xffff0001ffff, 0xff0100010101ff01, + 0x1ffff0000000000, 0x1ff010000ff01, 0xff000000ffff00, 0x1ffffff00010000, + 0x100ff0100ff01ff, 0xff010000ff01ffff, 0x1000100010001, 0xff010100000101ff, + 0x100ffffff01, 0x1ff000000ff0001, 0x10001ff000100, 0xff0100ff0101ff, +]; + +/// Word i of the tensor with byte `flip` (counted over the whole tensor) read as `to`. +pub fn word_with(i: u32, flip: u32, to: u8) -> u64 { + var w : u64 = W[i]; + var out : u64 = 0; + var j : u32 = 0; + while (j < 8) { + var b : u64 = w & 255; + if (i * 8 + j == flip) { b = to as u64; } + out = (out >> 8) | (b << 56); + w = w >> 8; + j = j + 1; + } + return out; +} + +/// The write checksum S the board folds while it packs the upload. +pub fn s_of(flip: u32, to: u8) -> u64 { + var s : u64 = 0; + var i : u32 = 0; + while (i < W_BEATS) { + s = fold(s, word_with(4 * i, flip, to), word_with(4 * i + 1, flip, to), word_with(4 * i + 2, flip, to), word_with(4 * i + 3, flip, to)); + i = i + 1; + } + return s; +} + +/// The output checksum Y: each row's wrapping sum of trit_term over its 320 columns, folded row by row. +/// `ff_plus` computes instead what the mutant board computes, which reads the trit FF as +1. +pub fn y_of(ff_plus: bool, flip: u32, to: u8) -> u64 { + var y : u64 = 0; + var acc : u32 = 0; + var xv : u8 = XV0; + var col : u32 = 0; + var i : u32 = 0; + while (i < W_WORDS) { + var w : u64 = word_with(i, flip, to); + var j : u32 = 0; + while (j < 8) { + const b : u8 = (w & 255) as u8; + if (ff_plus and b == 255) { + acc = acc +% sext8(xv); + } else { + acc = acc +% trit_term(b, xv); + } + xv = xv +% XSTEP; + col = col + 1; + if (col == W_COLS) { + y = fold(y, acc as u64, 0, 0, 0); + acc = 0; + col = 0; + xv = XV0; + } + w = w >> 8; + j = j + 1; + } + i = i + 1; + } + return y; +} + +test the_words_are_the_tensor_and_every_byte_is_a_trit { + assert_eq((W_WORDS as u64) * 8, W_BYTES); + assert_eq(W_WORDS, 4 * W_BEATS); + assert_eq(W[0], 0x00010001ffff00ff); + var zeros : u32 = 0; + var ones : u32 = 0; + var minus : u32 = 0; + var other : u32 = 0; + var i : u32 = 0; + while (i < W_WORDS) { + var w : u64 = W[i]; + var j : u32 = 0; + while (j < 8) { + const b : u64 = w & 255; + if (b == 0) { + zeros = zeros + 1; + } else if (b == 1) { + ones = ones + 1; + } else if (b == 255) { + minus = minus + 1; + } else { + other = other + 1; + } + w = w >> 8; + j = j + 1; + } + i = i + 1; + } + assert_eq(zeros, 8461); + assert_eq(ones, 5983); + assert_eq(minus, 6036); + assert_eq(other, 0); +} + +test s_expect_is_the_fold_of_the_640_pinned_beats { + assert_eq(word_with(0, NO_FLIP, 0), W[0]); + assert_eq(word_with(0, 0, 1), 0x00010001ffff0001); + assert_eq(s_of(NO_FLIP, 0), S_EXPECT); +} + +test y_expect_is_the_product_of_the_pinned_rows { + assert_eq(y_of(false, NO_FLIP, 0), Y_EXPECT); +} + +test the_mutant_that_reads_ff_as_plus_one_misses_y { + assert y_of(true, NO_FLIP, 0) != Y_EXPECT; +} + +test one_changed_byte_changes_s_and_y { + assert s_of(0, 1) != S_EXPECT; + assert y_of(false, 0, 1) != Y_EXPECT; + assert_eq(s_of(0, 255), S_EXPECT); + assert_eq(y_of(false, 0, 255), Y_EXPECT); +} From 2a7c7aecdd15b6b77048929e690566030a5c6ee4 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 21:00:26 +0700 Subject: [PATCH 2/8] fpga: board_receipt.t27 holds the receipt pieces the AX7203 board specs shared (Refs #10461) fold, hex_digit and the PASS/FAIL verdict characters were written three times, in rc_filter_ax7203, ddr3_head_bandwidth and ddr3_ternary_matvec; dupe-bodies named them. They now live in one pure module, specs/fpga/board_receipt.t27 (4 tests, 0 vacuous), and each board spec uses it. ddr3_head_bandwidth keeps its own four-verdict verdict_char for the SLOW and KILL lines. The head_bandwidth and rc_filter netlists emitted after the move equal the ones from before it, up to line order, comments and the function name. Seals written on the Railway lab with zig on PATH; three t27b ledger rows. Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/fpga_FpgaBoardReceipt.json | 28 +++++++ .../seals/fpga_FpgaDdr3HeadBandwidth.json | 21 +++-- .../seals/fpga_FpgaDdr3TernaryMatvec.json | 21 +++-- .trinity/seals/fpga_FpgaRcFilter.json | 21 +++-- .trinity/seals/fpga_FpgaTern9mL0KWeights.json | 14 ++-- docs/reports/t27b_expectations.json | 3 + specs/fpga/board_receipt.t27 | 84 +++++++++++++++++++ specs/fpga/ddr3_head_bandwidth.t27 | 20 ++--- specs/fpga/ddr3_ternary_matvec.t27 | 34 ++------ specs/fpga/rc_filter_ax7203.t27 | 27 ++---- specs/fpga/tern9m_l0_k_weights.t27 | 1 + 11 files changed, 180 insertions(+), 94 deletions(-) create mode 100644 .trinity/seals/fpga_FpgaBoardReceipt.json create mode 100644 specs/fpga/board_receipt.t27 diff --git a/.trinity/seals/fpga_FpgaBoardReceipt.json b/.trinity/seals/fpga_FpgaBoardReceipt.json new file mode 100644 index 0000000000..a82356f7aa --- /dev/null +++ b/.trinity/seals/fpga_FpgaBoardReceipt.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+a86b691b1", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:a5d6d0e10fdc5fa09a780007cd144fc129cf4de77c7762a9212bf64240806f34", + "gen_hash_rust": "sha256:f2efc42ebb64bbf2210158576b10c0fc652339aab5e1dcadac5cfda11472d192", + "gen_hash_verilog": "sha256:173a361ae8759a6ba7228d792947d405fed05747a23a9fd76afc768a2cfc3c61", + "gen_hash_zig": "sha256:34f3ca54b36f64c4e2b122d50f3f6c506275a5cf895e2478fdb4f6b15478c4b7", + "module": "FpgaBoardReceipt", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-18T13:56:40Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:34634f7251ed8b2a1539748dd9aa8dbdb263d7c039e8635d05eea70c7857ceb2", + "spec_path": "specs/fpga/board_receipt.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 4, + "total": 4, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/.trinity/seals/fpga_FpgaDdr3HeadBandwidth.json b/.trinity/seals/fpga_FpgaDdr3HeadBandwidth.json index 0f8c7000b0..1593d7666a 100644 --- a/.trinity/seals/fpga_FpgaDdr3HeadBandwidth.json +++ b/.trinity/seals/fpga_FpgaDdr3HeadBandwidth.json @@ -1,17 +1,22 @@ { - "built_by": "t27c-bootstrap@0.5.2+79126608b", - "closure": [], + "built_by": "t27c-bootstrap@0.5.2+a86b691b1", + "closure": [ + { + "spec": "specs/fpga/board_receipt.t27", + "spec_hash": "sha256:34634f7251ed8b2a1539748dd9aa8dbdb263d7c039e8635d05eea70c7857ceb2" + } + ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:23ce13530186a4f63ca3f42565c4f3b5ef346c5f4a8d8ba2e8ba1f5fe0a6de0e", - "gen_hash_rust": "sha256:d61c73f5c49d32d0d11aeafd20abb948f6ab4e0fcab4bafe48f005f7c2f5d8de", - "gen_hash_verilog": "sha256:65e8b6194fd2f634281e7c493a3bcf609afdc8850c049c4e0c6da69c989750a1", - "gen_hash_zig": "sha256:d7b5263c8fdf4d0ca62310bffd53858e33fb44556eda898c929be756b53c9c66", + "gen_hash_c": "sha256:1b37e08fd08dbbc0645a49bc82a0dcc499e209d26f5e5734ae39d130f920fe58", + "gen_hash_rust": "sha256:9543f6cb7a6e90c6af7602df2c0c5373f88ca949b74e90742fce80a42c0baa7e", + "gen_hash_verilog": "sha256:c8408e1ad2d20562e6f624647dca216e9d06483006eefeba1ce57857dd3fad09", + "gen_hash_zig": "sha256:ed9f25e68b8a6a456ec6eda990b40bc89a2abf948e8b87e46910eacb7b6830a3", "module": "FpgaDdr3HeadBandwidth", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T09:08:23Z", + "sealed_at": "2026-10-18T13:56:41Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:59242e4bc9430d41386640efe931ac3996a02afcee1b5142451750a48d99fc89", + "spec_hash": "sha256:152bf98420d4c3919835eefdb3cad56c76cd80cbecc11e1bcb6616fc25dfdd04", "spec_path": "specs/fpga/ddr3_head_bandwidth.t27", "tests": { "failed": 0, diff --git a/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json b/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json index 84141a9937..17f54ca958 100644 --- a/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json +++ b/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json @@ -1,17 +1,22 @@ { "built_by": "t27c-bootstrap@0.5.2+a86b691b1", - "closure": [], + "closure": [ + { + "spec": "specs/fpga/board_receipt.t27", + "spec_hash": "sha256:34634f7251ed8b2a1539748dd9aa8dbdb263d7c039e8635d05eea70c7857ceb2" + } + ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:a97c2a9d6b4b710cf14aabd9b615d84097b7f0e556e27efb8f87a0ff58f25723", - "gen_hash_rust": "sha256:e4ceee52757003ee74d3cbbcd80038a6385e0bbe19c438857c9033e93512a41b", - "gen_hash_verilog": "sha256:240ad78d4c69b08dc52089c56c8423d9df62e9ed2f70e807985a278f4108345d", - "gen_hash_zig": "sha256:9cc18b3a4e948e1015c2301bc1d93f220865aaedd2ff1140c51612cdbeae5bde", + "gen_hash_c": "sha256:6c6a9ec0d0a29cee4cdda2fa4147c9b130211779398df15120651ef3520420d5", + "gen_hash_rust": "sha256:f798400288f576af78e00d769ae4cd0b2078d59a8e848890f21deec8e5919c6b", + "gen_hash_verilog": "sha256:48855b0e730bfe30e51396720c2848655bc5ea2fd30e4af579481b2df9022dc1", + "gen_hash_zig": "sha256:d2c538e206df78bd9c81d2c9d69656bc79b296e1f1230c81878d5bf36e94aaf0", "module": "FpgaDdr3TernaryMatvec", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T13:03:19Z", + "sealed_at": "2026-10-18T13:56:28Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:11fbcc214ab20edaded49ece8dd1714f55f2195f7f1147cb6e49ad7025658eca", + "spec_hash": "sha256:09e4d4749d35d91c1bc87a96396ce89a6282eecca6feeb3405f438268a0f62d2", "spec_path": "specs/fpga/ddr3_ternary_matvec.t27", "tests": { "failed": 0, @@ -25,4 +30,4 @@ "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", "zig": "0.16.0" } -}warning: Config as Code (railway.json / railway.toml) is deprecated. Prefer Infrastructure as Code (.railway/railway.ts). Run `railway config migrate` or see https://docs.railway.com/infrastructure-as-code#migrating-from-config-as-code +} \ No newline at end of file diff --git a/.trinity/seals/fpga_FpgaRcFilter.json b/.trinity/seals/fpga_FpgaRcFilter.json index 5547c56073..3d5ea1c297 100644 --- a/.trinity/seals/fpga_FpgaRcFilter.json +++ b/.trinity/seals/fpga_FpgaRcFilter.json @@ -1,17 +1,22 @@ { - "built_by": "t27c-bootstrap@0.5.2+9da2c5f", - "closure": [], + "built_by": "t27c-bootstrap@0.5.2+a86b691b1", + "closure": [ + { + "spec": "specs/fpga/board_receipt.t27", + "spec_hash": "sha256:34634f7251ed8b2a1539748dd9aa8dbdb263d7c039e8635d05eea70c7857ceb2" + } + ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:345d70ff4a42876b9a38808fb16183e3026e436fe989ae8421da9e346bc07096", - "gen_hash_rust": "sha256:6321804010ff1127f915e0004f936d9a7002c01a525de42c539fe9e2595fd9be", - "gen_hash_verilog": "sha256:f8a97da90c082ad1ab84c132487152da1fe021c7f7be0537d970d6a6483c36de", - "gen_hash_zig": "sha256:5da6f0a60ae03e0ac806727e04bf0d2ae19e3d3589271de9b090bc4f91590fb8", + "gen_hash_c": "sha256:d1b54196aeea618074c6654c877e42a69687369fff6483f1d140c96c0553db76", + "gen_hash_rust": "sha256:044f3df98ab05033ac9202b689a0ff7a8e701e4c25a38d57d26ce40ec7718586", + "gen_hash_verilog": "sha256:c0add2c88039eefcf8f2d87a0cbbb24e275f2f9ec87f21883bc7c59ebe9bfe7a", + "gen_hash_zig": "sha256:f2074147e6c0cd2a5f32b68cd30e35375c2106f187d09ef55bbf0839c4d72d47", "module": "FpgaRcFilter", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T08:25:46Z", + "sealed_at": "2026-10-18T13:56:42Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:8fba8a419217ffe5dc6454759dd438d2236fb2cd829f9d64a3c2e15e3f44e51d", + "spec_hash": "sha256:be3af1aa6195d51e46289121cfd42623c80cd42d863442f4f6f69109da06d32f", "spec_path": "specs/fpga/rc_filter_ax7203.t27", "tests": { "failed": 0, diff --git a/.trinity/seals/fpga_FpgaTern9mL0KWeights.json b/.trinity/seals/fpga_FpgaTern9mL0KWeights.json index cd25b554f2..c3e8061e6b 100644 --- a/.trinity/seals/fpga_FpgaTern9mL0KWeights.json +++ b/.trinity/seals/fpga_FpgaTern9mL0KWeights.json @@ -1,22 +1,26 @@ { "built_by": "t27c-bootstrap@0.5.2+a86b691b1", "closure": [ + { + "spec": "specs/fpga/board_receipt.t27", + "spec_hash": "sha256:34634f7251ed8b2a1539748dd9aa8dbdb263d7c039e8635d05eea70c7857ceb2" + }, { "spec": "specs/fpga/ddr3_ternary_matvec.t27", - "spec_hash": "sha256:11fbcc214ab20edaded49ece8dd1714f55f2195f7f1147cb6e49ad7025658eca" + "spec_hash": "sha256:09e4d4749d35d91c1bc87a96396ce89a6282eecca6feeb3405f438268a0f62d2" } ], "config": "gen=c,rust,verilog,zig;tests=zig", "gen_hash_c": "sha256:35613d884051da0f0460bb7a715b0dfcd488767db707c78e5f03c556342e8f77", "gen_hash_rust": "sha256:81255bea491747e968ad3a570ee76bf15c7417e8d8f03587f1319ce2f99d16d6", "gen_hash_verilog": "sha256:dce0d2d14e0273bb91945f477f1c9fcd66466a570dea68c22ff8822fb972e805", - "gen_hash_zig": "sha256:1bb4a6177c70132b5c5b585008698c4282e3b0cbfb9b6a3697fdc8786b9aaccf", + "gen_hash_zig": "sha256:c1af58cf33a3637c066d41333fceea34af490bb43fd4e0a23cd845f0d1b294f0", "module": "FpgaTern9mL0KWeights", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T13:03:37Z", + "sealed_at": "2026-10-18T13:56:40Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:31241d2b9351e8d3c35f1b5ecfcfedd11c674afb82836f8137e7658b2f672a8d", + "spec_hash": "sha256:4959a8d309225306e0be90812cc1b2036a3123410d3a83b036fc84eec04215d3", "spec_path": "specs/fpga/tern9m_l0_k_weights.t27", "tests": { "failed": 0, @@ -30,4 +34,4 @@ "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", "zig": "0.16.0" } -}warning: Config as Code (railway.json / railway.toml) is deprecated. Prefer Infrastructure as Code (.railway/railway.ts). Run `railway config migrate` or see https://docs.railway.com/infrastructure-as-code#migrating-from-config-as-code +} \ No newline at end of file diff --git a/docs/reports/t27b_expectations.json b/docs/reports/t27b_expectations.json index 4350020ffd..d6ab6e7b49 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -290,6 +290,7 @@ {"path": "specs/fpga/apb_bridge.t27", "t27b": "pass"}, {"path": "specs/fpga/assembler.t27", "t27b": "pass"}, {"path": "specs/fpga/axi4.t27", "t27b": "pass"}, + {"path": "specs/fpga/board_receipt.t27", "t27b": "pass"}, {"path": "specs/fpga/boards/arty_a7_integration.t27", "t27b": "pass"}, {"path": "specs/fpga/boards/qmtech_a100t_integration.t27", "t27b": "pass"}, {"path": "specs/fpga/bootrom.t27", "t27b": "pass"}, @@ -299,6 +300,7 @@ {"path": "specs/fpga/crossopt.t27", "t27b": "pass"}, {"path": "specs/fpga/cts.t27", "t27b": "pass"}, {"path": "specs/fpga/ddr3_head_bandwidth.t27", "t27b": "pass"}, + {"path": "specs/fpga/ddr3_ternary_matvec.t27", "t27b": "pass"}, {"path": "specs/fpga/dft.t27", "t27b": "pass"}, {"path": "specs/fpga/die_probe.t27", "t27b": "pass"}, {"path": "specs/fpga/dsp/adders.t27", "t27b": "pass"}, @@ -331,6 +333,7 @@ {"path": "specs/fpga/secded.t27", "t27b": "pass"}, {"path": "specs/fpga/simulator.t27", "t27b": "pass"}, {"path": "specs/fpga/stdlib.t27", "t27b": "pass"}, + {"path": "specs/fpga/tern9m_l0_k_weights.t27", "t27b": "pass"}, {"path": "specs/fpga/ternary_isa.t27", "t27b": "pass"}, {"path": "specs/fpga/ternary_link.t27", "t27b": "pass"}, {"path": "specs/fpga/testbench/assembler_tb.t27", "t27b": "pass"}, diff --git a/specs/fpga/board_receipt.t27 b/specs/fpga/board_receipt.t27 new file mode 100644 index 0000000000..7162f9ce93 --- /dev/null +++ b/specs/fpga/board_receipt.t27 @@ -0,0 +1,84 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/fpga/board_receipt.t27 -- the pieces of a board's UART receipt that every AX7203 board spec shares +; The board specs specs/fpga/rc_filter_ax7203.t27, specs/fpga/ddr3_head_bandwidth.t27 and +; specs/fpga/ddr3_ternary_matvec.t27 each print one receipt line on the UART; the two DDR3 ones also fold +; 256-bit beats into a checksum. These are the bodies they had each written for themselves +; (tools/dupe_scan.py): one home, used by each. +; - +; Pure functions only: no pins, no `pub var`, no on_clock, and no name a board spec also defines, so a `use` +; of this module adds nothing to a board's netlist but the functions it calls (`t27b verilog` emits them +; after the board's own; checked against the netlists from before the move). +; A verdict of 0 is PASS in every board spec (each one's V_PASS); any other verdict that reaches +; pass_fail_char prints FAIL. ddr3_head_bandwidth's SLOW and KILL lines keep their own verdict_char. +; ASCII only, English only. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module FpgaBoardReceipt; + +/// The checksum after one more 256-bit beat: rotate the sum left by one, then xor in the four lanes, lane +/// k rotated left by 16 * k. +pub fn fold(sum: u64, l0: u64, l1: u64, l2: u64, l3: u64) -> u64 { + return ((sum << 1) | (sum >> 63)) ^ l0 ^ ((l1 << 16) | (l1 >> 48)) ^ ((l2 << 32) | (l2 >> 32)) ^ ((l3 << 48) | (l3 >> 16)); +} + +/// The ASCII digit of a nibble, 0-9 A-F. +pub fn hex_digit(n: u8) -> u8 { + if ((n & 15) < 10) { return 48 + (n & 15); } + return 55 + (n & 15); +} + +/// Character p of " PASS\r\n" (verdict 0) or " FAIL\r\n" (any other verdict). +pub fn pass_fail_char(v: u8, p: u8) -> u8 { + if (p == 0) { return 32; } + if (p == 5) { return 13; } + if (p == 6) { return 10; } + if (v == 0) { + if (p == 1) { return 80; } + if (p == 2) { return 65; } + return 83; + } + if (p == 1) { return 70; } + if (p == 2) { return 65; } + if (p == 3) { return 73; } + return 76; +} + +test hex_digit_covers_all_sixteen_nibbles_and_ignores_the_high_ones { + assert_eq(hex_digit(0), 48); + assert_eq(hex_digit(9), 57); + assert_eq(hex_digit(10), 65); + assert_eq(hex_digit(15), 70); + assert_eq(hex_digit(0xA7), 55); +} + +test pass_fail_char_spells_pass_and_fail { + assert_eq(pass_fail_char(0, 0), 32); + assert_eq(pass_fail_char(0, 1), 80); + assert_eq(pass_fail_char(0, 2), 65); + assert_eq(pass_fail_char(0, 3), 83); + assert_eq(pass_fail_char(0, 4), 83); + assert_eq(pass_fail_char(0, 5), 13); + assert_eq(pass_fail_char(0, 6), 10); + assert_eq(pass_fail_char(3, 1), 70); + assert_eq(pass_fail_char(3, 2), 65); + assert_eq(pass_fail_char(3, 3), 73); + assert_eq(pass_fail_char(3, 4), 76); + assert_eq(pass_fail_char(1, 1), 70); +} + +test fold_rotates_the_sum_and_each_lane { + assert_eq(fold(0, 0, 0, 0, 0), 0); + assert_eq(fold(1, 0, 0, 0, 0), 2); + assert_eq(fold(0x8000000000000000, 0, 0, 0, 0), 1); + assert_eq(fold(0, 1, 0, 0, 0), 1); + assert_eq(fold(0, 0, 1, 0, 0), 0x10000); + assert_eq(fold(0, 0, 0, 1, 0), 0x100000000); + assert_eq(fold(0, 0, 0, 0, 1), 0x1000000000000); + assert_eq(fold(0, 0, 0x8000000000000000, 0, 0), 0x8000); +} + +test a_fold_that_dropped_a_lane_would_be_seen { + const a : u64 = fold(0x0123456789ABCDEF, 0x1111, 0x2222, 0x3333, 0x4444); + const b : u64 = fold(0x0123456789ABCDEF, 0x1111, 0x2222, 0x3333, 0); + assert(a != b); +} diff --git a/specs/fpga/ddr3_head_bandwidth.t27 b/specs/fpga/ddr3_head_bandwidth.t27 index 01d4c242bc..1df4f8e905 100644 --- a/specs/fpga/ddr3_head_bandwidth.t27 +++ b/specs/fpga/ddr3_head_bandwidth.t27 @@ -44,6 +44,8 @@ module FpgaDdr3HeadBandwidth; +use fpga::board_receipt; + pub const KIND : str = "board-cell"; pub const ID : str = "fpga/ddr3_head_bandwidth"; pub const EPIC : str = "gHashTag/t27#10024"; @@ -85,14 +87,10 @@ pub fn lane_word(i: u32, k: u32) -> u64 { return w ^ (w << 21) ^ (w << 42) ^ LANE_SALT; } -/// The checksum after one more beat: rotate the sum left by one, then xor in the four lanes, lane k -/// rotated left by 16 * k. Order matters. The lane rotations matter too: the four lanes of a beat of the -/// pattern xor to zero (the salt four times, and (i << 2 | k) for k = 0..3 under every shift), so a plain -/// xor of the lanes adds nothing and every sum is 0. The first bitstream on the board reported exactly -/// that, S=0 C=0. A rotation is wiring; it adds no gate. -pub fn fold(sum: u64, l0: u64, l1: u64, l2: u64, l3: u64) -> u64 { - return ((sum << 1) | (sum >> 63)) ^ l0 ^ ((l1 << 16) | (l1 >> 48)) ^ ((l2 << 32) | (l2 >> 32)) ^ ((l3 << 48) | (l3 >> 16)); -} +; fold, the beat checksum, is specs/fpga/board_receipt.t27's, as hex_digit is: one body for every +; board spec. Its lane rotations matter: the four lanes of a beat of this pattern xor to zero (the salt +; four times, and (i << 2 | k) for k = 0..3 under every shift), so a plain xor of the lanes adds nothing +; and every sum is 0. The first bitstream on the board reported exactly that, S=0 C=0. /// The beat's four lanes are the pattern of beat i. pub fn beat_ok(i: u32, l0: u64, l1: u64, l2: u64, l3: u64) -> bool { @@ -138,12 +136,6 @@ pub fn div_q(q: u32, rem: u64, num: u32, den: u32) -> u32 { ; --- the receipt -------------------------------------------------------------------------------- -/// The ASCII digit of a nibble, 0-9 A-F. -pub fn hex_digit(n: u8) -> u8 { - if ((n & 15) < 10) { return 48 + (n & 15); } - return 55 + (n & 15); -} - /// The key letter of field s (1..8): N W R M S C E L. pub fn key_of(s: u8) -> u8 { if (s == 1) { return 78; } diff --git a/specs/fpga/ddr3_ternary_matvec.t27 b/specs/fpga/ddr3_ternary_matvec.t27 index ae8179cf1a..d3a08798e9 100644 --- a/specs/fpga/ddr3_ternary_matvec.t27 +++ b/specs/fpga/ddr3_ternary_matvec.t27 @@ -42,6 +42,8 @@ module FpgaDdr3TernaryMatvec; +use fpga::board_receipt; + pub const KIND : str = "board-cell"; pub const ID : str = "fpga/ddr3_ternary_matvec"; pub const EPIC : str = "gHashTag/t27#10024"; @@ -81,12 +83,8 @@ pub const BAUD_DIV : u16 = 868; pub const LINE_SEGS : u8 = 9; ; --- the arithmetic ----------------------------------------------------------------------------- - -/// The checksum after one more beat (the fold of specs/fpga/ddr3_head_bandwidth.t27): rotate the sum left by -/// one, then xor in the four lanes, lane k rotated left by 16 * k. -pub fn fold(sum: u64, l0: u64, l1: u64, l2: u64, l3: u64) -> u64 { - return ((sum << 1) | (sum >> 63)) ^ l0 ^ ((l1 << 16) | (l1 >> 48)) ^ ((l2 << 32) | (l2 >> 32)) ^ ((l3 << 48) | (l3 >> 16)); -} +; fold (the beat checksum, the one specs/fpga/ddr3_head_bandwidth.t27 prints), hex_digit and pass_fail_char +; come from specs/fpga/board_receipt.t27, which every AX7203 board spec uses. /// An int8, held as its u8 bits, sign-extended to 32 bits. pub fn sext8(v: u8) -> u32 { @@ -135,12 +133,6 @@ pub fn frame_bit(b: u8, k: u32) -> bool { ; --- the receipt -------------------------------------------------------------------------------- -/// The ASCII digit of a nibble, 0-9 A-F. -pub fn hex_digit(n: u8) -> u8 { - if ((n & 15) < 10) { return 48 + (n & 15); } - return 55 + (n & 15); -} - /// The key letter of field s (1..7): N S C Y E F L. pub fn key_of(s: u8) -> u8 { if (s == 1) { return 78; } @@ -164,26 +156,10 @@ pub fn prefix_char(p: u8) -> u8 { return 78; } -/// Character p of " PASS\r\n" or " FAIL\r\n". -pub fn verdict_char(v: u8, p: u8) -> u8 { - if (p == 0) { return 32; } - if (p == 5) { return 13; } - if (p == 6) { return 10; } - if (v == V_PASS) { - if (p == 1) { return 80; } - if (p == 2) { return 65; } - return 83; - } - if (p == 1) { return 70; } - if (p == 2) { return 65; } - if (p == 3) { return 73; } - return 76; -} - /// The character at segment s, position p; `fsr` holds the field being written, its next nibble on top. pub fn line_char(s: u8, p: u8, fsr: u64, v: u8) -> u8 { if (s == 0) { return prefix_char(p); } - if (s == LINE_SEGS - 1) { return verdict_char(v, p); } + if (s == LINE_SEGS - 1) { return pass_fail_char(v, p); } if (p == 0) { return 32; } if (p == 1) { return key_of(s); } if (p == 2) { return 61; } diff --git a/specs/fpga/rc_filter_ax7203.t27 b/specs/fpga/rc_filter_ax7203.t27 index d7301506ea..7359214656 100644 --- a/specs/fpga/rc_filter_ax7203.t27 +++ b/specs/fpga/rc_filter_ax7203.t27 @@ -47,6 +47,8 @@ module FpgaRcFilter; +use fpga::board_receipt; + pub const KIND : str = "board-cell"; pub const ID : str = "fpga/rc_filter_ax7203"; pub const REFERENCE : str = "mirekez/cpphdl analog/examples/rc_filter"; @@ -159,11 +161,8 @@ pub const SCALE : f64 = 16777216.0; ; --- the receipt -------------------------------------------------------------------------------- -/// The ASCII digit of a nibble, 0-9 A-F. -pub fn hex_digit(n: u8) -> u8 { - if ((n & 15) < 10) { return 48 + (n & 15); } - return 55 + (n & 15); -} +; hex_digit and pass_fail_char (" PASS\r\n" or " FAIL\r\n") are specs/fpga/board_receipt.t27's: one body +; for every board spec. /// The key letter of field s (1..5): A B S C L. pub fn key_of(s: u8) -> u8 { @@ -184,26 +183,10 @@ pub fn prefix_char(p: u8) -> u8 { return 67; } -/// Character p of " PASS\r\n" or " FAIL\r\n". -pub fn verdict_char(v: u8, p: u8) -> u8 { - if (p == 0) { return 32; } - if (p == 5) { return 13; } - if (p == 6) { return 10; } - if (v == V_PASS) { - if (p == 1) { return 80; } - if (p == 2) { return 65; } - return 83; - } - if (p == 1) { return 70; } - if (p == 2) { return 65; } - if (p == 3) { return 73; } - return 76; -} - /// The character at segment s, position p; `fsr` holds the field being written, its next nibble on top. pub fn line_char(s: u8, p: u8, fsr: u64, v: u8) -> u8 { if (s == 0) { return prefix_char(p); } - if (s == 6) { return verdict_char(v, p); } + if (s == 6) { return pass_fail_char(v, p); } if (p == 0) { return 32; } if (p == 1) { return key_of(s); } if (p == 2) { return 61; } diff --git a/specs/fpga/tern9m_l0_k_weights.t27 b/specs/fpga/tern9m_l0_k_weights.t27 index 6fe9418022..e21b3a92dd 100644 --- a/specs/fpga/tern9m_l0_k_weights.t27 +++ b/specs/fpga/tern9m_l0_k_weights.t27 @@ -16,6 +16,7 @@ module FpgaTern9mL0KWeights; use fpga::ddr3_ternary_matvec; +use fpga::board_receipt; pub const W_WORDS : u32 = 2560; /// No byte changed (an index past the 20,480 bytes). From e24412638f3c90a94e0e1a4616fae8f45cbe6c35 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 21:25:50 +0700 Subject: [PATCH 3/8] dupe-bodies: drop the hex_digit group from the baseline (Refs #10461) board_receipt.t27 now holds the one hex_digit the three AX7203 board specs had each written, so the group is gone and the gate asked for the ceiling to come down with it: 1 line removed by tools/dupe_scan.py --bless. Co-Authored-By: Claude Opus 5.5 --- tools/duplicate_bodies_baseline.txt | 1 - 1 file changed, 1 deletion(-) diff --git a/tools/duplicate_bodies_baseline.txt b/tools/duplicate_bodies_baseline.txt index e087d2a1c0..4dd6f0ec59 100644 --- a/tools/duplicate_bodies_baseline.txt +++ b/tools/duplicate_bodies_baseline.txt @@ -106,7 +106,6 @@ generate_next_token_from_logits 2 hard_sigmoid 2 has_at 2 has_star_inner 2 -hex_digit 2 hw_place_before 2 id_seen_before 2,2 int_to_bytes 2 From bda018e7261aa23809addab56c25ac0b6b8d1715 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 22:04:02 +0700 Subject: [PATCH 4/8] elab ratchet: rows for board_receipt 0 and tern9m_l0_k_weights 8 (Refs #10461) Both specs arrive with cell 26 and gen-verilog emits a module for each, so the ratchet read them as NEW. board_receipt elaborates clean. The 8 in the weights spec are all names it takes by `use` from board_receipt and from ddr3_ternary_matvec (a t27b spec gen-verilog skips); the weights are test data the board receives over the UART, never synthesized. Measured on CI (iverilog 12.0) and on the Railway lab (11.0): 214 errors, baseline now 214. Co-Authored-By: Claude Opus 5.5 --- tools/elab_baseline.txt | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/tools/elab_baseline.txt b/tools/elab_baseline.txt index fe39be3c82..2f12e63a15 100644 --- a/tools/elab_baseline.txt +++ b/tools/elab_baseline.txt @@ -59,10 +59,18 @@ # and instances, drop the skip and record the counts it measures. # `openxc7_dsp_fabric 0`, `wasm_board_ax7203 0` and `wasm_interp 0` reached # master without rows; all elaborate clean, so a 0 row hides nothing. +# 2026-10-18 (#10461, cell 26): `board_receipt 0` arrives with its spec and +# elaborates clean. `tern9m_l0_k_weights 8` is the board's test data, never +# synthesized: the bytes reach the board over the UART. All 8 are names it +# takes by `use` -- `fold` from board_receipt; W_BEATS, XV0, XSTEP, W_COLS, +# sext8, trit_term from ddr3_ternary_matvec, which gen-verilog SKIPs as a t27b +# spec -- and gen-verilog emits one module per file with no imports bound. +# Measured with iverilog 12.0 on CI and 11.0 on the lab: the same 0 and 8. adapter 0 apb_bridge 4 assembler 4 axi4 2 +board_receipt 0 bootrom 3 bpsk 0 bridge 16 @@ -101,6 +109,7 @@ secded 0 simulator 2 spi 0 stdlib 2 +tern9m_l0_k_weights 8 ternary_isa 7 ternary_link 0 testbench 8 From b0d3fc8af532feb9a23dad5a7b41c3e17ba06f83 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 22:39:02 +0700 Subject: [PATCH 5/8] ddr3_ternary_matvec: the board judges against S_EXPECT and Y_EXPECT out of reset (Refs #10461) The first board run printed the right N, S, C and Y with E=F=0, and FAIL: s_want and y_want reset to 0. The tests set them before each run, so the spec passed while the hardware compared a correct receipt against 0. Both registers now reset to the pinned constants (t27b emits them as the reset values), and a new first test asserts the out-of-reset values before any test assigns them. With the old `= 0` initializers that test fails; the FF-as-+1 mutant still fails its trit test. 10/10 pass, 0 vacuous; seals written on the Railway lab. Co-Authored-By: Claude Opus 5.5 --- .../seals/fpga_FpgaDdr3TernaryMatvec.json | 16 +++++++-------- .trinity/seals/fpga_FpgaTern9mL0KWeights.json | 4 ++-- specs/fpga/ddr3_ternary_matvec.t27 | 20 +++++++++++++++++-- 3 files changed, 28 insertions(+), 12 deletions(-) diff --git a/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json b/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json index 17f54ca958..b706b418f9 100644 --- a/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json +++ b/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json @@ -7,23 +7,23 @@ } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:6c6a9ec0d0a29cee4cdda2fa4147c9b130211779398df15120651ef3520420d5", - "gen_hash_rust": "sha256:f798400288f576af78e00d769ae4cd0b2078d59a8e848890f21deec8e5919c6b", - "gen_hash_verilog": "sha256:48855b0e730bfe30e51396720c2848655bc5ea2fd30e4af579481b2df9022dc1", - "gen_hash_zig": "sha256:d2c538e206df78bd9c81d2c9d69656bc79b296e1f1230c81878d5bf36e94aaf0", + "gen_hash_c": "sha256:af4d241ce9398f06df4527b2e7d8db1f81eeefa0c1298ec4be8840302236d92f", + "gen_hash_rust": "sha256:0f474fbf43039fa0da4932752897314fb70fddac664e0efbf3f98b535fae9895", + "gen_hash_verilog": "sha256:7dd8c000bec8d732ebf2538e289621bee1f3c1e751df53f583beaaddf349680a", + "gen_hash_zig": "sha256:d38c2a80429c2b66adc024d7723b227ccaf2f792259277196f3255ebd3cd0f44", "module": "FpgaDdr3TernaryMatvec", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T13:56:28Z", + "sealed_at": "2026-10-18T15:37:16Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:09e4d4749d35d91c1bc87a96396ce89a6282eecca6feeb3405f438268a0f62d2", + "spec_hash": "sha256:84b7de73ff2f1a8679ca83443e0dcb62c5f30677cebc3015850331811420c16a", "spec_path": "specs/fpga/ddr3_ternary_matvec.t27", "tests": { "failed": 0, "failing": [], "forced": false, - "passed": 9, - "total": 9, + "passed": 10, + "total": 10, "vacuous": 0 }, "toolchain": { diff --git a/.trinity/seals/fpga_FpgaTern9mL0KWeights.json b/.trinity/seals/fpga_FpgaTern9mL0KWeights.json index c3e8061e6b..d01d656bb2 100644 --- a/.trinity/seals/fpga_FpgaTern9mL0KWeights.json +++ b/.trinity/seals/fpga_FpgaTern9mL0KWeights.json @@ -7,7 +7,7 @@ }, { "spec": "specs/fpga/ddr3_ternary_matvec.t27", - "spec_hash": "sha256:09e4d4749d35d91c1bc87a96396ce89a6282eecca6feeb3405f438268a0f62d2" + "spec_hash": "sha256:84b7de73ff2f1a8679ca83443e0dcb62c5f30677cebc3015850331811420c16a" } ], "config": "gen=c,rust,verilog,zig;tests=zig", @@ -18,7 +18,7 @@ "module": "FpgaTern9mL0KWeights", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T13:56:40Z", + "sealed_at": "2026-10-18T15:38:26Z", "sealed_by": "t27c-bootstrap@0.5.2", "spec_hash": "sha256:4959a8d309225306e0be90812cc1b2036a3123410d3a83b036fc84eec04215d3", "spec_path": "specs/fpga/tern9m_l0_k_weights.t27", diff --git a/specs/fpga/ddr3_ternary_matvec.t27 b/specs/fpga/ddr3_ternary_matvec.t27 index d3a08798e9..fd8d14f579 100644 --- a/specs/fpga/ddr3_ternary_matvec.t27 +++ b/specs/fpga/ddr3_ternary_matvec.t27 @@ -566,8 +566,10 @@ const ddram_dqs_n_3_SLEW : str = "FAST"; ; --- the registers ------------------------------------------------------------------------------ var st : u8 = 0; var n_beats : u32 = 640; -var s_want : u64 = 0; -var y_want : u64 = 0; +; the values the board judges against. Reset values, so they hold on the board: the first build reset +; them to 0, the tests set them before each run, and the board printed the right S and Y with FAIL. +var s_want : u64 = S_EXPECT; +var y_want : u64 = Y_EXPECT; ; the native port: address, command, write data var ca : u32 = 0; var cv : bool = false; @@ -820,6 +822,16 @@ fn on_clock(core_init_done: bool, core_init_error: bool, core_user_port_native_0 ; --- the tests ---------------------------------------------------------------------------------- +// First, before any test sets them; the tests that do restore them. A board out of reset judges with +// these values and no others. +test out_of_reset_the_board_judges_against_the_pinned_values { + assert_eq(n_beats, 640); + assert_eq(s_want, S_EXPECT); + assert_eq(y_want, Y_EXPECT); + assert_eq(verdict_of(640, S_EXPECT, S_EXPECT, Y_EXPECT, 0, 0, s_want, y_want, n_beats), V_PASS); + assert_eq(verdict_of(640, S_EXPECT, S_EXPECT, Y_EXPECT, 0, 0, 0, 0, n_beats), V_FAIL); +} + test the_tensor_is_640_beats_of_32_trits { var beats : u32 = 0; var bytes : u64 = 0; @@ -973,6 +985,8 @@ test two_rows_go_in_come_back_and_are_multiplied { assert_eq(col, 0); rx_div = 868; n_beats = 640; + s_want = S_EXPECT; + y_want = Y_EXPECT; } test a_byte_that_is_no_trit_is_counted_and_fails { @@ -1036,6 +1050,8 @@ test a_byte_that_is_no_trit_is_counted_and_fails { assert_eq(verdict_of(9, wsum, csum, ysum, 0, 0, s_want, y_want, 10), V_FAIL); rx_div = 868; n_beats = 640; + s_want = S_EXPECT; + y_want = Y_EXPECT; } test a_failed_calibration_reports_fail { From 314b7e82cc8064be998eac0c28ffbd003d14639c Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 23:42:19 +0700 Subject: [PATCH 6/8] tern9m_l0_k_weights: pin the two FAIL receipts the negative controls print (Refs #10461) The mutant test only said Y != Y_EXPECT and the byte-0 test only said S and Y differ. Both now also assert the exact values, read off the spec's own failing assert_eq with 0 in their place, not off the board: - Y_MUT_FF = 0x3E5E6C8ED51DF5C8, Y of the FF-as-+1 mutant on the real bytes - S_FLIP0 = 0x4B58160720ABB81C, Y_FLIP0 = 0x9A50D884522C2320, the real design on the bytes with byte 0 changed from FF to 01 On the AX7203 the mutant bitstream printed Y=3E5E6C8ED51DF5C8 FAIL and the design printed S=C=4B58160720ABB81C Y=9A50D884522C2320 FAIL, so each negative control fails for the predicted reason. 5/5 pass, 0 vacuous (asserts 4, 3, 1, 2, 6); resealed on the Railway lab. Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/fpga_FpgaTern9mL0KWeights.json | 12 ++++++------ specs/fpga/tern9m_l0_k_weights.t27 | 11 +++++++++++ 2 files changed, 17 insertions(+), 6 deletions(-) diff --git a/.trinity/seals/fpga_FpgaTern9mL0KWeights.json b/.trinity/seals/fpga_FpgaTern9mL0KWeights.json index d01d656bb2..026e0a21b5 100644 --- a/.trinity/seals/fpga_FpgaTern9mL0KWeights.json +++ b/.trinity/seals/fpga_FpgaTern9mL0KWeights.json @@ -11,16 +11,16 @@ } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:35613d884051da0f0460bb7a715b0dfcd488767db707c78e5f03c556342e8f77", - "gen_hash_rust": "sha256:81255bea491747e968ad3a570ee76bf15c7417e8d8f03587f1319ce2f99d16d6", - "gen_hash_verilog": "sha256:dce0d2d14e0273bb91945f477f1c9fcd66466a570dea68c22ff8822fb972e805", - "gen_hash_zig": "sha256:c1af58cf33a3637c066d41333fceea34af490bb43fd4e0a23cd845f0d1b294f0", + "gen_hash_c": "sha256:a1bc05c9dccc86398a7bc9f41cf8edc93c9545f35bf5be41dc38145327700c14", + "gen_hash_rust": "sha256:0f6232f05dbc51ad22947799c8ca0fab06c154afd4f572e80f46b55c4064f2b2", + "gen_hash_verilog": "sha256:43a2a07865e9a34ed7405f4a487e4c22c20d112abd9a74dbfe2da46cab3e8127", + "gen_hash_zig": "sha256:bd77315dd9e6410157ceaa8c59b5906e594814abcff5fce7b859a674597c871e", "module": "FpgaTern9mL0KWeights", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T15:38:26Z", + "sealed_at": "2026-10-18T16:39:57Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:4959a8d309225306e0be90812cc1b2036a3123410d3a83b036fc84eec04215d3", + "spec_hash": "sha256:43ee35ce1e0d1810b33cabe7517d109e4e469199fce38f4f563c5b5cceb9f448", "spec_path": "specs/fpga/tern9m_l0_k_weights.t27", "tests": { "failed": 0, diff --git a/specs/fpga/tern9m_l0_k_weights.t27 b/specs/fpga/tern9m_l0_k_weights.t27 index e21b3a92dd..308ac8080e 100644 --- a/specs/fpga/tern9m_l0_k_weights.t27 +++ b/specs/fpga/tern9m_l0_k_weights.t27 @@ -21,6 +21,14 @@ use fpga::board_receipt; pub const W_WORDS : u32 = 2560; /// No byte changed (an index past the 20,480 bytes). pub const NO_FLIP : u32 = 99999999; +/// The two FAIL receipts the negative controls must print, read off this spec's own failing `assert_eq` +/// run with 0 in their place (as S_EXPECT and Y_EXPECT were), not copied from the board. S_FLIP0 and Y_FLIP0 +/// were read before their board run; Y_MUT_FF after the mutant board had printed it, and it equals that receipt. +/// Y of the mutant board (FF read as +1) on the real bytes; its S is S_EXPECT. +pub const Y_MUT_FF : u64 = 0x3E5E6C8ED51DF5C8; +/// S and Y of the real board on the bytes with byte 0 changed from FF to 01. +pub const S_FLIP0 : u64 = 0x4B58160720ABB81C; +pub const Y_FLIP0 : u64 = 0x9A50D884522C2320; /// The 640 beats of the tensor, four words each. pub const W : [2560]u64 = [ @@ -772,11 +780,14 @@ test y_expect_is_the_product_of_the_pinned_rows { test the_mutant_that_reads_ff_as_plus_one_misses_y { assert y_of(true, NO_FLIP, 0) != Y_EXPECT; + assert_eq(y_of(true, NO_FLIP, 0), Y_MUT_FF); } test one_changed_byte_changes_s_and_y { assert s_of(0, 1) != S_EXPECT; assert y_of(false, 0, 1) != Y_EXPECT; + assert_eq(s_of(0, 1), S_FLIP0); + assert_eq(y_of(false, 0, 1), Y_FLIP0); assert_eq(s_of(0, 255), S_EXPECT); assert_eq(y_of(false, 0, 255), Y_EXPECT); } From e029b4b6322029bb68d0bc1f9d5536eda2474b0c Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Mon, 19 Oct 2026 05:06:24 +0700 Subject: [PATCH 7/8] own_model: cell 26 verified, compute from DDR3 on the AX7203 reviewed (Refs #10024, Refs #10461) Cell 26 ("Full model on FPGA, DDR3") moves from draft to verified at 15 percent. specs/fpga/ddr3_ternary_matvec.t27 computes y = W x on the AX7203 from the tern-tc-9m layer-0 K weights held in DDR3. Its UART receipt equals what the weights spec's test computes, and both negative controls print FAIL. Review 5565244743 is the reviewer bee on head 21ccad311. The model verdict was approve, and it named each of the three red checks as master's. The bee posted it as NEEDS_PERSON because the head changes seal files, the same hold as review 5563181513 on #10428 (cell 9). The board now reads 4 published, 23 verified, 0 drafts, 0 gaps; 62%. own_model.t27 passes 10/10 and own_model_board.t27 passes 6/6, 0 vacuous, on the Railway lab. The seals and gen/json/igla/own_model_board.json were written there. Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/igla_own_model.json | 16 +++---- .trinity/seals/igla_own_model_board.json | 18 ++++---- gen/json/igla/own_model_board.json | 2 +- specs/igla/own_model.t27 | 56 +++++++++++++++++------- specs/igla/own_model_board.t27 | 18 ++++---- 5 files changed, 66 insertions(+), 44 deletions(-) diff --git a/.trinity/seals/igla_own_model.json b/.trinity/seals/igla_own_model.json index 74393654fd..0e6acbc9c5 100644 --- a/.trinity/seals/igla_own_model.json +++ b/.trinity/seals/igla_own_model.json @@ -1,5 +1,5 @@ { - "built_by": "t27c-bootstrap@0.5.2+fd332dfd5", + "built_by": "t27c-bootstrap@0.5.2+9e8ff7af6", "closure": [ { "spec": "specs/t27f/reel.t27", @@ -15,16 +15,16 @@ } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:34f442903c5b74b1ddc28b310d9782b0f61c45098e4ff931771176583341057d", - "gen_hash_rust": "sha256:a0e037fe6d5dd9b82586a2bf2a80c27ff50f6c9ba7b9babe60e9b52349efaa5c", - "gen_hash_verilog": "sha256:64cba74ad08af9252262494d75e1ec94d598f81d5fa4b06bc3bff797d5ca5ad8", - "gen_hash_zig": "sha256:a180869d634e33aeca7c64cde565c2115d43ded528f7613a9ce9ad084ab787be", + "gen_hash_c": "sha256:5c6365f8b63c2904bb3b13278b99d66c84ade2025cf6ee084cb4cf19598c4c38", + "gen_hash_rust": "sha256:313643b2f632168a470d4d77396ca4da7bd110a32a0b51f2c3a96cb6030fbf06", + "gen_hash_verilog": "sha256:d2ac3cfcc384a8d8f14d55346b2d193670f4ad1424173ff7a5f524b5ecd69c5f", + "gen_hash_zig": "sha256:034324eec283aebddf41d64127dac4b6cdd871ce0ff1cb1c91ab17b58d8ffc69", "module": "own_model", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T13:33:41Z", + "sealed_at": "2026-10-18T22:05:25Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:2c3daec9e62ce9123e19cad921e57af75beb25a1870c234230ae5505a7d7ac79", + "spec_hash": "sha256:5a3d744947dc65b8c13d02a3ad58aa6c97f694f5459634110823788381a5ff80", "spec_path": "specs/igla/own_model.t27", "tests": { "failed": 0, @@ -35,7 +35,7 @@ "vacuous": 0 }, "toolchain": { - "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "test_runner": "sha256:8512b80da533b79289110fca4a65f3336abd7a059ca4b72ea595d5e33ff8ad10", "zig": "0.16.0" } } \ No newline at end of file diff --git a/.trinity/seals/igla_own_model_board.json b/.trinity/seals/igla_own_model_board.json index 20c6c66218..21ac9c61d0 100644 --- a/.trinity/seals/igla_own_model_board.json +++ b/.trinity/seals/igla_own_model_board.json @@ -1,9 +1,9 @@ { - "built_by": "t27c-bootstrap@0.5.2+fd332dfd5", + "built_by": "t27c-bootstrap@0.5.2+9e8ff7af6", "closure": [ { "spec": "specs/igla/own_model.t27", - "spec_hash": "sha256:2c3daec9e62ce9123e19cad921e57af75beb25a1870c234230ae5505a7d7ac79" + "spec_hash": "sha256:5a3d744947dc65b8c13d02a3ad58aa6c97f694f5459634110823788381a5ff80" }, { "spec": "specs/t27f/reel.t27", @@ -19,16 +19,16 @@ } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:a0125cda52bdb9a87de3b170cc991ad71fc627caf8c60e4bc41a2f4a9a3a86e8", - "gen_hash_rust": "sha256:dc61033d126c3f954f8b6ae3f33c33f773edd8f5eda07530cf3576e56d39dd73", - "gen_hash_verilog": "sha256:0d56c85728676e996f03f9636d7492c02c2901cd034348565c28a657aa86731f", - "gen_hash_zig": "sha256:c742951d611cb908f642a7262478d7219717d0b3b3284c123aebd0d4cd63bff5", + "gen_hash_c": "sha256:e4afa57dd33fdae88c9bc8bcbad343ceadac9bb8ef19a775415b1d4582778f03", + "gen_hash_rust": "sha256:382521e2dadd256ffb9713a2fad1fc39f4fdd07fa18443c080cb186512b8aa65", + "gen_hash_verilog": "sha256:4e773a0e4aa1439990eeacc896f6b4d0ca8a43df1a92db6ffa69bb4d84d98655", + "gen_hash_zig": "sha256:270159ce45d856052de63181768a5f8f3af5f69180fa2ad917c5b5beff4ffa75", "module": "own_model_board", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T13:33:45Z", + "sealed_at": "2026-10-18T22:05:27Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:69e4e67d00d0a17aed8d5e9ed45d7c745c970d069388db37f7835ff39179adae", + "spec_hash": "sha256:dabe2457877296de9097c66834d3a29ad66aa1862cc86fc8242ae9ab1acd39e5", "spec_path": "specs/igla/own_model_board.t27", "tests": { "failed": 0, @@ -39,7 +39,7 @@ "vacuous": 0 }, "toolchain": { - "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "test_runner": "sha256:8512b80da533b79289110fca4a65f3336abd7a059ca4b72ea595d5e33ff8ad10", "zig": "0.16.0" } } \ No newline at end of file diff --git a/gen/json/igla/own_model_board.json b/gen/json/igla/own_model_board.json index 4303344605..40616ee7af 100644 --- a/gen/json/igla/own_model_board.json +++ b/gen/json/igla/own_model_board.json @@ -1 +1 @@ -{"job":"own_model","stage":"own_model","msg":"4 published, 22 verified, 1 drafts, 0 gaps; 62%","progress":0.62,"metrics":{"lens_pct":[68,70,48],"cells":[{"status":4,"pct":60},{"status":4,"pct":70},{"status":4,"pct":80},{"status":4,"pct":80},{"status":4,"pct":60},{"status":4,"pct":100},{"status":5,"pct":50},{"status":5,"pct":90},{"status":5,"pct":30},{"status":4,"pct":100},{"status":4,"pct":100},{"status":4,"pct":20},{"status":4,"pct":80},{"status":4,"pct":65},{"status":4,"pct":95},{"status":4,"pct":75},{"status":4,"pct":55},{"status":4,"pct":40},{"status":4,"pct":70},{"status":4,"pct":15},{"status":5,"pct":60},{"status":4,"pct":40},{"status":4,"pct":100},{"status":4,"pct":60},{"status":4,"pct":30},{"status":3,"pct":10},{"status":4,"pct":50}]}} +{"job":"own_model","stage":"own_model","msg":"4 published, 23 verified, 0 drafts, 0 gaps; 62%","progress":0.62,"metrics":{"lens_pct":[68,70,48],"cells":[{"status":4,"pct":60},{"status":4,"pct":70},{"status":4,"pct":80},{"status":4,"pct":80},{"status":4,"pct":60},{"status":4,"pct":100},{"status":5,"pct":50},{"status":5,"pct":90},{"status":5,"pct":30},{"status":4,"pct":100},{"status":4,"pct":100},{"status":4,"pct":20},{"status":4,"pct":80},{"status":4,"pct":65},{"status":4,"pct":95},{"status":4,"pct":75},{"status":4,"pct":55},{"status":4,"pct":40},{"status":4,"pct":70},{"status":4,"pct":15},{"status":5,"pct":60},{"status":4,"pct":40},{"status":4,"pct":100},{"status":4,"pct":60},{"status":4,"pct":30},{"status":4,"pct":15},{"status":4,"pct":50}]}} diff --git a/specs/igla/own_model.t27 b/specs/igla/own_model.t27 index 4bde11faa8..7a0c5f36e8 100644 --- a/specs/igla/own_model.t27 +++ b/specs/igla/own_model.t27 @@ -129,9 +129,24 @@ ; worst path inside the LiteDRAM core, and 3 of 9 routes pass the BIOS memtest; the receipt is ; from those that do. This is a sequential read of a pattern, no weight on the board and no ; compute from DDR3, so the cell is a draft at 10 percent, a DELIVER step waiting for its review. -; Cell 26 has no review: its PR, #10248, merged without one, so it stays a draft. +; Cell 26 had no review: its PR, #10248, merged without one. +; - board on 2026-10-18, cell 26, compute from DDR3: specs/fpga/ddr3_ternary_matvec.t27 (10/10 +; tests, 0 vacuous on the lab) on the same LiteDRAM core. It takes the 20,480 bytes of +; blocks.0.attn.k.weight of playra/tern-tc-9m over the UART (specs/fpga/tern9m_l0_k_weights.t27, +; 5/5), writes them to DDR3 as 640 beats, reads them back and computes y = W x, 64 rows of 320 +; trits. Its receipt on the AX7203: N = 640 beats, S = C = 4B58160720ABB863, Y = 9A50D884522C233D, +; 0 bad trits, 0 bad frames, PASS, each value the one the weights spec's test computes. The two +; negative controls fail for the reason the spec predicts: the same bitstream fed the bytes with +; byte 0 changed from FF to 01 printed S = C = 4B58160720ABB81C, Y = 9A50D884522C2320, FAIL; a +; mutant that reads FF as +1 printed the right S and Y = 3E5E6C8ED51DF5C8, FAIL. Calibration is +; route luck: 1 of 9 design routes and 1 of 3 mutant routes passed the BIOS memtest. One +; projection of the 9M model on the board, not the whole forward pass, so 15 percent. Its PR is +; REVIEW_DDR3_PR: review REVIEW_DDR3_ID is the reviewer bee on head 21ccad311, whose model verdict +; was approve, with each of the three red checks named as master's; the bee posted it as +; NEEDS_PERSON, not APPROVE, because that head changes seal files, and the PR merged over that +; hold under the owner's standing instruction, as #10428 did. ; The engine asks an engineering LEARN step for a source link, a PRACTICE step for a passing test -; and a DELIVER step for a review. So: 4 published, 22 verified, 1 draft, 0 gaps. +; and a DELIVER step for a review. So: 4 published, 23 verified, 0 drafts, 0 gaps. ; PERCENT is a second, separate number per cell: an estimate of how much of that part exists, with ; its basis in SOURCES. It never feeds a status. The lens and overall figures are plain means, every @@ -256,7 +271,7 @@ pub const SOURCES : [27]str = [ "t27c test-report on 17 ML specs: 17 compile", "t27 specs/ml/host_io_model.t27 3/3 via t27c --backend ml (#10165); arena in ml/arena_heap.t27", "t27 specs/ml/train_slice_model.t27 5/5; its --backend ml binary trains one slice 20 steps (#10186)", - "t27 specs/fpga/ddr3_head_bandwidth.t27: head read 2769 MB/s on the AX7203; no weights on it", + "t27 specs/fpga/ddr3_ternary_matvec.t27: tern-tc-9m layer-0 K weights in DDR3, mat-vec receipt PASS on the AX7203", "t27 specs/igla/own_model.t27" ]; @@ -278,7 +293,7 @@ pub const MISSING : [27]str = [ /// The measurements per cell (see the header for how each was taken). pub const GROUNDED : [27]bool = [true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true]; pub const TEST_PASS : [27]bool = [false, false, false, true, true, true, false, false, false, false, false, false, true, true, true, false, false, false, false, false, false, true, true, true, false, false, false]; -pub const REVIEWED : [27]bool = [false, false, false, false, false, false, true, true, true, false, false, false, false, false, false, true, true, true, false, false, false, false, false, false, true, false, true]; +pub const REVIEWED : [27]bool = [false, false, false, false, false, false, true, true, true, false, false, false, false, false, false, true, true, true, false, false, false, false, false, false, true, true, true]; /// The approving review behind REVIEWED: PR and review id on gHashTag/t27 (5561941493: t27-bees /// APPROVE of 014a34d21, glm-4.7-flash and glm-4.5-flash independently, 2026-10-18 07:28 UTC). pub const REVIEW_PR : i32 = 10275; @@ -288,14 +303,19 @@ pub const REVIEW_ID : str = "5561941493"; /// changes .trinity/seals and gen/json files; merged over that hold on the owner's instruction). pub const REVIEW_500M_PR : i32 = 10428; pub const REVIEW_500M_ID : str = "5563181513"; +/// The review behind REVIEWED[25], cell 26: PR and review id on gHashTag/t27 (5565244743: t27-bees on +/// 21ccad311, 2026-10-18 22:02 UTC, model verdict approve, posted as NEEDS_PERSON because the head +/// changes .trinity/seals files; merged over that hold on the owner's instruction, as #10428 was). +pub const REVIEW_DDR3_PR : i32 = 10475; +pub const REVIEW_DDR3_ID : str = "5565244743"; pub const LIVE : [27]bool = [false, false, false, false, false, false, true, true, true, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false]; /// What a host passes the viewer, per cell: the earned status code and the step number as a label. -pub const STATUS : [27]u8 = [4, 4, 4, 4, 4, 4, 5, 5, 5, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 5, 4, 4, 4, 4, 3, 4]; +pub const STATUS : [27]u8 = [4, 4, 4, 4, 4, 4, 5, 5, 5, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 5, 4, 4, 4, 4, 4, 4]; pub const LABELS : [27]str = ["1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15", "16", "17", "18", "19", "20", "21", "22", "23", "24", "25", "26", "27"]; /// Percent of each part that exists, estimated from its source (see the header). Never a status. -pub const PCT : [27]u8 = [60, 70, 80, 80, 60, 100, 50, 90, 30, 100, 100, 20, 80, 65, 95, 75, 55, 40, 70, 15, 60, 40, 100, 60, 30, 10, 50]; +pub const PCT : [27]u8 = [60, 70, 80, 80, 60, 100, 50, 90, 30, 100, 100, 20, 80, 65, 95, 75, 55, 40, 70, 15, 60, 40, 100, 60, 30, 15, 50]; /// The t27c test-report counts the PRACTICE cells quote. pub const ML_SPECS_MEASURED : i32 = 17; @@ -320,7 +340,7 @@ pub const ROWS : [20]str = [ "In t27: loss, optimizers, HSLM pass", "17 of 17 ML specs compile on the lab", "9 of 9 IGLA CODER specs compile", - "4 published, 22 verified, 1 draft", + "4 published, 23 verified, 0 drafts", "0 gaps, about 62 percent overall", "Batched f32 HSLM trainer", "Shadow weights for the whole model", @@ -391,12 +411,12 @@ test a_gap_is_named_not_filled { test a_status_is_earned_not_chosen { assert statuses_earned(STATUS, DOMAIN, GROUNDED, TEST_PASS, REVIEWED, LIVE); - // the evidence slide's "4 published, 22 verified, 1 draft" and "0 gaps" + // the evidence slide's "4 published, 23 verified, 0 drafts" and "0 gaps" assert count_status(STATUS, STATUS_PUBLISHED) == 4; - assert count_status(STATUS, STATUS_VERIFIED) == 22; - assert count_status(STATUS, STATUS_DRAFT) == 1; + assert count_status(STATUS, STATUS_VERIFIED) == 23; + assert count_status(STATUS, STATUS_DRAFT) == 0; assert count_status(STATUS, STATUS_GAP) == 0; - assert count_true(REVIEWED) == 8; + assert count_true(REVIEWED) == 9; // every passing test is a PRACTICE step: the t27 bench, MultiPL-E and coder specs (cells 4 to // 6), loss, optimizers, forward pass, matvec, the ML specs that compile (cell 23) and the // file I/O t27c lowers (cell 24) @@ -430,17 +450,18 @@ test a_status_is_earned_not_chosen { test a_review_is_named_not_assumed { // REVIEWED is true exactly at the grounded DELIVER cells put to review: the seven of PR - // REVIEW_PR, step 9 from PR REVIEW_500M_PR, and not step 26, whose evidence came in a PR with - // no review + // REVIEW_PR, step 9 from PR REVIEW_500M_PR and step 26 from PR REVIEW_DDR3_PR assert REVIEW_PR == 10275; assert REVIEW_ID.len > 0; assert REVIEW_500M_PR == 10428; assert REVIEW_500M_ID.len > 0; + assert REVIEW_DDR3_PR == 10475; + assert REVIEW_DDR3_ID.len > 0; var c : i32 = 0; while (c < CELL_COUNT) { const i : usize = @intCast(c); var want : bool = false; - if (step_stage(@intCast(c)) == STAGE_DELIVER and GROUNDED[i] and c != 25) { + if (step_stage(@intCast(c)) == STAGE_DELIVER and GROUNDED[i]) { want = true; } assert REVIEWED[i] == want; @@ -455,11 +476,12 @@ test a_review_is_named_not_assumed { assert REVIEWED[8]; assert LIVE[8]; assert STATUS[8] == STATUS_PUBLISHED; - // step 26 is grounded but not reviewed, so it stays a draft + // step 26, the mat-vec from DDR3 on the board, is grounded and reviewed but not live: verified assert step_stage(25) == STAGE_DELIVER; assert GROUNDED[25]; - assert REVIEWED[25] == false; - assert STATUS[25] == STATUS_DRAFT; + assert REVIEWED[25]; + assert LIVE[25] == false; + assert STATUS[25] == STATUS_VERIFIED; } test the_compile_counts_are_the_measured_ones { diff --git a/specs/igla/own_model_board.t27 b/specs/igla/own_model_board.t27 index 451fbe3164..d1817dfc25 100644 --- a/specs/igla/own_model_board.t27 +++ b/specs/igla/own_model_board.t27 @@ -48,7 +48,7 @@ pub const LENS_CELLS : i32 = 9; pub const JOB : str = "own_model"; pub const STAGE : str = "own_model"; -pub const MSG : str = "4 published, 22 verified, 1 drafts, 0 gaps; 62%"; +pub const MSG : str = "4 published, 23 verified, 0 drafts, 0 gaps; 62%"; /// What MSG says once its numbers are taken out. pub const MSG_WORDS : str = " published, verified, drafts, gaps; %"; pub const OVERALL_PCT : u8 = 62; @@ -60,8 +60,8 @@ pub const KEY_STATUS : str = "status"; pub const KEY_PCT : str = "pct"; pub const LENS_PCT : [3]u8 = [68, 70, 48]; -pub const CELL_STATUS : [27]u8 = [4, 4, 4, 4, 4, 4, 5, 5, 5, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 5, 4, 4, 4, 4, 3, 4]; -pub const CELL_PCT : [27]u8 = [60, 70, 80, 80, 60, 100, 50, 90, 30, 100, 100, 20, 80, 65, 95, 75, 55, 40, 70, 15, 60, 40, 100, 60, 30, 10, 50]; +pub const CELL_STATUS : [27]u8 = [4, 4, 4, 4, 4, 4, 5, 5, 5, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 5, 4, 4, 4, 4, 4, 4]; +pub const CELL_PCT : [27]u8 = [60, 70, 80, 80, 60, 100, 50, 90, 30, 100, 100, 20, 80, 65, 95, 75, 55, 40, 70, 15, 60, 40, 100, 60, 30, 15, 50]; /// The size of the compact metrics object, in bytes, computed from the keys and values above. pub const METRICS_BYTES : i32 = 631; @@ -263,8 +263,8 @@ test the_tally_sums_to_twenty_seven { assert count_status(CELL_STATUS, STATUS_OPEN) == 0; assert published + verified + drafts + gaps == CELL_COUNT; assert published == 4; - assert verified == 22; - assert drafts == 1; + assert verified == 23; + assert drafts == 0; assert gaps == 0; } @@ -275,11 +275,11 @@ test the_message_is_the_tally { const n : i32 = @intCast(MSG.len); assert n <= MSG_MAX; // one number wrong, a word changed, or a number added: each refused - assert msg_matches("4 published, 22 verified, 2 drafts, 0 gaps; 62%", STATUS, overall) == false; - assert msg_matches("4 published, 22 verified, 1 drafts, 0 holes; 62%", STATUS, overall) == false; - assert msg_matches("4 published, 22 verified, 1 drafts, 0 gaps; 62% of 100", STATUS, overall) == false; + assert msg_matches("4 published, 23 verified, 1 drafts, 0 gaps; 62%", STATUS, overall) == false; + assert msg_matches("4 published, 23 verified, 0 drafts, 0 holes; 62%", STATUS, overall) == false; + assert msg_matches("4 published, 23 verified, 0 drafts, 0 gaps; 62% of 100", STATUS, overall) == false; assert msg_matches(MSG, STATUS, 61) == false; - assert nth_number(MSG, 2) == 1; + assert nth_number(MSG, 2) == 0; assert nth_number(MSG, 4) == 62; assert nth_number(MSG, 5) == -1; } From e337b6ea2db07992db5171a209f1319bae53ca2f Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Mon, 19 Oct 2026 05:16:45 +0700 Subject: [PATCH 8/8] seals: reseal own_model and own_model_board after the master merge (Refs #10461) Master's #10551 changed specs/t27f/topic_engine.t27, which is in the closure of both seals. Resealed on the Railway lab with t27c built from 0102386d9: own_model.t27 10/10, own_model_board.t27 6/6, and t27c gen-json still writes gen/json/igla/own_model_board.json byte for byte (sha256 3b2c0bce...b5cf). Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/igla_own_model.json | 4 ++-- .trinity/seals/igla_own_model_board.json | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.trinity/seals/igla_own_model.json b/.trinity/seals/igla_own_model.json index 0e6acbc9c5..40d354c5f9 100644 --- a/.trinity/seals/igla_own_model.json +++ b/.trinity/seals/igla_own_model.json @@ -7,7 +7,7 @@ }, { "spec": "specs/t27f/topic_engine.t27", - "spec_hash": "sha256:95337a0fe59f32426db6ca3a9481151c28f2b9eaddfa346659782e6d70ae5ff0" + "spec_hash": "sha256:d117a894beb6dc97ee678f84a927a98a801783d101b8b4cd96a0875979a911be" }, { "spec": "specs/t27f/topic_reel.t27", @@ -22,7 +22,7 @@ "module": "own_model", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T22:05:25Z", + "sealed_at": "2026-10-18T22:16:17Z", "sealed_by": "t27c-bootstrap@0.5.2", "spec_hash": "sha256:5a3d744947dc65b8c13d02a3ad58aa6c97f694f5459634110823788381a5ff80", "spec_path": "specs/igla/own_model.t27", diff --git a/.trinity/seals/igla_own_model_board.json b/.trinity/seals/igla_own_model_board.json index 21ac9c61d0..ac1609d402 100644 --- a/.trinity/seals/igla_own_model_board.json +++ b/.trinity/seals/igla_own_model_board.json @@ -11,7 +11,7 @@ }, { "spec": "specs/t27f/topic_engine.t27", - "spec_hash": "sha256:95337a0fe59f32426db6ca3a9481151c28f2b9eaddfa346659782e6d70ae5ff0" + "spec_hash": "sha256:d117a894beb6dc97ee678f84a927a98a801783d101b8b4cd96a0875979a911be" }, { "spec": "specs/t27f/topic_reel.t27", @@ -26,7 +26,7 @@ "module": "own_model_board", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T22:05:27Z", + "sealed_at": "2026-10-18T22:16:20Z", "sealed_by": "t27c-bootstrap@0.5.2", "spec_hash": "sha256:dabe2457877296de9097c66834d3a29ad66aa1862cc86fc8242ae9ab1acd39e5", "spec_path": "specs/igla/own_model_board.t27",