这项技术将成为集成电路验证的未来？
验证（verification）是现代数字集成电路设计流程中不可或缺且至关重要的一环，其目的是保证设计功能按照既定的设计规约正确的实现。在一个完整的项目周期中，验证所占用的时间可高达60%-70%。按验证的具体目的，可以有很多种细分类别，而本文主要针对其中的“功能验证“，即只专注于设计逻辑功能的实现，而暂不考虑综合、布局布线后引入的电路延时与优化，从而导致的硬件与实际逻辑出现偏差的情况。
目前业界主流的验证方法主要是以UVM（Universal Verification Methodology）为代表的验证方法学，通常使用随机约束的方式，在电路仿真中自动产生受控的随机输入，从而驱动验证电路并完成验证功能。随着UVM的发展和广泛使用，特别是其中SystemVerilog语言加入了面向对象、功能覆盖、随机约束等更加类似软件开发的特性，使得验证平台间模块重用的效率得到提升，编程结构化变好，代码更加灵活。有关这些传统的验证方法的讨论和思考会在下文中逐步给出。
然而需要注意到的是，这些基于电路仿真的验证方法存在较多的根本性问题一直无法有效解决，如对极端情况的覆盖、过长的仿真时间、调试难度较大等等。这些问题也将会在后文一一讨论。在2018年初，几乎全部主流的CPU厂商都被发现在其CPU产品中存在熔断（Meltdown）和幽灵（Spectre）漏洞。这也在一个侧面表明，当代集成电路验证存在极高的复杂性，特别是对于大型设计而言。因此，业界一直在寻找其他更为有效的验证方法学。下文将介绍的“形式化验证“（Formal Verification）就是其中之一。
图1：熔断（Meltdown）和幽灵（Spectre）漏洞
和基于电路仿真的验证方法不同，笔者认为形式化验证的定义是：利用形式化方法，即基于严格的数学表述和模型，根据设计规约对设计功能进行属性描述，并自动进行数学分析和证明。这看上去似乎非常玄妙，但实际上形式化验证的过程可以粗略的由下图描述：
图2：形式化验证简要流程图
它很像我们上学时做过的数学证明题，即给一个命题，用数学定理和方法证明该命题是否成立。若不成立则给出一则反例。在形式化验证中，待测设计的某个功能和设计规约对应的描述就是命题的两部分，命题为证明二者是否等价，若得证则表示在任意情况下命题成立，若不得证则表示命题不成立，且会给出一个反例。这个推理和证明的过程通常由EDA工具自动完成。目前，业界主流的形式化验证EDA工具主要有Cadence的JasperGold，和Synposys的VC-Formal等。
需要注意的是，作为形式化验证的使用者，我们并不需要了解形式化方法的具体数学原理，亦或是证明的具体过程。在多数情况下，在形式化验证工具里的调试过程和传统电路仿真工具十分类似。在下一章，我将详细介绍形式化验证相比传统验证方法的主要优势。
与传统的基于仿真的验证方法相比，形式化验证主要有以下三个方面的优点。
第一，形式化验证能覆盖完整的设计状态空间。
与其他所有基于仿真的验证方法相比，这一点是形式化方法最大的优势所在。通常来讲，一个数字电路的设计通常由若干个逻辑状态空间（logic state space）组成，这其中可以包含以下几类状态：
电路复位后的初始化状态， 也称为复位状态；
内部逻辑实现时的中间状态；
各个输入输出的状态。
比如，在一个FIFO设计中，它的“满”、“空”指示就是输出的状态；在某一时刻，FIFO里内存的读写指针的位置就是中间状态；而当复位完成后，指针位置以及当时“满”、“空”指示的值就是复位状态。
如果将这些状态抽象提取出来，我们可以得到针对这个设计的完整的状态空间，如下图所示，其中每一个圆圈都代表电路中的一个可能的逻辑状态。而验证的最终目的，就是对完整的状态空间进行覆盖，并确定其满足既定的设计要求。
在电路仿真中，每次仿真实际上就是在状态空间里寻找一条从“复位状态”到“输出状态”的路径， 如下图中标出的一条路径。
图3：一次仿真得到的状态路径
需要注意的是，在仿真中每条路径的确定与仿真使用的输入（也称为激励或测试向量）有着密切的关 38 40575 38 15600 0 0 7493 0 0:00:05 0:00:02 0:00:03 7492。如果在每次仿真中使用不同的输入，例如采用随机约束的验证方法，那么有可能找到更多的状态路径，如下图所示。
图4：多次仿真得到的状态路径
然而，对于某些大型设计，即便使用了多种不同的输入，也有可能仍然找到相同或者部分重叠的路径，这样就导致某些状态很难被覆盖，即我们通常所说的“边界情况”（corner cases）。对于边界情况的处理，通常的做法是增加仿真次数，即尝试更多不同的输入组合；延长仿真时间；或者针对其创建新的“定向测试”等。然而不管使用何种方法，都会极大的增加完成验证所需的时间，以及投入的各类成本。最根本的问题在于，即便使用了这些方法，也并不能保证边界情况被100%覆盖，这是由于仿真无法遍历所有可能的输入向量。换句话说，基于仿真的验证只是检验了在使用某些测试向量时，系统不会出现漏洞，但无法保证当使用其他测试向量时，漏洞不会出现。上文提到的CPU “熔断”和“幽灵”漏洞，也从另一个角度很好的印证了这一点：一方面，我相信英特尔（及其他厂商）在设计芯片时已经进行了充分验证，但显然还存在边界情况。另一方面，即使芯片已上市并广泛使用多年，这些漏洞直到最近才被发现，这在一定程度上表明通过改变测试向量来进行边界情况的捕捉和覆盖，效果不够理想，往往更像是“大海捞针”。
形式化验证和基于电路仿真的验证方法的最根本不同在于，形式化验证并不基于某些给定的输入向量，而是通过数学方法分析、推导并证明某个逻辑功能在给出的边界范围内是否与设计规约完全吻合，若不吻合则会给出一个反例。在上面举的例子中，形式化验证可以从给定的复位状态开始，用数学方法自动探索并覆盖整个状态空间，如下图所示。从形式化的视角来看，这里所有的逻辑状态并没有本质的区别，因此即使是电路仿真很难发现的边界情况，也能很容易的通过形式化的方法进行覆盖。
图5：形式化验证对状态空间的全覆盖
通常而言，上述数学推理并证明的过程都被封装在EDA工具里，并由工具自动完成。因此作为形式化验证工具的使用者，我们并不需要深入理解这些工具的工作机制，以及其中复杂的数学理论。这进一步降低了形式化验证的使用门槛，同时能让设计和验证工程师从更为整体的角度思考验证策略，而非纠结于如何产生各类输入向量才能达成某种设计中的状态。
第二，形式化验证能提供最小实例
形式化验证的第二个主要优点在于能迅速提供一个最小实例，如下图所示。这里“最小实例”指的是，达到一个目标状态所需要的必要条件，包括各个输入值、寄存器的状态，以及达到目标状态需要的最少周期数等。
图6：形式化验证可以提供到达目标状态的最小实例
设想在一个复杂的状态机设计中，需要验证某个状态能否实现，且需要考察达到该状态时所需要的条件， 比如：如何给定输入、内部状体如何转换、通过多久才能达到该状态等等。如果使用电路仿真，会有以下几个问题：
1. 由于不确定何种输入向量才能达到目标状态，首先需要进行一系列仿真才有可能达到该状态。若目标状态恰好是边界状态，找到它本身的难度就很大。
2. 即使通过多次仿真找到了满足条件的输入向量，这样每次的仿真时间往往长达几十分钟到几小时，对复现和多次调试的效率影响很大。
3. 无法确定是否还有其他条件能够达到目标状态。
和电路仿真不同，形式化验证可以很快的给出达到目标状态的最小实例，或者反之，得出结论证明该目标状态永远不会被达到。电路设计者和验证者可以通过这个特性，利用形式化验证对目标状态进行快速调试，并通过给出的最小实例，更好的理解电路行为，及时发现其与设计规约的偏差。
第三，形式化验证能提供“基于状态”或“基于输出”的分析和调试方法。
如上文所述，传统的电路仿真都是基于输入的方法，即给出输入后才能观察内部状态以及电路输出。然而，形式化验证并不依赖任何输入，因此可以做到“基于状态”或者“基于输出”，并以此进行设计分析和调试。
例如，在基于状态的方法中，我们希望知道在一个设计中是否能够通过某种方式达到某种状态（如前文中所述），或者更进一步，希望将此状态作为接下来分析和调试的起始状态。可以想象，使用电路仿真达成这样的目标很难，因为需要先找到合适的输入、经过漫长的仿真时间后才可能达到该状态，而往往对于固定的输入只会得到固定的输出，如下图所示。
相比之下，形式化验证没有这些限制，而是可以任意指定起始状态，并可以由该状态为起点，探索后续的所有可能的状态空间，包括所有可能达到的输出状态，并给出对应的输入最小实例。同理，甚至可以指定某个输出状态为目标状态，由此反推达到该状态需要满足何种条件。
图7：形式化验证可以进行基于状态或输入的调试和验证
形式化验证有着传统基于仿真的验证方法学无可比拟的优势，看起来几乎是完美的验证方法学。可惜的是，形式化验证有着非常显著的缺点，其中最主要的就是所谓的“状态爆炸”问题（state explosion）。顾名思义，这代表了在某个设计中，理论上存在的状态可能非常多，超出了形式化验证工具可以处理的范围。例如，在一个简单的n位计数器中，可能存在2^n个状态，且状态数量随着计数器位数的增加呈指数级增长。同样的状态爆炸问题存在于存储器、各类数学运算单元如乘法器等等。
可以看到，这个问题是由形式化验证——具体而言是形式化验证中最为常用的模型验证（Model Checking）——的工作机制决定的，是形式化验证的根本性问题，无法通过优化算法或者工具完全解决。但是值得欣慰的是，学术界和业界也在不断探索用来缓解状态爆炸问题的各种方法。在理论上，有学者提出了以下方法，如：
符号模型验证（Symbolic Model Checking），即使用二元决策图（Binary Decision Diagrams – BDD）而非独立的状态列表来表达状态空间；
偏序约减（Partial Order Reduction），即检查各个状态和行为间的独立性以减小整体的状态空间；
基于反例的抽象优化（counterexample-guided abstraction refinement），即自适应的寻找合适的抽象层次，实现精度和运行时间的折中。
有界模型验证（Bounded Model Checking），即使用SAT（Boolean satisfiability）求解器在一定边界条件下寻找反例。
在实际应用中，业界也有一系列应对状态爆炸问题的方法，我将在下一章进行详细阐述。
那么，应该如何着手使用形式化验证？首先需要考虑如何将设计规约和需求用形式化的方法表述出来。
验证的本质就是将设计与设计规约进行一一比对的过程。在电路仿真中，通常使用参考模型（reference model）作为设计规约的实现形式。参考模型通常由高级语言，如C/C++、SystemC、MATLAB等实现，但有时也会通过RTL语言如SystemVerilog实现。与此不同的是，在形式化验证方法中，设计规约是通过形式化的语言进行抽象和描述的，而并不需要参考模型。具体而言，设计规约通常会被拆分成若干条“属性”（Property），然后通过SystemVerilog断言（SystemVerilog Assertion – SVA）来进行描述。
SVA是SystemVerilog语言的一个子集，其实它已然被广泛用于传统的电路仿真中，但使用范围比较受限，主要用来检查在仿真中某些状态（通常为异常状态）是否会发生。在形式化验证中，SVA则是作为主要的编程语言，用来描述设计规约的各条属性、对设计的行为进行建模、提供实际的约束、提取覆盖率等等。
总体而言，SVA的层次可以根据所表达的复杂度分为如下四级：
1. 布尔运算（Booleans），如
data[0] && data[1] && data[2]
2. 序列（sequence），用来表达在一段时间内发生的一系列布尔运算。因此可见序列的表示需要一个明确的时钟作为参考。例如：
req ##2 grant
这代表当req置一后再过两个时钟周期，grant再置一。
3. 属性（property），用来组合多个序列，并以此表明在设计中需要满足的某种逻辑关系。如：
A |-> B 和 A |=> B
其中A和B都为序列。本例中前者代表当A成立时，B在同一个周期内也必须成立；后者代表当A成立时，B在下一个周期必须成立。
4. 断言声明（assertion statements），用来表示对一则SVA属性所进行的动作，例如：
p1: assert property (A |-> B);
这代表将对括号内的property进行断言检查。具体来讲，断言声明通常使用以下三个关键词之一：assert，assume和cover。这三个关键词在形式化验证环境中的语义和在电路仿真中有所不同：
Assert：用来表明给定的断言声明（statement）必须在任何条件下都满足；
Assume：用来指定各种形式化验证的约束条件
Cover：用来表明在形式化验证的过程中必须要覆盖到的情况
由于篇幅所限，其他更深入的有关SVA的介绍和举例无法在本文给出。有兴趣的读者可以查看相关的文献书籍以了解更多。本文想强调的是，在形式化验证中，各种设计规约、约束条件、验证目标、覆盖点等，都是通过SVA进行表述和建模的。这样，可以把图2中所示的简单的形式化验证流程图扩展为如下图所示：
图8：扩展后的形式化验证流程
由上图和前图的对比可以看到，形式化验证引擎的输入输出都进行了一些扩展。在输入端，除了在仿真中也需要的待测模块以外，形式化验证还需要对输入进行一定的约束，并通过SVA的描述，提供待验证的断言和覆盖点。
通常来讲，使用形式化验证的第一步，并非是立即编写各种断言，而是构思需要对整个设计和验证环境添加怎样的约束。形式化约束的意义在于能很大程度上的减小状态空间，一方面能引导形式化验证工具在更加合理的状态区间中进行更有效的断言判定，另一方面能够从一开始就杜绝一些不合理的状态或条件的出现，从而避免验证出现漏报（false negative）。为形式化验证添加约束还能“强迫”设计者和验证工程师在整体上全面思考设计规约以及设计需求，从而在早期发现设计规约和需求中的漏洞和不足。
在明确各种约束条件之后，接下来需要考虑设计中存在哪些目标状态，并通过覆盖点进行覆盖。这与使用随机约束的验证方法中，提取功能覆盖率的思想比较类似。通常这些目标状态都在验证计划中给出。需要注意的是，在形式化验证中，覆盖点还有一个重要作用是防止误报（false positive）的出现。最极端的例子是，如果不给出任何断言，那么形式化验证工具就会给出全部断言都被证明的误报。因此需要覆盖点对目标状态进行覆盖，确保工具对相关断言的确进行了证明。
在形式化验证工具的输出端，通常会给出三类信息：
1.若断言得到证明，则会给出已经被证明的断言列表；
2.若断言被证明有误，则会给出一个反例（如上文所述通常为最小实例）；
3.若在有限时间之内，工具无法给出证明或反证，则会标明该断言的证明没有定论（inconclusive）。
有很多种可能性会导致出现最后一种情况，例如证明时间太短、断言及属性过于复杂等，但通常代表此时的状态空间太大，已经超出了形式化工具可以证明的范围。此时应该考虑着手减小状态空间，例如考虑简化断言、提供更多约束、尝试其他的形式化验证引擎等。也可以使用更进一步形式化验证技巧，如使用抽象模型（abstraction），设置黑盒（blackbox）或断点（cut-point），对待测设计采用分而治之的策略等。
例如对于一个大小为32位宽、512个存储单元的存储器，理论上它的状态空间存在2^(32*512)个状态， 即大约十亿的一千次方，已经远超计算机可以计算的范围。另一方面，对于存储器本身而言，其通常作为一个可配置的IP使用，对于使用存储器IP的设计而言，验证存储器自身的功能并非验证的目的。而且，我们往往可以安全的假设，存储器本身已经经过了IP提供商的完整验证，可以直接使用。此外，可以注意到每个存储器的存储单元均相互独立，很多情况下两个存储单元的内容并不会相互影响。
在这种情况下，我们可以使用针对存储器的抽象模型，只对少数存储单元进行精确建模，而不需关心其他单元，那么可以将整体的状态空间下降为2^(32*3)个状态。
对形式化验证中的抽象模型的研究一直是业界和学界的热点之一，比如，英国Imagination公司的Arshish Darbari等人曾经发表过多篇文章，详细阐述了关于FIFO、Arbiter等模块的形式化抽象方法。我的博士导师，伦敦帝国理工学院的Constantinides教授也曾对多项式数据通路的形式化验证开展过一系列理论研究工作。形式化验证咨询机构Oski也发表过一系列文章，详细讲解了诸如如何对FIFO等底层模块进行形式化抽象，如下图所示。
图9：Oski提出的FIFO形式化抽象方法
同时，形式化验证工具的提供商，如Candence和Synopsys也都提供了一些常用模块，如FIFO、存储器、乘法器等的抽象模型。
综上所述，一个较为完整的形式化验证环境会如下图所示。
图10：一个形式化验证环境示意图
在笔者眼中，形式化验证将在现代验证方法学中慢慢占有越来越重要的地位。这主要是由于形式化验证独特的工作原理，及其先天优于基于电路仿真的验证方法的各类特性。同时，形式化验证适用于多种不同的模块层级，从小规模的IP设计，到大规模的系统集成，都有可能使用形式化的方法进行验证。很多业界的公司都早已开展形式化验证的使用，比如英特尔就对其i7处理器的某核心部件全部使用形式化方法进行验证。另外，随着EDA工具的不断完善，普通的使用者，如设计和验证工程师，不需要掌握任何形式化理论或数学模型推导，这些过程都已被封装在工具中，这样大大简化了形式化验证的使用门槛。形式化验证另一个主要的作用在于，能够帮助设计者充分严谨的思考设计需求和规约，并在设计早期就能有效发现各类漏洞，而无需等待复杂的测试平台搭建完成。
另一方面，如前文提到的，形式化验证也伴随着先天的缺点，即不能有效处理拥有大量状态的设计，如存储器、数学运算器等。为了应对这样的情况，验证工程师需要掌握一些形式化验证技巧和抽象方法。此外，形式化验证与电路仿真的思考角度完全不同，一个熟练使用UVM和随机约束的验证工程师不一定能在短时间内很好的掌握形式化验证的思想和工作方法。这几点都使得形式化验证又不是那么简单易用。
因此，业界的共识在于，充分利用形式化验证和电路仿真的优点，扬长避短，在一个完整的项目周期内协同使用不同的验证方法学。业界有关项目进行时间和漏洞数量关系、修复漏洞的花费三者关系的经验图如下所示，可见在项目开发初期，是各类漏洞存在的高发期，但此时修复漏洞所需要的成本最少。等到项目行将结束并流片的时候，漏洞很难被找到，但一旦出现就往往需要花费大量成本进行修复。
图11：Bug数量、修复Bug的成本与所在的项目开发周期的关系
因此，在项目早期，可以利用形式化方法逐步完善设计规约，同时发现各类早期的问题和简单的漏洞。设计者也可以负责编写各类断言，而验证工程师负责形式化平台的搭建，以及更复杂断言的设计。与此同时，使用UVM等方法学搭建电路仿真平台，用以在更高层次（如系统集成时）、和项目中后期通过不间断的回归测试发现设计漏洞。当基本测试完成后，可以使用硬件模拟和FPGA原型设计等方法，再进行大量实际数据的测试。特别是对基于FPGA系统的设计，由于FPGA的可编程性，有条件的话可以更早进行硬件测试。
综上，在笔者看来，现代的验证方法学应该是形式化验证、电路仿真、硬件测试的三位一体的集合和统一。我也期待形式化验证方法能在业界受到更加广泛的使用。
作者简介
石侃博士，于伦敦帝国理工大学电子系取得博士学位，后加入英特尔公司可编程解决方案事业部任高级FPGA研发工程师至今。石侃在半导体行业有多年的学术研究和工业界开发经验，尤其深耕于FPGA、高性能与可重构计算、计算机网络和虚拟化等领域。他曾在多个学术界顶级会议和期刊如DAC、FCCM、TVLSI等发表过论文。在工业界，他主要从事使用FPGA进行数据中心网络加速器、网络功能虚拟化、高速有线网络通信等相关技术的研发和创新工作。
今天是《半导体行业观察》为您分享的第1551期内容，欢迎关注。
R
eading
推荐阅读（点击文章标题，直接阅读）
关注微信公众号 半导体行业观察，后台回复关键词获取更多内容
回复 兆易创新，看与兆易创新公司相关的文章
回复 摩尔定律，看更多与摩尔定律相关的文章
回复 材料，看更多与半导体材料相关的文章
回复 面板，看更多面板行业的文章
回复 晶体管，看更多与晶体管相关的文章
回复 晶圆，看晶圆制造相关文章
回复 士兰微，看更多与士兰微公司相关的文章
回复 封装，看更多与封装技术相关的文章
回复 展会，看《2017最新半导体展会会议日历》
回复 投稿，看《如何成为“半导体行业观察”的一员 》
回复 搜索，还能轻松找到其他你感兴趣的文章！
点击阅读原文了解摩尔精英