In this paper, we propose a task allocation method for multi-core systems based on the Duplication with Temporary Triple-Modular Redundancy and Reconfiguration (DTTR) scheme. The proposed method statically determines task allocation for given task graph and multi-core system model from task scheduling for fault patterns of cores. In the experiments, we evaluate the task allocation time and the overhead for the execution time while changing multi-core system models, task graphs, and upper bound of faulty cores. The proposed method allocates a task graph with 100 tasks to a multi-core system with 16 cores within a practical timeout condition. This task allocation allows the system to operate with a reasonable execution time overhead even if 6 arbitrary cores become faulty.

Several studies have been made on comparison between synchronous and asynchronous NoCs (Network-on- Chips). However, very few attempts have been made at fair comparison between synchronous NoCs designed by synchronous researchers and asynchronous ones designed by asynchronous researchers under the same functional specification using the same fabrication technology. In this paper, representative routers of both design styles are individually designed under the same conditions. Then, they are precisely compared in the viewpoint of area, latency, power, and fairness. As a result, we show "areas of specialty" of both routers, e.g., real-time control systems for asynchronous routers and multi-media data processing systems for synchronous ones.

Since asynchronous circuits consume power only when activities actually happen, the conventional serial communication scheme where the embedded clock is always transmitted and the clock and data recovery (CDR) circuit is continuously working is very wasteful for connecting asynchronous circuit cores. This paper proposes a new serial communication scheme for asynchronous circuits where the power consumption of the line drivers in the transmitter and the deserializer in the receiver are reduced to almost 0 for the period when no data is transmitted. The proposed scheme is based on a new encoding mechanism where four voltage levels are used in order to embed a clock signal explicitly and a new sampler that extracts the clock and data without using PLL/DLL based circuits. This paper shows overall ideas of the proposed scheme and some initial HSPICE simulation results using 28nm and 130nm device technologies.

This paper proposes multiple-clock multiple-edge-triggered multiple-bit flip-flops for designing simple and straight-forward asynchronous control circuits of the two-phase handshaking protocol. The proposed flip-flops have multiple clocks and multiple data inputs, and each data input can be stored in the flip-flop at both the rising edge and the falling edge of the corresponding clock. They can be applied in the asynchronous design of the two-phase handshaking protocol not only for synthesizing simple control circuits, but also for obtaining robust circuits. The performance of the proposed flip-flops have been evaluated using the PTM 22 nm HP device parameters.

Network-on-Chip (NoC) is now considered to be a promising approach to implementing many-core systems and some real-time applications are executed on them. However, it has not yet been proven that on-chip networks can theoretically satisfy the hard real-time constraints. In this paper, we propose the worst-case performance models of on-chip networks which represent the upper bound latency between NoC nodes. We explain when the latency becomes the maximum value and show some evaluation results of the proposed model based on two deadlock-free routing algorithms.

This paper proposes a multi-chip NoC approach for implementing centralized ECUs. Unlike the conventional approach where ECUs and sensors/actuators are connected tightly, it has potential to implement efficient and reliable systems for automotive applications. Then, this paper reports our experience of implementing our first chip designed for the multi-chip NoC platform, and shows some experimental results.

Network-on-Chip (NoC) is considered to be a promising approach to implement many-core systems and a large number of on-chip router optimization studies have been proposed. In this paper, we propose to dynamically adjust link-width of each port on a router optimized to spatially biased traffic. Different from the previous No Coptimization approaches, in which the optimization is almost performed in the NoC design step, the proposed method achieves a dynamical link-width optimization at run-time.

Mixed-signal designs integrate digital and analog circuits which complicates the already difficult verification problem. This paper presents a model, labeled hybrid Petri nets (LHPNs), that is developed to model this heterogeneous set of components. To support formal verification, this paper presents an efficient zone-based state space exploration algorithm for LHPNs. This algorithm uses a process known as warping which allows zones to describe continuous variables changing at variable rates. Finally, this paper describes the application of this algorithm to analog/mixed-signal circuit examples.

This paper proposes a floorplan method for asynchronous circuits with bundled-data implementation on FPGAs. The proposed method minimizes the delay of the control circuit while considering timing constraints required for bundled-data implementation. Through the implementation of the proposed method, this paper evaluates the proposed method in terms of performance and area for generated floorplans.

Divide-and-conquer is essential to address state explosion in model checking. Verifying each individual component in a system, in isolation, efficiently requires an appropriate context, which traditionally is obtained by hand. This paper presents an efficient modular model checking approach for asynchronous design verification. It is equipped with a novel abstraction refinement method that can refine a component abstraction to be accurate enough for successful verification. It is fully automated, and eliminates the need of finding an accurate context when verifying each individual component, although such a context is still highly desirable. This method is also enhanced with additional state space reduction techniques. The experiments on several nontrivial asynchronous designs show that this method efficiently removes impossible behaviors from each component including ones violating correctness requirements.

In this paper, we propose two new N-way arbiter circuits. One circuit is based on the token-ring arbiters and another circuit is based on the mesh arbiters. The idea of the ring arbiter is to generate a lock signal by a token which is based on the non-return-to-zero signaling. It can achieve low latency and high throughput arbitration for a heavy work load environment. The idea of the mesh arbiter is to perform arbitrations between N/2 pairs at the same level and repeat them N-1 times. They can issue grant signals fairly. In this paper, we compare the performance of these N-way arbiters using 65nm process technologies qualitatively and quantitatively. We conclude that the proposed mesh arbiters are suitable when the number of inputs is 5 or less. We also conclude that we must select the appropriate arbiters considering tradeoff between latency, throughput, area, and energy when the number of inputs is larger than 5.

