Байт масштаба на настоящей машине

Вы узнаете

Что нативный компилятор проверяет в той же спеке, включая то, что браузер пропустил.

Попробуйте

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

specs/numeric/e8m0.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/numeric/e8m0.t27
// E8M0 -- the OCP Microscaling shared scale, and the trit count it does not have.
//
// WHY THIS EXISTS. `specs/numeric/formats_catalog.t27` is the numeric SSOT and it
// names `e8m0` FIVE times as the storage of another format --
//
//     mxfp8   storage=u8_plus_shared_e8m0
//     mxfp6   storage=u8_packed_plus_e8m0
//     mxfp4   storage=u8_packed_plus_e8m0
//     mxgf6   storage=u8_packed_plus_e8m0
//     mxgf4   storage=u8_packed_plus_e8m0
//
// -- and `grep "id=e8m0 "` over the same file returns ZERO. The SSOT depends on a
// component it never defines. This file defines it. Measured 2026-08-16.
//
// LAYOUT.  E8M0 = [ exponent(8) ].  No sign. No mantissa. No implicit one.
//
//     value = 2^(E - 127),   E in [0, 254]
//     E = 255                is NaN
//
// Source: OCP Microscaling Formats (MX) Specification v1.0, Rouhani et al. 2023,
// arXiv:2310.10537 -- the citation the catalogue already carries for every one of
// the five dependants.
//
// THE RESULT THIS MIGRATION PRODUCED, which is why it is worth a spec and not a
// constant. E8M0's exponent takes 255 distinct finite values, e in [-127, +127].
// Five balanced trits span 3^5 = 243 and six span 3^6 = 729, so
//
//     243 < 255 < 729
//
// and E8M0's exponent field is NOT a whole number of trits. It needs six and
// uses 255 of 729 -- 35 percent. Contrast `specs/numeric/tnf17.t27`, whose
// offset field holds exactly 81 = 3^4 values and uses 81 of 81. That contrast is
// stated below as a comptime invariant rather than as prose, because it is the
// only thing this format tells us that its own standard does not.
//
// WHAT THIS IS NOT. E8M0 is a SHARED SCALE, applied once per block of elements,
// not a weight code. Under the golden sieve (specs/numeric/golden_sieve.t27) it
// is not a candidate at all: S1 asks |A| = 3^k and 255 is not a power of three.
// It is also, for the same reason it is cheap, exempt from the sieve's concerns
// -- a pure power of two applied to a whole block is one shift, one lane, no
// DSP, and it never enters a neuron's truth table.
//
// phi^2 + phi^-2 = 3 | TRINITY

module E8M0 {

    // ---- Field geometry, from the OCP MX v1.0 specification ----

    const E8M0_BITS       : u32 = 8;
    const E8M0_BIAS       : i32 = 127;   // code 127 == 2^0
    const E8M0_NAN_CODE   : u32 = 255;   // the one reserved code
    const E8M0_MAX_FINITE : u32 = 254;   // largest finite code, 2^127
    const E8M0_MIN_FINITE : u32 = 0;     // smallest finite code, 2^-127
    const E8M0_ONE        : u32 = 127;   // the code whose value is 1.0

    // Distinct finite values the field can hold: 0..254 inclusive.
    const E8M0_FINITE_CODES : u32 = 255;

    // Trit spans, written out because the numeric core has no exponentiation.
    //
    // W781 DEFECT, caught by the comptime invariant that is the reason this file
    // has invariants at all: the first version of this table started at 3^5, so
    // `trits_needed(81)` answered 5 and `packs_exactly(81)` came back FALSE for a
    // number that is exactly 3^4. The table must reach DOWN to every power a
    // caller might land on, not only up to the one the subject format needs.
    const THREE_POW_3 : u32 = 27;
    const THREE_POW_4 : u32 = 81;
    const THREE_POW_5 : u32 = 243;
    const THREE_POW_6 : u32 = 729;

    // TNF17e's offset field, for the contrast invariant below. Kept as a local
    // constant rather than an import so this file stays self-contained; the
    // value is checked against tnf17.t27's own TNF_OFFSET_MAX + 1.
    const TNF17_OFFSET_VALUES : u32 = 81;    // 3^4, and it uses all 81

    // ---- Decode ----

    // The unbiased exponent. Returns the exponent of a FINITE code; callers must
    // test e8m0_is_nan first, exactly as the standard requires.
    fn e8m0_exponent(x: u32) -> i32 {
        return ((x as i32) - E8M0_BIAS);
    }

    fn e8m0_is_nan(x: u32) -> bool {
        return (x == E8M0_NAN_CODE);
    }

    fn e8m0_is_finite(x: u32) -> bool {
        return (x <= E8M0_MAX_FINITE);
    }

