用于存储器抽象和使用该存储器抽象来验证的方法和装置

摘要

本发明公开了一种将包括存储器的电路设计的计算机实现的表示抽象为更小的网表，其可用标准验证工具和操作网表的其它工具进行分析。这些系统的正确性需要推理比电路设计中存在的存储器条目的数量少得多的数量，并且通过将这些存储器抽象为小得多的数量的条目，大大减小了验证问题的计算复杂度。

说明书

技术领域

本发明涉及集成电路设计，尤其涉及电子设计自动化工具以及对包括存储器的复杂设计进行验证与分析的工具。

背景技术

利用在比个体导线和基本门的级别高的级别上获取的设计信息来进行字级设计的分析是硬件验证中的一个新领域。在字级上，相对于一组不具有特殊语义的位级信号，数据通路单元和数据包本身被视为实体。

目前的模型检查技术针对检查面向控制的属性运转良好。然而，目前的模型检查技术针对具有宽数据通路和大型存储器的设计运转并不良好。以前的方法通过读取设计者注释或递增地计算设计的精确抽象来设法加速处理。然而，注释对于设计者来说是非常耗时的，而抽象的计算可以与解决原始问题一样困难。

最近围绕例如SMT求解器(S.Ranise和C.Tinelli.Satisfiabilitymodulo theories.Trends and Controversies-IEEE Intelligent SystemsMagazine，2006年12月)的字级公式判别过程，以及像UCLID(在2002年的Computer Aided Verification会议纪录中，R.Bryant，S.Lahiri，和S.Seshia的.Modeling and verifying systems using a logicof counter arithmetic with lambda expressions and uninterpretedfunctions.)和BAT(在2007年的Computer Aided Verification会议纪录中，P.Manolios，S.Srinivasan和D.Vroon.BAT：The bit-levelanalysis tool.)的基于归约的过程已经有了许多研究。然而，随着此研究方向预期的兴起，使用这些过程来进行模型检查在本质上受到限制，因为这些过程对公式进行分析而不是对时序系统进行分析。这有两种结果：第一，时序属性仅能依靠诸如利用边界检查推断无界正确性的归约和插值之类的方法，来利用这些过程进行检查。第二，这些过程不适用于进行时序系统验证的基于变换的方法(在2006年的CAD会议中的Formal Methods的会议记录，J.Baumgartner，T.Gloekler，D.Shanmugam，R.Seigler，G.V.Huben，H.Mony，P.Roessler，和B.Ramanandray的Enabling large-scale pervasive logic verificationthrough multi-algorithmic formal reasoning.)，其中时序验证问题由后端模型检查器的大规模集合中的任何一个来迭代地简化并处理。

传统模型检查的最大障碍之一是混合了复杂控制逻辑的大型存储器的存在。这典型地导致了非常困难或难于控制的模型检查问题。因此，对包括大型存储器的硬件设计的有界及无界属性的实际字级模型检查需要有效地实现。

发明内容

本发明提供了一种网表减小方法，其中一个用于包括存储器的电路设计的网表被抽象为一个能够用标准验证工具和操作网表的其它工具进行分析的更小的网表。这样的系统的正确性可能需要相比于原始电路设计中存在的存储器项数量进行更少地推理。通过将这样的存储器抽象为更少的项，验证问题的计算复杂度大大地减小。

在将电路设计表示为一个数据结构的方法中，计算机实现的电路设计表示能够得以简化，这个数据结构定义一个包括多个节点的网表，例如以有向非循环图DAG形式。例如，用高级描述语言表示的电路设计能够在处理后产生这种类型的输入数据结构。输入数据结构处理后产生一种在试图保持预先指定的用网表表示的电路设计的属性时，具有更小复杂度和需要实现更少存储器槽的更新的网表。

输入网表的处理包括：标识电路设计中的存储器和在标识出的存储器中标识单个槽的地址或者多个槽的地址，对于该存储器而言，相应的单个槽或者相应的多个槽需要满足所关注的指定属性。用实现单个槽或者多个槽的替代节点来替换在表示这样的存储器的网表中的节点。实现验证条件，该验证条件支持使用替代节点对指定属性的检查。应用这里所描述的处理，更新的网表中表示的存储器的尺寸通过消除表示无需满足指定属性的槽的节点来减小。

网表中已标识存储器的单个槽或多个槽用替代节点来替换，针对每一个已表示的槽，该替代节点包括包含这个已表示的槽的数据的当前状态替代节点(在下面例子中命名为“cont”)、下一状态替代节点、以及用其地址标识已表示的槽的节点(在下面的例子中命名为“sel”)和相应的下一状态节点。代表向已表示的槽的写入的节点利用多路复用器实现，如果写入地址与标识槽的节点的内容相匹配，则多路复用器用写入数据更新该槽的下一状态替代节点的内容，否则用当前状态替代节点的内容更新已表示的槽的下一状态替代节点的内容。对于网表中代表从已表示的槽的读取的节点，替代节点包括多路复用器，如果读取地址与标识槽的节点的内容相匹配，则这个多路复用器返回已表示的槽的当前状态替代节点的内容，否则返回从环境读取的非确定数据。

