使用可达性过度逼近进行验证的方法和系统

摘要

本发明公开了一种用于验证设计符合所需特性的方法、系统和计算机程序产品。该方法包括接收设计、所述设计的第一初始状态以及与所述设计相关的要验证的特性。扩展所述设计的第一初始状态以创建所述第一初始状态的超集，该超集包含从所述设计的所述第一初始状态可达的一个或多个状态。合成超集以定义所述设计的第二初始状态。通过将切割点插入到所述超集来过度逼近针对所述设计的所述超集的应用，以获得修改的超集，然后参考所述修改的超集验证所述特性。

说明书

相关申请的交叉引用

本申请涉及如下与本申请在同一日期提出的共同未决的美国专利申请，它们的全部内容在此结合作为参考：

序列号10/＿＿,＿＿(AUS920040651US1)，标题为“METHOD FORINCREMENTAL DESIGN REDUCTION VIA ITERATIVEOVERAPPROXIMATION AND RE-ENCODING STRATEGIES”。

技术领域

本发明一般涉及测试和验证，尤其涉及数字设计的验证。更特别的是，本发明涉及一种用于数字设计验证的系统、方法和计算机程序产品，其包括验证(verify)设计符合预期的特性。

背景技术

随着基于处理器的系统在人类活动的每个方面的日益渗透，对处理器、专用集成电路(ASIC)开发以及生产没有设计缺陷的系统的开发团体的需求日益增长。包括微处理器、数字信号和其他特殊目的处理器以及ASIC的电路产品已经与大批关键功能的性能密切相关，并且微处理器与日常生活的重要任务相关提高了人们对无误差的和无缺陷设计的期望。无论设计中的错误是通过对人类生活的影响还是仅仅通过对经济利益方面的影响来衡量，电路产品的消费者已失去了对设计错误所产生的结果的容忍。消费者将不会容忍例如在证券交易场所中、维持人的生命的医疗设备中或操控其交通工具的计算机中的计算错误。所有的这些活动代表了这样的一些领域：在这些领域中，对可靠电路结果的需求已上升为一个关键任务问题。

为了响应对可靠、无误差设计的日益增长的需求，处理器和ASIC设计以及开发团队已经开发出用于测试和验证的严格(即使是难以置信的昂贵)的方法。功能硬件验证已经成为用于验证诸如处理器芯片这种复杂设计的传统方法。因为用于设计的功能硬件验证时间的增长与逻辑元件的数量有关，所以复杂系统的功能硬件验证是现今最花费时间的计算任务之一。因此，以很少漏掉设计中的错误并减少开发时间作为目标，有效地使用功能硬件验证周期非常重要。

如上所述，功能硬件验证是一个计算上昂贵的过程；对于连续设计而言，功能硬件验证是一个完全PSPACE问题(通过算法的复杂性分析)，因此一般需要与所验证设计的大小成指数关系的资源。许多现有技术的功能硬件验证证明算法依赖于可达性分析，它需要列举出所测试设计的可达状态以评定该设计是否与它的技术要求相符，不幸的是它是一个大小受限的过程。

可达性分析是一个强大的验证框架；它能够确定设计是否满足技术要求(即，如果设计的所有可达状态都满足被验证的特性，那么就完成了正确性的验证)，也能够确定设计是否不满足其技术要求(如果设计的任一可达状态不满足被验证的特性)。可达性算法的操作是通过分配R_0作为所验证的设计的预定初始状态集合，然后分配R_{i+1}(i逐渐增加)作为从R_I进行一次设计转换就可到达的所有状态的集合。最后，R_{i+1}将为所有先前在R_0……R_i中遇到的状态的一个子集，此后这个过程将终止。这个最终的可达状态集合表示为R。为了部分地减轻某些用于计算可达状态精确集合这一昂贵过程的计算费用，已经有许多“过度逼近”可达状态集合的建议。例如，一些作者已经建议使用“归纳的”(inductive)方法。现有技术过度逼近方法的缺点是它们常常是不确定的，由于它们的过度逼近特性导致了“伪失效”(spurious failure)。

