形式等效性检查

形式等效性检查（英语：formal equivalence checking）是电子设计自动化的一个步骤。

简介通常是在集成电路设计中，通过一些数学方法（如二元决策图、布尔可满足性问题），来对不同电路之间进行形式验证，比较它们在行为上是否等效。1

形式验证在计算机硬件（特别是集成电路）和软件系统的设计过程中，形式验证的含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。

软件测试无法证明系统不存在缺陷，也不能证明它匹配一定的属性。只有形式化验证过程可以证明一个系统不存在某个缺陷或匹配某个或某些属性。系统无法被证明或测试为无缺陷，这是因为不可能形式地规定什么是“没有缺陷”。所有可以做的，就是证明一个系统没有任何可以想到的缺陷，并且满足所有的使系统匹配功能要求的和有用的属性。

在集成电路设计中，形式验证是一种集成电路设计的验证方法，它的主要思想是通过使用形式证明的方式来验证一个设计的功能是否正确。形式验证可以分为三大类：等价性检查（Equivalence Checking）、形式模型检查（Formal Model Checking，也被称作特性检查）和定理证明（Theory Prover）。

等价性检查的验证用于验证寄存器传输级设计与门级网表之间、门级网表与门级网表之间是否一致。在进行扫描链重排、时钟树综合等过程中，都可以用等价性检查保证网表的一致性。等价性检查已经融入集成电路标准设计流程中。等价性检查在检查ECO时非常有用。例如，设计者在修改门级网表时，由于手误，错将一个或门写成或非门，等价性检查工具通过比较寄存器传输级设计与门级网表，可以很容易地发现这种错误。

模型检查用时态逻辑来描述规范，通过有效的搜索方法来检查给定的系统是否满足规范。模型检查是目前研究的热点，但其验证的电路规模受限制这一问题还没有得到很好的解决。

定理证明把系统与规范都表示成数学逻辑公式，从公理出发寻求描述。定理证明验证的电路模型不受限制，但需要用户的人工干预和较多的背景知识。2

电子设计自动化电子设计自动化（英语：Electronic design automation，缩写：EDA）是指利用计算机辅助设计（CAD）软件，来完成超大规模集成电路（VLSI）芯片的功能设计、综合、验证、物理设计（包括布局、布线、版图、设计规则检查等）等流程的设计方式。

现今数字电路非常模组化（参见集成电路设计、设计收敛、设计流程 (EDA)），产线最前端将设计流程标准化，把设计流程区分为许多“细胞”（cells），而暂不考虑技术，接着细胞则以特定的集成电路技术实现逻辑或其他电子功能。制造商通常会提供组件库（libraries of components），以及符合标准模拟工具的模拟模型给生产流程。模拟 EDA 工具较不模组化，因为它需要更多的功能，零件间需要更多的互动，而零件一般说较不理想。

在电子产业中，由于半导体产业的规模日益扩大，EDA 扮演越来越重要的角色。使用这项技术的厂商多是从事半导体器件制造的代工制造商，以及使用 EDA 模拟软件以评估生产情况的设计服务公司。EDA 工具也应用在现场可编程逻辑门阵列的程序设计上。1

本词条内容贡献者为:

王沛 - 副教授、副研究员 - 中国科学院工程热物理研究所