Using a level oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model data-path circuits. On the other hand, in order to use such a model for larger circuit, some technique to avoid the state explosion problem is essential. This paper first defines a level oriented formal model based on time Petri nets, and then proposes a partial order reduction algorithm that prunes unnecessary state generation while guaranteeing the correctness of the verification.

We present a new framework for checking safety failures. The approach is based on the conservative inference of the internal states of a system by the observation of the interaction with its environment. It is based on two similar mechanisms : forward implication, which performs the analysis of the consequences of an input applied to the system, and backward implication, that performs the same task for an output transition. While being a very simple approach, it is general and we believe it can yield efficient algorithms in different safety-failure checking problems. As a case study, we have applied this framework to an existing problem, the hazard checking in (speed-independent) asynchronous circuits. Our new methodology yields an efficient algorithm that performs better or as well as all existing algorithms, while being more general than the fastest one.

This work proposes a technique to automatically obtain timing constraints for a given timed circuit to operate correctly. A designated set of delay parameters of a circuit are first set to sufficiently large bounds, and verification runs followed by failure analysis are repeated. Each verification run performs timed state space enumeration under the given delay bounds, and produces a failure trace if it exists. The failure trace is analyzed, and sufficient timing constraints to prevent the failure are obtained. Then, the delay bounds are tightened according to the timing constraints by using an ILP (Integer Linear Programming) solver. This process terminates when either some delay bounds under which no failure is detected are found or no new delay bounds to prevent the failures can be obtained. The experimental results using a naive implementation show that the proposed method can efficiently handle asynchronous benchmark circuits and nontrivial GasP circuits.

A new pipeline controller based on the Early Acknowledgement (EA) protocol is proposed for bundled-data asynchronous circuits. The EA protocol indicates acknowledgement by the falling edge of the acknowledgement signal in contrast to the 4-phase protocol, which indicates it on the rising edge. Thus, it can hide the overhead caused by the resetting period of the handshake cycle. Since we have designed our controller assuming several timing constraints, we first analyze the timing constraints under which our controller correctly works and then discuss their appropriateness. The performance of the controller is compared both analytically and experimentally with those of two other pipeline controllers, namely, a very high-speed 2-phase controller and an ordinary 4-phase controller. Our controller performs better than a 4-phase controller when pipeline has processing elements. We have obtained interesting results in the case of a non-linear pipeline with a Conditional Branch (CB) operation. Our controller has slightly better performance even compared to 2-phase controller in the case of a pipeline with processing elements. Its superiority lies in the EA protocol, which employs return-to-zero control signals like the 4-phase protocol. Hence, our controller for CB operation is simple in construction just like the 4-phase controller. A 2-phase controller for the same operation needs to have a slightly complicated mechanism to handle the 2-phase operation because of the non-return-to-zero control signals, and this results in a performance overhead.

This paper introduces a partially parallel inter-chip link architecture for asynchronous multi-chip Network-on-Chips (NoCs). The multi-chip NoCs that operate as a large NoC have been recently proposed for very large systems, such as automotive applications. Inter-chip links are key elements to realize high-performance multi-chip NoCs using a limited number of I/Os. The proposed asynchronous link based on level-encoded dual-rail (LEDR) encoding transmits several bits in parallel that are received by detecting the phase information of the LEDR signals at each serial link. It employs a burst-mode data transmission that eliminates a per-bit handshake for a high-speed operation, but the elimination may cause data-transmission errors due to cross-talk and power-supply noises. For triggering data retransmission, errors are detected from the embedded phase information; error-detection codes are not used. The throughput is theoretically modelled and is optimized by considering the bit-error rate (BER) of the link. Using delay parameters estimated for a 0.13 µm CMOS technology, the throughput of 8.82 Gbps is achieved by using 10 I/Os, which is 90.5% higher than that of a link using 9 I/Os without an error-detection method operating under negligible low BER (<10-20).

This paper develops a modular synthesis algorithm for timed circuits that is dramatically accelerated by partial order reduction. This algorithm synthesizes each module in a hierarchical design individually. It utilizes partial order reduction to reduce the state space explored for the other modules by considering a single interleaving of concurrently enabled transitions. This approach better manages the state explosion problem resulting in a more than 2 order of magnitude reduction in synthesis time. The improved synthesis time enables the synthesis of a larger class of timed circuits than was previously possible.

This paper develops a framework to support trace theoretic verification of timed circuits and systems. A theoretical foundation for classifying timed traces as either successes or failures is developed. The concept of the semimirror is introduced to allow conformance checking thus supporting hierarchical verification of timed circuits and systems. Finally, we relate our framework to those previously proposed for timing verification.

The problem of self-timed implementation of Boolean functions is explained. The notions of combinational delay-insensitive code and delay-insensitive function are defined, giving precise conditions under which memoryless self-timed implementation of Boolean functions is feasible. Examples of combinational delay-insensitive code and delay-insensitive function are given. Generic design style, using standard CAD library, for constructing quasi delay-insensitive self-timed function blocks is suggested. Our design style is compared to other self-timed function block design styles.