标识输入网表中存储器的处理过程包括：标识可重建模存储器(包括存储器阵列的部分或全部)，可重建模存储器的特征在于定址于存储器的当前状态和下一状态节点的所有读和写节点读取和写入相同宽度的数据，并且使用相同宽度的地址节点，以及存储器中单个槽或多个槽以通用方式初始化为确定值。

通过标识抽象对来选择已更新网表中的所要表示的槽，该抽象对包含描述必须被表示的存储器的相应槽和描述在必须被表示的周期内已更新网表中为符合例如电路设计的安全性定义一类的属性的各个节点。因而，抽象对与在已更新网表中已表示的槽相对应，并包括标识已表示槽的节点和表明读取已表示槽以符合属性的周期的延迟参数。

重写组合输出形式的验证功能以便当抽象对指定的节点已经拥有适当在前的多个周期时间内相应槽的对应值时检查输出。在实现已更新网表时使用与一个所关注的特殊属性相关的抽象对，以在已更新网表中建立一个节点集合，其为每一个抽象对在已表明周期中指定一个已表示槽，将已抽象的节点与在抽象对的延迟参数表明的周期中标识已表示槽的节点相比较。如果针对相关的抽象对表明匹配，则检查所关注属性的输出。

这里描述的一种实现中用一种反例指导精化处理来标识抽象对。例如，通过开始于一个例如没有抽象对的实现的初始的已更新网表，在已更新网表上迭代地执行一种模型检查处理，可标识出抽象对。如果模型检查在一个特殊状态失败，将捕获引起失败的迹线，然后基于特殊状态迹线所确定的输入和初始状态变量赋值的集合，利用该原始输入网表运行一种仿真。如果原始网表的仿真没有表明失败，则已更新网表被处理以找到造成失败的错误读取。选择抽象对以解决错误读取，并且将所选择的抽象对加入到已更新网表中。迭代返回到模型检查步骤，并重复处理，直至已更新网表通过模型检查，直至在仿真步骤探测到真正的缺陷，或者直至已更新网表变得比目标尺寸更大。

在用上面提及的使用有向非循环图数据结构的实现中，图中顶部节点包括表示电路输出的字级节点和下一状态变量，图中底部节点包括表示输入的所述字级节点、状态变量和二进制常向量，图中内部节点包括存储器和表示运算符的字级节点。

本申请提出的技术处理字级网表以标识可重建模存储器，可重建模存储器仅用专用的读和写节点与它们的环境进行交互，以统一方式初始化并统一存取。当通过推理相比于一个标准位级模型检查需要数量显著更少的存储器槽和时间实例得到证明时，能够以允许属性证据的形式抽象可重建模存储器。

这里描述的技术可作为一种在数据处理机上执行的处理，可作为适于执行所描述过程的一种数据处理机，也可作为数据处理机的一种计算机可执行程序并存储在计算机可读数据存储介质上。另外，这里的技术是制造集成电路的处理的一部分，集成电路制造包括定义例如在集成电路制造中用于光刻处理的掩模或掩模集合的布局数据一类的模式的数据开发。

这里描述的处理过程的特点包括实现能够在标准安全性属性验证问题上操作，能够无需抽象提示完全自动化，能够作为后端判定过程在典型位级模型检查器中可用，还能够无缝地适合一种标准变换验证范例。

本发明的其它方面和优势可在下面的附图，具体描述和权利要求中看到。

附图说明

图1是一种示例性集成电路设计流程的简化表示。

图2是一种适用于与这种技术的实施例以及这种技术的电路设计和电路实施方式一起使用的计算机系统的简化结构图。

图3是一种用于减小表示包括存储器的电路设计的数据结构尺寸并用减小后的数据结构执行验证过程的过程简化流程图。

图4是实现包括存储器和多个节点的网表的有向无环图的代表性例子。

图5是图4所示电路设计的一种抽象。

图6是与图5中抽象一起使用的安全性属性的一种实现。

图7-8是一种通过抽象存储器来减小代表电路设计的数据结构的过程的更详细流程图。

图9是读节点的多路复用器树的一种实现。

图10是用于与包括多个抽象对的已更新网表一起使用的安全性属性的一种实现。

图11是一种计算机实现的、反例指导的、抽象精化循环的框图。

具体实施方式

图1是一种示例性集成电路设计流程的简化表示。利用这里所有的流程图，可以理解，图1中的许多步骤可以组合、并行执行或以不影响完成功能的不同顺序执行。在某些情况下，只有也做出某些其他改变的情况下，步骤的重新排列才可能实现相同的结果，而在其它情况下，只有满足某些条件的情况下，步骤的重新排列才能实现相同的结果。这样的重新排列可能性对读者而言是明显的。

在高级处，图1的过程开始于产生构思(块100)并在EDA(电子设计自动化)软件设计过程中实现(块110)。当该设计最终定稿时，发生制造处理(块150)及封装和组装处理(块160)，最终导致完成集成电路芯片(结果170)。

EDA软件设计处理(块110)事实上由多个步骤112-130组成，但是为了简化以线性形式示出。在实际的集成电路设计处理中，特殊设计可能不得不返回执行这些步骤直至某些测试通过。类似地，在任何一种实际的设计处理中，这些步骤可能以不同的顺序或组合发生。因此，这里描述采用上下文和一般性解释提出，而不是作为特殊集成电路的一种具体的或推荐的设计流程。

