| ||
形式验证用来发现错误还是签字确认(signoff)?
后来Sabbagh将谈话引向了一个新问题。“我们应该使用形式验证来发现错误还是签字确认? 优缺点都有什么?”
第一个回应是“我们一开始将形式验证用于寻找缺陷,这已经是被证明非常成功的。缺点是没有一个明确的指标来衡量验证的进度。”
参与者对于签字确认意味着什么同样存在着一些分歧。一位参与者试着提供一个定义“签字确认意味着我将对后续发现的每一个缺陷负责。如果你在子系统的验证、模拟或者这个芯片上发现了一个缺陷,那么我将对其进行解释。这可能是由于人为的错误,也可能是因为我少放了一个检查器,但总会有一个原因。”
他们还对形式验证和仿真验证的角色进行了划分。“在我们的世界里,模块总是更大的系统的一部分,这需要使用仿真验证。所以即使某一部分可以使用形式验证,端到端的仿真仍然是必不可少的。所以我们不会放弃仿真验证的使用。”
他们讨论了如何更合适的使用这两种验证方式。“这意味着仿真验证可能在某些时候并不是一个好的选择,但我们仍需要进行系统级的仿真。当发现一个缺陷的时候,它需要被定位。举例来说,对于一个系统中的仲裁逻辑,我们可以使用形式验证来证明它的正确性,但端到端的仿真扔是必不可少的。唯一可以从仿真验证中减少的可能就是这部分逻辑的一些检查器。”
这一点似乎难以达成共识。“无论你将设计的层级怎么划分,是在模块级别进行划分或者子系统级别进行划分,都是为了消除错误。在进行了几周的随机激励测试后,如果在一个比较高的层级发现了错误,你会考虑采取什么措施来提高低级别的验证质量。会对在模块级别进行仿真验证或者形式验证,以增加能发现所有缺陷的信心。”
“从项目管理者的角度来看,当你说签字确认时,我能对此做什么样的理解呢?应该是只要形式验证能够胜任的部分,你都应该利用它来对这一部分进行完全的验证。”
一位与会者试图以IP块作为例子。“从覆盖率的角度考虑IP块的话,如果它已经经过了硅上的验证,你正在把它集成到一个系统内,看系统能否正确工作,这时并不需要记录IP的覆盖率。你可以把IP块当成一个黑盒,不必击中它的每个验证角落。”
一些与会者不同意这一观点。“当你把IP块引入一个系统中时,在系统级是看不到它在模块级与其它的模块的联系的,但是这意味着你激励的约束可能会出现问题。”
他们就覆盖率展开了讨论。“覆盖率存在的一个原因是它可以衡量一个验证环境的健壮程度。你不能将它的一部分从仿真环境中去除,因为这样就无法衡量这个验证环境的健壮程度。无论在仿真环境还是形式验证环境中,IP相关的覆盖率事件都需要被激活。”
“对我来说将形式验证用于发现错误还是确认签字,这是项目管理者的决策,而不是技术上的决策。如果仿真验证和形式验证共同存在,对于一个模块来讲有什么危害吗?必须在二者之中选择一个吗?”
大部分参与者都陷入思考。“当形式验证不太适用的时候,你可能会转向仿真验证。但是当形式验证更合适的时候……通常来讲,你用它来发现了缺陷,那这算是用于寻找缺陷呢还是用于签字确认呢?可能两者都有。”
还有一些反对意见,因为这意味着重复工作。“你必须弄清楚如何使用好现有的资源。有些情况下,形式验证的效果非常好,同时形式验证和仿真验证存在重叠部分,但是你不必因为哪些部分会重叠而重新制定验证目标,这有些过分。”
一位参与者试图理清验证流程。“这实际上是单元级别的验证到系统级别的验证的区别。我们有一个普遍的原则,希望尽可能早的在项目中发现尽可能多的缺陷。我们想要说的是形式验证在单元级别的表现非常好,并且没人会争辩说单元级别的形式验证会让你系统级别的验证无法进行。”
“你在依赖于更高级别的仿真验证来发现单元级别验证的问题!”。当谈话再次回到签字确认的问题时,谈话成了一个循环。“你正在发现缺陷,直到没有缺陷。你在努力发现错误的时候是怎么做的呢?你必须一直询问自己:是否验证的足够充分,可以来签字确认?所以为什么一定要把它们两个分开呢?”
一个回应是:“这是一个连续的过程。你从签字确认的目标开始,编写一些属性来发现一些缺陷,然后不断添加属性直到把整个签字确认的属性都验证到。但是你可能会遇到一些复杂的问题,并且……”
“这是一个项目时间的问题。在项目结束前,你希望能够一直停留在发现错误的阶段。你可以进一步推动验证的范围,并且发现系统中更深入的错误。”
看上去一个结论总是出现在另一个结论中。也许它们真正的区别是最初确定的目标和跟踪完成这一目标的质量。
原文来自于Semiengineering “Can Formal Replace Simulation?”
https://semiengineering.com/can-formal-replace-simulation/