3.3 形式验证（Formal Verification）

文档摘要

3.3 形式验证（Formal Verification） 3.3 形式验证（Formal Verification）：逻辑综合之后的确定性守门人在电子设计自动化（EDA）的宏大图景中，逻辑综合（Logic Synthesis）绝非终点——它是一次精密的“翻译”：将行为级或寄存器传输级（RTL）的抽象意图，映射为满足时序、面积与功耗约束的门级网表。然而，当综合工具输出一张由数百万个与非门、多路选择器和触发器构成的网表时，一个根本性问题如影随形：这张网表，是否真的忠实地实现了原始规格？它是否在每一个可能的输入序列、每一种状态转移路径、每一种边界条件组合下，都与参考模型保持语义一致？它是否隐含着未被测试激励覆盖的死锁、竞争冒险或状态爆炸漏洞？这些问题，无法靠仿真穷举回答；