尽管在改进可达性分析性能方面研究了几十年，这种技术仍然局限于应用于有几百个或更少的状态元件的设计中，并且还受到其他设计尺寸的阻碍。由于可达性分析的尺寸限制，已在过度逼近可达状态集合以能够简化计算的方式上进行了一些研究。例如，归纳证明从R_0作为自身不违反特性的所有状态开始(在确保设计的实际初始状态是这个已过度逼近的R_0的一个子集之后)，然后计算从这个已过度逼近的初始状态集合开始的过度逼近集合R’。这种方法的好处包括大幅度减少完成分析所需要的步骤数。这种归纳方法的主要缺点是它常常导致一个不确定的结果。特别是，如果过度逼近集合R’包含一些违反正被验证的特性的状态S’，那么不能立即辨明这个违反是仅仅由初始状态集合(即，S’是R’-R的一个子集)的过度逼近引起的，还是S’包含R中某些实际可达的状态。前一种情况是所验证特性的伪失效。所需要的是利用功能硬件验证模型验证数字设计的方法，尤其是利用增强的过度逼近方法验证数字设计的方法。

发明内容

本发明公开了一种用于验证设计符合所需特性的方法、系统和计算机程序产品。该方法包括接收设计，所述设计的第一初始状态或初始状态集合，以及与所述设计相关的要验证的特性(property)。扩展所述设计的第一初始状态或初始状态集合以创建所述第一初始状态或初始状态集合的超集，该超集包含从所述设计的所述第一初始状态或初始状态集合可达的所有状态。合成所述超集以定义所述设计的第二初始状态。通过将切割点插入到所述超集来过度逼近(overapproximate)所述设计的所述超集的应用以获得修改的超集，然后参考所述修改的超集验证所述特性。

附图说明

在所附权利要求书中阐明了认为是新颖的本发明的特征。然而，结合附图，通过参考下面的示例性实施例的详细描述将更好地理解发明本身、优选的使用模式以及其进一步的目标和优点。其中：

图1根据本发明的优选实施例，描述了其中装备有用于通过有效使用过度逼近来验证设计符合所需特性的计算机程序产品的数据处理系统的框图。

图2是根据本发明的优选实施例用于有效使用过度逼近来验证设计符合所需特性的过程的高级流程图。

具体实施方式

本发明通过提供一种通过有效使用过度逼近来验证设计符合所需特性的方法、系统和计算机程序产品，从而减轻了功能硬件验证周期中的指数复杂性和相关资源消耗的问题。本发明通过安全地过度逼近验证中的设计的可达状态集合，能够比传统技术更有效地管理可用资源。本发明考虑到了验证算法的更高的可缩放性，同时避免了现有过度逼近技术中经常出现的伪失效问题。本发明还减小了所验证的设计的尺寸(这加快了所有形式的分析)，并通过简化的初始状态表示和用于枚举过度逼近过程中所有可达状态所需的较少量的图像计算而增强了可到达性分析。

现在参考附图，尤其是参考图1，图1根据本发明的优选实施例，描述了其中装备有用于通过有效使用过度逼近来验证设计符合所需特性的计算机程序产品的数据处理系统的框图。数据处理系统100包含处理存储器单元(例如，RAM 102)和处理器104。数据处理系统100还包括诸如硬盘驱动器或其他直接访问存储装置的非易失存储器106。输入/输出(I/O)控制器108通过诸如网络电缆112的有线或无线链接提供到网络110的连接。I/O控制器108也通过诸如电缆或射频连接的有线或无线链接116连接到诸如键盘、显示设备、鼠标或打印机这样的用户I/O装置114。系统内部连接118连接处理器104、RAM 102、存储器106和I/O控制器108。

在RAM 102中，当根据本发明的优选实施例操作时，数据处理系统100存储了几项数据和指令。这几项包括设计(D)120、用于与逻辑验证工具124交互的输出表格122，以及二进制决策图(binarydecision diagram：BDD)生成器(builder)126。其他应用128和逻辑验证工具124通过操作系统130与处理器104、RAM 102、I/O控制器108以及存储器106连接。数据处理技术领域的技术人员将很快认识到，在不偏离本发明的范围的情况下，可以添加数据处理系统100的附加组件到所显示的那些组件或替代所显示的那些组件。

