The design of asynchronous controllers is an error-prone task. The absence of clock makes every signal transition relevant to the observable behavior of the system. Glitches, that can be tolerated in synchronous systems as long as they are produced far from clock edges, are unacceptable in an asynchronous system.
This talk will present some strategies to automate the synthesis and verification of asynchronous controllers. The underlying support of these strategies are based on the theory of concurrency. The talk will describe a logic synthesis framework from formal specifications based on interpreted Petri nets. It will also address the problem of formal verification of asynchronous systems using symbolic techniques and will explain some recent achievements in the verification of timed circuits.