现在提出EDA软件设计处理(块110)的组成步骤的简要描述。

系统设计(块112)：设计者描述想要实现的功能性，他们执行假设规划去精化功能性，检查成本等等。硬件-软件体系结构可在这个阶段发生。在此步骤中可使用的来自Synopsys公司的示例性EDA软件包括Model Architect，Saber，System Studio和Design产品。

逻辑设计和功能验证(块114)：在这个阶段，用于系统中模块的、例如VHDL或Verilog代码的高级描述语言(HDL)代码被编写并且针对功能准确性检查该设计。更具体地，检查该设计以确保其响应于特定输入激励而产生正确的输出。在此步骤中可使用的来自Synopsys公司的示例性EDA软件包括VCS，VERA，DesignMagellan，Formality，ESP和LEDA产品。利用下面更具体描述的存储器抽象的字级网表减小技术可实现为例如Magellan产品的一个部分或一个附加工具。

合成和可测性设计(块116)：这里，VHDL/Verilog转译为网表。可为目标技术优化网表。另外，发生用于准许对已完成芯片进行检查的测试的设计和实现。在此步骤中可使用的来自Synopsys公司的示例性EDA软件包括DesignPhysical Compiler，TestCompiler，Power Compiler，FPGA Compiler，TetraMAX和Design产品。

网表验证(块118)：在这个步骤，针对服从定时约束和与VHDL/Verilog源代码一致来检查网表。在此步骤中可使用的来自Synopsys公司的示例性EDA软件包括Formality，PrimeTime和VCS产品。

设计规划(块120)：这里，针对定时和顶层布线来构造并分析芯片的整体平面布置图。在此步骤中可使用的来自Synopsys公司的示例性EDA软件包括Astro和IC Compiler产品。

物理实现(块122)：在这个步骤发生布置(电路元件的定位)和布线(电路元件的连接)。在此步骤中可使用的来自Synopsys公司的示例性EDA软件包括AstroRail，Primetime和Star RC/XT产品。

分析和提取(决124)：在这个步骤，在晶体管级验证电路功能，这继而允许假定精化。在此步骤中可使用的来自Synopsys公司的示例性EDA软件包括AstroRail，PrimeRail，Primetime和Star RC/XT产品。

物理验证(块126)：在这个阶段执行各种功检查能以确保制造，电力问题，光刻问题和线路的正确性。在此步骤中可使用的来自Synopsys公司的示例性EDA软件包括Hercules产品。

流片(块127)：这个阶段提供“流片”数据，用于为产生成品芯片产生供光刻使用的掩模。在此步骤中可使用的来自Synopsys公司的示例性EDA软件包括CATS(R)系列产品。

分辨率增强(块128)：这个阶段涉及布局的几何操作，以改善设计的可制造性。在此步骤中可使用的来自Synopsys公司的示例性EDA软件包括Proteus/Progen，ProteusAF和PSMGen产品。

掩模制备(块130)：这个阶段包括掩模数据制备和掩模自身的刻写。在此步骤中可使用的来自Synopsys公司的示例性EDA软件包括CATS(R)系列产品。

这里描述的网表减小技术的实施例可在上述阶段的一个或多个中应用。例如，本发明的实施例可在逻辑设计和功能验证(图1的块114)中应用。在这个阶段，用于系统中模块的VHDL或Verilog代码被编写并且针对功能准确性检查该设计。更具体地，检查该设计以确保响应于特定输入激励来产生正确输出。

图2是适于与这种技术实施例一起使用的计算机系统210的简化结构图。计算机系统210典型地包括通过总线子系统212与许多外设通信的至少一个处理器214。这些外设可以包括包含存储器子系统226和文件存储子系统228的存储子系统224、用户接口输入设备222、用户接口输出设备220和网络接口子系统216。输入和输出设备允许用户与计算机系统210交互。网络接口子系统216提供接口(包括去往通信网络218的接口)给外部网络，并且通过通信网络218耦合至其它计算机系统中的相应接口设备。通信网络218可以包括许多互连计算机系统和通信链接。这些通信链接可能是有线链路、光纤链路、无线链路或任何用于信息通信的其它机制。在一个实施例中，通信网络218是因特网，在其它实施例中，通信网络218可以是任何合适的计算机网络。

用户接口输入设备222可包括键盘、鼠标一类的指示设备、跟踪球、触摸垫或图形写字板、扫描器、合并入显示器的触摸屏、语音识别系统一类的音频输入设备、麦克风以及其它类型的输入设备。一般而言，术语“输入设备”的使用意在包括用于将信息输入到计算机系统210或输入通信网络218上的所有可能的设备类型和方式。

用户接口输出设备220可包括显示子系统、打印机、传真机或如音频输出设备一类的非视觉显示。显示子系统可包括阴极射线管(CRT)、液晶显示器(LCD)一类的平板设备、投影设备或者用于创建可视图像的某一其它机制。显示子系统也可以诸如经音频输出设备提供非可视显示。一般而言，术语“输出设备”的使用意在包括用于将信息从计算机系统210输出到用户或另一个机器或计算机系统的所有可能的设备类型和方式。

