Similar to cyber-physical systems, analog/mixed-signal circuits are hybrid systems with a combined discrete and continuous dynamics. The hybrid dynamics makes it very hard to analyze those circuits and even simulation of those systems can be very time consuming. On top of that, many circuits are used in safety critical applications, such as pace makers or drive-by-wire systems. Thus, the need for a formal analysis of those systems is steadily increasing.
The objective of this research is to use hybrid automata as a modeling formalism for analog/mixed-signal circuits. Based on this formalism, new methods on automatic test generation and formal verification are developed. First results of a phase-locked loop indicate that formal verification of analog/mixed-signal circuits is feasible.