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.
Current research topic is the design and verification of cyber-physical systems. We look at these systems from physical modeling over automatic model generation of the electrical and systems on intermediate levels up to the construction and modling of on system level.
Exemplary fields of application are the automotive sector, the motorcycle sector and the e-bike sector as well as other areas. Methods for modeling, optimization, verification, signal processing, control and synthesis are being researched.
Machine-readable analog circuit specification provides significant productivity and security benefits. Especially in combination with formal methods, complete specifications can be created and tested.