t27.aiРусский

Induction

You will learn

Why bounded is not a proof, and how induction closes the gap -- or reports it cannot.

Bounded means bounded: k cycles checked is all k proves. To close the gap you need induction -- assume the invariant held up to cycle k, show it holds at k+1 -- and induction is honest in a way BMC is not: it can fail, and a failed induction is a finding, not an embarrassment. The widget is what an un-discharged obligation looks like when nobody looks: 12 Lean files, 15,553 lines and 4 sorry, reached by no build root -- nothing compiles them, so the proofs they contain have never been checked. An obligation no root reaches is not discharged; it is parked.

Try it

Find the 4 sorry in the Lean sweep and say what a build root that reached them would change; then name one invariant of uart_tb you would try to induct.

Open the interactive lesson →

tri lean: proofs that nothing compiles
tri lean: proofs that nothing compiles ↗

12 Lean files, 15,553 lines and 4 sorry, are reached by no build root: nothing compiles them.

specs/fpga/testbench/formal_tb.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/fpga/testbench/formal_tb.t27
// Formal Verification Testbench
// Tests SVA assertion generation, cover points, and proof properties
// phi^2 + 1/phi^2 = 3 | TRINITY

module Formal_Testbench {
    use fpga::formal::Formal;

    const CLK_PERIOD : u32 = 20;
    const SIM_TIMEOUT : u32 = 10_000_000;
    const NUM_ASSERTIONS : u32 = 64;
    const NUM_COVER_POINTS : u32 = 32;
    const NUM_ASSUME_POINTS : u32 = 16;

    var clk : bool = false;
    var rst_n : bool = false;
    var assert_fired : bool = false;
    var cover_hit : bool = false;
    var proof_passed : bool = false;
    var proof_depth : u32 = 0;

    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_immediate(condition : bool, name : str) -> bool {
        if !condition {
            return false;
        }
        return true;
    }

    fn check_concurrent(pre : bool, post : bool) -> bool {
        tick();
        if pre && !post {
            return false;
        }
        return true;
    }

    fn cover_point(condition : bool) -> bool {
        if condition {
            cover_hit = true;
        }
        return cover_hit;
    }

    fn run_proof(depth : u32) -> bool {
        var i : u32 = 0;
        proof_passed = true;
        while i < depth {
            tick();
            proof_depth = i;
            i = i + 1;
        }
        return proof_passed;
    }

    test test_reset_clears_asserts {
        reset();
        invariant assert_fired == false;
        invariant cover_hit == false;
        invariant proof_passed == false;
    }

    test test_immediate_assert_pass {
        var ok : bool = check_immediate(true, "test_assert");
        invariant ok == true;
    }

    test test_immediate_assert_fail {
        var ok : bool = check_immediate(false, "test_assert");
        invariant ok == false;
    }

    test test_concurrent_assert {
        var ok : bool = check_concurrent(true, true);
        invariant ok == true;
    }

    test test_cover_point_hit {
        cover_hit = false;
        var hit : bool = cover_point(true);
        invariant hit == true;
    }

    test test_cover_point_miss {
        cover_hit = false;
        var hit : bool = cover_point(false);
        invariant hit == false;
    }

    test test_proof_depth {
        var ok : bool = run_proof(100);
        invariant ok == true;
        invariant proof_depth == 99;
    }

    test test_proof_zero_depth {
        var ok : bool = run_proof(0);
        invariant ok == true;
        invariant proof_depth == 0;
    }

    test test_assertion_capacity {
        invariant NUM_ASSERTIONS == 64;
        invariant NUM_COVER_POINTS == 32;
        invariant NUM_ASSUME_POINTS == 16;
    }

    invariant num_assertions_positive : NUM_ASSERTIONS > 0;
    invariant num_cover_positive : NUM_COVER_POINTS > 0;

    test test_tick_function {
        clk = false;
        tick();
        invariant clk == true;
    }

    bench bench_formal_proof {
        reset();
        run_proof(1000);
    }
}

Open the lesson's spec in the player ↗

All lessons