在执行本发明的过程中，处理器104执行来自于程序(通常存储在RAM 102中)的指令。在本发明的优选实施例中，处理器104执行逻辑验证工具124。结合设计(D)120所包含的电路说明书上的二进制决策图生成器126的操作，逻辑验证工具124使用过度逼近有效地验证设计(D)120是否符合所需特性。一般来讲，逻辑验证工具124包含用于预测硬件的逻辑建模项的行为的基于规则的指令。逻辑验证工具124结合设计(D)120以及来自二进制决策图生成器126的相关二进制决策图(BDD)131，使用包含在其自身的指令内的一系列规则，其中所述二进制决策图生成器126将设计(D)120中的结构表示转换为BDD 131中的功能规范(canonical)形式。

设计(D)120可以构建许多不同种类的逻辑硬件(例如微处理器和专用集成电路(ASIC))的模型。设计(D)120在结构上被表示为一个连线表(netlist)，包含一个定向图表，图表中每个节点都是某一类型的门，例如与门、反向器、主输入(或随机门)或一个状态元件。BDD生成器126将设计(D)120转换为BDD 131，以和逻辑验证工具124一起使用。设计(D)120的连线表是以语义跟踪(semantic trace)来定义的，其随着时间的过去将门映射为BDD 131中的0,1值。设计(D)120中的每一个状态元件都与下一状态函数(定义在未来一个时间步长中将取什么值)以及初始值(定义在0时刻取什么值)有关，下一状态函数和初始值都表示为一个门。

逻辑验证工具124将结果记录到输出表格122。逻辑验证工具124也可以向用户I/O 114或应用128报告输出表格122的内容或设计(D)120状态的所选指示器。另外，逻辑验证工具124、操作系统130、设计(D)120以及输出表格122有时可以全部或部分地存储在存储器106中。

存储在RAM 102中的附加数据项包括第一初始状态(I)132、特性(P)134、可达状态(R)136、第二初始状态(I’)138、切割点(cutpoint)140、插入结果(I”)141和修改的超集(D+I”)142。第一初始状态(I)132包含用于验证的设计(D)120的初始状态或初始状态集合的说明。特性(P)134包含将在设计(D)120上验证的行为。可达状态(R)136包含能够在设计(D)120中实现的状态集合。第二初始状态(I’)138包含以可达状态(R)136为基础计算的设计(D)120的一个新的初始状态集合。切割点140包含一组用于插入第二初始状态(I’)138以便创建插入结果(I”)141的随机门插入指令，修改的超集(D+I”)142包含对于设计(D)120的过度逼近的应用插入结果(I”)141。

本发明的方法涉及一种用于以不会致使伪失效的方式“安全地”过度逼近第一初始状态(I)132的新颖方法。本发明的方法广泛地包括逻辑验证工具124，用于执行结构符号模拟以将第一初始状态(I)132中的初始状态集合注入到设计(D)120中(第一初始状态(I)132中的初始状态集合过低逼近(underapproximate)可达状态(R)136中的设计(D)120可达状态集合)，然后应用切割点140的插入来过度逼近那些初始状态，作为已过度逼近的应用插入结果(I”)141。逻辑验证工具124利用类似于“局部化”(localization)的语义分析方法来注入这些切割点140，以致从分析中尽可能多地消除初始状态逻辑(由此在已过度逼近的应用插入结果(I”)141中产生尽可能大的过度逼近)，同时努力确保已过度逼近的应用插入结果(I”)141中的结果过度逼近不会导致伪失效这种在诸如归纳法的现有过度逼近技术中频繁出现的缺陷。

