t27.aiEnglish

Индукция

Вы научитесь

Почему ограниченность — не доказательство и как индукция закрывает разрыв — или честно сообщает, что не может.

Ограниченность значит ограниченность: k проверенных тактов — это всё, что k доказывает. Чтобы закрыть разрыв, нужна индукция — предположить, что инвариант держался до такта k, и показать, что он держится на такте k+1, — и индукция честна так, как ограниченный перебор не бывает: она может не получиться, и неуспех индукции — находка, а не конфуз. Виджет показывает, как выглядит непогашенное обязательство, на которое никто не смотрит: 12 файлов Lean, 15,553 строки и 4 sorry, до которых не добирается ни один корень сборки — ничто их не компилирует, значит доказательства в них никогда не проверялись. Обязательство, до которого не добирается ни один корень, не погашено — оно припарковано.

Попробуйте

Найдите 4 sorry в прогоне по Lean и скажите, что изменил бы корень сборки, который до них добирается; затем назовите инвариант uart_tb, который попробовали бы доказать индукцией.

Открыть интерактивный урок →

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);
    }
}

Открыть spec урока в плеере ↗

Все уроки