Formal Verification of the Quasi-Static Behavior of Mixed-Signal Circuits by Property Checking

This paper proposes a verification flow for mixed-signal circuits. The presented flow is based on 'bounded model checking', a formal verification method. The behavior of the analog parts of a mixed-signal circuit is described with the help of rational numbers within the circuit description and in the properties, respectively. Our implemented Property-Checker checks formal properties for a given mixed-signal circuit design over a finite interval of time. The internal representation of the rational numbers has an almost arbitrary accuracy. By using the presented flow, the quasi-static behavior of a mixed-signal circuit can be exhaustively verified.