5.1.2 形式验证（Formal Verification）

文档摘要

5.1.2 形式验证（Formal Verification）形式验证，不是“用更高级的测试覆盖更多路径”，也不是“把仿真跑得更久一点”。它是一场与数学的深度对话——我们不再问“这个电路在一万次随机激励下有没有出错”，而是斩钉截铁地断言：“在所有可能的输入序列、所有合法的初始状态下，该电路绝不可能进入非法状态，且必然满足时序约束下的安全属性与活性属性。”这句话背后，没有概率，没有采样偏差，没有侥幸；它立于逻辑公理之上，由机器自动推演，可被独立验证，其结论具有与“1+1=2”同等强度的数学确定性。这便是形式验证（Formal Verification）的锋芒所在——它不模拟行为，而证明行为；不依赖经验，而诉诸演绎；不寻求反例，而穷尽空间。