得到一个统一的项目级视图的验证状态。
不久前,形式验证被认为是一种奇异的技术只有通过专家用于特定的验证的挑战,如缓存一致性。芯片的规模和复杂性不断增长,传统的仿真验证方法不能保持同步。的任务生成和运行足够测试消耗巨大的资源方面的工程师,模拟许可证和服务器。然而,即使无限仿真能力不能保证提供的功能的正确性。Constrained-random模拟,由于其本身的性质,是概率和几乎没有机会锻炼足够的设计找到深,个别案例bug。
由于这些原因,验证工程师越来越多地转向正式。他们高度重视锻炼的能力100%的设计行为,发现掩盖错误,数学证明没有缺陷依然存在。今天,几乎每个芯片开发团队至少有一些使用正式的技术。应用程序(应用程序)自动处理许多常见的验证任务,标准化的断言语言提供了跨工具可移植性,正式的引擎(“解决者”)是更强大的,和调试工具有所改善。方法提供指导,甚至给新用户成功的信心。
尽管有这些进步,使用正式的一个重要方面,没有很好地解决直到最近:集成的结果和覆盖率指标与仿真。一个统一的视图的验证状态是必不可少的工程领导和项目经理。他们需要考虑精力形式验证模拟域使用熟悉的措施和方法。采用正式允许更完整的验证和降低总体验证工作。经理决定工具和方法寻找这些好处的证据。
正式的工具总是生成结果和覆盖范围,但看这个数据独立于模拟不提供经理需要的项目级别的视图。从正式和仿真结果和覆盖范围必须集成提供这一观点。集成可以归结为三个主要的要求:使用正式的覆盖率分析来提高仿真效率,并排展示观点的正式和仿真结构覆盖率,和注释正式和仿真结果变成一个全面的验证计划。
的原因之一,仅模拟验证的不足是测试可能运行数天或数周努力打击覆盖目标实际上是遥不可及的。幸运的是,形式验证可以分析覆盖目标,确定unreachability,并将此信息传递给观众报道。这可以防止验证团队浪费任何时间在模拟试图达到这些目标,主要提高验证效率。此外,覆盖观众可以调整指标,这样遥不可及的目标不要人为地压低覆盖完成百分比。总的来说,正式unreachability分析显著加速关闭覆盖的过程。
第二种方法,正式可以集成模拟贡献自己的覆盖率。模拟覆盖显示测试是否达到一个特定的目标。这有助于识别领域的设计没有行使。然而,仅仅触及覆盖目标并不意味着一个错误的设计可以被探测到。解决这个问题的唯一方法是使用突变,插入错误的设计和运行测试是否检测到的错误。这增加了大量的模拟和开销是很少使用作为验证过程的一部分。
正式的、基于模型的变异分析是自动的和更有效。不需要改变设计规范;没有仪器或重新编译步骤。所得到的指标显示设计中错误的部分不会被任何断言。这些信息有助于确定设计是否有足够的断言,应该添加额外的断言。基于模型的变异范围允许有意义的集成模拟覆盖。验证团队和项目经理可以查看正式和模拟并排覆盖率结果,减少工作重叠,并加快审核,从而最大化投资回报(ROI)的形式验证工作。
最后,它是至关重要的,正式的结果是反映在验证计划。现代规划工具允许定义相关的设计要求产品规格。需求分为设计特性,然后验证步骤来测试这些功能。仿真结果注释回计划,以便经理知道,当所有的测试已经成功运行。同样的,正式的工具可以注释结果回计划展示当他们完成验证过程的一部分。这提供了一个统一的视图的验证进度,帮助确定下一步行动和决定何时准备tape-out设计。
在过去的几年中,特定于供应商的解决方案提供所有这三个集成点已经出现。然而,验证团队不想被限制在一个单一的供应商的流。这抑制创新,使得它不可能从多个EDA供应商选择的最佳工具。最近这个限制被引入OneSpin PortableCoverage的解决方案,它允许正式工具集成模拟器,覆盖数据库,覆盖观众,和验证计划工具从任何供应商或供应商的集合。最后要求主流形式验证终于得到解决。
更多的信息可以发现:http://bit.ly/2PO0Ezt。
|
|
|
|
|
|
|
|
|
|
留下一个回复