Induced hierarchical verification of asynchronous circuits using a partial order technique.

摘要

Speed-independent circuits are asynchronous circuits that should "work correctly" regardless of their gate delays. Correctness---hazard-freedom and conformance of a circuit to its specification---can be verified by checking failure-freedom of a closed circuit. Being highly concurrent, asynchronous circuits may have state spaces that are exponential in the size of the circuit. Consequently, asynchronous circuit verification techniques that are based on full state space exploration frequently suffer from the so called state space explosion problem, even for moderately sized circuits.; To attack the state space explosion problem, a new theoretical framework for induced hierarchical verification of speed-independent circuits is proposed. In this framework, a closed circuit is partitioned into a set of circuit-blocks by an observationally-sufficient set of external signals. A partial order reduction technique is then used to find a safe abstraction of the behavior of the external signals. It is shown that if a safe abstraction is used to derive an abstract environment module for each circuit block, then the circuit is failure-free iff all of its sub-circuits are failure-free, where a sub-circuit is a circuit block composed with its abstract environment module. A divide and conquer approach that is based on this result can thus accurately verify a circuit by verifying its smaller sub-circuits in a hierarchical fashion.; A previous approach for induced hierarchical verification of speed-independent circuits used a form of functional abstraction to find safe abstractions and consequently it required the set of external signals to include all memory element outputs. The new framework is a generalization of the previous approach; it uses a partial order reduction technique (i.e., behavioral abstraction) to find safe abstractions, and asserts that inclusion of all memory element outputs is not a fundamental requirement for observational-sufficiency of a set of external signals. The proposed partial order technique successfully avoids the state explosion problem by exploring only one interleaving of internal signal transitions.; The framework is implemented into a CAD tool called SPHINX. Experimental results show significant speed-ups in verification of circuits dominated by memory elements.