存储子系统224存储基本编程和数据构造，其提供这里描述的某一个或所有EDA工具的功能，包括网表减小技术和应用于分析已减小网表的验证工具。这些软件模块通常由处理器214执行。

存储器子系统226典型地包括许多存储器，其中包括一个用于在程序执行期间存储指令和数据的主随机存取存储器(RAM)230和一个存储固定指令的只读存储器(ROM)232。文件存储子系统228为程序和数据文件提供永久性存储，并可包括硬盘驱动器、与相关可移动介质一起的软盘驱动器、CD-ROM驱动器、光驱或可移动介质磁带盘。实现某些实施例功能性的数据库和模块可存储在文件存储子系统228中。

总线子系统212提供一种让计算机系统210的各种组成部分和子系统相互之间按期望进行通信的机制。尽管总线子系统212简化图示为单条总线，但是总线子系统的可选实施例可采用多条总线。

计算机可读介质240可以是一种与文件存储子系统228和/或网络接口子系统216相关联的介质。计算机可读介质可以是硬盘、软盘、CD-ROM、光学介质、可移动媒体磁带盘或电磁波。计算机可读介质240被示出为存储有电路设计280，包括例如电路设计的HDL描述和利用所描述技术创建的简化的网表。还示出利用所描述技术创建的电路290。

计算机系统210本身可以包括各种类型，这些类型包括个人计算机、便携式计算机、工作站、计算机终端、网络计算机、电视、大型机或任何一种其它数据处理系统或用户设备。由于计算机和网络不断变化的性质，图2所示的计算机系统210的描述意在仅仅是用于示出优选实施例的具体例子。计算机系统210的许多其它配置可能比图2所示计算机系统拥有更多或更少的组成部分。

图3是针对包含操作减小的网表的电路设计而执行验证步骤的处理的一个基本流程图。在图3的处理中，包括多个节点的字级网表从电路设计的高级描述语言描述编译而来，优选地采用节点的有向无环图形式(块300)。存储器抽象技术的实施例在字级节点上操作。然而，备选系统可应用到位级实现。标准前端流程采取用例如硬件描述语言(HDL)表达的寄存器传送级(RTL)描述，补充以用户约束、属性和其它信息的定义；以及产生下面具体描述的隐含时钟DAG表示。所用的标准前端流程是通过将具有属性和约束的硬件设计处理成代表一组无约束输入I、状态变量S和常量上的组合逻辑的多个节点，将电路设计编译成网表。作为结果的多个节点的顶部包含下一状态变量S’和单比特输出O。可以使用这种技术验证的属性包括其失败由某个假定值为“false”的输出来发信号的所有安全性属性。安全性属性是电路设计属性的子类，其具有某个输出总是具有的形式(也就是说，其失败可总是由有限迹(finite trace)来表明)。另外，在一些实施例中，每个状态变量可以假定为具有未知的初始状态。

在以这种方式编译的图中的内部节点包括如下：

node1＝not(node2)

node1＝and(node2，node3)

node1＝arithOp(node2，node3)，arithOp是{+，-，...}的成员

node1＝compOp(node2，node3)，compOp是{＜、≤、＝、≠、≥、＞}的成员

node1＝mux(selector，node2，node3)

node1＝extract(x，node2)

node1＝concat(node2，node3，...)

node1＝read(op1，addrj)

node1＝write(opk，addri，dataj)

在结果的位i是通过将布尔运算符应用到输入节点的位i这种意义上，“not(非)”和“and(与)”运算符是逐位运算符。如果selector(选择信号)为真，则“mux”节点返回node2，否则返回node3。“extract”节点通过从其操作数的位置(x)到(x+k-1)取出k位，而构造一个更小的位向量。最终，“concat”节点通过串接其操作数形成更大的位向量，而形成更大的信号。供连接的自变量列表中在前的运算符变成更高阶位，所以concat(01，00)变成0100。

mux节点的选择信号和比较运算符节点的输出限制为具有一位的宽度。这样的信号就是所谓的位级信号。不是位级信号的信号称为字级信号。术语“segment(段)”指的是一组连续的位，并且可以表示整个字或字的部分。

读节点和写节点用于建模存储器。读节点的语义指示：针对宽度为w的读节点，该节点返回结果，该结果是在它的自变量里从位向量op中取出位置addr*w...(addr+1)*(w-1)的多个位。对具有宽度为w的数据操作数的写节点，写节点返回用其自变量中的数据重写其自变量中位向量op的区域addr*w...(addr+1)*(w-1)得到的结果位向量。读节点和写节点的地址空间无需限制为任何一种特定形式。越界读取针对不存在的位返回非确定值。越界写入不做任何事。专用“(存储器)”寄存器节点或对读节点和写节点可以应用于什么信号的约束不是必需的。因而，RTL存储器设计就像任何其它节点一样可建模为位向量寄存器。通过控制逻辑的合理使用并配合多个读节点和写节点，在本例中的DAG支持具有大量读端口和写端口的任意复合存储器接口。此外，通过嵌套读、写和其它节点，复合策略可在作为同周期读和写结果的更新命令和读命令上实现。