现在转向图2，图2给出了一个高级逻辑流程图，其根据本发明的优选实施例示意了使用过度逼近有效验证设计符合所需特性的过程。该过程开始于步骤200。下一个步骤是201，它描述了接收设计(D)120、第一初始状态(I)132和特性(P)134的逻辑验证工具124。然后该过程进入到步骤202。在步骤202，逻辑验证工具124通过执行来自第一初始状态(I)132的状态空间遍历的任何形式的过低逼近，扩展第一初始状态(I)132中的初始状态集合，以获得状态集合S。仅需要S是指定第一初始状态(I)132的超集(包括附加状态，或完全相同的状态集合)，并且S是可达状态(R)136的子集。它的实例算法包括基于图表的二进制决策或结构符号模拟，部分或完全的可达性分析，以及‘再定时’(在此通过符号模拟计算再定时的初始值)。应该指出，第一初始状态(I)132的指定集合可能自身包含多个状态，这将允许某些实施例简化或省略步骤202。

还应注意的是，步骤202中执行的分析经常用在整个验证流的其他部分；这个步骤可能事实上不需要付出专门的努力，并经常仅仅需要重新使用已执行过的验证工作。例如，在基于多引擎的逻辑验证工具124中，步骤202的工作可能是“先前运行的”引擎所付出的努力的副产品。

接着，该过程执行到步骤204，步骤204举例说明了逻辑验证工具124将可达状态(R)136合成到设计(D)120的第二初始状态(I’)138中。第二初始状态(I’)138是第一初始状态(I)132的超集以及可达状态(R)136的子集。如果在步骤202中扩大了初始状态(I)132，步骤208可能包括将扩大的第二初始状态(I’)138合成到一个连线表中并更新连线表状态元件的初始值映射以便反映这个更新的集合，从而创建一个修改了的连线表。如果第二初始状态(I’)138是通过结构符号模拟获得的，那么本领域的技术人员将会认识到这个映射是微不足道的，并且它仅仅需要将状态元件的初始值映射更新到结构符号模拟期间所获得的门。否则，逻辑验证工具124可能使用现有的技术合成第二初始状态(I’)138(例如，如果状态集合由BDD 131表示，那么逻辑验证工具124可以通过在参数的随机变量上使用直接多路复用器表示，以“允许”不同路线通过BDD节点，然后将初始值映射更新到适当的合成门，来将状态集合合成为一个连线表)。此外，在基于多引擎的逻辑验证工具124中，这个编码经常是‘先前运行的’引擎所付出的努力的副产品。

接着，该过程执行到步骤206。在步骤206，通过注入切割点140到第二初始状态(I’)138以产生插入结果(I”)141以及通过组合设计(D)120和插入结果(I”)141，逻辑验证工具124过度逼近设计(D)120与第二初始状态(I’)138的组合以创建修改的超集(D+I”)142。切割点插入是指以随机门取代连线表中的门的过程。经切割点插入修改的设计称为“已过度逼近的”设计，因为它可以“模拟”原始的设计-随机门可以展示出其所取代的门可展示的任何行为，但是反过来不一定正确。该过程接着进行到步骤208，该步骤描述了逻辑验证工具124在修改的超集(D+I”)142上验证特性(P)134。

该过程接着执行到步骤210。在步骤210，逻辑验证工具124确定设计(D)120上的特性(P)134是否已经被证明是正确的，或者在步骤208中是否已经通过尝试验证设计(D)120上的特性(P)134而获得了它的一个有效反例。如果设计(D)120上的特性(P)134已经被证明是正确的，或者在步骤208中通过尝试验证设计(D)120上的特性(P)134已经获得了设计(D)120上的特性(P)134的一个有效反例，那么该过程移动到步骤212。在步骤212，逻辑验证工具124将步骤208的结果记录到输出表格122，这表明已相对于设计(D)120上的特性(P)134完成了验证。该过程接着在步骤214结束。

在步骤210，如果设计(D)120上的特性(P)134没有被证明是正确的并且在步骤208中没有通过尝试验证设计(D)120上的特性(P)134而获得设计(D)120上的特性(P)134的一个有效反例，那么该过程移动到步骤216。步骤216举例说明了逻辑验证工具124确定是否在步骤208中通过尝试验证设计(D)120上的特性(P)134而获得了设计(D)120上的特性(P)134的一个伪反例。如果逻辑验证工具124确定在步骤208中通过尝试验证设计(D)120上的特性(P)134时没有获得设计(D)120上的特性(P)134的一个伪反例，那么过程接下来移动到步骤220，该步骤描述了逻辑验证工具124用插入结果(I”)141的内容取代第一初始状态(I)132的内容，为步骤202-210的过程的迭代重复做准备。然后该过程转向步骤202，该步骤已在上面描述了。

