什么是形式化验证？ 以及软件形式化验证

软件开发中一般使用“测试”来找bug，这种方法只能找到bug，不能证明程序没有bug。

形式化验证 是用逻辑来验证程序的可靠性，就是把一段程序用逻辑的方法证明一遍，证明它能得到预期的结果，没有bug。一般这类研究主要应用于昂贵的航天器材的操作系统、危险的医疗设备的程序之中。因为航天器材、医疗设备牵扯到人的生命，如果操作系统出现错误，那么很危险，又不能用测试一遍一遍的测，所以用形式化验证来做。比如美国航天局NASA就会雇佣大批形式化验证的专家来验证他们操作系统的正确性。 学习这个方向，最好有比较好的逻辑知识（数理逻辑、拉姆达验算），最好比较了解程序（比如操作系统的设计、编译器的设计等）。 这个方向是比较犀利的研究方向，但不大容易出论文，需要长时间积累才能发一篇好论文。 这个方向只是科研方向，不适合找工作，如果你读完硕士打算找工作而不做研究，这个方向不适合。因为企业没人用形式化验证来验证程序。

传统上在硬件设计领域比较常用。主要原因就是硬件设计周期长，成本高，一旦生产出来就很难改动了。例如一个 CPU 设计如果已经出芯片了，那么出了问题就是大事。Peter 自己以前所在的能源动力领域，很多电厂设备也都要做数学上的论证，不过我们那会儿不用形式化验证这个词，我们叫建模，或者叫软件模拟。如果直接用一台机器去做各种试验，那么成本是很高的，而用数学去构建一台虚拟的机器去验证，既可以运行全部的输入和输出，做到论证充分，同时又没有太高的成本。

Formal Verification（形式验证)

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

形式验证是一个系统性的过程，将使用数学推理来验证设计意图（指标）在实现(RTL)中是否得以贯彻。形式验证可以克服所有3种仿真挑战，由于形式验证能够从算法上穷尽检查所有随时间可能变化的输进值。

形式验证的出现

由于仿真对于超大规模设计来说太耗费时间，形式验证就出现了。当确认设计的功能仿真是正确的以后，设计实现的每一个步骤的结果都可以与上个步骤的结果做形式比较，也就是等价检查，如果一致就说明设计合理，不必进行仿真了。

形式验证主要是进行逻辑形式和功能的一致性比较，是靠工具自己来完成，无需开发测试向量。而且由于实现的每个步骤之间逻辑结构变化都不是很大，所有逻辑的形式比较会非常快。这比仿真的时间要少很多。一般要做形式验证的步骤有：RTL和RTL。

IC设计验证方法

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

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

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

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

软件设计验证方法

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

形式验证工具

• Synopsys的Formality
• Cadence LEC(Logic Equivalence Check)

形式验证的优点

1. 由于形式验证技术是借用数学上的方法将待验证电路和功能描述或参考设计直接进行比较，因此测试者不必考虑如何获得测试向量。
2. 形式验证是对指定描述的所有可能的情况进行验证，而不是仅仅对其中的一个子集进行多次试验，因此有效地克服了模拟验证的不足。
3. 形式验证可以进行从系统级到门级的验证，而且验证时间短，有利于尽早、尽快地发现和改正电路设计中的错误，有可能缩短设计周期。

形式验证与仿真的区别

验证实现工作包括将多种输进条件定义为测试计划的一部分、创建功能覆盖模型、开发测试平台、创建输进激励发生器、编写指导性测试以及执行测试、分析覆盖率指标、调整激励发生器以面向未验证的设计部分，然后反复这一过程。

形式验证补充了模拟验证的不足，二者各有优势，互为补充，缺一不可。

仿真是一种基于经验的模拟验证方法，通过反复试验试图查明缺陷，这要花相当多的时间尝试所有可能的组合，因此永远不会完整。另外，由于工程师必须定义和产生大量输进条件，他们的工作重点将是如何在非设计目标基础上分解设计。

形式验证是穷尽式数学技术，使工程师仅关注设计意图。纯形式验证技术与仿真验证相反，专注于证实模块的端到端、直接对应微架构规范的高层要求，帮助用户戏极大进步项目的设计和验证产能，同时确保正确性。

为何大部分程序员都没听说过？

但是大部分的程序员可能从来都没用过形式化验证，这是为啥呢？

首先就是因为软件迭代太快了。尤其在互联网领域，创新是不变的主题，对一套系统建立数学模型是有很高的时间成本的，对于要频繁迭代的系统就显得不适合了。

软件很容易升级。跟硬件不一样，软件有了 Bug ，可以连夜修复，很多用户根本不会注意到。万一有用户遇到了 bug ，起码后台数据库的数据一般不会损坏，打个电话，让客服帮忙弄一下，谁家的软件又没 bug 呢？

软件是有测试的。对于没有写过代码的同学可能不太熟悉什么叫做写测试。写测试，也就是去写一些能有验证代码的代码。测试代码中其实往往也会模拟一些输入和输出情况的。形式化验证是超豪华版的测试，用严格的数学论证，保证逻辑没有死角。

本文转自：

• https://blog.csdn.net/weixin_38438451/article/details/80491947
• https://zhuanlan.zhihu.com/p/56369013