返回至图3，遍历输入网表以标识可重建模存储器和这些存储器的读节点和写节点(块301)。可重建模存储器是一种可用这种技术提取的存储器。基本上，一种实际实现中的可重建模存储器可以限于其中的所有槽以统一方式寻址的那些，其仅以另一个实现能够容易替换的方式与设计的其余部分通信，并且具有特定简单结构的下一状态函数。更正式地，在一个给出寄存器变量mem的实现中，对mem标记为“纯存储器节点”的存储器节点的集合可以递归地定义如下：

1)节点mem是mem的纯存储器节点；

2)因opk是mem的纯存储器节点，所以write(opk，addrj，dataj)是纯存储器节点；

3)如果optruek和opfalsek是mem的纯存储器节点，则mux(sel1，optruek，opfalsek)是纯存储器节点。

状态变量mem的纯读节点集合由所有网表读节点read(opi，addrj)组成，其中opi是mem的纯存储器节点。此外，对mem的写节点集合由所有write(opk，addrj，dataj)组成，其中opk是mem的纯存储器节点。

给定此专有名词，可重建存储器可定义为满足以下要求的寄存器状态变量mem：

1)支持mem的所有读节点和写节点用相同宽度a的地址节点读和写相同宽度w的数据。此外，mem的位宽是w的整数m倍，并且2a≤m*w使得所有存储器存取发生在存储器内部。

2)mem初始化为布尔常量0000...0，1111...1，或者另一个确定的初始化值。

3)mem的下一状态函数是mem的纯存储器节点，并且没有其它下一状态函数是mem的纯存储器节点。

4)来自mem的每一个扇出路径包括终结于(1)mem的下一状态节点或(2)纯读节点的纯存储器节点的序列。

第一要求确保存储器被视为以统一方式读和写的槽的位向量。第二要求确保所有槽具有相同的初始状态，其保证为在已更新网表中表示而选择的槽都具有相同的初始状态。剩下的要求确保存储器寄存器仅在其它状态寄存器的扇入和通过读节点输出处发生，并且存储器的下一状态函数是在更新存储器的不同写节点之间选择的简单多路复用器树。

在此描述中运用的可重建模存储器的定义在能够覆盖大多数感兴趣的存储器实现与足够简单以提供相对直接的存储器抽象算法之间提供了一种平衡。其它类型存储器也能用适当的处理得以重建模，以考虑例外情况。

针对编码为字级DAG的网表，一种直接线性遍历算法可用于提取可重建模存储器的集合，并且计算它们相关的读节点和写节点的集合。

再次返回至图3，一旦可重建模存储器已经随其读节点和写节点的集合一起被标识，存储器便可被重建模以将所表示的存储器槽的数量减小为满足所感兴趣的指定属性(诸如安全性属性或安全性属性的集合)所需的那些槽，如下面(块302)具体描述的。

然后，减小的网表被处理以确定电路设计是满足指定属性，还是可以执行更严格的模型检查(块303)。如下所述，在特定的已减小网表上的模型检查在代表性实施例中实现为抽象精化循环的一部分。此外，已减小网表可用非常多样的工具处理，包括在用于时序电路验证的基于变换的方法中进行操作的工具。

图4是以一种包括含有存储器的电路设计的DAG形式实现的一个示例性网表。在DAG的底部，网表包括mem16384(即具有16384位宽的存储器的当前状态节点400)、宽度为9的读地址节点raddr9401、宽度为9的写地址节点waddr9402、宽度为32的数据节点data32403和宽度为32的常量节点032404。DAG的顶部包括宽度为1的输出节点safe1 418和存储器的下一状态节点mem’16384 419。读节点405通过用节点401的地址读取存储器节点400产生输出。比较器节点406比较读节点405的输出和存储在节点407中的常量10032。

＞运算符节点408比较数据节点403的内容与节点409中的常量20032的内容。节点408运算符的结果作为多路复用器410的selector输入。当节点408的输出为真时，多路复用器410选择数据节点403的内容，当节点408的输出为假时，从节点404中选择常量032。利用多路复用器节点410的输出所提供的数据，在写地址节点402所给出的地址处，写节点411为存储器节点400写下一状态寄存器406。

因此，在每一个时钟周期，系统从mem读取地址raddr处的槽的内容。如果数据大于200，则系统还将输入数据写入地址waddr处的槽，否则向其写入0。所实现的属性是安全性属性，要求从mem读取的值绝不等于100。显然，这对于在此简单系统中任何执行迹线都为真。并且，这个命题可通过推理存储器中单个槽的随着时间的内容(即，最后一个槽读取)来得到证明。

图4中建模的电路可概念性地划分为两个部分。第一部分(虚线415所包围的)包含大型存储器mem，并且通过两个输入和两个输出与设计的其余部分通信，这两个输入和输出是：节点402和411之间的9比特宽度的写地址端口wa，节点410和411之间的32比特宽度的写数据端口wd，节点401和405之间的9比特宽度的读地址端口ra，节点405和406之间的32比特宽度的读数据端口rd。图4电路的第二部分是电路的平衡。

