Directed versus random
You will learn
When one carefully chosen case beats a thousand random ones, and when it does not.
A directed test is one case you chose because you know it bites: the empty FIFO, the full one, the wrap. A random one is cheap volume. They are not rivals; they are a sequence. The widget is the knockout experiment turned into a tool: three performance bits were claimed, and one knockout bitstream per bit -- the same design with that bit tied off -- proves each one matters. That is directed testing's whole argument: one bit, one prediction, one bitstream, measured.
Try it
Pick one performance bit in the knockout widget and say what the no-knockout run would have to show for the bit to be a lie.
The A/B bitstreams differ in three bits. Each knockout clears one: 3 bytes from the working .bit.
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
}
All lessons
Module 1 · Why verify
Designs that compile and are wrong, the model that decides, and the plan written before the code.
Module 2 · Testbenches
Stimulus, checks and a verdict, written as one spec beside the design it judges.
Module 3 · Waveforms
A trace of every signal, read the way a hardware engineer reads it, and two runs compared.
Module 4 · Conformance vectors
Cases with the answer written beside them, kept where the compiler can reach them.
Module 5 · Cosimulation
Spec, simulator and board agreeing on the bench Artix-7 XC7A200T, and what to do when they do not.
Module 6 · Coverage
What the tests touched: lines, toggles, states, and what that number hides.
Module 7 · Formal
Assertions that hold every cycle, bounded search for a counterexample, and why a proof needs induction.
Module 8 · Mutation
Break the design on purpose and count what the tests catch.
Module 9 · Sign-off
One command, every receipt, a clean verdict you can show.