Hazard Checking of Timed Asynchronous Circuits Revisited

This paper proposes a new approach for the hazard checking of timed asynchronous circuits. Previous papers proposed either exact algorithms, which suffer from state-space explosion, or efficient algorithms which use ( conservative) approximations to avoid state-space explosion, but have the drawback of a rather conservative definition of failure states, which results in the rejection of designs which are valid. Algorithms based on [1], extending it to the timed case [7], while being very efficient, are unable to handle circuits with internal loops, which prevents their use in some cases. We propose a new approach to the problem in order to overcome the mentioned limitations, without sacrificing efficiency. To do so, we first introduce a general framework targeted at the conservative checking of safety failures. This framework is not restricted to the checking of timed asynchronous circuits. Then, we propose a new ( conservative) semantics to timed circuits, in order to use the proposed framework for hazard checking of such circuits. Using this framework with the proposed semantics yields an efficient algorithm that solves the limitations of the previous approaches.