[Back]

U. Schmid:
"FWF-Proposal DMAC: Digital Modeling of Asynchronous Integrated Circuits";
Report No. TUW-278607, 2018.

The project proposal Digital Modeling of Asynchronous Integrated Circuits for Fast Dynamic Timing Analysis and Formal Verification (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.
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 discovered a new channel model that differs from almost all existing ones in that the input-to-output delay depends on the history in the signal traces. Most importantly, we identified delay functions that are mathematical involutions as being key for faithfulness, in the sense that we managed to rigorously prove that our involution channels are 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 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 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.

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

https://publik.tuwien.ac.at/files/publik_278607.pdf