软件开发中一般使用“测试”来查找bug，但这种方法只能找到bug，无法证明程序中没有bug。 形式化验证是利用逻辑验证程序的可靠性，是用逻辑的方法对某个程序进行一次证明，证明其能得到预期的结果，没有错误。 一般来说，这类研究主要应用于昂贵的航天设备操作系统、危险医疗设备程序。 宇宙机器和医疗机器关系到人命，如果操作系统有错误的话就很危险，而且在测试中不能多次测量，所以我们在进行形式化的验证。 例如，美国航天局(NASANASA )将聘请许多经过形式验证的专家来验证操作系统的正确性。 要学习这个方向，最好有逻辑知识(数理逻辑，随机计算)，知道程序)操作系统的设计，编译器的设计等。 虽然这个方向是比较尖锐的研究方向，但是出论文并不容易，出好论文需要很长时间的积累。 这个方向是科研方向，不适合找工作。 如果你打算读硕士学位不做研究就找工作的话，这个方向不适合。 因为企业没有人通过形式上的验证来验证程序。
格式验证)。
在计算机硬件，特别是集成电路、软件系统的设计过程中，形式验证是指或基于某种形式的规范或属性，采用数学方法证明其正确性或不正确性。
形式验证是一个系统性的过程，利用数学推理来验证设计意图(指标)在实现(RTL )中是否得到贯彻。 因为形式验证可以克服所有3个仿真课题，形式验证可以从算法上全面检查所有可能随时间变化的输入值。
形式验证形式验证的出现
由于仿真在超大规模设计中耗时过长，出现了形式验证。 验证了设计的功能模拟正确后，设计实现的每个步骤的结果可以与上一步骤的结果进行形式上的比较。 也就是说，是等效检查。 一致则设计合理，不需要进行模拟。
形式验证主要是进行逻辑形式和功能的一致性比较，由工具自身进行，无需开发测试向量。 此外，所有逻辑的形式都非常快，因为实现的每个步骤之间的逻辑结构变化不是很大。 这比模拟的时间少得多。 一般来说，进行形式验证的步骤是RTL和RTL。
集成电路设计验证方法
:2em;">形式验证（Formal Verification）是一种IC设计的验证方法，它的主要思想是通过使用形式证明的方式来验证一个设计的功能是否正确。形式验证可以分为三大类：等价性检查（Equivalence Checking）、形式模型检查（Formal Model Checking）（也被称作特性检查）和定理证明(Theory Prover) 。等价性检查的验证用于验证RTL设计与门级网表、门级网表与门级网表是否一致。在进行扫描链重排、时钟树综合等过程中，都可以用等价性检查保证网表的一致性。等价性检查已经融入IC标准设计流程中。等价性检查在检查ECO时非常有用。例如，设计者在修改门级网表时，由于手误，错将一个或门写成或非门，等价性检查工具通过比较RTL设计与门级网表，可以很容易地发现这种错误。
模型检查用时态逻辑来描述规范，通过有效的搜索方法来检查给定的系统是否满足规范。模型检查是目前研究的热点，但其验证的电路规模受限制这一问题还没有得到很好的解决。
定理证明把系统与规范都表示成数学逻辑公式，从公理出发寻求描述。定理证明验证的电路模型不受限制，但需要使用者的人工干预和较多的背景知识。
软件设计验证方法
形式化验证过程可以证明一个系统不存在某个缺陷或符合某个或某些属性。软件测试无法证明系统不存在缺陷，也不能证明它符合一定的属性。系统无法被证明或测试为无缺陷，这是因为不可能形式地规定什么是“没有缺陷”。所有可以做的，就是证明一个系统没有任何可以想到的缺陷，并且满足所有的使系统符合功能要求的和有用的属性。
形式验证工具：
Synopsys的Formality
Cadence LEC(Logic Equivalence Check)
形式验证的优点
1. 由于形式验证技术是借用数学上的方法将待验证电路和功能描述或参考设计直接进行比较，因此测试者不必考虑如何获得测试向量。
2. 形式验证是对指定描述的所有可能的情况进行验证，而不是仅仅对其中的一个子集进行多次试验，因此有效地克服了模拟验证的不足。
3. 形式验证可以进行从系统级到门级的验证，而且验证时间短，有利于尽早、尽快地发现和改正电路设计中的错误，有可能缩短设计周期。
折叠编辑本段区别验证实现工作包括将多种输进条件定义为测试计划的一部分、创建功能覆盖模型、开发测试平台、创建输进激励发生器、编写指导性测试以及执行测试、分析覆盖率指标、调整激励发生器以面向未验证的设计部分，然后反复这一过程。
形式验证补充了模拟验证的不足，二者各有优势，互为补充，缺一不可。
仿真是一种基于经验的模拟验证方法，通过反复试验试图查明缺陷，这要花相当多的时间尝试所有可能的组合，因此永远不会完整。另外，由于工程师必须定义和产生大量输进条件，他们的工作重点将是如何在非设计目标基础上分解设计。
形式验证是穷尽式数学技术，使工程师仅关注设计意图。纯形式验证技术与仿真验证相反，专注于证实模块的端到端、直接对应微架构规范的高层要求，帮助用户戏极大进步项目的设计和验证产能，同时确保正确性。