Ассерты

Вы научитесь

Что такое ассерт в коде и сколько стоит проверять его каждый такт.

Попробуйте

Запишите один немедленный и один параллельный ассерт для FIFO с названными тактом и сбросом; затем посмотрите в виджете зависимостей, что сам tri предполагает имеющимся.

specs/fpga/formal.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/formal.t27
// Formal Verification Specification for Trinity T27 FPGA HIR
// Defines assertion kinds, properties, and coverage points
// Generates SystemVerilog Assertions (SVA) alongside Verilog
// Uses flat arrays + count fields (parser-compatible)
// phi^2 + 1/phi^2 = 3 | TRINITY

module Formal {

    // === Assertion kind ===

    pub const AssertKind = enum(i8) {
        immediate = 0,
        concurrent = 1,
        cover = 2,
        assume = 3,
    }

    // === Assertion severity ===

    pub const AssertSeverity = enum(i8) {
        info = 0,
        warning = 1,
        error = 2,
        fatal = 3,
    }

    // === Clocking mode ===

    pub const ClockMode = enum(i8) {
        posedge = 0,
        negedge = 1,
        both_edges = 2,
    }

    // === Capacity constants ===

    pub const MAX_ASSERTIONS : u32 = 64;
    pub const MAX_COVER_POINTS : u32 = 32;
    pub const MAX_ASSUME_POINTS : u32 = 16;

    // === Formal assertion ===

    pub struct FormalAssert {
        name : &str,
        kind : i8,
        severity : i8,
        condition : &str,
        clock : &str,
        reset : &str,
        description : &str,
    }

    // === Cover point ===

pub struct CoverPoint {
    name : &str,
    condition : &str,
    clock : &str,
    description : &str,
    _dummy : u32,
}

    // === Assumption ===

pub struct FormalAssume {
    name : &str,
    condition : &str,
    clock : &str,
    description : &str,
    _dummy : u32,
}

    // === Formal verification config ===

    pub struct FormalConfig {
        name : &str,
        module_name : &str,
        clock : &str,
        reset : &str,
        clock_mode : i8,
        depth : u32,
        timeout_cycles : u32,
    }

    // === Constructor helpers ===

    fn formal_config(name: &str, module_name: &str, clock: &str, reset: &str) -> FormalConfig {
        return FormalConfig{
            .name = name,
            .module_name = module_name,
            .clock = clock,
            .reset = reset,
            .clock_mode = 0,
            .depth = 20,
            .timeout_cycles = 100,
        };
    }

    fn with_depth(cfg: FormalConfig, depth: u32) -> FormalConfig {
        var result = cfg;
        result.depth = depth;
        return result;
    }

    fn with_timeout(cfg: FormalConfig, timeout: u32) -> FormalConfig {
        var result = cfg;
        result.timeout_cycles = timeout;
        return result;
    }

    fn immediate_assert(name: &str, condition: &str, severity: i8, description: &str) -> FormalAssert {
        return FormalAssert{
            .name = name,
            .kind = 0,
            .severity = severity,
            .condition = condition,
            .clock = "",
            .reset = "",
            .description = description,
        };
    }

    fn concurrent_assert(name: &str, condition: &str, clock: &str, reset: &str, description: &str) -> FormalAssert {
        return FormalAssert{
            .name = name,
            .kind = 1,
            .severity = 2,
            .condition = condition,
            .clock = clock,
            .reset = reset,
            .description = description,
        };
    }

    fn cover_point(name: &str, condition: &str, clock: &str, description: &str) -> CoverPoint {
        return CoverPoint{
            .name = name,
            .condition = condition,
            .clock = clock,
            .description = description,
        };
    }

    fn assume(name: &str, condition: &str, clock: &str, description: &str) -> FormalAssume {
        return FormalAssume{
            .name = name,
            .condition = condition,
            .clock = clock,
            .description = description,
        };
    }

    // === Query functions ===

    fn is_immediate(a: FormalAssert) -> bool {
        return a.kind == 0;
    }

    fn is_concurrent(a: FormalAssert) -> bool {
        return a.kind == 1;
    }

    fn is_cover(a: FormalAssert) -> bool {
        return a.kind == 2;
    }

    fn is_assume(a: FormalAssert) -> bool {
        return a.kind == 3;
    }

    fn severity_str(sev: i8) -> &str {
        return "error";
    }

    fn clock_mode_str(mode: i8) -> &str {
        return "posedge";
    }

    fn is_posedge(cfg: FormalConfig) -> bool {
        return cfg.clock_mode == 0;
    }

    // === Validation ===

    fn validate_assertion(a: FormalAssert) -> u32 {
        var errors : u32 = 0;
        if (a.name == "") {
            errors = errors + 1;
        }
        if (a.condition == "") {
            errors = errors + 1;
        }
        if (a.kind == 1 and a.clock == "") {
            errors = errors + 1;
        }
        return errors;
    }

