数字集成电路的设计过程如下图所示。
其中谈形式验证的时候很无知。 老师说其实我也不太记得了，就从网上找了：
形式验证(Formal Verification )是一种集成电路设计的验证方法，以使用数学证明的方法验证设计功能是否正确为主要思想。
形式验证可以分为三类：
等效性检查(Equivalence Checking )、
形式检查(也称为形式模型检查)特性检查) )
定理证明(Theory Prover ) ) )。
首先，我不理解为什么要进行形式上的验证。 老师给出了答案。 是为了确保综合电路与你的设计一致。 电路不是也集成了道具吗？ 为什么不能保证一致性？
老师说道具也是人做的，也有可能出错，所以要确认一下。 似乎有道理，当时对形式验证的理解是这样的初步概念。
之后工作了几年，还做了很多项目。 对形式验证的理解可能有点深。
我们平时最常做的模拟是输入各种case，涵盖各种组合，希望始终100%验证所有情况。 但是，在某些情况下，不能实现这个目的。 假设你有一个32位的比较器：
比较相等、大、大的结果。
假设您使用高速模拟器每微秒运行一次向量。 在模拟器中模拟完整的模拟向量所需的时间如下。
264(allinputpatterns ) X10-6
------------- -请参阅
3600 (第二季度) x24 (家庭) x365 (日期)
584，942年
这显然是不现实的验证时间。 用于形式验证
通过严格的数学推理证明了待测设计的正确性，由于其静态、数学特性，避免了列出所有可能的测试向量，而且可以达到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之前突然有一个错误，改动很大，看模拟已经来不及了。 臭虫为什么能安心出去，只能依靠等效性检查。 因此，等效性检测工具已被主流设计流程所采用。
等效性检测问题需要参考设计作为说明，如何设计理想的参考模型(gold design )是一项非常重要的任务
。此外，等价性验证是为了找出实现的不一致性，而不能找出参考设计原先就可能存在的bug。另外等价性检查不能验证设计对象的时序，只能验证功能，因此它通常需要和时序分析工具配合在一起使用。
等价性检查主要是比较两种设计中相应的组合功能块。可以在参考设计中指定比较点，然后比较2种设计在该点的逻辑功能是否等价。比较点可以是输出端口、寄存器、锁存器、黑盒输入pin或被驱动的线网等。
逻辑锥(logical cone)是一组可驱动比较点的信号，它有n个输入(基本输入，状态点)和一个输出(基本输出，状态点)，也可以包含其他逻辑锥，如下图所示：
最右边是一个输出端口，可以将它将作为一个比较点，与参考设计中相应的对象进行比较，比较的过程实际上就是考察它们的逻辑锥是否等价。所以对于报告出来的不匹配的点，我们也可以通过对它们逻辑锥进行分析，来找出具体的原因。
因此，等价性检查的具体工作就是比较两种设计中的关键点的等价性并将两种设计中任何不匹配之处标记、报告出来。
等价性检查的工具有：
Synopsys的Formality，
Cadence的Incisive Conformal，
Mentor Graphics公司的FormalPro等
而具体的应用例子网上也能找到一些，如果找不到可以在公众号留言邮箱索取啊。
最后，总结一下模拟仿真和形式验证的比较：
形式验证目前还不能完全取代模拟仿真验证。两者各有所长，技术互补，在验证过程中应该结合使用，争取找出设计中所有的bug，哈哈！