用于验证的序列扩展正则表达式的综合
Synthesis of Sequential Extended Regular Expressions for Verification
摘要：
综合技术采用可实现的线性时序逻辑规范，并产生实现规范的正确电路。生成的电路可以直接使用，也可以用作检查逻辑设计正确性的斜接。通常，这些技术生成非确定性有限状态自动机，其可以以可能的指数代价确定。最近的研究结果表明，使用确定性自动机的符号和有界模型检验的LTL安全性能的多个优点。在本文中，我们提出了一种技术与支持工具，采取一个顺序扩展的正则表达式规范Φ，和一个逻辑设计实现S，并生成一个时序电路C，表示为一个与反转图，检查是否S满足Φ。该技术将生成的电路C传递给有界模型检查器ABC，以验证正确性。我们用自由输入变量对Φ中的不确定性进行编码，得到了许多状态，它们与Φ的大小成斜接线性关系。我们的技术成功地生成了模型检查器的输入，而其他技术由于指数爆破而失败，并且在大多数情况下，ABC成功地找到了设计中的缺陷，否则无法检查，或者验证了设计。我们评估了我们的技术对几个工业基准，包括IBM仲裁器，负载平衡器，和交通灯系统，并比较我们的结果与NuSMV框架。我们的方法发现了缺陷，并且验证了NuSMV无法验证的系统。
英文摘要：
Synthesis techniques take realizable Linear Temporal Logic specifications and produce correct cir- cuits that implement the specifications. The generated circuits can be used directly, or as miters that check the correctness of a logic design. Typically, those techniques generate non-deterministic finite state automata, which can be determinized at a possibly exponential cost. Recent results show multiple advantages of using deterministic automata in symbolic and bounded model checking of LTL safety properties. In this paper, we present a technique with a supporting tool that takes a sequential extended regular expression specification Φ, and a logic design implementation S, and generates a sequential circuit C, expressed as an And-Inverted-Graph, that checks whether S satisfies Φ. The technique passes the generated circuit C to ABC, a bounded model checker, to validate correctness. We use free input variables to encode the non- determinism in Φ and we obtain a number of states in miter linear in the size of Φ. Our technique succeeds to generate the input to the model checker while other techniques fail because of the exponential blowup, and in most cases, ABC succeeds to either find defects in the design that was otherwise uncheckable, or validate the design. We evaluated our technique against several industrial benchmarks including the IBM arbiter, a load balancer, and a traffic light system, and compared our results with the NuSMV framework. Our method found defects and validated systems NuSMV could not validate.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
