From 1b8d4f15ba9989fa282d12304504731761f73475 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 00:43:16 +0700 Subject: [PATCH 1/2] fpga(ax7203): RLC and 5-node ladder through the linear cell -- one board top for both circuits, bitstreams built, board run pending (Closes #10565) specs/fpga/analog_cell_ax7203.t27 (module FpgaAnalogCell) runs the series RLC and the 5-node RC ladder of specs/analog/linear.t27 on the AX7203, one run of 200 steps and one receipt line each, alternating. The machine is a serial shift-and-add multiply-accumulate over a ROM of the circuit's D and N words; the cell's pack, opposite, round_back, add_sm and fold are used as they are, by use. The PLL, UART frame and receipt fields are M0's, by use. 11 tests, 0 vacuous; the tests compare every state of every step with the cell's step. Fmax 106.30 MHz against 100 MHz (nextpnr-xilinx, xc7a200tfbg484-2). The board run and the UART captures are the follow-up, #10565: the build session could not reach USB or the serial port. Part of #10496. Co-Authored-By: Claude Sonnet 5.5 --- .trinity/seals/fpga_FpgaAnalogCell.json | 37 + specs/fpga/analog_cell_ax7203.t27 | 987 ++++++++++++++++++++++++ 2 files changed, 1024 insertions(+) create mode 100644 .trinity/seals/fpga_FpgaAnalogCell.json create mode 100644 specs/fpga/analog_cell_ax7203.t27 diff --git a/.trinity/seals/fpga_FpgaAnalogCell.json b/.trinity/seals/fpga_FpgaAnalogCell.json new file mode 100644 index 0000000000..d3ff6d1446 --- /dev/null +++ b/.trinity/seals/fpga_FpgaAnalogCell.json @@ -0,0 +1,37 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+9b556b7c3", + "closure": [ + { + "spec": "specs/analog/linear.t27", + "spec_hash": "sha256:3ddef7be183aba583ed285334ee389b48a65b41335e98914514235db7c4e5d62" + }, + { + "spec": "specs/fpga/rc_filter_ax7203.t27", + "spec_hash": "sha256:8fba8a419217ffe5dc6454759dd438d2236fb2cd829f9d64a3c2e15e3f44e51d" + } + ], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:82720a752019f679089c83012da03469a33e1d926aed3c1fb8834d85d048f8c7", + "gen_hash_rust": "sha256:58585b41c1243f7a1a80c46f0540f896a00bc282f029573adec866764824c579", + "gen_hash_verilog": "sha256:400e4cd5b90ca51eb4187847ad5912de497365f8e2ed5b75ed9124aec7dc0a73", + "gen_hash_zig": "sha256:1a1ab13f972fe545a593ab4c866076c0fb4220bb72075bf266644c4eb82833b3", + "module": "FpgaAnalogCell", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-18T16:51:49Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:9980520c7b863914ad4962b8f3841cb1729d00a0c88b02ae4831b2877ab2b652", + "spec_path": "specs/fpga/analog_cell_ax7203.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 11, + "total": 11, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/specs/fpga/analog_cell_ax7203.t27 b/specs/fpga/analog_cell_ax7203.t27 new file mode 100644 index 0000000000..2d962febdf --- /dev/null +++ b/specs/fpga/analog_cell_ax7203.t27 @@ -0,0 +1,987 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/fpga/analog_cell_ax7203.t27 -- the linear analog cell on the ALINX AX7203: a series RLC and a 5-node RC ladder +; M1b of the analog emulation epic (#10486, issue #10496). The cell is specs/analog/linear.t27 (#10487); the board +; plumbing is M0 (specs/fpga/rc_filter_ax7203.t27, #10276): the PLL, the UART frame and the receipt fields are M0's +; declarations and fns, brought in by `use`. What is written here is the machine that runs the cell's step on the fabric, +; and the two circuits' tables as a ROM. Everything hand-written is this file. +; - +; ONE TOP, TWO CIRCUITS. The machine is the same for every circuit: only the ROM (the circuit's D and N words), the +; state count, the state the receipt reports and the expected values change. The board runs the series RLC, prints its +; receipt line, runs the 5-node ladder, prints its line, and goes round again, so every line is a fresh run of 200 steps +; and the lines alternate RLC, LAD5, RLC, LAD5. Two copies of one machine would be two copies of one on_clock, which +; the dupe ratchet refuses (and which would drift); CK_FIRST and CK_LAST pick the circuits the board cycles through, so +; a build of one circuit alone is the same file with CK_FIRST = CK_LAST. +; - +; THE STEP (linear.t27). Every state, constant and input is an unsigned sign-magnitude word (bit 31 = negative, bits 0..30 +; the magnitude in units of 2^-24 V). One step is x_i' = x_i + rnd(sum_j D_ij x_j + N_i u): the positive terms add into +; one u64, the negative terms into another, one subtraction gives the magnitude and the direction, round_back rounds it +; half away from zero, add_sm adds it to the old state. The cell's scalar fns do that in one clock each; on the fabric +; each is split across clocks, and the tests prove the split gives the same word as the cell's next_x. +; - +; THE MACHINE. One term (a constant c times a state or the source x) at a time, rows in order, 200 steps: +; P_LOAD the ROM word c, the operand x, and the direction (opposite) of the product +; P_MUL shift-and-add over the bits of |x| until none is left: |c| << b is added into the positive or the negative +; register for every set bit b. This is the cell's prod, one bit a clock: no DSP slice (DSP48E1 with live +; operands reads wrong on openXC7, BENCHMARKS.md 4.4, so the flow is -nodsp) and no wide combinational multiplier +; P_CMP which register is larger P_SUB the difference P_RND round_back, and the old state +; P_PACK the direction P_ADD add_sm P_STORE the new state, the fold, A and B +; P_COMMIT all new states become the old ones, the next step. +; The clocks of a run depend on the bit lengths of the states, and are deterministic: the tests pin them (C). +; on_clock reads every register before it writes it, so the tests in this file and the clock edge agree. +; THE RESTART. The button and LOCKED pass M0's two registers. While they say no, the request flags `fin` and `hard` are set +; every clock, and the next clock puts the machine back to its start (circuit CK_FIRST, line 0). A finished line sets `fin` +; alone, and the next clock starts the next circuit. The flags are registers beside the logic they restart: in the first +; build the second synchroniser register drove the whole restart, sat by the pads, and failed 100 MHz on that wire. +; - +; THE CIRCUITS (the tables are linear.t27's, RLC_* and LAD5_*). Series RLC, R = 100 Ohm, L = 10 uH, C = 1 nF, dt = 5 ns, +; unknowns [node between R and L, capacitor voltage, inductor current * 100 Ohm]; A and B are the capacitor voltage after +; step 99 and step 199 (it rings: A is above 1 V). 5-node RC ladder, R = 1 kOhm and C = 1 nF per section, dt = 50 ns; +; A and B are the last node. S is the cell's fold over every state of every step, state by state. +; - +; THE RECEIPT. 115200 baud on N15, one line after each run, then the next circuit runs: +; T27 RLC A=<16 hex> B=<16 hex> S=<16 hex> C=<16 hex> L=<16 hex> PASS +; T27 LAD5 A=... (the same fields) +; L counts the lines since the button. PASS when A, B and S are the values linear.t27's run derives for that circuit, else +; FAIL. LEDs (active low) as M0: B13 the run is over, C13 FAIL, D14 PASS, D15 a heartbeat. The button T6 resets. +; - +; NEGATIVE CONTROLS. One coefficient one LSB off in one ROM word (RLC address 5, the capacitor's own D; ladder address +; 12): the cell's run on the changed table gives the A, B and S below, the tests assert they differ from the right ones +; and that the verdict is FAIL, and a build with that one literal changed prints exactly those values with FAIL. +; - +; WHAT A PASS SAYS. This board, running RTL generated from this file, ran the linear cell for 200 steps on each of the two +; circuits and produced the same states, bit for bit, as the cell's step in linear.t27 (the tests compare every state of +; every step), so its A, B and S are the cell's. By the cell's own tests those are within 9 LSB (RLC) and 41 LSB (ladder) +; of the double-precision backward Euler run of the same method. +; WHAT IT DOES NOT SAY. Nothing about power. Nothing about the continuous circuit: only about backward Euler at this dt. +; Nothing about another circuit: the tables are two of the cell's, and a netlist reader is M2. Nothing about real time: +; a run takes more clocks than the circuit has time. ASCII only, English only. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module FpgaAnalogCell; + +use analog::linear; +use fpga::rc_filter_ax7203; + +pub const KIND : str = "board-cell"; +pub const ID : str = "fpga/analog_cell_ax7203"; +pub const REFERENCE : str = "specs/analog/linear.t27, M0 specs/fpga/rc_filter_ax7203.t27"; +pub const BOARD : str = "ALINX AX7203"; +pub const PART : str = "xc7a200tfbg484-2"; + +; --- the circuits ------------------------------------------------------------------------------- +pub const CK_RLC : u8 = 0; +pub const CK_LAD5 : u8 = 1; +/// The board cycles through the circuits CK_FIRST .. CK_LAST, one run and one line each. +pub const CK_FIRST : u8 = 0; +pub const CK_LAST : u8 = 1; +pub const RLC_STATES : u8 = 3; +pub const LAD5_STATES : u8 = 5; +/// The state the receipt reports as A and B: the capacitor voltage, and the last node of the ladder. +pub const RLC_OUT : u8 = 1; +pub const LAD5_OUT : u8 = 4; + +; --- what the board must report, derived by the cell's run (the tests assert it) ------------------- +pub const RLC_EXP_A : u32 = 18050612; +pub const RLC_EXP_B : u32 = NEG | 1265689; +pub const LAD5_EXP_A : u32 = 2963590; +pub const LAD5_EXP_B : u32 = 4464373; +/// The clocks of a run, as the receipt's C field. +pub const RLC_CLOCKS : u32 = 56666; +pub const LAD5_CLOCKS : u32 = 139400; + +; --- the negative controls: one coefficient one LSB off ----------------------------------------------- +/// The index in linear.t27's D table, and the ROM address it has here (row * (n + 1) + column). +pub const RLC_FAULT_IDX : usize = 4; +pub const RLC_FAULT_ADDR : u8 = 5; +pub const LAD5_FAULT_IDX : usize = 10; +pub const LAD5_FAULT_ADDR : u8 = 12; +/// What the cell's run gives with that coefficient one LSB further from zero. +pub const RLC_BAD_A : u32 = 18050590; +pub const RLC_BAD_B : u32 = NEG | 1265681; +pub const RLC_BAD_S : u64 = 0x89932D8FBE407911; +pub const LAD5_BAD_A : u32 = 2963600; +pub const LAD5_BAD_B : u32 = 4464385; +pub const LAD5_BAD_S : u64 = 0x321615C52B5B23EA; + +; --- the machine -------------------------------------------------------------------------------- +pub const P_LOAD : u8 = 0; +pub const P_MUL : u8 = 1; +pub const P_CMP : u8 = 2; +pub const P_SUB : u8 = 3; +pub const P_RND : u8 = 4; +pub const P_PACK : u8 = 5; +pub const P_ADD : u8 = 6; +pub const P_STORE : u8 = 7; +pub const P_COMMIT : u8 = 8; + +; --- per-circuit facts -------------------------------------------------------------------------- + +/// The state count of circuit c. +pub fn nstates(c: u8) -> u8 { + if (c == CK_RLC) { return RLC_STATES; } + return LAD5_STATES; +} + +/// The state the receipt reports as A and B. +pub fn out_of(c: u8) -> u8 { + if (c == CK_RLC) { return RLC_OUT; } + return LAD5_OUT; +} + +/// The circuit after c: the last goes back to the first. +pub fn next_ck(c: u8) -> u8 { + if (c == CK_LAST) { return CK_FIRST; } + return c + 1; +} + +pub fn expect_a(c: u8) -> u32 { + if (c == CK_RLC) { return RLC_EXP_A; } + return LAD5_EXP_A; +} + +pub fn expect_b(c: u8) -> u32 { + if (c == CK_RLC) { return RLC_EXP_B; } + return LAD5_EXP_B; +} + +pub fn expect_s(c: u8) -> u64 { + if (c == CK_RLC) { return RLC_EXP_S; } + return LAD5_EXP_S; +} + +/// PASS when the run of circuit c gave its derived A, B and S. +pub fn verdict_for(c: u8, a: u32, b: u32, sm: u64) -> u8 { + if (a == expect_a(c) and b == expect_b(c) and sm == expect_s(c)) { return V_PASS; } + return V_FAIL; +} + +; --- the ROM: the circuit's words at address row * (n + 1) + column ------------------------------------ +; Row i is D_i0 .. D_i(n-1), then N_i. The words are linear.t27's RLC_D, RLC_NV, LAD5_D and LAD5_NV, spelled as they are +; there; `t27b verilog` lowers no array, so the table is an if-chain, and a test compares every word with the cell's. + +/// The series RLC (3 states, 4 words a row). +pub fn rom_rlc(a: u8) -> u32 { + if (a == 0) { return NEG | 16777216; } + if (a == 1) { return 797017; } + if (a == 2) { return NEG | 15940348; } + if (a == 3) { return 15980199; } + if (a == 4) { return 0; } + if (a == 5) { return NEG | 39851; } + if (a == 6) { return 797017; } + if (a == 7) { return 39851; } + if (a == 8) { return 0; } + if (a == 9) { return NEG | 797017; } + if (a == 10) { return NEG | 836868; } + if (a == 11) { return 797017; } + return 0; +} + +/// The 5-node ladder (5 states, 6 words a row). +pub fn rom_lad5(a: u8) -> u32 { + if (a == 0) { return NEG | 1493558; } + if (a == 1) { return 696153; } + if (a == 2) { return 31709; } + if (a == 3) { return 1444; } + if (a == 4) { return 69; } + if (a == 5) { return 764183; } + if (a == 6) { return 696153; } + if (a == 7) { return NEG | 1461849; } + if (a == 8) { return 697597; } + if (a == 9) { return 31778; } + if (a == 10) { return 1513; } + if (a == 11) { return 34808; } + if (a == 12) { return 31709; } + if (a == 13) { return 697597; } + if (a == 14) { return NEG | 1461780; } + if (a == 15) { return 697666; } + if (a == 16) { return 33222; } + if (a == 17) { return 1585; } + if (a == 18) { return 1444; } + if (a == 19) { return 31778; } + if (a == 20) { return 697666; } + if (a == 21) { return NEG | 1460336; } + if (a == 22) { return 729375; } + if (a == 23) { return 72; } + if (a == 24) { return 69; } + if (a == 25) { return 1513; } + if (a == 26) { return 33222; } + if (a == 27) { return 729375; } + if (a == 28) { return NEG | 764183; } + if (a == 29) { return 3; } + return 0; +} + +/// The ROM word of circuit c at address a. +pub fn rom(c: u8, a: u8) -> u32 { + if (c == CK_RLC) { return rom_rlc(a); } + return rom_lad5(a); +} + +; --- the operands and the finish ------------------------------------------------------------------- + +/// Operand k of a row: state k, or the source u when k is the state count. +pub fn pick(k: u8, n: u8, s0: u32, s1: u32, s2: u32, s3: u32, s4: u32, u: u32) -> u32 { + if (k == n) { return u; } + if (k == 0) { return s0; } + if (k == 1) { return s1; } + if (k == 2) { return s2; } + if (k == 3) { return s3; } + return s4; +} + +/// The magnitude of the difference of the two registers, the larger one first. +pub fn diff_mag(big_first: bool, p: u64, q: u64) -> u64 { + if (big_first) { return p - q; } + return q - p; +} + +; --- the receipt: M0's line, with a prefix per circuit ------------------------------------------------ + +/// The length of the circuit's name: RLC, LAD5. +pub fn name_len(c: u8) -> u8 { + if (c == CK_RLC) { return 3; } + return 4; +} + +/// Character p of "T27 RLC" or "T27 LAD5". +pub fn name_char(c: u8, p: u8) -> u8 { + if (p < 4) { return prefix_char(p); } + if (c == CK_RLC) { + if (p == 4) { return 82; } + if (p == 5) { return 76; } + return 67; + } + if (p == 4) { return 76; } + if (p == 5) { return 65; } + if (p == 6) { return 68; } + return 53; +} + +/// The last position of segment s: the prefix has the circuit's name, every other segment is M0's. +pub fn seg_end(c: u8, s: u8) -> u8 { + if (s == 0) { return 3 + name_len(c); } + return seg_last(s); +} + +/// The character at segment s, position p of the line of circuit c. +pub fn next_char(c: u8, s: u8, p: u8, f: u64, v: u8) -> u8 { + if (s == 0) { return name_char(c, p); } + return line_char(s, p, f, v); +} + +; --- 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 pins in -------------------------------------------------------------------------------- +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"; + +; --- the clock and the reset: M0's, unchanged --------------------------------------------------- +const clkbuf : IbufdsOut = IBUFDS(clk200_p, clk200_n); +const clkbuf_O_PERIOD_PS : u32 = 5000; +const pll : PllOut = PLLE2_ADV(clkbuf.O, pll.CLKFBOUT, false, false, 5.0, 0.01, 8, 1, 16, 0, "FALSE"); +const gclk : BufgOut = BUFG(pll.CLKOUT0); +const gclk_O_PERIOD_PS : u32 = 10000; + +const btn : IbufOut = IBUF(cpu_reset_n); + +// No asynchronous reset: the button and LOCKED pass two registers (M0's), they set the restart request, and on the next +// edge on_clock puts every register back to its start (M0, where an async clear printed C=1199). +const clk : bool = gclk.O; +const rst_n : bool = true; +const en : bool = true; + +; --- the registers ------------------------------------------------------------------------------ +var st : u8 = 0; +var ph : u8 = 0; +var ck : u8 = 0; +var ri : u8 = 0; +var ti : u8 = 0; +var ra : u8 = 0; +var step_n : u8 = 0; +var x0 : u32 = 0; +var x1 : u32 = 0; +var x2 : u32 = 0; +var x3 : u32 = 0; +var x4 : u32 = 0; +var y0 : u32 = 0; +var y1 : u32 = 0; +var y2 : u32 = 0; +var y3 : u32 = 0; +var y4 : u32 = 0; +var mc : u64 = 0; +var mr : u32 = 0; +var opp : bool = false; +var accp : u64 = 0; +var accn : u64 = 0; +var ge : bool = false; +var dmag : u64 = 0; +var rnd : u32 = 0; +var xi : u32 = 0; +var dword : u32 = 0; +var ynew : u32 = 0; +var cs : u64 = 0; +var va : u32 = 0; +var vb : u32 = 0; +var cyc : u32 = 0; +var verdict : u8 = 1; +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 upos : u8 = 0; +var fsr : u64 = 0; +var lines : u32 = 0; +var last : bool = false; +var hard : bool = false; +var fin : bool = false; +var hb : u32 = 0; +var go0 : bool = false; +var go1 : bool = false; + +; --- the pins out: registers, set from the state one clock later (a pub var is an output reg) ---- +pub var uart_tx : bool = true; +const uart_tx_LOC : str = "N15"; +const uart_tx_IOSTANDARD : str = "LVCMOS33"; +pub var led_0 : bool = true; +const led_0_LOC : str = "B13"; +const led_0_IOSTANDARD : str = "LVCMOS33"; +pub var led_1 : bool = true; +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"; + +// Every var is read before it is written, so the test's order and the clock edge agree. +fn on_clock(pll_LOCKED: bool, btn_O: bool) { + uart_tx = st != ST_REPORT or (tx_sh & 1) == 1; + led_0 = st != ST_REPORT; + led_1 = !(st == ST_REPORT and verdict == V_FAIL); + led_2 = !(st == ST_REPORT and verdict == V_PASS); + led_3 = ((hb >> 27) & 1) == 1; + hb = hb + 1; + if (fin) { + if (hard) { + ck = CK_FIRST; + lines = 0; + hard = false; + } else { + ck = next_ck(ck); + } + st = ST_RUN; + ph = P_LOAD; + ri = 0; + ti = 0; + ra = 0; + step_n = 0; + x0 = 0; + x1 = 0; + x2 = 0; + x3 = 0; + x4 = 0; + accp = 0; + accn = 0; + cs = 0; + cyc = 0; + va = 0; + vb = 0; + verdict = V_FAIL; + tx_cnt = 0; + tx_sh = 1023; + tx_left = 0; + seg = 0; + upos = 0; + fsr = 0; + last = false; + fin = false; + } else if (st == ST_RUN) { + cyc = cyc + 1; + if (ph == P_LOAD) { + mc = (rom(ck, ra) & MAG) as u64; + mr = pick(ti, nstates(ck), x0, x1, x2, x3, x4, vin_at(step_n as u32)) & MAG; + opp = opposite(rom(ck, ra), pick(ti, nstates(ck), x0, x1, x2, x3, x4, vin_at(step_n as u32))); + ph = P_MUL; + } else if (ph == P_MUL) { + if (mr == 0) { + if (ti == nstates(ck)) { + ph = P_CMP; + } else { + ti = ti + 1; + ra = ra + 1; + ph = P_LOAD; + } + } else { + if ((mr & 1) == 1) { + if (opp) { + accn = accn + mc; + } else { + accp = accp + mc; + } + } + mc = mc << 1; + mr = mr >> 1; + } + } else if (ph == P_CMP) { + ge = accp >= accn; + ph = P_SUB; + } else if (ph == P_SUB) { + dmag = diff_mag(ge, accp, accn); + ph = P_RND; + } else if (ph == P_RND) { + rnd = round_back(dmag); + xi = pick(ri, nstates(ck), x0, x1, x2, x3, x4, 0); + ph = P_PACK; + } else if (ph == P_PACK) { + dword = pack(rnd, !ge); + ph = P_ADD; + } else if (ph == P_ADD) { + ynew = add_sm(xi, dword); + ph = P_STORE; + } else if (ph == P_STORE) { + cs = fold(cs, ynew); + if (ri == 0) { + y0 = ynew; + } else if (ri == 1) { + y1 = ynew; + } else if (ri == 2) { + y2 = ynew; + } else if (ri == 3) { + y3 = ynew; + } else { + y4 = ynew; + } + if (ri == out_of(ck)) { + if ((step_n as u32) == CHARGE_STEPS - 1) { va = ynew; } + if ((step_n as u32) == STEPS - 1) { vb = ynew; } + } + accp = 0; + accn = 0; + ti = 0; + ra = ra + 1; + if (ri == nstates(ck) - 1) { + ph = P_COMMIT; + } else { + ri = ri + 1; + ph = P_LOAD; + } + } else { + x0 = y0; + x1 = y1; + x2 = y2; + x3 = y3; + x4 = y4; + if ((step_n as u32) == STEPS - 1) { st = ST_JUDGE; } + step_n = step_n + 1; + ri = 0; + ra = 0; + ph = P_LOAD; + } + } else if (st == ST_JUDGE) { + verdict = verdict_for(ck, va, vb, cs); + st = ST_REPORT; + } else { + if (tx_cnt != 0) { + tx_cnt = tx_cnt - 1; + } else { + tx_cnt = baud_div - 1; + if (tx_left != 0) { + if (last and tx_left == 1) { fin = true; } + tx_sh = (tx_sh >> 1) | 512; + tx_left = tx_left - 1; + } else { + tx_sh = frame(next_char(ck, seg, upos, fsr, verdict)); + tx_left = 9; + if (upos == seg_end(ck, seg)) { + fsr = field(seg + 1, va, vb, cs, cyc, lines); + upos = 0; + if (seg == LINE_SEGS - 1) { + seg = 0; + lines = lines + 1; + last = true; + } else { + seg = seg + 1; + } + } else { + if (seg != 0 and seg != LINE_SEGS - 1 and upos >= 3) { fsr = fsr << 4; } + upos = upos + 1; + } + } + } + } + if (!go1) { + fin = true; + hard = true; + } + go1 = go0; + go0 = pll_LOCKED and btn_O; +} + +; --- test-only helpers (the hardware does not reach them) ---------------------------------------------- + +/// The machine as the button leaves it, then circuit first selected (the start of a run). +fn boot(first: u8) { + go0 = true; + go1 = false; + on_clock(true, true); + on_clock(true, true); + ck = first; +} + +/// How many ROM words of circuit c differ from the cell's D (n * n, row-major) and N tables. +fn rom_bad(c: u8, n: usize, d: []const u32, nv: []const u32) -> u32 { + var bad : u32 = 0; + var i : usize = 0; + var j : usize = 0; + while (i < n) { + j = 0; + while (j < n) { + if (rom(c, (i * (n + 1) + j) as u8) != d[i * n + j]) { bad = bad + 1; } + j = j + 1; + } + if (rom(c, (i * (n + 1) + n) as u8) != nv[i]) { bad = bad + 1; } + i = i + 1; + } + return bad; +} + +/// Runs the machine from reset on circuit c, beside the cell's step on the tables d and nv, and counts the words where +/// they differ: every state after every step, and the fold after every step. The machine is left at ST_JUDGE. +fn board_vs_cell(c: u8, n: usize, d: []const u32, nv: []const u32) -> u32 { + boot(c); + var xr : [5]u32 = [0] ** 5; + var yr : [5]u32 = [0] ** 5; + var folded : u64 = 0; + var bad : u32 = 0; + var t : u32 = 0; + var i : usize = 0; + while (t < STEPS) { + step(n, d, nv, &xr, vin_at(t), &yr); + i = 0; + while (i < n) { + folded = fold(folded, yr[i]); + i = i + 1; + } + while ((step_n as u32) == t and st == ST_RUN) { on_clock(true, true); } + i = 0; + while (i < n) { + if (pick(i as u8, 255, x0, x1, x2, x3, x4, 0) != yr[i]) { bad = bad + 1; } + xr[i] = yr[i]; + i = i + 1; + } + if (cs != folded) { bad = bad + 1; } + t = t + 1; + } + return bad; +} + +/// The accumulators after the finish phases run on p, q and an old state of x0 (the machine's P_CMP .. P_ADD). +fn finish_row(p: u64, q: u64, old: u32) -> u32 { + boot(CK_RLC); + accp = p; + accn = q; + x0 = old; + ri = 0; + ph = P_CMP; + while (ph != P_STORE) { on_clock(true, true); } + return ynew; +} + +/// The value of one hex digit, 0-9 A-F. +fn hex_val(ch: u8) -> u64 { + if (ch >= 65) { return (ch - 55) as u64; } + return (ch - 48) as u64; +} + +/// The 16 hex digits of buf from position at. +fn hex_run(buf: []const u8, at: usize) -> u64 { + var v : u64 = 0; + var k : usize = 0; + while (k < 16) { + v = (v << 4) | hex_val(buf[at + k]); + k = k + 1; + } + return v; +} + +; --- the tests ---------------------------------------------------------------------------------- + +test the_rom_is_the_cells_tables_word_for_word_and_sees_one_lsb { + assert_eq(rom_bad(CK_RLC, RLC_N, &RLC_D, &RLC_NV), 0); + assert_eq(rom_bad(CK_LAD5, LAD5_N, &LAD5_D, &LAD5_NV), 0); + var dr : [9]u32 = RLC_D; + dr[RLC_FAULT_IDX] = dr[RLC_FAULT_IDX] + 1; + assert_eq(rom_bad(CK_RLC, RLC_N, &dr, &RLC_NV), 1); + var dl5 : [25]u32 = LAD5_D; + dl5[LAD5_FAULT_IDX] = dl5[LAD5_FAULT_IDX] + 1; + assert_eq(rom_bad(CK_LAD5, LAD5_N, &dl5, &LAD5_NV), 1); + var nr : [3]u32 = RLC_NV; + nr[2] = nr[2] + 1; + assert_eq(rom_bad(CK_RLC, RLC_N, &RLC_D, &nr), 1); + // the fault addresses are the faulty words' places in the ROM: row * (n + 1) + column + assert_eq(RLC_FAULT_ADDR as usize, (RLC_FAULT_IDX / RLC_N) * (RLC_N + 1) + RLC_FAULT_IDX % RLC_N); + assert_eq(LAD5_FAULT_ADDR as usize, (LAD5_FAULT_IDX / LAD5_N) * (LAD5_N + 1) + LAD5_FAULT_IDX % LAD5_N); + assert_eq(rom_rlc(RLC_FAULT_ADDR), NEG | 39851); + assert_eq(rom_lad5(LAD5_FAULT_ADDR), 31709); +} + +test the_circuit_facts_agree_with_the_cell { + assert_eq(RLC_STATES as usize, RLC_N); + assert_eq(LAD5_STATES as usize, LAD5_N); + assert_eq(nstates(CK_RLC), 3); + assert_eq(nstates(CK_LAD5), 5); + assert_eq(out_of(CK_RLC), 1); + assert_eq(out_of(CK_LAD5), 4); + assert_eq(next_ck(CK_RLC), CK_LAD5); + assert_eq(next_ck(CK_LAD5), CK_RLC); + assert_eq(expect_s(CK_RLC), RLC_EXP_S); + assert_eq(expect_s(CK_LAD5), LAD5_EXP_S); + assert_eq(RLC_EXP_B & MAG, 1265689); + assert(is_neg(RLC_EXP_B)); + // the right values pass, and each of A, B, S alone being wrong fails, for both circuits and across them + assert_eq(verdict_for(CK_RLC, RLC_EXP_A, RLC_EXP_B, RLC_EXP_S), V_PASS); + assert_eq(verdict_for(CK_RLC, RLC_EXP_A + 1, RLC_EXP_B, RLC_EXP_S), V_FAIL); + assert_eq(verdict_for(CK_RLC, RLC_EXP_A, RLC_EXP_B + 1, RLC_EXP_S), V_FAIL); + assert_eq(verdict_for(CK_RLC, RLC_EXP_A, RLC_EXP_B, RLC_EXP_S ^ 1), V_FAIL); + assert_eq(verdict_for(CK_LAD5, LAD5_EXP_A, LAD5_EXP_B, LAD5_EXP_S), V_PASS); + assert_eq(verdict_for(CK_LAD5, LAD5_EXP_A + 1, LAD5_EXP_B, LAD5_EXP_S), V_FAIL); + assert_eq(verdict_for(CK_LAD5, LAD5_EXP_A, LAD5_EXP_B + 1, LAD5_EXP_S), V_FAIL); + assert_eq(verdict_for(CK_LAD5, LAD5_EXP_A, LAD5_EXP_B, LAD5_EXP_S ^ 1), V_FAIL); + assert_eq(verdict_for(CK_LAD5, RLC_EXP_A, RLC_EXP_B, RLC_EXP_S), V_FAIL); + assert_eq(verdict_for(CK_RLC, LAD5_EXP_A, LAD5_EXP_B, LAD5_EXP_S), V_FAIL); +} + +test the_expected_values_are_what_the_cells_run_derives { + const mn_rlc : [30]f64 = derive(&RLC_KIND, &RLC_A, &RLC_B, &RLC_VAL, RLC_NE, RLC_DT, RLC_ZS); + var xa : [5]u32 = [0] ** 5; + var xb : [5]u32 = [0] ** 5; + const ca : RunOut = run(RLC_N, &RLC_D, &RLC_NV, &mn_rlc, CHARGE_STEPS, &xa); + const cb : RunOut = run(RLC_N, &RLC_D, &RLC_NV, &mn_rlc, STEPS, &xb); + assert_eq(xa[RLC_OUT as usize], RLC_EXP_A); + assert_eq(xb[RLC_OUT as usize], RLC_EXP_B); + assert_eq(cb.sig, RLC_EXP_S); + assert ca.worst < (RLC_MAX_ERR_LSB as f64); + assert cb.worst < (RLC_MAX_ERR_LSB as f64); + // the capacitor rings above 1 V at 5 us, and the inductor current changes sign + assert(xa[RLC_OUT as usize] > ONE); + assert(is_neg(xb[RLC_OUT as usize])); + const m5 : [30]f64 = derive(&LAD5_KIND, &LAD5_A, &LAD5_B, &LAD5_VAL, LAD5_NE, LAD5_DT, LAD5_ZS); + var ya : [5]u32 = [0] ** 5; + var yb : [5]u32 = [0] ** 5; + const da : RunOut = run(LAD5_N, &LAD5_D, &LAD5_NV, &m5, CHARGE_STEPS, &ya); + const db : RunOut = run(LAD5_N, &LAD5_D, &LAD5_NV, &m5, STEPS, &yb); + assert_eq(ya[LAD5_OUT as usize], LAD5_EXP_A); + assert_eq(yb[LAD5_OUT as usize], LAD5_EXP_B); + assert_eq(db.sig, LAD5_EXP_S); + assert da.worst < (LAD5_MAX_ERR_LSB as f64); + assert db.worst < (LAD5_MAX_ERR_LSB as f64); +} + +test the_serial_multiplier_adds_what_the_cells_term_adds { + boot(CK_RLC); + const cs_tab : [10]u32 = [NEG | 797017, 797017, NEG | 1, 0, 7, MAG, ONE, NEG | ONE, 15940348, NEG | 39851]; + const xs_tab : [10]u32 = [18050612, NEG | 123456, NEG | 1, 5, 0, MAG, ONE, MAG, 67108863, 1]; + var k : usize = 0; + var clocks : u32 = 0; + while (k < 10) { + ph = P_MUL; + accp = 0; + accn = 0; + mc = (cs_tab[k] & MAG) as u64; + mr = xs_tab[k] & MAG; + opp = opposite(cs_tab[k], xs_tab[k]); + ti = 0; + clocks = 0; + while (ph == P_MUL) { + on_clock(true, true); + clocks = clocks + 1; + } + assert_eq(accp, pos_after(0, cs_tab[k], xs_tab[k])); + assert_eq(accn, neg_after(0, cs_tab[k], xs_tab[k])); + assert_eq(accp + accn, prod(cs_tab[k], xs_tab[k])); + k = k + 1; + } + // zero takes the one clock that finds no bit; ONE (25 bits) takes 25 + 1 + ph = P_MUL; + mc = 5; + mr = 0; + opp = false; + ti = 0; + clocks = 0; + while (ph == P_MUL) { + on_clock(true, true); + clocks = clocks + 1; + } + assert_eq(clocks, 1); + ph = P_MUL; + mc = 5; + mr = ONE; + ti = 0; + clocks = 0; + while (ph == P_MUL) { + on_clock(true, true); + clocks = clocks + 1; + } + assert_eq(clocks, 26); +} + +test the_finish_phases_equal_the_cells_next_x { + // half an LSB rounds away from zero, both ways; equal registers give zero; a negative old state; a carry across zero + assert_eq(finish_row(8388608, 0, 5), next_x(5, 8388608, 0)); + assert_eq(finish_row(0, 8388608, 5), next_x(5, 0, 8388608)); + assert_eq(finish_row(8388607, 0, 5), 5); + assert_eq(finish_row(5, 5, NEG | 9), NEG | 9); + assert_eq(finish_row(0, 8388608, 0), NEG | 1); + assert_eq(finish_row(25165824, 8388608, NEG | 3), next_x(NEG | 3, 25165824, 8388608)); + assert_eq(finish_row(1099511627776, 3, 1000), next_x(1000, 1099511627776, 3)); + assert_eq(finish_row(3, 1099511627776, NEG | 1000), next_x(NEG | 1000, 3, 1099511627776)); + assert_eq(finish_row(33554432, 0, NEG | 1), next_x(NEG | 1, 33554432, 0)); + assert_eq(finish_row(0, 33554432, 1), next_x(1, 0, 33554432)); + assert_eq(diff_mag(true, 9, 4), 5); + assert_eq(diff_mag(false, 4, 9), 5); +} + +test the_board_machine_runs_the_rlc_like_the_cell { + const mn : [30]f64 = derive(&RLC_KIND, &RLC_A, &RLC_B, &RLC_VAL, RLC_NE, RLC_DT, RLC_ZS); + assert_eq(board_vs_cell(CK_RLC, RLC_N, &RLC_D, &RLC_NV), 0); + assert_eq(st, ST_JUDGE); + assert_eq(step_n as u32, STEPS); + var xa : [5]u32 = [0] ** 5; + var xb : [5]u32 = [0] ** 5; + const ca : RunOut = run(RLC_N, &RLC_D, &RLC_NV, &mn, CHARGE_STEPS, &xa); + const cb : RunOut = run(RLC_N, &RLC_D, &RLC_NV, &mn, STEPS, &xb); + assert_eq(va, xa[RLC_OUT as usize]); + assert_eq(vb, xb[RLC_OUT as usize]); + assert_eq(cs, cb.sig); + assert_eq(va, RLC_EXP_A); + assert_eq(vb, RLC_EXP_B); + assert_eq(cs, RLC_EXP_S); + assert_eq(cyc, RLC_CLOCKS); + assert ca.peak < HEADROOM; + on_clock(true, true); + assert_eq(st, ST_REPORT); + assert_eq(verdict, V_PASS); +} + +test the_board_machine_runs_the_ladder_like_the_cell { + const mn : [30]f64 = derive(&LAD5_KIND, &LAD5_A, &LAD5_B, &LAD5_VAL, LAD5_NE, LAD5_DT, LAD5_ZS); + assert_eq(board_vs_cell(CK_LAD5, LAD5_N, &LAD5_D, &LAD5_NV), 0); + assert_eq(st, ST_JUDGE); + assert_eq(step_n as u32, STEPS); + var xa : [5]u32 = [0] ** 5; + var xb : [5]u32 = [0] ** 5; + const ca : RunOut = run(LAD5_N, &LAD5_D, &LAD5_NV, &mn, CHARGE_STEPS, &xa); + const cb : RunOut = run(LAD5_N, &LAD5_D, &LAD5_NV, &mn, STEPS, &xb); + assert_eq(va, xa[LAD5_OUT as usize]); + assert_eq(vb, xb[LAD5_OUT as usize]); + assert_eq(cs, cb.sig); + assert_eq(va, LAD5_EXP_A); + assert_eq(vb, LAD5_EXP_B); + assert_eq(cs, LAD5_EXP_S); + assert_eq(cyc, LAD5_CLOCKS); + assert ca.peak < HEADROOM; + on_clock(true, true); + assert_eq(st, ST_REPORT); + assert_eq(verdict, V_PASS); +} + +test one_lsb_in_one_coefficient_changes_a_b_and_s_and_fails { + const mn : [30]f64 = derive(&RLC_KIND, &RLC_A, &RLC_B, &RLC_VAL, RLC_NE, RLC_DT, RLC_ZS); + var dr : [9]u32 = RLC_D; + dr[RLC_FAULT_IDX] = dr[RLC_FAULT_IDX] + 1; + var xa : [5]u32 = [0] ** 5; + var xb : [5]u32 = [0] ** 5; + const ca : RunOut = run(RLC_N, &dr, &RLC_NV, &mn, CHARGE_STEPS, &xa); + const cb : RunOut = run(RLC_N, &dr, &RLC_NV, &mn, STEPS, &xb); + assert_eq(xa[RLC_OUT as usize], RLC_BAD_A); + assert_eq(xb[RLC_OUT as usize], RLC_BAD_B); + assert_eq(cb.sig, RLC_BAD_S); + assert(RLC_BAD_A != RLC_EXP_A); + assert(RLC_BAD_B != RLC_EXP_B); + assert(RLC_BAD_S != RLC_EXP_S); + assert_eq(verdict_for(CK_RLC, RLC_BAD_A, RLC_BAD_B, RLC_BAD_S), V_FAIL); + // the machine, whose ROM is the right table, disagrees with the cell run on the faulty one + assert(board_vs_cell(CK_RLC, RLC_N, &dr, &RLC_NV) > 0); + assert(cs != RLC_BAD_S); + const m5 : [30]f64 = derive(&LAD5_KIND, &LAD5_A, &LAD5_B, &LAD5_VAL, LAD5_NE, LAD5_DT, LAD5_ZS); + var dl5 : [25]u32 = LAD5_D; + dl5[LAD5_FAULT_IDX] = dl5[LAD5_FAULT_IDX] + 1; + var ya : [5]u32 = [0] ** 5; + var yb : [5]u32 = [0] ** 5; + const da : RunOut = run(LAD5_N, &dl5, &LAD5_NV, &m5, CHARGE_STEPS, &ya); + const db : RunOut = run(LAD5_N, &dl5, &LAD5_NV, &m5, STEPS, &yb); + assert_eq(ya[LAD5_OUT as usize], LAD5_BAD_A); + assert_eq(yb[LAD5_OUT as usize], LAD5_BAD_B); + assert_eq(db.sig, LAD5_BAD_S); + assert(LAD5_BAD_A != LAD5_EXP_A); + assert(LAD5_BAD_B != LAD5_EXP_B); + assert(LAD5_BAD_S != LAD5_EXP_S); + assert_eq(verdict_for(CK_LAD5, LAD5_BAD_A, LAD5_BAD_B, LAD5_BAD_S), V_FAIL); + assert(board_vs_cell(CK_LAD5, LAD5_N, &dl5, &LAD5_NV) > 0); + assert(cs != LAD5_BAD_S); +} + +test the_run_starts_after_lock_and_button_and_restarts_on_the_button { + go0 = false; + go1 = false; + st = ST_REPORT; + cyc = 77; + lines = 5; + ck = CK_LAD5; + on_clock(false, true); + on_clock(true, false); + on_clock(false, false); + assert_eq(st, ST_RUN); + assert_eq(cyc, 0); + assert_eq(lines, 0); + assert_eq(ck, CK_FIRST); + on_clock(true, true); + assert_eq(cyc, 0); + on_clock(true, true); + assert_eq(cyc, 0); + on_clock(true, true); + assert_eq(cyc, 0); + on_clock(true, true); + assert_eq(cyc, 1); + var k : u32 = 0; + while (st != ST_REPORT) { + on_clock(true, true); + k = k + 1; + } + assert_eq(k, RLC_CLOCKS); + assert_eq(cyc, RLC_CLOCKS); + assert_eq(verdict, V_PASS); + on_clock(true, false); + on_clock(true, true); + on_clock(true, true); + assert_eq(st, ST_REPORT); + on_clock(true, true); + assert_eq(st, ST_RUN); + assert_eq(cyc, 0); + assert_eq(lines, 0); + assert_eq(verdict, V_FAIL); +} + +test the_pins_show_the_state_one_clock_later { + go0 = true; + go1 = true; + last = false; + fin = false; + st = ST_REPORT; + verdict = V_PASS; + tx_sh = 1022; + tx_cnt = 5; + hb = 0x08000000; + on_clock(true, true); + assert(!uart_tx); + assert(!led_0); + assert(led_1); + assert(!led_2); + assert(led_3); + verdict = V_FAIL; + tx_sh = 1023; + on_clock(true, true); + assert(uart_tx); + assert(!led_1); + assert(led_2); + st = ST_JUDGE; + on_clock(true, true); + assert(uart_tx); + assert(led_0); + assert(led_1); +} + +test the_board_prints_passing_receipts_for_both_circuits_in_turn { + boot(CK_FIRST); + baud_div = 1; + var buf : [128]u8 = [0] ** 128; + var got : usize = 0; + var line : u32 = 0; + var ch : u8 = 0; + var ticks : u32 = 0; + var plen : usize = 0; + var ea : u32 = 0; + var eb : u32 = 0; + var es : u64 = 0; + var ec : u32 = 0; + var fld : usize = 0; + var at : usize = 0; + while (line < 4 and ticks < 2000000) { + on_clock(true, true); + ticks = ticks + 1; + if (st == ST_REPORT and tx_left == 9) { + ch = ((tx_sh >> 1) & 255) as u8; + buf[got] = ch; + got = got + 1; + if (ch == 10) { + if (line % 2 == 0) { + plen = 7; + ea = RLC_EXP_A; + eb = RLC_EXP_B; + es = RLC_EXP_S; + ec = RLC_CLOCKS; + assert_eq(buf[4], 82); + assert_eq(buf[5], 76); + assert_eq(buf[6], 67); + } else { + plen = 8; + ea = LAD5_EXP_A; + eb = LAD5_EXP_B; + es = LAD5_EXP_S; + ec = LAD5_CLOCKS; + assert_eq(buf[4], 76); + assert_eq(buf[5], 65); + assert_eq(buf[6], 68); + assert_eq(buf[7], 53); + } + assert_eq(got, plen + 102); + assert_eq(buf[0], 84); + assert_eq(buf[1], 50); + assert_eq(buf[2], 55); + assert_eq(buf[3], 32); + fld = 0; + while (fld < 5) { + at = plen + fld * 19; + assert_eq(buf[at], 32); + assert_eq(buf[at + 2], 61); + fld = fld + 1; + } + assert_eq(buf[plen + 1], 65); + assert_eq(buf[plen + 20], 66); + assert_eq(buf[plen + 39], 83); + assert_eq(buf[plen + 58], 67); + assert_eq(buf[plen + 77], 76); + assert_eq(hex_run(&buf, plen + 3), ea as u64); + assert_eq(hex_run(&buf, plen + 22), eb as u64); + assert_eq(hex_run(&buf, plen + 41), es); + assert_eq(hex_run(&buf, plen + 60), ec as u64); + assert_eq(hex_run(&buf, plen + 79), line as u64); + assert_eq(buf[plen + 95], 32); + assert_eq(buf[plen + 96], 80); + assert_eq(buf[plen + 97], 65); + assert_eq(buf[plen + 98], 83); + assert_eq(buf[plen + 99], 83); + assert_eq(buf[plen + 100], 13); + got = 0; + line = line + 1; + } + } + } + assert_eq(line, 4); + assert_eq(lines, 4); + baud_div = BAUD_DIV; +} From b773546ac7d09e2e250aae379b749c140a179115 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 08:12:25 +0700 Subject: [PATCH 2/2] fpga: board_receipt's beat checksum is fold_beat, so the analog cell's board top keeps its fold (Closes #10565) specs/fpga/board_receipt.t27 (#10475) declared a five-argument `fold`. rc_filter_ax7203.t27 imports it, and rc_filter_ax7203.t27 and specs/analog/linear.t27 both declare a two-argument `fold`. use_resolve.rs leaves a name that two modules of one import closure declare differently unresolved, so specs/fpga/analog_cell_ax7203.t27 (which imports linear and rc_filter_ax7203) stopped compiling after master merged: "use of undeclared identifier 'fold'". board_receipt's own header says it declares no name a board spec also defines; the rename makes that true. - board_receipt, ddr3_head_bandwidth, ddr3_ternary_matvec, tern9m_l0_k_weights: every call is the five-argument beat checksum; renamed to fold_beat, bodies unchanged. - Tests: board_receipt 4/4, rc_filter_ax7203 10/10, tern9m_l0_k_weights 5/5, ddr3_head_bandwidth 12/12, ddr3_ternary_matvec 10/10, analog_cell_ax7203 11/11, 0 vacuous each (t27c test-report). - Resealed the four renamed specs, rc_filter_ax7203 (its closure names board_receipt) and analog_cell_ax7203 (toolchain); seal --verify all MATCH. Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/fpga_FpgaAnalogCell.json | 8 +++--- .trinity/seals/fpga_FpgaBoardReceipt.json | 16 ++++++------ .../seals/fpga_FpgaDdr3HeadBandwidth.json | 18 ++++++------- .../seals/fpga_FpgaDdr3TernaryMatvec.json | 18 ++++++------- .trinity/seals/fpga_FpgaRcFilter.json | 8 +++--- .trinity/seals/fpga_FpgaTern9mL0KWeights.json | 20 +++++++-------- specs/fpga/board_receipt.t27 | 25 +++++++++++-------- specs/fpga/ddr3_head_bandwidth.t27 | 20 +++++++-------- specs/fpga/ddr3_ternary_matvec.t27 | 16 ++++++------ specs/fpga/tern9m_l0_k_weights.t27 | 4 +-- 10 files changed, 78 insertions(+), 75 deletions(-) diff --git a/.trinity/seals/fpga_FpgaAnalogCell.json b/.trinity/seals/fpga_FpgaAnalogCell.json index d3ff6d1446..a349a4bb81 100644 --- a/.trinity/seals/fpga_FpgaAnalogCell.json +++ b/.trinity/seals/fpga_FpgaAnalogCell.json @@ -1,5 +1,5 @@ { - "built_by": "t27c-bootstrap@0.5.2+9b556b7c3", + "built_by": "t27c-bootstrap@0.5.2+ea35d9b72", "closure": [ { "spec": "specs/analog/linear.t27", @@ -7,7 +7,7 @@ }, { "spec": "specs/fpga/rc_filter_ax7203.t27", - "spec_hash": "sha256:8fba8a419217ffe5dc6454759dd438d2236fb2cd829f9d64a3c2e15e3f44e51d" + "spec_hash": "sha256:be3af1aa6195d51e46289121cfd42623c80cd42d863442f4f6f69109da06d32f" } ], "config": "gen=c,rust,verilog,zig;tests=zig", @@ -18,7 +18,7 @@ "module": "FpgaAnalogCell", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T16:51:49Z", + "sealed_at": "2026-10-19T01:11:30Z", "sealed_by": "t27c-bootstrap@0.5.2", "spec_hash": "sha256:9980520c7b863914ad4962b8f3841cb1729d00a0c88b02ae4831b2877ab2b652", "spec_path": "specs/fpga/analog_cell_ax7203.t27", @@ -31,7 +31,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/fpga_FpgaBoardReceipt.json b/.trinity/seals/fpga_FpgaBoardReceipt.json index a82356f7aa..492181f7ee 100644 --- a/.trinity/seals/fpga_FpgaBoardReceipt.json +++ b/.trinity/seals/fpga_FpgaBoardReceipt.json @@ -1,17 +1,17 @@ { - "built_by": "t27c-bootstrap@0.5.2+a86b691b1", + "built_by": "t27c-bootstrap@0.5.2+ea35d9b72", "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", + "gen_hash_c": "sha256:d139e6c20f6e0ec7b82695f7d2129db82a790ce33469bf1f4cad5b232dbe5e07", + "gen_hash_rust": "sha256:8f229651558403c6f383bf5821e3bdd69fb19e21584e31ba9f55b0c328ac9119", + "gen_hash_verilog": "sha256:8a67141169339e2c4532917bbd174e4503b114b7825e73bed7c62bf2564c4a97", + "gen_hash_zig": "sha256:ef4c8fc51db4c3d9430be665982556fce21adcd53243c847affb26419368a767", "module": "FpgaBoardReceipt", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T13:56:40Z", + "sealed_at": "2026-10-19T01:11:02Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:34634f7251ed8b2a1539748dd9aa8dbdb263d7c039e8635d05eea70c7857ceb2", + "spec_hash": "sha256:dad72ec0abe3b1020f0e9bff20027682d1d40d26f427965ad111fa2282a325a1", "spec_path": "specs/fpga/board_receipt.t27", "tests": { "failed": 0, @@ -22,7 +22,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/fpga_FpgaDdr3HeadBandwidth.json b/.trinity/seals/fpga_FpgaDdr3HeadBandwidth.json index 1593d7666a..ff88947acd 100644 --- a/.trinity/seals/fpga_FpgaDdr3HeadBandwidth.json +++ b/.trinity/seals/fpga_FpgaDdr3HeadBandwidth.json @@ -1,22 +1,22 @@ { - "built_by": "t27c-bootstrap@0.5.2+a86b691b1", + "built_by": "t27c-bootstrap@0.5.2+ea35d9b72", "closure": [ { "spec": "specs/fpga/board_receipt.t27", - "spec_hash": "sha256:34634f7251ed8b2a1539748dd9aa8dbdb263d7c039e8635d05eea70c7857ceb2" + "spec_hash": "sha256:dad72ec0abe3b1020f0e9bff20027682d1d40d26f427965ad111fa2282a325a1" } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:1b37e08fd08dbbc0645a49bc82a0dcc499e209d26f5e5734ae39d130f920fe58", - "gen_hash_rust": "sha256:9543f6cb7a6e90c6af7602df2c0c5373f88ca949b74e90742fce80a42c0baa7e", - "gen_hash_verilog": "sha256:c8408e1ad2d20562e6f624647dca216e9d06483006eefeba1ce57857dd3fad09", - "gen_hash_zig": "sha256:ed9f25e68b8a6a456ec6eda990b40bc89a2abf948e8b87e46910eacb7b6830a3", + "gen_hash_c": "sha256:3248e16baecb5ee11a6d7fa26ae227b25cb59aaa5dc2cb7134c6f088258feadc", + "gen_hash_rust": "sha256:c0611521a3e92417d9001deff13337dfc67e076b653401e427c763eb60f0c3e9", + "gen_hash_verilog": "sha256:6136d87130ca4fd11fc8ecffd7d742a6de6c80ddd29ea9bc1055011861fff74c", + "gen_hash_zig": "sha256:cfac0b07859bec1b77fe08fde2f147c3882de0f2ecdf7698049e19b99577eeb5", "module": "FpgaDdr3HeadBandwidth", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T13:56:41Z", + "sealed_at": "2026-10-19T01:11:07Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:152bf98420d4c3919835eefdb3cad56c76cd80cbecc11e1bcb6616fc25dfdd04", + "spec_hash": "sha256:aec485ee482ee1833a3518087f6381d9f75bbd49854d01ef1dd09053a56c4c9e", "spec_path": "specs/fpga/ddr3_head_bandwidth.t27", "tests": { "failed": 0, @@ -27,7 +27,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/fpga_FpgaDdr3TernaryMatvec.json b/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json index b706b418f9..b02d6223f2 100644 --- a/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json +++ b/.trinity/seals/fpga_FpgaDdr3TernaryMatvec.json @@ -1,22 +1,22 @@ { - "built_by": "t27c-bootstrap@0.5.2+a86b691b1", + "built_by": "t27c-bootstrap@0.5.2+ea35d9b72", "closure": [ { "spec": "specs/fpga/board_receipt.t27", - "spec_hash": "sha256:34634f7251ed8b2a1539748dd9aa8dbdb263d7c039e8635d05eea70c7857ceb2" + "spec_hash": "sha256:dad72ec0abe3b1020f0e9bff20027682d1d40d26f427965ad111fa2282a325a1" } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:af4d241ce9398f06df4527b2e7d8db1f81eeefa0c1298ec4be8840302236d92f", - "gen_hash_rust": "sha256:0f474fbf43039fa0da4932752897314fb70fddac664e0efbf3f98b535fae9895", - "gen_hash_verilog": "sha256:7dd8c000bec8d732ebf2538e289621bee1f3c1e751df53f583beaaddf349680a", - "gen_hash_zig": "sha256:d38c2a80429c2b66adc024d7723b227ccaf2f792259277196f3255ebd3cd0f44", + "gen_hash_c": "sha256:a342d03c59ede4a34c4bc0fa93285f1fd273eeb9a0cb3b13fd6ca1913848e2b3", + "gen_hash_rust": "sha256:c0d46dd557d195d583211fffe5c3c47e1ac32323d6e789688c80b416eaec8c6b", + "gen_hash_verilog": "sha256:0c149fb374f44339aa3d65c9c95f9bd1995c661186a28b34767fb6bf312c02d0", + "gen_hash_zig": "sha256:e54b2d4c607a3299647b51b831c36e0fd6935a80036a35c89206da1ef6261013", "module": "FpgaDdr3TernaryMatvec", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T15:37:16Z", + "sealed_at": "2026-10-19T01:11:09Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:84b7de73ff2f1a8679ca83443e0dcb62c5f30677cebc3015850331811420c16a", + "spec_hash": "sha256:09d56919a54d89a7636534eaea5290ed3fcfc31d0c5cef3ef069cad77ebc9d87", "spec_path": "specs/fpga/ddr3_ternary_matvec.t27", "tests": { "failed": 0, @@ -27,7 +27,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/fpga_FpgaRcFilter.json b/.trinity/seals/fpga_FpgaRcFilter.json index 3d5ea1c297..8c4792fc62 100644 --- a/.trinity/seals/fpga_FpgaRcFilter.json +++ b/.trinity/seals/fpga_FpgaRcFilter.json @@ -1,9 +1,9 @@ { - "built_by": "t27c-bootstrap@0.5.2+a86b691b1", + "built_by": "t27c-bootstrap@0.5.2+ea35d9b72", "closure": [ { "spec": "specs/fpga/board_receipt.t27", - "spec_hash": "sha256:34634f7251ed8b2a1539748dd9aa8dbdb263d7c039e8635d05eea70c7857ceb2" + "spec_hash": "sha256:dad72ec0abe3b1020f0e9bff20027682d1d40d26f427965ad111fa2282a325a1" } ], "config": "gen=c,rust,verilog,zig;tests=zig", @@ -14,7 +14,7 @@ "module": "FpgaRcFilter", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T13:56:42Z", + "sealed_at": "2026-10-19T01:11:27Z", "sealed_by": "t27c-bootstrap@0.5.2", "spec_hash": "sha256:be3af1aa6195d51e46289121cfd42623c80cd42d863442f4f6f69109da06d32f", "spec_path": "specs/fpga/rc_filter_ax7203.t27", @@ -27,7 +27,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/fpga_FpgaTern9mL0KWeights.json b/.trinity/seals/fpga_FpgaTern9mL0KWeights.json index 026e0a21b5..aa2161b676 100644 --- a/.trinity/seals/fpga_FpgaTern9mL0KWeights.json +++ b/.trinity/seals/fpga_FpgaTern9mL0KWeights.json @@ -1,26 +1,26 @@ { - "built_by": "t27c-bootstrap@0.5.2+a86b691b1", + "built_by": "t27c-bootstrap@0.5.2+ea35d9b72", "closure": [ { "spec": "specs/fpga/board_receipt.t27", - "spec_hash": "sha256:34634f7251ed8b2a1539748dd9aa8dbdb263d7c039e8635d05eea70c7857ceb2" + "spec_hash": "sha256:dad72ec0abe3b1020f0e9bff20027682d1d40d26f427965ad111fa2282a325a1" }, { "spec": "specs/fpga/ddr3_ternary_matvec.t27", - "spec_hash": "sha256:84b7de73ff2f1a8679ca83443e0dcb62c5f30677cebc3015850331811420c16a" + "spec_hash": "sha256:09d56919a54d89a7636534eaea5290ed3fcfc31d0c5cef3ef069cad77ebc9d87" } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:a1bc05c9dccc86398a7bc9f41cf8edc93c9545f35bf5be41dc38145327700c14", - "gen_hash_rust": "sha256:0f6232f05dbc51ad22947799c8ca0fab06c154afd4f572e80f46b55c4064f2b2", - "gen_hash_verilog": "sha256:43a2a07865e9a34ed7405f4a487e4c22c20d112abd9a74dbfe2da46cab3e8127", - "gen_hash_zig": "sha256:bd77315dd9e6410157ceaa8c59b5906e594814abcff5fce7b859a674597c871e", + "gen_hash_c": "sha256:e17b6372fb0007de7ffeb5f73119e6e0ccb7b52a7e073e82428e68daef147f34", + "gen_hash_rust": "sha256:f65498c3aa02c6195e4a50ddbac6ee0dde40d1f81e8a14591bece9c4a05f1757", + "gen_hash_verilog": "sha256:03d2802eb117e8ce690afd09f636f0ec02764f18e741b4fcdaf2d3fa464987e9", + "gen_hash_zig": "sha256:6a00b49c743f944a6ba2ca04fae04ab21acafcbfb589a0dda3d8d22c4264c3e4", "module": "FpgaTern9mL0KWeights", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T16:39:57Z", + "sealed_at": "2026-10-19T01:11:04Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:43ee35ce1e0d1810b33cabe7517d109e4e469199fce38f4f563c5b5cceb9f448", + "spec_hash": "sha256:ea62f86f729a344db8f8a312854ca555d5eb6fce7408b0f1ff3ea9da5488f5b2", "spec_path": "specs/fpga/tern9m_l0_k_weights.t27", "tests": { "failed": 0, @@ -31,7 +31,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/specs/fpga/board_receipt.t27 b/specs/fpga/board_receipt.t27 index 7162f9ce93..7789b8874d 100644 --- a/specs/fpga/board_receipt.t27 +++ b/specs/fpga/board_receipt.t27 @@ -8,6 +8,9 @@ ; 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). +; The beat checksum is `fold_beat`, not `fold`: specs/fpga/rc_filter_ax7203.t27 and specs/analog/linear.t27 both +; declare a two-argument `fold`, and a name two modules of one import closure declare differently is left +; unresolved (bootstrap/src/use_resolve.rs), so a board spec that imports the analog cell and M0 lost its `fold`. ; 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. @@ -17,7 +20,7 @@ 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 { +pub fn fold_beat(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)); } @@ -67,18 +70,18 @@ test pass_fail_char_spells_pass_and_fail { } 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); + assert_eq(fold_beat(0, 0, 0, 0, 0), 0); + assert_eq(fold_beat(1, 0, 0, 0, 0), 2); + assert_eq(fold_beat(0x8000000000000000, 0, 0, 0, 0), 1); + assert_eq(fold_beat(0, 1, 0, 0, 0), 1); + assert_eq(fold_beat(0, 0, 1, 0, 0), 0x10000); + assert_eq(fold_beat(0, 0, 0, 1, 0), 0x100000000); + assert_eq(fold_beat(0, 0, 0, 0, 1), 0x1000000000000); + assert_eq(fold_beat(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); + const a : u64 = fold_beat(0x0123456789ABCDEF, 0x1111, 0x2222, 0x3333, 0x4444); + const b : u64 = fold_beat(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 1df4f8e905..d3b05766ea 100644 --- a/specs/fpga/ddr3_head_bandwidth.t27 +++ b/specs/fpga/ddr3_head_bandwidth.t27 @@ -87,7 +87,7 @@ pub fn lane_word(i: u32, k: u32) -> u64 { return w ^ (w << 21) ^ (w << 42) ^ LANE_SALT; } -; fold, the beat checksum, is specs/fpga/board_receipt.t27's, as hex_digit is: one body for every +; fold_beat, 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. @@ -652,7 +652,7 @@ fn on_clock(core_init_done: bool, core_init_error: bool, core_user_port_native_0 wcyc = wcyc + 1; if (core_user_port_native_0_cmd_ready and ci < n_beats) { ci = ci + 1; } if (core_user_port_native_0_wdata_ready and di < n_beats) { - wsum = fold(wsum, lane_word(di, 0), lane_word(di, 1), lane_word(di, 2), lane_word(di, 3)); + wsum = fold_beat(wsum, lane_word(di, 0), lane_word(di, 1), lane_word(di, 2), lane_word(di, 3)); di = di + 1; } } @@ -667,7 +667,7 @@ fn on_clock(core_init_done: bool, core_init_error: bool, core_user_port_native_0 if (core_user_port_native_0_cmd_ready and ci < n_beats) { ci = ci + 1; } if (rv) { if (!beat_ok(ri, rb0, rb1, rb2, rb3)) { err = err + 1; } - rsum = fold(rsum, rb0, rb1, rb2, rb3); + rsum = fold_beat(rsum, rb0, rb1, rb2, rb3); dnum = dnum + BEAT_X_MHZ; ri = ri + 1; } @@ -801,20 +801,20 @@ test no_two_beats_or_lanes_share_a_word { } test the_checksum_knows_the_order_of_the_beats { - const a : u64 = fold(fold(0, 1, 2, 4, 8), 16, 32, 64, 128); - const b : u64 = fold(fold(0, 16, 32, 64, 128), 1, 2, 4, 8); + const a : u64 = fold_beat(fold_beat(0, 1, 2, 4, 8), 16, 32, 64, 128); + const b : u64 = fold_beat(fold_beat(0, 16, 32, 64, 128), 1, 2, 4, 8); assert a != b; - assert_eq(fold(0, 1, 2, 4, 8), 2251816993685505); - assert_eq(fold(9223372036854775808, 0, 0, 0, 0), 1); + assert_eq(fold_beat(0, 1, 2, 4, 8), 2251816993685505); + assert_eq(fold_beat(9223372036854775808, 0, 0, 0, 0), 1); assert_eq(lane_word(5, 0) ^ lane_word(5, 1) ^ lane_word(5, 2) ^ lane_word(5, 3), 0); - assert_eq(fold(0, lane_word(0, 0), lane_word(0, 1), lane_word(0, 2), lane_word(0, 3)), 16182248147329805489); + assert_eq(fold_beat(0, lane_word(0, 0), lane_word(0, 1), lane_word(0, 2), lane_word(0, 3)), 16182248147329805489); } test the_head_folds_to_a_sum_the_board_must_report { var sum : u64 = 0; var i : u32 = 0; while (i < HEAD_BEATS) { - sum = fold(sum, lane_word(i, 0), lane_word(i, 1), lane_word(i, 2), lane_word(i, 3)); + sum = fold_beat(sum, lane_word(i, 0), lane_word(i, 1), lane_word(i, 2), lane_word(i, 3)); i = i + 1; } assert_eq(sum, 0xFFB7236C398EE555); @@ -883,7 +883,7 @@ test a_beat_read_back_wrong_is_a_fail_at_any_rate { err = 0; dnum = 0; rv = false; - wsum = fold(fold(0, lane_word(0, 0), lane_word(0, 1), lane_word(0, 2), lane_word(0, 3)), lane_word(1, 0), lane_word(1, 1), lane_word(1, 2), lane_word(1, 3)); + wsum = fold_beat(fold_beat(0, lane_word(0, 0), lane_word(0, 1), lane_word(0, 2), lane_word(0, 3)), lane_word(1, 0), lane_word(1, 1), lane_word(1, 2), lane_word(1, 3)); on_clock(true, false, false, false, true, lane_word(0, 0), lane_word(0, 1), lane_word(0, 2), lane_word(0, 3), true); on_clock(true, false, false, false, true, lane_word(1, 0), lane_word(1, 1), lane_word(1, 2) ^ 4, lane_word(1, 3), true); on_clock(true, false, false, false, false, 0, 0, 0, 0, true); diff --git a/specs/fpga/ddr3_ternary_matvec.t27 b/specs/fpga/ddr3_ternary_matvec.t27 index fd8d14f579..fdf09869d9 100644 --- a/specs/fpga/ddr3_ternary_matvec.t27 +++ b/specs/fpga/ddr3_ternary_matvec.t27 @@ -83,7 +83,7 @@ pub const BAUD_DIV : u16 = 868; pub const LINE_SEGS : u8 = 9; ; --- the arithmetic ----------------------------------------------------------------------------- -; fold (the beat checksum, the one specs/fpga/ddr3_head_bandwidth.t27 prints), hex_digit and pass_fail_char +; fold_beat (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. @@ -688,7 +688,7 @@ fn on_clock(core_init_done: bool, core_init_error: bool, core_user_port_native_0 } 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)); + wsum = fold_beat(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 { @@ -707,7 +707,7 @@ fn on_clock(core_init_done: bool, core_init_error: bool, core_user_port_native_0 } } 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); + csum = fold_beat(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; @@ -731,7 +731,7 @@ fn on_clock(core_init_done: bool, core_init_error: bool, core_user_port_native_0 } } else { if (col == W_COLS) { - ysum = fold(ysum, acc as u64, 0, 0, 0); + ysum = fold_beat(ysum, acc as u64, 0, 0, 0); acc = 0; col = 0; xv = XV0; @@ -912,7 +912,7 @@ 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)); + sref = fold_beat(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; @@ -926,7 +926,7 @@ test two_rows_go_in_come_back_and_are_multiplied { x = x +% XSTEP; c = c + 1; } - yref = fold(yref, a as u64, 0, 0, 0); + yref = fold_beat(yref, a as u64, 0, 0, 0); r = r + 1; } st = ST_LOAD; @@ -993,7 +993,7 @@ 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)); + sref = fold_beat(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; @@ -1007,7 +1007,7 @@ test a_byte_that_is_no_trit_is_counted_and_fails { st = ST_LOAD; n_beats = 10; s_want = sref; - y_want = fold(0, a as u64, 0, 0, 0); + y_want = fold_beat(0, a as u64, 0, 0, 0); ca = 0; cv = false; wv = false; diff --git a/specs/fpga/tern9m_l0_k_weights.t27 b/specs/fpga/tern9m_l0_k_weights.t27 index 308ac8080e..5ab2b75989 100644 --- a/specs/fpga/tern9m_l0_k_weights.t27 +++ b/specs/fpga/tern9m_l0_k_weights.t27 @@ -694,7 +694,7 @@ 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)); + s = fold_beat(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; @@ -721,7 +721,7 @@ pub fn y_of(ff_plus: bool, flip: u32, to: u8) -> u64 { xv = xv +% XSTEP; col = col + 1; if (col == W_COLS) { - y = fold(y, acc as u64, 0, 0, 0); + y = fold_beat(y, acc as u64, 0, 0, 0); acc = 0; col = 0; xv = XV0;