    // ---- Encode ----

    // The inverse of e8m0_exponent, for e in [-127, +127]. Out-of-range inputs
    // return the NaN code rather than wrapping: a scale that cannot be
    // represented is not a scale, and silently aliasing it to a representable
    // one is how a block of elements acquires the wrong magnitude.
    fn e8m0_encode(e: i32) -> u32 {
        if (e < (0 - E8M0_BIAS)) { return E8M0_NAN_CODE; }
        if (e > E8M0_BIAS) { return E8M0_NAN_CODE; }
        return ((e + E8M0_BIAS) as u32);
    }

    // ---- Trit accounting: the part the standard does not state ----

    // Whether `n` distinct values fit in five balanced trits, six, or neither
    // exactly. Returns the number of trits NEEDED; 0 means more than six.
    fn trits_needed(n: u32) -> u32 {
        if (n <= THREE_POW_3) { return 3; }
        if (n <= THREE_POW_4) { return 4; }
        if (n <= THREE_POW_5) { return 5; }
        if (n <= THREE_POW_6) { return 6; }
        return 0;
    }

    // The codes a trit count leaves unused. This is the substrate tax on the
    // exponent field, in the same units the rest of the numeric line uses.
    fn trit_waste(n: u32) -> u32 {
        if (trits_needed(n) == 3) { return (THREE_POW_3 - n); }
        if (trits_needed(n) == 4) { return (THREE_POW_4 - n); }
        if (trits_needed(n) == 5) { return (THREE_POW_5 - n); }
        if (trits_needed(n) == 6) { return (THREE_POW_6 - n); }
        return 0;
    }

    // Does `n` land exactly on a power of three, i.e. pack with zero waste?
    fn packs_exactly(n: u32) -> bool {
        return (trit_waste(n) == 0);
    }

    // ---- Combinational port surface (T81: without this the module has no
    // boundary and synthesises to nothing) ----
    //
    // Round-trip a code through decode and encode. Exercises the bias path in
    // both directions and the NaN guard, in one function.
    fn on_comb(x: u32) -> u32 {
        if (e8m0_is_nan(x)) { return E8M0_NAN_CODE; }
        return e8m0_encode(e8m0_exponent(x));
    }

    // ---- Tests ----

    test one_is_code_one_two_seven
        given e = e8m0_exponent(E8M0_ONE)
        then e == 0

    test smallest_finite_is_minus_one_two_seven
        given e = e8m0_exponent(E8M0_MIN_FINITE)
        then e == -127

    test largest_finite_is_plus_one_two_seven
        given e = e8m0_exponent(E8M0_MAX_FINITE)
        then e == 127

    test nan_code_is_detected
        given r = e8m0_is_nan(E8M0_NAN_CODE)
        then r == true

    test max_finite_is_not_nan
        given r = e8m0_is_nan(E8M0_MAX_FINITE)
        then r == false

    test nan_code_is_not_finite
        given r = e8m0_is_finite(E8M0_NAN_CODE)
        then r == false

    test encode_zero_gives_one
        given c = e8m0_encode(0)
        then c == 127

    test encode_minus_one_two_seven
        given c = e8m0_encode(-127)
        then c == 0

    test encode_plus_one_two_seven
        given c = e8m0_encode(127)
        then c == 254

    // The guard, and the reason it exists: 2^128 has no E8M0 code, and returning
    // code 1 for it would scale a whole block by 2^-126.
    test encode_out_of_range_is_nan
        given c = e8m0_encode(128)
        then c == 255

    test encode_below_range_is_nan
        given c = e8m0_encode(-128)
        then c == 255

    // ---- Trit accounting ----

    test exponent_field_needs_six_trits
        given t = trits_needed(E8M0_FINITE_CODES)
        then t == 6

    test exponent_field_wastes_four_hundred_seventy_four
        given w = trit_waste(E8M0_FINITE_CODES)
        then w == 474

    test tnf17_offset_needs_exactly_four_trits
        given t = trits_needed(TNF17_OFFSET_VALUES)
        then t == 4

    test tnf17_offset_wastes_nothing
        given w = trit_waste(TNF17_OFFSET_VALUES)
        then w == 0

    // ---- Port surface ----

    test comb_round_trips_one
        given r = on_comb(E8M0_ONE)
        then r == 127

    test comb_round_trips_max_finite
        given r = on_comb(E8M0_MAX_FINITE)
        then r == 254

    test comb_passes_nan_through
        given r = on_comb(E8M0_NAN_CODE)
        then r == 255

    // ---- Invariants ----

    // The field holds 2^8 codes, of which exactly one is reserved.
    invariant one_code_is_reserved
        assert E8M0_FINITE_CODES + 1 == 256

