Abstract:
During these last few years, asynchronous circuits have gained interest due to their potential advantages, such as local synchronization, elimination of the clock skew problem, faster and less power-consuming circuits, electro-magnetic compatibility and high degree of modularity. However, the concurrent nature of asynchronous circuits makes them difficult to design, verify and test. Despite the recent advances, more investigation is required to make asynchronous circuits attractive to the circuit design community. Unless solid automatic methodologies and tools appear, the intrinsic advantages of asynchronous will remain forever potential.
The goal of this work is providing automatic methodologies to guarantee that only correctly designed and manufactured asynchronous circuits are issued to the market. Consequently, the key points to tackle are specification validation, circuit verification and testing. Specification validation assures that the specification of the circuit has different properties. Circuit verification involves to processes: proving that a circuit behaves accordingly to its specification and guaranteeing that the circuit fulfills several properties. Testing exercises the circuit by applying different patterns to the circuit inputs; by selecting those patterns conveniently, a faulty and a correct circuit will exhibit different behavior.
Several languages and formalisms allow to specify the behavior of asynchronous circuits: CSP, Petri nets, process algebras, etc. We have chosen Petri nets because they are familiar to researchers in several fields, in particular to the asynchronous circuit design community. Since Petri nets are capable of representing a high degree of parallelism, even small nets may have a huge set of reachable markings (states). We present the isomorphism between Petri nets and boolean algebras that allows to represent sets of markings by means of boolean functions, and operations between sets by boolean operations. Symbolic BDD based techniques are used to efficiently manage these boolean functions and operations.
By using symbolic algorithms, similar to those used for traversing Finite State Machines, the set of reachable markings is computed. We propose some modifications to speed-up this computation, as well as algorithms to formally verify various properties.
The first goal of circuit verification is achieved by composing a circuit with its specification, thus forming a closed system. In our framework the specification is described as a Petri net and the circuit as a flat netlist of gates. Both specification and circuit are modeled by boolean functions and, therefore, the whole system can be represented and manipulated by using BDDs. Two approaches are presented: the first one uses all the variables of the circuit, whereas the second one automatically abstracts internal combinational signals. With this reduction in the number of signals, complexity is made dependent on the number of memory elements rather than on the number of signals. The necessary and sufficient conditions for the second method to be exact are also demonstrated.
The last contribution is devoted to testing asynchronous circuits. First, the behavior of the asynchronous circuit under test is characterized by means of symbolic BDD techniques. This analysis allows to obtain the set of patterns that can be used for testing. And second, a symbolic automatic test pattern generation algorithm, successfully used with synchronous circuits, is adapted to asynchronous circuits. This algorithm looks for test patterns, but only takes those that the previous circuit analysis permits. Other synchronous techniques like fault simulation and random test pattern generation are adapted and used to speed-up the whole process.
The correctness of verification and testing methods is mathematically proven and the efficiency is shown through numerous examples. The approaches are contrasted with previous work, and the advantages and drawbacks are discussed. It is worth mentioning that the presented methodologies are fully automated, and they have been implemented as automatic verification and test pattern generation tools.
On the basis exposed in this work, several topics appear as future lines of work. The problem of verification with timing constraints is the next step to obtain a more accurate methodology. In reference to testing, other fault models and test pattern generation for IDD testing will be considered. As a general consideration, verification and testing of mixed asynchronous-synchronous systems will be studied.