t27.aiEnglish

Два произведения, одна сумма

Вы узнаете

Как умножение с накоплением в GF-T16 считает a1 * b1 + a2 * b2, ядро умножения матриц.

Каждый слой сети — стопка скалярных произведений, а скалярное произведение — сложенные произведения. gft_dot2.t27 — самое маленькое: y = a1 * b1 + a2 * b2 в GF-T16, 16-битной величине из 7-битного смещения и 9-битной мантиссы со смещением 40. В такой раскладке 1.0 — это код 20480, а 2.0 — код 20992. В спеке два теста: 1 * 1 = 1 и 1 * 1 + 1 * 1 = 2.

Попробуйте

Найдите оба теста и раскодируйте 20480 и 20992 вручную по value = (1 + mant / 512) * 2^(offset - 40). Затем найдите строку в gft_mul, которая обрабатывает перенос, когда произведение переходит 2.

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

GoldenFloat 14: two products, one sum
GoldenFloat 14: two products, one sum ↗

The two tests of gft_dot2.t27, read from gft_dot2.t27. Lesson 14 of the GoldenFloat course.

specs/ternary/gft_dot2.t27

module GftDot2;
// #1764 + GF-T: a SPEC-FIRST GF-T16 2-term dot product (MAC), y = a1*b1 + a2*b2.
//
// GF-T16 is the ternary-native GoldenFloat format now proven bit-exact ON SILICON
// (AX7203, gft_dot2 3/3). Its MAC is the kernel of every matmul / inference layer.
// The hand-written trinity-fpga/build/gft_dot2/*.v note that `t27c gen-verilog`
// could not emit this directly because it interleaved `reg` decls with statements
// (illegal Verilog) -- that backend bug is FIXED (#1741 hoists fn-local decls), so
// this is the spec-first realization of the SAME arithmetic, bit-exact to the
// silicon-proven RTL.
//
// GF-T16 packed magnitude: [ offset(7) : mant(9) ], value = (1 + mant/512) *
// 2^(offset-40). BIAS=40, OFFSET_MAX=80, MANT_ONE=512 (=1<<9), SIG_BITS=10.
// All intermediates are non-negative small integers, so i32 arithmetic (signed
// shifts/compares/multiply on positive values) is bit-identical to the unsigned
// hardware and keeps the typechecker's literal typing happy.

// GF-T ladder multiply (magnitude): sign-free, balanced-ternary exponent add.
fn gft_mul(a: u16, b: u16) -> u16 {
    var a_off : i32 = (a >> 9) as i32;
    var a_mant : i32 = (a & 511) as i32;
    var b_off : i32 = (b >> 9) as i32;
    var b_mant : i32 = (b & 511) as i32;
    // full-precision significand product (1+M/512) scaled by 512^2
    var prod : i32 = (512 + a_mant) * (512 + b_mant);
    var carry : i32 = 0;
    if (prod >= 524288) { carry = 1; }               // 2*512*512 renorm boundary
    var sum : i32 = a_off + b_off + carry;
    var out_off : i32 = 0;
    if (sum >= 40) {
        var result : i32 = sum - 40;
        if (result >= 80) { out_off = 80; } else { out_off = result; }
    }
    // renormalize the mantissa by the carry (divisors are powers of two -> shifts)
    var out_mant : i32 = (prod >> 9) - 512;
    if (carry == 1) { out_mant = (prod >> 10) - 512; }
    return ((out_off << 9) | out_mant) as u16;
}

// GF-T ladder add (same-sign): align the smaller operand, add, renormalize by one carry.
fn gft_add(a: u16, b: u16) -> u16 {
    var a_off : i32 = (a >> 9) as i32;
    var a_mant : i32 = (a & 511) as i32;
    var b_off : i32 = (b >> 9) as i32;
    var b_mant : i32 = (b & 511) as i32;
    var hi_off : i32 = b_off;
    var hi_m : i32 = b_mant;
    var lo_off : i32 = a_off;
    var lo_m : i32 = a_mant;
    if (a_off >= b_off) {
        hi_off = a_off; hi_m = a_mant; lo_off = b_off; lo_m = b_mant;
    }
    var d : i32 = hi_off - lo_off;
    var sb : i32 = 0;
    if (d < 10) { sb = (512 + lo_m) >> d; }          // align smaller significand right
    var sum : i32 = (512 + hi_m) + sb;
    var out_off : i32 = hi_off;
    var out_mant : i32 = sum - 512;
    if (sum >= 1024) {                                // significand carry -> exp += 1
        var e : i32 = hi_off + 1;
        if (e >= 80) { out_off = 80; } else { out_off = e; }
        out_mant = (sum >> 1) - 512;
    }
    return ((out_off << 9) | out_mant) as u16;
}

// The MAC: y = a1*b1 + a2*b2, the multiply-accumulate at the heart of inference.
fn on_comb(a1: u16, b1: u16, a2: u16, b2: u16) -> u16 {
    return gft_add(gft_mul(a1, b1), gft_mul(a2, b2));
}

// 1.0 = (1 + 0/512) * 2^0 -> offset 40, mant 0 -> 40<<9 = 20480 = 0x5000.
test one_times_one_mul { assert_eq(gft_mul(20480, 20480), 20480); }       // 1*1 = 1
test dot_one { assert_eq(on_comb(20480, 20480, 20480, 20480), 20992); }   // 1*1+1*1 = 2 (0x5200)
endmodule

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

Все уроки