From e9b142504e265d3b54f51ff5518320415774780f Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 14:51:36 +0700 Subject: [PATCH] fpga(ax7203): rc_filter without Verilog real -- f64 references in the tests, comptime_float PLL params (Closes #10294) #10278 merged at its first commit, before its own reds were fixed: - fpga-lint: t27c gen-verilog emits a module-level f64 fn as `function real` and an f64 param as `input real`; yosys read_verilog -sv refuses both (TOK_REAL). The f64 backward-Euler references now run inline in the tests, compared as squares, and PLLE2_ADV takes comptime_float. Same bounds as before; the clocked machine is unchanged. - duplicate-bodies: hex_digit blessed (the copy in ddr3_head_bandwidth is deliberate, t27b bitstream specs are self-contained). - elab ratchet: rc_filter_ax7203 8 recorded as a KNOWN GAP (t27c has no lowering for pin attributes or primitive instances; t27b builds the bitstream), plus 0 rows for three modules master added without one. Lab: 10/10 tests, 0 vacuous; seal spec_hash 3728871b. t27b top.v logic same as the board-verified build. Board: bitstream e619e966, 2130 of 2130 consecutive lines PASS. Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/fpga_FpgaRcFilter.json | 12 ++-- specs/fpga/rc_filter_ax7203.t27 | 96 +++++++++++++++------------ tools/duplicate_bodies_baseline.txt | 1 + tools/elab_baseline.txt | 15 +++++ 4 files changed, 75 insertions(+), 49 deletions(-) diff --git a/.trinity/seals/fpga_FpgaRcFilter.json b/.trinity/seals/fpga_FpgaRcFilter.json index 1a7e057540..471a0e661d 100644 --- a/.trinity/seals/fpga_FpgaRcFilter.json +++ b/.trinity/seals/fpga_FpgaRcFilter.json @@ -2,16 +2,16 @@ "built_by": "t27c-bootstrap@0.5.2+a86b691b1", "closure": [], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:6badf72a9b42f3f2f22a6a47b675a1a358d8eda511aa5891ba5840233022c08d", - "gen_hash_rust": "sha256:22908f9adf0a9fd001ce4698a55e4e9964d6b1fa24282c33dcf8768721988e9f", - "gen_hash_verilog": "sha256:12175721fae881e0794cafc4a07355802e5428893d122961b849532cb47e22a6", - "gen_hash_zig": "sha256:175dfc240569063b01740f40484a3e2afc90a2dc41c498b709ce4934ca8139bb", + "gen_hash_c": "sha256:0d8d5fc925210336cd05292836dcc30da5e845d60285427c76658a303d56be96", + "gen_hash_rust": "sha256:156ba364b202e548825093b2ddb417ea72d7d6ed9f69ead68bc54b41f396b85b", + "gen_hash_verilog": "sha256:90bddb94a07f0f42bd10ae74e9c011101f39c2dc325baac08e041e1d2df7e91b", + "gen_hash_zig": "sha256:acb0b5b1fabeb7c69bbdc1b34adaaaedd1288c23474fa2fe05dc81568afa5850", "module": "FpgaRcFilter", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T07:16:04Z", + "sealed_at": "2026-10-18T07:41:41Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:8b7a454463add58280616ceefc638bb819ab72e3c2d1e8f445a5fad0213dfc2b", + "spec_hash": "sha256:3728871b26cf0504c6e76306f7633547787c034d04da93493229cbd229d8e36a", "spec_path": "specs/fpga/rc_filter_ax7203.t27", "tests": { "failed": 0, diff --git a/specs/fpga/rc_filter_ax7203.t27 b/specs/fpga/rc_filter_ax7203.t27 index 24d09031ac..62e8600276 100644 --- a/specs/fpga/rc_filter_ax7203.t27 +++ b/specs/fpga/rc_filter_ax7203.t27 @@ -149,28 +149,13 @@ pub fn verdict_of(a: u32, b: u32, s: u64) -> u8 { return V_FAIL; } -; --- the double-precision references, for the tests -------------------------------------------------- +; --- the double-precision references live in the tests ---------------------------------------------- +; t27c gen-verilog turns a module-level f64 fn into a Verilog `function real`, which yosys refuses, +; so the f64 backward-Euler runs are written inline in the tests and compared as squares: +; |d| < t is d * d < t * t. -pub fn fabs(x: f64) -> f64 { - if (x < 0.0) { return 0.0 - x; } - return x; -} - -/// A raw voltage in volts. -pub fn volts(raw: u32) -> f64 { - return (raw as f64) / 16777216.0; -} - -/// Backward Euler in f64 from 0 V with a 1 V input: n steps of v' = (v + a) / (1 + a). -pub fn be_charge(n: u32, a: f64) -> f64 { - var v : f64 = 0.0; - var k : u32 = 0; - while (k < n) { - v = (v + a) / (1.0 + a); - k = k + 1; - } - return v; -} +/// Volts per raw unit is 1 / SCALE. +pub const SCALE : f64 = 16777216.0; ; --- the receipt -------------------------------------------------------------------------------- @@ -259,7 +244,7 @@ pub fn BUFG(I: bool) -> BufgOut {} /// A PLL: 200 MHz in, VCO = 200 * 8 = 1600 MHz, CLKOUT0 = 1600 / 16 = 100 MHz; CLKFBOUT feeds CLKFBIN. /// The settings are the ones LiteDRAM's S7PLL used on this board for the DDR3 cell, which locked. pub struct PllOut { CLKOUT0: bool, CLKFBOUT: bool, LOCKED: bool } -pub fn PLLE2_ADV(CLKIN1: bool, CLKFBIN: bool, RST: bool, PWRDWN: bool, CLKIN1_PERIOD: f64, REF_JITTER1: f64, CLKFBOUT_MULT: comptime_int, DIVCLK_DIVIDE: comptime_int, CLKOUT0_DIVIDE: comptime_int, CLKOUT0_PHASE: comptime_int, STARTUP_WAIT: str) -> PllOut {} +pub fn PLLE2_ADV(CLKIN1: bool, CLKFBIN: bool, RST: bool, PWRDWN: bool, CLKIN1_PERIOD: comptime_float, REF_JITTER1: comptime_float, CLKFBOUT_MULT: comptime_int, DIVCLK_DIVIDE: comptime_int, CLKOUT0_DIVIDE: comptime_int, CLKOUT0_PHASE: comptime_int, STARTUP_WAIT: str) -> PllOut {} /// An input buffer, so the button reaches on_clock as an instance output (btn_O). pub struct IbufOut { O: bool } @@ -431,7 +416,8 @@ fn on_clock(pll_LOCKED: bool, btn_O: bool) { test the_coefficient_is_one_over_21 { assert_eq(G21 * 21, (ONE as u64) - 1); assert_eq(TAU_NS, R_OHM * C_PF / 1000); - assert fabs(0.05 / 1.05 - 1.0 / 21.0) < 0.000000000000001; + const dg : f64 = 0.05 / 1.05 - 1.0 / 21.0; + assert dg * dg < 0.000000000000001 * 0.000000000000001; assert_eq(mul_g21(1), G21); assert_eq(mul_g21(ONE), (ONE as u64) * G21); assert_eq(mul_g21(12345678), 12345678 * G21); @@ -448,23 +434,36 @@ test the_first_steps_are_backward_euler { assert_eq(rc_step(ONE, ONE), ONE); assert_eq(rc_step(0, 0), 0); assert_eq(rc_step_g(1559786, ONE, G21), rc_step(1559786, ONE)); - assert fabs(volts(rc_step(0, ONE)) - be_charge(1, 0.05)) < 0.00000006; - assert fabs(volts(rc_step(798915, ONE)) - be_charge(2, 0.05)) < 0.00000006; + const x1 : f64 = 0.05 / 1.05; + const x2 : f64 = (x1 + 0.05) / 1.05; + const r1 : u32 = rc_step(0, ONE); + const r2 : u32 = rc_step(798915, ONE); + const d1 : f64 = (r1 as f64) / SCALE - x1; + const d2 : f64 = (r2 as f64) / SCALE - x2; + assert d1 * d1 < 0.00000006 * 0.00000006; + assert d2 * d2 < 0.00000006 * 0.00000006; } test the_charge_at_5_us_is_cpphdls_0_992396 { var v : u32 = 0; + var x : f64 = 0.0; var k : u32 = 0; while (k < CHARGE_STEPS) { v = rc_step(v, ONE); + x = (x + 0.05) / 1.05; k = k + 1; } assert_eq(v, EXP_A); - assert fabs(volts(v) - CPPHDL_5US) < 0.0000005; - assert fabs(volts(v) - be_charge(100, 0.05)) < 0.0000002; - assert fabs(be_charge(100, 0.05) - CPPHDL_5US) < 0.0000005; - assert fabs(be_charge(100, 0.05) - ANALYTIC_5US) > 0.0008; - assert fabs(be_charge(100, 0.05) - ANALYTIC_5US) < 0.0009; + const vv : f64 = (v as f64) / SCALE; + const dc : f64 = vv - CPPHDL_5US; + const dx : f64 = vv - x; + const xc : f64 = x - CPPHDL_5US; + const xa : f64 = x - ANALYTIC_5US; + assert dc * dc < 0.0000005 * 0.0000005; + assert dx * dx < 0.0000002 * 0.0000002; + assert xc * xc < 0.0000005 * 0.0000005; + assert xa * xa > 0.0008 * 0.0008; + assert xa * xa < 0.0009 * 0.0009; } test the_whole_run_stays_within_3_lsb_of_f64 { @@ -473,36 +472,47 @@ test the_whole_run_stays_within_3_lsb_of_f64 { var sum : u64 = 0; var worst : f64 = 0.0; var k : u32 = 0; - var e : f64 = 0.0; + var d : f64 = 0.0; + var u : u32 = 0; while (k < STEPS) { - v = rc_step(v, vin_at(k)); - x = (x + 0.05 * volts(vin_at(k))) / 1.05; + u = vin_at(k); + v = rc_step(v, u); + x = (x + 0.05 * ((u as f64) / SCALE)) / 1.05; sum = fold(sum, v); - e = fabs(volts(v) - x); - if (e > worst) { worst = e; } + d = (v as f64) / SCALE - x; + if (d * d > worst) { worst = d * d; } k = k + 1; } assert_eq(v, EXP_B); assert_eq(sum, EXP_S); - assert worst < 3.0 / 16777216.0; + assert worst < (3.0 / SCALE) * (3.0 / SCALE); assert worst > 0.0; assert_eq(verdict_of(EXP_A, v, sum), V_PASS); } test halving_the_step_converges_toward_the_analytic { - const e1 : f64 = fabs(be_charge(100, 0.05) - ANALYTIC_5US); - const e2 : f64 = fabs(be_charge(200, 0.025) - ANALYTIC_5US); - assert e2 < e1; - assert e1 / e2 > 1.9; - assert e1 / e2 < 2.1; + var x1 : f64 = 0.0; + var x2 : f64 = 0.0; var v : u32 = 0; var k : u32 = 0; while (k < 200) { + if (k < 100) { x1 = (x1 + 0.05) / 1.05; } + x2 = (x2 + 0.025) / 1.025; v = rc_step_g(v, ONE, 409200); k = k + 1; } - assert fabs(volts(v) - be_charge(200, 0.025)) < 0.000002; - assert fabs(volts(v) - ANALYTIC_5US) < e1; + const d1 : f64 = x1 - ANALYTIC_5US; + const d2 : f64 = x2 - ANALYTIC_5US; + const q1 : f64 = d1 * d1; + const q2 : f64 = d2 * d2; + assert q2 < q1; + assert q1 / q2 > 1.9 * 1.9; + assert q1 / q2 < 2.1 * 2.1; + const vv : f64 = (v as f64) / SCALE; + const dv : f64 = vv - x2; + const da : f64 = vv - ANALYTIC_5US; + assert dv * dv < 0.000002 * 0.000002; + assert da * da < q1; } test the_fold_knows_the_order_and_a_wrong_rounding_fails { diff --git a/tools/duplicate_bodies_baseline.txt b/tools/duplicate_bodies_baseline.txt index a50d17052c..151dae65ca 100644 --- a/tools/duplicate_bodies_baseline.txt +++ b/tools/duplicate_bodies_baseline.txt @@ -104,6 +104,7 @@ get 2 hard_sigmoid 2 has_at 2 has_star_inner 2 +hex_digit 2 hw_place_before 2 id_seen_before 2,2 is_counter_power_of_two 2 diff --git a/tools/elab_baseline.txt b/tools/elab_baseline.txt index ad26ec0c9b..c3fbd70676 100644 --- a/tools/elab_baseline.txt +++ b/tools/elab_baseline.txt @@ -46,6 +46,17 @@ # branch that merged master. Both elaborate clean; a 0 row hides nothing. # `eth_rx 0` (#8333) arrives with its spec; it elaborates clean too. # `trinet_node 0` (#8356) arrives with its spec; it elaborates clean too. +# +# 2026-10-18: +8. `rc_filter_ax7203 8` is a NEW module +# (specs/fpga/rc_filter_ax7203.t27, #10278) and a KNOWN GAP, not a regression: +# the spec is written for `t27b verilog`, which is what builds its bitstream +# (board receipt PASS). t27c gen-verilog has no lowering for its pin attributes +# or primitive instances: 3 pins read `undefined`, and IBUFDS, PLLE2_ADV, BUFG +# and IBUF become localparams with a function call (5 errors, one of them the +# PLL's feedback loop read as a recursive parameter). Same class as +# ddr3_head_bandwidth, which is left to that spec's owner. +# `openxc7_dsp_fabric 0`, `wasm_board_ax7203 0` and `wasm_interp 0` reached +# master without rows; all elaborate clean, so a 0 row hides nothing. adapter 0 apb_bridge 4 assembler 4 @@ -74,10 +85,12 @@ mac 0 memory 5 mmcm 2 mtbf 2 +openxc7_dsp_fabric 0 partition 2 placement 6 power 2 power_analysis 1 +rc_filter_ax7203 8 reset_sync 2 rgmii 0 rgmii_sniff 0 @@ -96,4 +109,6 @@ trinet_node 0 uart 0 vcd_conformance_compare 13 vcd_trace 14 +wasm_board_ax7203 0 +wasm_interp 0 zerodsp_top 5