    fn validate_cover(c: CoverPoint) -> u32 {
        var errors : u32 = 0;
        if (c.name == "") {
            errors = errors + 1;
        }
        if (c.condition == "") {
            errors = errors + 1;
        }
        return errors;
    }

    fn validate_assume(a: FormalAssume) -> u32 {
        var errors : u32 = 0;
        if (a.name == "") {
            errors = errors + 1;
        }
        if (a.condition == "") {
            errors = errors + 1;
        }
        return errors;
    }

    fn validate_config(cfg: FormalConfig) -> u32 {
        var errors : u32 = 0;
        if (cfg.name == "") {
            errors = errors + 1;
        }
        if (cfg.module_name == "") {
            errors = errors + 1;
        }
        if (cfg.clock == "") {
            errors = errors + 1;
        }
        if (cfg.depth == 0) {
            errors = errors + 1;
        }
        if (cfg.timeout_cycles == 0) {
            errors = errors + 1;
        }
        return errors;
    }

    // === Tests ===

    test immediate_assert_creation
        given a = immediate_assert("no_overflow", "count < MAX", 2, "counter never overflows")
        then is_immediate(a) == true
        and is_concurrent(a) == false
        and a.condition == "count < MAX"

    test concurrent_assert_creation
        given a = concurrent_assert("handshake", "valid ##1 ready", "clk", "rst_n", "valid followed by ready")
        then is_concurrent(a) == true
        and is_immediate(a) == false
        and a.clock == "clk"

    test cover_point_creation
        given c = cover_point("all_states", "state == S0 || state == S1", "clk", "cover all states")
        then c.name == "all_states"
        and c.condition != ""

    test assume_creation
        given a = assume("stable_reset", "(!$isunknown(rst_n))", "clk", "reset is never X")
        then a.name == "stable_reset"
        and a.condition != ""

    test formal_config_creation
        given cfg = formal_config("uart_props", "UART_TX", "clk", "rst_n")
        then cfg.name == "uart_props"
        and cfg.module_name == "UART_TX"
        and cfg.clock == "clk"
        and cfg.reset == "rst_n"
        and is_posedge(cfg) == true

    test with_depth
        given cfg = formal_config("f", "M", "clk", "rst_n")
        and cfg2 = with_depth(cfg, 50)
        then cfg2.depth == 50

    test with_timeout
        given cfg = formal_config("f", "M", "clk", "rst_n")
        and cfg2 = with_timeout(cfg, 500)
        then cfg2.timeout_cycles == 500

    test validate_assertion_ok
        given a = immediate_assert("ok", "x > 0", 2, "desc")
        then validate_assertion(a) == 0

    test validate_assertion_empty_name
        given a = immediate_assert("", "x > 0", 2, "desc")
        then validate_assertion(a) > 0

    test validate_assertion_empty_condition
        given a = immediate_assert("a", "", 2, "desc")
        then validate_assertion(a) > 0

    test validate_concurrent_no_clock
        given a = concurrent_assert("a", "x ##1 y", "", "rst_n", "desc")
        then validate_assertion(a) > 0

    test validate_cover_ok
        given c = cover_point("cp", "x", "clk", "desc")
        then validate_cover(c) == 0

    test validate_cover_empty_name
        given c = cover_point("", "x", "clk", "desc")
        then validate_cover(c) > 0

    test validate_assume_ok
        given a = assume("a", "x", "clk", "desc")
        then validate_assume(a) == 0

    test validate_assume_empty
        given a = assume("", "", "clk", "desc")
        then validate_assume(a) > 0

    test validate_config_ok
        given cfg = formal_config("f", "M", "clk", "rst_n")
        then validate_config(cfg) == 0

    test validate_config_empty_name
        given cfg = formal_config("", "M", "clk", "rst_n")
        then validate_config(cfg) > 0

    test validate_config_empty_clock
        given cfg = formal_config("f", "M", "", "rst_n")
        then validate_config(cfg) > 0

    // === Invariants ===

    invariant depth_positive
        given cfg = formal_config("inv", "M", "clk", "rst_n")
        assert cfg.depth > 0

    invariant timeout_positive
        given cfg = formal_config("inv", "M", "clk", "rst_n")
        assert cfg.timeout_cycles > 0

    invariant validate_non_negative
        given a = immediate_assert("inv", "x", 2, "d")
        assert validate_assertion(a) >= 0

    invariant config_validate_non_negative
        given cfg = formal_config("inv", "M", "clk", "rst_n")
        assert validate_config(cfg) >= 0

    // === Benchmarks ===

    bench validate_latency
        measure: nanoseconds to validate_assertion(immediate_assert("b", "x > 0", 2, "d"))
        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 Капстоун: проверить модуль целиком