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

引言


随着集成电路规模的不断扩大，从设计到流片（Tape-out）的全流程中，验证环节的核心地位日益凸显。有效的验证不仅是设计完美的基石，更是确保电路在实际应用中稳定运行的保障。尤为关键的是，逻辑或功能错误是导致流片失败的首要原因，占比高达50%。功能验证正是解决这一难题的利器，它助力工程师精准识别逻辑设计漏洞、性能不达标问题以及设计代码中的功能缺陷，从而最大限度地规避流片风险。
针对超大规模集成电路（VLSI）设计，目前功能验证有两种方法：动态仿真验证和形式化验证（Formal Verification）。形式化验证采用数学方法来比较原设计和修改设计之间的逻辑功能的异同，而动态仿真验证是对两设计施加相同的激励后，观测电路对激励的反应异同。
面对大型设计，传统的动态仿真验证方法在覆盖率和效率上面临挑战。为了达到100%的覆盖率，动态仿真验证所需要的矢量就会越多，这时形式化验证在这方面就有优势了，成为现代IC设计验证流程中的关键一环。

一

什么是形式化验证

形式化验证是一种基于严格数学推理的设计验证技术，它摒弃了物理测试与模拟的依赖，专注于通过静态、全面的逻辑分析来确保设计的正确性。此方法显著降低了对庞大测试集的需求，并力求实现接近完美的验证覆盖率。
形式化验证作为EDA、数学及编程语言等多学科交叉的产物，自上世纪90年代起便崭露头角，最初应用于RTL代码与门级网表的LEC（逻辑等价性检查），随后逐步扩展到各类EDA工具，以应对不同验证场景的需求。
目前，形式化验证主要分为两个技术方向：等价性检查和属性检查。其中。等价性检查，作为核心验证手段，通过对比功能验证后的HDL设计与综合后的网表功能，确保两者在功能层面上的完全一致，从而保证门级电路与寄存器传输级（Register Transfer Level, RTL）模型之间的一致性。这一方法有效防范了综合工具潜在的缺陷及人为误操作，对于提升设计质量至关重要。

形式化验证的实施涉及多个关键环节：

★属性定义（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的利器，有利于尽快、尽早的发现并协助改正电路设计中的错误，提高设计质量，缩短芯片设计周期。

三

望安科技助力芯片安全领域

望安科技作为一家以“形式化验证”为核心技术的安全服务及产品提供商，已在形式化验证领域深耕多年，公司拥有的形式化验证核心技术，在领域内已达到了国际先进水平。望安科技全面支持国家重大项目、关键系统及行业企业信息安全、认证保障，安全产品及服务面向航空航天、国防、轨道交通、区块链、互联网金融、物联网、芯片设计制造等重大领域。

在芯片设计过程中，安全性是一个至关重要的考虑因素。芯片的安全性问题可能导致信息泄露、入侵攻击以及系统崩溃等严重后果。望安科技通过形式化验证技术，可以对芯片设计进行全面的安全性验证，发现潜在的安全漏洞和攻击路径，确保芯片在各种威胁下的安全性和正确性，为芯片制造商和应用开发者提供可靠的安全保障。

文章部分内容来源：思尔芯S2C


END


浙江望安科技有限公司

浙江望安科技有限公司是以“形式化验证”和“安全认证”为核心的安全服务及产品提供商。公司致力于为国家重大项目、关键系统及行业企业提供安全保障。业务覆盖航空航天、国防、轨道交通、区块链、物联网、工业控制、芯片设计、操作系统、数据库等重大行业。


公司提供信息技术安全评估标准CC EAL1-EAL7级安全保障级别、IEC 61508、ISO 26262、GM/T国密以及FIPS等高等级安全认证咨询与技术服务，已与国内外多个认证/检测机构建立联合实验室、签署合作协议等。公司拥有自主知识产权的软件源码形式化测试与验证工具W-AVC、基础软硬件形式化建模与验证工具W-Cert、CC安全认证全周期实施平台W-CaaS等工具平台。公司核心技术和工具已应用于载人航天工程、中航工业集团、航天科技集团、航天科工集团、中国信科、小米科技、中国移动、中科海微、元心科技等，覆盖国家重点行业及企业。


联系我们

公司官网: www.wonsec.com

联系方式: 400-675-8118 

公司邮箱: wangan@wonsec.com


NEWS