数字IC的设计流程，如下图所示：
其中讲到形式验证的时候就懵了。当时老师说，其实我也记不太清了，就从网上找了一下：
形式验证（Formal Verification）是一种IC设计的验证方法，它的主要思想是通过使用数学证明的方式来验证一个设计的功能是否正确。
形式验证可以分为三大类：
等价性检查（Equivalence Checking）、
形式模型检查（Formal Model Checking）（也被称作特性检查）
定理证明(Theory Prover)
首先我当时很不理解，为什么要做形式验证。老师给了一个答案，为了确认综合后的电路跟你的设计是一致的。电路不也是工具综合出来的吗？为什么不能保证一致性？
老师说工具也是人做出来的，也有可能会出错，所以要确认。好像有一定的道理，当时对形式验证的理解就是这么一个初步概念。
后来工作了几年，也做了不少项目，对形式验证的理解可能稍微深刻一点。
我们平时做的最多的模拟仿真，就是给各种case的输入，穷尽各种组合，总是希望100%的验证到所有的情况。但是有些情况下，你不太可能达到这一个目的。假如有一个32位的比较器：
比较产生等于、大于、大于的结果。
假设采用一个快速模拟器，每微秒运行一个向量，则用模拟器模拟完全部模拟向量需要的时间为：
264 (all input patterns) X 10-6
---------------------------------------------------
3600 (seconds) X 24 (hours) X 365 (days)
≈584,942 years
显然这是一个不切实际的验证时间。而形式验证使用
严格的数学推理来证明待测试设计的正确性，由于其静态、数学的特性，避免了对所有可能测试向量的枚举，而且能够达到100%无死角的检测。
定理证明是形式验证技术中最高大上的，它需要设计行为的形式化描述，通过严格的数学证明，比较HDL描述的设计和系统的形式化描述在所有可能输入下是否一致。这种验证方法需要非常深厚的数学功底，而且不能完全自动化，所以应用案例较少。当然还是有一些例子，例如HOL系统、PVS系统和ACL2系统等，并且都有成功应用案例。Moore等人验证了AMD5K86芯片的除法算法的微码，Brock等验证了Motorola的CAP处理器，Clark等验证了SRT除法算法。
模型检验是一种检测设计是否具有所需属性的方法，如安全性、活性和公平性。模型检验所针对的对象是同步时序设计。系统的设计spec用时序状态逻辑公式来描述。而通过对有限状态系统的所有可能的状态空间遍历来证明设计是符合规范的，增强设计者的信心；或者是通过提供违反spec的反例，以帮助设计者来发现早期设计的错误。反例给出的方式是从系统的初始状态出发到“坏”的状态的路径。系统的状态空间能够用有效的抽象符号算法来隐含地描述。抽象符号算法包括有向迁移图、二叉决策图(BDD- binary decision diagram)、合取范式(CNF- conjunctive normal form)等有效手段。
目前比较著名的模型检验工具：
Carnegie Mellon大学的符号模型检验工具SMV，
Stanford 研究所的原型验证系统PVS，
U.C.Berkerley的验证和综合工具VIS
和Bell实 验室的软件和协议验证工具Spin等。
等价性检查用于比较设计的两种实现是否一致，可分为组合等价性检查和时序等价性检查。目前是我们设计验证过程中用得最多的方法。它也是利用数学技术来验证参考设计与改动后的设计等价，主要目的是在一个设计经过变换之后，穷尽地检验变换前后的功能一致性，即证明设计的变换没有产生功能的变化，如下图所示：
等价性检查被广泛应用到设计流程中的各个不同阶段，用于验证不同设计层次之间的功能一致性，
或者用来验证RTL级对RTL级、RTL级对门级以及门级实现之间是否等价。
等价性检查的主要优点是比穷举式的模拟仿真更快，通常可在数小时内验证数百万门规模集成电路的一致性，这对模拟仿真是不可能的。比如我们在tapeout前突然因为一个bug改动比较大，看仿真已经来不及了，but怎么能放心的出去呢，只能靠等价性检查。因此，等价性检查工具已经被主流的设计流程所采用。
等价性检查的问题是需要一个参考设计作为描述，而如何设计一个理想参考模型（gold design）又是一个很重的任务。此外，等价性验证是为了找出实现的不一致性，而不能找出参考设计原先就可能存在的bug。另外等价性检查不能验证设计对象的时序，只能验证功能，因此它通常需要和时序分析工具配合在一起使用。
等价性检查主要是比较两种设计中相应的组合功能块。可以在参考设计中指定比较点，然后比较2种设计在该点的逻辑功能是否等价。比较点可以是输出端口、寄存器、锁存器、黑盒输入pin或被驱动的线网等。
逻辑锥(logical cone)是一组可驱动比较点的信号，它有n个输入(基本输入，状态点)和一个输出(基本输出，状态点)，也可以包含其他逻辑锥，如下图所示：
最右边是一个输出端口，可以将它将作为一个比较点，与参考设计中相应的对象进行比较，比较的过程实际上就是考察它们的逻辑锥是否等价。所以对于报告出来的不匹配的点，我们也可以通过对它们逻辑锥进行分析，来找出具体的原因。
因此，等价性检查的具体工作就是比较两种设计中的关键点的等价性并将两种设计中任何不匹配之处标记、报告出来。
等价性检查的工具有：
Synopsys的Formality，
Cadence的Incisive Conformal，
Mentor Graphics公司的FormalPro等
而具体的应用例子网上也能找到一些，如果找不到可以在公众号留言邮箱索取啊。
最后，总结一下模拟仿真和形式验证的比较：
形式验证目前还不能完全取代模拟仿真验证。两者各有所长，技术互补，在验证过程中应该结合使用，争取找出设计中所有的bug，哈哈！
