目前业界主流的验证方法主要是以UVM（Universal Verification Methodology）为代表的验证方法学，通常使用随机约束的方式，在电路仿真中自动产生受控的随机输入，从而驱动验证电路并完成验证功能。随着UVM的发展和广泛使用，特别是其中SystemVerilog语言加入了面向对象、功能覆盖、随机约束等更加类似软件开发的特性，使得验证平台间模块重用的效率得到提升，编程结构化变好，代码更加灵活。有关这些传统的验证方法的讨论和思考会在下文中逐步给出。

　　然而需要注意到的是，这些基于电路仿真的验证方法存在较多的根本性问题一直无法有效解决，如对极端情况的覆盖、过长的仿真时间、调试难度较大等等。这些问题也将会在后文一一讨论。在2018年初，几乎全部主流的CPU厂商都被发现在其CPU产品中存在熔断（Meltdown）和幽灵（Spectre）漏洞。这也在一个侧面表明，当代集成电路验证存在极高的复杂性，特别是对于大型设计而言。因此，业界一直在寻找其他更为有效的验证方法学。下文将介绍的“形式化验证“（Formal Verification）就是其中之一。

　　它很像我们上学时做过的数学证明题，即给一个命题，用数学定理和方法证明该命题是否成立。若不成立则给出一则反例。在形式化验证中，待测设计的某个功能和设计规约对应的描述就是命题的两部分，命题为证明二者是否等价，若得证则表示在任意情况下命题成立，若不得证则表示命题不成立，且会给出一个反例。这个推理和证明的过程通常由EDA工具自动完成。目前，业界主流的形式化验证EDA工具主要有Cadence的JasperGold，和Synposys的VC-Formal等。

　　然而，对于某些大型设计，即便使用了多种不同的输入，也有可能仍然找到相同或者部分重叠的路径，这样就导致某些状态很难被覆盖，即我们通常所说的“边界情况”（corner cases）。对于边界情况的处理，通常的做法是增加仿真次数，即尝试更多不同的输入组合；延长仿真时间；或者针对其创建新的“定向测试”等。然而不管使用何种方法，都会极大的增加完成验证所需的时间，以及投入的各类成本。最根本的问题在于，即便使用了这些方法，也并不能保证边界情况被100%覆盖，这是由于仿真无法遍历所有可能的输入向量。换句哈希 HASH话说，基于仿真的验证只是检验了在使用某些测试向量时，系统不会出现漏洞，但无法保证当使用其他测试向量时，漏洞不会出现。上文提到的CPU “熔断”和“幽灵”漏洞，也从另一个角度很好的印证了这一点：一方面，我相信英特尔（及其他厂商）在设计芯片时已经进行了充分验证，但显然还存在边界情况。另一方面，即使芯片已上市并广泛使用多年，这些漏洞直到最近才被发现，这在一定程度上表明通过改变测试向量来进行边界情况的捕捉和覆盖，效果不够理想，往往更像是“大海捞针”。