Bugs that compile

You will learn

Why a clean compile proves so little, and what a seal without output is worth.

Try it

Open the seal sweep and find the 16 specs with no output; then open uart_tb in the player and say out loud what a compile of it does not prove.

specs/fpga/testbench/uart_tb.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/testbench/uart_tb.t27
// UART Testbench Specification
// Tests UART TX/RX functionality, state machines, and timing
// φ² + 1/φ² = 3 | TRINITY

module UART_Testbench {
    // Import base types and UART module
    use base::types;
    use fpga::uart::UART_Bridge;

    // 1. Testbench Configuration

    // Simulation timing
    const TIMESCALE : str = "1ns/1ps";
    const CLK_PERIOD : u32 = 20;           // 50 MHz = 20ns period
    const SIM_TIMEOUT : u32 = 10_000_000;  // 10ms simulation timeout

    // Test data patterns
    const TEST_DATA_1 : u8 = 0xAA;
    const TEST_DATA_2 : u8 = 0x55;
    const TEST_DATA_3 : u8 = 0x00;
    const TEST_DATA_4 : u8 = 0xFF;

    // 2. Testbench Signals

    // Clock and reset
    var clk : bool = false;
    var rst_n : bool = false;

    // UART signals
    var uart_tx_line : bool = true;    // TX output (idle high)
    var uart_rx_line : bool = true;    // RX input

    // Internal monitoring
    var tx_busy : bool = false;
    var rx_data_valid : bool = false;
    var rx_data : u8 = 0;

    // Test counters
    var test_passed : u32 = 0;
    var test_failed : u32 = 0;
    var sim_cycle : u32 = 0;

    // 3. Clock Generation

    // generate_clock() → void
    // Generate 50 MHz clock
    fn generate_clock() -> void {
        clk = !clk;
        sim_cycle = sim_cycle + 1;
    }

    // 4. Test Helpers

    // assert_pass(condition: bool, message: str) → void
    // Record test pass
    fn assert_pass(condition: bool, message: str) -> void {
        if (condition) {
            test_passed = test_passed + 1;
        } else {
            test_failed = test_failed + 1;
        }
    }

    // wait_cycles(n: u32) → void
    // Wait n clock cycles
    fn wait_cycles(n: u32) -> void {
        var i : u32 = 0;
        while (i < n) {
            generate_clock();
            i = i + 1;
        }
    }

    // wait_tx_ready() → void
    // Wait until TX is ready
    fn wait_tx_ready() -> void {
        var timeout : u32 = 0;
        while (!uart_tx_ready() && timeout < 1000) {
            generate_clock();
            timeout = timeout + 1;
        }
    }

    // wait_rx_data() → (bool, u8)
    // Wait for RX data, return (success, data)
    fn wait_rx_data() -> (bool, u8) {
        var timeout : u32 = 0;
        while (!uart_rx_has_data() && timeout < 10000) {
            generate_clock();
            timeout = timeout + 1;
        }
        if (uart_rx_has_data()) {
            return (true, uart_rx_read_data());
        } else {
            return (false, 0);
        }
    }

    // 5. Test Cases

    // test_uart_tx_byte(data: u8) → void
    // Test single byte transmission
    fn test_uart_tx_byte(data: u8) -> void {
        // Wait for ready
        wait_tx_ready();

        // Start transmission
        const success = uart_tx_write(data);
        assert_pass(success == true, "TX write success");

        // Wait for completion
        var timeout : u32 = 0;
        while (uart_tx.tx_busy && timeout < 20000) {
            generate_clock();
            timeout = timeout + 1;
        }

        assert_pass(!uart_tx.tx_busy, "TX completed");
    }

