形式验证( Formal Verifcation)是指采用数学方法分析电路行为，找出电路功能错误的静态验证方法。形式验证不需要验证激励和电路仿真，具有比仿真验证更高的完备性。形式验证可以分为两大类:等价性检查和属性检查。

等价性检查( Equivalence Checking)可验证电路在不同阶段(例如寄存器传输级设计与门级网表阶段、综合网表与布局布线网表阶段)的表征模型是否功能致。在扫描链(Scan Chain)重排、时钟树综合等过程中也可以通过等价性检查确保网表一致性。 等价性检查目前已经融入集成电路标准 设计流程中。

等价性检查通过遍历所有可能的输入，对比两个模型的功能一致性。对比时通常将电路转换为正则表达式。例如，图5-24中的两个电路具有相同的正则表达式，虽然电路结构不同，但功能是等价的。

属性检查又称模型检查( Model Checking),是通过数学搜索的方法检查电路是否满足设定的属性规范。属性检查一般以电路模型、覆盖点、断言(Asetion)和电路约束为输入，在约束环境下检查电路的所有可能状态对断言是否有效。若属性检查失败则表明找到电路的功能错误，检查工具输出不符合约束的反例。属性检查覆盖逻辑的所有可能性，需较大内存空间，限制了待验证电路的规模。