无界模型检验中融合电路信息的SAT算法研究(.doc

计算机学报2009年6期薄袁肃蒇蚆蚄罿蒆莆衿袅肃薈蚂袁肂蚀羈膀肁莀螀肆肀蒂羆羂聿薅蝿袈聿蚇薁膇膈莇螇肂膇葿薀羈膆蚁螅羄膅莁蚈袀膄蒃袄腿膃薅蚆肅膃蚈袂羁膂莇蚅袇芁蒀袀螃芀薂蚃肂艿莂袈肈芈蒄螁羄芇薆羇袀芇虿螀膈芆莈薂肄莅蒁螈羀莄薃薁袆莃芃螆螂莂蒅蕿膁莁薇袄肇莁虿蚇羃莀荿袃衿荿蒁蚆膇蒈薄袁肃蒇蚆蚄罿蒆莆衿袅肃薈蚂袁肂蚀羈膀肁莀螀肆肀蒂羆羂聿薅蝿袈聿蚇薁膇膈莇螇肂膇葿薀羈膆蚁螅羄膅莁蚈袀膄蒃袄腿膃薅蚆肅膃蚈袂羁膂莇蚅袇芁蒀袀螃芀薂蚃肂艿莂袈肈芈蒄螁羄芇薆羇袀芇虿螀膈芆莈薂肄莅蒁螈羀莄薃薁袆莃芃螆螂莂蒅蕿膁莁薇袄肇莁虿蚇羃莀荿袃衿荿蒁蚆膇蒈薄袁肃蒇蚆蚄罿蒆莆衿袅肃薈蚂袁肂蚀羈膀肁莀螀肆肀蒂羆羂聿薅蝿袈聿蚇薁膇膈莇螇肂膇葿薀羈膆蚁螅羄膅莁蚈袀膄蒃袄腿膃薅蚆肅膃蚈袂羁膂莇蚅袇芁蒀袀螃芀薂蚃肂艿莂袈肈芈蒄螁羄芇薆羇袀芇虿螀膈芆莈薂肄莅蒁螈羀莄薃薁袆莃芃螆螂莂蒅蕿膁莁薇袄肇莁虿蚇羃莀荿袃衿荿蒁蚆膇蒈薄袁肃蒇蚆蚄罿蒆莆衿袅肃薈蚂袁肂蚀羈膀肁莀螀肆肀蒂羆羂聿薅蝿袈聿蚇薁膇 无界模型检验中融合电路信息的SAT算法研究本文获得国家自然科学基金项目（60633060），国家重点基础研究发展计划(973)课题(2005CB321605)和国家高技术研究发展计划(863)课题(2007AA01Z476)的资助。赵阳，男，1983年生，硕士研究生。研究方向为VLSI/SoC设计验证。E-mail: , 电话吕涛，女，1978年生，博士研究生。研究方向为VLSI/SoC测试与验证。李华伟，女，1974年生，博士，副研究员。研究方向为集成电路时延测试、测试生成、设计验证和可靠性设计。李晓维，男，1964年生，研究员,研究方向为VLSI/SoC设计验证与测试、可信计算等。赵阳1, 2 吕涛1, 2 李华伟1 李晓维1(1、中国科学院计算机系统结构重点实验室, 计算技术研究所，北京 100190；2、中国科学院研究生院，北京 100039)摘要：针对从电路转化而来的SAT问题，通用SAT求解器存在一个缺陷电路互连信息的缺失这是造成很多无关推导的根源。本文提出了一个统一的基于CNF数据结构的电路SAT无界模型检验框架。首先我们提出了定值子句的概念，利用这一概念可以在CNF结构中保存电路的互连信息，在搜索过程中更早的识别可满足解，减少不必要的搜索。其次，本文提出了在CNF结构上的状态变量赋值精简方法，摆脱了以往基于SAT的无界模型检验中这一步骤对门级电路结构的依赖。实验数据表明，利用本文方法进行前像计算能够取得明显的加速。同时，我们比较了两种搜索顺序在多时帧搜索中的效果。实验结果表明利用本文方法可以验证传统模型检验方法难于验证的复杂电路属性。关键词：设计验证、无界模型检验、Boolean可满足性问题（SAT）、寄存器传输级（RTL）设计A Novel Circuit SAT Solver in Unbounded Model CheckingZHAO Yang1, 2 LV Tao1, 2 LI Huawei 1 LI Xiaowei1(1. Key Laboratory of Computer System and Architecture, Institute of Computing Technology, Chinese Academy of Sciences, Beijing, 100190;2. Graduate School of Chinese Academy of Sciences, Beijing, 100039)Abstract: For the circuit-oriented SAT problems, general purpose SAT solver will make some unnecessary decision and deduction. The reason lies in that the circuit structure information is lost in the convertion to CNF. To overcome this short back in SAT-based unbounded model checking, an improved SAT solver is proposed. First, the concept of define-value clauses is given to store the circuit structure in CNF. Our improved solver avoids many redundant decisions which would be made by previous solvers. And then, A CNF-based assignment reduction algorithm is employed to speedup the convergence in search. The experimental result shows that our solver achieves obvious speedup over a previous method in preimage computation. Our merhod is capable of handling complex circuit property checking on which BDD methods would hardly work.Key words: design verification, unbounded model checking, Boolean satisfiability (SAT), register-transition level (RTL)111、引言日益复杂的集成电路设计对于功能验证方法提出了越来越高的要求。面对庞大的状态空间，传统的模拟验证方法已经很难保证其完备性，而模型检验方法1一直受囿于状态爆炸的问题，只能应用于模块级设计的验证中。近年来，由于在布尔可满足性问题（Boolean Satisfiability, SAT）的求解方面取了一些进展，与SAT问题相关的形式验证方法被广泛的研究。其中，基于SAT的有界模型检验方法2是其中影响比较大的成果。这一方法可以在给定的时序深度内寻找可能出现的反例。美中不足的是，有界模型检验不是一种完全的算法，如果没有找到反例，并不能证明电路符合某一属性。McMillan首先在文献3中提出了基于SAT的无界模型检验方法。相比BDD而言，SAT求解器能够处理更大规模的设计，最新的SAT求解器可以在可接受的时间内求解包含上万个变量，几十万个子句的问题。由于无界模型检验需要在很大的状态空间中进行搜索，有效的剪除无关子空间、减少不必要的搜索是提高验证效率的关键技术。通用SAT求解器存在一个比较突出的问题：不支持无关位，针对电路问题会产生大量的不必要赋值。一方面，无关逻辑锥上的搜索会降低SAT求解的速度，另一方面，无关的状态变量赋值会降低算法求得不动点的速度。这是SAT求解器运用于无界模型检验的重要问题之一，也是本文要试图解决的问题。本文实现了一个基于SAT的无界模型检验平台。目前，这个平台可以处理前像计算（preimage computation）和安全属性（safeness property）的检验。我们的算法是以程序包的形式，添加在开源的验证平台VIS 4（由Berkeley大学和Colorado大学共同开发）中。我们选用了Princeton大学开发的通用SAT求解器zChaff 5作为基础进行了优化，优化技术将在第4节阐述。验证流程如图 1所示。图 1：本文的验证流程SAT求解器只能处理Boolean变量，而RTL设计中的数据类型则比较丰富。本文利用Berkeley大学提供的开源工具vl2mv4，将Verilog设计转化为统一的Boolean变量的格式blif_mv4，同时运用VIS工具来解析这一文件格式。由于vl2mv支持常用的Verilog可综合语法，因此我们的平台可以处理大多数的Verilog设计。相比综合而言，这种转换开销很小，得到的设计描述抽象层次更高，适合于设计验证的需要。针对电路的属性检验问题，本文对于已有SAT求解方法的改进集中在以下两个方面：首先，针对电路设计转换得来的SAT问题，本文提出了定值子句的概念，使得CNF数据结构上可以保存电路的互连信息。这样，在保留SAT求解器本身高效的搜索算法的同时，考虑了电路的结构信息，减少了不必要的搜索。其次，我们提出了基于CNF数据结构的减少状态变量上赋值的算法。我们把文献6 7中运用的类似于ATPG中D算法的赋值精简思想运用到本文的SAT求解器中来。不同的是，我们的算法在CNF上进行搜索。在整个验证过程中，我们只需要CNF而不需要维护门级电路结构。改进的SAT求解器可以完成无界模型检验的全过程。本文的结构如下：在第2节，我们首先回顾无界模型检验相关的理论和技术，以及已有工作。第3节介绍了从RTL设计到SAT问题的转化过程。第4节详细阐述了本文针对电路SAT问题引入的一些概念，以及对于SAT求解器的优化策略。第5节介绍了本文在时序搜索中所采用的策略。第6节给出实验结果并加以分析，说明本文方法的有效性和优越性。下文中的讨论是在如下基本假定下进行的：文中讨论的设计限于单时钟的同步时序电路。为了描述问题方便，我们将“电路中的节点”和“变量”等同起来。下文中提到的“变量”都是指Boolean变量。2、理论背景及相关工作2.1 无界模型检验与时态逻辑逻辑电路一般被模型化为有限状态机。电路中包含l个寄存器用来记录当前电路所处的状态，同时有i个原始输入。连接输入和寄存器的组合逻辑网络决定了状态之间的迁移关系。状态空间S可以表述为l维Boolean向量的集合，每一个元素代表着一个寄存器的取值。同理，输入空间I是一个i维Boolean向量的集合。根据有限状态机的定义，可以定义迁移关系T：其中表示下一个时间帧上的状态集合。模型检验本质上是将待验证系统转化为描述状态迁移的结构（如Kripke结构），利用状态空间上的搜索来检验时态逻辑命题。不同的模型检验框架对应着不同的状态迁移表述方法和搜索策略。最早的显式模型检验是使用状态迁移图来描述设计，直接在图上进行标记来完成属性检验。由于状态的数目往往很大，显示模型检验能够处理的问题规模非常有限。符号模型检验利用符号表示状态集合，并且使用符号运算进行状态搜索。基于BDD的模型检验和基于SAT问题的模型检验都可以归结为这种方法。现有的符号模型检验一般不需要显式的描述待验证系统中所有状态以及它们的迁移关系，只需要表述状态中单步的状态迁移。求解一个状态集合的单步可达状态称为前像计算。对状态集合S进行前像计算，可以定义为：基于前像计算，常见的CTL属性都可以用迭代求不动点的方式得到满足属性的状态集合。例如满足时态逻辑EF f的状态集合可以通过演算表述为：在基于SAT的模型检验中，待验证的电路以及状态集合S都被转化为CNF。电路前像计算转化为对这个CNF所有解的搜索问题。每一个求得的解都是前像集合中的一个状态。属性检验是针对状态空间的迭代过程。每一个求得的状态会被映射到寄存器的输入，成为需要求解的前像目标。因此，前像解的表述应尽可能的精简，覆盖尽可能大的空间。例如在2维状态空间a,b中，1,x（其中x位表示无关位）的表述就要比列举两个解1,1和1,0有优势。因此这也是以往工作着力解决的问题。对于使用SAT求解器的模型检验，这一问题更为突出，因为一般的SAT求解器不支持x位。使用SAT进行前像计算，与一般的SAT问题相比有两点不同：1. 一般的SAT求解器只需要判断一个问题是否存在可满足解；而前像问题需要搜索所有可满足的解，复杂度更大。2. 前像计算中的存在量词作用在原始输入上，求得的解是状态空间上的集合。因此，搜索算法每次得到的解只需要保留必要的状态变量赋值。这样可以更快的剪除搜索空间，减少重复搜索。2.2 相关工作McMillan在文献3中提出将SAT用于无界模型检验的方法：将电路转换成CNF，利用SAT求解器搜索满足电路目标的解；对每个求得的解通过分析蕴含图的方法来减少其中不相关的状态变量赋值，最后精简后的解被转换成一个阻塞子句添加到SAT的子句集合中。这种方法直接与这一方法相比，本文采用了改进后的SAT算法，同时采用了更贴近电路结构的状态变量赋值精简方法。利用ATPG进行前像计算进而实现属性检验是一条重要的技术路线，而且与基于SAT的方法有大量的融合。文献8比较了两种引擎在形式验证中的优缺点和效率。ATPG相对于SAT求解器的一个很大的优势在于：ATPG是针对电路的方法，由于有J-frontier的信息，ATPG不会对所有的变量尝试赋值，因此能够产生一组相对精简并满足搜索目标的赋值，求得的解往往包含有很多无关位，即x位。对于前像搜索这样的需要状态穷举的问题，这是一个非常宝贵的特点。ATPG应用于无界模型检验的缺点主要在于：缺少有效的识别等价的子空间的方法，容易产生重复搜索的问题。文献9使用改进型的ATPG进行前像计算。该方法利用了一种 “成功信息驱动”（Success Driven Learning）的学习策略，采用电路割集来记录等价状态，从而剪除状态空间，避免重复搜索。同时，利用BDD来记录已经获得的解集合。这种方法计算前像解的效率很高。Lu等学者实现了时序电路可满足性求解器Seq-SAT 7。它采用类似AIG10的数据结构来表示电路并进行搜索。在决策上顺序上区分了原始输入和寄存器，并采用了ATPG的D算法用以减少不必要的状态赋值。Ganai和Gupta等学者11提出了基于电路余因子（Cofactor）的方法进行状态赋值精简。电路被转换成OR/INVERTER结构，利用专用的求解器在该结构上进行搜索。在找到一个解后，采用启发式的策略对于未取值的原始输入赋值，使得一次搜索能够覆盖尽可能多的状态，从而有效的减少属性验证中的迭代次数。以上三种方法都是针对门级电路的，RTL设计必须转换为门级网表之后才能使用这些方法进行处理。本文的工作可以处理一般的RTL设计，将其转化为CNF进行属性检验, 并实现了优化的SAT求解方法以及CNF结构上的状态变量赋值精简。文献12提出了一种动态无关子句剪除的方法，用来实现识别无关逻辑锥的目的。这种方法与我们的思路是类似的，但是需要在动态决策中不断进行递归的向后标记，因此在性能上受到一些限制。我们的方法通过维护CNF-J-frontier，避免了向后搜索，实现相同的效果。同时，我们还把这种思想扩展到状态变量赋值精简上。国内也有这方面的研究，如文献13中，作者采用了SAT求解器和ATPG相结合的方法进行前像计算。利用SAT求解器进行解的枚举，用ATPG进行状态变量赋值精简，分别利用两种引擎的优势。但是，这种方法需要维护两套数据结构，其间的交互会带来效率上的损失。在本文最后通过比较实验可以更明确的看出这一点。3、RTL设计到CNF的转化在RTL设计中，电路中的互连和组合逻辑关系都被抽象为变量之间的赋值和运算。变量可以代表寄存器（伪输入）、原始输入或组合网络中的内部节点。组合逻辑可以用Boolean函数的形式来表述：其中，是任意的n维Boolean函数。都是组合逻辑中的变量（节点）。组合网络可以通过一系列变量之间的定值关系被描述出来。定义1： 我们将设计中的Boolean函数称为广义逻辑门，为这个门的输出，是这个门的输入。一个广义门有且只有一个输出。广义逻辑门的概念包含了与门、或门等简单逻辑门。它能够方便的表达一些更复杂的组合逻辑。图 2中是一个二输入选择器， 我们可以将它看作是一个以O为输出，a、b、select为输入的广义门。并且给出了在blif_mv 关于blif_mv文件格式，可以参阅参考文献4中的相关内容。文件中的格式：每一个.table结构都可以被看作一个广义门，其中第一行中“-”左侧的变量代表输入变量，右侧的为输出变量。下边两行分别表示输入和输出的对应关系。“-”代表x位。如第一行表示，当Select取0时，无论A、B取何值，输出O的值都等于A。图 2：广义门在blif_mv格式中，.table结构利用类似真值表的结构来表述这个广义门所表示的Boolean函数。而相比真值表，table结构提供了一些更灵活简洁的表述，如无关位（-），默认值（default）和等号（=）结构。我们的工具支持这些常用的blif_mv语法。广义门模型表示了电路中节点之间值的关系，相比门级的网表而言，这种表述更精简。从Boolean函数转化得到的CNF等价于这个函数的谓词：公式 1: Boolean函数到CNF的转化广义门对应的函数关系可以转化为一个CNF。整个设计最终转化的范式设为CNFckt，转换的过程就是不断向CNFckt中添加子句的过程。转换过程与blif_mv文件的规模呈线性时间复杂度。表格 1统计了VIS Verification Benchmarks 4中，几个Verilog设计转化为AIG和CNF之后的变量数。可以看出，本文方法转换得来的问题包含的变量个数更少。减少变量个数有利于减少搜索深度，提高效率。这也是我们选择CNF作为数据结构的主要动机。表格 1：变量个数比较benchAIGCNFFIFOs3909649crc5335547Rotate1289197Palu1289268Vsa162609928874、针对电路的SAT求解器优化对于一般的SAT问题而言，判定一组赋值为可满足解的标准是：这组赋值可以使得所有子句都被满足。而现有的很多SAT求解器，往往需要对所有变量赋值后才能确定一个可满足的解。对逻辑电路对应的SAT问题，这些方式会造成很多不必要的赋值。我们可以通过一个例子说明：如图 3，S1、S2、A、B、C都是输入，搜索的目标是O2=1，当前已经有赋值C=1和S2=1。从直观来讲，这一组赋值已经满足搜索目标。但转换为SAT问题以后，此时仍然有子句未被满足。一般的SAT求解器都会继续在S1，A，B三个变量上进行决策和推导但这并不影响搜索的结果。图 3：广义门转换为SAT问题造成这一问题的根源在于，电路转换为SAT问题以后，电路互连信息被忽略。SAT求解器不能识别如上例所示的无关逻辑锥。本节提出的优化策略，就是针对于这一问题而提出的。可以看出，在CNF数据结构上进行一些微小的修改，就可以获得电路的互连信息。同时，对SAT求解器的终止条件进行一些修改，就可以使求解器在处理类似电路问题时能够避免不必要的决策。41 定值子句在上述广义门模型中，除原始输入和伪输入以外，每一个变量都是一个广义门的输出，每一个变量的值都由其对应的广义门所对应的函数给定。为了在SAT求解器中利用这种互连和定值的关系，我们做出如下定义：定义2： 在广义门模型中，变量是广义门的输出， 是这个广义门的输入。称是的定值变量。由广义门转化得到的CNF子句成为变量的定值子句（define-value clause）。如图 3所示，图中的四个被满足的子句是O2的定值子句，另外四个子句是O1的定值子句。原始输入和伪输入没有定值子句。在ATPG中，对于输出有确定的取值的门，如果它的输入取值可以蕴含出这个输出的值，称这个取值被满足（justified）。这样的概念可以推广到广义门模型上。如图 3中给定C=1、S2=1，输出的取值O2=1已被满足，但如果仅有C=1，则O2=1不能被满足。电路决策的终点，要求所有的内部节点都被满足，保证电路中每一点的值都能满足电路约束。广义门的类型比相比简单逻辑门要丰富的多，判定不同类型的广义门被满足的规则也非常复杂。最直观的解决方法是搜索广义门的真值表，但这样做的时间和空间开销都很大。如果利用定值子句的定义，则问题可以被大大简化。定理：给定广义门转换的CNF范式，输入变量为，输出变量为。对于一个给定的赋值，输入变量上的一组赋值可以使的定值子句都被满足，等价于的取值被满足。证明：根据第3节中的公式 1，CNF为真与等价，因此如果输入上的一组赋值能够使定值子句被满足，则这组赋值必然有。因此，在这个广义门上不会产生冲突；反之，如果的赋值与的值存在，必然有的定值子句全部满足。以图 3为例：尽管O1信号的取值没有给定，C=1、S1=1已经使O2=1的赋值被满足。输入变量（包括原始输入、伪输入）在每一帧内的取值没有约束，它们的取值总是被满足。以上的定义和定理是针对单个广义门的，我们可以推广到全电路的情况。定义3： 如果一个电路中所有变量的赋值都被满足，我们称这组赋值对于该电路是一组可满足赋值。在对电路设计的搜索过程中，每次对一个变量进行赋值，都需要考虑这个值能否被满足。电路的输入可以任意取值，但内部变量都是一个广义门的输出，其取值由它的输入决定。ATPG中用J-frontier的概念来描述。J-frontier是一个变量集合，有确定取值、但当前输入上的赋值尚不能推出这个值的内部变量被包括在J-frontier中。在我们的CNF模型中，我们可以类似的引入CNF-J-frontier的概念：定义4： CNF-J-frontier是一个子句集合，当一个变量被赋值，这个变量的定值子句就被加入到这个集合中。推论：根据定义3：、定义4：，如果CNF-J-frontier中所有的子句都被满足，则当前的赋值对整个电路是一组可满足赋值。每一次SAT求解器搜索的终止的条件可以变为：CNF-J-frontier中的子句都被满足。由于CNF-J-frontier只是全部子句的一个子集，取到可满足赋值比满足所有子句的条件要弱。对于电路SAT问题，可满足赋值对于满足电路约束是充分的。由于考虑了电路信息，可满足赋值避免了很多无用的赋值。再来看图 3所示的例子：O2=1，其定值子句全部被满足。C、S2都是输入，因此已经构成了一组可满足赋值，尽管有四个子句未被满足，搜索过程已经可以停止。这样，针对于电路的搜索问题，改进后的SAT求解器减少了很多不必要的决策和赋值。根据变量取值与其定值子句之间的关系，可以做出如下定义：定义5： 一个变量的定值子句可以根据这个变量的值分为两类。这个变量以正/负相（positive/ negative phase）出现的定值子句称为这个变量的定值为0/1子句（define-value-0/1 clause, DV0/1C）。通过本节的定义，我们可以将图 3中的电路表示为图 4中CNF的形式。定义5：的直观意义在于，当变量取1（或0）时，定值为1（或0）子句需要由输入变量满足，它给出了此时输入需要满足的约束，而其他定值子句都被自动满足。如图 4中，如果O1=1，原来的4个子句等价于O1的两个定值为1子句：。42状态变量赋值精简减少状态变量赋值要求对于取得的可满足赋值尽量精简。这一要求可以在搜索过程中实现,如：在J-frontier上进行决策的方法可以实现这一目的，但文献7中的实验证明这种决策方法效率不高。比较可行的方式是在搜索到一个可满足解之后进行精简，这也是大部分已有方法，如文献6 7中的思路。图 4：带有电路互联信息的CNF在简单逻辑门电路中，从输出向取控制值的输入进行搜索，可以得到满足输出的必要赋值。推广到广义门上，由于有上一小节中定理的保证，对于每一个被满足的定值子句，每句中只要选出一个变量的赋值，即可构成精简的可满足赋值。这是在CNF上进行赋值精简的基本思路。我们通过直观的例子来说明在CNF上进行状态变量赋值精简的过程：图 5中的电路与图 4中相同，O2=1是搜索目标。假定每一个输入都是状态变量。如图，当前取到了一组可满足赋值。我们的目标是从中提取出最精简的可满足赋值。图 5：状态变量赋值精简O2=1，搜索O2的定值为1子句，O1=1，S2=0使得这两个子句满足，S2是伪输入，总是可满足的。而对于O1，需要在它的定值为1子句中搜索，A=1，B=1使得这两个子句满足，因此，我们就找到了一组最精简的状态变量取值，使电路被满足。我们注意到，图 5中S1和C的取值对于目标的满足没有影响。对于任意一个取确定值的变量（如电路输出），在状态变量上寻找其精简可满足赋值的算法如图 6。精简后的赋值保存在reduced_assignment_stack中。图 6: 赋值精简算法5 、多时帧搜索策略CTL属性验证都需要进行不动点的求解。因此，一次验证过程中，前像算法要搜索不同的目标并多次运行。如果运用SAT求解器，每一次的迭代都要更换一个SAT问题。为了适应多时间帧上的搜索，文献14中提出了一种策略，通过引入变量来表示一个前像目标。这种方法的好处在于可以灵活的更换前像目标而不更改原有CNF中的大部分子句，并且可以灵活的选择目标之间的搜索顺序。本文工作，在CNF的构成方面借鉴了这一思想。我们称引入的用来表示前像目标的变量为目标变量。图 7中是多时帧迭代过程中SAT求解器需要求解的CNF结构。CNFckt是由设计转换而来的CNF，CNFstate定义了引入的目标变量与前像目标之间的等价关系。clauseobj是前像求解的目标，用若干目标变量的或运算表述，构成一个子句，允许同时搜索多个目标。CNFblock是阻塞子句，每求到一组可满足解都要将其求反并添加到子句库中以避免这个解被再次搜索到。CNFconflict子句的添加是SAT求解器提取的冲突学习子句。在求解过程中，clauseobj必须被满足。举例说明，如果我们搜索的目标唯一，假定为：O1=1、O2=1，那么首先引入一个变量S1，将约束S1（O11）（O21）转化为CNF子句加入待求解的问题中。并且（S1）是目标子句（图中的clauseobj）。求解过程中，由于它是一个单一文字子句，S1被蕴涵为1，并蕴涵出O11、O21。如果引入新的前像目标S2，则目标子句改为（S1S2），S1或S2为1都可以使目标子句满足，这样就可以达到同时搜索多个前像目标的目的。图 7：CNF结构我们着重考察了两种策略：1 广度优先搜索：每次进行完整的前像求解，将所有求得的前像求或运算，成为下一次前像求解的目标。2 混合搜索：每求得一个解，就将它加入到前像目标当中，寻找下一个前像解。直观的讲，两种策略各有优劣：广度优先搜索前像目标切换的次数少，对于一个目标穷举之后再切换下一个目标；而混合搜索每次同时搜索更多目标。通过下一节的实验数据我们可以比较一下这两种搜索策略的优劣。6 、实验及分析我们的实验分为两部分。首先比较本文提出的算法进行前像计算与以往算法的效率。然后，我们比较上一节中提出的两种多时帧算法宽度优先和混合搜索算法的效率，并与现有的基于BDD的算法做比较。我们的实验平台是主频为2.4GHz P4处理器的PC机，内存为480M。61前像计算我们选择了ITC99和ISCAS89电路来比较本文方法与文献13中算法的效率。之所以选择门级电路进行比较，是考虑文献13中的方法是处理门级设计的。在同一设计级别进行比较，有助于显示出算法本身的效率。前像的目标定为bench中出现的前三个寄存器取0。表格 2列出了两种算法所需的时间和求得的前像解个数。我们可以观察到文献13的算法由于采用了更有效的原始输入替代的方法减少状态变量上的赋值，在减少前像解的数量上效果显著。比较明显的优势体现在s38584电路上。但由于该方法采用了SAT和ATPG两套策略分别进行求解和状态变量赋值精简，其效率受到了一些影响。在整体的求解速度上来讲，本文的算法更快。因此，在减少状态变量赋值和求解效率之间，需要有一个折衷。本文提出的算法完整的保留了SAT求解器在处理CNF搜索的高效性，并且不存在数据结构之间的交互。在这一比较中体现出一定的优势。表格 2：前像计算bench本文算法文献13算法前像解个数运行时间前像解个数运行时间b0525320.7712583.98b12100.0180.06s953260.01100.08s14231890.0220.03s9234725613.34262132.79s3841710.0210.06s38584957229.572292.4462 EF属性检验本节实验的目标是计算满足属性的状态集合。其中属性为设计中寄存器的一些取值。实验选择了VIS Verification Benchmarks，每个benchmark的规模及功能描述如表格 3所示，其中FFs一栏表示设计中包含的状态变量的个数。表格 4分别列出了本文中提到的宽度优先搜索、混合搜索方法，以及VIS中基于BDD的可达性分析的运行时间（Time）和内存消耗（Mem）。我们设定运行时间的上界为1000秒。实验证明对于大多数算例，宽度优先搜索比混合搜索的效率高。原因在于混合搜索每得到一个解，都需要重置CNF命题，尽管它能够更早的搜索更深的时序上的解，但总的效率低于宽度优先搜索。相比SAT算法，BDD算法需要消耗更多的内存；并且，在很多的电路验证中没有在规定时间内得到结果。这是内存需求过大导致的，是“状态爆炸”的表现。从处理问题的规模上，我们可以看出基于SAT的模型检验在处理的问题规模上具有优势。表格 3：bench描述benchFFs简单功能描述Lock9密码锁twoAll30一个填数字游戏（FourByFour）表格为24的情况。b0534简单的内存控制器b12121一个按键游戏机CRC32CRC校验码生成Rotator64移位器Vsa1666支持9条算术指令的简单16bit CPU核FIFOs142两种FIFO队列的等价性检验7 、总结本文首先回顾了基于SAT无界模型检验的基本框架和技术难点。我们提出定值子句的概念，揭示了CNF与电路结构的关系。在此基础上定义了CNF上的可满足赋值。这样，SAT求解器在处理电路问题时就不必穷举所有变量的赋值，决策过程可以动态的识别无关的子句。并且，我们提出了基于电路CNF表示的状态变量赋值精简算法。在多时帧搜索顺序方面，我们比较了宽度优先搜索和混合策略。本文实现了一个统一基于CNF数据结构的无界模型检验框架。与传统的方法相比，我们的方法在验证层次、问题规模、效率方面有一定的优势。由于其固有的计算复杂度，无界模型检验将会继续受到工业界和学术界的关注。这个问题的最终解决，可能需要结合很多现有的方法如ATPG，BDD，SAT等。本文在SAT求解器融合电路互连信息方面做了一些尝试。仍然有很多问题，如解的有效表示，状态空间的进一步化简，高效的帧间学习策略等，需要进一步的研究。表格 4：属性检验实验结果bench本文算法VIS宽度优先搜索混合搜索运行时间(s)内存消耗(KB)运行时间(s)内存消耗(KB)运行时间(s)内存消耗(KB)Lock0.002020.002030.004,814twoAll0.013430.054311.6015,439b120.142,1360.732,192time outN/AFIFOs217.67317time outN/Atime outN/Acrc361.132520.023,358time outN/ARotate0.004480.00451time outN/APalu0.002944.313,358time outN/AVsa16(属性1)0.041,9310.111,939time outN/AVsa16(属性2)0.152,0110.832,079time outN/A参考文献：1 Bryant R. E. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 1986, 35(8):677-691.2 Biere A., Cimatti A., Clarke E., O. Strichman, and Zhu Y. Symbolic Model Checking without BDDs. /Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems. Amsterdam, 1999. Heidelberg:Springer Berlin, 1999:193-2073 McMillan K. L. Applying SAT Methods in Unbounded Symbolic Model Checking. /Proceedings of CAV. Copenhagen, 2002. Heidelberg:Springer Berlin, 2002: 303-3234 VIS webpage. /vis/5 zChaff Webpage. /chaff/ zchaff.html6 Hyeong-Ju Kang, In-Cheol Park. SAT-based Unbounded Symbolic Model Checking. IEEE Transaction on Computer-aided Design of Integrated Circuit and Systems, 2005, 24(2):129- 140.7 Lu F., Iyer M. K., Parthasarathy G., Wang L.-C. and Cheng K.-T. An Efficient Sequential SAT Solver with Improved Search Strategies. /Proceedings of the DATE. Munich, 2005. Washington: IEEE Computer Society, 2005:1002-10078 Parthasarathy G., Cheng K.-T., Huang C. Y. An Analysis of ATPG and SAT Algorithms for Formal Verification. /Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop. Monterey, 2001. Washington: IEEE Computer Society, 2001:177-1829 Li B., Hsiao M. S., and Sheng S. A Novel SAT All-solutions Solver for Efficient Preimage Computation. /Proceedings of the DATE. Paris, 2004. Washington: IEEE Computer Society, 2004: 272-27710 Kuehlmann A., Paruthi V., Krohm F., Ganai M. K. Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification. IEEE Transactions On Computer-aided Design Of Integrated Circuits And Systems, 2002, 21(12): 1377-139411 Ganai M. K., Gupta A., and Ashar P. Efficient SAT-based Unbounded Symbolic Model Checking Using Circuit Cofactoring. /Proceedings of the ICCAD. San Jose, 2004. Piscataway:IEEE Press, 2004:510-51712 Gupta A., Gupta A., Yang Z. Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation. /Proceedings of the DAC. Las Vegas, 2001. New York:ACM Press, 2001:536-54113 Liu Lingyi, Zhao Yang, Lv Tao, Li Huawei, Li Xiaowei. Combining ATPG and SAT for Preimage Computation in Unbounded Model Checking. Chinese Journal of Computer-Aided Design & Computer Graphic. 2007. 19(3): 376-380. (刘领一，赵阳，吕涛，李华伟，李晓维. 结合ATPG和SAT的无界模型检验前像计算方法，计算机辅助设计与图形学报，Vol.19，No.3, March, 2007)14 Chauhan P., Clarke E. M., and Kroening D. Using SAT Based Image Computation for Reachability Analysis. Pittsburg: Carnegie Mellon University, School of Computer Science, Technical Report: CMU-CS-03-151, 2003.ZHAO Yang, born in 1983, master candidate. His research interests include formal verification and integrated circuit design.LV Tao, born in 1978, Ph.D. candidate, assistant professor. Her research interests include VLSI/SoC design and verificationLI Huawei, born in 1974, Ph.D., associate professor. Her research interests include VLSI/SoC design and verification, test generation, delay testing, design for reliability and so on.LI Xiaowei, born in 1964, Ph.D., professor. His research interests include VLSI/SoC design and test, design for reliability and so on.BackgroundBinary Decision Diagram (BDD) makes model checking a pratical methods in real design verification. It has achieved wide acceptance in academy and also successful application in industry, like the verifying the correctness of IEEE Futurebus+ standard (IEEE Standard 896.1-1991). The state-of-the-art BDD-based algorithm can handle up to 10120 states in design. But its weakness of unacceptable memory consumption in constructing the structure and doing operation, especially when the circuit design becomes more and more complex. This problem is known as the “space explosion” in model checking.SAT is a classic problem in computer science. It is the first known NP-complete problem and has wide applications in artificial intelligence, programming and electrical design automation (EDA). In recent years, many new efficient schemes of SAT solving are proposed, including two-literal watch, conflict-driven learning and VSIDS decision