In order to reduce state explosion problem, techniques such as symbolic state space traversal and partial order reduction have been proposed. Combining these two techniques, however, seems difficult, and only a few research projects related to this topic have been reported. In this paper, we propose handling single place zero reachability problem of Petri nets by using both partial order reduction and symbolic state space traversal based on ZBDDs. We also show experimental results of several examples.

Geometric region method is one of the techniques to handle real-time systems which have potentially infinite state spaces. However, the original geometric region method gives incorrect results for the CTL model checking of time Petri nets. In this paper, we discuss the sufficient condition for the geometric region graphs to be correct with respect to the CTL model checking of time Petri nets, and then propose a technique to partition given geometric regions so that the graphs satisfy the sufficient condition. Finally, we implement the proposed algorithm, and compare it with the other methods by using small examples.

This paper presents a formal verification method based on logic simulation. In our method, some restricted class of circuits which include data paths can be verified without abstraction of data paths by using symbolic values. Our verifier extracts a transition relation from the state graph (given as a specification) which is expressed using symbolic values, and verifies based on simulation using those symbolic values if the circuit behaves correctly with respect to each transition of the specification. If the verifier terminates with "correct," then it can be guaranteed that for any applicable input vector sequence, the circuit and the specification behaves identically. We have implemented the proposed method on a Unix workstation and verified some FIFO and LIFO circuits by using it.

The Scalable-Delay-Insensitive (SDI) model is proposed for high-performance asynchronous system design. In this paper, we focus on checking whether a circuit under SDI model satisfies some untimed properties, and formally show that checking these properties in the SDI model can be reduced to checking the same properties in the bounded delay model. This result suggests that the existing verification algorithms for the bounded delay model can be used for the verification of SDI circuits, which significantly helps the designers of SDI circuits.

In this paper, we propose a redundant task allocation method for multi-core systems based on the Duplication with Temporary Triple-Modular Redundancy and Reconfiguration (DTTR) scheme. The proposed method determines task allocation of a given task graph to a given multi-core system model from task scheduling in given fault patterns. Fault patterns defined in this paper consist of a set of faulty cores and a set of surviving cores. To optimize the average failure rate of the system, task scheduling minimizes the execution time of the task graph preserving the property of the DTTR scheme. In addition, we propose a selection method of fault patterns to be scheduled to reduce the task allocation time. In the experiments, at first, we evaluate the proposed selection method of fault patterns in terms of the task allocation time. Then, we compare the average failure rate among the proposed method, a task allocation method which packs tasks into particular cores as much as possible, a task allocation method based on Simulated Annealing (SA), a task allocation method based on Integer Linear Programming (ILP), and a task allocation method based on task scheduling without considering the property of the DTTR scheme. The experimental results show that task allocation by the proposed method results in nearly the same average failure rate by the SA based method with shorter task allocation time.

We propose a fault diagnosis and reconfiguration method based on the Pair and Swap scheme to improve the reliability and the MTTF (Mean Time To Failure) of network-on-chip based multiple processor systems where each processor core has its private memory. In the proposed scheme, two identical copies of a given task are executed on a pair of processor cores and the results are compared repeatedly in order to detect processor faults. If a fault is detected by mismatches, the fault is identified and isolated using a TMR (Triple Module Redundancy) and the system is reconfigured by the redundant processor cores. We propose that each task is quadruplicated and statically assigned to private memories so that each memory has only two different tasks. We evaluate the reliability of the proposed quadruplicated task allocation scheme in the viewpoint of MTTF. As a result, the MTTF of the proposed scheme is over 4.3 times longer than that of the duplicated task allocation scheme.

Multiple-way (N-way) asynchronous arbitration is an important issue in asynchronous system design. In this paper, novel implementation methods of N-way asynchronous arbiters are presented. We first present N-way rectangle mesh arbiters using 2-way mutual exclusion elements. Then, N-way token-ring arbiters based on the non-return-to-zero signaling is also presented. The former can issue grant signals with the same percentage for all the arriving request signals while the latency is proportional to the number of inputs. The latter can achieve low latency and low energy arbitration for a heavy workload environment and a large number of inputs. In this paper, we compare their performances using the 28nm FD-SOI process technologies qualitatively and quantitatively.

This paper proposes new scheduling methods for asynchronous circuits with bundled-data implementations. Since operations in asynchronous circuits start after the completion of a previous operation, this method approximates the set of start times for each operation using the delay of the resources. Next, this method decides on control steps from the approximated sets of start times, which are used in scheduling algorithms. This paper extends two scheduling algorithms used for synchronous circuits so that the approximated sets of start times and the decided control steps are used. Finally, this paper shows the effectiveness of our proposed methods by comparing scheduling results with ones obtained by the original two scheduling algorithms.

This paper proposes a partial order reduction algorithm for timed trace theoretic verification in order to detect both safety failures and timing failures of timed circuits efficiently. This algorithm is based on the framework of timed trace theoretic verification according to the original untimed trace theory. Consequently, its conformance checking supports hierarchical structure when verifying timed circuits. Experimenting with the STARI and DME circuits, the proposed approach shows its effectiveness.