t27.aiEnglish

Где входит тактовый сигнал

Вы узнаете

Откуда на самом деле берётся тактовый сигнал платы и как кольцевой генератор внутри кристалла измерили на трёх кристаллах через JTAG.

Тактовый сигнал входит в плату, а не в кристалл: генератор на печатной плате ведёт вывод. Спека платы QMTech Wukong (XC7A200T в корпусе FGG676, деталь xc7a200tfgg676) ещё и измеряет тактовый сигнал, который не покидает кристалл: CFGMCLK — кольцевой генератор без кварца. UG470 даёт номинал 65 МГц в коридоре 50-80 МГц. Его измерили на трёх подключённых кристаллах, хронометрируя прескалер 2^24 через JTAG: 70770, 68490 и 67200 кГц. Запись запускает нативный t27c на спеке платы: проходят 15 тестов, 11 инвариантов доказаны comptime.

Попробуйте

В записи найдите три измеренных значения CFGMCLK и номера busdev их кристаллов; затем в окне спеки найдите коридор UG470, с которым их сравнивают, и прескалер, который сделал их читаемыми.

Открыть интерактивный урок →

t27c on wukong_v1.t27 -- the board spec, native
t27c on wukong_v1.t27 -- the board spec, native ↗

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

Открыть спеку урока в плеере ↗

Все уроки