形式化验证如何助力超大规模芯片设计？发表时间：2024-09-12 16:17 随着集成电路规模的不断扩大，从设计到流片（Tape-out）的全流程中，验证环节的核心地位日益凸显。有效的验证不仅是设计完美的基石，更是确保电路在实际应用中稳定运行的保障。尤为关键的是，逻辑或功能错误是导致流片失败的首要原因，占比高达50%。功能验证正是解决这一难题的利器，它助力工程师精准识别逻辑设计漏洞、性能不达标问题以及设计代码中的功能缺陷，从而最大限度地规避流片风险。 形式化验证是一种基于严格数学推理的设计验证技术，它摒弃了物理测试与模拟的依赖，专注于通过静态、全面的逻辑分析来确保设计的正确性。此方法显著降低了对庞大测试集的需求，并力求实现接近完美的验证覆盖率。 形式化验证的实施涉及多个关键环节： ★属性定义（Properties）：精确阐述设计需遵循的特性与规范，涵盖时序逻辑、状态转换规则及各项约束条件。 ★规约语言:采用如SystemVerilog Assertions（SVA）、Property Specification Language（PSL）等形式化规约语言，将属性与约束转化为可验证的表达式。 ★定理证明器（Theorem Provers）：依托形式化逻辑与推理机制，自动验证属性是否成立，为设计逻辑的正确性提供坚实保障。 ★模型检查器（Model Checkers）：全面探索系统状态空间，寻找可能违反预定性质的执行路径，确保设计在所有可能情况下均能满足既定要求。 形式化验证的基本流程是一个连贯且系统化的过程。这一过程从明确验证目标开始，设计团队首先需要界定哪些部分或功能需要接受形式验证的严格审查。再采用形式规约语言（如SystemVerilog Assertions、PSL）定义属性和规约，作为验证基础。进入验证环境配置阶段，团队选择适合的验证工具（定理证明器、模型检查器），并依据设计特性和需求进行优化配置，以确保验证效率与准确性。 验证执行为核心，定理证明器通过数学推理验证属性与规约的正确性，模型检查器则全面探索系统状态空间，检查违规执行序列。验证结束后，团队分析验证结果，识别并修正设计中的错误或不一致。此过程可能多次迭代，直至设计完全符合验证要求。 二 形式化验证工具的优势 形式化验证是一种基于数学推理的验证方法，通过对芯片设计的数学模型进行全面而严谨的分析，可以发现潜在的设计错误、漏洞和安全隐患。相较于动态验证而言，形式化验证至少有四个无可替代的重要优势。 ★验证空间完备性：当所有输入端的每个信号，每一时钟周期都只有0或1两种取值，那么任何一种测试场景都是完备测试空间的一个时空二维的子集。通过对RTL转化成形式化验证模型，将功能验证问题转化成了给定行为的数学推导，进而对完备验证空间进行遍历。 ★精准定位错误场景：一旦有一个设计场景导致断言不成功，会精准给出特定时钟下的特定波形。而传统的动态验证是基于Log进行debug，需要从事务级进行推导，逐级定位可能的设计问题。 ★验证环境简单高效：不需要搭建复杂、层次繁多的验证环境，针对待测试场景精准描述Property，进而进行输入场景遍历和推导证明。 ★覆盖率收集脱离工程师人为风险：形式化验证覆盖率收集方案是基于算法和模型由工具自发完成，整个过程不依赖于人工定义function coverage，这极大程度地避免了因人为失误导致的覆盖率准确度不高的风险。总体来说，形式化验证技术效率高，完备性强，是发现人类正常思维以外的corner bug的利器，有利于尽快、尽早的发现并协助改正电路设计中的错误，提高设计质量，缩短芯片设计周期。 总体来说，形式化验证技术效率高，完备性强，是发现人类正常思维以外的corner bug的利器，有利于尽快、尽早的发现并协助改正电路设计中的错误，提高设计质量，缩短芯片设计周期。 三 望安科技助力芯片安全领域 望安科技作为一家以“形式化验证”为核心技术的安全服务及产品提供商，已在形式化验证领域深耕多年，公司拥有的形式化验证核心技术，在领域内已达到了国际先进水平。望安科技全面支持国家重大项目、关键系统及行业企业信息安全、认证保障，安全产品及服务面向航空航天、国防、轨道交通、区块链、互联网金融、物联网、芯片设计制造等重大领域。 在芯片设计过程中，安全性是一个至关重要的考虑因素。芯片的安全性问题可能导致信息泄露、入侵攻击以及系统崩溃等严重后果。望安科技通过形式化验证技术，可以对芯片设计进行全面的安全性验证，发现潜在的安全漏洞和攻击路径，确保芯片在各种威胁下的安全性和正确性，为芯片制造商和应用开发者提供可靠的安全保障。 |
