diff --git a/.trinity/seals/analog_AnalogMosPsp103Data.json b/.trinity/seals/analog_AnalogMosPsp103Data.json index 36ff7cbdba..90f1986230 100644 --- a/.trinity/seals/analog_AnalogMosPsp103Data.json +++ b/.trinity/seals/analog_AnalogMosPsp103Data.json @@ -7,23 +7,23 @@ } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:b54bb70dcdaad8eac3180a3a51ee5d30d340b951edd734d4e817c161c1081f94", - "gen_hash_rust": "sha256:22cfdd782fe043555e0aa880bf922c2de502545f50aa5c92fb3e27fb0231fd2a", - "gen_hash_verilog": "sha256:f0e9948d7d18bf642dceae55962767fd570aea0a3c5dd0590d315566afc3509a", - "gen_hash_zig": "sha256:c9e11b43a265e022f096562ce39f6963dea17aa55489c83ccf2fc953ba1c186e", + "gen_hash_c": "sha256:83abce2660327df33c17d296932949f34452d4c2da56e9d585073079e3b6af7f", + "gen_hash_rust": "sha256:abdec74a2de33e2b249ef77300bc550827a82a3bda849fe2225b58df71ef8d7e", + "gen_hash_verilog": "sha256:1a459f8111272cef5616af605e2fa8500e76b86f24d2648606d6a352a309af82", + "gen_hash_zig": "sha256:a2d2c04035b7511edc876b496e7ebc0b417b35956a48783b22f1afb71ec4c5db", "module": "AnalogMosPsp103Data", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-20T03:08:15Z", + "sealed_at": "2026-10-20T03:32:22Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:c4d59c5d87b03810373bfabb9024f4e1051184f3abab9a613e02ab0ae54848d9", + "spec_hash": "sha256:86e7c154c88a325e41ff4a154a3b766cb8d65e89e2ea82176b46ee4fc523dd74", "spec_path": "specs/analog/mos_psp103_data.t27", "tests": { "failed": 0, "failing": [], "forced": false, - "passed": 11, - "total": 11, + "passed": 12, + "total": 12, "vacuous": 0 }, "toolchain": { diff --git a/.trinity/seals/fpga_FpgaPsp103Inv.json b/.trinity/seals/fpga_FpgaPsp103Inv.json new file mode 100644 index 0000000000..ecf9c38756 --- /dev/null +++ b/.trinity/seals/fpga_FpgaPsp103Inv.json @@ -0,0 +1,53 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+42a4860c4", + "closure": [ + { + "spec": "specs/analog/linear.t27", + "spec_hash": "sha256:3ddef7be183aba583ed285334ee389b48a65b41335e98914514235db7c4e5d62" + }, + { + "spec": "specs/analog/mos_psp103.t27", + "spec_hash": "sha256:e04b69e5c43188a3d46a4c0949cfc727f239721de73fb46e92c8a845bbbbc98e" + }, + { + "spec": "specs/analog/mos_psp103_data.t27", + "spec_hash": "sha256:86e7c154c88a325e41ff4a154a3b766cb8d65e89e2ea82176b46ee4fc523dd74" + }, + { + "spec": "specs/analog/mos_table.t27", + "spec_hash": "sha256:54e248069ae620d18d260231e238b6bc42dc3c65792bd1673b162c2dc97b2edb" + }, + { + "spec": "specs/fpga/rc_filter_ax7203.t27", + "spec_hash": "sha256:be3af1aa6195d51e46289121cfd42623c80cd42d863442f4f6f69109da06d32f" + }, + { + "spec": "specs/fpga/sar_adc_ax7203.t27", + "spec_hash": "sha256:4db9099fe0019743e3300f8281fffcfe33ad653d7f953dee149749ee7d332888" + } + ], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:b771fb1b1fcc4f15da4406867270ee816694efc0599624dfffbbbb27d8b8646c", + "gen_hash_rust": "sha256:6f3c61044f101192974b16e4cc2370fb521d030cfbb7db75d6a5c9cbd37c8c46", + "gen_hash_verilog": "sha256:01be0dc34ed7c33c9db90ae2017f7a12a4da24da08b5abd5ffdda186fb590c8d", + "gen_hash_zig": "sha256:1dc394384cd096057be4350fa242682fde32dea71336bafd54a334de8a06d3ff", + "module": "FpgaPsp103Inv", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-20T03:38:21Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:7b0a701839d65311137e8e03e564b0d60526286090390683f912592a3391dd4c", + "spec_path": "specs/fpga/psp103_inv_ax7203.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 15, + "total": 15, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:8512b80da533b79289110fca4a65f3336abd7a059ca4b72ea595d5e33ff8ad10", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/.trinity/seals/fpga_FpgaSarAdc.json b/.trinity/seals/fpga_FpgaSarAdc.json index 4efe86e187..740b8ef024 100644 --- a/.trinity/seals/fpga_FpgaSarAdc.json +++ b/.trinity/seals/fpga_FpgaSarAdc.json @@ -1,5 +1,5 @@ { - "built_by": "t27c-bootstrap@0.5.2+ea35d9b72", + "built_by": "t27c-bootstrap@0.5.2+42a4860c4", "closure": [ { "spec": "specs/analog/linear.t27", @@ -7,7 +7,7 @@ }, { "spec": "specs/analog/sar_adc.t27", - "spec_hash": "sha256:48e8825a4a6a7fc24ce23472bcba5499dcafbd399ac45a14fb153a0a020018e2" + "spec_hash": "sha256:208a64705a1d07ff14d3131d999135a3d5da6c7cb9bc2e919430d7e60b34db68" }, { "spec": "specs/analog/sar_cdac.t27", @@ -22,13 +22,13 @@ "gen_hash_c": "sha256:cb648c123b7e68b21c2d3104308014a597c781f7bd9c74c60ca2bcf399e49ccb", "gen_hash_rust": "sha256:d1801d59922c582d2ddbed1d68ea6eec5f5957852c725ad3bc9b899062a7a5d1", "gen_hash_verilog": "sha256:30e45f0b102e0d2da8590d230deccad81ef5fd16ecdb0ea20438a2d9734f7f77", - "gen_hash_zig": "sha256:81b4bfac62fcdde580527a093ce82df500c4ad86e08b098ad19217ffb7694c11", + "gen_hash_zig": "sha256:92d85db28d226f9dbafbe5ea6c949ebd7c6050e4ab7883eecc26b2b8627c2795", "module": "FpgaSarAdc", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-19T07:59:22Z", + "sealed_at": "2026-10-20T03:38:27Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:54c6f2c7e86c000f060cf8efab0123386431999ae803b285d364011b5aa89691", + "spec_hash": "sha256:4db9099fe0019743e3300f8281fffcfe33ad653d7f953dee149749ee7d332888", "spec_path": "specs/fpga/sar_adc_ax7203.t27", "tests": { "failed": 0, diff --git a/docs/analog/board-psp103-inv-2026-10-20.md b/docs/analog/board-psp103-inv-2026-10-20.md new file mode 100644 index 0000000000..fd1c37558a --- /dev/null +++ b/docs/analog/board-psp103-inv-2026-10-20.md @@ -0,0 +1,121 @@ +# Board run of the PSP103 inverter, tt corner, tables in block RAM, 2026-10-20 + +Issue #11208 (M3d, success criterion SC-003 of the analog epic #10486), a lane of the night loop #11063. English, ASCII only. + +This is the first analog board top that reads the PSP103 tables: `specs/fpga/psp103_inv_ax7203.t27` runs the 500 fF CMOS inverter of `specs/analog/mos_psp103.t27` (400 backward Euler steps of dt = 100 ps, tt current and drain-charge tables, three Newton iterations a step) on the ALINX AX7203, holds the four tables and the 400 expected samples in block RAM, and prints one UART line per step. Every number below was measured in this run. + +What this document does not say: nothing about speed, power or value. Fmax is nextpnr's post-route estimate for one placement of one netlist. A PASS says the board agrees with the spec's own fixed-point run, which `mos_psp103.t27` puts within 0.020 % (rise) and 0.0041 % (fall) of ngspice's 50 % delays at tt; it does not say anything about another corner, another load or another gate waveform. + +## 1. The run + +- Source: the specs as committed at `8e76e1b1a` on `lane/m3d-11208` (`psp103_inv_ax7203.t27`, and `mos_psp103_data.t27` with its clocked port and `TT_RUN`). Nothing was edited between the commit and the build; the control is a scratch copy (section 2). +- Compilers: `t27c` sha256 `016fb83b7f02d045...` and `t27b` sha256 `d7ec5790dc29b3f3...`, the release binaries of the shared build directory. +- Toolchain: yosys 0.63 (git 70a11c6bf0e8dd669f56c7da3587f78b405138e2), the openXC7 fork of nextpnr-xilinx and prjxray from the shared build directory, chipdb `xc7a200tfbg484-2.bin` (md5 `59f828c441e6e6081bfee63ff994660e`), `openFPGALoader v1.1.1`. +- Board and cable: ALINX AX7203, `xc7a200tfbg484-2`. `t27c boards` named the cable: `--busdev-num 1:4 idcode 0x3636093 family artix a7 200t` (Digilent HS2, FT232H). UART: the CP2102N bridge of the board, 115200 baud 8N1, pin N15, read by one reader from the terminal tab of the desktop app, started before the load; the port was free before and after. +- Programming: SRAM only (`openFPGALoader` without `-f` or `-m`; the output shows `Load SRAM` and `done 1`). No flash memory and no eFUSE was written. +- Disk: free space on `/` was 5.3 to 6.5 GiB during the run (the lane brief's floor is 5 GiB); each 22 MB frames file was deleted once its bitstream existed. + +## 2. How it was built + +`$O` is the shared openXC7 build directory, `$B` a scratch output directory. + +``` +t27b verilog specs/fpga/psp103_inv_ax7203.t27 > $B/top.v # 1215 lines, module FpgaPsp103Inv +t27c gen-verilog specs/analog/mos_psp103_data.t27 > $B/data.v # 39959 lines, module AnalogMosPsp103Data +yosys -l $B/x.log $B/x.ys + # x.ys: + read_verilog -sv $B/top.v $B/data.v + synth_xilinx -family xc7 -top FpgaPsp103Inv -flatten -abc9 -nodsp -nosrl -run :coarse + techmap -map +/cmp2lut.v -map +/cmp2lcu.v -D LUT_WIDTH=6 + alumacc + opt + memory -nomap + opt_clean + setattr -set ram_style "block" t:$mem_v2 + synth_xilinx -family xc7 -top FpgaPsp103Inv -flatten -abc9 -nodsp -nosrl -run map_memory: + stat + write_json $B/x.json +$O/np-main/build/nextpnr-xilinx --chipdb $O/xc7a200tfbg484-2.bin --json $B/x.json --fasm $B/x.fasm --freq 100 [--seed 2] --log $B/x.pnr.log +PYTHONPATH=$O/prjxray $O/venv/bin/python3 $O/prjxray/utils/fasm2frames.py --db-root $O/prjxray-db/artix7 --part xc7a200tfbg484-2 $B/x.fasm $B/x.frames +$O/px-main/build/tools/xc7frames2bit --part_file $O/prjxray-db/artix7/xc7a200tfbg484-2/part.yaml --part_name xc7a200tfbg484-2 --frm_file $B/x.frames --output_file $B/x.bit +openFPGALoader -c digilent_hs2 --busdev-num 1:4 $B/x.bit # SRAM only +``` + +The pins are attributes in the spec, so there is no constraint file and no hand-written Verilog: the board top is `t27b verilog` output, the RAM is `t27c gen-verilog` output. The one line that is not in the spec is `setattr -set ram_style "block"`, a yosys directive in the build script (see section 6). + +The negative control is the same `top.v` and a `data.v` generated from a scratch copy of `mos_psp103_data.t27` whose `on_clock` reads `SS_N`, `SS_P`, `SS_QD_N`, `SS_QD_P` instead of the four `TT_` tables (the copy lived in `specs/analog/` for one command, because a `use` does not resolve elsewhere, and was deleted). The two generated `data.v` files differ in exactly four lines, the four table reads. The expected samples (`TT_RUN`) are the tt ones in both. + +## 3. The board table + +| | tt top | ss control | +|---|---|---| +| `top.v` sha256 | `5bf24f964e7f59358b02a5a931a72c51b01255c04c1ec310e082eda1d5abd84e` | the same | +| `data.v` sha256 | `91a80c709ab09eb99bb09bcc18d833c3cd5c084dcddc2f35e0014b4cec9c6dd0` | `12b85f1c16f12127...` | +| LUT (yosys, LUT2..LUT6) | 1426 (LUT2 461, LUT3 172, LUT4 165, LUT5 334, LUT6 294; plus 170 INV) | 1422 (468, 198, 198, 311, 247; plus 170 INV) | +| FF | 1219 (FDRE 1196, FDSE 23) | 1219 (1196, 23) | +| DSP48E1 | 0 | 0 | +| BRAM | 4 RAMB36E1 + 1 RAMB18E1 (the four 625-word tables and the 400-word run) | 4 RAMB36E1 + 1 RAMB18E1 | +| LUT ROM | none: the tables are in block RAM, not in LUTs | none | +| CARRY4 (yosys / nextpnr) | 207 / 211 | 207 / 211 | +| nextpnr SLICE_LUTX / SLICE_FFX | 2768 / 1219 of 269200 | 2764 / 1219 | +| Fmax before routing (first line) | 72.73 MHz (FAIL at 100) | 78.61 MHz (seed 2) | +| Fmax after routing (second line) | **103.61 MHz** (PASS at 100) | **107.33 MHz** (PASS at 100), seed 2; seed 1 gave 96.57 MHz (FAIL) | +| frames file | 20230 lines, no fasm2frames error | 20230 | +| receipt lines, well-formed | 1217 (L = 0 to 1216, no gap) | 1217 (L = 0 to 1216, no gap) | +| lines whose Y equals the spec's sample | 1217 of 1217 (tt run) | 1217 of 1217 (ss run) | +| PASS / FAIL | **1217 / 0** | 231 / 986 | +| a complete round (N = 0 .. 399) | 400 of 400 PASS, S at N = 18F `0x215DC5EAC4C48576` = `EXP_S_TT_Q` | 77 PASS, 323 FAIL, S at N = 18F `0x987F22AC4132345B` = `EXP_S_SS_Q` | + +Resources are the same order as the SAR top (908 LUT, 538 FF) plus the multiplier, the divider and the 64-bit accumulators; the tables cost no LUT. + +## 4. The captures + +Each capture is 7 seconds, one reader, started before the load. A line is well-formed when it matches `T27 PSP N=<3 hex> Y=<7 hex> E=<7 hex> S=<16 hex> L=<4 hex> (PASS|FAIL)` exactly; only well-formed lines are counted. Before the new configuration took over, the previous design on the board was still printing: in the tt capture 17 lines of the SAR top and a fragment, in the control capture ten whole lines of the tt top (L = 0xD4F6 and up) and three fragments. The last line of each capture is cut where the reader is killed. Those are the only malformed lines, and the first line of our design, `L=0000`, is intact in both captures (it follows the cut tail of the previous design's line on the same text line; the judge looks for the receipt grammar inside a line and starts at the first `N=000 .. L=0000` line, and says how many lines of the previous design it dropped: 0 for the tt capture, 10 for the control). + +| | tt top | ss control | +|---|---|---| +| capture bytes / sha256 | 81485, `b34dafeae9e75c46...` | 81221, `bc4d0dfa86f7be9e...` | +| bitstream sha256 (header carries a time) | `29994e0d605d6812...` | `8f8db254206f496c...` | +| lines starting with `T27 ` | 1235 | 1230 | +| well-formed lines of the design | 1217 | 1217 | +| N sequence | 0, 1, .., 399, 0, 1, .. with no break | the same | +| S of every line = fold of the spec's samples up to N | 1217 of 1217 | 1217 of 1217 (ss samples) | +| verdict differs from the spec's prediction | 0 of 1217 | 0 of 1217 | + +First lines of the tt capture and the control, for the record: + +``` +tt T27 PSP N=000 Y=00A8451 E=00A8451 S=00000000000A8451 L=0000 PASS + T27 PSP N=001 Y=019C356 E=019C356 S=00000000000CCBF4 L=0001 PASS +control T27 PSP N=000 Y=009C1F2 E=00A8451 S=000000000009C1F2 L=0000 FAIL + T27 PSP N=001 Y=017FB6A E=019C356 S=000000000004788E L=0001 FAIL +``` + +### The control, step by step + +`mos_psp103.t27`'s own ss run (`run_fix_q` on `SS_N`, `SS_P`, `SS_QD_N`, `SS_QD_P` from the tt rest value of 3 units) differs from the tt run at 323 of the 400 steps: every step except 145 (the one place the ss output crosses the tt output) and 324 to 399 (both back at the rest value). A test in `psp103_inv_ax7203.t27` pins that (`CTRL_FAILS`, `CTRL_PASS_AT`, `CTRL_SETTLED_FROM`, `EXP_S_SS_Q`) and a second test runs the machine on the ss tables and gets the same verdicts. On the board: + +| | predicted | measured | +|---|---|---| +| FAIL steps in a round | 323: N = 0 .. 144, 146 .. 323 | the same 323 steps, in every one of the three rounds | +| PASS steps in a round | 77: N = 145 and 324 .. 399 | the same 77 | +| Y on every line | the ss run's sample | 1217 of 1217 | +| S at N = 18F | `EXP_S_SS_Q` = `0x987F22AC4132345B` | `0x987F22AC4132345B` | + +## 5. Tests + +`t27c test-report specs/fpga/psp103_inv_ax7203.t27`: 15 tests, 15 pass, 0 fail, 0 vacuous (runtime asserts per test from 11 to 14482). `t27c test-report specs/analog/mos_psp103_data.t27`: 11 tests, 11 pass, 0 fail, 0 vacuous. `t27b test specs/fpga/psp103_inv_ax7203.t27 --check` and `t27b test specs/analog/mos_psp103_data.t27 --check` exit 0; for the board top t27b prints `runtime asserts unknown`, because its interpreter's fuel (20 million steps a file, `specs/tri/t27b/check_budget.t27`) runs out in the whole-run tests (a 400-step run is about 760000 clocks, and the UART test and the control run it again): the JIT ran all 15 tests and they pass; the interpreter agrees on the part it had fuel for. + +## 6. What differed from the plan, and traps + +1. **`t27c gen-verilog` writes nothing for an array that came in by `use`.** The reference is left undeclared (the same defect #8769 records for functions), so the tables could not be read from the board spec. The memory is therefore generated from the module that owns the arrays: `mos_psp103_data.t27` got a clocked port next to them (`on_clock(addr, idx)`, five output registers) and the board top instantiates it as an extern, like the PLL. A minimal repro for #5980: a spec with `use analog::mos_psp103_data::{TT_N};` and `on_clock` reading `TT_N[addr]` generates Verilog with `TT_N` undeclared. +2. **yosys maps a 625-word ROM to flip-flops and LUTs** (about 1270 LUT, 909 of them LUT6, and 79 FDRE for the four tables in a probe) unless the memory carries `ram_style = "block"`; with it the same module is 4 RAMB36E1 and no LUT. `gen-verilog` cannot write the attribute, so the build script sets it with `setattr` on the `$mem_v2` cells. Worth a rule in `gen-verilog` (an attribute on a const array that the spec marks) or in `t27c silicon`. +3. **A `const rst_n` in a `gen-verilog` module makes yosys refuse the process** (`negedge` of a constant: "Multiple edge sensitive events found"). The data module leaves `rst_n` and `en` as ports and the top ties them to 1, which `flatten` and `opt` fold into plain flip-flops, so the memory's read register merges into the block RAM. +4. **Names of module vars must not collide with locals of imported functions** (`acc`, `y0`, `lo`, `hi`, `cx`, `fx`: `blend`, `id_of` and the rest declare them): t27b refuses a local that shadows a module var. The datapath registers are `r_`-prefixed. +5. **Read before write.** `on_clock` assigns with non-blocking semantics in hardware; the tests run it sequentially, so a var read after its own assignment in the same call (a counter incremented, then compared) passes in hardware and fails in the test or the reverse. Two such places were found by the divider test and reordered. +6. **The control missed timing once**: with the default seed the ss build reached 96.57 MHz after routing (FAIL at 100); seed 2 gave 107.33 MHz. The tt top closed at the default seed. +7. The reader attached before the load saw the previous design's lines; the judge starts at the first `L=0000`, `N=000` line. + +## 7. Not claimed + +No speed claim (a step is about 1700 to 1960 clocks, 19 us at 100 MHz; the line of a step is 5.7 ms of UART; nothing here is compared with ngspice's wall time). No power. tt only: the other four corners are other tables and no other bitstream was built. One gate waveform (two levels, an ideal step), one load (500 fF with dt = 100 ps). The expected samples are the spec's own output stored in the RAM, so a PASS is agreement with the spec, not with ngspice; the spec's distance to ngspice is the one `mos_psp103.t27` measures. diff --git a/specs/analog/mos_psp103_data.t27 b/specs/analog/mos_psp103_data.t27 index b21b905698..0cdb1450ba 100644 --- a/specs/analog/mos_psp103_data.t27 +++ b/specs/analog/mos_psp103_data.t27 @@ -7812,6 +7812,64 @@ pub fn fold_q(c: u32) -> u64 { return s; } +; --- the board's ROM view (M3d, issue #11208): the tt tables and the tt run, behind one clocked port ------------------ +; specs/fpga/psp103_inv_ax7203.t27 runs the 500 fF inverter of specs/analog/mos_psp103.t27 on the AX7203 and reads these tables from block RAM. `t27c gen-verilog` +; carries a const array of its own module into Verilog as a memory with its initial contents, and carries nothing that came in by `use`: so the port is here, next +; to the arrays, and the board spec instantiates this module and imports the same arrays for its tests. `addr` selects a word of the four tt tables (node +; ix * 25 + iy), `idx` a sample of the run; each output is a register, the word of the address the port saw one clock earlier (a synchronous read). +; TT_RUN is not a number a deck printed. It is what the board's arithmetic gives: `run_fix_q` of mos_table.t27 on TT_N, TT_P, TT_QD_N, TT_QD_P with K_NEWTON = 3 +; Newton iterations, from the DC rest value (3 units), the gate at Vdd before step 0, 400 steps of dt = 100 ps on 500 fF. The board spec recomputes it word for +; word; here it is pinned by the fold that spec pins as EXP_S_TT_Q. +/// The fold of TT_RUN: the S of the last line the board prints. +pub const PIN_TT_RUN : u64 = 0x215DC5EAC4C48576; + +/// The 400 samples of the tt 500 fF inverter run, in units of 2^-24 V: the output after step 0 .. 399. +pub const TT_RUN : [400]u32 = [ + 689233, 1688406, 2683706, 3674563, 4660278, 5639992, 6612644, 7576936, 8531290, 9473823, 10401968, 11312829, 12203320, 13070185, + 13910217, 14720502, 15496651, 16236419, 16938689, 17601313, 18223616, 18806582, 19349120, 19853814, 20320443, 20751603, 21148826, 21513489, + 21848339, 22154968, 22434812, 22690262, 22923444, 23135902, 23328720, 23503747, 23662627, 23806850, 23937765, 24056604, 24164218, 24261378, + 24349114, 24428338, 24499877, 24564477, 24622809, 24675484, 24723049, 24765999, 24804783, 24839805, 24871429, 24899987, 24925773, 24949059, + 24970085, 24989072, 25006217, 25021699, 25035678, 25048302, 25059701, 25069994, 25079290, 25087683, 25095262, 25102106, 25108286, 25113867, + 25118906, 25123457, 25127566, 25131276, 25134627, 25137652, 25140384, 25142851, 25145079, 25147091, 25148907, 25150547, 25152029, 25153366, + 25154573, 25155664, 25156649, 25157538, 25158342, 25159067, 25159722, 25160312, 25160846, 25161328, 25161764, 25162157, 25162512, 25162832, + 25163121, 25163383, 25163619, 25163832, 25164025, 25164199, 25164355, 25164497, 25164625, 25164740, 25164845, 25164938, 25165023, 25165099, + 25165169, 25165232, 25165289, 25165341, 25165387, 25165428, 25165466, 25165500, 25165530, 25165557, 25165582, 25165604, 25165625, 25165644, + 25165661, 25165675, 25165689, 25165701, 25165712, 25165722, 25165730, 25165738, 25165746, 25165753, 25165759, 25165764, 25165769, 25165773, + 25165777, 25165781, 25165784, 25165787, 25165790, 25165793, 25165795, 25165797, 25165799, 25165801, 25165802, 25165803, 25165804, 25165805, + 25165806, 25165807, 25165808, 25165809, 25165810, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, + 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, + 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, 25165811, + 25165811, 25165811, 25165811, 25165811, 24233230, 22906610, 21589340, 20282582, 18987794, 17707063, 16443187, 15199640, 13980956, 12792926, + 11642639, 10538247, 9488330, 8500897, 7582250, 6736098, 5963229, 5262009, 4632525, 4068789, 3567785, 3122689, 2730467, 2384806, + 2080301, 1813893, 1580798, 1376849, 1198403, 1042306, 906550, 788476, 685780, 596460, 518774, 451205, 392438, 341324, + 296868, 258202, 224572, 195322, 169883, 147755, 128511, 111772, 97214, 84553, 73540, 63961, 55631, 48385, + 42083, 36602, 31834, 27688, 24081, 20945, 18217, 15845, 13781, 11985, 10424, 9066, 7886, 6858, + 5965, 5189, 4513, 3925, 3414, 2969, 2582, 2246, 1954, 1699, 1478, 1286, 1119, 973, + 846, 736, 640, 557, 484, 421, 367, 319, 277, 241, 209, 181, 157, 136, + 119, 103, 89, 78, 68, 59, 51, 44, 38, 33, 29, 25, 22, 19, + 16, 14, 12, 10, 9, 8, 7, 6, 5, 4, 3, 3, 3, 3, + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 3, 3, 3, 3, 3, 3, 3 +]; + +pub var tn : u32 = 0; +pub var tp : u32 = 0; +pub var qn : u32 = 0; +pub var qp : u32 = 0; +pub var ex : u32 = 0; + +fn on_clock(addr: u16, idx: u16) { + tn = TT_N[addr as usize]; + tp = TT_P[addr as usize]; + qn = TT_QD_N[addr as usize]; + qp = TT_QD_P[addr as usize]; + ex = TT_RUN[idx as usize]; +} + test the_five_corners_are_the_numbers_ngspice_printed { // A table is the NMOS table, the PMOS table and the inverter's transfer, in that order. var s : u64 = fold_arr(&TT_N, 625, 0); @@ -8238,6 +8296,48 @@ test the_log_domain_tables_are_the_numbers_ngspice_printed { assert fold_arr(&t, 4851, 0) != fold_arr(&TT_LG_N, 4851, 0); } +test the_rom_port_reads_the_tt_tables_and_the_tt_run { + // The port answers with the word of the address it was given, for every node of the four tables and every sample of the run. + var i : usize = 0; + var s : u64 = 0; + while (i < 625) { + on_clock(i as u16, 0); + assert_eq(tn, TT_N[i]); + assert_eq(tp, TT_P[i]); + assert_eq(qn, TT_QD_N[i]); + assert_eq(qp, TT_QD_P[i]); + i = i + 1; + } + i = 0; + while (i < 400) { + on_clock(0, i as u16); + assert_eq(ex, TT_RUN[i]); + s = fold(s, ex); + i = i + 1; + } + assert_eq(s, PIN_TT_RUN); + // The run starts 41 mV above the rail it rests on (the rising edge), ends back at the rest value, and never leaves the table's range. + assert_eq(TT_RUN[0], 689233); + assert_eq(TT_RUN[399], 3); + var top : u32 = 0; + i = 0; + while (i < 400) { + if (TT_RUN[i] > top) { top = TT_RUN[i]; } + i = i + 1; + } + assert_eq(top, 25165811); + // A changed sample is seen by the pin. + var t : [400]u32 = [0] ** 400; + i = 0; + while (i < 400) { + t[i] = TT_RUN[i]; + i = i + 1; + } + t[200] = t[200] + 1; + assert fold_arr(&t, 400, 0) != PIN_TT_RUN; + assert_eq(fold_arr(&TT_RUN, 400, 0), PIN_TT_RUN); +} + test the_log_domain_tables_of_ss_ff_fs_and_sf_are_the_numbers_ngspice_printed { // M3c-4 (#11211). Per corner (ff, ss, fs, sf; the tt corner's are above), the two log tables N then P (tag word first), the 1000 + 1000 currents at cell centres, and the references the corner // is judged by (the 1000 R2 points and the 576 midpoints, N then P): the pins see one changed number, and the accessors route to the named corner's arrays. diff --git a/specs/fpga/psp103_inv_ax7203.t27 b/specs/fpga/psp103_inv_ax7203.t27 new file mode 100644 index 0000000000..1f380d37f4 --- /dev/null +++ b/specs/fpga/psp103_inv_ax7203.t27 @@ -0,0 +1,1374 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/fpga/psp103_inv_ax7203.t27 -- the PSP103 CMOS inverter on the ALINX AX7203: 400 backward Euler steps, tt corner, tables in block RAM, one UART receipt line per step +; M3d of the analog emulation epic (#10486, issue #11208, success criterion SC-003). The inverter is the one of specs/analog/mos_psp103.t27 at 500 fF with +; dt = 100 ps (M3c, `q500_run`): the NMOS table and the PMOS table of sg13_lv_nmos / sg13_lv_pmos (PSP 103.6, 27 C, mos_tt) and the two drain-charge tables, +; read by the exact-integer bilinear reader of specs/analog/mos_table.t27 (`id_of`, `gds_cell`), solved at the output node by that file's backward Euler step +; (`board_step_q`: K_NEWTON = 3 Newton iterations, gate at Vdd before step 0, 0 V for steps 0 .. 199, Vdd for steps 200 .. 399, from the DC rest value of 3 units). +; This file is the board top of it. The four tables are NOT copied here: they come in by `use` from specs/analog/mos_psp103_data.t27 for the tests, and the board +; reads the same arrays from block RAM through that module's clocked port (see TABLES IN BLOCK RAM). What is written here is the machine, the receipt and the tests. +; Nothing of M3a/M3b/M3c, M0, M1b or the SAR top is edited; the pattern of specs/fpga/sar_adc_ax7203.t27 is followed: the restart request flags, the end of a line, +; the receipt as segments, the pins as attributes, the tests that run the machine beside the spec. +; - +; THE ARITHMETIC IS THE SPEC'S, ONE BIT A CLOCK. mos_table.t27 does a table read with 64-bit products (`blend`) and a Newton move with a 64-bit division +; (`newton_move`). The board has no DSP slice and no float, so the same integers are made in fabric by a shift-and-add multiplier and a restoring divider, a few +; hundred clocks a read, and tests compare every one with the spec's own function: the multiplier with `*`, the divider with `newton_move`, a whole read with +; `id_of` and `gds_cell` for all four tables, an iteration with `gq_pos`, `gq_neg` and `gq_deriv`, a step with `board_step_q`, the run with `run_fix_q`. +; A step is 14 table reads (2 for the previous step's charge, 3 x 4 for the iterations), each of which fetches the four nodes of its cell, then +; lo = t00 (CELL - fx) + t10 fx hi = t01 (CELL - fx) + t11 fx id = (lo (CELL - fy) + hi fy + 2^39) >> 40 (six products) +; gds = (dpos(t01, t00) (CELL - fx) + dpos(t11, t10) fx + 2^19) >> 20 (two products) +; exactly as `blend` and `blend1` write them. Then p, n, d (gq_pos, gq_neg, gq_deriv), the quotient q = (|p - n| 2^20 + d / 2) / d by 47 restoring steps (the design +; bounds are g < 2^26 and d < 2^23; the run's largest are 1344396 and 1216890, a test measures both), and y moves down by q (p >= n) or up by q, clamped to 0 and Vdd. +; 1700 to 1960 clocks a step (about 19 us at 100 MHz); the line of the previous step takes 5.7 ms, so the machine is idle 99.7 % of the time and nothing is pipelined. +; - +; TABLES IN BLOCK RAM. `t27c gen-verilog` writes a const array of the module it compiles as a memory with its initial contents, and writes nothing for a name that +; came in by `use` (the reference is left undeclared, #8769 for functions; the same for arrays). So the memory lives where the arrays live: specs/analog/mos_psp103_data.t27 +; has, next to TT_N, TT_P, TT_QD_N, TT_QD_P and the 400-word TT_RUN (the samples of the spec's own run), a clocked port `on_clock(addr, idx)` whose five outputs are +; registers: the word of each table at `addr` and the sample `idx`, as seen one clock earlier. This file's top instantiates that module (`AnalogMosPsp103Data`, an extern +; like the PLL) and the build reads both Verilog files. A read is therefore two clocks from the address register to the machine: the address is set, the RAM +; samples it, the machine takes the word. The machine runs the four nodes of a cell down that pipe one a clock. yosys maps a 625-word ROM to flip-flops and LUTs unless +; its memory carries `ram_style = "block"`, which `gen-verilog` does not write; the build script sets that attribute on the memories of the module (and says so in the table). +; - +; THE MACHINE, one phase a clock at 100 MHz (the PLL of M0 from the 200 MHz oscillator). A step: +; P_STEP y0 = y, the gate a of this step and a0 of the one before it, iteration 0 +; P_JOB job jn picks the table (jt) and the point (jvg, jvd): 0 qp (Vdd - a0, Vdd - y0) 1 qn (a0, y0) 2 tn (a, y) 3 qn (a, y) 4 tp (Vdd - a, Vdd - y) 5 qp (Vdd - a, Vdd - y) +; P_LIM P_CELL P_BASE the point held to the table, its cell (cx, cy), the position in the cell (fx, fy), the address of node (cx, cy) = 25 cx + cy +; P_RD1 .. P_RD5 the four nodes, t00 t10 t01 t11, down the two-clock pipe of the RAM +; P_LO1 .. P_G3 the eight products by P_MUL (the multiplier: add x when the weight's low bit is set, shift, until the weight is 0) +; P_ACC job 0 and 1 keep their id (c1, c2); jobs 2 .. 5 add id and gds to p = y + c1 + .., n = y0 + c2 + .. and d = CELL + .. (P_IT starts an iteration) +; P_PN P_DIV P_UPD q, then y; the third iteration ends the step +; then the verdict (y against the spec's sample), the order-sensitive fold of the samples, and the line. No clock chains more than one add, one compare or one table mux. +; - +; THE RESTART. As the SAR top: the button and LOCKED pass two registers; while they say no the request flags `fin` and `hard` are set every clock and the next clock +; puts the machine at step 0, line 0, y at the rest value. A finished line sets `fin` alone and the next clock starts the next step. After step 399 the board goes back to +; step 0 (y at the rest value, the fold cleared), so the 400 lines repeat for as long as the capture runs (L counts on). THE END OF A LINE is the SAR top's: `fin` is set +; GAP_BITS bit times after the LF's stop bit has ended. +; - +; THE RECEIPT. 115200 baud on N15 (divider 868 from 100 MHz), one line per step, M0's grammar: +; T27 PSP N=<3 hex> Y=<7 hex> E=<7 hex> S=<16 hex> L=<4 hex> PASS +; N the step (0 .. 18F), Y the output the board computed after it (units of 2^-24 V, 59.6 nV), E the spec's sample for it (TT_RUN, from the RAM), S the order-sensitive +; fold of the board's samples of this round (N = 0 .. this one; at N = 18F it is EXP_S_TT_Q, 0x215DC5EAC4C48576), L the lines since the button. PASS when Y equals E, else +; FAIL. 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. The same top with the ss tables in the tt top: TT_N, TT_P, TT_QD_N, TT_QD_P read as SS_N, SS_P, SS_QD_N, SS_QD_P, the rest value and the +; samples E unchanged. The spec's own run on those tables (`run_fix_q`, a test) differs from the tt run at 323 of the 400 steps, every step but 145 and 324 .. 399 (the +; ss output crosses the tt one once, and both are back at the rest value of 3 units from step 324), so a build with the ss tables prints FAIL on those 323 lines and PASS on +; the other 77; its fold at N = 18F is the ss run's, EXP_S_SS_Q = 0x987F22AC4132345B, and its Y on every line is the ss run's sample. +; - +; WHAT A PASS SAYS. This board, running RTL generated from this file and from the data module, solved the backward Euler step of the 500 fF PSP103 inverter at the +; tt corner from the foundry-model tables 400 times and produced, at every step, the sample the spec's fixed-point run produces (the tests compare the machine with +; the spec's functions at every level above, and the whole run word for word, including the clocks of the line at the real baud divider). By mos_psp103.t27 that run +; is within 0.020 % and 0.0041 % of ngspice's two 50 % delays at tt. +; WHAT IT DOES NOT SAY. Nothing about the circuit beyond that spec: a table model of PSP103, tt only here (the other four corners are other tables, not built), 27 C, one +; gate waveform (two levels, an ideal step), one load. The machine reads any gate voltage inside 0 .. Vdd but the run only ever uses the two rails. Nothing about speed +; (19 us a step is not a comparison with ngspice: ngspice's wall time is mostly its start-up and this board's is mostly the UART), power, noise or another node count. +; The expected samples are the spec's own output stored in the RAM: a PASS says the board agrees with the spec, not with ngspice. ASCII only, English only. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module FpgaPsp103Inv; + +use analog::linear; +use analog::mos_table::{VDD, CELL, CELL_BITS, HALF_Q, NODES, K_NEWTON, RUN_STEPS, gate_at, lim, cell_of, frac_of, dpos, mag_diff, id_of, gds_cell, blend, blend1, newton_move, gq_pos, gq_neg, gq_deriv, board_step_q, run_fix_q}; +use analog::mos_psp103::{dc_out, EXP_S_TT_Q, EXP_S_SS_Q}; +use analog::mos_psp103_data::{TT_N, TT_P, TT_QD_N, TT_QD_P, TT_RUN, SS_N, SS_P, SS_QD_N, SS_QD_P}; +use fpga::rc_filter_ax7203; +use fpga::sar_adc_ax7203::hex_at; + +pub const KIND : str = "board-cell"; +pub const ID : str = "fpga/psp103_inv_ax7203"; +pub const REFERENCE : str = "specs/analog/mos_psp103.t27 (M3c q500_run), specs/analog/mos_table.t27 (run_fix_q), specs/analog/mos_psp103_data.t27 (tt tables, TT_RUN)"; +pub const BOARD : str = "ALINX AX7203"; +pub const PART : str = "xc7a200tfbg484-2"; + +; --- the run, as the board holds it ---------------------------------------------------------------- +/// The steps of a round (mos_table's RUN_STEPS, as a u16), and the index of the last. +pub const STEPS_N : u16 = 400; +pub const STEP_LAST : u16 = 399; +/// The Newton iterations of a step (mos_table's K_NEWTON, as a u8) and the table reads of an iteration (jobs 2 .. 5). +pub const ITERS : u8 = 3; +pub const JOB_LAST : u8 = 5; +/// The DC rest value of the tt tables (dc_out(TT_N, TT_P, Vdd)): the output before step 0, 3 units. +pub const REST_TT : u32 = 3; +/// The idle bit times after the last stop bit of a line, before the next step starts. +pub const GAP_BITS : u8 = 2; +/// The characters of a line, and its segments. +pub const LINE_LEN : usize = 66; +pub const PSP_SEGS : u8 = 7; +/// The restoring divider: bits of the dividend (g 2^20 + d / 2 is under 2^47), and the bounds the run keeps g and d under. +pub const DIV_BITS : u8 = 47; +pub const G_BOUND : u32 = 67108864; +pub const D_BOUND : u32 = 8388608; +/// 2^19: the rounding of a gds read. +pub const HALF_G : u64 = 524288; +/// The negative control: the steps at which the ss tables give the tt sample (145, and 324 .. 399), so 323 FAIL lines. +pub const CTRL_FAILS : u32 = 323; +pub const CTRL_PASS_AT : u16 = 145; +pub const CTRL_SETTLED_FROM : u16 = 324; + +; --- the machine -------------------------------------------------------------------------------- +pub const P_STEP : u8 = 0; +pub const P_JOB : u8 = 1; +pub const P_LIM : u8 = 2; +pub const P_CELL : u8 = 3; +pub const P_BASE : u8 = 4; +pub const P_RD1 : u8 = 5; +pub const P_RD2 : u8 = 6; +pub const P_RD3 : u8 = 7; +pub const P_RD4 : u8 = 8; +pub const P_RD5 : u8 = 9; +pub const P_LO1 : u8 = 10; +pub const P_MUL : u8 = 11; +pub const P_LO2 : u8 = 12; +pub const P_LO3 : u8 = 13; +pub const P_HI2 : u8 = 14; +pub const P_HI3 : u8 = 15; +pub const P_W2 : u8 = 16; +pub const P_W3 : u8 = 17; +pub const P_G2 : u8 = 18; +pub const P_G3 : u8 = 19; +pub const P_ACC : u8 = 20; +pub const P_IT : u8 = 21; +pub const P_PN : u8 = 22; +pub const P_DIV : u8 = 23; +pub const P_UPD : u8 = 24; + +; --- facts -------------------------------------------------------------------------------------- + +/// The gate of the step before step n: Vdd before step 0 (the circuit rests with its gate high), else the gate of step n - 1. +pub fn prev_gate(n: u16) -> u32 { + if (n == 0) { return VDD; } + return gate_at(((n - 1) as u32)); +} + +/// The table job jn reads: 0 tn, 1 tp, 2 qn, 3 qp (the order of the RAM's outputs). +pub fn job_table(jn: u8) -> u8 { + if (jn == 0) { return 3; } + if (jn == 1) { return 2; } + if (jn == 2) { return 0; } + if (jn == 3) { return 2; } + if (jn == 4) { return 1; } + return 3; +} + +/// The gate coordinate of job jn: the previous gate for the two charge terms of the previous point, this gate for the NMOS side, its mirror for the PMOS side. +pub fn job_vg(jn: u8, ga: u32, ga0: u32) -> u32 { + if (jn == 0) { return VDD - ga0; } + if (jn == 1) { return ga0; } + if (jn == 2 or jn == 3) { return ga; } + return VDD - ga; +} + +/// The drain coordinate of job jn: the previous output y0 for jobs 0 and 1, the iterate y for the others, mirrored for the PMOS side. +pub fn job_vd(jn: u8, y: u32, y0: u32) -> u32 { + if (jn == 0) { return VDD - y0; } + if (jn == 1) { return y0; } + if (jn == 2 or jn == 3) { return y; } + return VDD - y; +} + +/// The word of the table jt among the four the RAM answers with. +pub fn pick_word(jt: u8, tn: u32, tp: u32, qn: u32, qp: u32) -> u32 { + if (jt == 0) { return tn; } + if (jt == 1) { return tp; } + if (jt == 2) { return qn; } + return qp; +} + +/// The address of node (cx, cy): 25 cx + cy, as shifts and adds (25 = 16 + 8 + 1). +pub fn node_base(cx: u32, cy: u32) -> u16 { + return ((cx << 4) + (cx << 3) + cx + cy) as u16; +} + +/// The remainder register of the divider after it takes the next bit of the dividend (bit 46 of dq). +pub fn div_r2(rem: u32, dq: u64) -> u32 { + return (rem << 1) | (((dq >> 46) & 1) as u32); +} + +/// PASS when the board's sample equals the spec's. +pub fn psp_verdict(y: u32, e: u32) -> u8 { + if (y == e) { return V_PASS; } + return V_FAIL; +} + +; --- the receipt: M0's line, with the fields of a step ---------------------------------------------------- +; hex_digit and pass_fail_char (board_receipt), frame, prefix_char (M0) are shared; the segments are these: +; 0 "T27 PSP" 1 " N=" + 3 hex 2 " Y=" + 7 hex 3 " E=" + 7 hex 4 " S=" + 16 hex 5 " L=" + 4 hex 6 " PASS\r\n" + +/// The key letter of field s (1..5): N Y E S L. +pub fn psp_key(s: u8) -> u8 { + if (s == 1) { return 78; } + if (s == 2) { return 89; } + if (s == 3) { return 69; } + if (s == 4) { return 83; } + return 76; +} + +/// The hex digits of field s (1..5). +pub fn psp_width(s: u8) -> u8 { + if (s == 1) { return 3; } + if (s == 2 or s == 3) { return 7; } + if (s == 4) { return 16; } + return 4; +} + +/// The last position of segment s: the prefix and the verdict have 7 characters, a field has " X=" and its digits. +pub fn psp_seg_last(s: u8) -> u8 { + if (s == 0) { return 6; } + if (s == PSP_SEGS - 1) { return 6; } + return 2 + psp_width(s); +} + +/// Character p of "T27 PSP": M0's "T27 " and the name. +pub fn psp_prefix(p: u8) -> u8 { + if (p < 4) { return prefix_char(p); } + if (p == 4) { return 80; } + if (p == 5) { return 83; } + return 80; +} + +/// The character at segment s, position p; `fsr` holds the field being written, its next nibble on top. +pub fn psp_char(s: u8, p: u8, fsr: u64, v: u8) -> u8 { + if (s == 0) { return psp_prefix(p); } + if (s == PSP_SEGS - 1) { return pass_fail_char(v, p); } + if (p == 0) { return 32; } + if (p == 1) { return psp_key(s); } + if (p == 2) { return 61; } + return hex_digit((fsr >> 60) as u8); +} + +/// Field s (1..5) placed at the top of the 64-bit register, so that its first digit is nibble 15: 4 * (16 - width) bits up. +pub fn psp_top(s: u8, n: u16, y: u32, e: u32, sum: u64, l: u32) -> u64 { + if (s == 1) { return (n as u64) << 52; } + if (s == 2) { return (y as u64) << 36; } + if (s == 3) { return (e as u64) << 36; } + if (s == 4) { 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 tables' RAM: the clocked port of specs/analog/mos_psp103_data.t27, generated by `t27c gen-verilog`. Its outputs are the word of TT_N, TT_P, TT_QD_N, TT_QD_P at +/// `addr` and the sample TT_RUN[idx], each a register. rst_n and en are the module's own inputs, tied high here. +pub struct RomOut { tn: u32, tp: u32, qn: u32, qp: u32, ex: u32 } +pub fn AnalogMosPsp103Data(clk_: bool, rst_n_: bool, en_: bool, addr: u16, idx: u16) -> RomOut {} + +; --- 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 SAR top): 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 stp : u16 = 0; +var r_y : u32 = 3; +var r_y0 : u32 = 3; +var r_ga : u32 = 0; +var r_ga0 : u32 = 0; +var r_it : u8 = 0; +var r_jn : u8 = 0; +var r_jt : u8 = 0; +var r_vg : u32 = 0; +var r_vd : u32 = 0; +var r_gv : u32 = 0; +var r_dv : u32 = 0; +var r_cx : u32 = 0; +var r_cy : u32 = 0; +var r_fx : u32 = 0; +var r_fy : u32 = 0; +var r_ad : u16 = 0; +var r_t0 : u32 = 0; +var r_t1 : u32 = 0; +var r_t2 : u32 = 0; +var r_t3 : u32 = 0; +var r_mx : u64 = 0; +var r_mw : u32 = 0; +var r_mret : u8 = 0; +var r_acc : u64 = 0; +var r_lo : u64 = 0; +var r_hi : u64 = 0; +var r_id : u32 = 0; +var r_gd : u32 = 0; +var r_c1 : u32 = 0; +var r_c2 : u32 = 0; +var r_sp : u32 = 0; +var r_sn : u32 = 0; +var r_sd : u32 = 0; +var r_up : bool = false; +var r_dq : u64 = 0; +var r_dvs : u32 = 0; +var r_rem : u32 = 0; +var r_qt : u32 = 0; +var r_dc : u8 = 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 gap : u8 = 0; +var hard : bool = false; +var fin : bool = false; +var hb : u32 = 0; +var go0 : bool = false; +var go1 : bool = false; + +; --- the tables' RAM: an instance of the data module, the address and the sample index are registers -------- +const rom : RomOut = AnalogMosPsp103Data(clk, true, true, r_ad, stp); + +; --- 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, rom_tn: u32, rom_tp: u32, rom_qn: u32, rom_qp: u32, rom_ex: u32) { + 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) { + stp = 0; + r_y = REST_TT; + lines = 0; + cs = 0; + hard = false; + } else { + if (stp == STEP_LAST) { + stp = 0; + r_y = REST_TT; + cs = 0; + } else { + stp = stp + 1; + } + } + st = ST_RUN; + ph = P_STEP; + verdict = V_FAIL; + tx_cnt = 0; + tx_sh = 1023; + tx_left = 0; + seg = 0; + upos = 0; + fsr = 0; + last = false; + gap = 0; + fin = false; + } else if (st == ST_RUN) { + if (ph == P_STEP) { + r_y0 = r_y; + r_ga = gate_at((stp as u32)); + r_ga0 = prev_gate(stp); + r_it = 0; + r_jn = 0; + ph = P_JOB; + } else if (ph == P_JOB) { + r_vg = job_vg(r_jn, r_ga, r_ga0); + r_vd = job_vd(r_jn, r_y, r_y0); + r_jt = job_table(r_jn); + ph = P_LIM; + } else if (ph == P_LIM) { + r_gv = lim(r_vg); + r_dv = lim(r_vd); + ph = P_CELL; + } else if (ph == P_CELL) { + r_cx = cell_of(r_gv); + r_cy = cell_of(r_dv); + r_fx = frac_of(r_gv); + r_fy = frac_of(r_dv); + ph = P_BASE; + } else if (ph == P_BASE) { + r_ad = node_base(r_cx, r_cy); + ph = P_RD1; + } else if (ph == P_RD1) { + r_ad = r_ad + 25; + ph = P_RD2; + } else if (ph == P_RD2) { + r_t0 = pick_word(r_jt, rom_tn, rom_tp, rom_qn, rom_qp); + r_ad = r_ad - 24; + ph = P_RD3; + } else if (ph == P_RD3) { + r_t1 = pick_word(r_jt, rom_tn, rom_tp, rom_qn, rom_qp); + r_ad = r_ad + 25; + ph = P_RD4; + } else if (ph == P_RD4) { + r_t2 = pick_word(r_jt, rom_tn, rom_tp, rom_qn, rom_qp); + ph = P_RD5; + } else if (ph == P_RD5) { + r_t3 = pick_word(r_jt, rom_tn, rom_tp, rom_qn, rom_qp); + ph = P_LO1; + } else if (ph == P_LO1) { + r_acc = 0; + r_mx = r_t0 as u64; + r_mw = CELL - r_fx; + r_mret = P_LO2; + ph = P_MUL; + } else if (ph == P_MUL) { + if (r_mw == 0) { + ph = r_mret; + } else { + if ((r_mw & 1) == 1) { r_acc = r_acc + r_mx; } + r_mx = r_mx << 1; + r_mw = r_mw >> 1; + } + } else if (ph == P_LO2) { + r_mx = r_t1 as u64; + r_mw = r_fx; + r_mret = P_LO3; + ph = P_MUL; + } else if (ph == P_LO3) { + r_lo = r_acc; + r_acc = 0; + r_mx = r_t2 as u64; + r_mw = CELL - r_fx; + r_mret = P_HI2; + ph = P_MUL; + } else if (ph == P_HI2) { + r_mx = r_t3 as u64; + r_mw = r_fx; + r_mret = P_HI3; + ph = P_MUL; + } else if (ph == P_HI3) { + r_hi = r_acc; + r_acc = HALF_Q; + r_mx = r_lo; + r_mw = CELL - r_fy; + r_mret = P_W2; + ph = P_MUL; + } else if (ph == P_W2) { + r_mx = r_hi; + r_mw = r_fy; + r_mret = P_W3; + ph = P_MUL; + } else if (ph == P_W3) { + r_id = (r_acc >> 40) as u32; + r_acc = HALF_G; + r_mx = dpos((r_t2 as u64), (r_t0 as u64)); + r_mw = CELL - r_fx; + r_mret = P_G2; + ph = P_MUL; + } else if (ph == P_G2) { + r_mx = dpos((r_t3 as u64), (r_t1 as u64)); + r_mw = r_fx; + r_mret = P_G3; + ph = P_MUL; + } else if (ph == P_G3) { + r_gd = (r_acc >> 20) as u32; + ph = P_ACC; + } else if (ph == P_ACC) { + if (r_jn == 0) { + r_c1 = r_id; + r_jn = 1; + ph = P_JOB; + } else if (r_jn == 1) { + r_c2 = r_id; + r_jn = 2; + ph = P_IT; + } else if (r_jn == 2 or r_jn == 3) { + r_sp = r_sp + r_id; + r_sd = r_sd + r_gd; + r_jn = r_jn + 1; + ph = P_JOB; + } else if (r_jn == 4) { + r_sn = r_sn + r_id; + r_sd = r_sd + r_gd; + r_jn = 5; + ph = P_JOB; + } else { + r_sn = r_sn + r_id; + r_sd = r_sd + r_gd; + ph = P_PN; + } + } else if (ph == P_IT) { + r_sp = r_y + r_c1; + r_sn = r_y0 + r_c2; + r_sd = CELL; + ph = P_JOB; + } else if (ph == P_PN) { + r_up = r_sp >= r_sn; + r_dq = (((mag_diff(r_sp, r_sn)) as u64) << 20) + ((r_sd as u64) >> 1); + r_dvs = r_sd; + r_rem = 0; + r_qt = 0; + r_dc = 0; + ph = P_DIV; + } else if (ph == P_DIV) { + if (div_r2(r_rem, r_dq) >= r_dvs) { + r_rem = div_r2(r_rem, r_dq) - r_dvs; + r_qt = (r_qt << 1) | 1; + } else { + r_rem = div_r2(r_rem, r_dq); + r_qt = r_qt << 1; + } + r_dq = r_dq << 1; + if (r_dc == DIV_BITS - 1) { ph = P_UPD; } + r_dc = r_dc + 1; + } else { + if (r_up) { + if (r_qt >= r_y) { r_y = 0; } else { r_y = r_y - r_qt; } + } else { + if (r_qt >= VDD - r_y) { r_y = VDD; } else { r_y = r_y + r_qt; } + } + if (r_it == ITERS - 1) { + st = ST_JUDGE; + } else { + r_jn = 2; + ph = P_IT; + } + r_it = r_it + 1; + } + } else if (st == ST_JUDGE) { + verdict = psp_verdict(r_y, rom_ex); + cs = fold(cs, r_y); + st = ST_REPORT; + } else { + if (tx_cnt != 0) { + tx_cnt = tx_cnt - 1; + } else { + tx_cnt = baud_div - 1; + if (tx_left != 0) { + 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(psp_char(seg, upos, fsr, verdict)); + tx_left = 9; + if (upos == psp_seg_last(seg)) { + fsr = psp_top(seg + 1, stp, r_y, rom_ex, cs, lines); + upos = 0; + if (seg == PSP_SEGS - 1) { + seg = 0; + lines = lines + 1; + last = true; + } else { + seg = seg + 1; + } + } else { + if (seg != 0 and seg != PSP_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 RAM as the tests model it: its five output registers, and which corner's tables it holds (false: tt, true: ss, the control). +var m_tn : u32 = 0; +var m_tp : u32 = 0; +var m_qn : u32 = 0; +var m_qp : u32 = 0; +var m_ex : u32 = 0; +var m_ss : bool = false; + +fn rom_n(a: u16) -> u32 { + if (m_ss) { return SS_N[a as usize]; } + return TT_N[a as usize]; +} + +fn rom_p(a: u16) -> u32 { + if (m_ss) { return SS_P[a as usize]; } + return TT_P[a as usize]; +} + +fn rom_qn(a: u16) -> u32 { + if (m_ss) { return SS_QD_N[a as usize]; } + return TT_QD_N[a as usize]; +} + +fn rom_qp(a: u16) -> u32 { + if (m_ss) { return SS_QD_P[a as usize]; } + return TT_QD_P[a as usize]; +} + +/// The table jt of the tt corner as a slice, for the spec's own reader. +fn tab_of(t: u8) -> []const u32 { + if (t == 0) { return &TT_N; } + if (t == 1) { return &TT_P; } + if (t == 2) { return &TT_QD_N; } + return &TT_QD_P; +} + +/// One clock of the board with the RAM beside it: the machine sees the words the RAM registered at the last edge, and the RAM registers the words of the +/// address and the sample index the machine held before this edge (a synchronous read). +fn tick() { + const a : u16 = r_ad; + const s : u16 = stp; + on_clock(true, true, m_tn, m_tp, m_qn, m_qp, m_ex); + m_tn = rom_n(a); + m_tp = rom_p(a); + m_qn = rom_qn(a); + m_qp = rom_qp(a); + m_ex = TT_RUN[s as usize]; +} + +/// The machine as the button leaves it, then step k selected with the output of the step before it (the start of step k). +fn boot_at(k: u16) { + go0 = true; + go1 = false; + m_tn = 0; + m_tp = 0; + m_qn = 0; + m_qp = 0; + m_ex = 0; + tick(); + tick(); + stp = k; + if (k == 0) { + r_y = REST_TT; + } else { + r_y = TT_RUN[(k - 1) as usize]; + } +} + +/// Runs the machine from where it stands to the end of the step (ST_JUDGE); the clocks it took. +fn run_to_judge() -> u32 { + var n : u32 = 0; + while (st == ST_RUN and n < 100000) { + tick(); + n = n + 1; + } + return n; +} + +/// Runs until the machine is at phase p, or n clocks have passed; the clocks it took. +fn run_to_phase(p: u8, limit: u32) -> u32 { + var n : u32 = 0; + while (ph != p and n < limit) { + tick(); + n = n + 1; + } + return n; +} + +/// The next word of a linear congruential sequence (the tests' own pseudo-random points). +fn lcg(x: u32) -> u32 { + return x *% 1664525 +% 1013904223; +} + +; --- the tests ---------------------------------------------------------------------------------- + +test the_constants_are_the_specs { + assert_eq(STEPS_N as u32, RUN_STEPS); + assert_eq((STEP_LAST as u32) + 1, RUN_STEPS); + assert_eq(ITERS as u32, K_NEWTON); + assert_eq(dc_out(&TT_N, &TT_P, VDD), REST_TT); + assert_eq(HALF_G, (CELL >> 1) as u64); + assert_eq(HALF_Q, 549755813888); + assert_eq(CELL, 1 << 20); + assert_eq(NODES, 25); + assert_eq((DIV_BITS as u32), 47); + assert_eq(CTRL_FAILS + 77, RUN_STEPS); + // the run the RAM holds is the spec's run, word for word + var out : [400]u32 = [0] ** 400; + var res : [400]u32 = [0] ** 400; + const s : u64 = run_fix_q(&TT_N, &TT_P, &TT_QD_N, &TT_QD_P, K_NEWTON, REST_TT, VDD, false, &out, &res); + assert_eq(s, EXP_S_TT_Q); + var i : usize = 0; + var f : u64 = 0; + var worst : u32 = 0; + while (i < 400) { + assert_eq(TT_RUN[i], out[i]); + f = fold(f, TT_RUN[i]); + if (res[i] > worst) { worst = res[i]; } + i = i + 1; + } + assert_eq(f, EXP_S_TT_Q); + // the last Newton residual is at most 2 units at every step (mos_psp103.t27): the board's three iterations are enough + assert(worst <= 2); + assert(worst >= 1); + // a changed sample is seen + assert(TT_RUN[100] + 1 != out[100]); +} + +test the_gate_the_jobs_and_the_addresses_are_the_specs { + assert_eq(prev_gate(0), VDD); + assert_eq(prev_gate(1), 0); + assert_eq(prev_gate(200), 0); + assert_eq(prev_gate(201), VDD); + assert_eq(prev_gate(399), VDD); + var n : u16 = 0; + while (n < STEPS_N) { + if (n > 0) { assert_eq(prev_gate(n), gate_at(((n - 1) as u32))); } + n = n + 1; + } + // the six jobs: which table, at which point + assert_eq(job_table(0), 3); + assert_eq(job_table(1), 2); + assert_eq(job_table(2), 0); + assert_eq(job_table(3), 2); + assert_eq(job_table(4), 1); + assert_eq(job_table(5), 3); + assert_eq(job_vg(0, 100, 7), VDD - 7); + assert_eq(job_vd(0, 100, 7), VDD - 7); + assert_eq(job_vg(1, 100, 7), 7); + assert_eq(job_vd(1, 100, 7), 7); + assert_eq(job_vg(2, 100, 7), 100); + assert_eq(job_vd(2, 100, 7), 100); + assert_eq(job_vg(3, 100, 7), 100); + assert_eq(job_vd(3, 100, 7), 100); + assert_eq(job_vg(4, 100, 7), VDD - 100); + assert_eq(job_vd(4, 100, 7), VDD - 100); + assert_eq(job_vg(5, 100, 7), VDD - 100); + assert_eq(job_vd(5, 100, 7), VDD - 100); + assert_eq(JOB_LAST, 5); + assert_eq(pick_word(0, 10, 20, 30, 40), 10); + assert_eq(pick_word(1, 10, 20, 30, 40), 20); + assert_eq(pick_word(2, 10, 20, 30, 40), 30); + assert_eq(pick_word(3, 10, 20, 30, 40), 40); + // 25 cx + cy by shifts, for every cell of the grid and the node one past it + var cxx : u32 = 0; + var cyy : u32 = 0; + while (cxx < 24) { + cyy = 0; + while (cyy < 24) { + assert_eq(node_base(cxx, cyy) as u32, cxx * NODES + cyy); + assert(((node_base(cxx, cyy) as u32) + NODES + 1) < 625); + cyy = cyy + 1; + } + cxx = cxx + 1; + } + assert_eq(psp_verdict(5, 5), V_PASS); + assert_eq(psp_verdict(5, 6), V_FAIL); +} + +test the_shift_and_add_multiplier_is_the_product { + var xs : [9]u64 = [0, 1, 3, 4095, 1048575, 1048576, 2097151, 8388607, 8796093022207]; + var ws : [9]u32 = [0, 1, 2, 3, 12345, 524287, 1048575, 1048576, 1000003]; + var i : usize = 0; + var j : usize = 0; + var n : u32 = 0; + var longest : u32 = 0; + while (i < 9) { + j = 0; + while (j < 9) { + boot_at(0); + r_acc = 77; + r_mx = xs[i]; + r_mw = ws[j]; + r_mret = P_LO3; + ph = P_MUL; + n = run_to_phase(P_LO3, 100); + assert_eq(r_acc, 77 + xs[i] * (ws[j] as u64)); + if (n > longest) { longest = n; } + j = j + 1; + } + i = i + 1; + } + // a product of a weight under 2^21 takes at most 22 clocks, so a read stays a few hundred + assert_eq(longest, 22); +} + +test the_restoring_divider_is_the_specs_newton_move { + var gs : [10]u32 = [0, 1, 2, 12345, 1048576, 33554432, 25165823, 67108863, 500000, 3]; + var ds : [8]u32 = [1048576, 1048577, 1500000, 2097159, 4194304, 8388607, 1310720, 3000001]; + var i : usize = 0; + var j : usize = 0; + var longest : u32 = 0; + var n : u32 = 0; + while (i < 10) { + j = 0; + while (j < 8) { + boot_at(0); + r_sp = gs[i] + 1000; + r_sn = 1000; + r_sd = ds[j]; + ph = P_PN; + n = run_to_phase(P_UPD, 100); + assert_eq(r_qt, newton_move(gs[i], ds[j] as u64)); + assert(r_up); + // and the other direction + r_sp = 1000; + r_sn = gs[i] + 1000; + ph = P_PN; + n = n + run_to_phase(P_UPD, 100); + assert_eq(r_qt, newton_move(gs[i], ds[j] as u64)); + if (gs[i] > 0) { assert(!r_up); } + if (n > longest) { longest = n; } + j = j + 1; + } + i = i + 1; + } + // P_PN and 47 clocks of P_DIV, twice here (once a direction); the dividend fits 47 bits + assert_eq(longest, 2 * (1 + (DIV_BITS as u32))); + assert(((67108863 as u64) << 20) + 4194303 < (1 << 47)); +} + +test a_table_read_is_the_specs_id_and_gds_for_all_four_tables { + var vgs : [12]u32 = [0, 1, 524288, 1048575, 1048576, 1048577, 5255225, 14631487, 24117248, 25165823, 25165824, 25200000]; + var vds : [14]u32 = [0, 1, 524288, 1048575, 1048576, 3, 7340033, 13107200, 20000000, 24817248, 25165823, 25165824, 25165825, 30000000]; + var t : u8 = 0; + var i : usize = 0; + var j : usize = 0; + var n : u32 = 0; + var longest : u32 = 0; + var reads : u32 = 0; + var x : u32 = 12345; + while (t < 4) { + i = 0; + while (i < 12) { + j = 0; + while (j < 14) { + boot_at(0); + r_jt = t; + r_vg = vgs[i]; + r_vd = vds[j]; + ph = P_LIM; + n = run_to_phase(P_ACC, 2000); + assert_eq(r_id, id_of(tab_of(t), vgs[i], vds[j])); + assert_eq(r_gd, gds_cell(tab_of(t), vgs[i], vds[j])); + if (n > longest) { longest = n; } + reads = reads + 1; + j = j + 1; + } + i = i + 1; + } + // 150 points of a pseudo-random sequence over the whole range and a little beyond it + i = 0; + while (i < 150) { + x = lcg(x); + const vg : u32 = (x >> 3) % 25200000; + x = lcg(x); + const vd : u32 = (x >> 3) % 25200000; + boot_at(0); + r_jt = t; + r_vg = vg; + r_vd = vd; + ph = P_LIM; + n = run_to_phase(P_ACC, 2000); + assert_eq(r_id, id_of(tab_of(t), vg, vd)); + assert_eq(r_gd, gds_cell(tab_of(t), vg, vd)); + // the four nodes the machine fetched, through the spec's own blend and blend1 + assert_eq(r_id, blend((r_t0 as u64), (r_t1 as u64), (r_t2 as u64), (r_t3 as u64), r_fx, r_fy)); + assert_eq(r_gd, blend1(dpos((r_t2 as u64), (r_t0 as u64)), dpos((r_t3 as u64), (r_t1 as u64)), r_fx)); + if (n > longest) { longest = n; } + reads = reads + 1; + i = i + 1; + } + t = t + 1; + } + assert_eq(reads, 4 * (12 * 14 + 150)); + // a read is a few hundred clocks, whatever the point + assert(longest < 300); + assert(longest > 100); +} + +test an_iteration_has_the_specs_p_n_d_and_move_at_every_step_checked { + var ks : [8]u16 = [0, 1, 2, 57, 199, 200, 201, 399]; + var k : usize = 0; + var maxg : u32 = 0; + var maxd : u32 = 0; + var iters : u32 = 0; + while (k < 8) { + const step : u16 = ks[k]; + boot_at(step); + const a : u32 = gate_at((step as u32)); + const a0 : u32 = prev_gate(step); + var y0v : u32 = REST_TT; + if (step > 0) { y0v = TT_RUN[(step - 1) as usize]; } + var y : u32 = y0v; + var it : u32 = 0; + while (it < 3) { + run_to_phase(P_PN, 20000); + assert_eq(r_y, y); + assert_eq(r_sp, gq_pos(&TT_N, &TT_QD_N, &TT_QD_P, y, y0v, a, a0)); + assert_eq(r_sn, gq_neg(&TT_P, &TT_QD_N, &TT_QD_P, y, y0v, a, a0)); + assert_eq((r_sd as u64), gq_deriv(&TT_N, &TT_P, &TT_QD_N, &TT_QD_P, y, a)); + if (mag_diff(r_sp, r_sn) > maxg) { maxg = mag_diff(r_sp, r_sn); } + if (r_sd > maxd) { maxd = r_sd; } + run_to_phase(P_UPD, 200); + tick(); + y = r_y; + iters = iters + 1; + it = it + 1; + } + assert_eq(st, ST_JUDGE); + assert_eq(y, TT_RUN[step as usize]); + k = k + 1; + } + assert_eq(iters, 24); + // the divider's dividend fits 47 bits and its remainder 24: g < 2^26 and d < 2^23 on these steps (the whole run is measured below) + assert(maxg < G_BOUND); + assert(maxd < D_BOUND); + assert(maxg > 1000); +} + +test a_step_is_the_specs_board_step { + var ks : [10]u16 = [0, 1, 2, 3, 57, 199, 200, 201, 300, 399]; + var k : usize = 0; + var longest : u32 = 0; + var n : u32 = 0; + while (k < 10) { + const step : u16 = ks[k]; + boot_at(step); + n = run_to_judge(); + assert_eq(st, ST_JUDGE); + var y0v : u32 = REST_TT; + if (step > 0) { y0v = TT_RUN[(step - 1) as usize]; } + assert_eq(r_y, board_step_q(&TT_N, &TT_P, &TT_QD_N, &TT_QD_P, y0v, gate_at((step as u32)), prev_gate(step))); + assert_eq(r_y, TT_RUN[step as usize]); + if (n > longest) { longest = n; } + k = k + 1; + } + // 1700 to 1960 clocks a step (about 19 us), the same for every step to within the multipliers' early exits + assert(longest < 2200); + assert(longest > 1800); +} + +test the_ss_prediction_of_the_negative_control_is_the_specs { + var out : [400]u32 = [0] ** 400; + var res : [400]u32 = [0] ** 400; + const s : u64 = run_fix_q(&SS_N, &SS_P, &SS_QD_N, &SS_QD_P, K_NEWTON, REST_TT, VDD, false, &out, &res); + assert_eq(s, EXP_S_SS_Q); + var i : usize = 0; + var fails : u32 = 0; + var ok : u32 = 0; + while (i < 400) { + const same : bool = out[i] == TT_RUN[i]; + if (same) { ok = ok + 1; } else { fails = fails + 1; } + // PASS exactly at step 145 and from step 324 + const want : bool = i == (CTRL_PASS_AT as usize) or i >= (CTRL_SETTLED_FROM as usize); + assert_eq(same, want); + i = i + 1; + } + assert_eq(fails, CTRL_FAILS); + assert_eq(ok, 400 - CTRL_FAILS); + // the ss run is not a shifted tt run: it differs at the first step and is back at the rest value at the end + assert(out[0] != TT_RUN[0]); + assert_eq(out[399], REST_TT); + assert_eq(out[324], REST_TT); + assert(out[323] != REST_TT); +} + +test the_machine_with_ss_tables_fails_exactly_the_predicted_lines { + var out : [400]u32 = [0] ** 400; + var res : [400]u32 = [0] ** 400; + const s : u64 = run_fix_q(&SS_N, &SS_P, &SS_QD_N, &SS_QD_P, K_NEWTON, REST_TT, VDD, false, &out, &res); + m_ss = true; + boot_at(0); + var k : usize = 0; + var fails : u32 = 0; + var passes : u32 = 0; + while (k < 400) { + run_to_judge(); + assert_eq(st, ST_JUDGE); + assert_eq(stp as usize, k); + assert_eq(r_y, out[k]); + tick(); + assert_eq(st, ST_REPORT); + if (out[k] == TT_RUN[k]) { + assert_eq(verdict, V_PASS); + passes = passes + 1; + } else { + assert_eq(verdict, V_FAIL); + fails = fails + 1; + } + if (k == 399) { assert_eq(cs, EXP_S_SS_Q); } + // the line is not sent here: the request for the next step is raised and taken + fin = true; + tick(); + k = k + 1; + } + m_ss = false; + assert_eq(fails, CTRL_FAILS); + assert_eq(passes, 400 - CTRL_FAILS); + assert_eq(s, EXP_S_SS_Q); +} + +test the_run_starts_after_lock_and_button_and_restarts_on_the_button { + go0 = false; + go1 = false; + st = ST_REPORT; + lines = 5; + stp = 17; + cs = 99; + r_y = 12345; + on_clock(false, true, 0, 0, 0, 0, 0); + on_clock(true, false, 0, 0, 0, 0, 0); + on_clock(false, false, 0, 0, 0, 0, 0); + assert_eq(st, ST_RUN); + assert_eq(ph, P_STEP); + assert_eq(lines, 0); + assert_eq(stp, 0); + assert_eq(cs, 0); + assert_eq(r_y, REST_TT); + tick(); + assert_eq(ph, P_STEP); + tick(); + assert_eq(ph, P_STEP); + tick(); + assert_eq(ph, P_STEP); + tick(); + assert_eq(ph, P_JOB); + assert_eq(r_y0, REST_TT); + assert_eq(r_ga, 0); + assert_eq(r_ga0, VDD); + var k : u32 = 0; + while (st == ST_RUN) { + tick(); + k = k + 1; + } + tick(); + assert_eq(st, ST_REPORT); + assert_eq(verdict, V_PASS); + assert_eq(cs, TT_RUN[0] as u64); + assert_eq(r_y, TT_RUN[0]); + // the button again: back to step 0, line 0, the fold cleared, y at the rest value + stp = 9; + lines = 3; + r_y = 777; + on_clock(true, false, 0, 0, 0, 0, 0); + on_clock(true, true, 0, 0, 0, 0, 0); + on_clock(true, true, 0, 0, 0, 0, 0); + assert_eq(st, ST_REPORT); + on_clock(true, true, 0, 0, 0, 0, 0); + assert_eq(st, ST_RUN); + assert_eq(stp, 0); + assert_eq(lines, 0); + assert_eq(cs, 0); + assert_eq(r_y, REST_TT); + 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; + tick(); + assert(!uart_tx); + assert(!led_0); + assert(led_1); + assert(!led_2); + assert(led_3); + verdict = V_FAIL; + tx_sh = 1023; + tick(); + assert(uart_tx); + assert(!led_1); + assert(led_2); + st = ST_JUDGE; + tick(); + assert(uart_tx); + assert(led_0); + assert(led_1); +} + +test the_receipt_segments_add_up_to_a_66_character_line { + var n : usize = 0; + var s : u8 = 0; + while (s < PSP_SEGS) { + n = n + (psp_seg_last(s) as usize) + 1; + s = s + 1; + } + assert_eq(n, LINE_LEN); + // the fields: widths, and the keys N Y E S L + assert_eq(psp_width(1), 3); + assert_eq(psp_width(2), 7); + assert_eq(psp_width(3), 7); + assert_eq(psp_width(4), 16); + assert_eq(psp_width(5), 4); + assert_eq(psp_key(1), 78); + assert_eq(psp_key(2), 89); + assert_eq(psp_key(3), 69); + assert_eq(psp_key(4), 83); + assert_eq(psp_key(5), 76); + // every field sits at the top of the register: its first digit is nibble 15 + assert_eq(psp_top(1, 399, 0, 0, 0, 0) >> 52, 399); + assert_eq(psp_top(2, 0, 25165824, 0, 0, 0) >> 36, 25165824); + assert_eq(psp_top(3, 0, 0, 25165811, 0, 0) >> 36, 25165811); + assert_eq(psp_top(4, 0, 0, 0, 0x0123456789ABCDEF, 0), 0x0123456789ABCDEF); + assert_eq(psp_top(5, 0, 0, 0, 0, 0xABCD) >> 48, 0xABCD); + // the longest values fit their fields: 25165824 = 0x1800000 is 7 digits, 399 = 0x18F is 3 + assert(25165824 < (1 << 28)); + assert(399 < (1 << 12)); +} + +test the_board_prints_400_lines_equal_to_the_specs_run_then_goes_round_again { + var out : [400]u32 = [0] ** 400; + var res : [400]u32 = [0] ** 400; + const s : u64 = run_fix_q(&TT_N, &TT_P, &TT_QD_N, &TT_QD_P, K_NEWTON, REST_TT, VDD, false, &out, &res); + assert_eq(s, EXP_S_TT_Q); + m_ss = false; + boot_at(0); + baud_div = 1; + var buf : [72]u8 = [0] ** 72; + 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; + var maxg : u32 = 0; + var maxd : u32 = 0; + var seen_pn : u32 = 0; + while (line < 402 and ticks < 20000000) { + tick(); + ticks = ticks + 1; + if (ph == P_PN and st == ST_RUN) { + if (mag_diff(r_sp, r_sn) > maxg) { maxg = mag_diff(r_sp, r_sn); } + if (r_sd > maxd) { maxd = r_sd; } + seen_pn = seen_pn + 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 % 400) as usize; + if (kk == 0) { want = 0; } + want = fold(want, out[kk]); + // "T27 PSP" + assert_eq(buf[0], 84); + assert_eq(buf[1], 50); + assert_eq(buf[2], 55); + assert_eq(buf[3], 32); + assert_eq(buf[4], 80); + assert_eq(buf[5], 83); + assert_eq(buf[6], 80); + // " N=", " Y=", " E=", " S=", " L=": a space, the key, an equals sign, then the digits + assert_eq(buf[7], 32); + assert_eq(buf[8], 78); + assert_eq(buf[9], 61); + assert_eq(buf[13], 32); + assert_eq(buf[14], 89); + assert_eq(buf[15], 61); + assert_eq(buf[23], 32); + assert_eq(buf[24], 69); + assert_eq(buf[25], 61); + assert_eq(buf[33], 32); + assert_eq(buf[34], 83); + assert_eq(buf[35], 61); + assert_eq(buf[52], 32); + assert_eq(buf[53], 76); + assert_eq(buf[54], 61); + assert_eq(hex_at(&buf, 10, 3), kk as u64); + assert_eq(hex_at(&buf, 16, 7), out[kk] as u64); + assert_eq(hex_at(&buf, 26, 7), out[kk] as u64); + assert_eq(hex_at(&buf, 26, 7), TT_RUN[kk] as u64); + assert_eq(hex_at(&buf, 36, 16), want); + assert_eq(hex_at(&buf, 55, 4), line as u64); + // " PASS\r\n" + assert_eq(buf[59], 32); + assert_eq(buf[60], 80); + assert_eq(buf[61], 65); + assert_eq(buf[62], 83); + assert_eq(buf[63], 83); + assert_eq(buf[64], 13); + assert_eq(buf[65], 10); + passes = passes + 1; + if (kk == 399) { assert_eq(want, EXP_S_TT_Q); } + got = 0; + line = line + 1; + } + } + } + assert_eq(line, 402); + assert_eq(lines, 402); + assert_eq(passes, 402); + // the divider's range over the whole run: g under 2^26, d under 2^23, and 3 iterations of 402 steps were seen + assert_eq(seen_pn, 3 * 402); + assert(maxg < G_BOUND); + assert(maxd < D_BOUND); + assert_eq(maxg, 1344396); + assert_eq(maxd, 1216890); + baud_div = BAUD_DIV; +} + +test a_different_sample_prints_fail_and_the_leds_follow { + // the ss tables in the tt top: the first step's sample differs from the spec's, so its line says FAIL + m_ss = true; + boot_at(0); + baud_div = 1; + var buf : [72]u8 = [0] ** 72; + var got : usize = 0; + var ch : u8 = 0; + var ticks : u32 = 0; + var seen : u32 = 0; + while (seen == 0 and ticks < 1000000) { + tick(); + 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; } + } + } + m_ss = false; + assert_eq(seen, 1); + assert_eq(got, LINE_LEN); + assert_eq(hex_at(&buf, 10, 3), 0); + // Y is the ss run's first sample (639474), E the tt run's (689233) + assert_eq(hex_at(&buf, 16, 7), 639474); + assert_eq(hex_at(&buf, 26, 7), 689233); + assert_eq(buf[59], 32); + assert_eq(buf[60], 70); + assert_eq(buf[61], 65); + assert_eq(buf[62], 73); + assert_eq(buf[63], 76); + assert_eq(verdict, V_FAIL); + 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. 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. + m_ss = false; + boot_at(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_run : u32 = 0; + var run : u32 = 0; + var gapseen : u32 = 0; + while (got < 79 and ticks < 4000000) { + tick(); + ticks = ticks + 1; + now = uart_tx; + if (prev and !now) { + run = hi_run; + hi_run = 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 == 66 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_run = hi_run + 1; } + prev = now; + } + assert_eq(got, 79); + assert_eq(ferr, 0); + // line 0 whole: "T27 PSP N=000 Y=00A8451 E=00A8451 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], 80); + assert_eq(buf[5], 83); + assert_eq(buf[6], 80); + assert_eq(hex_at(&buf, 10, 3), 0); + assert_eq(hex_at(&buf, 16, 7), TT_RUN[0] as u64); + assert_eq(hex_at(&buf, 26, 7), TT_RUN[0] as u64); + assert_eq(hex_at(&buf, 36, 16), TT_RUN[0] as u64); + assert_eq(buf[60], 80); + assert_eq(buf[64], 13); + assert_eq(buf[65], 10); + // line 1 starts with the same seven characters, then " N=001" + assert_eq(buf[66], 84); + assert_eq(buf[67], 50); + assert_eq(buf[68], 55); + assert_eq(buf[69], 32); + assert_eq(buf[70], 80); + assert_eq(buf[71], 83); + assert_eq(buf[72], 80); + assert_eq(buf[73], 32); + assert_eq(buf[74], 78); + assert_eq(buf[75], 61); + assert_eq(hex_at(&buf, 76, 3), 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 (and the 1900 clocks of the next step) + assert(gapseen >= (1 + (GAP_BITS as u32)) * bd); + assert_eq(GAP_BITS, 2); + baud_div = BAUD_DIV; +} diff --git a/specs/fpga/sar_adc_ax7203.t27 b/specs/fpga/sar_adc_ax7203.t27 index 3d8d73320f..13efd153eb 100644 --- a/specs/fpga/sar_adc_ax7203.t27 +++ b/specs/fpga/sar_adc_ax7203.t27 @@ -626,7 +626,7 @@ fn board_vs_spec(i: u8, kk: []const u32, off: u32) -> u32 { } /// The value of the n hex digits of buf from position at. -fn hex_at(buf: []const u8, at: usize, n: usize) -> u64 { +pub fn hex_at(buf: []const u8, at: usize, n: usize) -> u64 { var v : u64 = 0; var k : usize = 0; while (k < n) {