图4所示存储器可抽象为图5所示用两个寄存器的当前状态和下一状态版本来替换16384位宽的当前状态和下一状态存储器节点，其中寄存器的当前状态和下一状态版本是：如通过包含槽地址来标识已表示的存储器槽的9位宽的sel节点500和sel’节点501，以及作为已表示槽内容的容器的32比特宽度的cont节点502和cont’节点503。以这种方式表示的槽在电路初始化期间被选择，并在后续系统执行期间保持不变。在这个实现中节点sel具有无约束初始状态和只将当前状态值传给下一状态节点501的下一状态函数。寄存器cont502、503初始化为存储器槽的指定初始值，如全为0。

从图4实现得到的写节点由多路复用器504替换，如果sel节点500的内容等于比较器505的输出所指示写地址端口wa9的地址，则多路复用器504用写数据端口wd32的数据更新cont的下一状态值，否则其将cont的当前状态节点502传给下一状态节点503。从图4实现得到的读节点由多路复用器506替换，如果sel节点500的内容等于读地址端口ra9的地址(如比较器507的输出所指示的)，则多路复用器504将cont的当前状态节点502的内容提供给读端口rd32，否则其提供来自非确定读节点508的非确定数据。

另外，在图6所示例子中，更新网表以改变正确性的定义，以便仅当从当前时钟周期读取的地址是sel节点500指示的已表示槽的地址的时候，才检查感兴趣的属性。因此，节点408的输出安全由implication运算符601的输出提供。如果如节点600的输出所表明的，提供读地址端口ra的节点401与sel节点500的内容相匹配，则implication运算符601仅检查原始安全定义电路safedef1 602的输出。这种实现可防止因发生(1)最终周期中raddr的值不同于sel所选择的初始值和(2)ndtrd 508的内容是100的情况下由存储器抽象引入的干扰性反例。在这个反例中，由sel初始化选来用于表示的槽与反例中读取的地址不是同步的。这导致可能错误地触发安全定义的假输出的错误读取。通过重新实现图6所示的验证条件，产生错误的假显示的可能性得以消除。

在根据图4-6描述的例子中，存储器在raddr节点401标识的槽的当前值上进行抽象。这对那个例子运转良好。然而对于许多系统，从多个在前的时间实例和周期中进行存储器存取不得不正确的运行来保证在当前周期中能够检查系统的正确性。例如，为了检查完全的多部分信息总是正确地传送，安全性定义需要读取序列的随着时间的执行都是正确的。为了处理这些类型的系统，在抽象对(v_i，d_i)的集合上的此方法过程中抽象可重建模存储器，其中vi是例如raddr节点401的信号，包含所要表示的槽的读地址，di是表明在当前周期之前的多个周期的整数时间延迟。节点vi和所有抽象对必须具有存储器上操作的读和写的地址节点同样的宽度。在图4-6所描述的例子中，在单个的抽象对{(raddr9，0)}上抽象存储器。

在已减小网表的特殊实现中利用的抽象对集合由下面描述的过程来标识。假定抽象对已经被标识，图7和图8提供了一种流程图来引入已表示的槽，重实现读节点以及改变验证条件来产生已更新网表。

该处理涉及遍历输入网表来标识一个可重建模存储器(块700，块701)。对于每个可重建模存储器引入抽象对的数量“n”(块702)。每个抽象对(v_i，d_i)按照块703所示去处理，这是通过用一个未初始化的初始状态函数和一个将前一状态值传给下一状态变量sel’i(块704)的下一状态函数为(v_i，d_i)引入当前状态变量seli。seli寄存器将包含系统运行期间此抽象对所表示的槽的具体数量。另外，为已表示的槽引入容器寄存器conti和它的下一状态寄存器cont’i。容器寄存器以对应原始mem节点的初始化的方式进行初始化。驱动下一状态寄存器cont’的函数在已更新网表中作为已标识存储器的下一状态函数的节点。这是可能的，因为本例中可重建模存储器的定义保证了mem的下一状态函数是mem的纯存储器节点。

接下来，已标识的可重建模存储器mem的网表中纯存储器节点由替代节点所替换。如块705所示，如果节点是已标识的存储器，则容器寄存器(conti)和对应于当前抽象对的初始化向量用作存储器的替代节点(块706)。如果节点是一个write(opk，addr1，datam)形式的写节点(块707)，将用逻辑mux(sel1＝addr1，datam，s0)来替换它，其中s0表示图5(块708)中如容器寄存器cont一类已更新网表中对应opk的节点。

进入图8，如果节点是mux(selector，optrue，opfalse)形式的一个多路复用器(块709)，将用逻辑mux(seli＝addr1，s0，s1)来替换它，其中s0和s1是在已更新网表中分别表示optrue和opfalse的节点(块710)。

接下来，替代节点连接到相应槽的下一状态容器寄存器cont’i，如图5中节点504连接到cont’503(块711)。这个处理以这种方式遍历抽象对直至它们都在已更新网表中重新实现(块712，块713)。

接下来重新实现读节点。如果节点具有read(opk，addr1)的形式，其中opk由用于抽象对的存储器中的已表示槽来替换，然后改变读节点多路复用器树以包含这个已表示槽(块714)。读节点的多路复用器树的实现将参照图10在下面描述。

