Model Checking of Analog Systems using an Analog Specification Language

In this contribution an advanced methodology for model checking of analog systems is introduced. A new analog specification language (ASL)for efficient property specifications is defined and model checking algorithms for implementing this language are presented. This allows verification of complex static and dynamic circuit properties like oscillation and startup time that have not yet been formally verifiable with previous approaches. The new verification methodology is applied to example circuits and experimental results are discussed and compared to conventional circuit simulation.