Framework for formally verifying analog and mixed-signal designs

Abstract

This chapter proposes a complementary formal-based solution to the verification of analog and mixed-signal (AMS) designs. The authors use symbolic computation to model and verify AMS designs through the application of induction-based model checking. They also propose the use of higher order logic theorem proving to formally verify continuous models of analog circuits. To test and validate the proposed approaches, they developed prototype implementations in Mathematica and HOL and target analog and mixed-signal systems such as delta-sigma modulators.