    // test_uart_rx_byte(data: u8) → void
    // Test single byte reception
    fn test_uart_rx_byte(data: u8) -> void {
        // Simulate RX transmission
        var bit_idx : u8 = 0;

        // Start bit
        uart_rx_sync(false);
        wait_cycles(BAUD_DIVISOR / 2);

        // Data bits
        while (bit_idx < 8) {
            const bit = (data >> bit_idx) & 1 == 1;
            uart_rx_sync(bit);
            wait_cycles(BAUD_DIVISOR);
            bit_idx = bit_idx + 1;
        }

        // Stop bit
        uart_rx_sync(true);
        wait_cycles(BAUD_DIVISOR);

        // Check received data
        const (success, received) = wait_rx_data();
        assert_pass(success && received == data, "RX data match");
    }

    // test_uart_loopback() → void
    // Test TX -> RX loopback
    fn test_uart_loopback() -> void {
        const data = TEST_DATA_1;

        // Start TX
        wait_tx_ready();
        uart_tx_write(data);

        // Connect TX to RX
        var tx_count : u32 = 0;
        while (uart_tx.tx_busy && tx_count < 20000) {
            uart_rx_line = uart_tx_get_line();
            uart_rx_tick();
            uart_tx_tick();
            tx_count = tx_count + 1;
        }

        // Check RX received data
        const (success, received) = wait_rx_data();
        assert_pass(success && received == data, "Loopback data match");
    }

    // test_uart_framing_error() → void
    // Test framing error detection
    fn test_uart_framing_error() -> void {
        // Start bit
        uart_rx_sync(false);
        wait_cycles(BAUD_DIVISOR / 2);

        // Data bits
        var bit_idx : u8 = 0;
        while (bit_idx < 8) {
            uart_rx_sync(bit_idx < 4);  // Pattern
            wait_cycles(BAUD_DIVISOR);
            bit_idx = bit_idx + 1;
        }

        // Stop bit LOW (error)
        uart_rx_sync(false);
        wait_cycles(BAUD_DIVISOR);

        // Check framing error
        assert_pass(uart_rx_has_framing_error(), "Framing error detected");
    }

    // test_uart_reset() → void
    // Test UART reset
    fn test_uart_reset() -> void {
        // Start a transmission
        uart_tx_write(TEST_DATA_1);

        // Apply reset
        rst_n = false;
        wait_cycles(10);
        rst_n = true;
        wait_cycles(10);

        // Check TX is ready
        assert_pass(uart_tx_ready() && !uart_tx.tx_busy, "TX reset to ready");
        assert_pass(uart_tx_get_line() == true, "TX line idle high");
    }

    // test_uart_idle_line() → void
    // Test idle line state
    fn test_uart_idle_line() -> void {
        wait_tx_ready();
        assert_pass(uart_tx_get_line() == true, "Idle line high");
    }

    // test_uart_multiple_bytes() → void
    // Test multiple byte transmission
    fn test_uart_multiple_bytes() -> void {
        const bytes = [TEST_DATA_1, TEST_DATA_2, TEST_DATA_3, TEST_DATA_4];
        var i : usize = 0;

        while (i < bytes.len()) {
            test_uart_tx_byte(bytes[i]);
            i = i + 1;
        }

        assert_pass(i == 4, "All bytes transmitted");
    }

    // test_uart_baud_rate_timing() → void
    // Test baud rate timing
    fn test_uart_baud_rate_timing() -> void {
        const data = TEST_DATA_1;

        // Record start cycle
        const start_cycle = sim_cycle;

        // Transmit
        test_uart_tx_byte(data);

        const cycles = sim_cycle - start_cycle;
        const expected = (10 * BAUD_DIVISOR);  // 10 bits @ baud rate

        assert_pass(cycles >= expected && cycles <= expected + 100, "Baud rate timing");
    }

    // 6. Test Sequences

