EDA形式化验证漫谈：仿真之外，验证之内

“在未来五年内仿真将逐渐被淘汰，仅用于子系统和系统级验证。与此同时，形式化验证方法已经开始处理一些系统级任务。随着技术发展，更多Formal相关的商业标准化会推出。”

Intel fellow 

M. V. Achutha Kiran Kumar

随着Formal技术的发展，业内已经有不少公司有专门的形式化验证团队，也培养了一批热爱Formal，愿意来钻研这门技术的EDA人。

仿真方法学是动态验证的一种，是一个“你想到哪里才能验到哪里”的验证方式，本质上在不断做加法。你需要先让自己尽可能多地想到各种场景、耗费大量时间搭建测试环境，再试图“碰出BUG”，但是这种方式更擅长发现设计“这里有BUG”，但却很难回答“那里没有BUG”的问题。

这方面形式化验证工具有很大的优势。

形式化验证则被称为静态验证，是一种基于严格的数学与算法的验证方法学。用户利用SVA断言描述清楚需要证明的设计规格，通过编译RTL和基于SVA的断言语言，建立Formal模型，然后不断做减法，发现不符合模型的“反例”。

显而易见的一个优势是，形式化验证工具能够通过建立数学模型，实现更敏捷的反向验证，以类似数学定理证明的方式，通过对所有可能的激励空间进行遍历，保证逻辑没有死角，实现验证的完备化、自动化。

传统的仿真工具，在进入具体发现bug阶段前，往往需要很长时间为UVM搭建一个完备的验证平台（testbench）；而在调试（Debug）阶段，当出现UVM error，需要问题定位时，仿真工具一般需要从UVM繁杂的log到rtl再到waveform、信号级别，这也是一个很长的回溯曲线。形式化验证在这两个方面，则可以节省很多时间，尤其是通过直接提供反例波形，可以精准直指相关信号进行问题定位。

早期大家可能会担心，觉得Formal工具是不是有使用门槛，这种担心来源于形式化验证工具使用过程中，需要基于对设计的全面理解，才能正确构建验证模型的断言和约束。

一方面，形式化验证对验证工程师而言，确实能够大大的减轻焦虑，芯华章2021年推出GalaxFV，并且在项目的打磨中，持续不断地在丰富应用级断言库，并对其参数化、提高可配置性，让GalaxFV更加容易使用。

另外，随着设计规模增加，工具更加的自动化、智能化，理解设计会成为工程师的一大优势！用好Formal工具，项目将不再需要靠堆人、堆license、堆时间来提高验证质量。