Capstone: verify a module whole

You will learn

Carry one module from spec to board with the whole verification stack behind it.

Try it

Choose a module of your own and write its verification plan: vectors, tb checks, coverage targets, assertions, mutants, sign-off; then run the flow widget end to end and mark where your plan would have stopped a real bug.

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;
        }
    }
}

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