Verification of Asynchronous Circuits using Timed Automata
Marius Dorel Bozga, Hou Jianmin, Oded Maler, Sergio Yovine · Electronic Notes in Theoretical Computer Science · 2002
In this work we apply the timing verification tool OpenKronos, which is based on timed automata, to verify correctness of numerous asynchronous circuits. The desired behavior of these circuits is specified in terms of signal transition graphs (STG) and we check whether the synthesized circuits behave correctly under the assumption that the inputs satisfy the STG conventions and that the gate delays are bounded between two given numbers. Our results demonstrate the viability of the timed automaton approach for timing analysis of certain classes of circuits.