    // run_tests() → void
    // Run all test sequences
    fn run_tests() -> void {
        print("  t27 UART TESTBENCH");
        print("║          t27 UART TESTBENCH                              ║");
        print("  01 + 1/23 = 3 | TRINITY");
        print("║  φ² + 1/φ² = 3 | TRINITY                                 ║");
        print("  Running test sequences...");

        // Apply reset
        rst_n = false;
        wait_cycles(10);
        rst_n = true;
        wait_cycles(10);

        print("[TEST 1] UART TX byte transmission");
        test_uart_tx_byte(TEST_DATA_1);
        print("  [PASS]");

        print("[TEST 2] UART idle line");
        test_uart_idle_line();
        print("  [PASS]");

        print("[TEST 3] UART multiple bytes");
        test_uart_multiple_bytes();
        print("  [PASS]");

        print("[TEST 4] UART reset");
        test_uart_reset();
        print("  [PASS]");

        print("[TEST 5] UART baud rate timing");
        test_uart_baud_rate_timing();
        print("  [PASS]");

        print("[TEST 6] UART framing error");
        test_uart_framing_error();
        print("  [PASS]");

        print("[TEST 7] UART loopback");
        test_uart_loopback();
        print("  [PASS]");

        // Summary
        print("  Simulation complete.");
        print("║          SIMULATION RESULTS                                  ║");
        print("  Collecting results...");
        print("║  Passed: ", test_passed, "                                    ║");
        print("║  Failed: ", test_failed, "                                    ║");
        if (test_failed == 0) {
            print("║  STATUS: ✓ ALL TESTS PASSED                             ║");
        } else {
            print("║  STATUS: ✗ SOME TESTS FAILED                           ║");
        }
        print("  Done.");
    }

    // TDD-Inside-Spec: Invariants for UART_Testbench

    invariant tb_clk_period_correct
        assert CLK_PERIOD == 20  // 50MHz

    invariant tb_timescale_defined
        assert TIMESCALE == "1ns/1ps"

    invariant tb_timeout_defined
        assert SIM_TIMEOUT == 10_000_000

    invariant tb_test_data_defined
        assert TEST_DATA_1 == 0xAA and TEST_DATA_2 == 0x55

    invariant tb_baud_divisor_matches_uart
        assert BAUD_DIVISOR == 434  // 50MHz / 115200

    invariant tb_counter_bounds
        assert test_passed < 1000 and test_failed < 1000

    invariant tb_sim_cycle_increments
        given old = sim_cycle
        when generate_clock()
        then sim_cycle == old + 1

    invariant tb_wait_cycles_increments_correctly
        given old_cycle = sim_cycle
        and   wait_cycles(10)
        then sim_cycle >= old_cycle + 10

    invariant tb_initially_reset
        assert test_passed == 0 and test_failed == 0

    invariant tb_tx_line_idle_high
        given uart_tx_ready() == true
        then uart_tx_get_line() == true

    invariant tb_timeout_prevents_infinite_loop
        assert true

    test uart_tb_tx_idle_high
        given uart_tx_line = true
        then uart_tx_line == true

    test uart_tb_rx_idle_high
        given uart_rx_line = true
        then uart_rx_line == true

    test uart_tb_test_data_patterns
        given TEST_DATA_1 = 0xAA
        and   TEST_DATA_2 = 0x55
        and   TEST_DATA_3 = 0x00
        and   TEST_DATA_4 = 0xFF
        then TEST_DATA_1 != TEST_DATA_2
        then TEST_DATA_3 != TEST_DATA_4

    test uart_tb_clk_period_valid
        given CLK_PERIOD = 20
        then CLK_PERIOD > 0

    test uart_tb_sim_timeout_valid
        given SIM_TIMEOUT = 10_000_000
        then SIM_TIMEOUT > 0

    test uart_tb_counters_start_zero
        given test_passed = 0
        and   test_failed = 0
        and   sim_cycle = 0
        then test_passed == 0 and test_failed == 0

    test uart_tb_all_test_data_distinct
        given patterns = [0xAA, 0x55, 0x00, 0xFF]
        then patterns[0] != patterns[1]
        then patterns[2] != patterns[3]

    bench tb_full_simulation_time
        measure: cycles for run_tests()
        target: < 1_000_000

    bench tb_tx_byte_cycles
        measure: cycles to test_uart_tx_byte(0xAA)
        target: < 10_000

    bench tb_rx_byte_cycles
        measure: cycles to test_uart_rx_byte(0x55)
        target: < 10_000
}

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