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 statespace explosion, or efficient algorithms which use a (conservative) approximation to avoid state-space explosion but can result in the rejection of designs which are valid. In particular, [7] presents a timed extention of the work in [1] which is very efficient but is not able to handle circuits with internal loops, which prevents its 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. Secondly, we propose a new (conservative) semantics for 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 addresses the limitations of the previous approaches.