基于有界模型检验的自动化技术实现计算的过近似

CTCT理论计算机科学电子笔记144（2006）79-92www.elsevier.com/locate/entcs用有界模型检验计算过近似丹尼尔·克罗宁1瑞士苏黎世联邦理工学院计算机科学系摘要Bounded Model Checking（BMC）搜索具有有界长度k的性质φ的反例。如果找不到这样的反例，k就增加。当k超过完整性阈值（即，k足够大以确保不存在反例）或当SAT过程超过其时间或存储器界限时。然而，完整性阈值对于大多数实际情况来说太大或者太难计算。硬件设计人员经常修改他们的设计，以获得更好的验证和测试结果。本文提出了一种基于割点插入的自动化技术，以获得模型的过近似，1）保持安全属性，2）具有足够小的a，可以使用BMC实际证明φ该算法使用基于证明的抽象细化来去除虚假的反例。保留字： 有界模型检验，SAT过程，安全性1介绍在硬件行业，正式的验证已经建立。 模型检验于1981年引入，[10，12]是商业环境中最常用的形式验证技术之一。然而，它存在着状态爆炸问题。在基于BDD的符号模型检查的情况下，这个问题以不可管理的大型BDD的形式表现出来[7]。这个问题可以通过一种形式化的验证技术来部分解决，Bounded Model Checking（BMC），由Biere等人提出在BMC中，1电子邮件：daniel. inf.ethz.ch1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.07.02180D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）79|CT复模型M的转移关系及其规范φ被联合展开到深度k，以获得一个公式，然后使用命题SAT程序（如Cha [25]）检查该公式的可满足性。在φ是安全性质的情况下，如果存在，则该公式是满意的一个长度为k的例子，即， M/=k|φ。如果不为0，则k增加到寻找更长的反例。如果SAT过程超过了它的时间或内存界限，找到了一个反例，或者k超过了一个完整性阈值[17]。在后一种情况下，k足够大以确保不存在反例，因此我们得出M=φ。BMC已成功用于发现非常大的工业电路中的细微错误[27，14]。BMC的缺点是它通常仅适用于refutation;类型Gp的属性的最佳已知完整性阈值是M的可达性直径，即，状态图中从任意初始状态到任意可达状态的最长最短路径。在实践中，直径通常很难计算，而且通常是模型中状态变量数量的指数。递归直径[6]是可达性直径的过度近似。然而，它仍然难以计算，并且通常比可达直径大得多因此，在实践中，证明安全属性的主要方法是抽象。抽象技术通过映射将实际的具体系统的状态集合转换为抽象的、更小的状态集合，以保持系统的相关行为在硬件领域，最常用的抽象技术是局部化的结果[19，28，8]。Theabstractmo delM创建从通过移除大量的锁存器以及计算其下一状态所需的逻辑，来对给定电路进行优化。被移除的闩锁称为不可见闩锁。保留在抽象模型中的锁存器称为可见锁存器。初始的抽象模型是通过将属性中的闩锁设置为可见而将其余的设置为不可见来创建的。然后将抽象模型传递给模型检查器，通常是基于BDD的，比如SMV.局部化约简是对原电路可达性的保守这意味着，如果抽象满足该性质，则该性质在原始电路上也成立。保守抽象的缺点是，当抽象的模型检查失败时，它可能会产生一个不对应于任何具体反例的反例。这叫做伪反例.为了确定反例是否可以在混凝土模型上模拟，通常会形成一个有界模型检查实例：D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）7981将设计的具体过渡关系与给定属性共同展开，得到布尔公式。展开步骤的数目由抽象反例的长度给出。然后使用SAT程序检查布尔公式是否满足[28]。抽象轨迹中的转换有时被添加以减少搜索空间。缺点是，其他相同长度的反例只能通过额外的细化来检测。如果实例是可满足的，则反例是实数，算法终止。如果实例是不可满足的，那么抽象反例就是虚假的，必须进行抽象细化。抽象细化技术的基本思想是创建一个新的抽象模型，它包含更多的细节（例如，更可见的锁存器）以防止伪反例。这个过程是迭代的，直到属性被证明或反证。有许多方法可以细化抽象。如果使用抽象反例进行精化，则该过程称为反例引导抽象精化框架，或简称CEGAR [19，2，9，15，28]。因此，成功地应用带有本地化缩减的抽象细化通常需要三个组件：(i) 一种基于BDD的模型检测器，具有足够的抽象模型容量，(ii) 具有足够容量来执行抽象轨迹模拟的有界模型模拟器，(iii) 一种在模拟失败的情况下细化抽象的方法在实践中，尽管抽象，第一步往往是瓶颈，特别是如果属性依赖于许多锁存器。本文提出了一种许多硬件工程师在非正式和手动设置中常用的技术：如果设计过于复杂，无法进行仿真或验证，工程师可以切割或分割电路。形式上，这对应于移除电路的部分并通过非确定性选择的输入来替换丢失的信号。这样的切割点不一定移除锁存器，并且还可以保留仅依赖于被移除的锁存器的逻辑。所得到的电路在安全特性方面是原始电路贡献本文建议使用截点插入[18]来计算anabstract抽象模型具有两个特点：1）M过度近似M，以及因此，安全属性被保留，2）我们可以在语法上（因此，有效地）识别一个完整性阈值CT，它足够小，82D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）79|CTBMC与绑定。因此，如果找不到反例，我们可以得出M=φ。如果找到一个反例，我们检查它是否是假的。如果是这样，则细化切割点以消除伪迹线。与[22]类似，我们使用失败模拟运行的不满意性证明进行改进。因此，我们可以在抽象细化循环中省略基于BDD的模型检查器，并依赖BMC作为唯一的推理引擎。这允许仅用BMC就能证明许多性能相关工作Baumgartner等人[5]进行了类似于本文所用的结构分析，以获得完整性阈值。在本文中提出的算法相比，电路的抽象，以获得一个较小的完整性阈值不适用。推广了文[4]中的结果。BMC的完整性阈值的概念在[17]中引入在[11]中给出了任意LTL性质的完全性阈值。在[1]中给出了考虑属性中谓词的直径检验的优化。另一种获得BMC完整版本的流行技术是使用BMC来证明归纳不变量[26]。该技术使用约束来强制简单（即，无环）路径，其类似于用于执行递归直径测试的约束。Somenzi等人[20]使用这些约束来获得一个完整的BMC，用于抽象细化框架中的抽象模型。如[20]中所述，必须使用BMC搜索的深度可以指数地大于可达性直径。已经提出了许多方法来细化通过局部化约简完成的抽象。在[13]中，Clarke等人提出使用ILP求解器和机器学习技术为抽象模型选择一组合适的锁存器。关于如何改进基本BMC实例之外的模拟步骤的详细信息，请参见[3]。在[8]中，Chauhan等人建议分析失败的BMC运行的连接图，以获得细化信息。McMillan [22]使用了类似的方法：分析失败BMC运行的不满意内核，以获得用于局部化减少的新锁存器集。使用BDD验证抽象模型。McMillan在[21]中提出了第一个基于SAT而没有任何抽象的完整模型检查方法。SAT求解器被修改为执行前像计算。该方法枚举前映像中的状态。的放大，避免了显式的状态枚举。D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）7983|CTCTCT这是从constriction graph中得到的。在[23]中，McMillan提出了使用插值，以获得基于BMC推理引擎的完整模型检查器。纲要在第2节中，我们提供了关于有界模型检查、完整性阈值、局部化简化和自动抽象细化的背景信息。我们在第3节中描述了我们应用的抽象。实验结果见第4节。2背景2.1完全性阈值与直径设M表示由有限个状态集S、初始状态集IS和转移关系RS×S定义的有限转移系统。 由M |= φ我们表示M的任何计算都满足性质φ，而M =kφ我们表示长度为k或更小的所有计算都不违反φ。定义2.1完备性阈值[17]，表示为，对于有限转移系统M和性质φ，是任何自然数，如果没有违反φ的长度计算，φ对M所做的任何计算都成立：M| = CTφ−→M| = φ如果M| = φ，则最小的CT为0，否则为最短反例的长度。因此，计算最小CT与确定M是否|= φ成立。因此，在实践中，目标是计算最小CT的过近似。定义2.2有限转移系统M的直径，记为d（M），是M的任意两个可达状态之间的最长最短路径的长度（由其边数定义）。定义2.3有限变迁系统M的初始直径，记为dI（M），是从M的任何初始状态到任何可达状态的最长最短路径的长度。在[6]中已经观察到d（M）是一个足够大的界以证明形式AGp的性质。这个界限可以通过使用初始化直径dI（M）来改进。在[17]中确定了AFp形式的性质的界。在[11]中找到了计算任意LTL性质的a的方法84D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）79∈⊆×G2 1 2 1--121212计算直径测试特定的k是否是对应于QBF实例的直径。尽管QBF求解器取得了进展，但迄今为止解决此类实例的尝试都失败了。Biere等人在[6]中建议使用SAT来计算复发直径，这是直径的过度近似。然而，对于大多数有趣的电路，递归直径要么太大，要么太难计算。Mneimneh和Sakallah [24]修改SAT求解器以通过路径枚举计算直径。2.2用结构分析模型检查经常应用于电路，通常以网表的形式给出。Baumgartner等人。[5]建议利用这些网表的结构来计算直径的过度近似定义2.4网表是一个有向图（V，E，T），其中V是顶点的有限集合，EVV是边的集合，T（v）是顶点v V的类型。类型是AND（与门）、inv（反相器）、reg（寄存器）、inp（主输入）中的一种。类型和的顶点的入度至少为1，inv和reg类型的顶点的入度正好为1，inp类型的顶点的入度正好为0。符号给定两个顶点vv，我们写v。vi <$（v，v）∈E，且v~Ev在E中存在从v1到v2的路径。我们写v1~Ev如果T（v） =T（v） =reg且有一条从v出发的路到E中的v2，只通过类型为和的顶点（门），inv。我们要求任何这样的路径是非循环的，即， 锁存器之间的逻辑必须是组合的。这种网表的语义定义是直接的。在Verilog中给出的电路的转换到这样的网表对应于综合。定义2.5网表N=（VJ，EJ，T）的闩锁依赖图（LDG）是有向图（V，E），其中V={v∈VJ|T（v）=reg}是锁存器的集合在N中，并且在LDG i中的两个锁存器v1和v2之间存在边沿，是从v1到v2 在N中，仅使用门，即，v1→v2中国v1EJG v2.定义2.6电路中的元件是LDG的连通子图。组件图是通过将每个组件替换为单个顶点而生成的图。我们用下式表示我们导出的分量C的直径的界：（C）. 显然，如果k是C中的锁存器的数量，则2k是这样的界限。EE12~D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）7985∆1∆2O=. . .. . .Fig. 1. 两个组件的顺序组合。 组合物直径的界是单个直径的总和在[5]中，基于组件的结构导出了各种类型组件的直径界限，例如，用于ROM、常数锁存器和非循环组件。特别地，观察到顺序组成的两个组分的直径的界限之和是组合物的界限：定理2.7设C1和C2是两个分支，且φ（C1）和φ（C2）分别是C1和C2的直径的界.这两个界的和是序列组合C1→C2的直径的界（图1）：（C1→C2）=2.3通过切入点插入进行切入点插入对应于将网表中的信号替换为新的主要输入[18]。由此产生的电路M是一个过度近似的原始电路M，以及可达性属性的保守抽象正如在[4]中已经指出的，M的完备性阈值不是一个完整的M的阈值;抽象电路通常具有小得多的直径。通过插入切割点，直径不会增加3具有过逼近3.1概述图2显示了本文中使用的技术的概述。该算法遵循[22]中使用的基于证明的抽象细化循环。我们使用2.3节中描述的切割点插入作为抽象技术.作为初始抽象，我们插入割点，使得抽象模型的网表中的所有循环都被消除。这导致非常小的完整性阈值。与大多数实现抽象细化的相关论文相反，我们没有使用基于BDD的模型来验证抽象模型。相反，我们计算M的完整性阈值CT。这是描述在细节在第3节。二、然后用粘结剂CT在金属板上进行BMC。86D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）79进入摘要计算k：=CTBMCM|=kφ？是的属性保存没有细化伪反例BMC编号M|= kφ？混凝土臭虫图二.使用BMC和完整性阈值的如果该性质在M上成立，则我们可以推断它也在M上成立，并且算法终止。否则，我们从BMC运行中获得一个抽象的反例。然后循环继续进行相关的工作。细化步骤略有不同，并在第3.3节中进行了描述。3.2存在循环时计算CT我们推广了文[5]中的结果，以便得到更大类设计的完全性阈值。直径过近似的主要问题是闩锁依赖图中的循环。对于无环组分，最重要的结果总结见第2.2节。因此，考虑在锁存器依赖图中具有周期的电路。这样的周期是非常常见的，并且通常由计数器或流水线电路中的转发逻辑产生。为了过度近似这种电路的直径，我们定义了加权分量图的概念定义3.1加权分量图是一个分量图（如定义2.6所示），其中每个边都被分配了一个权重ω我们写C1→ωC2i，则存在从C1到C2的边，其权为ω。令V1表示C1中的锁存器集合，使得存在到LDG中的C2中的锁存器的路径设V2用C2表示这些锁存器。权重对应于连接V1和V2的信号的数量。作为一种特殊情况，考虑一个回路I，其直径为φI。我们假设电路可以用一个有n：=1级的流水线来表示。现在添加一个单位反馈环路（图3），形成电路O。形成反馈回路的信号在I的最后一级计算，并用作I的第一级的输入。从阶段i到阶段i+1有任意连接，但不允许有其他连接。权利要求3.2具有n级和一位反馈回路的简单流水线的直径以2·n为界。D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）7987··→ ⇐⇒∨i=1·KIO=2k·1. . .0 1我不知道你在说什么I−1X. . .图三.具有一位自环的组件的直径以2 μ I为界，其中μI表示不具有环的组件的直径的界。见图4。具有自环的组件的直径由I2 k限定，其中I表示不具有环的组件的直径的界限，并且k是环的权重。我们在附录中提供了权利要求3.2的证明。这个结果可以通过逐位消除外环来权利要求3.3令C1，...，表示成对不同分量的列表，a) 在依赖图中形成循环，以及b）不包含子循环，即，CiC jj= i + 1（i，j）=（n，1）.由该循环形成的分量的直径由2k乘以分量的直径的边界的总和来限定，其中k是循环上的任何边j的权重：ω（C1→ω1C2→ω2...→ωn−1 Cn→ωnC1） =2ωj·n（Ci）证明是通过重新安排组件，使得所需的边缘表示的反向循环，然后通过应用权利要求3.2k次。例3.4如果循环仅由一个分支组成（图4），则分支和循环的直径以I2 k为界，其中I表示不含循环的分支直径的界限，k表示循环的权重。k位计数器就是这种情况的一个例子如果循环有多个分量，则希望在具有最小权重的边缘上打破循环，因为边界在边缘的权重中是指数的。如图5所示：可以使用任一边缘删除循环。图6显示了共享一个组件的两个循环。 这种循环不能用上述方法消除。使用所有组件中的闩锁数量来估算直径。. . .88D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）79∆1∆2JC1C2C3K. . .. . .图五.可以使用具有权重k或j的边来打破循环。应选择具有最小权重的边。图六、两个圈共享一个顶点C2.循环不能被移除。3.3提炼抽象如果检测到虚假的反例，我们将获得用于模拟的BMC实例的不满意的核心。与[22]类似，我们识别这个核心中的信号（在[22]中，锁存器被识别）。我们通过删除与核心中发现的信号相对应的切割点来细化切割点。我们不引入新的分界点。4实验结果我们已经实现了第3节中描述的算法。我们使我们的实现可供其他研究人员进行实验我们将该算法应用于[16]中已经使用的各种电路，以确定其有效性。基准测试是从一个实施的顺序RISC微处理器与Tomasulo调度器。我们比较了新算法的性能与普通的有界模型检测的性能。所有实验都在运行Linux的2.5 GHz Intel Xenon机器上进行。Bounded Model Checking仅用于反驳，即，它不能断定没有错误跟踪。相反，它会将属性检查到给定循环数。 在[16]中，检查的属性与一个C程序我们检查安全属性，这更容易。表1总结了实验结果。每个电路的简短描述可以在[16]中找到。总之，传统的BMC通常优于新的算法，如果属性是要反驳。这是意料之中的，因为反驳是在精化循环中使用常规BMC实例完成的。然而，实验也D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）7989CT基准闩锁bug长度运行时间BMC运行时抽象分钟10203040ALU管道141920.2s3.5s26.7s132.5s*0.2sALU管2419--107.7s495.1s**1.1sRF11024--7.4s30.4s56.3s83.4s7.0sRF2102410.4s4.6s7.8s23.4s*7.5sROB12963--2.0s5.4s7.8s22.1s225.6sROB22963--182.8s***310.2sROB32963161.8s1.7s4.2s6.3s8.7s6.3sROB4296364*4.3s38.3s124.0s387.0s33.3s表1试验结果如果没有给出错误长度，则该属性保持不变。BMC的运行时间是针对不同深度给出的。“min”列包含最短反例的BMC运行时间（如果适用）星号（*）表示超过1000秒的超时如果要显示该属性，请显示该技术的好处在许多情况下，细化循环可以显示具有小范围的属性5结论我们提出了一个抽象细化循环，它只依赖于BMC作为其唯一的推理引擎。我们使用切割点插入，以获得一个抽象的模型，具有较小的完整性阈值。完整性阈值是过度近似的结构分析，允许循环电路。 如果抽象太粗糙，则会删除切割点，这会导致更少的虚假行为，但也会导致更大的完整性阈值。我们的初步实验结果表明，该技术在实现流水线的电路上表现良好。我们使我们的实现可供其他研究人员进行实验。2今后工作本文提出的算法要求严格限制电路的锁存器依赖图的形状。 作为未来的工作，我们计划扩展计算算法，以允许任意闩锁依赖图。我们还计划改进改进细化算法，以便添加切割点，而不仅仅是删除。2http://www.inf.ethz.ch/personal/daniekro/ebmc/90D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）79引用[1] Awedh，M.和F.Somenzi，用有界模型检验证明，在：R。Alzheimer和D.A. Peled，editors，16th International Conference on Computer Aided Verification（CAV），Lecture Notes inComputer Science3114（2004），pp.96比108[2] 球，T。和S. Rajamani，Boolean Programs：A Model and Process for Software Analysis，Technical Report 2000-14，Microsoft Research（2000）.[3] Barner，S.，D. Geist和A. Gringauze，带重建分层和回溯的符号定位简化。，in：E. Brinksma和K. G. Larsen，编辑，第14届计算机辅助验证国际会议论文集，计算机科学讲义2404（2002），pp. 六十五比七十七[4] Baumgartner ， J. 和 A.Kuehlmann ， Enhanceddiameterboundingviastructuraltransformation，in：Design，Automation and Test in Europe Conference and Exposition（2004），pp.36比41[5] 鲍姆加特纳，J.，A. Kuehlmann和J.A. Abraham，通过结构分析进行属性检查，在：E。Brinksma和K. G. Larsen，编辑，第14届计算机辅助验证国际会议（CAV）会议，计算机科学讲义2404（2002），pp.151-165.[6] Biere，A.，A. Cimatti，E. Clarke和Y. Yhu，Symbolic model checking without BDDs，第五届国际系统构造与分析工具与算法会议论文集（TACAS），计算机科学讲义1579（1999），第1579页。193-207.[7] Burch，J.R.，E. M. Clarke，K. L. McMillan，D. L.迪尔和L. J. Hwang，Symbolic modelchecking：1020states and beyond，Information and Computation98（1992），pp.142-170[8] 乔汉，P.，E. M.克拉克，J.H. Kukula，S.萨普拉河Veith和D. Wang，Automated abstractionrefinement for model checking large state spaces using sat based conjuncict analysis. ，in：M.Aagaard和J. W. O’Leary, editors, 33-51.[9] Clarke，E.，O. Grumberg，S. Jha，Y.卢和V.H. 反例引导的抽象细化，在：CAV，2000年，pp。154-169。[10] Clarke，E.，O. Grumberg和D.Peled，[11] Clarke，E.，D.克鲁宁岛Strichman和J. Ouaknine，有界模型检查的完整性和复杂性，在：第五届验证，模型检查和抽象解释国际会议，计算机科学讲义2937（2004），pp. 85比96[12] Clarke，E. M.和E. A. Emerson，Synthesis of synchronization skeletons for branching timetemporal logic，in：Logic of Programs：Workshop，LNCS131，Springer-Verlag，1981。[13] Clarke，E. M.，A. Gupta，J. H. Kukula和O. Strichman，基于SAT的抽象细化， 使用ILP和机器学习技术。，in ：E. Brinksma 和K. G. Larsen ，编辑，第14届计算机辅助验证国际会议（CAV）会议记录，计算机科学讲义2404（2002），pp.265-279。[14] Copty，F.，L.菲克斯河Fraer，E. Giunchiglia，G. Kamhi，A. Tacchella和M. Y. Vardi，Benefitsof bounded model checking at an industrial setting，in：G.贝里，H。Comon和A. Finkel，editors，Proceedings of the 13th International Conference on Computer Aided Verification（CAV 2001），number 2102 in Lecture Notes in Computer Science（2001），pp.436-453[15] 达斯，S。和D.Dill，抽象转换关系的逐次逼近，在：第16届IEEE计算机科学逻辑年会（LICS）（2001），pp.51比60[16] Kroening ， D. 和 E.Clarke ， Checking consistency of C and Verilog using predicateabstraction and induction，in：Proceedings of ICCAD（2004），pp.66-72.D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）7991[17] Kroening，D.和O.Strichman，递归直径的有效计算，在：L。扎克，P. Attie，A. Cortesi和S. Mukhopadhyay，编辑，第四届验证，模型检查和抽象解释国际会议，计算机科学讲义2575（2003），pp. 298-309.[18] Kuehlmann，A.和F. Krohm，使用切割和堆的等效性检查，在：第34届设计自动化年度会议（DAC）（1997年）会议记录中，pp.263-268。[19] 库尔尚河，“Computer-aided verification of coordinating processes: the automata-theoreticapproach,” Princeton University Press,[20] 李，B.，C. Wang和F. Somenzi，使用满意度作为唯一决策程序的符号模型检查中的抽象细化，国际软件工具技术转移杂志（STTT）7（2005），pp. 143-155[21] McMillan，K.，在无界符号模型检验中应用SAT方法，在：第14届计算机辅助验证，2002年，pp。250-264。[22] McMillan，K.和N.Amla，Automatic abstraction without counterexamples，收录于第九届国际系统构造与分析工具与算法会议论文集（TACAS），计算机科学讲义（2003）。[23] McMillan，K. L.，内插和基于SAT的模型检测，在：W。A. H. Jr.和F. Somenzi，编辑，第15届计算机辅助验证（CAV）国际会议论文集，计算机科学讲义2725（2003），pp.1-13号。[24] Mneimneh，M.和K. Sakallah，基于SAT的顺序深度计算，在：亚洲南太平洋设计自动化会议（ASPDAC），2003年，pp.87比92[25] Moskewicz，M.，C. Madigan，Y.赵湖，加-地Zhang和S. Malik，Cha Cha：Engineering anefficient SAT solver，in：DAC，2001，pp. 530-535[26] Shepherd，M.，S. Singh和G. 张文龙，应用归纳法与SAT求解器的安全性检验，第三届计算机辅助设计形式化方法国际会议（FMCAD）（2000年），页。108比125[27] Shtrichman，O.，为有界模型检查调整，在：E。Emerson和A.Sistla，编辑，第12届计算机辅助验证国际会议论文集（CAV 2000），计算机科学讲义（2000年），pp.480-494.[28] Wang，D.，中国科学院，P. Ho，J. Long，J. Kukula，Y. Zhu，T. Ma和R. Damiano，通过形式，模拟和混合引擎的抽象细化进行形式属性验证，在：DAC，2001年，pp.35比40一 证明令Di表示级i中的寄存器可以取的值的范围。令Pi（t）∈Di表示在时间t时流水线阶段i中的值。当i >0时，Pi只依赖于Pi−1。设fi表示该依赖关系的函数：（A.1）Pi（t）=fi（Pi−1（t−1））令Γ（t）∈B表示时间t处的反馈比特的值。仅使用Pn−1我们用γn−1表示函数，代表了这种依赖性。（A.2）Γ（t）=γn−1（Pn−1（t））这个定义可以归纳地扩展到其他阶段：92D. Kroening/Electronic Notes in Theoretical Computer Science 144（2006）79∈D≥≤·(A.3)γi（x）：=γi+1（fi+1（x））因此，一旦到达最后一级，级i中的数据值xi将产生γi（x定义A.1我们称γi（x）为阶段i的颜色。引理A.2对于所有0≤i≤jn，阶段j在时间t的颜色是阶段i在时间t-j+i的颜色：γn−1（Pn−1（t））=γi（Pi（t−j+i））这个引理的证明很容易通过n−1−i上的归纳法来完成。令i（t）表示周期t中的主输入的值。第一阶段的计算值仅取决于反馈位和这些主要输入。设第一阶段计算的值表示为f0（i，γ）∈D0。引理A.3任何阶段在时间t n的值只取决于主输入和n个周期前同一阶段的颜色。证据首先，观察到t≥n时的Pi（t）仅取决于周期t−i−1期间的主输入值和时间t−i−1时的反馈位值：(A.4) P i（t）= f i. f0（i（t − i − 1），Γ（t − i − 1））通过扩展Eq中的定义A.2，我们得到：(A.5) P i（t）= f i. <$f0（i（t − i − 1），γn−1（Pn−1（t − i − 1）我们可以使用引理A.2，其中j=n−1来重写等式。A.5并获得：(A.6) P i（t）= f i. f0（i（t−i−1），γi（Pi（t−n）阶段i在时间t-n的颜色是γi（Pi（t-n）），这就结束了这个主张。Q我们现在展示主要的主张3.2。证据[权利要求3.2]我们证明了我们可以在2·n个时钟周期或更少的时间内使流水线进入任何可达状态。如果s是可达的，则必须存在路径s0，...， s t从初始状态s0到状态s=st。 设t表示路径的长度，如果t2n，则没有什么可显示的.否则，我们使电路进入状态s如下：（1）我们从相同的初始状态s0开始。(2)在接下来的n个周期中，通过选择适当的主输入，我们将流水线带入一个状态，使得时间n的颜色与状态st-n的颜色匹配。这样的主输入存在，否则st−n是不可达的。（3）在周期n到2n- 1中，我们将流水线带入所需通过简单地重放用于获得st−n+1，.， s t。根据引理A.3，这是充分的。Q