uvm 形式验证_形式化芯片验证：救世主还是乌托邦

小鱼儿 2023-01-01 15:49 234阅读 0赞

## **一、芯片验证：随机仿真vs形式化方法** ##

验证（verification）是现代数字集成电路设计流程中不可或缺且至关重要的一环，其目的是保证设计功能按照既定的设计规约正确的实现。在一个完整的项目周期中，验证所占用的时间可高达60%-70%。  
按验证的具体目的，可以有很多种细分类别，而本文主要针对其中的“功能验证“，即只专注于设计逻辑功能的实现，而暂不考虑综合、布局布线后引入的电路延时与优化，从而导致的硬件与实际逻辑出现偏差的情况。  
目前业界主流的验证方法主要是以UVM（Universal Verification Methodology）为代表的验证方法学，**通常使用随机约束的方式，在电路仿真中自动产生受控的随机输入，从而驱动验证电路并完成验证功能**。  
随着UVM的发展和广泛使用，特别是其中SystemVerilog语言加入了面向对象、功能覆盖、随机约束等更加类似软件开发的特性，使得验证平台间模块重用的效率得到提升，编程结构化变好，代码更加灵活。有关这些传统的验证方法的讨论和思考会在下文中逐步给出。

![6a29224f75078b107c6a84632f6e9bb5.png][]

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

![9f4315dc85415fd1756a8c6d89aeb670.png][]

## **二、什么是形式化验证** ##

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

![a726a30441b783a082e7a06daafc8324.png][]

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

![60e2fdea8e6869d1d3f84dd18ec62834.png][]

需要注意的是，作为形式化验证的使用者，我们并不需要了解形式化方法的具体数学原理，亦或是证明的具体过程。事实上，芯片工程师也没有相应的数学知识和功底，能够在算法层面对形式化验证方法进行修改和调试。  
在多数情况下，在形式化验证工具里的调试过程和传统电路仿真工具十分类似。接下来，我将详细介绍形式化验证相比传统验证方法的主要优势。

## **三、形式化验证的主要优点** ##

与传统的基于仿真的验证方法相比，形式化验证有着本质性的不同。形式化验证方法拥有很多特殊的优点，能够在理论上完全克服传统验证方法的缺陷和不足。总结说来，形式化验证的优点主要体现在下三个方面。**第一，形式化验证能覆盖完整的设计状态空间。**  
与其他所有基于仿真的验证方法相比，这一点是形式化方法最大的优势所在。通常来讲，一个数字电路的设计通常由若干个逻辑状态空间（logic state space）组成，这其中可以包含以下几类状态：

*  电路复位后的初始化状态， 也称为复位状态；
 *  内部逻辑实现时的中间状态；
 *  各个输入输出的状态。

比如，在一个FIFO设计中，它的“满”、“空”指示就是输出的状态；在某一时刻，FIFO里内存的读写指针的位置就是中间状态；而当复位完成后，指针位置以及当时“满”、“空”指示的值就是复位状态。  
如果将这些状态抽象提取出来，我们可以得到针对这个设计的完整的状态空间，如下图所示，其中每一个圆圈都代表电路中的一个可能的逻辑状态。而验证的最终目的，就是对完整的状态空间进行覆盖，并确定其满足既定的设计要求。  
在电路仿真中，每次仿真实际上就是在状态空间里寻找一条从“复位状态”到“输出状态”的路径， 如下图中标出的一条路径。

![aaca2d43bd0ebd99c638797e5a84ed81.png][]

需要注意的是，在仿真中每条路径的确定与仿真使用的输入（也称为激励或测试向量）有着密切的关系。如果在每次仿真中使用不同的输入，例如采用随机约束的验证方法，那么有可能找到更多的状态路径，如下图所示。

![7a4d07e459bd71e88b1177fdcac14b94.png][]

然而，对于某些大型设计，即便使用了多种不同的输入，也有可能仍然找到相同或者部分重叠的路径，这样就导致某些状态很难被覆盖，即我们通常所说的“边界情况”（corner cases）。  
对于边界情况的处理，通常的做法包括：**增加仿真次数，即尝试更多不同的输入组合；延长仿真时间；或者针对其创建新的“定向测试”等**。然而不管使用何种方法，都会极大的增加完成验证所需的时间，以及投入的各类成本。  
最根本的问题在于，即便使用了这些方法，也并不能保证边界情况被100%覆盖，这是由于仿真无法遍历所有可能的输入向量。换句话说，基于仿真的验证只是检验了在使用某些测试向量时，系统不会出现漏洞，但无法保证当使用其他测试向量时，漏洞不会出现。  
上文提到的CPU “熔断”和“幽灵”漏洞，也从另一个角度很好的印证了这一点：一方面，我相信CPU厂商在设计芯片时已经进行了充分验证，但显然还存在边界情况。另一方面，即使芯片已上市并广泛使用多年，这些漏洞直到最近才被发现，这在一定程度上表明通过改变测试向量来进行边界情况的捕捉和覆盖，效果不够理想，往往更像是“大海捞针”。  
形式化验证和基于电路仿真的验证方法的最根本不同在于，形式化验证并不基于某些给定的输入向量，**而是通过数学方法分析、推导并证明某个逻辑功能在给出的边界范围内是否与设计规约完全吻合，若不吻合则会给出一个反例。**  
在上面举的例子中，形式化验证可以从给定的复位状态开始，用数学方法自动探索并覆盖整个状态空间，如下图所示。从形式化的视角来看，这里所有的逻辑状态并没有本质的区别，因此即使是电路仿真很难发现的边界情况，也能很容易的通过形式化的方法进行覆盖。

