Abstract interpretation of combinational asynchronous circuits

A technique, based upon abstract interpretation, is presented that allows general gate-level combinational asynchronous circuits with uncertain delay characteristics to be reasoned about. Our approach is particularly suited to the simulation and model checking of circuits where the identification of possible glitch states (static and dynamic hazards) is required. We present a concrete model based upon signals represented as (possibly non-deterministic) functions from absolute dense time to the Booleans, and a hierarchy of achronous abstractions linked by Galois connections, each model offering varying tradeoffs between accuracy and complexity. Many of these abstract domains resemble extended, multi-value logics: transitional logics that include extra values representing transitions as well as steady states, and static/clean logics that include the values image and image representing ‘unknown but fixed for all time’ and ‘can never glitch’ respectively. Our framework captures several pre-existing analyses as particular instances in the hierarchy of abstractions.