Where the clock enters
You will learn
Where a board's clock really comes from, and how a ring oscillator inside the chip was measured on three dice over JTAG.
The clock enters the board, not the chip: an oscillator on the PCB drives a pin. The board spec of the QMTech Wukong (XC7A200T in an FGG676 package, part xc7a200tfgg676) also measures a clock that never leaves the chip: CFGMCLK, a ring oscillator with no crystal behind it. UG470 gives 65 MHz nominal over a 50-80 MHz envelope. It was measured on the three attached dice by timing a 2^24 prescaler over JTAG: 70770, 68490 and 67200 kHz. The recording runs the native t27c on the board spec: 15 tests pass, 11 invariants are proved comptime.
Try it
In the recording, find the three measured CFGMCLK values and the busdev numbers of their dice; then in the spec frame find the UG470 envelope they are compared with and the prescaler that made them readable.
t27c 0.4.0 on a laptop (macOS): 15 tests of the Wukong board spec pass natively and 11 invariants are proved comptime; the part line names the xc7a200tfgg676 the board carries.
specs/boards/wukong_v1.t27
// SPDX-License-Identifier: Apache-2.0
// t27/specs/boards/wukong_v1.t27
// QMTech Wukong V1 / XC7A200T-FGG676 -- the board actually on this bench.
//
// WHY THIS EXISTS. `specs/boards/` held three files before this one:
// `arty_a7.t27` (a different board, csg324) and `xc7a100t_full.t27` /
// `xc7a100t_minimal.t27` -- both for an XC7A100T. The chip on every one of the
// three connected boards is an XC7A200T; `fpga/HARDWARE_SSOT.md` recorded that
// on 2026-07-03 and no spec followed. So the board this project builds for,
// flashes and reads verdicts off had NO machine-checkable description at all,
// while two specs described a part that is not here. Measured 2026-08-17 (W805).
//
// WHAT THIS FILE IS FOR, beyond bookkeeping. A partner analysis concluded that a
// 1.7-billion-weight ternary LLM (Ternary-Bonsai-1.7B, Q2_0, 2.125 bits/weight)
// "fits the board": 457.3 MB of weights against 1 GB of DDR3 on an Alinx AX7203.
// That board is not this board. This file states, as comptime invariants, the
// two things that decide the question here:
//
// 1. NON-VOLATILE STORAGE IS MEASURED AND IT IS NOT ENOUGH. The SPI flash
// answers JEDEC 0x20ba18 on all three dice -- Micron N25Q128, 128 Mbit,
// 16 MiB. Against 457.3 MB of weights that is a 27x shortfall, and it is a
// constraint that appears in none of the partner's P0 items. Weights that
// do not fit the flash have no home across a power cycle: every boot must
// stream them from a host.
//
// 2. DRAM CAPACITY IS NOT MEASURED, so the fit question is not answered here.
// This file does NOT guess it. `DRAM_BYTES_MEASURED = false` and the
// predicate `weights_fit_dram` is deliberately unusable until a real
// measurement replaces the sentinel. Guessing 1 GB because a different
// board has 1 GB is precisely the substitution this file exists to stop.
//
// Sources for the model figures: two partner documents dated 2026-08-17 --
// "Does the ternary model fit in an AX7203, and what is needed" and "Protocol of
// a real run: the ternary model answers" -- which read the geometry out of the
// GGUF metadata rather than from prose. Titles translated; the originals are
// Russian and live outside this repository.
//
// phi^2 + 1/phi^2 = 3 | TRINITY
module BoardWukongV1 {
// ---- Identity, all read off the hardware ----
const BOARD_NAME : &str = "QMTech Wukong V1";
const FPGA_PART : &str = "xc7a200tfgg676-1";
const FPGA_FAMILY : &str = "artix7";
// openFPGALoader reports this on busdev 1:4, 1:6 and 1:8 alike.
const JTAG_IDCODE : u32 = 0x03636093;
// The prjxray-db entry used for place-and-route. Same die, same BGA-676
// pinout; Xilinx publishes only `xc7a200tfbg676pkg.txt`. See
// fpga/HARDWARE_SSOT.md §2026-07-05.
const PNR_PART : &str = "xc7a200tfbg676-1";
// Fabric, from the Artix-7 datasheet for the 200T.
const LUT_TOTAL : u32 = 215_360;
const DSP48E1_TOTAL: u32 = 740;
// ---- The cables ----
//
// Three Digilent FTDI cables, all `0x0403:0x6014`, ALL SHARING serial
// 210512180081. Serial-based addressing therefore cannot separate them and
// `--busdev-num` is the only handle. This is recorded as data because it has
// cost this project thirteen waves of mis-diagnosis.
const CABLE_COUNT : u32 = 3;
const CABLE_VID : u32 = 0x0403;
const CABLE_PID : u32 = 0x6014;
const CABLES_SHARE_SERIAL : bool = true;
// ---- SPI flash: MEASURED, on all three dice ----
const FLASH_JEDEC_ID : u32 = 0x20BA18; // Micron N25Q128
const FLASH_MBIT : u32 = 128;
const FLASH_BYTES : u32 = 16_777_216; // 128 Mbit / 8
// ---- CFGMCLK: MEASURED on each of the three dice (T495) ----
//
// STARTUPE2's CFGMCLK is an internal RING OSCILLATOR with no crystal; UG470
// gives 65 MHz nominal over a 50-80 MHz envelope. Measured by timing the
// `beat` bit of `fpga/verilog/e8m0_jtag.v` (a 2^24 prescaler) over JTAG at
// 199 samples/s, 60 s per die. Held in kHz because the numeric core is
// integer; the three dice are named by their `--busdev-num`.
//
// These are the first physical characterisation of these parts. They cost no
// rebuild, no package pin and no extra logic -- every BSCAN wrapper in
// fpga/verilog/ already carries the heartbeat that makes them readable.
const CFGMCLK_KHZ_BUSDEV_1_4 : u32 = 70_770;
const CFGMCLK_KHZ_BUSDEV_1_6 : u32 = 68_490;
const CFGMCLK_KHZ_BUSDEV_1_8 : u32 = 67_200;
const CFGMCLK_KHZ_NOMINAL : u32 = 65_000; // UG470
const CFGMCLK_KHZ_MIN : u32 = 50_000; // UG470 envelope
const CFGMCLK_KHZ_MAX : u32 = 80_000;
fn cfgmclk_in_datasheet_range(khz: u32) -> bool {
if (khz < CFGMCLK_KHZ_MIN) { return false; }
if (khz > CFGMCLK_KHZ_MAX) { return false; }
return true;
}
// ---- DRAM: NOT MEASURED. Do not fill this in from a datasheet. ----
//
// The sentinel is zero and the flag is false. Every predicate below that
// depends on DRAM refuses to answer while the flag is false, rather than
// returning a plausible number. A wrong capacity here would propagate into a
// partner-facing feasibility claim, which is exactly how the AX7203 figure
// arrived at this bench in the first place.
const DRAM_BYTES_MEASURED : bool = false;
const DRAM_BYTES : u32 = 0;
// ---- The workload under question ----
//
// Ternary-Bonsai-1.7B-Q2_0: 1.72e9 weights, block of 128 weights in 34 bytes
// (32 bytes of ternary codes + one FP16 scale) = 2.125 bits/weight.
// Tensor sum 457.3 MB; the GGUF file is 436 MiB, which agrees to 0.03%.
const MODEL_WEIGHT_BYTES : u32 = 457_300_000;
const MODEL_LARGEST_TENSOR_BYTES : u32 = 3_300_000; // an FFN tensor
const BRAM_BYTES : u32 = 1_600_000; // 1.60 MB on the 200T
// KV cache per token, fp16: 28 layers * 8 KV heads * 128 * 2 = 57344 values.
const KV_BYTES_PER_TOKEN : u32 = 114_688;
// ---- Predicates ----
// The one that is answerable today.
fn weights_fit_flash() -> bool {
return (MODEL_WEIGHT_BYTES <= FLASH_BYTES);
}
// How many times over the weights exceed non-volatile storage, floored.
fn flash_shortfall_factor() -> u32 {
return (MODEL_WEIGHT_BYTES / FLASH_BYTES);
}
// The one that is NOT answerable today. Returns false when the capacity has
// not been measured -- NOT because the weights do not fit, but because the
// question has no input. Callers must test `DRAM_BYTES_MEASURED` first; that
// is the same discipline `e8m0_is_nan` imposes in specs/numeric/e8m0.t27.
fn weights_fit_dram() -> bool {
if (DRAM_BYTES_MEASURED == false) { return false; }
return (MODEL_WEIGHT_BYTES <= DRAM_BYTES);
}
// The largest single tensor against block RAM. Independent of DRAM, and it
// is what forces tiling regardless of how the capacity question resolves.
fn largest_tensor_fits_bram() -> bool {
return (MODEL_LARGEST_TENSOR_BYTES <= BRAM_BYTES);
}
// KV cache for a context length, in bytes.
fn kv_bytes(ctx_tokens: u32) -> u32 {
return (KV_BYTES_PER_TOKEN * ctx_tokens);
}
// ---- Combinational port surface (T81) ----
//
// Without a data port the module has no boundary and synthesises to nothing.
// This one answers a storage query: given a code, return the byte figure it
// names. It is a lookup, and that is honest -- this module describes a board,
// it does not compute on one.
fn on_comb(x: u32) -> u32 {
if (x == 0) { return FLASH_BYTES; }
if (x == 1) { return MODEL_WEIGHT_BYTES; }
if (x == 2) { return BRAM_BYTES; }
if (x == 3) { return KV_BYTES_PER_TOKEN; }
if (x == 4) { return LUT_TOTAL; }
return 0;
}
// ---- Tests ----
test idcode_is_the_two_hundred_t
given v = JTAG_IDCODE
then v == 0x03636093
test flash_is_one_twenty_eight_mbit
given v = FLASH_MBIT
then v == 128
test flash_bytes_follow_from_mbit
given v = FLASH_BYTES
then v == 16777216
// THE RESULT. The weights do not fit the flash, and this is the constraint
// no plan on the table lists.
test weights_do_not_fit_flash
given r = weights_fit_flash()
then r == false
test flash_shortfall_is_twenty_seven_fold
given f = flash_shortfall_factor()
then f == 27
// The DRAM question is refused, not answered.
test dram_capacity_is_not_measured
given m = DRAM_BYTES_MEASURED
then m == false
test dram_fit_refuses_to_answer
given r = weights_fit_dram()
then r == false
test largest_tensor_exceeds_bram
given r = largest_tensor_fits_bram()
then r == false
test kv_for_one_k_context
given b = kv_bytes(1024)
then b == 117440512
test comb_returns_flash_bytes
given r = on_comb(0)
then r == 16777216
test comb_returns_lut_total
given r = on_comb(4)
then r == 215360
// ---- CFGMCLK, measured (T495) ----
test die_one_four_is_in_range
given r = cfgmclk_in_datasheet_range(CFGMCLK_KHZ_BUSDEV_1_4)
then r == true
test die_one_six_is_in_range
given r = cfgmclk_in_datasheet_range(CFGMCLK_KHZ_BUSDEV_1_6)
then r == true
test die_one_eight_is_in_range
given r = cfgmclk_in_datasheet_range(CFGMCLK_KHZ_BUSDEV_1_8)
then r == true
test a_frequency_below_the_envelope_is_rejected
given r = cfgmclk_in_datasheet_range(40_000)
then r == false
// ---- Invariants ----
invariant flash_bytes_are_mbit_over_eight
assert FLASH_BYTES * 8 == FLASH_MBIT * 1_048_576
// The shortfall, asserted at compile time so it cannot be softened in prose.
invariant weights_exceed_flash
assert MODEL_WEIGHT_BYTES > FLASH_BYTES
invariant shortfall_is_at_least_twenty_seven
assert MODEL_WEIGHT_BYTES > (FLASH_BYTES * 27)
// Tiling is forced by BRAM alone, whatever the DRAM turns out to be.
invariant tiling_is_mandatory
assert MODEL_LARGEST_TENSOR_BYTES > BRAM_BYTES
// The sentinel must stay a sentinel until someone measures the board.
invariant dram_sentinel_is_zero_while_unmeasured
assert DRAM_BYTES == 0
// Three cables, and they cannot be told apart by serial.
invariant three_cables_share_one_serial
assert CABLE_COUNT == 3
// ALL THREE DICE RUN FAST. Every one measures above the 65 MHz nominal --
// 3.4%, 5.4% and 8.9% -- and all three stay inside the envelope. Asserted so
// the ordering cannot be lost to prose: 1:4 is the fastest of the three.
invariant every_die_runs_above_nominal
assert CFGMCLK_KHZ_BUSDEV_1_8 > CFGMCLK_KHZ_NOMINAL
invariant one_four_is_the_fastest_die
assert CFGMCLK_KHZ_BUSDEV_1_4 > CFGMCLK_KHZ_BUSDEV_1_6
invariant one_six_is_faster_than_one_eight
assert CFGMCLK_KHZ_BUSDEV_1_6 > CFGMCLK_KHZ_BUSDEV_1_8
// The measured spread is 5.19%, comfortably inside the envelope's width.
invariant spread_is_smaller_than_the_envelope
assert (CFGMCLK_KHZ_BUSDEV_1_4 - CFGMCLK_KHZ_BUSDEV_1_8)
< (CFGMCLK_KHZ_MAX - CFGMCLK_KHZ_MIN)
// A ternary core needs no DSP48E1; the FP16 block scales do. One scale per
// 128 weights over 1.72e9 weights is 13.4e6 multiplies per token, which is
// roughly one DSP48E1 of the 740 at a few tokens per second -- so "zero
// DSP48" is true of the ternary core and false of the full pipeline.
invariant the_die_has_dsp_even_though_our_cores_use_none
assert DSP48E1_TOTAL == 740
// ---- Bench ----
bench wukong_storage_arithmetic
assert weights_fit_flash() == false
assert flash_shortfall_factor() == 27
assert largest_tensor_fits_bram() == false
assert kv_bytes(1024) == 117440512
}
// phi^2 + 1/phi^2 = 3 | TRINITY
All lessons
Module 1 · What a clock is
One edge, one world: what shares a clock edge shares a world, the period and the jitter of a real edge, and where the clock enters a board.
Module 2 · Clock trees
Skew and insertion delay, the global buffer network, and the trap of gating a clock with logic.
Module 3 · PLL and MMCM
Multiply and divide one clock into another, move its phase in steps of the VCO, and which clocks the analyzer treats as related.
Module 4 · Resets
Assert asynchronously, release synchronously: the three reset kinds, the release pipe, and the tree a reset grows.
Module 5 · Metastability
The setup-hold window, the mean time between failures in integer arithmetic, and the two flops that fix it.
Module 6 · Crossing many bits
Why a binary bus tears, why Gray code does not, and the handshake that moves a pulse between worlds.
Module 7 · The asynchronous FIFO
Pointers, flags and depth: the buffer that moves a stream between two clocks.
Module 8 · Constraints
The lines that tell the analyzer what a clock is, which paths not to check, and what the pins must meet.
Module 9 · On the board
A CDC report, one crossing captured at the flip-flops, and the bitstream diff that closes the course.