理论计算机科学电子笔记119（2005）3-16www.elsevier.com/locate/entcs基于SAT的时态安全属性归纳Roy Armonia，1 Limor Fixa，1Ranan Fraera，1ScottHuddfarb，1Nir Pitermana，1 Moshe Y.Vardic，2，3a设计技术b台式机产品集团c部莱斯大学计算机科学系摘要本文提出的工作解决了在大型RTL设计上充分验证复杂时序特性的挑战。 窗口归纳由Shepherd、Singh和Stalmarck提出，作为一种增强有界模型检验的技术，用于安全属性的无界验证。虽然归纳法被证明对组合性质是非常有效的，但以前已知的方法没有处理时间性质的情况。我们引入明确的感应，一个新的感应计划针对时间属性，并互动发展的归纳证明。显式归纳的创新思想是使归纳方案成为规范的显式部分，在那里它可以很容易地控制，使用像ForSpec这样的高度表达性语言。我们展示了显式归纳是如何在ForSpec编译器和有界模型检查器Thunder中通过微小的修改实现的。最后，我们描述了如何明确感应被用于验证奔腾TM4处理器中具有广泛反馈的大型控制电路。通过显式归纳验证的电路比通过传统模型检查方法验证的电路大几个数量级。关键词：SAT，诱导，开窗诱导，安全性1电子邮件：firstname. intel.com2电子邮件：vardi@cs.rice.edu3部分由NSF资助CCR-9988322、CCR-0124077、CCR-0311326、IIS- 9908435、IIS-9978135、EIA-0086264和ANI-0216467、BSF资助9800096和英特尔公司资助。1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.12.0214R. Armoni等人/理论计算机科学电子笔记119（2005）31介绍形式验证的一般目标是以数学上精确的论证形式提供令人信服的证据，证明系统的正确性，表明系统（实现）满足所需属性（规范）的集合。在模型检查中，我们通过检查对系统进行建模的标记状态转换图是否满足指定此行为的时序逻辑公式来验证有限状态系统关于期望行为的正确性[6]。模型检查有两个主要优点，即它是全自动的，并且在失败的情况下会产生一个反例（系统的错误执行）。基于BDD [4，10]的符号模型检测的引入增加了模型检测的能力，并使其成为硬件行业的标准[1]。BDD是布尔函数的规范表示，用于表示模型的状态集和转换基于BDD的模型检查器计算可达状态集（有时分析循环），以确保没有不允许的行为。尽管容量增加了，但很快就发现，国家爆炸仍然是一个问题。一个重大突破是引入了有界模型检查器[2]。有界模型检验基于以布尔可满足性问题的形式伪造指定的计算路径的表示。有界模型检查的使用增加了模型检查器处理的模型的大小;然而，这是有代价的。对于验证问题，我们不再得到一个完全被证明的答案，而是得到一种保证，即不存在给定长度的反例。这一观察使得有界模型检查特别适合于错误搜索。 然而，有界模型检查器处理的边界的大小是有限制的，这使得我们对正在验证的设计的正确性缺乏完全的保证。在实践中，大多数规范都是安全属性。如果我们可以通过检查有限计算路径推断出一个属性为假，则该属性称为安全性。形式为ALWAYSp的组合属性，也称为不变量，是安全性属性的一个特殊情况，具有两个独特的特征：• 每个安全属性都可以通过下面描述的编译过程简化为不变量[8]。• 一些不变量可以用一种强大的技术完全证明，称为归纳[13]。除了作为一种完整的证明技术之外，归纳法还具有比有界模型检查更好的能力，因为它只需将模型展开到很小的深度。下面的段落解释了归纳是如何工作的。R. Armoni等人/理论计算机科学电子笔记119（2005）35≥1.1不变量的归纳法传统的数学归纳法可以用来证明一个性质P（n）对所有非负整数n成立。归纳证明包括证明以下两个子目标：• 证明P（0）为真。• 证明对所有k，P（k）蕴涵P（k+1）。在形式验证中，归纳法被用来证明一个过渡系统中的不变量P，通过证明P在系统的初始状态下成立，并且P由系统的过渡关系保持[9]。在许多情况下，P本身不是归纳的，人们必须找到P的一个归纳的加强。更正式地说，设M=（S，S0，T）是一个转移系统，其中S是一个状态集，S0<$S是一个初始状态集，T<$S×S是一个转移关系。为了表述的简单，我们将状态集作为谓词，例如，通过使用集合的特征函数。证明P的经典归纳方法是基于手动找到一个性质Q（归纳假设），使得Q≠P，并证明以下两个子目标：• M的初态满足Q：对于所有的态x0，我们有S0（x0）<$Q（x0）• Q由跃迁关系维持：对于所有的状态x0和x1，我们有Q（x0）<$T（x0，x1）<$Q（x1）这个经典的方法在理论上是合理的和完备的，其中理论上的完备性通过使性质Q描述M的可达状态集来证明。注意，归纳假设通常比完整的可达状态描述简单当它成功时，归纳能够处理比有界模型检查更大的模型，因为归纳步骤只需要考虑长度为1的路径，而有界模型检查需要检查足够长的路径以获得合理的置信度[3]。1.2窗口归纳在许多情况下，构造简单归纳的归纳不变量是不可行的。窗口归纳法是一种改进的归纳法，它可以大大简化在硬件模型上证明的归纳不变量的寻找。在数学上，窗口大小为N0的窗口归纳包括以下两个步骤：• 证明对于0≤k≤N，P（k）为真。• 证明对于所有k，（P（k））≠... P（k + N））6R. Armoni等人/理论计算机科学电子笔记119（2005）3硬件系统中的窗口归纳证明实现如下[13]。为了证明P是系统M的不变量，我们做以下事情：(i) 手动找到P的强化Q，其中Q隐含P。通常，我们选择Q为P，即 P。(ii) 找到一个N，对于这个N，以下两个证明是可实现的：(a) Base：Q在从初始状态开始的所有长度为N的路径中成立：S0（x0）T（x0，x1）. T（xN−1，xN）<$Q（x0）<$Q（x1）<$.Q（xn）(b) 步骤：对于长度为N+ 1的任意路径，如果Q在第一个N+ 1个状态，那么它在状态N+2也成立T（x0，x1）= 0. T（xN，xN+1） Q（xN）这种方法也被认为是健全和完整的。即使没有加强P，如果我们将归纳步骤仅限制为无环路径，则可以通过选择N为转移系统M的递归直径来证明完备性，即，无环路径的最大长度，单位为M。加窗归纳法相对于经典归纳法的优势在于，它为用户提供了两种加强归纳假设的方法：加强不变量Q或延长窗口N。(For为了简单起见，我们在后面的讨论中没有提到无循环条件，但它在我们的工具中实现了。在[13]中使用了窗口归纳法，在[5]中被认为是更抽象的。Intel中的正式验证环境将此归纳方案作为SAT模型检查器Thunder中的自动模式。边界N迭代地增加，直到证明成功或达到给定的极限窗口归纳法与标准归纳法具有相同的理论能力，但窗口归纳法往往允许更简单的归纳假设。在许多情况下，窗口的大小相对较小。与简单归纳一样，我们得到了两全其美：我们得到了正确性证明，我们得到了处理非常大的模型的能力。直觉上，顺序硬件电路中的流水线是为什么窗口归纳证明可以使用比相同属性的非窗口归纳证明更简单的归纳假设。当感兴趣的属性P依赖于深度d的管道时，具有窗口大小d的窗口归纳有时可以归纳地证明P而不加强P。但是在这种情况下，一个类似的标准归纳证明通常必须加强P以表达管道上的许多内部不变量，以便证明成功。[13]中的技术已在Intel成功使用，因为它们被证明对于验证组合属性非常有效其中一个好处是，R. Armoni等人/理论计算机科学电子笔记119（2005）37Z=1Fs0Z=1S1FZ=0S2！F这种方法的另一个优点是，它使许多感应机制自动化，包括自动搜索工作感应窗口大小。1.3时间性质当一个属性P不是组合的，而是一个复杂的时间规范，比如一个使用规范语言ForSpec编写的典型公式，如何通过归纳证明P可能并不明显。如前所述，这些断言通常是安全属性。ForSpec编译器将P合成为自动机AP和不变式ZP[14，8]，使得对于每个转换系统M：M| = P i MP |= ALWAYS ZP其中MP=M<$AP表示M和AP的同步合成。 上面关于ForSpec编译器行为的观察，立即表明对于安全属性P，可以使用经典归纳方法来证明M| = P，证明MP| = ALWAYSZP.作为一个例子，考虑ForSpec属性ALWAYS<$（f，f），它为f的两个连续出现提供条件，其中f是一个组合属性。当编译它的否定时，属性EVENTUALLY（f，f），我们可以得到，例如，图1中的三态自动机。这个自动机可以在初始状态s0中循环，或者在接收到输入时不确定地移动到s1F. f的第二次出现需要从s1移动到接受状态s2，而<$f的出现使我们回到s0。输出Z标记了接受这个自动机的状态，使得Z=0当且仅当原始属性ALWAYS<$（f，f）失败。如果我们设法通过归纳法证明ALWAYSZ，那么我们也有ALWAYS<$（f，f）的完整证明。真真Fig. 1. EVENTUALLY（f，f）的接受自动机-ALWAYS <$（f，f）的否定这种方法是在英特尔的Thunder之上实现的，Thunder是一个有界模型检查器[7]。当调用归纳算法时，该工具搜索足够大的窗口大小N，对于该窗口大小N，要求（ii-a）和（ii-b）都成立。完备性保证了这样一个N的存在，即使不加强不变量。在实践中，对于许多组合不变量，归纳成功地具有合理小的N对于ForSpec中表达的时态属性8R. Armoni等人/理论计算机科学电子笔记119（2005）3−ǁ然而，该工具通常不能完成证明。正如我们现在所解释的，这个问题既是算法问题，也是方法问题。在 算 法 方 面 ， 该 方 法 支 持 严 重 的 容 量 问 题 。 再 次 考 虑 性 质P=ALWAYS <$（f，f）和图1中的自动机。假设这个性质可以通过经典归纳法证明，即，M的初始状态满足<$（f，f），<$（f，f）由转换关系保持。因此，该属性在窗口N=1时通过。然而，总是Z不能通过具有小窗口N的归纳法来证明。对于每一个小的N，存在长度为N+1的路径失败于归纳步骤（路径在转换到s1和s2之前，在s0中循环N1次）。虽然这条路径只在自动机AP中包含循环，但它在乘积MP=M AP中很可能是无循环路径。在最坏的情况下，诱导成功的最小窗口N是系统M的递归直径（M中无环路径的最小长度），它通常超过工具的能力。(It这个问题似乎是由例子中使用的特定自动机引起的，但事实并非如此。减小窗口大小的一种方式是手动地加强不变性Zp。然而，这需要在增广设计M P上表达一个不变量。虽然可以期望用户理解系统M的内部细节，但是不能期望用户理解自动机AP的内部细节，自动机AP是ForSpec编译器的输出。用户甚至更不可能理解M与AP的交互作用。因此，要求用户生成M P的不变性是不现实的。这表明，隐式归纳，即使有人工干预，不能有效地用于验证时间ForSpec属性。1.4时间性质这种局限性实际上是我们工作的动力。我们想直接对原始的时间公式进行归纳推理，而不是对它的编译结果。为此，我们将归纳方案明确编码为规范的一部分未能证明归纳会产生一个有意义的反例，它反映了失败的真正原因，而不再是由于编译工件。理解感应失效是加强感应性能的关键线索在我们看来，这是唯一有效的方法，允许用户在找到正确归纳假设的迭代过程中进行手动指导。在这方面，我们进一步采用[13]的方法，据我们所知，这是直接对时间属性进行归纳的第一次尝试。R. Armoni等人/理论计算机科学电子笔记119（2005）39∧更精确地说，再考虑一个转移系统M=（S，S0，T），用uninit（M）表示未初始化的模型（S，S，T），其中S中的每个状态都是初始状态。考虑ForSpec公式P。 我们说P是有界的，如果存在k，使得对于每条路径π，P在π上的真值可以通过考虑长度为k的π的前缀来确定。例如，aNEXT [5]b（即a现在成立，b在5个时间单位后成立）总是可以通过考虑长度为6的前缀来确定。类似地，（a [3]，b [2]）TRIGGERS NEXTc的真值（也就是说，3次出现a后2次出现b后必须出现c）可以通过考虑长度为6的前缀来确定。另一方面，不存在一个界限k，使得公式a直到b或（a[2]b <$c）触发下一个d的真值（即，a出现2次，然后b出现一定次数，然后ac必须后跟d）可以通过考虑长度为k的前缀来确定。假设P是一个有界ForSpec规范。通过显式归纳证明ALWAYSP需要以下条件：(i) 手动找到P的强化Q，其中ALWAYSQ意味着ALWAYSP。同样，Q通常被选为P，即某个值。(ii) 找到一个N，对于这个N，以下两个证明是可实现的：(a) 基础：证明M| = ALWAYS [0，N] Q(b) 步骤：证明uninit（M）|=（ALWAYS [0，N] Q）NEXT [N +1] Q对于有界公式Q，（ii-a）和（ii-b）都可以使用有界模型检验来证明，我们稍后会讨论对于不熟悉ForSpec语言的读者，公式ALWAYS[0，N]Q意味着Q在路径的前N+1个状态类似地，NEXT[N+1]Q意味着Q保持在路径的第N+现在，我们可以很容易地看到，显式归纳中的要求（ii-a）和（ii-b）与窗口归纳中的要求类似。 作为因此，显式归纳也是合理和完整的（回想一下loopfreeness默认约束）。显式归纳和隐式归纳的主要区别在于，归纳不再是模型检测器内部的算法。相反，归纳方案成为规范的一个组成部分，用户可以使用ForSpec规范语言的表达能力这结合了窗口归纳法的性质和证明比简单不变量更复杂的性质的能力。10R. Armoni等人/理论计算机科学电子笔记119（2005）32工具问题本节检查实施第1.4小节中所述的归纳检查（ii-a）和（ii-b）所需的工具支持。首先请注意，（ii-a）归结为检查断言ALWAYSQ直到界限N（参见下面的讨论这是一个简单的有界模型检验问题。类似地，（ii-b）可以被简化为对断言ALWAYSQ执行有界模型检查，其界限恰好为N+1（再次，参见下面的讨论），假设ALWAYS[0，N]Q，在M的未初始化版本上。这意味着该工具在由三个较小模型组成的模型上执行精确的N+1• - 未初始化的模型单元init（M）=（S，S，T），其从原始模型M=（S，S0，T）导出，• 断言ALWAYSQ的初始化自动机，• 假设ALWAYS[0，N]Q的初始化自动机。虽然模型M必须是未初始化的，以使归纳是合理的，但ForSpec编译的两个自动机必须像在常规运行中一样初始化。例如，在假设的[0，N]时间窗口中使用的计数器需要从0开始，否则我们的检查不能正确地实现归纳步骤。综上所述，我们已经减少（ii-b）到另一个有界模型检查的实例，其中属性ALWAYSQ在边界N+1处被严格检查，并且初始约束仅从两个ForSpec自动机中选择性地构建，而不是从模型M本身或其他ForSpec属性。为了解决最后一个问题，我们向用户提供了一个新的ForSpec关键字，归纳假设，他可以用来标记假设总是[0，N] Q。通过这种方式，可以区分加强诱导证明的假设和指定与邻居RTL块的接口的常规假设。基于new关键字，ForSpec编译器将它生成的每一个自动机标记为断言、假设或归纳假设。 这个信息被传递给模型检查器，以确保只使用来自断言和归纳假设的初始约束。最后，请注意，在上面的两个检查中使用的界限N和N+1适用于Q是组合属性的情况。我们前面提到过，P（因此Q）可以是有界安全属性。在这种情况下，使用的边界取决于P中采用的时间窗口的长度。通常，我们最终会选择一个o集合k，使得归纳基（ii-a）为R. Armoni等人/理论计算机科学电子笔记119（2005）311在边界N+k处检查，而在边界N + k处检查归纳步骤（ii-b）。N+k+1。3使用方法在本节中，我们将介绍使用显式归纳的方法。从使用的角度来看，显式归纳和隐式归纳之间有三个主要区别：• 用户必须显式地编写归纳假设，其中隐式归纳根据断言自动构建它。• 用户必须在显式归纳中提供窗口大小，而隐式归纳通过尝试越来越大的大小来搜索工作归纳窗口大小。• 在隐式归纳中，不变量是属性自动转换的结果。因此，用户可能会发现很难加强不变量（如上所述），他最可能的策略是增加窗口大小。在显式归纳中，可以通过改变不变量和窗口大小来实现强化。表达显式归纳证明所需的ForSpec指令是ASSERT、ASSUME和归纳假设。关键字ASSUME用于给出辅助假设（例如，关于输入的假设等）。显式归纳技术不依赖于ForSpec的使用，下面描述的ForSpec结构有助于表达和维护归纳假设。我们利用ForSpec中的例如，我们定义了一个块模板，它为给定的属性Q生成归纳规范（Q，N），并为窗口N生成归纳假设和证明所需的断言：电磁感应规格（Q，N）：={直到循环NN：= ALWAYS[0，N]Q;在所有时间：= ALWAYSQ;}Q的显式归纳指令在For- Spec中如下所示：12R. Armoni等人/理论计算机科学电子笔记119（2005）3mypec：= numerical induction specs（Q，N）;//实例化块诱导假设mypec/直到循环N;始终保持ASSERTmypec/;然后，我们在N+1个周期的模型检查中检查这两个指令块模板不仅给了我们一个紧凑的符号，它还使表示断言和归纳假设的低级公式保持同步。它们涉及相同的属性Q和相同的界限N，这可以防止误报。在某些情况下，对于不同的诱导假设，使用不同的窗口大小是方便的这提供了对每个属性所依赖的管道/逻辑深度的有用洞察，并且还有助于选择最小的充足模型检查器边界来控制复杂性。这种方法的优点是，它足够灵活，可以针对不同的规格使用独立或相同的感应窗口大小。对于任何可以归纳证明的性质，都会有一些归纳窗口大小，它和所有较大的窗口大小都会产生成功的最初不知道需要多大的窗口大小，因此从更大的窗口大小开始可能是有益的。另一方面，较短的窗口大小可以更快地找到反例，并且较短的反例更容易调试。作为一般规则，我们估计一个可能有效的归纳窗口大小N，并试图证明性质Q。如果我们得到一个失败的，我们检查反例。如果反例看起来可能是由于初始化管道不同步，则需要增加归纳窗口大小。如果反例看起来像是由形式模型中的某种状态引起的，而这种状态在实际电路中是不应该达到的，那么归纳假设可能需要加强。强化假设通常会增加一个新的约束，禁止一些有问题的状态组合，有助于反例。依赖于简单流水线的断言展示了窗口归纳优于把一个窗口归纳假设变成一个更大的简单归纳的不变量。在加窗归纳假设可以简单地参考管道末端的感兴趣值的情况下，简单归纳不变量必须明确地表达每个管道阶段的约束。 当驱动断言证明的逻辑比简单的流水线更复杂时，构造简单归纳不变量的时间和成本要高得多。R. Armoni等人/理论计算机科学电子笔记119（2005）313这种方法还允许纯简单感应和长感应窗口之间的中间方法对于易于去流水线化的简单流水线，可以将流水线划分为两个（或更多个）长度大致相等的片段，并仅在划分点和结束处表示不变量。对于非常长的流水线，这可以大致减半所需的感应窗口大小，只有一个小的depipelining不变的建设成本。这是任何窗口归纳技术的一个优点，包括我们的，这种交易是可用的。4锁协议在奔腾TM4处理器中的应用在奔腾TM4中使用锁协议，允许不同的线程在几个共享资源上执行原子操作。锁协议的验证很重要，因为它与其他几个微架构功能进行了微妙的交互，使其功能正确性至关重要。述锁协议与高速缓存一致性协议以及与若干其它性能优化交互。这种协议的一个基本要求是互斥：没有资源可以同时被两个线程锁定。这个属性由形式为ALWAYSaTRIGGERSb[k]的ForSpec公式表示，其中a和b是设计的某些信号，k是整数。请注意，此属性是有界的。使用有界模型检查，证明了这个属性的所有痕迹多达50个周期。考虑到这个性质的重要性，有必要得到一个完整的无界证明，为此我们使用了显式归纳法当试图证明互斥性质时，我们很快就会得到失败的结论。模型检查器提供了一个见证轨迹，而归纳步骤并不适用于该轨迹。通常这是由于在真实模型中无法到达的状态开始。 例如，协议的控制部分被建模为有限状态机。一些归纳失败是包括某些事件的并发发生的跟踪，这些事件实际上不能在真实模型中一起发生。添加一个简单的归纳假设可以消除这种微不足道的失败。因此，发展归纳证明是一个迭代的过程，在这个过程中，我们不断加强归纳假设，这是基于以前建立归纳的尝试的失败。总的来说，我们必须增加大约20个约束条件，才能让这个假设足够强，从而建立归纳法。归纳证明的窗口大小因性质而异。只有三个属性是可证明的窗口大小为一个周期。所有其他性质都是在6到12个周期的窗口大小下证明的。14R. Armoni等人/理论计算机科学电子笔记119（2005）3我们验证的模型相当大，包含大约12，000个状态元素。这大大超出了基于BDD的模型检查器的容量（几百个状态元素）。对本文所述已证实性质的验证需要三至六个人工月。大多数诱导步骤运行在20分钟内完成，检查36个步骤，使用600M以下的内存。所有诱导步骤运行在3小时内完成，检查48个步骤，使用1G内存。5类似的归纳方法有两种可能的替代方法可以与我们的方法进行比较。最直接的比较是基于[13]的隐式归纳目前在Thunder中实现的这种方法无法归纳证明大多数ForSpec中编写的时态属性，因此无法进行直接比较。我们在前面解释了隐式归纳法对时间性质失败的原因。虽然容量问题不能通过使用不同的编译方案来消除，但我们相信它可以得到缓解。例如，如果我们将属性编译成确定性自动机，则归纳步骤（ii-b）的反例迹将受到更多约束，从而减少所需的窗口大小N。这是一个有待进一步研究的课题即使该技术变得可用，对于非常大的模型，我们的方法仍然可能优于隐式归纳，因为我们的方法可以在逐个属性的基础上对归纳窗口长度进行洞察。与我们的方法的另一个比较是使用STE代替归纳SAT作为有界模型检查器。使用STE的归纳法[12]在英特尔已经成功使用了好几年，特别是在数据路径逻辑和浮点性质证明方面。Sajid和Kaviola率先将STE归纳扩展到中等复杂的控制逻辑属性[11]。由于工具的差异，STE和SAT归纳方法之间的直接比较并不容易。我们的12000状态元件模型，即使减少到关键锁存器，也可能是[11]中 3000状态元件模型的两倍多也许SAT归纳和STE归纳之间最大的区别是做窗口归纳的明显困难或不切实际（与简单归纳）。使用STE的窗口归纳在理论上是可能的，但它有快速变量爆破和/或先行条件的问题。[11]的工作包括简单的归纳法正是出于这个原因。R. Armoni等人/理论计算机科学电子笔记119（2005）3156结果这里介绍的概念已经在英特尔的正式验证工具套件中实现只需要对ForSpec编译器和Thunder（我们基于SAT的模型检查器）进行微小的修改。显式归纳法已成功地用于DPG正式验证组。特别是，最令人印象深刻的应用是对上述锁协议的全面验证。模型的大小、12000个状态元素和协议的复杂性不言自明。但是，除了定量数据之外，还有一种新方法的影响，这种方法可以解决现有技术无法处理的验证问题。窗口归纳法的使用似乎是成功证明这些性质的一个关键因素。如果有必要将我们的窗口归纳假设分解为足以进行简单归纳的假设，合理的估计是，规范量将增加至少10倍，甚至至少三倍，可理解性和可维护性将大大降低。7总结本文提出的方法和工具支持解决了在大型RTL设计上充分验证复杂时序属性这里提倡的方法是互动发展的归纳证明。有很多正在进行的研究自动归纳证明，但没有satisfactory技术已经发现，即使是组合属性。我们相信，为了证明我们工作中遇到的复杂性，需要用户指导来找到正确的归纳不变量。在我们的方法的核心是显式归纳，一个新的归纳计划针对时间属性，并互动发展的归纳证明。时间属性的情况下，没有充分解决以前已知的方法。显式归纳的创新思想是使归纳方案成为规范的显式部分，在那里它可以很容易地控制，使用像ForSpec这样的高度表达性语言。目前的经验表明，显式归纳能够处理以前所有现有技术都难以处理的验证问题。为了进一步推动这种方法，我们未来的工作将集中在自动化一些手动任务上，例如通过让工具建议归纳不变量的候选者。16R. Armoni等人/理论计算机科学电子笔记119（2005）3引用[1] 啤酒，我，S.本-戴维角Reinner和A. Landver，RuleBase：一个面向行业的正式验证工具，在：Proc. 第33届设计自动化会议（1996年），pp。655-660[2] Biere，A.，A. Cimatti，E. Clarke，M. Fujita和Y. Zhu，使用SAT过程代替BDD的符号模型检查，在：Proc. 第36届设计自动化会议（1999年），pp。317-320[3] Biere，A.，E.克拉克河Raimi和Y. Zhu，使用无BDD的符号模型检查的PowerPC[tm]微处理器的安全特性，在：计算机辅助验证，Proc.11th International Conference，Lecture Notes inComputer Science1633（1999），pp. 172-183.[4] 布莱恩特河，基于图的布尔函数操作算法，IEEE计算机学报C-35（1986）。[5] Claessen，K.，归纳和状态机（1999），未出版。[6] Clarke，E.，O. Grumberg和D. Peled，[7] Copty，F.，L.菲克斯河Fraer，E. Giunchiglia，G. Kamhi，A. Tacchella和M. Vardi，Benefits ofbounded model checking at an industrial setting，in：Computer Aided Verification，Proc.第13届国际会议，计算机科学讲义2102（2001），pp。436-453[8] Kupferman ， O. 和 M. Vardi ， Model Checking of Safety Properties ， Formal Methods inSystem Design19（2001），pp. 291-314.[9] 曼纳角，巴西-地和A. Pnueli，[10] McMillan，K.，[11] Sajid，K.和R. Kaviola，使用符号模拟和归纳验证pSTTM4 BUS循环逻辑，英特尔设计测试与技术会议，2003年。[12] 塞 格 尔 角 和 R. Bryant ， Formal Verification by Symbolic Evaluation of Partially-orderedTrajectories，Formal Methods in SystemDesign， 1995，第6页。147-189.[13] Shepherd，M.，S. Singh和G. Stalmarck，Check safety properties using induction and aSAT- solver，in：Proc. 计算机辅助设计中的形式方法第三次会议，计算机科学讲义1954（2000），pp。108比125[14] Vardi，M.和p.Wolper，Reasoning about Infinite Computations，信息与计算115（1994），pp. 1比37
我的内容管理
展开
