形式验证工具对系统功能的设计

形式验证工具（Formal Verification Tool）是通过数学逻辑的算法来判断硬件设计的功能是否正确，通常有等价性检查（Equivalence Checking）和属性检查（Property Checking）两种方法。

等价性检查用来检查两个数字集成电路设计之间的逻辑等价性。在集成电路设计过程中许多步骤都可能做逻辑修改，例如插入可测性设计逻辑、时钟树综、工程变更单等，如果用仿真验证会耗费大量时间而且难以保证验证的覆盖率。等价性检查时通过静态和数学逻辑的算法来比较修改前后逻辑的一致性，理论上可实现全覆盖验证。

对于给定的两个网表（可以称为原始网表和修订网表），假设两个网表的输入信号、输出信号，以及网表中的输入信号、输出信号和网表中的寄存器配对，产生多对组合逻辑锥（Combinational Logic Cones）;然后再用二元决策图（Binary Decision Diagram）、合取范式的可满足性求解器（SAT So lver）等算法，对每一对组合逻辑锥进行比较。如果每一对里两个逻辑锥的布尔函数都是等价的，就能断定两个网表的静态和时序逻辑功能是相同的。等价性检查验证示意图如图5-112所示。

当原始网表和修订网表的寄存器个数不相同时 ，上述的算法通常会发现有些配对的组合逻辑锥里的两个布尔函数是不等价的。这时就必须用一些检测时序逻辑等效性（Sequential Equivalence Checking）的算法做进一步分析，从而判定两个网表的逻辑功能是否相同。

属性检查时一种分析电路设计是否满足某些给定规范或断言（Assertion）的方法。首先用逻辑结构和形式化逻辑描述系统模型和待验证的属性，如时序逻辑结构、有限状态机和形式逻辑公式等，再通过形式验证的算法来检测设计是否满足该属性。属性检查技术又可以分为定理证明（Theorem Proving）和模型检查（Model Checking）。

定理证明是将设计和待验证的属性用某种形式化逻辑系统的公式表示出来，再根据该系统的公理、推理规则以及已经证明的定理，推导出表达系统属性的公式，从而证明设计满足该属性。这种推导的过程通常需要人工参与，并要对系统功能设计有相当程度的了解。

模型检查是用时序逻辑结构或有限状态机表示待检验的设计。首先用某种时态逻辑表示设计应该具有的属性，再通过二元决策图、合取范式可满足性求解、自动测试生成（ATPG）等技术搜寻设计的状态空间，检测是否在所有可能的状态下设计都满足这些属性。如果检测出设计不满足某种属性时，也能给出反例，方便错误的定位。模型检查算法通常不需要人工参与，但如果设计可能存在的状态空间太大时，会遭遇所谓的状态爆炸（State Explosin）问题，导致无法在有限的时间内得到最终的结果。

由于工艺的不断演进，等价性检查和属性检查的技术必须不断地改进才能处理越来越大的设计规模。

审核编辑：彭静