近年来，由于集成电路规模不断扩大、复杂度日益提高，使得对确保芯片功能正确性、完整性最重要一环的验证技术面临一系列的巨大挑战。如何保证快速、高效地实现对更大规模电路，进行全面有效的验证是目前芯片设计行业不得不去面对并解决的痛点。传统基于电路的仿真技术，一直存在诸多问题且无法有效解决，比如，对极端情况无法覆盖、过长的仿真时间、测试环境搭建等。而业界也在不断探索一些更为有效的验证方法学，比如，形式化验证，便携式激励标准(PSS)等。
形式化方法是一种基于严格的数学与算法的验证方法学。在芯片验证上，用户利用SVA断言描述清楚需要证明的设计规格，通过编译RTL和基于SVA的断言语言，建立Formal模型。一方面根据设计spec的要求，提取需要验证的功能点，进而通过SVA断言语言，逐个描述与定义待检查的功能场景。另一方面约束非法场景的发生，并自动进行数学分析和证明，通过对所有可能的激励空间进行遍历，保证逻辑没有死角。相较于动态验证而言，形式化验证至少有四个无可替代的重要优势。
形式化验证四大优势
01 验证空间完备性
当所有输入端的每个信号，每一时钟周期都只有0或1两种取值，那么任何一种测试场景都是完备测试空间的一个时空二维的子集。通过对RTL转化成形式化验证模型，将功能验证问题转化成了给定行为的数学推导，进而对完备验证空间进行遍历。
02 精准定位错误场景
一旦有一个设计场景导致断言不成功，会精准给出特定时钟下的特定波形。而传统的动态验证是基于Log进行debug，需要从事务级进行推导，逐级定位可能的设计问题。
03 验证环境简单高效
不需要搭建复杂、层次繁多的验证环境，针对待测试场景精准描述Property，进而进行输入场景遍历和推导证明。
04 覆盖率收集脱离工程师人为风险
形式化验证覆盖率收集方案是基于算法和模型由工具自发完成，整个过程不依赖于人工定义function coverage，这极大程度地避免了因人为失误导致的覆盖率准确度不高的风险。
总体来说，形式化验证技术效率高，完备性强，是发现人类正常思维以外的corner bug的利器，有利于尽快、尽早的发现并协助改正电路设计中的错误，提高设计质量，缩短芯片设计周期。
芯华章穹瀚GalaxFV就是这样一种面向HDL电路设计的形式化验证工具，能够从数学上完备地证明“电路的实现方案是否满足了设计规范所描述的功能”。GalaxFV在保留形式化验证完备性的基础上，依托于芯华章智V验证平台（FusionVerify Platform）, 与其他验证工具在编译、调试、覆盖率等方面互融互通，进一步加速设计验证收敛，帮助芯片设计在更早期阶段，完成简单高效的完备验证，从而极大地提升验证效率。
使用GalaxFV的验证实例
以下实例是中国研究生创“芯”大赛中，深圳大学参与芯华章企业命题“纠错编解码算法实现和验证”的优秀作品。
基于Verilog语言设计的信道纠错编解码算法实现模块
下面我们对一个基于Verilog语言设计的信道纠错编解码算法实现模块，使用GalaxFV来构建形式化验证流程。
该模块是通信领域芯片中，为了保障信息传输连续不失真，而进行的信道纠错的设计。它通过对原始五个信道编码扩容成七个通道，并且在这七个通道中至多任意两个通道损坏的情况下，能够通过解码来恢复原始输入端五个信道的数据。
该设计具有各种设计规格，每一个设计规格可以用一条SVA属性(property)来描述（如图所示），最终对应一个个验证目标(Goals)。
在形式化验证中，我们用约束(assume)Property来构造验证激励，其中‘asm_ch’对应第一个设计规格，这条属性可描述为：信道注错使能（低有效）信号‘channel’至少需要有5个比特位的数值为1，即发生损毁的通道数最多为2个。
形式化验证通过断言(assert)属性来实现功能检查。而‘ast_sym_data_0’则对应第二个设计规格，这条属性可描述为：在复位结束之后的每一个时钟周期，如果信道0的输入数据为标记数据，那么从当前周期开始的四个周期后，信道0的输出数据都会等于标记数据。其中标记数据为常量，下方的波形图展示了该属性的预期行为。
实例中的形式化验证环境展示
首先，我们需要通过约束属性来规避不符合设计需求的激励。其次，我们需要对特殊的信号（比如时钟与复位信号）进行定义，以保证工具能够对这些信号做合适的处理。除此之外，我们通过自研的scoreboard进行数据一致性的检查。
GalaxFV依靠自主研发的字级建模方法，可将百万行级别的设计代码转化为数学模型，把验证问题转化成数学求解问题，然后依靠求解器进行求解。而求解器就像“操作系统”，对数学上高度复杂的系统进行分解并给出最终的证明结果。
同时GalaxFV具备动态智能调度，就好比有一个“控制中心”，可根据验证目标的特征匹配出最佳方案，因地制宜地选用不同的“操作系统”进行求解。最后通过分布式计算将设计 “分而治之”。对于一个大规模的计算问题，GalaxFV可将它分成一些可以同时进行的小任务，让多个计算机对它们分别进行处理，最终得到验证结果。
产品亮点
采用高性能字级建模（Word-Level Modeling）方法构建
相比于比特级建模（Bit-Level Modeling）方法, 字级建模方法具备以下优势：
Ⅰ.建模颗粒度大
Ⅱ.性能表现好
Ⅲ.可同时调用字级求解器和比特级求解器
Ⅳ.可扩展性能力强
Ⅴ.自主研发的专用、高效的应用级断言库
GalaxFV对于设计中常用到的标准组件构建了专用、高效的应用级断言库，对其参数化，提高可配置性，降低了用户构建断言与约束的难度。可充分利用算力，提高并行效率的同时，提高易用性和使用效率，为形式化验证应用于产业降低了门槛。
搭载自研的高并发、高性能求解器
GalaxFV在服务器集群或云平台上发挥分布式计算的强大性能，为快速证明求解赋能。并且，GalaxFV研发了针对求解器的智能分组和调度预测算法，结合每种引擎的算法和特性，在面对不同的设计和断言类型时，组合调度各个求解器单元进行求解，进一步提高求解效率。
结合了这些技术特点，GalaxFV在一些客户设计上给出了亮眼的性能表现，相比于现有的业界知名形式化验证工具，实测性能超越其约20%。（ 仅针对某AsyncFIFO设计实测得出Measured only for a certain AsyncFIFO design）
芯华章穹瀚GalaxFV采用数学方法来求解验证难题，是对仿真技术的有力补充，先进的建模方法与调度算法，在我们的rtllib模块性能实测中，性能表现优秀，对工程应用有很高的价值。
—— 周孝斌，天数智芯形式验证专家
形式化验证基于数学思维进行验证求解，具备极高的可靠性，可以大大缩短开发周期。面对形式化验证工具使用门槛较高的难点，芯华章研发团队采用了字级建模方法构建，并搭载自主研发的专用断言库与求解器，让具有高完备性优势的形式化验证工具，能够帮助更多的芯片研发工程师在项目开发初期，尽早地发现问题、快速修复。
—— 齐正华，芯华章科技研发副总裁