Timing analysis of asynchronous circuits using timed automata

In this paper we present a method formodeling asynchronous digital circuits by timed automata. The constructed timed automata serve as \mechanical" and veri able objects for asynchronous sequential machines in the same sense that (untimed) automata do for synchronous machines. These results, combined with recent results concerning the analysis and synthesis of timed automata provide for the systematic treatment of a large class of problems that could be treated by conventional simulation methods only in an ad-hoc fashion. The problems that can be solved due to the results presented in this paper include: the reachability analysis of a circuit with uncertainties in gate delays and input arrival times, inferring the necessary timing constraints on input signals that guaranteea proper functioningof a circuit and calculatingthe delay characteristics of the components required in order to meet some given behavioral speci cations. Notwithstanding the existence of negative theoretical re...

• Type: Conference
• Year: 1995
• Where: CHARME
• Authors: Oded Maler, Amir Pnueli
• Keywords: CHARME 1995, Hardware, Timed Automata, Timed Automata Analysis, Timed Automata Provide