Bug打猎!螺旋在正式报道关闭

通过侯和金马克埃斯林格表示

许多公司都使用正式的验证来验证复杂的soc和安全性至关重要的设计。使用正式的验证来确认设计功能和发现功能缺陷正成为一种有效的验证方法。尽管形式验证不会处理的复杂性在SoC设计水平,它是一种有效的工具来验证设计块或IP综合。

不幸的是,关闭过程不是定义良好的正式报道。不同的公司,甚至不同的项目团队在一个公司可能使用不同的标准。有经验的形式验证用户知道如何提炼形式验证直觉的结果。然而,新用户发现这个技能挑战的主人,导致沮丧和失望。在本文中,我们抓住细化过程中循序渐进的方法,制定得更生动,这样很容易理解和复制。

形式验证的成功因素

有必要了解的因素确定正式的验证项目的成功。各种正式的团队从多个公司记录以下六个因素的成功基于他们的经历。

• 设计的复杂性
• 子目标和目标的质量断言
• 界面的完整性约束
• 正式的控制和编制引擎
• 初始状态的质量为正式的探索
• 正式的专业知识的用户

如果我们想要成功签署了设计与正式的报道,我们将不可避免地需要对付所有上面提到的成功因素。来帮助我们管理和(可能更重要的是)允许经理形象化,我们介绍了“螺旋细化”错误亨特雷达,图1。它捕获的六个因素的轴雷达图表。目标是确定的主要障碍,如正式的可用性专家或界面的完整性约束。然后我们可以逐步改善或完善其他因素实现正式报道关闭。

“螺旋细化”正式报道关闭方法

正式报道关闭过程由多个阶段和迭代。为了简化的解释,我们分类的过程分为三个阶段,如图1所示。

0 -开始阶段:原始的RTL设计

阶段1 -设置:正式的验证测试规划,配置,和抽象

2 -验证阶段:正式的证明,bug探索和改进

关闭3 -验收阶段:正式报道

图1:雷达图表形式验证的成功因素。

设置阶段的目标是收集所有必要的信息,创建一个正式的验证测试计划,并建立了正式的验证环境。在这个阶段,我们提取目标设计的功能设计规范文档。形成一个正式的验证测试计划,我们定义的配置和操作环境和捕获需求的综合列表。一旦完成测试计划,我们开始编写属性约束环境和捕获定义的需求。断言的初始阶段发展重点提炼断言和约束匹配需求。用户的正式设计知识、语言能力和经验将决定这个阶段的效率。

第二阶段的目的是验证设计中的属性和修复任何错误发现的形式验证。这是一个提纯的过程,需要不断改善的成功因素,这样我们可以确认尽可能多的属性。CPU资源是这个阶段的关键。大多数设计公司已经有一个服务器群环境设置功能模拟回归。通过约束设计基于操作的模式,抽象,和接口,我们可以建立一个多处理环境。我们可以配置正式工具派遣数百家小型工作与不同的正式服务器农场引擎和技术环境。帮助正式验证一些复杂的断言,我们应该不断完善他们的准备。技术,如分解,辅助或子目标断言,assume-guarantee是常用的。如果设计需要一个特殊的初始化序列建立正确的设计,最好是设置后开始正式的验证已经完成。

验收阶段的目的是确认充分验证已经完成,我们可以签署形式验证的块。随着验证的发展,达到一个阶段,大部分的目标场景验证。断言被证明或解雇预期(即。,消极的场景),而一些断言可能仍然是不确定的。有效正式的验证结果,在这个阶段,我们面临这些关键问题:

• 有足够的断言来覆盖所有功能的设计?
• 有没有差距断言报道关于目标功能?
• 是不确定的断言的深度足以签字的功能?

我们把正式的保险来解决这些问题。不同类型的正式报道:计算可达性报道,可观测性报道,证明核心覆盖,和有界证明覆盖。这些帮助我们理解质量的断言在设计以及实际的元素已经正式确认。同时,他们确定在遥不可及的元素设计在形式验证和潜在的过度约束。

螺旋的良好效果

看到这是如何工作的,我们将使用一个示例设计项目:一个数据包的调度器,重视并将传入的数据包根据预定的仲裁方案。图2描述了我们如何能够应用成功的六个因素在每个循环的三个阶段细化方法关闭正式报道。