    invariant bias_centres_the_range
        assert E8M0_BIAS * 2 == (E8M0_MAX_FINITE as i32)

    invariant one_sits_at_the_bias
        assert (E8M0_ONE as i32) == E8M0_BIAS

    invariant nan_is_the_code_above_max_finite
        assert E8M0_NAN_CODE == E8M0_MAX_FINITE + 1

    // THE RESULT. E8M0's exponent does not pack into trits and TNF17e's does.
    // Stated as an assertion so the contrast is checked at compile time rather
    // than asserted in a comment that can rot.
    invariant e8m0_exponent_does_not_pack_into_trits
        assert packs_exactly(E8M0_FINITE_CODES) == false

    invariant tnf17_offset_packs_exactly
        assert packs_exactly(TNF17_OFFSET_VALUES) == true

    // 243 < 255 < 729 -- the reason it needs six trits and cannot use five.
    invariant two_hundred_fifty_five_sits_between_the_powers
        assert THREE_POW_5 < E8M0_FINITE_CODES

    invariant two_hundred_fifty_five_is_below_three_to_the_six
        assert E8M0_FINITE_CODES < THREE_POW_6

    // The waste is the tax, and it is 65 percent of a six-trit field.
    invariant six_trit_field_is_mostly_unused
        assert trit_waste(E8M0_FINITE_CODES) > (E8M0_FINITE_CODES + 200)

    // ---- Bench ----

    bench e8m0_decode_encode
        assert e8m0_exponent(E8M0_ONE) == 0
        assert e8m0_encode(0) == E8M0_ONE
        assert on_comb(E8M0_MAX_FINITE) == E8M0_MAX_FINITE
}

// phi^2 + 1/phi^2 = 3 | TRINITY

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

Все уроки

• Модуль 1 · Чип

  Что такое FPGA, какой чип у нас и как его выводы встречаются с платой.

  1. 01 FPGA — это сетка, которую вы настраиваете
  2. 02 Какой это чип?
  3. 03 Выводы, шарики и корпус

• Модуль 2 · Числа в железе

  Биты, триты и форматы чисел, и сколько стоит арифметика в логике.

  1. 04 Биты, триты и GF16
  2. 05 Сколько стоит арифметика
  3. 06 Сколько помещается на чип

• Модуль 3 · Ваша программа на t27

  Напишите спеку, проверьте её и увидьте, почему «компилируется» не значит «верно».

  1. 07 Привет, t27
  2. 08 Тесты — часть спеки
  3. 09 Компилируется — не значит верно

• Модуль 4 · Внутри t27c

  Как компилятор читает спеку и что он пишет, включая нативный t27b.

  1. 10 Стадии t27c
  2. 11 t27c на настоящей машине
  3. 12 Семь бэкендов и t27b

• Модуль 5 · От спеки к железу

  Verilog, который пишет t27c, ячейки, в которые он превращается, и что делает одна LUT.

  1. 13 От спеки к Verilog
  2. 14 Посчитайте ячейки
  3. 15 Одна LUT вблизи

• Модуль 6 · Читаем синтез

  Что yosys сообщает о вашем дизайне и какие предупреждения важны.

  1. 16 Важные предупреждения синтеза
  2. 17 Конечные автоматы
  3. 18 Куда уходят LUT

• Модуль 7 · Размещение, трассировка, тайминг

  Где ячейки оказываются на кристалле и успевает ли тактовая частота.

  1. 19 Размещение: где оказываются ячейки
  2. 20 Глубина логики
  3. 21 Тайминг и запас

• Модуль 8 · Битстрим

  Как оттрассированный дизайн становится битами, которые загружает чип, без Vivado.

  1. 22 От FASM к фреймам
  2. 23 Сборка по пунктам
  3. 24 Читаем битстрим

• Модуль 9 · На плате

  Спросите чип, кто он, загрузите биты и проверьте их.

  1. 25 JTAG спрашивает чип
  2. 26 Те же биты — на плате
  3. 27 Итог: переугадайте yosys

• Модуль 10 · Лаборатория: наши исследования

  Свой формат чисел, честная таблица результатов и таблицы модели, перемноженные на плате.

  1. 28 T27: наш собственный формат чисел
  2. 29 Честная таблица результатов
  3. 30 Таблицы модели на плате

• Модуль 11 · ИИ-числа: блок MX

  Как ИИ-чипы хранят веса в нескольких битах: один общий масштаб на блок, сам байт масштаба и что один выброс делает с соседями.

  1. 31 Один масштаб на блок весов
  2. 32 Байт масштаба на настоящей машине
  3. 33 Один выброс, много нулей