Золотая модель

Вы научитесь

Что такое эталонная модель и как набор соответствия держит инструмент в рамках.

Попробуйте

Откройте tri-fpga-specs и прочитайте тест-блоки одного spec соответствия; затем откройте testbench.t27 и назовите четыре формы, которые обязан иметь тестбенч.

specs/fpga/testbench.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/testbench.t27
// T27 HIR Testbench Auto-Generation Specification
// Automatically generates Verilog testbenches from HIR modules
// Includes clock generation, reset sequencing, stimulus, and checking
// Uses flat arrays + count fields (parser-compatible)
// phi^2 + 1/phi^2 = 3 | TRINITY

module Testbench {

    // === Testbench clock config ===

    pub struct TbClockCfg {
        period_ns : u32,
        duty_cycle : u32,
        phase_ns : u32,
    }

    fn clock_cfg(period: u32) -> TbClockCfg {
        return TbClockCfg{
            .period_ns = period,
            .duty_cycle = 50,
            .phase_ns = 0,
        };
    }

    fn half_period(cfg: TbClockCfg) -> u32 {
        return cfg.period_ns / 2;
    }

    // === Reset config ===

    pub struct TbResetCfg {
        active_low : bool,
        delay_cycles : u32,
        duration_cycles : u32,
    }

    fn reset_cfg(delay: u32, duration: u32) -> TbResetCfg {
        return TbResetCfg{
            .active_low = true,
            .delay_cycles = delay,
            .duration_cycles = duration,
        };
    }

    fn reset_end_cycle(cfg: TbResetCfg) -> u32 {
        return cfg.delay_cycles + cfg.duration_cycles;
    }

    // === Stimulus entry ===

    pub struct TbStimulus {
        cycle : u32,
        signal : &str,
        value : u32,
    }

    fn stimulus(cycle: u32, signal: &str, value: u32) -> TbStimulus {
        return TbStimulus{
            .cycle = cycle,
            .signal = signal,
            .value = value,
        };
    }

    // === Expected check ===

    pub struct TbCheck {
        cycle : u32,
        signal : &str,
        expected : u32,
        mask : u32,
    }

    fn check(cycle: u32, signal: &str, expected: u32) -> TbCheck {
        return TbCheck{
            .cycle = cycle,
            .signal = signal,
            .expected = expected,
            .mask = 4294967295,
        };
    }

    fn check_with_mask(cycle: u32, signal: &str, expected: u32, mask: u32) -> TbCheck {
        return TbCheck{
            .cycle = cycle,
            .signal = signal,
            .expected = expected,
            .mask = mask,
        };
    }

    // === Testbench config ===

    pub struct TbConfig {
        name : &str,
        dut_name : &str,
        timescale : &str,
        max_cycles : u32,
        timeout_ns : u32,
        fail_fast : bool,
    }

    fn tb_config(dut: &str, max_cycles: u32) -> TbConfig {
        return TbConfig{
            .name = "tb",
            .dut_name = dut,
            .timescale = "1ns/1ps",
            .max_cycles = max_cycles,
            .timeout_ns = max_cycles * 10,
            .fail_fast = true,
        };
    }

    // === Validation ===

    fn validate_tb_config(cfg: TbConfig) -> u32 {
        var errors : u32 = 0;
        if cfg.dut_name == "" {
            errors = errors + 1;
        }
        if cfg.max_cycles == 0 {
            errors = errors + 1;
        }
        return errors;
    }

    fn validate_stimulus(s: TbStimulus) -> u32 {
        var errors : u32 = 0;
        if s.signal == "" {
            errors = errors + 1;
        }
        return errors;
    }

    fn validate_check(c: TbCheck) -> u32 {
        var errors : u32 = 0;
        if c.signal == "" {
            errors = errors + 1;
        }
        return errors;
    }

    // === Query functions ===

    fn stim_applied_before(stim: TbStimulus, cycle: u32) -> bool {
        return stim.cycle <= cycle;
    }

    fn check_at_cycle(ck: TbCheck, cycle: u32) -> bool {
        return ck.cycle == cycle;
    }

    fn total_sim_ns(clock_cfg: TbClockCfg, cycles: u32) -> u32 {
        return clock_cfg.period_ns * cycles;
    }

