【形式化验证】从小众走向普及，在芯片领域发挥重要作用
来源:
|
作者:望安科技
|
发布时间: 338天前
|
624 次浏览
|
分享到:
形式化验证作为一种全新的验证方法，近年来在芯片开发中快速发展，正逐渐取代传统的仿真方法。
虽然仿真在系统级验证方面仍然发挥着重要的作用，但对于单元级的signoff而言，形式化验证已经成为首选。据估计，在未来五年内仿真将逐渐被取代，仅用于子系统和系统级验证。与此同时，形式化验证方法已经开始处理一些系统级任务，随着技术的不断创新，形式化验证将逐步开始处理更多系统级任务。
近五年来，更多机构和设计验证人员更广泛地参与到了整体验证目标之中。除了率先在半导体设计中采用形式化验证技术的英特尔公司以外，还有很多其他半导体和系统公司的开发者们开始积极地尝试这一技术。
这种扩张一定程度是因为验证结果比以往更加容易获取，以及可以被更好地量化。“应用程序”概念的出现极大地缩短了有效验证的学习曲线，对覆盖率定义的改进也让开发者们更加相信，形式化验证以得到有效衡量。此外，属性检查证明了形式化验证可以解决仿真所无法解决的难题。
一旦有一个设计场景导致断言不成功，会精准给出特定时钟下的特定波形。而传统的动态验证是基于Log进行debug，需要从事务级进行推导，逐级定位可能的设计问题。
形式化验证是一种基于数学推理的验证方法，通过对芯片设计的数学模型进行全面而严谨的分析，可以发现潜在的设计错误、漏洞和安全隐患。相较于动态验证而言，形式化验证至少有四个无可替代的重要优势。
当所有输入端的每个信号，每一时钟周期都只有0或1两种取值，那么任何一种测试场景都是完备测试空间的一个时空二维的子集。通过对RTL转化成形式化验证模型，将功能验证问题转化成了给定行为的数学推导，进而对完备验证空间进行遍历。
一旦有一个设计场景导致断言不成功，会精准给出特定时钟下的特定波形。而传统的动态验证是基于Log进行debug，需要从事务级进行推导，逐级定位可能的设计问题。
不需要搭建复杂、层次繁多的验证环境，针对待测试场景精准描述Property，进而进行输入场景遍历和推导证明。
形式化验证覆盖率收集方案是基于算法和模型由工具自发完成，整个过程不依赖于人工定义function coverage，这极大程度地避免了因人为失误导致的覆盖率准确度不高的风险。
总体来说，形式化验证技术效率高，完备性强，是发现人类正常思维以外的corner bug的利器，有利于尽快、尽早的发现并协助改正电路设计中的错误，提高设计质量，缩短芯片设计周期。
五年前，有人可能认为形式化验证是解决专门问题的小众技术，但这种观点现在已经逐渐被改变。现在，大型系统和半导体公司将形式化验证视为任何可信验证策略的重要组成部分。更重要的是，形式化验证方法现在已经发展到可在某些领域中取代仿真的地步。形式化验证开始为系统级领域做出贡献，而在以前，形式化验证在这些领域被认为是不切实际的。
对于形式化验证和形式化验证团队来说，这是一个令人兴奋的时代。由于贡献不断增大和在业务关键型需求上为人们带来的更多信心，形式化验证技术对所有数字设计领域的产品设计和开发变得越来越重要。
望安科技作为一家以“形式化验证”为核心技术的安全服务及产品提供商，已在形式化验证领域研究多年，公司拥有的形式化验证核心技术，在领域内已达到了国际先进水平。望安科技全面支持国家重大项目、关键系统及行业企业信息安全、认证保障，安全产品及服务面向航空航天、国防、轨道交通、区块链、互联网金融、物联网、芯片设计制造等重大领域。
在芯片设计过程中，安全性是一个至关重要的考虑因素。芯片的安全性问题可能导致信息泄露、入侵攻击以及系统崩溃等严重后果。望安科技通过形式化验证技术，可以对芯片设计进行全面的安全性验证，发现潜在的安全漏洞和攻击路径，确保芯片在各种威胁下的安全性和正确性，为芯片制造商和应用开发者提供可靠的安全保障。
