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
