Сквозные сценарии

Вы научитесь

Как сценарий проходит весь поток и что сквозной прогон доказывает, чего не могут юниты.

Попробуйте

Пройдите по виджету потока слой за слоем и назовите артефакт каждого слоя; затем найдите в e2e_demo место, где пропавший артефакт останавливает прогон.

specs/fpga/e2e_demo.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/e2e_demo.t27
// T27 End-to-End Demo Specification
// Exercises the full toolchain: assembler -> ternary core -> GF16 -> VCD trace
// Validates the complete FPGA pipeline from spec to hardware simulation
// Uses flat arrays + count fields (parser-compatible)
// phi^2 + 1/phi^2 = 3 | TRINITY

module E2eDemo {

    // === Demo program (trivial ternary kernel) ===

    pub struct DemoKernel {
        name : &str,
        instr_count : u32,
        gf16_ops : u32,
        alu_ops : u32,
        mem_ops : u32,
    }

    fn hello_kernel() -> DemoKernel {
        return DemoKernel{
            .name = "hello_trinity",
            .instr_count = 12,
            .gf16_ops = 4,
            .alu_ops = 6,
            .mem_ops = 2,
        };
    }

    fn gf16_mac_kernel() -> DemoKernel {
        return DemoKernel{
            .name = "gf16_mac_demo",
            .instr_count = 20,
            .gf16_ops = 10,
            .alu_ops = 6,
            .mem_ops = 4,
        };
    }

    // === Pipeline simulation result ===

    pub struct PipeResult {
        cycles : u32,
        instr_retired : u32,
        stalls : u32,
        gf16_results : u32,
        errors : u32,
    }

    fn pipe_result_ok(cycles: u32, retired: u32, gf16: u32) -> PipeResult {
        return PipeResult{
            .cycles = cycles,
            .instr_retired = retired,
            .stalls = 0,
            .gf16_results = gf16,
            .errors = 0,
        };
    }

    fn pipe_result_error(cycles: u32, errors: u32) -> PipeResult {
        return PipeResult{
            .cycles = cycles,
            .instr_retired = 0,
            .stalls = 0,
            .gf16_results = 0,
            .errors = errors,
        };
    }

    // === Demo config ===

    pub struct DemoConfig {
        kernel : DemoKernel,
        clock_mhz : u32,
        max_cycles : u32,
        trace_enabled : bool,
        formal_check : bool,
    }

    fn demo_config(kernel: DemoKernel) -> DemoConfig {
        return DemoConfig{
            .kernel = kernel,
            .clock_mhz = 100,
            .max_cycles = 100000,
            .trace_enabled = true,
            .formal_check = true,
        };
    }

    // === Query functions ===

    fn ipc(result: PipeResult) -> u32 {
        if result.cycles == 0 {
            return 0;
        }
        return result.instr_retired * 100 / result.cycles;
    }

    fn cpi(result: PipeResult) -> u32 {
        if result.instr_retired == 0 {
            return 0;
        }
        return result.cycles / result.instr_retired;
    }

    fn gf16_throughput(result: PipeResult, clock_mhz: u32) -> u32 {
        if result.cycles == 0 {
            return 0;
        }
        return result.gf16_results * clock_mhz * 1000 / result.cycles;
    }

    fn sim_time_us(cfg: DemoConfig, cycles: u32) -> u32 {
        if cfg.clock_mhz == 0 {
            return 0;
        }
        return cycles / cfg.clock_mhz;
    }

    fn kernel_size_bytes(kernel: DemoKernel) -> u32 {
        return kernel.instr_count * 4;
    }

    fn passed(result: PipeResult) -> bool {
        return result.errors == 0 and result.instr_retired > 0;
    }

    // === Validation ===

    fn validate_kernel(kernel: DemoKernel) -> u32 {
        var errors : u32 = 0;
        if kernel.name == "" {
            errors = errors + 1;
        }
        if kernel.instr_count == 0 {
            errors = errors + 1;
        }
        return errors;
    }

    fn validate_config(cfg: DemoConfig) -> u32 {
        var errors : u32 = 0;
        errors = errors + validate_kernel(cfg.kernel);
        if cfg.clock_mhz == 0 {
            errors = errors + 1;
        }
        if cfg.max_cycles == 0 {
            errors = errors + 1;
        }
        return errors;
    }

    // === Tests ===

    test hello_kernel_creation
        given k = hello_kernel()
        then k.name == "hello_trinity"
        and k.instr_count == 12
        and k.gf16_ops == 4
        and k.alu_ops == 6
        and k.mem_ops == 2

