Bounded model checking

You will learn

How a bounded search explores every input up to k cycles, and what that proves.

Try it

Set a depth k and say exactly what your BMC run proves and does not; then find in the key sweep what '0 hits' took to be checkable rather than assumed.

specs/fpga/formal.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/formal.t27
// Formal Verification Specification for Trinity T27 FPGA HIR
// Defines assertion kinds, properties, and coverage points
// Generates SystemVerilog Assertions (SVA) alongside Verilog
// Uses flat arrays + count fields (parser-compatible)
// phi^2 + 1/phi^2 = 3 | TRINITY

module Formal {

    // === Assertion kind ===

    pub const AssertKind = enum(i8) {
        immediate = 0,
        concurrent = 1,
        cover = 2,
        assume = 3,
    }

    // === Assertion severity ===

    pub const AssertSeverity = enum(i8) {
        info = 0,
        warning = 1,
        error = 2,
        fatal = 3,
    }

    // === Clocking mode ===

    pub const ClockMode = enum(i8) {
        posedge = 0,
        negedge = 1,
        both_edges = 2,
    }

    // === Capacity constants ===

    pub const MAX_ASSERTIONS : u32 = 64;
    pub const MAX_COVER_POINTS : u32 = 32;
    pub const MAX_ASSUME_POINTS : u32 = 16;

    // === Formal assertion ===

    pub struct FormalAssert {
        name : &str,
        kind : i8,
        severity : i8,
        condition : &str,
        clock : &str,
        reset : &str,
        description : &str,
    }

    // === Cover point ===

pub struct CoverPoint {
    name : &str,
    condition : &str,
    clock : &str,
    description : &str,
    _dummy : u32,
}

    // === Assumption ===

pub struct FormalAssume {
    name : &str,
    condition : &str,
    clock : &str,
    description : &str,
    _dummy : u32,
}

    // === Formal verification config ===

    pub struct FormalConfig {
        name : &str,
        module_name : &str,
        clock : &str,
        reset : &str,
        clock_mode : i8,
        depth : u32,
        timeout_cycles : u32,
    }

    // === Constructor helpers ===

    fn formal_config(name: &str, module_name: &str, clock: &str, reset: &str) -> FormalConfig {
        return FormalConfig{
            .name = name,
            .module_name = module_name,
            .clock = clock,
            .reset = reset,
            .clock_mode = 0,
            .depth = 20,
            .timeout_cycles = 100,
        };
    }

    fn with_depth(cfg: FormalConfig, depth: u32) -> FormalConfig {
        var result = cfg;
        result.depth = depth;
        return result;
    }

    fn with_timeout(cfg: FormalConfig, timeout: u32) -> FormalConfig {
        var result = cfg;
        result.timeout_cycles = timeout;
        return result;
    }

    fn immediate_assert(name: &str, condition: &str, severity: i8, description: &str) -> FormalAssert {
        return FormalAssert{
            .name = name,
            .kind = 0,
            .severity = severity,
            .condition = condition,
            .clock = "",
            .reset = "",
            .description = description,
        };
    }

    fn concurrent_assert(name: &str, condition: &str, clock: &str, reset: &str, description: &str) -> FormalAssert {
        return FormalAssert{
            .name = name,
            .kind = 1,
            .severity = 2,
            .condition = condition,
            .clock = clock,
            .reset = reset,
            .description = description,
        };
    }

    fn cover_point(name: &str, condition: &str, clock: &str, description: &str) -> CoverPoint {
        return CoverPoint{
            .name = name,
            .condition = condition,
            .clock = clock,
            .description = description,
        };
    }

    fn assume(name: &str, condition: &str, clock: &str, description: &str) -> FormalAssume {
        return FormalAssume{
            .name = name,
            .condition = condition,
            .clock = clock,
            .description = description,
        };
    }

    // === Query functions ===

    fn is_immediate(a: FormalAssert) -> bool {
        return a.kind == 0;
    }

    fn is_concurrent(a: FormalAssert) -> bool {
        return a.kind == 1;
    }

    fn is_cover(a: FormalAssert) -> bool {
        return a.kind == 2;
    }

    fn is_assume(a: FormalAssert) -> bool {
        return a.kind == 3;
    }

    fn severity_str(sev: i8) -> &str {
        return "error";
    }

    fn clock_mode_str(mode: i8) -> &str {
        return "posedge";
    }

    fn is_posedge(cfg: FormalConfig) -> bool {
        return cfg.clock_mode == 0;
    }

    // === Validation ===

    fn validate_assertion(a: FormalAssert) -> u32 {
        var errors : u32 = 0;
        if (a.name == "") {
            errors = errors + 1;
        }
        if (a.condition == "") {
            errors = errors + 1;
        }
        if (a.kind == 1 and a.clock == "") {
            errors = errors + 1;
        }
        return errors;
    }

