Modelling and Analysis of Asynchronous Circuits and Timing Diagrams Using Parametric Timed Automata

Many successful model checking methods have been applied to hardware design in real-time applications. In this paper, we apply Parametric Timed Automata (PTA) to model the delays of asynchronous circuits. The PTAs modelling the delays of asynchronous circuits fall into the so-called lower bound and upper bound automata (L/U automata) which are subclasses of general PTAs with a decidable reachability problem. A transformation from Regular Timing Diagrams (RTDs) to PTA is also introduced. Although formal methods present an emerging technique in computer aided verification, designers sometimes use informal notations or diagrams to describe and analyze realworld systems. We develop an approach to transform RTDs into PTA, in order to take advantage of the reachability algorithm designed for PTAs.