Build and verify

You will learn

How one command re-runs every sweep and turns a build into a verdict.

Try it

Run the audit and find the one count with the largest denominator; then read build_verify and mark which checks are re-derived, not remembered.

specs/fpga/verification/build_verify.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/verification/build_verify.t27
// FPGA Build Verification Spec
// Validates all FPGA specs can generate Verilog and pass structural checks
// phi^2 + 1/phi^2 = 3 | TRINITY

module BuildVerify {
    const TOTAL_FPGA_MODULES : u32 = 33;
    const TOTAL_TESTBENCHES : u32 = 30;
    const TOTAL_BOARD_CONFIGS : u32 = 3;
    const TOTAL_SPECS : u32 = 66;
    const NUM_BACKENDS : u32 = 4;
    const VERILOG_FILES : u32 = 66;

    struct ModuleReport {
        name : str;
        verilog_lines : u32;
        has_tests : bool;
        has_invariants : bool;
        has_bench : bool;
    }

    struct BuildResult {
        total_specs : u32;
        parse_ok : u32;
        typecheck_ok : u32;
        gen_zig_ok : u32;
        gen_verilog_ok : u32;
        gen_c_ok : u32;
        gen_rust_ok : u32;
        seal_ok : u32;
        failures : u32;
    }

    fn check_build_clean(result : BuildResult) -> bool {
        return result.failures == 0;
    }

    fn coverage_percent(ok : u32, total : u32) -> u32 {
        if total == 0 { return 0; }
        return (ok * 100) / total;
    }

    test test_module_count {
        invariant TOTAL_FPGA_MODULES == 31;
    }

    test test_testbench_count {
        invariant TOTAL_TESTBENCHES == 30;
    }

    test test_board_count {
        invariant TOTAL_BOARD_CONFIGS == 3;
    }

    test test_total_specs {
        invariant TOTAL_SPECS == TOTAL_FPGA_MODULES + TOTAL_TESTBENCHES + TOTAL_BOARD_CONFIGS;
    }

    test test_backend_count {
        invariant NUM_BACKENDS == 4;
    }

    test test_verilog_file_count {
        invariant VERILOG_FILES == TOTAL_SPECS;
    }

    test test_coverage_100 {
        var cov : u32 = coverage_percent(66, 66);
        invariant cov == 100;
    }

    test test_coverage_0 {
        var cov : u32 = coverage_percent(0, 66);
        invariant cov == 0;
    }

    test test_coverage_50 {
        var cov : u32 = coverage_percent(23, 46);
        invariant cov == 50;
    }

    test test_check_build_clean_success {
        var result : BuildResult = BuildResult {
            total_specs: 66,
            parse_ok: 66,
            typecheck_ok: 66,
            gen_zig_ok: 66,
            gen_verilog_ok: 66,
            gen_c_ok: 66,
            gen_rust_ok: 66,
            seal_ok: 66,
            failures: 0
        };
        invariant check_build_clean(result) == true;
    }

    test test_check_build_clean_failure {
        var result : BuildResult = BuildResult {
            total_specs: 66,
            parse_ok: 65,
            typecheck_ok: 66,
            gen_zig_ok: 66,
            gen_verilog_ok: 66,
            gen_c_ok: 66,
            gen_rust_ok: 66,
            seal_ok: 66,
            failures: 1
        };
        invariant check_build_clean(result) == false;
    }

    invariant total_specs_positive : TOTAL_SPECS > 0;
    invariant no_backend_gaps : NUM_BACKENDS == 4;
    invariant all_backends_equal : VERILOG_FILES == TOTAL_SPECS;
}

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