Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings
Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings
复制标题
使用展开的异步电路的迹线理论验证
DOI：
10.1007/3-540-60045-0_50
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
K. McMillan
中科院分区：
文献类型：
--
作者：
K. McMillan
提出了一种基于Petri网展开的速度无关电路的层次化迹论验证方法。其目的是避免由于并发转换的交错而导致的状态爆炸。电路元件的迹线结构用Petri网表示。实现和规范之间的一致性测试组成的实现与规范的镜像，展开产生的产品网到一个发生网，并测试此网的故障。后一个问题被证明是NP完全的，但一个实用的分支定界算法。在两个可扩展的异步控制电路的例子中，发现展开大小随着电路大小线性增长，而状态的数量呈指数增长。在一种情况下，展开方法成功地验证了大型配置，而基于BDD的遍历技术没有。
An approach is presented for hierarchical, trace-theoretic verification of speed-independent circuits based on Petri net unfolding. The purpose is to avoid the explosion of states that results from interleaving of concurrent transitions. The trace structures of the circuit components are represented by Petri nets. Conformance between implementation and specification is tested by composing the implementation with the mirror of the specification, unfolding the resulting product net into an occurrence net, and testing this net for failures. The latter problem is shown to be NP-complete, however a practical branch-and-bound algorithm is presented. In two examples of scalable asynchronous control circuits, the unfolding size is found to grow linearly with the circuit size, while the number of states grows exponentially. In one case, the unfolding method succeeds in verifying large configurations while BDD-based traversal techniques do not.