From 1b6b4aff0c797fc8411c1a42a8ddc8b5796f8d53 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 13:51:13 +0700 Subject: [PATCH 1/3] fpga(ax7203): the SAR converter of the golden deck on the board -- 31 conversions, one UART receipt each, a one-literal negative control (Closes #10910) specs/fpga/sar_adc_ax7203.t27 (module FpgaSarAdc) is the board top of the M4e converter (specs/analog/sar_adc.t27): a machine that walks the spec's MSB-first sequence on the fabric (neg, diff, decide, ratio, K x VCM as two shifted adds, round, plate step), with the 31 held samples, the DAC's ten Vout ratios and the two pinned codes of each conversion as if-chain ROMs. It prints one line per conversion, "T27 SAR K=.. C=.. E=.. N=.. S=.. L=.. PASS|FAIL", PASS when the board's code equals the spec's fitted code (30 of the 31 are also ngspice's). Twelve tests, 0 vacuous: the ROMs equal the spec's tables word for word; a plate step is the spec's DAC event for every plate; the three-clock decision is decide(); the machine gives the spec's code for all 31 conversions and the same Vout voltage after every one of the eleven decisions; a conversion is 75 clocks; one more DAC unit on the LSB plate (one rom_k literal) fails exactly 16 of the 31 conversions, the spec's own bridge and Bit_8 controls fail all 31; the restart, the pins and 63 UART lines (two rounds and the wrap) decode. Nothing in specs/analog/ or its seals is touched. Bitstreams are built locally and not committed. Co-Authored-By: Claude Sonnet 5.5 --- .trinity/seals/fpga_FpgaSarAdc.json | 45 ++ specs/fpga/sar_adc_ax7203.t27 | 1042 +++++++++++++++++++++++++++ 2 files changed, 1087 insertions(+) create mode 100644 .trinity/seals/fpga_FpgaSarAdc.json create mode 100644 specs/fpga/sar_adc_ax7203.t27 diff --git a/.trinity/seals/fpga_FpgaSarAdc.json b/.trinity/seals/fpga_FpgaSarAdc.json new file mode 100644 index 0000000000..810d222e68 --- /dev/null +++ b/.trinity/seals/fpga_FpgaSarAdc.json @@ -0,0 +1,45 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+ea35d9b72", + "closure": [ + { + "spec": "specs/analog/linear.t27", + "spec_hash": "sha256:3ddef7be183aba583ed285334ee389b48a65b41335e98914514235db7c4e5d62" + }, + { + "spec": "specs/analog/sar_adc.t27", + "spec_hash": "sha256:48e8825a4a6a7fc24ce23472bcba5499dcafbd399ac45a14fb153a0a020018e2" + }, + { + "spec": "specs/analog/sar_cdac.t27", + "spec_hash": "sha256:a7c45039214a8b2e92333a88befc95af33ff482ce08af3be97e2c5b8be3eacd3" + }, + { + "spec": "specs/fpga/rc_filter_ax7203.t27", + "spec_hash": "sha256:be3af1aa6195d51e46289121cfd42623c80cd42d863442f4f6f69109da06d32f" + } + ], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:fdeddedfbdeccfd4b6c78d87c485fb9b382969cbbfb39dabbe99c5ff82af33c4", + "gen_hash_rust": "sha256:32364716a0eb63162fff91c14b35b6aeb87d2299dac87a5fcab5f5c19d2377fc", + "gen_hash_verilog": "sha256:a9a73405ddd4d1e16cd1d1692d78eae729c144a39644cf61cf23522a22041ce5", + "gen_hash_zig": "sha256:8a8cf9f903401630176bfdb0b20d9e81f81b3f63366046ea3b21ebeaaf990356", + "module": "FpgaSarAdc", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-19T06:43:07Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:baebf530feb0c8aa4fc034ce7aa3677edfd7f4c9ad343dccc63f9ec152571406", + "spec_path": "specs/fpga/sar_adc_ax7203.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 12, + "total": 12, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:8512b80da533b79289110fca4a65f3336abd7a059ca4b72ea595d5e33ff8ad10", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/specs/fpga/sar_adc_ax7203.t27 b/specs/fpga/sar_adc_ax7203.t27 new file mode 100644 index 0000000000..aae794414a --- /dev/null +++ b/specs/fpga/sar_adc_ax7203.t27 @@ -0,0 +1,1042 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/fpga/sar_adc_ax7203.t27 -- the SAR converter of the golden deck on the ALINX AX7203: 31 conversions, one UART receipt line each +; M4e-board of the SAR ADC milestone (#10524, epic #10486, issue #10910). The converter is specs/analog/sar_adc.t27 (M4e, #10818): the M4a split +; capacitive DAC with its 1-unit bridge and one fitted top-plate parasitic (specs/analog/sar_cdac.t27), a sign comparator with one fitted offset, +; the MSB-first sequence of the deck, run on the 31 held samples of our own ngspice + PSP103 run. This file is the board top of it: the words +; of the DAC, the samples and the two pinned codes of each conversion are ROMs, and the machine below walks the spec's sequence on the fabric. +; The converter's functions (neg_word, decide, convert_sar, model_k, round_back, add_sm, pack, fold), M0's PLL, UART frame and verdict +; constants and the receipt's digits (specs/fpga/board_receipt.t27) come in by `use`; what is written here is the machine, the ROMs and the +; line of the receipt. Everything hand-written is this file. Nothing of M1b (specs/fpga/analog_cell_ax7203.t27) is edited; its pattern is +; followed: the restart request flags, the ROM as an if-chain, the receipt as segments, the tests that run the machine beside the spec. +; - +; THE CONVERSION (sar_adc.t27, sar_core). A conversion holds the two top plates at the sample, xp = V(VDP) and xn = V(VDN), as words (bit 31 = +; negative, bits 0..30 the magnitude in units of 2^-24 V). Decision i = 0 .. 10, MSB first: b = (xp - xn + OFF > 0); then, for i < 10, the plate of +; Bit_(10 - i) moves, down for the P half and up for the N half when b is set, the other way when it is clear, by rnd(K x VCM), K the plate's Vout +; ratio. The code is the eleven decisions. The spec runs net1 too; it never reaches the comparator and nothing reads it, so the board does not +; (a test runs both nodes of the spec beside the machine and compares Vout after every decision). +; - +; THE MACHINE, one step a clock at 100 MHz (the PLL of M0 from the 200 MHz oscillator), the same for every conversion: +; P_SMP xp and xn from the sample ROM, the two pinned codes from theirs +; P_NEG xnn = neg_word(xn) P_DIFF td = add_sm(xp, xnn) P_DEC dd = add_sm(td, OFF) +; P_BIT b = dd > 0 (sar_adc's decide, split over three clocks), the code takes the bit; the last decision stops here, the others load +; the plate's ratio K from the DAC ROM +; P_MUL K x VCM as two shifted adds (VCM = 2^23 + 2^22 = 0.75 V: the plate's step is a constant times a ROM constant, so no live operand is +; multiplied: no DSP slice, no serial multiplier) +; P_RND round_back of the product P_APP xp and xn take the step, with opposite signs, and the next decision starts +; No clock chains more than one add_sm: the spec's decide() is neg_word and two add_sm in one expression, and it is split here over three clocks +; (a test compares the split with decide). A conversion is 75 clocks from P_SMP to the verdict (a test pins it); no loop depends on data. After +; the verdict the receipt line is sent, then the next conversion runs. +; - +; THE RESTART. As M1b: 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 at conversion 0 and line 0. A finished line sets `fin` alone and the next clock starts the next +; conversion. After conversion 30 the board goes back to conversion 0, so the 31 lines repeat for as long as the capture runs (L counts on). +; - +; THE ROMS (if-chains: `t27b verilog` refuses array indexing; a test compares every word with the spec's own table). +; rom_vp, rom_vn q_sm(S_VP[k]), q_sm(S_VN[k]): the held top plates of conversion k, V(VDP) and V(VDN) of the ngspice run at 500 k + 98 ns +; rom_exp FIT_CODE[k]: what the spec's fitted converter gives (the board must print it as C) +; rom_ng NG_CODE[k]: the code of the ngspice run (printed as N, not judged) +; rom_k model_k(UNITS, 1.0, CP_FIT)[2 j + 1], the Vout ratio of plate j (j = 0 is Bit_1): the fitted DAC, 10 words +; OFF_WORD q_sm(OFF_FIT_V): the comparator offset, +6.7 mV +; - +; THE RECEIPT. 115200 baud on N15 (divider 868 from 100 MHz), one line per conversion, M0's grammar: +; T27 SAR K=<2 hex> C=<3 hex> E=<3 hex> N=<3 hex> S=<16 hex> L=<4 hex> PASS +; K the conversion (0 .. 1E), C the board's 11-bit code, E the spec's code for it, N the ngspice code, S the order-sensitive fold of the board's +; codes of this round (K = 0 .. this one), L the lines since the button. PASS when C equals E, else FAIL. N is not judged: 30 of the 31 E equal N +; (conversion 25, K=19 in hex: 1841 against 1842, is the one the spec reports as a miss at 0.133 mV from a threshold). LEDs (active low) as M0: B13 +; the line is being sent, C13 FAIL, D14 PASS, D15 a heartbeat. The button T6 resets. +; - +; THE NEGATIVE CONTROL. One literal of rom_k changed: plate j = 0 (Bit_1) with the ratio of 2 units instead of 1, word 16083 to 32166, which is +; one more DAC unit on the LSB plate. The spec's own converter on that table gives the codes FAULT_CODE; 16 of the 31 conversions differ from +; E (FAULT_MASK), and a build with that one literal changed prints FAIL on exactly those lines and PASS on the other 15. +; - +; WHAT A PASS SAYS. This board, running RTL generated from this file, ran the converter of sar_adc.t27 on the 31 held samples and produced, for +; every conversion, the code that spec's fitted model produces (the tests compare the machine with convert_sar on all 31, and the voltage of +; the top plates after every one of the eleven decisions with the spec's own DAC events). By that spec 30 of those 31 codes are the ones the +; ngspice + PSP103 run of the golden deck gave. +; WHAT IT DOES NOT SAY. Nothing about the circuit beyond the spec: the comparator and the top-plate load are two fitted numbers (OFF_FIT_V, CP_FIT), +; fitted on these 31 conversions, so 30 of 31 describes this run and predicts nothing; the switch is the run's, not modelled; the SAR logic is +; a sequence, not gates. Nothing about speed: a conversion takes 75 clocks (0.75 us) and 63 characters of line (5.5 ms), which is not a +; comparison with the 65 minutes of ngspice. Nothing about power, noise, mismatch, another corner or another sample set. The board holds +; ROMs of the samples: it does not sample anything. ASCII only, English only. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module FpgaSarAdc; + +use analog::linear; +use analog::sar_cdac; +use analog::sar_adc; +use fpga::rc_filter_ax7203; + +pub const KIND : str = "board-cell"; +pub const ID : str = "fpga/sar_adc_ax7203"; +pub const REFERENCE : str = "specs/analog/sar_adc.t27 (M4e), specs/analog/sar_cdac.t27 (M4a), M1b specs/fpga/analog_cell_ax7203.t27"; +pub const BOARD : str = "ALINX AX7203"; +pub const PART : str = "xc7a200tfbg484-2"; + +; --- the converter's numbers, as the board holds them ---------------------------------------------- +/// The conversions the board cycles through (sar_adc's N_CONV, as a u8). +pub const CONVS : u8 = 31; +/// The decisions of a conversion (sar_adc's DECISIONS, as a u8), and the index of the last. +pub const DECS : u8 = 11; +pub const DEC_LAST : u8 = 10; +/// The index of the last plate (sar_cdac's PLATES - 1): the first decision moves it. +pub const PLATE_LAST : u8 = 9; +/// q_sm(OFF_FIT_V): +6.7 mV in units of 2^-24 V. +pub const OFF_WORD : u32 = 112407; +/// The clocks from P_SMP to the verdict, as a test measures them: 1 + 10 * 7 + 4. +pub const CONV_CLOCKS : u32 = 75; +/// The order-sensitive fold of the 31 codes of a round (FIT_CODE), the S of the line K = 1E. +pub const ROUND_FOLD : u64 = 0xADF99975C7; + +; --- the negative control: one more DAC unit on the LSB plate -------------------------------------- +/// The plate and the word of rom_k that the control changes (the right word is 16083), and the 2 units' ratio it is. +pub const FAULT_J : u8 = 0; +pub const FAULT_WORD : u32 = 32166; +/// Bit k set: conversion k prints FAIL with the changed word. +pub const FAULT_MASK : u32 = 687562312; +pub const FAULT_FAILS : u32 = 16; +/// The codes of the spec's converter on the changed table, conversion by conversion. +pub const FAULT_CODE : [31]u32 = [ + 1006, 841, 686, 545, + 421, 321, 249, 205, + 194, 214, 266, 349, + 457, 585, 733, 889, + 1053, 1214, 1370, 1513, + 1634, 1734, 1809, 1850, + 1862, 1841, 1789, 1709, + 1601, 1470, 1325 +]; + +; --- the machine -------------------------------------------------------------------------------- +pub const P_SMP : u8 = 0; +pub const P_NEG : u8 = 1; +pub const P_DIFF : u8 = 2; +pub const P_DEC : u8 = 3; +pub const P_BIT : u8 = 4; +pub const P_MUL : u8 = 5; +pub const P_RND : u8 = 6; +pub const P_APP : u8 = 7; + +; --- facts -------------------------------------------------------------------------------------- + +/// The conversion after k: the last goes back to the first. +pub fn next_cv(k: u8) -> u8 { + if (k == CONVS - 1) { return 0; } + return k + 1; +} + +/// Is the word d above zero? A word is never "negative zero" (pack), so this is: some magnitude and no sign bit. +pub fn is_above(d: u32) -> bool { + return (d & MAG) != 0 and !is_neg(d); +} + +/// PASS when the board's code equals the spec's. +pub fn sar_verdict(c: u32, e: u32) -> u8 { + if (c == e) { return V_PASS; } + return V_FAIL; +} + +; --- the ROMs: the spec tables as if-chains ----------------------------------------------------------- + +/// V(VDP) of conversion k, the held top plate of the P half: q_sm(S_VP[k]), a word (volts * 2^24). +pub fn rom_vp(k: u8) -> u32 { + if (k == 0) { return 12196511; } + if (k == 1) { return 10314520; } + if (k == 2) { return 8443463; } + if (k == 3) { return 6730616; } + if (k == 4) { return 5242576; } + if (k == 5) { return 4037944; } + if (k == 6) { return 3160452; } + if (k == 7) { return 2645106; } + if (k == 8) { return 2511430; } + if (k == 9) { return 2764607; } + if (k == 10) { return 3394871; } + if (k == 11) { return 4377699; } + if (k == 12) { return 5675815; } + if (k == 13) { return 7238929; } + if (k == 14) { return 9005712; } + if (k == 15) { return 10911068; } + if (k == 16) { return 12880327; } + if (k == 17) { return 14823351; } + if (k == 18) { return 16694161; } + if (k == 19) { return 18406454; } + if (k == 20) { return 19894283; } + if (k == 21) { return 21099508; } + if (k == 22) { return 21977905; } + if (k == 23) { return 22494334; } + if (k == 24) { return 22629076; } + if (k == 25) { return 22376936; } + if (k == 26) { return 21747343; } + if (k == 27) { return 20764796; } + if (k == 28) { return 19466446; } + if (k == 29) { return 17902675; } + return 16134515; +} + +/// V(VDN) of conversion k, the held top plate of the N half: q_sm(S_VN[k]). +pub fn rom_vn(k: u8) -> u32 { + if (k == 0) { return 12737566; } + if (k == 1) { return 14824034; } + if (k == 2) { return 16693584; } + if (k == 3) { return 18403882; } + if (k == 4) { return 19890435; } + if (k == 5) { return 21098874; } + if (k == 6) { return 21977956; } + if (k == 7) { return 22496393; } + if (k == 8) { return 22633787; } + if (k == 9) { return 22385033; } + if (k == 10) { return 21759692; } + if (k == 11) { return 20781182; } + if (k == 12) { return 19488095; } + if (k == 13) { return 17929315; } + if (k == 14) { return 16162429; } + if (k == 15) { return 14260264; } + if (k == 16) { return 12293195; } + if (k == 17) { return 10313714; } + if (k == 18) { return 8444397; } + if (k == 19) { return 6733514; } + if (k == 20) { return 5246539; } + if (k == 21) { return 4039228; } + if (k == 22) { return 3161086; } + if (k == 23) { return 2643860; } + if (k == 24) { return 2507640; } + if (k == 25) { return 2757646; } + if (k == 26) { return 3383909; } + if (k == 27) { return 4362798; } + if (k == 28) { return 5655787; } + if (k == 29) { return 7213825; } + return 8978491; +} + +/// The code the spec's fitted converter gives conversion k (FIT_CODE[k]): what the board must print as C. +pub fn rom_exp(k: u8) -> u32 { + if (k == 0) { return 1006; } + if (k == 1) { return 841; } + if (k == 2) { return 686; } + if (k == 3) { return 544; } + if (k == 4) { return 421; } + if (k == 5) { return 321; } + if (k == 6) { return 248; } + if (k == 7) { return 205; } + if (k == 8) { return 194; } + if (k == 9) { return 215; } + if (k == 10) { return 267; } + if (k == 11) { return 348; } + if (k == 12) { return 456; } + if (k == 13) { return 585; } + if (k == 14) { return 732; } + if (k == 15) { return 889; } + if (k == 16) { return 1052; } + if (k == 17) { return 1215; } + if (k == 18) { return 1370; } + if (k == 19) { return 1512; } + if (k == 20) { return 1635; } + if (k == 21) { return 1735; } + if (k == 22) { return 1808; } + if (k == 23) { return 1851; } + if (k == 24) { return 1862; } + if (k == 25) { return 1841; } + if (k == 26) { return 1789; } + if (k == 27) { return 1708; } + if (k == 28) { return 1601; } + if (k == 29) { return 1471; } + return 1325; +} + +/// The code our own ngspice + PSP103 run of the golden deck gave conversion k (NG_CODE[k]); printed as N, not judged. +pub fn rom_ng(k: u8) -> u32 { + if (k == 0) { return 1006; } + if (k == 1) { return 841; } + if (k == 2) { return 686; } + if (k == 3) { return 544; } + if (k == 4) { return 421; } + if (k == 5) { return 321; } + if (k == 6) { return 248; } + if (k == 7) { return 205; } + if (k == 8) { return 194; } + if (k == 9) { return 215; } + if (k == 10) { return 267; } + if (k == 11) { return 348; } + if (k == 12) { return 456; } + if (k == 13) { return 585; } + if (k == 14) { return 732; } + if (k == 15) { return 889; } + if (k == 16) { return 1052; } + if (k == 17) { return 1215; } + if (k == 18) { return 1370; } + if (k == 19) { return 1512; } + if (k == 20) { return 1635; } + if (k == 21) { return 1735; } + if (k == 22) { return 1808; } + if (k == 23) { return 1851; } + if (k == 24) { return 1862; } + if (k == 25) { return 1842; } + if (k == 26) { return 1789; } + if (k == 27) { return 1708; } + if (k == 28) { return 1601; } + if (k == 29) { return 1471; } + return 1325; +} + +/// The Vout charge-transfer ratio of plate j (j = 0 is Bit_1) of the fitted DAC (bridge 1 unit, Cp 0.63 units): model_k(UNITS, 1.0, CP_FIT)[2 j + 1]. +pub fn rom_k(j: u8) -> u32 { + if (j == 0) { return 16083; } + if (j == 1) { return 32166; } + if (j == 2) { return 64332; } + if (j == 3) { return 128665; } + if (j == 4) { return 257329; } + if (j == 5) { return 514658; } + if (j == 6) { return 1029317; } + if (j == 7) { return 2058633; } + if (j == 8) { return 4117266; } + return 8234532; +} + +; --- the receipt: M0's line, with the fields of a conversion --------------------------------------------- +; hex_digit and pass_fail_char (board_receipt), frame, prefix_char (M0) are shared; the segments are these: +; 0 "T27 SAR" 1 " K=" + 2 hex 2 " C=" + 3 hex 3 " E=" + 3 hex 4 " N=" + 3 hex 5 " S=" + 16 hex 6 " L=" + 4 hex 7 " PASS\r\n" + +pub const SAR_SEGS : u8 = 8; + +/// The key letter of field s (1..6): K C E N S L. +pub fn sar_key(s: u8) -> u8 { + if (s == 1) { return 75; } + if (s == 2) { return 67; } + if (s == 3) { return 69; } + if (s == 4) { return 78; } + if (s == 5) { return 83; } + return 76; +} + +/// The hex digits of field s (1..6). +pub fn sar_width(s: u8) -> u8 { + if (s == 1) { return 2; } + if (s == 5) { return 16; } + if (s == 6) { return 4; } + return 3; +} + +/// The last position of segment s: the prefix and the verdict have 7 characters, a field has " X=" and its digits. +pub fn sar_seg_last(s: u8) -> u8 { + if (s == 0) { return 6; } + if (s == SAR_SEGS - 1) { return 6; } + return 2 + sar_width(s); +} + +/// Character p of "T27 SAR": M0's "T27 " and the name. +pub fn sar_prefix(p: u8) -> u8 { + if (p < 4) { return prefix_char(p); } + if (p == 4) { return 83; } + if (p == 5) { return 65; } + return 82; +} + +/// The character at segment s, position p; `fsr` holds the field being written, its next nibble on top. +pub fn sar_char(s: u8, p: u8, fsr: u64, v: u8) -> u8 { + if (s == 0) { return sar_prefix(p); } + if (s == SAR_SEGS - 1) { return pass_fail_char(v, p); } + if (p == 0) { return 32; } + if (p == 1) { return sar_key(s); } + if (p == 2) { return 61; } + return hex_digit((fsr >> 60) as u8); +} + +/// Field s (1..6) placed at the top of the 64-bit register, so that its first digit is nibble 15: 4 * (16 - width) bits up. +pub fn sar_top(s: u8, k: u8, c: u32, e: u32, n: u32, sum: u64, l: u32) -> u64 { + if (s == 1) { return (k as u64) << 56; } + if (s == 2) { return (c as u64) << 52; } + if (s == 3) { return (e as u64) << 52; } + if (s == 4) { return (n as u64) << 52; } + if (s == 5) { return sum; } + return (l as u64) << 48; +} + +; --- 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 (M0, M1b): the button and LOCKED pass two registers, they set the restart request, and on the next +// edge on_clock puts the machine back at its start. +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 cv : u8 = 0; +var dc : u8 = 0; +var xp : u32 = 0; +var xn : u32 = 0; +var xnn : u32 = 0; +var td : u32 = 0; +var dd : u32 = 0; +var bt : bool = false; +var code : u32 = 0; +var ex : u32 = 0; +var ng : u32 = 0; +var mc : u64 = 0; +var pacc : u64 = 0; +var rnd : u32 = 0; +var cs : u64 = 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) { + cv = 0; + lines = 0; + cs = 0; + hard = false; + } else { + if (cv == CONVS - 1) { cs = 0; } + cv = next_cv(cv); + } + st = ST_RUN; + ph = P_SMP; + dc = 0; + code = 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) { + if (ph == P_SMP) { + xp = rom_vp(cv); + xn = rom_vn(cv); + ex = rom_exp(cv); + ng = rom_ng(cv); + ph = P_NEG; + } else if (ph == P_NEG) { + xnn = neg_word(xn); + ph = P_DIFF; + } else if (ph == P_DIFF) { + td = add_sm(xp, xnn); + ph = P_DEC; + } else if (ph == P_DEC) { + dd = add_sm(td, OFF_WORD); + ph = P_BIT; + } else if (ph == P_BIT) { + bt = is_above(dd); + if (is_above(dd)) { + code = (code << 1) | 1; + } else { + code = code << 1; + } + if (dc == DEC_LAST) { + st = ST_JUDGE; + } else { + mc = rom_k(PLATE_LAST - dc) as u64; + ph = P_MUL; + } + } else if (ph == P_MUL) { + pacc = (mc << 23) + (mc << 22); + ph = P_RND; + } else if (ph == P_RND) { + rnd = round_back(pacc); + ph = P_APP; + } else { + xp = add_sm(xp, pack(rnd, bt)); + xn = add_sm(xn, pack(rnd, !bt)); + dc = dc + 1; + ph = P_NEG; + } + } else if (st == ST_JUDGE) { + verdict = sar_verdict(code, ex); + cs = fold(cs, code); + 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(sar_char(seg, upos, fsr, verdict)); + tx_left = 9; + if (upos == sar_seg_last(seg)) { + fsr = sar_top(seg + 1, cv, code, ex, ng, cs, lines); + upos = 0; + if (seg == SAR_SEGS - 1) { + seg = 0; + lines = lines + 1; + last = true; + } else { + seg = seg + 1; + } + } else { + if (seg != 0 and seg != SAR_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 conversion `first` selected (the start of a conversion). +fn boot(first: u8) { + go0 = true; + go1 = false; + on_clock(true, true); + on_clock(true, true); + cv = first; +} + +/// Runs conversion i from reset to its verdict state; the clocks it took, P_SMP to ST_JUDGE. +fn run_conv(i: u8) -> u32 { + boot(i); + var n : u32 = 0; + while (st == ST_RUN and n < 1000) { + on_clock(true, true); + n = n + 1; + } + return n; +} + +/// Runs the machine on conversion i from reset, beside the spec's own sequence on the ratio words kk with both nodes of both halves +/// (M4a's events, the comparator word `off`), and counts the disagreements: Vout of each half before every decision, the code so far +/// before every decision, and the final code. The machine is left in ST_JUDGE. +fn board_vs_spec(i: u8, kk: []const u32, off: u32) -> u32 { + boot(i); + const s0 : u32 = q_sm(S_VP[i as usize]); + const s1 : u32 = q_sm(S_VN[i as usize]); + var rp : [2]u32 = [s0, s0]; + var rn : [2]u32 = [s1, s1]; + var qp : [2]u32 = [0, 0]; + var qn : [2]u32 = [0, 0]; + var bad : u32 = 0; + var want : u32 = 0; + var d : usize = 0; + while (d < DECISIONS) { + while (st == ST_RUN and !(ph == P_NEG and (dc as usize) == d)) { on_clock(true, true); } + if (xp != rp[1]) { bad = bad + 1; } + if (xn != rn[1]) { bad = bad + 1; } + if (code != want) { bad = bad + 1; } + const b : bool = decide(rp[1], rn[1], off); + want = want * 2; + if (b) { want = want + 1; } + if (d < PLATES) { + const j : usize = PLATES - 1 - d; + event_k(kk, j, plate_step(!b), &rp, &qp); + event_k(kk, j, plate_step(b), &rn, &qn); + rp[0] = qp[0]; + rp[1] = qp[1]; + rn[0] = qn[0]; + rn[1] = qn[1]; + } + d = d + 1; + } + while (st == ST_RUN) { on_clock(true, true); } + if (code != want) { bad = bad + 1; } + return bad; +} + +/// The value of the n hex digits of buf from position at. +fn hex_at(buf: []const u8, at: usize, n: usize) -> u64 { + var v : u64 = 0; + var k : usize = 0; + while (k < n) { + const c : u8 = buf[at + k]; + if (c >= 65) { + v = (v << 4) | ((c - 55) as u64); + } else { + v = (v << 4) | ((c - 48) as u64); + } + k = k + 1; + } + return v; +} + +/// The characters a line has: M0's prefix and verdict (7 each), a segment per field. +pub const LINE_LEN : usize = 63; + +; --- the tests ---------------------------------------------------------------------------------- + +test the_roms_are_the_specs_tables_word_for_word { + var i : usize = 0; + var same : u32 = 0; + while (i < N_CONV) { + assert_eq(rom_vp(i as u8), q_sm(S_VP[i])); + assert_eq(rom_vn(i as u8), q_sm(S_VN[i])); + assert_eq(rom_exp(i as u8), FIT_CODE[i]); + assert_eq(rom_ng(i as u8), NG_CODE[i]); + if (FIT_CODE[i] == NG_CODE[i]) { same = same + 1; } + i = i + 1; + } + // the spec's fitted codes are 30 of the 31 ngspice ones; the one miss is conversion 25 + assert_eq(same, 30); + assert(FIT_CODE[25] != NG_CODE[25]); + const kf : [20]u32 = model_k(&UNITS, 1.0, CP_FIT); + var j : usize = 0; + while (j < PLATES) { + assert_eq(rom_k(j as u8), kf[2 * j + 1]); + j = j + 1; + } + assert_eq(OFF_WORD, q_sm(OFF_FIT_V)); + assert_eq(CONVS as usize, N_CONV); + assert_eq(DECS as usize, DECISIONS); + assert_eq((DEC_LAST as usize) + 1, DECISIONS); + assert_eq((PLATE_LAST as usize) + 1, PLATES); + assert_eq(next_cv(CONVS - 1), 0); + assert_eq(next_cv(0), 1); + assert_eq(next_cv(29), 30); + // VCM is two shifted adds: 0.75 V = 2^23 + 2^22 in units of 2^-24 V + const one : u64 = 1; + assert_eq((one << 23) + (one << 22), VCM as u64); + // a word of any table changed by one LSB is seen by the comparison above + assert(rom_k(3) + 1 != kf[7]); + assert(rom_vp(8) + 1 != q_sm(S_VP[8])); +} + +test a_plate_step_is_the_specs_dac_event_for_every_plate { + const kf : [20]u32 = model_k(&UNITS, 1.0, CP_FIT); + var j : usize = 0; + while (j < PLATES) { + const m : u64 = rom_k(j as u8) as u64; + const a : u64 = (m << 23) + (m << 22); + assert_eq(a, prod(rom_k(j as u8), VCM)); + var x : [2]u32 = [0, 0]; + var y : [2]u32 = [0, 0]; + event_k(&kf, j, plate_step(true), &x, &y); + assert_eq(y[1], pack(round_back(a), false)); + event_k(&kf, j, plate_step(false), &x, &y); + assert_eq(y[1], pack(round_back(a), true)); + j = j + 1; + } +} + +test the_three_clock_decision_is_the_specs_decide { + var vs : [10]u32 = [0, 1, 5, NEG | 1, NEG | 5, OFF_WORD, NEG | OFF_WORD, OFF_WORD - 1, OFF_WORD + 1, 12582912]; + var i : usize = 0; + var j : usize = 0; + var above : u32 = 0; + while (i < 10) { + j = 0; + while (j < 10) { + const p : u32 = vs[i]; + const n : u32 = vs[j]; + assert_eq(is_above(add_sm(add_sm(p, neg_word(n)), OFF_WORD)), decide(p, n, OFF_WORD)); + if (decide(p, n, OFF_WORD)) { above = above + 1; } + j = j + 1; + } + i = i + 1; + } + // some pairs decide above and some do not, so the comparison above is not about one answer + assert(above > 20); + assert(above < 80); + var k : usize = 0; + while (k < N_CONV) { + const p : u32 = rom_vp(k as u8); + const n : u32 = rom_vn(k as u8); + assert_eq(is_above(add_sm(add_sm(p, neg_word(n)), OFF_WORD)), decide(p, n, OFF_WORD)); + assert_eq(is_above(add_sm(add_sm(n, neg_word(p)), OFF_WORD)), decide(n, p, OFF_WORD)); + k = k + 1; + } + assert(!is_above(0)); + assert(!is_above(NEG | 5)); + assert(is_above(1)); + assert(is_above(MAG)); + assert_eq(sar_verdict(5, 5), V_PASS); + assert_eq(sar_verdict(5, 6), V_FAIL); +} + +test the_machine_gives_the_specs_code_for_all_31_conversions { + const kf : [20]u32 = model_k(&UNITS, 1.0, CP_FIT); + const off : u32 = q_sm(OFF_FIT_V); + var i : usize = 0; + var ngmatch : u32 = 0; + while (i < N_CONV) { + assert_eq(board_vs_spec(i as u8, &kf, off), 0); + assert_eq(st, ST_JUDGE); + assert_eq(code, convert_sar(&kf, q_sm(S_VP[i]), q_sm(S_VN[i]), off)); + assert_eq(code, FIT_CODE[i]); + assert_eq(ex, FIT_CODE[i]); + assert_eq(ng, NG_CODE[i]); + on_clock(true, true); + assert_eq(st, ST_REPORT); + assert_eq(verdict, V_PASS); + if (code == NG_CODE[i]) { ngmatch = ngmatch + 1; } + i = i + 1; + } + assert_eq(ngmatch, 30); +} + +test a_conversion_takes_the_same_clocks_for_every_sample { + var i : usize = 0; + while (i < N_CONV) { + assert_eq(run_conv(i as u8), CONV_CLOCKS); + assert_eq(st, ST_JUDGE); + assert_eq(dc, DEC_LAST); + i = i + 1; + } + // the clocks are 1 (P_SMP) + 10 decisions of 7 + the last decision's 4 + assert_eq(CONV_CLOCKS, 1 + 10 * 7 + 4); + // the code is eleven bits: it never reaches 2048 + assert(code < 2048); +} + +test one_more_unit_on_the_lsb_plate_fails_exactly_where_predicted { + const kf : [20]u32 = model_k(&UNITS, 1.0, CP_FIT); + const off : u32 = q_sm(OFF_FIT_V); + var kb : [20]u32 = kf; + kb[2 * (FAULT_J as usize) + 1] = FAULT_WORD; + assert_eq(FAULT_WORD, 2 * rom_k(FAULT_J)); + assert(FAULT_WORD != rom_k(FAULT_J)); + // the spec's converter on the changed table: the pinned codes, and FAIL on the pinned conversions + var mask : u32 = 0; + var fails : u32 = 0; + var bitv : u32 = 1; + var i : usize = 0; + while (i < N_CONV) { + const c : u32 = convert_sar(&kb, q_sm(S_VP[i]), q_sm(S_VN[i]), off); + assert_eq(c, FAULT_CODE[i]); + if (sar_verdict(c, FIT_CODE[i]) == V_FAIL) { + mask = mask | bitv; + fails = fails + 1; + } + bitv = bitv << 1; + i = i + 1; + } + assert_eq(mask, FAULT_MASK); + assert_eq(fails, FAULT_FAILS); + // 16 FAIL and 15 PASS: the verdict is per conversion, not one answer for the run + assert_eq(fails + 15, 31); + // the machine with the right ROM disagrees with the changed table's converter on exactly those conversions + var dis : u32 = 0; + var dmask : u32 = 0; + bitv = 1; + i = 0; + while (i < N_CONV) { + run_conv(i as u8); + if (code != convert_sar(&kb, q_sm(S_VP[i]), q_sm(S_VN[i]), off)) { + dis = dis + 1; + dmask = dmask | bitv; + } + bitv = bitv << 1; + i = i + 1; + } + assert_eq(dis, FAULT_FAILS); + assert_eq(dmask, FAULT_MASK); +} + +test the_specs_own_two_controls_fail_every_line { + const off : u32 = q_sm(OFF_FIT_V); + // the bridge of 2 units, and Bit_8 with 3 units, each as the spec derives its whole table + const kb : [20]u32 = model_k(&UNITS, 2.0, CP_FIT); + var bad : [10]u32 = UNITS; + bad[7] = 3; + const ku : [20]u32 = model_k(&bad, 1.0, CP_FIT); + var i : usize = 0; + var failb : u32 = 0; + var failu : u32 = 0; + while (i < N_CONV) { + if (sar_verdict(convert_sar(&kb, q_sm(S_VP[i]), q_sm(S_VN[i]), off), FIT_CODE[i]) == V_FAIL) { failb = failb + 1; } + if (sar_verdict(convert_sar(&ku, q_sm(S_VP[i]), q_sm(S_VN[i]), off), FIT_CODE[i]) == V_FAIL) { failu = failu + 1; } + i = i + 1; + } + assert_eq(failb, 31); + assert_eq(failu, 31); +} + +test the_run_starts_after_lock_and_button_and_restarts_on_the_button { + go0 = false; + go1 = false; + st = ST_REPORT; + lines = 5; + cv = 17; + cs = 99; + on_clock(false, true); + on_clock(true, false); + on_clock(false, false); + assert_eq(st, ST_RUN); + assert_eq(ph, P_SMP); + assert_eq(lines, 0); + assert_eq(cv, 0); + assert_eq(cs, 0); + on_clock(true, true); + assert_eq(ph, P_SMP); + on_clock(true, true); + assert_eq(ph, P_SMP); + on_clock(true, true); + assert_eq(ph, P_SMP); + on_clock(true, true); + assert_eq(ph, P_NEG); + assert_eq(xp, rom_vp(0)); + assert_eq(xn, rom_vn(0)); + assert_eq(ex, rom_exp(0)); + assert_eq(ng, rom_ng(0)); + var k : u32 = 0; + while (st == ST_RUN) { + on_clock(true, true); + k = k + 1; + } + assert_eq(k, CONV_CLOCKS - 1); + assert_eq(code, FIT_CODE[0]); + on_clock(true, true); + assert_eq(st, ST_REPORT); + assert_eq(verdict, V_PASS); + assert_eq(cs, FIT_CODE[0] as u64); + // the button again: back to conversion 0, line 0, the fold cleared + cv = 9; + lines = 3; + 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(cv, 0); + assert_eq(lines, 0); + assert_eq(cs, 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_receipt_segments_add_up_to_a_63_character_line { + var n : usize = 0; + var s : u8 = 0; + while (s < SAR_SEGS) { + n = n + (sar_seg_last(s) as usize) + 1; + s = s + 1; + } + assert_eq(n, LINE_LEN); + // the fields: widths, and the keys K C E N S L + assert_eq(sar_width(1), 2); + assert_eq(sar_width(2), 3); + assert_eq(sar_width(5), 16); + assert_eq(sar_width(6), 4); + assert_eq(sar_key(1), 75); + assert_eq(sar_key(6), 76); + // every field sits at the top of the register: its first digit is nibble 15 + assert_eq(sar_top(1, 30, 0, 0, 0, 0, 0) >> 56, 30); + assert_eq(sar_top(2, 0, 2047, 0, 0, 0, 0) >> 52, 2047); + assert_eq(sar_top(3, 0, 0, 1000, 0, 0, 0) >> 52, 1000); + assert_eq(sar_top(4, 0, 0, 0, 1862, 0, 0) >> 52, 1862); + assert_eq(sar_top(5, 0, 0, 0, 0, 0x0123456789ABCDEF, 0), 0x0123456789ABCDEF); + assert_eq(sar_top(6, 0, 0, 0, 0, 0, 0xABCD) >> 48, 0xABCD); + assert_eq(ROUND_FOLD, 0xADF99975C7); + var f : u64 = 0; + var i : usize = 0; + while (i < N_CONV) { + f = fold(f, FIT_CODE[i]); + i = i + 1; + } + assert_eq(f, ROUND_FOLD); +} + +test the_board_prints_31_passing_lines_then_goes_round_again { + boot(0); + baud_div = 1; + var buf : [64]u8 = [0] ** 64; + var got : usize = 0; + var line : u32 = 0; + var ch : u8 = 0; + var ticks : u32 = 0; + var want : u64 = 0; + var kk : usize = 0; + var passes : u32 = 0; + while (line < 63 and ticks < 3000000) { + 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) { + assert_eq(got, LINE_LEN); + kk = (line % 31) as usize; + if (kk == 0) { want = 0; } + want = fold(want, FIT_CODE[kk]); + // "T27 SAR" + assert_eq(buf[0], 84); + assert_eq(buf[1], 50); + assert_eq(buf[2], 55); + assert_eq(buf[3], 32); + assert_eq(buf[4], 83); + assert_eq(buf[5], 65); + assert_eq(buf[6], 82); + // " K=", " C=", " E=", " N=", " S=", " L=": a space, the key, an equals sign, then the digits + assert_eq(buf[7], 32); + assert_eq(buf[8], 75); + assert_eq(buf[9], 61); + assert_eq(buf[12], 32); + assert_eq(buf[13], 67); + assert_eq(buf[14], 61); + assert_eq(buf[18], 32); + assert_eq(buf[19], 69); + assert_eq(buf[20], 61); + assert_eq(buf[24], 32); + assert_eq(buf[25], 78); + assert_eq(buf[26], 61); + assert_eq(buf[30], 32); + assert_eq(buf[31], 83); + assert_eq(buf[32], 61); + assert_eq(buf[49], 32); + assert_eq(buf[50], 76); + assert_eq(buf[51], 61); + assert_eq(hex_at(&buf, 10, 2), kk as u64); + assert_eq(hex_at(&buf, 15, 3), FIT_CODE[kk] as u64); + assert_eq(hex_at(&buf, 21, 3), FIT_CODE[kk] as u64); + assert_eq(hex_at(&buf, 27, 3), NG_CODE[kk] as u64); + assert_eq(hex_at(&buf, 33, 16), want); + assert_eq(hex_at(&buf, 52, 4), line as u64); + // " PASS\r\n" + assert_eq(buf[56], 32); + assert_eq(buf[57], 80); + assert_eq(buf[58], 65); + assert_eq(buf[59], 83); + assert_eq(buf[60], 83); + assert_eq(buf[61], 13); + assert_eq(buf[62], 10); + passes = passes + 1; + if (kk == 30) { assert_eq(want, ROUND_FOLD); } + got = 0; + line = line + 1; + } + } + } + assert_eq(line, 63); + assert_eq(lines, 63); + assert_eq(passes, 63); + baud_div = BAUD_DIV; +} + +test a_wrong_code_prints_fail_and_the_leds_follow { + boot(25); + baud_div = 1; + var buf : [64]u8 = [0] ** 64; + var got : usize = 0; + var ch : u8 = 0; + var ticks : u32 = 0; + var seen : u32 = 0; + while (st == ST_RUN) { on_clock(true, true); } + // the machine has the right code; E is changed by one before the verdict, as if the board had misconverted + ex = ex + 1; + while (seen == 0 and ticks < 100000) { + 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) { seen = 1; } + } + } + assert_eq(seen, 1); + assert_eq(got, LINE_LEN); + // K=19 is conversion 25: C is the board's 1841, E the changed 1842 (which is also what ngspice gave), N 1842 + assert_eq(hex_at(&buf, 10, 2), 25); + assert_eq(hex_at(&buf, 15, 3), 1841); + assert_eq(hex_at(&buf, 21, 3), 1842); + assert_eq(hex_at(&buf, 27, 3), 1842); + assert_eq(buf[56], 32); + assert_eq(buf[57], 70); + assert_eq(buf[58], 65); + assert_eq(buf[59], 73); + assert_eq(buf[60], 76); + baud_div = BAUD_DIV; +} From b76beea9ca85e7cc14cd55dd0202189b8147c85e Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 14:52:53 +0700 Subject: [PATCH 2/3] fpga(ax7203): sar_adc -- a line ends after its full stop bit and a two-bit-time gap; the board lost "T27 SAR " at the start of every line after the first (Closes #10910) Found on the board: every line after the first began with the same seven bytes 95 BA 02 9A 05 49 81 instead of "T27 SAR ". The cause: the transmitter set the restart request `fin` at the shift that starts the LF's stop bit (tx_left == 1), and the next conversion plus the next line's first start bit follow about 80 clocks later, 0.09 of a bit time at 868 clocks a bit. The LF's stop bit was cut to a tenth of its time, a terminal read a framing error, hunted for the next falling edge and took bit 4 of the "T" for a start bit. M1b has tens of thousands of clocks between lines, so it never showed; the 8-clocks-per-bit simulation had 10 bit times of compute between lines, so it did not show either. The fix: `fin` is set only after the last frame's stop bit has run its whole bit time and the line has been idle GAP_BITS (2) more bit times (one new register, `gap`, reset with the restart). Nothing else changes in the machine, the ROMs or the receipt. One new test (13 in all, 0 vacuous): the machine at the real divider 868 with a receiver that samples the middle of each bit reads line 0 and the first 12 bytes of line 1 with no framing error, the line was high for the stop bit and two more bit times before line 1's first start bit; with the old handshake it fails (4 framing errors). The simulation of the generated Verilog at 868 clocks a bit reads 34 lines, K = 00 .. 1E and the wrap, all equal to the expected ones. Co-Authored-By: Claude Sonnet 5.5 --- .trinity/seals/fpga_FpgaSarAdc.json | 16 ++-- specs/fpga/sar_adc_ax7203.t27 | 119 +++++++++++++++++++++++++++- 2 files changed, 126 insertions(+), 9 deletions(-) diff --git a/.trinity/seals/fpga_FpgaSarAdc.json b/.trinity/seals/fpga_FpgaSarAdc.json index 810d222e68..490d020001 100644 --- a/.trinity/seals/fpga_FpgaSarAdc.json +++ b/.trinity/seals/fpga_FpgaSarAdc.json @@ -19,23 +19,23 @@ } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:fdeddedfbdeccfd4b6c78d87c485fb9b382969cbbfb39dabbe99c5ff82af33c4", - "gen_hash_rust": "sha256:32364716a0eb63162fff91c14b35b6aeb87d2299dac87a5fcab5f5c19d2377fc", - "gen_hash_verilog": "sha256:a9a73405ddd4d1e16cd1d1692d78eae729c144a39644cf61cf23522a22041ce5", - "gen_hash_zig": "sha256:8a8cf9f903401630176bfdb0b20d9e81f81b3f63366046ea3b21ebeaaf990356", + "gen_hash_c": "sha256:cb648c123b7e68b21c2d3104308014a597c781f7bd9c74c60ca2bcf399e49ccb", + "gen_hash_rust": "sha256:d1801d59922c582d2ddbed1d68ea6eec5f5957852c725ad3bc9b899062a7a5d1", + "gen_hash_verilog": "sha256:30e45f0b102e0d2da8590d230deccad81ef5fd16ecdb0ea20438a2d9734f7f77", + "gen_hash_zig": "sha256:81b4bfac62fcdde580527a093ce82df500c4ad86e08b098ad19217ffb7694c11", "module": "FpgaSarAdc", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-19T06:43:07Z", + "sealed_at": "2026-10-19T07:43:14Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:baebf530feb0c8aa4fc034ce7aa3677edfd7f4c9ad343dccc63f9ec152571406", + "spec_hash": "sha256:a20aaba7fcbd5274a3f0b1b4b0b9613f058f0e901f9037bbaa1534f3d73ed59c", "spec_path": "specs/fpga/sar_adc_ax7203.t27", "tests": { "failed": 0, "failing": [], "forced": false, - "passed": 12, - "total": 12, + "passed": 13, + "total": 13, "vacuous": 0 }, "toolchain": { diff --git a/specs/fpga/sar_adc_ax7203.t27 b/specs/fpga/sar_adc_ax7203.t27 index aae794414a..f5445d4357 100644 --- a/specs/fpga/sar_adc_ax7203.t27 +++ b/specs/fpga/sar_adc_ax7203.t27 @@ -31,6 +31,15 @@ ; and the next clock puts the machine at conversion 0 and line 0. A finished line sets `fin` alone and the next clock starts the next ; conversion. After conversion 30 the board goes back to conversion 0, so the 31 lines repeat for as long as the capture runs (L counts on). ; - +; THE END OF A LINE (found on the board, 2026-10-19; the first build got it wrong). A line is finished when its last frame, the LF, has had its +; stop bit for the whole bit time, and the transmitter has then been idle for GAP_BITS bit times: only then is `fin` set. The first build set +; `fin` at the shift that STARTS the stop bit (tx_left == 1). M1b gets away with that, as its next line is tens of thousands of clocks away; here +; the next conversion starts about 80 clocks later, 0.09 of a bit time, so the next line's first start bit cut the LF's stop bit to a tenth of its time. A +; terminal then reads the LF with a framing error, hunts for the next falling edge, and takes bit 4 of the "T" for a start bit: every line +; after the first began with the same seven wrong bytes 95 BA 02 9A 05 49 81 and the 8-byte "T27 SAR " was lost (the fields after it were fine). +; The simulation at 8 clocks per bit did not show it, since 80 clocks were then 10 bit times: the ratio of compute to bit time is the thing, +; so the test below runs the machine at the real divider, 868, and decodes the wire with a receiver that samples the middle of each bit. +; - ; THE ROMS (if-chains: `t27b verilog` refuses array indexing; a test compares every word with the spec's own table). ; rom_vp, rom_vn q_sm(S_VP[k]), q_sm(S_VN[k]): the held top plates of conversion k, V(VDP) and V(VDN) of the ngspice run at 500 k + 98 ns ; rom_exp FIT_CODE[k]: what the spec's fitted converter gives (the board must print it as C) @@ -81,6 +90,8 @@ pub const DECS : u8 = 11; pub const DEC_LAST : u8 = 10; /// The index of the last plate (sar_cdac's PLATES - 1): the first decision moves it. pub const PLATE_LAST : u8 = 9; +/// The idle bit times after the last stop bit of a line, before the next conversion starts. +pub const GAP_BITS : u8 = 2; /// q_sm(OFF_FIT_V): +6.7 mV in units of 2^-24 V. pub const OFF_WORD : u32 = 112407; /// The clocks from P_SMP to the verdict, as a test measures them: 1 + 10 * 7 + 4. @@ -411,6 +422,7 @@ var upos : u8 = 0; var fsr : u64 = 0; var lines : u32 = 0; var last : bool = false; +var gap : u8 = 0; var hard : bool = false; var fin : bool = false; var hb : u32 = 0; @@ -464,6 +476,7 @@ fn on_clock(pll_LOCKED: bool, btn_O: bool) { upos = 0; fsr = 0; last = false; + gap = 0; fin = false; } else if (st == ST_RUN) { if (ph == P_SMP) { @@ -516,9 +529,14 @@ fn on_clock(pll_LOCKED: bool, btn_O: bool) { } 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 if (last) { + if (gap == GAP_BITS) { + fin = true; + } else { + gap = gap + 1; + } } else { tx_sh = frame(sar_char(seg, upos, fsr, verdict)); tx_left = 9; @@ -1040,3 +1058,102 @@ test a_wrong_code_prints_fail_and_the_leds_follow { assert_eq(buf[60], 76); baud_div = BAUD_DIV; } + +test a_line_ends_with_a_full_stop_bit_and_an_idle_gap_at_the_real_bit_period { + // The real divider and no shortcut: 868 clocks a bit, about 80 clocks of compute between two lines. The receiver is a terminal's: + // it hunts for a falling edge, takes the middle of the start bit, samples 8 data bits and the stop bit at the middle of each bit + // period, and counts a stop bit read low as a framing error. Line 0 is read in full, then the first 12 bytes of line 1. + boot(0); + baud_div = BAUD_DIV; + const bd : u32 = BAUD_DIV as u32; + const half : u32 = bd / 2; + var buf : [80]u8 = [0] ** 80; + var got : usize = 0; + var ticks : u32 = 0; + var prev : bool = true; + var now : bool = true; + var inframe : bool = false; + var cnt : u32 = 0; + var k : u32 = 0; + var sh : u32 = 0; + var rb : u32 = 0; + var one : u32 = 1; + var ferr : u32 = 0; + var hi : u32 = 0; + var run : u32 = 0; + var gapseen : u32 = 0; + while (got < 75 and ticks < 800000) { + on_clock(true, true); + ticks = ticks + 1; + now = uart_tx; + if (prev and !now) { + run = hi; + hi = 0; + } + if (!inframe) { + if (prev and !now) { + // the idle run before the first frame of line 1 is the one that follows line 0's LF + if (got == 63 and gapseen == 0) { gapseen = run; } + inframe = true; + cnt = 0; + rb = 0; + } + } else { + cnt = cnt + 1; + if (cnt >= half and (cnt - half) % bd == 0) { + k = (cnt - half) / bd; + if (k == 0) { + if (now) { + ferr = ferr + 1; + inframe = false; + } + } else if (k <= 8) { + if (now) { + sh = k - 1; + rb = rb | (one << sh); + } + } else { + if (!now) { ferr = ferr + 1; } + buf[got] = (rb & 255) as u8; + got = got + 1; + inframe = false; + } + } + } + if (now) { hi = hi + 1; } + prev = now; + } + assert_eq(got, 75); + assert_eq(ferr, 0); + // line 0 whole: "T27 SAR K=00 C=3EE E=3EE N=3EE S=... L=0000 PASS" CR LF + assert_eq(buf[0], 84); + assert_eq(buf[1], 50); + assert_eq(buf[2], 55); + assert_eq(buf[3], 32); + assert_eq(buf[4], 83); + assert_eq(buf[5], 65); + assert_eq(buf[6], 82); + assert_eq(hex_at(&buf, 10, 2), 0); + assert_eq(hex_at(&buf, 15, 3), FIT_CODE[0] as u64); + assert_eq(hex_at(&buf, 33, 16), FIT_CODE[0] as u64); + assert_eq(buf[57], 80); + assert_eq(buf[61], 13); + assert_eq(buf[62], 10); + // line 1 starts with the same seven characters, then " K=01": the prefix the first build lost + assert_eq(buf[63], 84); + assert_eq(buf[64], 50); + assert_eq(buf[65], 55); + assert_eq(buf[66], 32); + assert_eq(buf[67], 83); + assert_eq(buf[68], 65); + assert_eq(buf[69], 82); + assert_eq(buf[70], 32); + assert_eq(buf[71], 75); + assert_eq(buf[72], 61); + assert_eq(hex_at(&buf, 73, 2), 1); + // the line was high for the LF's whole stop bit and GAP_BITS more bit times before line 1's first start bit + assert(gapseen >= (1 + (GAP_BITS as u32)) * bd); + assert(gapseen < (1 + (GAP_BITS as u32)) * bd + 200); + assert_eq(GAP_BITS, 2); + baud_div = BAUD_DIV; +} From 4b53ed61a91561786944c13b882801b5b2e826db Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 15:03:09 +0700 Subject: [PATCH 3/3] fpga(ax7203): sar_adc -- header wording: the terminal takes the fourth data bit of the "T" for a start bit (comment only, Closes #10910) Comment-only change in the spec header: the generated Verilog is byte for byte the one the _v2 bitstreams were built from (sha256 d8e31fdcc479...), and the seal's generated-code hashes are unchanged; only spec_hash moves. Co-Authored-By: Claude Sonnet 5.5 --- .trinity/seals/fpga_FpgaSarAdc.json | 4 ++-- specs/fpga/sar_adc_ax7203.t27 | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.trinity/seals/fpga_FpgaSarAdc.json b/.trinity/seals/fpga_FpgaSarAdc.json index 490d020001..4efe86e187 100644 --- a/.trinity/seals/fpga_FpgaSarAdc.json +++ b/.trinity/seals/fpga_FpgaSarAdc.json @@ -26,9 +26,9 @@ "module": "FpgaSarAdc", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-19T07:43:14Z", + "sealed_at": "2026-10-19T07:59:22Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:a20aaba7fcbd5274a3f0b1b4b0b9613f058f0e901f9037bbaa1534f3d73ed59c", + "spec_hash": "sha256:54c6f2c7e86c000f060cf8efab0123386431999ae803b285d364011b5aa89691", "spec_path": "specs/fpga/sar_adc_ax7203.t27", "tests": { "failed": 0, diff --git a/specs/fpga/sar_adc_ax7203.t27 b/specs/fpga/sar_adc_ax7203.t27 index f5445d4357..3d8d73320f 100644 --- a/specs/fpga/sar_adc_ax7203.t27 +++ b/specs/fpga/sar_adc_ax7203.t27 @@ -35,7 +35,7 @@ ; stop bit for the whole bit time, and the transmitter has then been idle for GAP_BITS bit times: only then is `fin` set. The first build set ; `fin` at the shift that STARTS the stop bit (tx_left == 1). M1b gets away with that, as its next line is tens of thousands of clocks away; here ; the next conversion starts about 80 clocks later, 0.09 of a bit time, so the next line's first start bit cut the LF's stop bit to a tenth of its time. A -; terminal then reads the LF with a framing error, hunts for the next falling edge, and takes bit 4 of the "T" for a start bit: every line +; terminal then reads the LF with a framing error, hunts for the next falling edge, and takes the fourth data bit of the "T" for a start bit: every line ; after the first began with the same seven wrong bytes 95 BA 02 9A 05 49 81 and the 8-byte "T27 SAR " was lost (the fields after it were fine). ; The simulation at 8 clocks per bit did not show it, since 80 clocks were then 10 bit times: the ratio of compute to bit time is the thing, ; so the test below runs the machine at the real divider, 868, and decodes the wire with a receiver that samples the middle of each bit.