关键因素达到一个可量化的测量功能验证的完整性。
“签收”可能是最令人激动和可怕的字眼在半导体的发展。后几个月,甚至几年的团队努力,提交设计硅制造的确是一个令人兴奋的和有益的活动。但是,常常有明显的焦虑——如果任何错过的问题导致不得不“转”芯片,增加的成本和上市时间延迟可以是惊人的。因此,在开发过程中每个阶段都必须有明确定义的标准最终贡献的结果。正式的验证也不例外,本文讨论了七个关键步骤,必须采取实现必要的信心正式验收。
形式验证涉及到数学分析的寄存器传输级(RTL)对设计的设计和指定的属性。断言属性(断言)指定目的设计行为,假设属性(约束)控制分析,并覆盖特性测量分析练习设计。与模拟或仿真,正式的详尽且不依赖testbench或测试向量。它是一个功能强大的技术,但重要的是让用户记住,结果只是被分析的属性。因此,正式审核关注的七个步骤确保属性是足够的数量和质量,提供一个可量化的测量功能验证的完整性。
第一步是一个彻底的对测试计划和规范。设计和验证工程师编写属性基于测试计划中标识设计特点。如果计划不准确地反映目标功能的规范,那么属性可能是不完整的。综述通常由验证小组,虽然设计工程师可能涉及。设计师需要第二步,他们查看属性和正式的结果。他们知道自己的RTL代码和预期的行为,所以有很深的洞察力方面的设计应由断言检查和验证期间覆盖。这两个审查步骤可能发生多次在项目设计和属性演变和正式运行完成。
数学形式验证的目的是证明所有的观点都是正确的而覆盖完整的设计。因为这在很大程度上取决于属性,剩下的五个步骤在正式验收涉及回答关键问题之间的交互设计和属性:
VC正式下一代形式验证的解决方案和支持应用程序(应用程序)从Synopsys对此有能力回答这些问题以最小的用户工作。例如,VC正式可以自动执行快速分析,跟踪从每个断言或覆盖房地产看到的哪些部分设计的锥(COI)的影响。这提供了第一个问题的答案,不过后来的步骤在每个COI提供更深入的分析。值在这个阶段的关键是识别任何注册,输入或输出不COI内任何断言,这意味着它们没有被验证通过正式的分析。知道具体验证漏洞很好指导用户确定需要哪些额外的断言。
图1:快速跟踪的视锥细胞的影响。
第四步地址担心过度约束可能掩盖错误的设计。如果约束是不正确的,那么形式分析可能不是考虑的一些法律设计的行为。参与引发一个错误,如果这种行为是可以被断言,该错误将被错过,断言的证明是无效的。VC正式执行over-constraint分析找到的代码由于约束。任何行为在这段代码中,可能会引发一个错误不会被考虑,直到用户调整的约束使部分设计可及。分析报告哪些约束影响这部分的设计,显示的根源unreachability和使它更容易为用户进行必要的调整。
形式验证是一个详尽的技术,任何芯片项目的首选目标是实现一个完整的证据的断言。这是一个计算密集型的问题,在大型设计复杂的属性可能需要很长一段时间,或者需要大量的内存,得到一个完整的(无限)证明每一个断言。VC正式应用的算法可以生成有界的证明和报告周期(深度)的数量对于每一次这样的证据。它还提供了总体设计的连续的深度信息来帮助用户决定是否实现有限的证据提供高信心(虽然不确定性)的设计是正确的。这回答第三个关键问题,用户可以请求更有界证明如果足够的自信心水平尚未达到的。
第六步部分设计解决的问题真正得到证实。COI的方法是快速但在断言密度和质量判断过于乐观。内一些寄存器或输入COI可能不是参与证明(全部或有界)相关的断言。VC正式的一个子集上执行正式的岩心分析每个COI来确定哪些寄存器或输入所需的证据。这些可以映射覆盖率指标和VC Synopsys对此威尔第的正式可以生成一个覆盖数据库自动调试系统。在威尔第的覆盖率查看器,用户可以合并的结果模拟和正式评估互补验证所提供的两种技术。
图2:执行正式的核心分析并提供覆盖的结果。
正式的岩心分析比COI更精确,但是它不能回答最后的问题正式关闭。它可以告诉用户的东西关于登记检查,但是没有如果一切已经检查。最后一步结合VC与Synopsys对此正式正式Testbench分析仪(自由贸易协定)的应用提供最精确的断言的指标。自由贸易区的应用将缺点(突变)插入Synopsys对此确信功能评定系统的设计模型bug通常发现在RTL代码的类型。例子包括一个变量或表达式困高或低,指定一个不正确的值(例如0,而不是1)和一个不正确的操作(如加法而不是减法)指定。分析确定每个故障检测到任何断言。任何未被发现的错误突出显示清晰的代码指导用户应该添加什么断言。
正式验收的七个步骤建立一个方法,关键问题的答案形式分析和利用的特性。Synopsys对此VC正式用户可以应用这些步骤自动在适当点芯片开发项目从技术和确保获得最大价值没有验证漏洞。正式验收流程的更多信息,包括演示VC正式,可用的网络研讨会。
|
|
|
|
|
|
|
|
|
|
留下一个回复