    test gf16_mac_kernel_creation
        given k = gf16_mac_kernel()
        then k.name == "gf16_mac_demo"
        and k.instr_count == 20
        and k.gf16_ops == 10

    test pipe_result_ok
        given r = pipe_result_ok(100, 95, 10)
        then r.cycles == 100
        and r.instr_retired == 95
        and r.stalls == 0
        and r.gf16_results == 10
        and r.errors == 0

    test pipe_result_error
        given r = pipe_result_error(50, 2)
        then r.errors == 2
        and r.instr_retired == 0

    test ipc_calculation
        given r = pipe_result_ok(100, 50, 0)
        then ipc(r) == 50

    test ipc_zero_cycles
        given r = pipe_result_ok(0, 0, 0)
        then ipc(r) == 0

    test cpi_calculation
        given r = pipe_result_ok(200, 100, 0)
        then cpi(r) == 2

    test cpi_zero_retired
        given r = pipe_result_ok(100, 0, 0)
        then cpi(r) == 0

    test gf16_throughput_calc
        given r = pipe_result_ok(1000, 500, 100)
        then gf16_throughput(r, 100) == 10000

    test sim_time_us
        given cfg = demo_config(hello_kernel())
        then sim_time_us(cfg, 100000) == 1000

    test kernel_size_bytes
        given k = hello_kernel()
        then kernel_size_bytes(k) == 48

    test passed_ok
        given r = pipe_result_ok(100, 50, 10)
        then passed(r) == true

    test passed_with_errors
        given r = pipe_result_error(100, 1)
        then passed(r) == false

    test validate_hello_kernel
        given k = hello_kernel()
        then validate_kernel(k) == 0

    test validate_empty_kernel
        given k = DemoKernel{.name = "", .instr_count = 0, .gf16_ops = 0, .alu_ops = 0, .mem_ops = 0}
        then validate_kernel(k) > 0

    test validate_demo_config
        given cfg = demo_config(hello_kernel())
        then validate_config(cfg) == 0

    // === Invariants ===

    invariant kernel_size_positive
        given k = hello_kernel()
        assert kernel_size_bytes(k) > 0

    invariant ipc_non_negative
        given r = pipe_result_ok(100, 50, 0)
        assert ipc(r) >= 0

    invariant sim_time_non_negative
        given cfg = demo_config(hello_kernel())
        assert sim_time_us(cfg, 100000) >= 0

    // === Benchmarks ===

    bench e2e_latency
        measure: nanoseconds for pipe_result_ok(1000, 500, 50)
        target: < 100ns
}

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

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

Все уроки

• Модуль 1 · Зачем проверять

  Дизайны, которые компилируются и ошибаются; модель, которая выносит вердикт; план, записанный до кода.

  1. 01 Баги, которые компилируются
  2. 02 Золотая модель
  3. 03 Сначала план

• Модуль 2 · Тестбенчи

  Стимулы, проверки и вердикт, записанные как один spec рядом с дизайном, который они судят.

  1. 04 Анатомия тестбенча
  2. 05 Самопроверка вместо всматривания
  3. 06 Направленные против случайных

• Модуль 3 · Временные диаграммы

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

  1. 07 Формат VCD
  2. 08 Отладка по волнам
  3. 09 Сравнение двух трасс

• Модуль 4 · Векторы соответствия

  Случаи с ответом, записанным рядом, там, откуда их достанет компилятор.

  1. 10 Что такое вектор
  2. 11 Векторы как эталонная линейка
  3. 12 Сквозные сценарии

• Модуль 5 · Косимуляция

  Spec, симулятор и плата сходятся в одном ответе на стенде Artix-7 XC7A200T, и что делать, когда не сходятся.

  1. 13 Тройное согласие
  2. 14 Внутри симулятора
  3. 15 Когда они не сходятся

• Модуль 6 · Покрытие

  Чего коснулись тесты: строки, переключения, состояния — и что прячет это число.

  1. 16 Строки и переключения
  2. 17 Покрытие автоматов
  3. 18 Покрытие лжёт

• Модуль 7 · Формальные методы

  Ассерты, верные каждый такт; ограниченный поиск контрпримера; и почему доказательству нужна индукция.

  1. 19 Ассерты
  2. 20 Ограниченная проверка моделей
  3. 21 Индукция

• Модуль 8 · Мутации

  Ломайте дизайн нарочно и считайте, что заметили тесты.

  1. 22 Убить мутанта
  2. 23 Выжившие мутанты
  3. 24 Сила тестов

• Модуль 9 · Приёмка

  Одна команда, все квитанции, чистый вердикт, который можно показать.

  1. 25 Сборка и проверка
  2. 26 Стенд проверяет себя
  3. 27 Капстоун: проверить модуль целиком