Title :
Verification of Analog/Mixed-Signal Circuits Using Symbolic Methods
Author :
Walter, David ; Little, Scott ; Myers, Chris ; Seegmiller, Nicholas ; Yoneda, Tomohiro
Author_Institution :
Univ. of Northern Philippines, Vigan
Abstract :
This paper presents two symbolic model checking algorithms for the verification of analog/mixed-signal circuits. The first model checker utilizes binary decision diagrams while the second is a bounded model checker that uses a satisfiability modulo theory solver. Both methods have been implemented, and preliminary results are promising.
Keywords :
Petri nets; binary decision diagrams; circuit analysis computing; formal verification; hardware description languages; mixed analogue-digital integrated circuits; analog/mixed-signal circuits; binary decision diagrams; model checker; satisfiability modulo theory solver; symbolic methods; symbolic model checking; Analog circuits; Boolean functions; Cities and towns; Data structures; Formal verification; Mechanical factors; Semiconductor device noise; Space exploration; State-space methods; Time domain analysis; Analog/mixed-signal (AMS) circuits; binary decision diagrams (BDDs); formal verification; satisfiability modulo theories;
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
DOI :
10.1109/TCAD.2008.2006159
