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

C.-L. Chen, T. Lin, and H.-C. Yen (Taiwan)


Parametric Timed Automata, Asynchronous Circuits, Tim ing Diagrams, Model Checking


Many successful model checking methods have been ap plied 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 au tomata) which are subclasses of general PTAs with a decid able reachability problem. A transformation from Regular Timing Diagrams (RTDs) to PTA is also introduced. Al though formal methods present an emerging technique in computer aided verification, designers sometimes use in formal notations or diagrams to describe and analyze real world systems. We develop an approach to transform RTDs into PTA, in order to take advantage of the reachability al gorithm designed for PTAs.

Important Links:

Go Back