    fn validate_cover(c: CoverPoint) -> u32 {
        var errors : u32 = 0;
        if (c.name == "") {
            errors = errors + 1;
        }
        if (c.condition == "") {
            errors = errors + 1;
        }
        return errors;
    }

    fn validate_assume(a: FormalAssume) -> u32 {
        var errors : u32 = 0;
        if (a.name == "") {
            errors = errors + 1;
        }
        if (a.condition == "") {
            errors = errors + 1;
        }
        return errors;
    }

    fn validate_config(cfg: FormalConfig) -> u32 {
        var errors : u32 = 0;
        if (cfg.name == "") {
            errors = errors + 1;
        }
        if (cfg.module_name == "") {
            errors = errors + 1;
        }
        if (cfg.clock == "") {
            errors = errors + 1;
        }
        if (cfg.depth == 0) {
            errors = errors + 1;
        }
        if (cfg.timeout_cycles == 0) {
            errors = errors + 1;
        }
        return errors;
    }

    // === Tests ===

    test immediate_assert_creation
        given a = immediate_assert("no_overflow", "count < MAX", 2, "counter never overflows")
        then is_immediate(a) == true
        and is_concurrent(a) == false
        and a.condition == "count < MAX"

    test concurrent_assert_creation
        given a = concurrent_assert("handshake", "valid ##1 ready", "clk", "rst_n", "valid followed by ready")
        then is_concurrent(a) == true
        and is_immediate(a) == false
        and a.clock == "clk"

    test cover_point_creation
        given c = cover_point("all_states", "state == S0 || state == S1", "clk", "cover all states")
        then c.name == "all_states"
        and c.condition != ""

    test assume_creation
        given a = assume("stable_reset", "(!$isunknown(rst_n))", "clk", "reset is never X")
        then a.name == "stable_reset"
        and a.condition != ""

    test formal_config_creation
        given cfg = formal_config("uart_props", "UART_TX", "clk", "rst_n")
        then cfg.name == "uart_props"
        and cfg.module_name == "UART_TX"
        and cfg.clock == "clk"
        and cfg.reset == "rst_n"
        and is_posedge(cfg) == true

    test with_depth
        given cfg = formal_config("f", "M", "clk", "rst_n")
        and cfg2 = with_depth(cfg, 50)
        then cfg2.depth == 50

    test with_timeout
        given cfg = formal_config("f", "M", "clk", "rst_n")
        and cfg2 = with_timeout(cfg, 500)
        then cfg2.timeout_cycles == 500

    test validate_assertion_ok
        given a = immediate_assert("ok", "x > 0", 2, "desc")
        then validate_assertion(a) == 0

    test validate_assertion_empty_name
        given a = immediate_assert("", "x > 0", 2, "desc")
        then validate_assertion(a) > 0

    test validate_assertion_empty_condition
        given a = immediate_assert("a", "", 2, "desc")
        then validate_assertion(a) > 0

    test validate_concurrent_no_clock
        given a = concurrent_assert("a", "x ##1 y", "", "rst_n", "desc")
        then validate_assertion(a) > 0

    test validate_cover_ok
        given c = cover_point("cp", "x", "clk", "desc")
        then validate_cover(c) == 0

    test validate_cover_empty_name
        given c = cover_point("", "x", "clk", "desc")
        then validate_cover(c) > 0

    test validate_assume_ok
        given a = assume("a", "x", "clk", "desc")
        then validate_assume(a) == 0

    test validate_assume_empty
        given a = assume("", "", "clk", "desc")
        then validate_assume(a) > 0

    test validate_config_ok
        given cfg = formal_config("f", "M", "clk", "rst_n")
        then validate_config(cfg) == 0

    test validate_config_empty_name
        given cfg = formal_config("", "M", "clk", "rst_n")
        then validate_config(cfg) > 0

    test validate_config_empty_clock
        given cfg = formal_config("f", "M", "", "rst_n")
        then validate_config(cfg) > 0

    // === Invariants ===

    invariant depth_positive
        given cfg = formal_config("inv", "M", "clk", "rst_n")
        assert cfg.depth > 0

    invariant timeout_positive
        given cfg = formal_config("inv", "M", "clk", "rst_n")
        assert cfg.timeout_cycles > 0

    invariant validate_non_negative
        given a = immediate_assert("inv", "x", 2, "d")
        assert validate_assertion(a) >= 0

    invariant config_validate_non_negative
        given cfg = formal_config("inv", "M", "clk", "rst_n")
        assert validate_config(cfg) >= 0

    // === Benchmarks ===

    bench validate_latency
        measure: nanoseconds to validate_assertion(immediate_assert("b", "x > 0", 2, "d"))
        target: < 100ns
}

// 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