Formal verification of analog circuits is a method of proving the correctness of a design using mathematical methods. This method, which is widely used in digital circuits, allows a more precise design verification than the simulation.
We investigate in many methods for the formal verification of analog and mixed-signal circuits and systems. One of the developed methods is able to prove that two given nonlinear dynamic circuits have the same behavior (equivalence checking). This is done via a non-linear mapping of the associated state space representations of the two systems using a Kronecker canonical form and a nonlinear order reduction.
Another method may have certain properties, e.g. detect no occurrence of overshoots of analog circuits (model checking).
The research topic investigates in the automatic synthesis of analogue circuits, especially in structural synthesis. The methods generate structures (netlists) that are automatically sized in a commercial circuit sizing tool. This approach allows an overall full automatic design flow for analog circuits similar to the digital approach from specification to sized netlist. The main challenges is the suitable limitation of the search space which grows with circuit size and the adaptation to continuous technology changes.
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.
The design of energy-efficient neural networks is supported and optimized using the synthesis methods developped by us. Due to foccussing on analog implementations, we can implement circuits beeing very close to the technical limitations for energy consumption.
Machine-readable analog circuit specification provides significant productivity and security benefits. Especially in combination with formal methods, complete specifications can be created and tested.
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.
Symbolic analysis - a method underlying some of the above-mentioned topics - serves to set up and simplify a symbolic nonlinear differential equation system from the netlist description of a circuit. The main research topic is the development of simplification algorithms. The main goal is to increase the visibility of the circuit.