在处理对应已标识存储器的节点之后，改变验证条件(块715)以便于仅当抽象节点标识的信号vi已经具有在之前时间实例di处选择的合适的值的时候检查属性。实现验证条件的一种技术是定义一个临时公式prevdi(s)，如果t≥d其在系统精确执行的时间点t处，值为真，和组合信号s在时间点t-d估为真。假定对信号s有n个抽象对(v_i，d_i)，新的安全输出可由为临时公式合成一个检查器来产生：

其中safedef当作提供旧的安全输出的组合节点。在图4描述的例子中，safedef将是当读数据端口rd的数据不等于100时为真的节点406。该检查器可用延迟某些网表节点比较的在前值的多个寄存器链的简单形式来实现。参照图10在下面描述这个例子。注意，已标识存储器mem是可重建模存储器。因此其只能通过读节点在其它状态变量扇入处出现。已更新网表为满足安全性条件重新实现所有必要的读节点。因此，网表的减小可以通过移除原始存储器mem和所有以上述方式依赖于它的逻辑得到。

块716-718示出了处理的某些实施例重新实现网表所涉及的附加步骤。在流程图中插入这些节点来反映它们是所使用处理实例的一部分，而不是表明处理执行的一种顺序。首先，如上所述，在一种方法中为所有读节点引入寄存器ndtrd。备选实现可应用双轨编码，在信号通道中将寄存器增加额外位以作为表明内容是否非确定的标志。网表可被评估以确定哪种方法对给定电路设计实现和所选择技术更加有效(块716)。这可以通过一次用双轨编码执行重新实现循环(如节点702-715)、一次用非确定数据节点执行重新实现循环并比较结果来完成。此外，为各种节点设立初始化函数，包括不是全0或全1存储器的容器节点，放宽可重建模存储器的定义以允许非统一初始化(块717)。最终，可重建模存储器的定义可放宽到允许无约束地址宽度，在这些情况下已更新网表可通过增加检查读和写节点的越界地址进一步更新(块718)。

一旦生成已更新网表，该处理进行到执行一种反例指导抽象精化处理来确定是否需要增加附加抽象对(块719)。参照图11描述一种代表性的反例指导抽象精化处理的细节。

参照上面块714所提及的，用图9所示多路复用器树的形式在已更新网表中表示纯读节点。图9所示多路复用器树返回其地址与读地址端口ra的地址相匹配的第一个所选槽的内容。如果地址与任何一个所选槽不匹配，则从输入节点ndtrd901的环境读取一个非确定值。这个多路复用器树包括多路复用器905-0到905-n，并且接收标识已表示槽sel0到seln的节点作为输入，其在比较器节点902-0到902-n处与读地址端口的地址相比较。比较器节点902-0到902-n的输出用作相应多路复用器905-0到905-n上的selector输入。此外，多路复用器树接收用于已表示的槽cont0到contn的替代节点以作为输入。如果比较器节点902-0的输出为真，多路复用器905-0选择cont0的内容，否则选择多路复用器905-1(未示出)的输出。如果比较器节点902-n的输出为真，树中最后一个多路复用器905-n选择contn的内容，否则选择ndtrd节点901中的值。

图10表示上面提及的参照块713的验证条件的重新实现。在这个例子中，“safe”输出920由隐含运算符921驱动。当AND节点922的输出为真时，隐含运算符仅仅操作去检查安全性定义safedef1的输出。AND节点922由一个其输出由被在抽象对中所表明的合适延迟时间进行延迟的抽象对上的比较器集合驱动。因此，来自抽象对(v₀，d₀)910-0的值v0与标识抽象对所表示槽的sel0节点相比较。因为延迟值d0是0，表明抽象对应于在当前周期中的槽读取，所以比较器911-0的输出无延迟地应用到AND节点922。来自抽象对(v₁，d₁)910-1的值v1与标识抽象对所表示槽的sel1节点相比较。因为延迟值d1是1，表明抽象对对应于在先于当前周期1个周期的周期中的槽读取，所以比较器911-1的输出通过寄存器912以一个1周期延迟应用到AND节点922。来自抽象对(v₂，d₂)910-2的值v2与标识抽象对所表示槽的sel2节点相比较。因为延迟值d2是2，表明抽象对对应于在先于当前周期2个周期的周期中读数，所以比较器911-2的输出通过寄存器913和914以一个2周期延迟应用到AND节点922。在图10中延迟寄存器被简化以避免图的拥挤。在一个代表性的系统中，延迟912通过建立一个具有下一状态节点d1’的节点d1来实现。比较器911-1在当前周期中提供节点d1’。将寄存器d1的内容作为输入提供至AND节点922。同样地，延迟913和914通过创建寄存器d1和d2来实现，其中下一状态节点寄存器d1’由比较器911-2的输出来驱动，当前状态寄存器d1驱动下一状态节点寄存器d2’，并且将d2作为输入提供至AND节点922。

