Digital Modeling of Asynchronous Integrated Circuits

The project proposal DMAC: Digital Modeling of Asynchronous Integrated Circuits for Fast Dynamic Timing Analysis and Formal Verification 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. This proposal emerged from some discoveries obtained in the context of two recent FWF projects, where we happened to realize the importance of the scientific questions to be addressed in DMAC from two very different angles: As a basis for correctness proofs of fault-tolerant digital circuits and as a mandatory prerequisite for practical formal verification of reasonably large asynchronous circuit designs. In our attempts to get a first grip on these scientific questions, we incidentally discovered a new involution channel model that differs from almost all existing ones in that the input-to-output delay depends on the history in the signal traces. Interestingly, it turned out to be the only candidates for a faithful digital circuit model known so far. DMAC is devoted to fully explore this avenue scientifically. The most challenging open questions that shall be answered in this project are how to enlarge the class of circuits where the involution model and variants thereof are indeed faithful, how to compose gates with different electrical properties, how to parameterize 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 incorporate our models into existing timing analysis and verification tools. Besides demonstrating the practical feasibility of our approach, this is a mandatory step for experimentally evaluating the accuracy of our models.

The project DMAC (Digital Modeling of Asynchronous Integrated Circuits for Fast Dynamic Timing Analysis and Formal Verification) was devoted to the development of purely digital models for asynchronous circuits, which enable accurate and fast dynamic timing analysis and are a mandatory prerequisite for any attempt on practical formal verification of such designs. The models were supposed to 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 targeted continuous-time discrete-value models here, which essentially boil down to elaborate delay models for gates and/or interconnecting channels. These project goals were reached via the development of our Involution Delay Model and our Hybrid Thresholded Delay Models for multi-input gates, which were even implemented in a prototype tool for fast dynamic timing analysis of digital integrated circuits.