【形式化验证】从小众走向普及，在芯片领域发挥重要作用
来源:
|
作者:望安科技
|
发布时间: 337天前
|
623 次浏览
|
分享到:
形式化验证作为一种全新的验证方法，近年来在芯片开发中快速发展，正逐渐取代传统的仿真方法。
虽然仿真在系统级验证方面仍然发挥着重要的作用，但对于单元级的signoff而言，形式化验证已经成为首选。据估计，在未来五年内仿真将逐渐被取代，仅用于子系统和系统级验证。与此同时，形式化验证方法已经开始处理一些系统级任务，随着技术的不断创新，形式化验证将逐步开始处理更多系统级任务。
近五年来，更多机构和设计验证人员更广泛地参与到了整体验证目标之中。除了率先在半导体设计中采用形式化验证技术的英特尔公司以外，还有很多其他半导体和系统公司的开发者们开始积极地尝试这一技术。
这种扩张一定程度是因为验证结果比以往更加容易获取，以及可以被更好地量化。“应用程序”概念的出现极大地缩短了有效验证的学习曲线，对覆盖率定义的改进也让开发者们更加相信，形式化验证以得到有效衡量。此外，属性检查证明了形式化验证可以解决仿真所无法解决的难题。
一旦有一个设计场景导致断言不成功，会精准给出特定时钟下的特定波形。而传统的动态验证是基于Log进行debug，需要从事务级进行推导，逐级定位可能的设计问题。
形式化验证是一种基于数学推理的验证方法，通过对芯片设计的数学模型进行全面而严谨的分析，可以发现潜在的设计错误、漏洞和安全隐患。相较于动态验证而言，形式化验证至少有四个无可替代的重要优势。
当所有输入端的每个信号，每一时钟周期都只有0或1两种取值，那么任何一种测试场景都是完备测试空间的一个时空二维的子集。通过对RTL转化成形式化验证模型，将功能验证问题转化成了给定行为的数学推导，进而对完备验证空间进行遍历。
一旦有一个设计场景导致断言不成功，会精准给出特定时钟下的特定波形。而传统的动态验证是基于Log进行debug，需要从事务级进行推导，逐级定位可能的设计问题。
不需要搭建复杂、层次繁多的验证环境，针对待测试场景精准描述Property，进而进行输入场景遍历和推导证明。
形式化验证覆盖率收集方案是基于算法和模型由工具自发完成，整个过程不依赖于人工定义function coverage，这极大程度地避免了因人为失误导致的覆盖率准确度不高的风险。
