The golden model

You will learn

What a reference model is, and how a conformance suite holds a tool to it.

Try it

Open tri-fpga-specs and read one conformance spec's test blocks; then open testbench.t27 and name the four shapes a tb must have.

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

Open the lesson's spec in the player ↗

All lessons

• Module 1 · Why verify

  Designs that compile and are wrong, the model that decides, and the plan written before the code.

  1. 01 Bugs that compile
  2. 02 The golden model
  3. 03 Plan before code

• Module 2 · Testbenches

  Stimulus, checks and a verdict, written as one spec beside the design it judges.

  1. 04 Anatomy of a testbench
  2. 05 Self-checking, not staring
  3. 06 Directed versus random

• Module 3 · Waveforms

  A trace of every signal, read the way a hardware engineer reads it, and two runs compared.

  1. 07 The VCD format
  2. 08 Debug with waves
  3. 09 Compare two traces

• Module 4 · Conformance vectors

  Cases with the answer written beside them, kept where the compiler can reach them.

  1. 10 What a vector is
  2. 11 Golden ruler vectors
  3. 12 End-to-end scenarios

• Module 5 · Cosimulation

  Spec, simulator and board agreeing on the bench Artix-7 XC7A200T, and what to do when they do not.

  1. 13 Three-way agreement
  2. 14 Inside the simulator
  3. 15 When they disagree

• Module 6 · Coverage

  What the tests touched: lines, toggles, states, and what that number hides.

  1. 16 Line and toggle
  2. 17 FSM coverage
  3. 18 Coverage lies

• Module 7 · Formal

  Assertions that hold every cycle, bounded search for a counterexample, and why a proof needs induction.

  1. 19 Assertions
  2. 20 Bounded model checking
  3. 21 Induction

• Module 8 · Mutation

  Break the design on purpose and count what the tests catch.

  1. 22 Kill the mutant
  2. 23 Surviving mutants
  3. 24 Test strength

• Module 9 · Sign-off

  One command, every receipt, a clean verdict you can show.

  1. 25 Build and verify
  2. 26 The board self-tests
  3. 27 Capstone: verify a module whole