Verification of Analog/Mixed-Signal Circuits Using Symbolic Methods

David Walter, Scott Little, Chris Myers, Nicholas Seegmiller, Tomohiro Yoneda
December 2008
DOI

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.

Type
Journal article
state-space methods analog/mixed-signal circuits binary decision diagram Boolean function hardware description language mixed analogue-digital integrated circuits formal verification model checker satisfiability modulo theories satisfiability modulo theory solver symbolic methods symbolic model checking space exploration semiconductor device noise petri nets circuit analysis analog circuits analog/mixed-signal (AMS) circuits data structure time domain analysis mechanical factors
David Walter
David Walter
Amazon (AWS S3), Senior SDE
Scott Little
Scott Little
Maxim Integrated, EDA
Chris Myers
Chris Myers
Department Chair / Professor

Related