Digital Modeling of Asynchronous Integrated Circuits

The project Digital Modeling of Asynchronous Integrated Circuits (DMAC) is devoted to the development of a purely digital model for asynchronous circuits, which enables accurate and fast dynamic timing analysis and is a mandatory prerequisite for any attempt on practical formal verification of such designs. The envisioned model shall be accurate and realistic (= faithful), in the sense that the behavior of circuits described in the model is exactly, i.e., within the modeling accuracy, the same as the behavior of the corresponding real circuit. In contrast to analog models, which are known to be faithful but suffer from excessive simulation times, we target continuous-time discrete-value models here, which essentially boil down to elaborate delay models for gates and/or interconnecting channels.

The project builds on our novel involution model, which considers input-to-output delays as as function of the history in the signal trace. DMAC will fully explore this avenue scientifically, by answering questions such as how to enlarge the class of circuits where the involution model and variants thereof are faithful, how to compose gates with different electrical properties, in particular, different threshold voltage levels, how to accurately model subtle delay variation originating in the Charlie effect in multi-input gates, how to parametrize and characterize the model for a given technology and given operating conditions, and how to possibly further improve the modeling coverage and accuracy. In addition, we will also make the first steps to incorporate our models into existing timing analysis and verification tools for validation purposes.

Keywords: Digital integrated circuits, continuous-time delay modeling, dynamic timing analysis, model composition, correctness proofs, formal verification.

Project duration: 2019-2023