正式应用在全芯片级别可以针对特定的验证问题,即使在非常大的设计。
形式验证传统上被认为是一种先进的技术专家彻底验证逻辑块,或者小的街区。但是,如果你跟任何人参与这些天,你会发现大多数的正式用户运行应用程序(“应用程序”)针对特定的验证问题。此外,许多这样的应用程序,尤其是连通性检查,正在运行在非常大的全芯片级设计。我们想利用这个月的探索这两个极端之间的联系,看看发生了什么变化,未来可能会发生什么。
让我们承认,形式验证的传统观点是根植于现实。正式技术详尽分析所有可能的行为设计的验证。这个形成鲜明对比,模拟练习只有一小部分可能的行为通过运行特定的测试。如果没有测试触发一个设计错误,该错误将不会被发现。如果错误触发,但没有观察到的变化结果,错误不会被发现。给定一个足够强大的属性集来描述目的行为,正式工具不仅可以找到所有缺陷也证明不存在更多的缺陷。
分析所有可能的行为是一个复杂的数学问题。即使是很小的设计可能的状态数远远超过宇宙中原子的数量。正式的算法不考虑这些国家一个接一个地与模拟。然而,更大的设计更多的分析是必要的。序列复杂性的深度也是一个因素。有规律的突破能力和正式的算法的性能,因此用户现在运行在大量和集群难以想象的仅仅几年前。
其他因素也促进更广泛的采用正式的验证。标准化的描述格式的广泛部署,特别是SystemVerilog断言(上海广电)子集,减少了所需的专业知识水平写正式的属性。现在可以旗帜基于模型的变异范围设计的部分未被断言。正式的工具现在有更多的自动化和模仿调试特性,也使设计和使用验证工程师不是正式的专家。然而,它仍然是罕见的整个芯片设计正式完全验证。
相反,许多正式的应用程序通常运行在全芯片级别。大约15年前,EDA工具开发人员开始正式的技术应用到特定的验证问题。目标仍然发现bug和证明所有bug被发现,但只有那些与这个问题相关的bug被解决。连通性检查是一个验证的挑战很好解决的一个正式的应用程序。
分析时钟域和电力领域是另外两个验证任务也适合应用程序的解决方案。所有这三个应用程序必须运行在完整的芯片,因为只有在这个级别,所有设计信息是可用的。上运行完整的芯片是可能的因为只有一小部分设计相关问题。不相关的逻辑是修剪掉而建立的正式模型速度分析。
连接已经被证明是一个特别受欢迎的应用程序,因为现代SoC包含复杂的子系统由成千上万的高度可配置模块的实例和IP块。可编程元素提供灵活性和适应性,同时多路I / O垫允许用户控制的协议运行。一个connectivity-checking应用自动确保设计满足连接规范,可以使用简单的表定义在一个电子表格。这个规范显示所有所需的连接,包括任何控制条件或延误(登记水平)的路径。应用程序发现任何设计错误,一旦这些都是固定的,证明了设计与规范。
我们现在看到越来越多的芯片大小和复杂性使正式的应用程序更有价值,尤其是连接检查。数十亿门soc可能成千上万的模块实例化和一百万多个复杂的连接需要验证。毫无机会,模拟或手工技术就足够了。我们认为连通性检查是一种理想的形式验证中的应用。我们继续投资,以确保我们可以处理世界上最大的设计。花了几十年的形式验证取得主流地位,我们当然不想失去现在。
|
|
|
|
|
|
|
|
|
|
留下一个回复