验证（verification）是现代数字集成电路设计流程中不可或缺且至关重要的一环，其目的是保证设计功能按照既定的设计规约正确的实现。在一个完整的项目周期中，验证所占用的时间可高达60%-70%。按验证的具体目的，可以有很多种细分类别，而本文主要针对其中的“功能验证“，即只专注于设计逻辑功能的实现，而暂不考虑综合、布局布线后引入的电路延时与优化，从而导致的硬件与实际逻辑出现偏差的情况。

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

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

和基于电路仿真的验证方法不同，笔者认为形式化验证的定义是：利用形式化方法，即基于严格的数学表述和模型，根据设计规约对设计功能进行属性描述，并自动进行数学分析和证明。这看上去似乎非常玄妙，但实际上形式化验证的过程可以粗略的由下图描述：

图2：形式化验证简要流程图

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

需要注意的是，作为形式化验证的使用者，我们并不需要了解形式化方法的具体数学原理，亦或是证明的具体过程。在多数情况下，在形式化验证工具里的调试过程和传统电路仿真工具十分类似。

深圳市丽晶微电子科技有限公司，专注于太阳能闪灯IC，太阳能充电IC，太阳能控制器IC方案，太阳能草坪灯控制IC，太阳能路灯控制器IC，太阳能草坪灯IC，太阳能草坪灯驱动IC,太阳能草坪灯芯片，太阳能充电管理IC，太阳能充电芯片，太阳能控制芯片，太阳能电池充电芯片，太阳能充电控制芯片，太阳能LED灯串驱动芯片。