Formal verification is a method to mathematically prove the correctness of a system design with respect to a property specification (model checking) or a reference implementation (equivalence checking). At the Electronic Design Automation Group, advanced methods for formal verification of analog and mixed analog/digital circuits and systems are developed. Research focuses on circuit modeling for verification, property specification languages, and formal verification algorithms.
The synthesis problem could be divided in topology construction and circuit sizing. One approach deals with on circuit sizing, which determines transistor dimensions and other circuit parameters automatically on a formal basis, resulting verified sizing with optimal performances for small circuit sizes. Another approch tries to find circuit topologies in an automatic way using symbolic analysis for synthesis and analysis subtasks.
Recent semiconductor technologies are challenging not only due to large parameter variations but also due to aging of the transistors itself. At the design methodology group we develop analysis techniques for modling NBTI-aging of transistors in analog circuits and largely differing time scales and methods for redundant self-healing system configurations of heterogeneous (especially analog) systems.
The design and use of analog circuits are increasingly shifting to higher levels of abstraction. Hence today all the systems are designed using some analog components. Within companies, as well as for customer relations paper specifications for analog / mixed-signal components are still commonly used, which hinderes a consistent, error-free design process. Subject of the developed machine-readable specification include digital IO cells as an LVDS driver and the classical analog cells e.g. OPs, ADCs, DACs. The specification is targeted to be used in a fully automated verification procedure and prepares for the synthesis of analog cells. The aim is to develop a complete description of all design and verification properties with the necessary information in a consistent way.