由于集成电路规模增大，单个芯片已经可以包含整个电路系统，因此设计过程的复杂性迅速增加。解决电路设计复杂性的一种方法是进行层次化设计。这种方法从系统级、行为级、寄存器传输级、功能级、门级以及开关级等不同的级别对设计进行描述，每级还可以细化为许多层次，使得设计对象逐级细化。
　　在如此广阔的设计领域里，每个步骤都有可能发生错误。验证作为保证设计正确性的主要手段，其重要性是不言而喻的，而且，设计人员希望越早发现错误越好，如果要到版图级验证时才发现错误，所造成的损失将是十分巨大的。开发适合于各个设计阶段和设计层次的验证工具，帮助设计人员尽早发现和排除错误，是EDA的一个重要研究课题。
　　在目前流行的设计方法和实际设计流程中，设计正确性的验证通常采用的是模拟验证方法（Simulation Verification Method）。所谓模拟验证，是指从电路描述（语言描述或图形描述）中提取出模型，然后将外部激励信号或数据施加于该模型，进行计算并观察输出结果，判断该电路描述是否实现了预期的功能 。

　　我们在第3章已经讲了模拟验证的方法。请读者参考第3章内容。

　　模拟验证采用仿真运行的手段，为设计人员提供了可行的判别数据，在实际设计中发挥着巨大的作用。但是，这种技术的不足之处也是十分明显的，主要表现在：
　　　1. 模拟方法严重依赖于测试向量的选取。合理而充分地选取测试向量本身就是一个十分艰巨的课题。
　　　2. 模拟方法的效率不高。VLSI的设计常常需要反复修改，而每次修改后都需要模拟，以确认本次修改达到了预期目的且没有引入新的错误，因此设计人员用在模拟验证上的时间常常是设计时间的2至3倍。
　　电路规模较小的时候，这些不足所造成的影响还不太明显；随着电路规模的迅速增长，模拟验证的不足便突出地摆在了设计人员面前，如测试向量的选择愈加困难，测试向量集的规模呈指数级增加，模拟时间变得不可忍受等。人们开始认识到，必须提供多种设计正确性的验证手段，来解决设计人员所处的这种不利环境。于是，人们提出了一种新的验证方法──-形式验证（Formal Verification）。
　　所谓形式验证，是指从数学上完备地证明或验证电路的实现方案（简称实现）是否确实实现了电路设计描述（简称描述）的功能。
　　与模拟验证相比，形式验证有不少优点。
　　　1. 首先，由于形式验证技术是借用数学上的方法将待验证电路和功能描述或参考设计直接进行比较，因此测试者不必考虑如何获得测试向量。
　　　2. 其次，形式验证是对指定描述的所有可能的情况进行验证，而不是仅仅对其中的一个子集进行多次试验，因此有效地克服了模拟验证的不足。
　　　3. 此外，形式验证可以进行从系统级到门级的验证，而且验证时间短，有利于尽早、尽快地发现和改正电路设计中的错误，有可能缩短设计周期。

　　国外的形式验证研究从七十年代开始。由于当时电路规模不大，模拟验证基本上可以满足设计要求，而且当时也没有有效的数学方法，所以只是在学校和实验室里提出了一些验证方法，并没有得到工业界的足够重视。从八十年代后期开始，形式验证得到越来越广泛的关注，形式验证技术迅速发展。1990年代，已有一些商用软件出现，如Compass Design Automation(San Jose, CA)公司的VFormal，Chrysalis Symbolic Design(Andover MA)公司的Design VERIFYer等。但是这些软件主要还是针对组合电路的形式验证，而时序电路的形式验证，目前尚无成熟的方法和相应软件问世，还处于高校实验室的研究阶段，比较典型的系统有Univ. California at Berkeley的VIS系统，Carnegie-Mellon Univ.(CMU, Pittsburgh, PA)的SMV系统等。

　　形式验证也有其致命的弱点。形式验证到目前为止仍然不能有效的验证电路的性能，如电路的时延和功耗等。然而，形式验证的作用正是补充了模拟验证的不足，二者各有优势，互为补充，缺一不可。

　　形式验证不是要取代模拟验证，恰恰相反，二者是互补的，共同完成验证的任务。形式验证目前只是对功能（或功能方面的性质）进行验证，而模拟验证则对电路性能，尤其是时延性能，能够精确的模拟。另外，形式验证往往值能判断设计正确与否，难以给出电路的什么位置有设计错误，而这一点恰又是模拟验证的优势。