新闻动态
形式化验证如何助力超大规模芯片设计？
来源: | 作者:望安科技 | 发布时间: 8天前 | 55 次浏览 | 分享到:

★模型检查器（Model Checkers）：全面探索系统状态空间，寻找可能违反预定性质的执行路径，确保设计在所有可能情况下均能满足既定要求。

形式化验证的基本流程是一个连贯且系统化的过程。这一过程从明确验证目标开始，设计团队首先需要界定哪些部分或功能需要接受形式验证的严格审查。再采用形式规约语言（如SystemVerilog Assertions、PSL）定义属性和规约，作为验证基础。进入验证环境配置阶段，团队选择适合的验证工具（定理证明器、模型检查器），并依据设计特性和需求进行优化配置，以确保验证效率与准确性。

验证执行为核心，定理证明器通过数学推理验证属性与规约的正确性，模型检查器则全面探索系统状态空间，检查违规执行序列。验证结束后，团队分析验证结果，识别并修正设计中的错误或不一致。此过程可能多次迭代，直至设计完全符合验证要求。

二

形式化验证工具的优势

形式化验证是一种基于数学推理的验证方法，通过对芯片设计的数学模型进行全面而严谨的分析，可以发现潜在的设计错误、漏洞和安全隐患。相较于动态验证而言，形式化验证至少有四个无可替代的重要优势。

★验证空间完备性：当所有输入端的每个信号，每一时钟周期都只有0或1两种取值，那么任何一种测试场景都是完备测试空间的一个时空二维的子集。通过对RTL转化成形式化验证模型，将功能验证问题转化成了给定行为的数学推导，进而对完备验证空间进行遍历。

★精准定位错误场景：一旦有一个设计场景导致断言不成功，会精准给出特定时钟下的特定波形。而传统的动态验证是基于Log进行debug，需要从事务级进行推导，逐级定位可能的设计问题。

★验证环境简单高效：不需要搭建复杂、层次繁多的验证环境，针对待测试场景精准描述Property，进而进行输入场景遍历和推导证明。

★覆盖率收集脱离工程师人为风险：形式化验证覆盖率收集方案是基于算法和模型由工具自发完成，整个过程不依赖于人工定义function coverage，这极大程度地避免了因人为失误导致的覆盖率准确度不高的风险。总体来说，形式化验证技术效率高，完备性强，是发现人类正常思维以外的corner bug的利器，有利于尽快、尽早的发现并协助改正电路设计中的错误，提高设计质量，缩短芯片设计周期。

总体来说，形式化验证技术效率高，完备性强，是发现人类正常思维以外的corner bug的利器，有利于尽快、尽早的发现并协助改正电路设计中的错误，提高设计质量，缩短芯片设计周期。

NEWS