This paper presents two symbolic model checking algorithms for the verification of analog/mixed-signal circuits. The first model checker utilizes binary decision diagrams while the second is a bounded model checker that uses a satisfiability modulo theory solver. Both methods have been implemented, and preliminary results are promising.

This paper presents a Boolean based symbolic model checking algorithm for the verification of analog/mixed-signal (AMS) circuits. The systems are modeled in VHDL-AMS, a hardware description language for AMS circuits. The VHDL-AMS description is compiled into labeled hybrid Petri nets (LH-PNs) in which analog values are modeled as continuous variables that can change at rates in a bounded range and digital values are modeled using Boolean signals. System properties are specified as temporal logic formulas using timed CTL (TCTL). The verification proceeds over the structure of the formula and maps separation predicates to Boolean variables. The state space is thus represented as a Boolean function using a binary decision diagram (BDD) and the verification algorithm relies on the efficient use of BDD operations.

This paper presents an efficient method for verifying hazard-freedom in gate-level timed asynchronous circuits. Timed circuits are a class of asynchronous circuits that are optimized using explicit timing information. In asynchronous circuits, correct operation requires that there are no hazards in the circuit implementation. Therefore, when designing an asynchronous circuit, each internal node and output of the circuit must be verified for hazard-freedom to ensure correct operation. Current verification algorithms for timed circuits require an explicit state exploration that often results in state explosion for even modest-sized examples. The goal of this paper is to abstract the behavior of internal nodes and utilize this information to make a conservative determination of hazard-freedom for each node in the circuit. Experimental results indicate that this approach is substantially more efficient than existing timing verification tools. These results also indicate that this method scales well for large examples that could not be previously analyzed, in that it is capable of analyzing these circuits in less than a second. While this method is conservative in that some false hazards may be reported, our results indicate that their number is small

This paper presents a decomposition-based method for timed circuit design that is capable of significantly reducing the cost of synthesis. In particular, this method synthesizes each output individually. It begins by contracting the timed signal transition graph (STG) to include only transitions on the output of interest and its possible trigger signals. Next, the reachable state space for this contracted STG is analyzed to determine a minimal number of additional signals, which must be reintroduced into the STG to obtain complete state coding. The circuit for this output is then synthesized from this STG. Results show that the quality of the circuit implementation is nearly as good as the one found from the full reachable state space, but it can be applied to find circuits for which full-state-space methods cannot be successfully applied. The proposed method has been implemented as a part of our tool Nii-Utah Timed Asynchronous circuit Synthesis system (nutas), and its first version is available at http://research.nii.ac.jp/~yoneda.

System on a chip design results in the integration of digital, analog, and mixed-signal circuits on the same substrate which further complicates the already difficult validation problem. This paper presents a new model, labeled hybrid Petri nets (LHPNs), that is developed to be capable of modeling such a heterogeneous set of components. This paper also describes a compiler from VHDL-AMS to LHPNs. To support formal verification, this paper presents an efficient zone-based state space exploration algorithm for LHPNs. This algorithm uses a process known as warping to allow zones to describe continuous variables that may be changing at variable rates. Finally, this paper describes the application of this algorithm to a couple of analog/mixed-signal circuit examples.

This paper presents a method to address state explosion in timed-circuit verification by using abstraction directed by the failure model. This method allows us to decompose the verification problem into a set of subproblems, each of which proves that a specific failure condition does not occur. To each subproblem, abstraction is applied using safe transformations to reduce the complexity of verification. The abstraction preserves all essential behaviors conservatively for the specific failure model in the concrete description. Therefore, no violations of the given failure model are missed when only the abstract description is analyzed. An algorithm is also shown to examine the abstract error trace to either find a concrete error trace or report that it is a false negative. This paper presents results using the proposed failure-directed abstractions as applied to several large timed-circuit designs.

We present a method to address state explosion in timed circuit verification by using abstraction directed by the failure model. This method allows us to decompose the verification problem into a set of subproblems, each of which proves that a specific failure condition does not occur. To each subproblem, abstraction is applied using safe transformations to reduce the complexity of verification. The abstraction preserves all essential behaviors conservatively for the specific failure model in the concrete description. Therefore, no violations of the given failure model are missed when only the abstract description is analyzed. An algorithm is also shown to examine the abstract error trace to either find a concrete error trace or report that it is a false negative. We present results using the proposed failure directed abstractions as applied to two large timed circuit designs.

Using a level-oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model datapath circuits. On the other hand, in order to use such a model on large circuits, techniques to avoid the state explosion problem must be developed. This paper first introduces a level-oriented formal model based on time Petri nets, and then proposes its partial order reduction algorithm that prunes unnecessary state generation while guaranteeing the correctness of the verification.

Conformance has been used as a correctness criterion for asynchronous circuits. In the case of untimed systems, conformance of an implementation to a specification is equivalent to the failure-freeness between the implementation and the mirror of the specification. For bounded-delay systems, in general this property does not hold. In this paper, we define various notions of failures and examine whether the above property holds or not. We then discuss an alternative and effective algorithm for conformance checking of bounded-delay asynchronous circuits.

For the formal verification of asynchronous circuits, a framework to support trace theoretic verification of timed circuits and systems was developed. 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.

It is known that many systems have the regular structure constructed from several kinds of basic modules. We focus on parameterized asynchronous circuits with a wheel structure, which consists of one kernel module and many identical symmetry modules, and aim at verifying such systems of arbitrary sizes. In this paper we propose a fully automatic state enumeration procedure for wheel structured systems with an infinite number of symmetry modules based on the state representation using finite automata. We also apply a partial order reduction algorithm for the verification of the wheel structured systems in order to reduce the average computational costs, and demonstrate the efficiency of the proposed algorithm by several experimental results.