Abstract interpretation of combinational asynchronous circuits

Abstract

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. A hierarchy of alternative abstractions linked by Galois connections is presented, each 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 S and C representing 'unknown but fixed for all time' and 'can never glitch' respectively. © Springer-Verlag 2004.