Капстоун: проверить модуль целиком

Вы научитесь

Провести один модуль от spec до платы со всем проверочным стеком за спиной.

Попробуйте

Выберите собственный модуль и запишите его план проверки: векторы, проверки тестбенча, цели покрытия, ассерты, мутанты, приёмка; затем прогоните виджет потока от начала до конца и отметьте, где ваш план остановил бы настоящий баг.

specs/fpga/testbench/integration_tb.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/testbench/integration_tb.t27
// Full FPGA Integration Testbench
// Tests top-level connectivity: MAC + UART + SPI + Memory + Bridge
// phi^2 + 1/phi^2 = 3 | TRINITY

module Integration_Testbench {
    const CLK_PERIOD : u32 = 20;
    const SIM_TIMEOUT : u32 = 20_000_000;
    const NUM_MODULES : u32 = 5;

    var clk : bool = false;
    var rst_n : bool = false;
    var mac_busy : bool = false;
    var uart_tx_ready : bool = false;
    var spi_done : bool = false;
    var mem_ready : bool = false;
    var bridge_busy : bool = false;
    var all_modules_idle : bool = false;
    var integration_passed : bool = false;

    var test_passed : u32 = 0;
    var test_failed : u32 = 0;

    fn tick() {
        clk = false;
        clk = true;
    }

    fn reset() {
        rst_n = false;
        tick();
        tick();
        rst_n = true;
        tick();
    }

    fn check_all_idle() -> bool {
        return !mac_busy && uart_tx_ready && spi_done && mem_ready && !bridge_busy;
    }

    test test_reset_all_modules {
        reset();
        all_modules_idle = check_all_idle();
        invariant all_modules_idle == true;
    }

    test test_module_count {
        invariant NUM_MODULES == 5;
    }

    test test_mac_uart_pipeline {
        reset();
        mac_busy = true;
        tick();
        tick();
        mac_busy = false;
        uart_tx_ready = true;
        tick();
        invariant uart_tx_ready == true;
    }

    test test_spi_memory_pipeline {
        reset();
        spi_done = false;
        tick();
        tick();
        spi_done = true;
        mem_ready = true;
        tick();
        invariant mem_ready == true;
    }

    test test_full_pipeline {
        reset();
        mac_busy = true;
        tick();
        mac_busy = false;
        uart_tx_ready = true;
        tick();
        spi_done = true;
        mem_ready = true;
        bridge_busy = true;
        tick();
        bridge_busy = false;
        all_modules_idle = check_all_idle();
        invariant all_modules_idle == true;
        integration_passed = true;
    }

    test test_stress_pipeline {
        reset();
        var i : u32 = 0;
        while i < 10 {
            mac_busy = true;
            tick();
            mac_busy = false;
            uart_tx_ready = true;
            tick();
            spi_done = true;
            mem_ready = true;
            bridge_busy = true;
            tick();
            bridge_busy = false;
            i = i + 1;
        }
        all_modules_idle = check_all_idle();
        invariant all_modules_idle == true;
    }

    invariant num_modules_positive : NUM_MODULES > 0;

    test test_tick_function {
        reset();
        var initial_clk : bool = clk;
        tick();
        invariant clk == !initial_clk;
    }

    bench bench_integration_throughput {
        reset();
        var i : u32 = 0;
        while i < 50 {
            mac_busy = true;
            tick();
            mac_busy = false;
            uart_tx_ready = true;
            tick();
            i = i + 1;
        }
    }
}

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