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

Volume

27

Issue

12

fYear

2008

Firstpage

2223

Lastpage

2235

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;

fLanguage

English

Journal_Title

Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on

Publisher

ieee

ISSN

0278-0070

Type

jour

DOI

10.1109/TCAD.2008.2006159

Filename

4670059