随着现代集成电路的密度及性能要求越来越高，导致现在的IC设计愈发艰难，仿真模拟无法更好测试验证IC系统功能，这时就要用上形式验证环节，但是很多人都没听说过形式验证，所以今天讲讲怎么做好形式验证。

一般来说，用仿真方法来验证IC系统功能存在两个缺点，一是很难对一些隐蔽错误进行定位功能；二是仿真时间相对较长，尤其是随着IC系统规模的增大，这些缺陷越来越令人无法忍受，因此，形式验证是最有希望解决此问题的途径。

形式验证，大致上可分为模型检查（Model Checking）、定理证明（Theory Prover）和等价性检查三类。

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

定理证明是把系统与规范都表示成数学逻辑公式，从公理出发寻求描述。定理证明的好处是验证的电路模型是不受限制，但缺点是要求使用者的人工干预及具备较多的背景知识。

等价性检查的验证常用语验证RTL设计于门级网表、门级网表与门级网表是否一致性，等价性检查已融入IC标准设计榴城中，如图所示：

等价性检查在检查ECO时非常有用，如工程师在修改门级网表时，由于手误错将或门写成非门，等价性工具通过比较RTL设计于门级网表，很容易找出该种错误。

与前两种形式方法相比，等价性检查功能最弱，但自动化程序最高。