图11示出了一个针对特殊设计问题找到抽象对的过程。一种可选择方法是将依赖于用户提供一种抽象对集合的标识作为到该过程的输入。然而，图11所示的自动方法是优选的。因此，对于图11的过程，在设计中维护每一个可重建模存储器的抽象对的当前集合。每一个可重建模存储器的抽象对集合在图11所示的迭代过程中单调增长。这种过程提供了一种具有0个抽象对的初始抽象，其中没有表示可重建模存储器的存储器槽(块950)。在这种初始抽象中，表示一个系统，其中存储器的每个读数返回一个非确定结果。给定初始抽象，计算已抽象的系统来提供使用了图7和图8示例上述方法过程的一个已更新网表(块951)。将已更新网表应用到一个位级模型检查路径，如典型的用于现有技术去检查设计的正确性(块952)。如果所检查属性在已更新网表上维持，则抽象过程进行至在原始系统上的有界检查(块953)。在这个步骤中，使用一种标准的基于SAT的有界检查程序检查原始系统的有界正确性，由对应于已更新网表中抽象对集合的最大延迟值的多个周期所界定的。如果此检查通过，则声明系统正确(块960)。如果原始系统的有界检查失败，则原始系统是有故障的并报告错误(块955)。

如果块952的模型检查在更新的网表表示的已抽象系统上探测到一个反例，则本方法过程试图精化抽象。已抽象系统的输入是原始系统输入的超集。所以在原始系统上用从表明已更新网表失败的迹线中确定的输入和状态变量进行的仿真可以重现这个反例(块954)。如果在仿真中探测到缺陷，则将错误报告给用户(块955)。如果在仿真中没有发生缺陷，就有必要精化抽象集合以移除错误迹线。

因为在原始系统与可能引入干扰性反例的抽象系统之间的唯一区别在于存储器编码，在某个时间实例处的某个已抽象读节点必须返回一个未表示槽的内容。通过检查在原始系统上运行的仿真和比较在抽象前读节点和在抽象后读节点，随着时间的错误读数在抽象系统的执行中能够得以标识(块956)。

不是所有的错误读数都会对已检查属性造成影响。通过在抽象系统仿真中最初对所有错误读数强行置数为正确值和迭代地以贪婪方式缩减已校正的集合直至确定依然移除错误的强置读数的局部最小值，这个方法过程确定读数的最小集合以及相关的时间点。

给定要校正的一个错误读数的集合和其中发生错误读取的错误周期的时间距离，必须为每一个时间点标识抽象信号。抽象信号可用如下的启发性方法进行选择：如果存储器读节点的片段相对于存储器槽数量比某个选择的如20％一类的经验值小，则用在其离最终周期的相应时间距离处失败读取的地址信号来创建新的抽象对。然而，如果存储器读节点的片段相对于存储器槽数量大于所选择值，则这个过程检索一种寄存器，这种寄存器(1)与存储器的地址宽度相同，(2)在存储器的影响锥中，和(3)包含在执行读取的时间实例处错误读节点读取的地址值。经找到满足这些标准的寄存器后，已标识的寄存器节点用于创建一个新的抽象对。在具有大量读节点的电路设计中，为了成功抽象存储器，包含已标识槽的寄存器入口应当出现在设计的其它地方。这种假设对于处理某些类型的存储器是关键的，如其中每个周期读取存储器的每一个条目但在给定时间事件只有少量读取的内容可编址存储器。

例如，对一个具有32个槽和两个读节点的单个可重建模存储器设计的抽象版本假定一个长度为15个周期的反例。如果形式为read(mem，raddri)的读节点需要在失败周期之前的一个时间步长周期13具有一个正确值，则为了移除缺陷迹线将当前抽象集合增加一个抽象对(raddri，1)。然而如果存储器有28个读节点，则这个过程将检索在周期13包含读取失败的具体地址的寄存器reg，并且找到的寄存器将形成一个新抽象集合(reg，1)的基础。如果没有这样的寄存器存在，则这个方法过程回复到原始的未抽象的存储器建模。

在块957已经选择出抽象对的新集合后，该过程执行评估处理是否完成的步骤(块959)。当然这个步骤随同图11所示处理的其它步骤可以任何合适的顺序发生。例如，例如块951之后确定的已抽象尺寸大于原始网表尺寸的75％，则这个方法过程可分支到使用原始网表(块958)。在一种可选情况下，在块959系统检查以确定处理是否超过一个时间限制或超过一个表明是否实现改进的预先指定数量的循环。

在任何事件中，抽象系统增加抽象对的新集合并且完成适应这个抽象对的新集合所需要的改变(块951)。这个方法过程如图11所示迭代的循环直至模型检查成功(块960)，报告错误(块955)，或作出判定使用原始网表(块958)。

引入一种使用字级网表信息标识可重建模存储器的技术。这些仅用专用读和写节点与环境交互的存储器，用一种指定方式初始化并统一存取。应用包含这样存储器的网表的一种抽象，以准许证明某些类型的属性，其中通过推理一个比标准位级模型检查所需存储器槽和时间实例更小的数量来完成证明。为了避免不得不依赖来自用户的抽象信息，使用一种反例驱动抽象精化框架来分析干扰性反例以递增地精化抽象。

技术特点包括(1)适用于一种标准基于变换的安全性属性验证的验证系统，(2)算法是全自动的，(3)不需用户输入抽象，和(4)任一位级模型检查器可在我们的抽象精化框架内用作判定过程。

当根据较佳实施例和上面描述的例子说明本发明时，可以理解这些例子意在解释而不是限定范围。可以预期的是，对于现有的本领域技术人员不难完成变形和组合，这些变形和组合均在本发明的精神和下面权利要求的范围之内。