如果逻辑验证工具124确定在步骤208中通过尝试验证设计(D)120上的特性(P)134已经获得了设计(D)120上的特性(P)134的一个伪反例，那么处理过程接下来移动到步骤218，该步骤举例说明了逻辑验证工具124精炼切割点140，以响应步骤206中的切割点插入产生了太过粗略的过度逼近。然后过程转向步骤206，该步骤已在上面描述了。

在一个实施例中，逻辑验证工具124可以使用“局部化精炼”方案以防止伪失效。逻辑验证工具124将首先通过在每个门插入切割点140，大概地过度逼近初始状态集合，其中每个门被映射作为初始状态(I)132中的状态变量的初始状态。然后，逻辑验证工具124执行低成本的过低逼近分析(例如随机模拟，或者SAT或基于BDD的符号模拟)以发现是否会发生任何的伪失效。应指出，过低逼近算法相比可达性分析(即，完全-NP相对完全-PSPACE的关系)具有较低的复杂性。如果存在伪失效，逻辑验证工具124分析导致那些伪失效(例如，和失效关联的语义跟踪)的起因，并且通过移去相应的表示原因的(causal)切割点140和取而代之地将切割点140注入到早期切割点140的扇入(fan-in)中的门中，来试图精炼早期的过度逼近。这个过程可根据需要重复多次，以便消除所有可疑的“伪失效”。因此，可以对去除了伪失效的“安全地”过度逼近的设计应用诸如可达性分析的证明算法。

正如所述的，优选实施例的方法通过过度逼近它的初始状态表示来将设计(D)120转换为一个简化的形式。然后逻辑验证工具124可以使用简化的设计来导入到其他的过程，例如导入到应用128，其将试图解决所产生的问题。另外，可以在迭代过程中应用优选实施例的方法来产生递增的简化。在基于多引擎的逻辑验证工具124工具集中，逻辑验证工具124还可以对所产生的简化问题应用任何一种附加转换。

本发明带来的好处多种多样。首先，切割点插入减小了所验证特性的影响范围内门的数量，这样就增强了所有的后续分析。其次，因为本优选实施例的特定切割点插入方案过度逼近初始状态集合，所以可达性分析算法的深度趋向于减少，反过来减少了资源的整体使用。另外，本优选实施例中的特定过度逼近形式通常可通过使BDD更加对称、更加紧凑和更易于操作，而增强基于BDD的分析。最后一条优点说明了基于BDD的实现方法可以从本发明特别获得明确的好处。第三，本优选实施例的过度逼近方法唯一依赖于过度逼近设计(D)120的连线表的初始状态(I)132。

如上所述，通过安全地过度逼近要验证的设计的可达状态集合，本发明比传统技术能更有效地管理可利用资源。本发明促进了证明算法的更高等级的可缩放性，同时避免了现有技术过度逼近方法中经常出现的伪失效问题。本发明减小了要验证的设计的尺寸(这加快了所有形式的分析)，并通过简化的初始状态表示和用于枚举过度逼近过程中所有可达状态所需的较少量的图像计算，增强了可到达性分析。

尽管如参考优选实施例的描述已经特别示出了本发明，本领域的技术人员将理解，可在形式和细节上对其做各种改变，而不偏离本发明的精神和范围。同样重要的是应注意，尽管已经在全功能计算机系统的上下文中描述了本发明，本领域的技术人员将理解的是，本发明的机制能够作为各种形式的程序产品而发布，不管携带用于实际执行发布的介质的信号的特殊类型如何，本发明都一样适用。携带介质的信号的例子包括但不局限于诸如软盘或CD ROM的可记录类型介质以及诸如模拟或数字通信链路的传输类型介质。