图2:螺旋包调度器设计细化方法。

阶段1:设置

1. 设计的复杂性:设计的深度和广度对形式验证直接处理效率低下。为了提高效率,我们减少渠道的数量和大小,包长度,为杰出的交易数量的缓冲。这不是困难的设计很容易配置。设计团队帮助我们生成多个simple-and-true表示。
2. 可访问性的正式专家:内部正式专家帮助设计抽象过程的早期。我们已经承认他们的股东价值分析知识和正式编码技术是为项目的成功的决定性因素之一。
3. 正式的控制引擎:记忆和不重要的部件的设计变成了黑匣子。初步正式运行和可达性分析进行确认的正式的引擎有足够的控制设计。
4. 断言的质量:正式专家与设计师紧密合作创建的属性测试计划和分析潜在的失败场景设计的关键部分。我们开发了复杂的断言检查数据包的数据完整性和以信用为基础的调度方案。然后可观测性报道被用来测量断言密度,以确保足够的覆盖率的关键功能。
5. 接近的初始状态:我们用好的序列初始化设计。如图2所示,它是所有阶段保持不变。
6. 完整性约束的:外部和内部正式断言IP数据包传输协议,取得AXI总线接口,配置,和内存接口。他们对所有阶段保持不变。

阶段2:验证

1. 设计的复杂性:我们降低了设计的复杂性进一步通过定制设计抽象正式运行的焦点。这种方法允许我们推出更高效的并发正式运行。
2. 可访问性的正式专家:正式专家和工具厂商帮助分区和启动正式运行在多个服务器群环境的核心。
3. 正式的控制引擎:我们使用所有的正式运行形式验证引擎寻找证据和侵犯。我们试图尽可能有效利用多处理的四个级别。
4. 断言的质量:反馈提供的工具正式运行,发动机健康动态和活跃的逻辑被正式的验证分析。我们分解复杂的断言和添加辅助断言更好地了解正式的进展。这些断言帮助指导正式过程一旦被证实。我们继续完善数据独立性和非确定性的断言。这些进一步改进设计的可控制性和正式的效率。
5. 接近的初始状态:在第一阶段一样。
6. 完整性约束的:在第一阶段一样。

阶段3:签收

后检查证明属性和调试阶段2中的违规行为,我们专注于不确定属性在这最后阶段和正式报道。这是正式的一部分覆盖关闭方法。

1. 设计的复杂性:我们使用相同的设计抽象阶段2。
2. 可访问性的正式专家:在第二阶段一样。
3. 正式的控制引擎:我们改变了正式编制执行可观察性和可达性分析。重点是衡量正式报道证明和有界断言证据。我们利用相同的多处理环境,设置在第二阶段。
4. 断言的质量:正式覆盖计算了各种方法根据焦点和精度要求。我们专注于可观察性的报道,以确保有足够的断言和有界证明是足够深覆盖目标属性。
5. 接近的初始状态:在第一阶段一样。
6. 完整性约束的:第一阶段一样;但我们也跑了可达性分析来确认我们没有过度约束设计。

总结

多家公司已经证明,形式验证是一个可行的替代硅块级设计验收和bug狩猎。“螺旋细化”雷达和方法提供必要的指导项目团队采用这一互动过程。它抓住了成功因素,有助于指导不同的部署方法。三个phases-set,验证,signoff-help项目团队建立一个流程,安排任务,并设置评论如果需要从一个阶段到另一个地方。过程是确定任何障碍然后逐步完善或改进的成功因素,这样正式的验证可以从阶段阶段。总体目标是验证设计的功能和关闭确认完成正式报道。

更多地了解如何更有效地检测并修正错误在你的下一个设计中,阅读完整的白皮书形式验证经历:螺旋细化方法硅缺陷打猎从西门子EDA。

金侯博士是一名产品工程师,正式的IC验证系统分部的西门子EDA。侯有超过12年的正式和assertion-based验证。她曾作为CAE和PE、产品定义的经验,客户支持,工具测试、客户培训、技术营销、以及目前的体育,正式的应用程序。侯蒙特利尔大学获得博士学位,加拿大蒙特利尔。