![404fb02469020e56053922a30be8bc36.png][]

通常而言，上述数学推理并证明的过程都被封装在EDA工具里，并由工具自动完成。因此作为形式化验证工具的使用者，我们并不需要深入理解这些工具的工作机制，以及其中复杂的数学理论。这进一步降低了形式化验证的使用门槛，同时能让设计和验证工程师从更为整体的角度思考验证策略，而非纠结于如何产生各类输入向量才能达成某种设计中的状态。**第二，形式化验证能提供最小实例。**  
形式化验证的第二个主要优点在于能迅速提供一个最小实例，如下图所示。这里“最小实例”指的是，达到一个目标状态所需要的必要条件，包括各个输入值、寄存器的状态，以及达到目标状态需要的最少周期数等。

![b292d8dcbf0d93aebbe913a1dd4c8250.png][]

设想在一个复杂的状态机设计中，需要验证某个状态能否实现，且需要考察达到该状态时所需要的条件， 比如：如何给定输入、内部状态如何转换、通过多久才能达到该状态等等。  
此时如果使用电路仿真，会有以下几个问题：

1.  由于不确定何种输入向量才能达到目标状态，首先需要进行一系列仿真才有可能达到该状态。若目标状态恰好是边界状态，找到它本身的难度就很大。
2.  即使通过多次仿真找到了满足条件的输入向量，这样每次的仿真时间往往长达几十分钟到几小时，对复现和多次调试的效率影响很大。
3.  无法确定是否还有其他条件能够达到目标状态。

和电路仿真不同，形式化验证可以很快的给出达到目标状态的最小实例，或者反之，得出结论证明该目标状态永远不会被达到。  
电路设计者和验证者可以通过这个特性，利用形式化验证对目标状态进行快速调试，并通过给出的最小实例，更好的理解电路行为，及时发现其与设计规约的偏差。**第三，形式化验证能提供“基于状态”或“基于输出”的分析和调试方法。**  
如上文所述，传统的电路仿真都是基于输入的方法，即给出输入后才能观察内部状态以及电路输出。然而，形式化验证并不依赖任何输入，因此可以做到“基于状态”或者“基于输出”，并以此进行设计分析和调试。  
例如，在基于状态的方法中，我们希望知道在一个设计中是否能够通过某种方式达到某种状态（如前文中所述），或者更进一步，希望将此状态作为接下来分析和调试的起始状态。  
可以想象，使用电路仿真达成这样的目标很难，因为需要先找到合适的输入、经过漫长的仿真时间后才可能达到该状态，而往往对于固定的输入只会得到固定的输出，如下图所示。

![edde914164dd7c47f02ac9d9811feeea.png][]

相比之下，形式化验证没有这些限制，而是可以任意指定起始状态，并可以由该状态为起点，探索后续的所有可能的状态空间，包括所有可能达到的输出状态，并给出对应的输入最小实例，见下图。同理，甚至可以指定某个输出状态为目标状态，由此反推达到该状态需要满足何种条件。

![6332d7917573d52068ffc802a6b5b590.png][]

## **四、小结** ##

本文着重介绍了芯片的形式化验证方法的独特优势，几乎弥补了传统的芯片验证方法的所有短板和缺陷。  
然而，究竟形式化验证是传说中芯片验证的“救世主”，还是只不过是看似美丽的“乌托邦”，其实取决于它最大的主要缺点。我们且看下回分解。

--------------------

***更多原创芯文、芯情、芯事，欢迎关注公众号“老石谈芯”***

![2efc108dcfa2c56755e2cd55e1f39720.png][]

[6a29224f75078b107c6a84632f6e9bb5.png]: /images/20221120/1aeb86824c9449669cba80ffd5c73e7b.png
[9f4315dc85415fd1756a8c6d89aeb670.png]: /images/20221120/0240073484c74a03b427cbae907e747a.png
[a726a30441b783a082e7a06daafc8324.png]: /images/20221120/14cc3cdb53844b348730b30ea1f6629e.png
[60e2fdea8e6869d1d3f84dd18ec62834.png]: /images/20221120/c686b990bc8d4bd3b10982a2f2395341.png
[aaca2d43bd0ebd99c638797e5a84ed81.png]: /images/20221120/e977ee8cf43c40bbb7a9a69a3e33c412.png
[7a4d07e459bd71e88b1177fdcac14b94.png]: /images/20221120/06553c5b53e84489aeca0d3b4d5dbeef.png
[404fb02469020e56053922a30be8bc36.png]: /images/20221120/5e3f569630b4466b8c0e14c03d7595a2.png
[b292d8dcbf0d93aebbe913a1dd4c8250.png]: /images/20221120/25102f5106014d678393f3f56ebd36c2.png
[edde914164dd7c47f02ac9d9811feeea.png]: /images/20221120/992350ca02df45df9d85974c6aa74db8.png
[6332d7917573d52068ffc802a6b5b590.png]: /images/20221120/85a81a5be33747599734f537fa406d3d.png
[2efc108dcfa2c56755e2cd55e1f39720.png]: /images/20221120/c4bd36111d644495b78438ba527445f6.png