形式化验证作为一种全新的验证方法,近年来在芯片开发中快速发展,正逐渐取代传统的仿真方法。
虽然仿真在系统级验证方面仍然发挥着重要的作用,但对于单元级的signoff而言,形式化验证已经成为首选。据估计,在未来五年内仿真将逐渐被取代,仅用于子系统和系统级验证。与此同时,形式化验证方法已经开始处理一些系统级任务,随着技术的不断创新,形式化验证将逐步开始处理更多系统级任务。
近五年来,更多机构和设计验证人员更广泛地参与到了整体验证目标之中。除了率先在半导体设计中采用形式化验证技术的英特尔公司以外,还有很多其他半导体和系统公司的开发者们开始积极地尝试这一技术。
这种扩张一定程度是因为验证结果比以往更加容易获取,以及可以被更好地量化。“应用程序”概念的出现极大地缩短了有效验证的学习曲线,对覆盖率定义的改进也让开发者们更加相信,形式化验证以得到有效衡量。此外,属性检查证明了形式化验证可以解决仿真所无法解决的难题。
这些成功的案例激发了开发者们对形式化验证更深入的思考:作为一种有效的验证技术,形式化验证是否只适用于特殊情况,或者是否有可能显著提高整体验证任务的贡献?
考虑到数据路径元件在GPU、DSP、AI和当今许多其他加速器中的重要性,突破数据路径边界是利用形式化验证技术完成绝大多数单元signoff任务的关键一步。这种从动态signoff到形式化signoff的变化,大大提升了生产力。而以往的实验证明,用这一方法signoff的一些关键模块在多代产品中没有出现一个错误。运用形式化技术达到了更高的生产率和更高的质量,这一点已然被证实。
目前企业倾向于开展基础培训来帮助应届毕业生了解和进入行业,在接受培训后,形式化验证开发者往往对工作的热情要远高于其他人,而在大学校园内,亦设置了EE/CS本科相关课程来支持行业对形式化验证开发人才的需求,期待相关专家人才迅速增多,去探索自己职业所面临的挑战和机遇。
形式化验证未来展望
五年前,有人可能认为形式化验证是解决专门问题的小众技术,但这种观点现在已经逐渐被改变。现在,大型系统和半导体公司将形式化验证视为任何可信验证策略的重要组成部分。更重要的是,形式化验证方法现在已经发展到可在某些领域中取代仿真的地步。形式化验证开始为系统级领域做出贡献,而在以前,形式化验证在这些领域被认为是不切实际的。
对于形式化验证和形式化验证团队来说,这是一个令人兴奋的时代。由于贡献不断增大和在业务关键型需求上为人们带来的更多信心,形式化验证技术对所有数字设计领域的产品设计和开发变得越来越重要。