Formal Abstraction and Verification of Analog Circuits (faveAC)

The faveAC project is a project funded by the German Research Foundation (DFG). This project represents a collaboration between the Leibniz University of Hanover, the Technical University of Munich and the Gothe University of Frankfurt.

The project focusses on formal verification of AMS (Anlog-mixed-signal) circuits. Compared to the digital domain, verification is poorly distributed in the analog domain. Approaches to the verification of analog circuitry are not scalable with the exception of approaches for linear behavior. However, the nonlinear behavior of a circuit is usually the reason for the failure.

The University of Frankfurt investigates in a fully automated software solution that uses abstractions to model system behavior. The abstractions made should continue to describe the complete system behavior. The developed subsystems are then to be brought together using compositional methods. The aim is to develop an approach that is scalable as well as applicable for non-linear circuits and thus enables the verification of larger AMS circuits.

In order to secure the abstractions made, equivalence checking is used for various abstraction levels. Another goal is also to safely model parameter variations. Overall, the approach is compositional so that larger systems can be tested. Finally, the verification of the circuit is determined by means of an reachability analysis of the abstract system behavior versus the specification.