    fn stim_count_before(stimuli: [TbStimulus], count: u32, cycle: u32) -> u32 {
        var found : u32 = 0;
        var i : u32 = 0;
        while i < count {
            if stimuli[i].cycle <= cycle {
                found = found + 1;
            }
            i = i + 1;
        }
        return found;
    }

    // === Tests ===

    test clock_cfg_creation
        given cfg = clock_cfg(10)
        then cfg.period_ns == 10
        and cfg.duty_cycle == 50
        and half_period(cfg) == 5

    test reset_cfg_creation
        given cfg = reset_cfg(5, 10)
        then cfg.active_low == true
        and cfg.delay_cycles == 5
        and cfg.duration_cycles == 10
        and reset_end_cycle(cfg) == 15

    test stimulus_creation
        given s = stimulus(10, "uart_tx", 1)
        then s.cycle == 10
        and s.signal == "uart_tx"
        and s.value == 1

    test check_creation
        given c = check(20, "led", 5)
        then c.cycle == 20
        and c.signal == "led"
        and c.expected == 5
        and c.mask == 4294967295

    test check_with_mask_creation
        given c = check_with_mask(20, "data", 255, 255)
        then c.mask == 255

    test tb_config_creation
        given cfg = tb_config("uart_top", 10000)
        then cfg.dut_name == "uart_top"
        and cfg.max_cycles == 10000
        and cfg.timeout_ns == 100000

    test validate_tb_config_ok
        given cfg = tb_config("dut", 1000)
        then validate_tb_config(cfg) == 0

    test validate_tb_config_empty_dut
        given cfg = TbConfig{.name = "tb", .dut_name = "", .timescale = "1ns/1ps", .max_cycles = 1000, .timeout_ns = 10000, .fail_fast = true}
        then validate_tb_config(cfg) > 0

    test validate_stimulus_ok
        given s = stimulus(0, "clk", 1)
        then validate_stimulus(s) == 0

    test validate_stimulus_empty_signal
        given s = TbStimulus{.cycle = 0, .signal = "", .value = 0}
        then validate_stimulus(s) > 0

    test validate_check_ok
        given c = check(10, "out", 42)
        then validate_check(c) == 0

    test stim_applied_before_yes
        given s = stimulus(5, "sig", 1)
        then stim_applied_before(s, 10) == true

    test stim_applied_before_no
        given s = stimulus(15, "sig", 1)
        then stim_applied_before(s, 10) == false

    test check_at_cycle_match
        given c = check(10, "sig", 1)
        then check_at_cycle(c, 10) == true

    test check_at_cycle_no_match
        given c = check(10, "sig", 1)
        then check_at_cycle(c, 20) == false

    test total_sim_ns
        given cfg = clock_cfg(10)
        then total_sim_ns(cfg, 100) == 1000

    test stim_count_before_empty
        given stimuli = [TbStimulus]{}
        then stim_count_before(stimuli, 0, 10) == 0

    test stim_count_before_all_before
        given stimuli = [TbStimulus]{stimulus(1, "a", 1), stimulus(2, "b", 2), stimulus(3, "c", 3)}
        then stim_count_before(stimuli, 3, 10) == 3

    test stim_count_before_none_before
        given stimuli = [TbStimulus]{stimulus(15, "a", 1), stimulus(20, "b", 2)}
        then stim_count_before(stimuli, 2, 10) == 0

    test stim_count_before_some_before
        given stimuli = [TbStimulus]{stimulus(5, "a", 1), stimulus(10, "b", 2), stimulus(15, "c", 3)}
        then stim_count_before(stimuli, 3, 10) == 2

    test stim_count_before_partial_array
        given stimuli = [TbStimulus]{stimulus(1, "a", 1), stimulus(5, "b", 2), stimulus(10, "c", 3), stimulus(15, "d", 4), stimulus(20, "e", 5)}
        then stim_count_before(stimuli, 3, 10) == 3

    // === Invariants ===

    invariant half_period_not_zero
        given cfg = clock_cfg(10)
        assert half_period(cfg) > 0

    invariant reset_end_after_delay
        given cfg = reset_cfg(5, 10)
        assert reset_end_cycle(cfg) > cfg.delay_cycles

    invariant timeout_sufficient
        given cfg = tb_config("dut", 1000)
        assert cfg.timeout_ns >= cfg.max_cycles

    // === Benchmarks ===

    bench tb_gen_latency
        measure: nanoseconds for tb_config("dUT", 10000)
        target: < 50ns
}

// 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 Капстоун: проверить модуль целиком