Symbolic Model Checking of Analog/Mixed-Signal Circuits

David Walter, Scott Little, Nicholas Seegmiller, Chris J. Myers, Tomohiro Yoneda
January 2007
DOI

Abstract

This paper presents a Boolean based symbolic model checking algorithm for the verification of analog/mixed-signal (AMS) circuits. The systems are modeled in VHDL-AMS, a hardware description language for AMS circuits. The VHDL-AMS description is compiled into labeled hybrid Petri nets (LH-PNs) in which analog values are modeled as continuous variables that can change at rates in a bounded range and digital values are modeled using Boolean signals. System properties are specified as temporal logic formulas using timed CTL (TCTL). The verification proceeds over the structure of the formula and maps separation predicates to Boolean variables. The state space is thus represented as a Boolean function using a binary decision diagram (BDD) and the verification algorithm relies on the efficient use of BDD operations.

Type
Conference paper
Publication
2007 Asia and South Pacific Design Automation Conference
logic design state-space methods analog/mixed-signal circuits binary decision diagram Boolean function hardware description language mixed analogue-digital integrated circuits temporal logic timed CTL VHDL-AMS description formal verification circuit simulation labeled hybrid Petri net model logic real time systems oscillators Boolean variable petri nets circuit analog circuits Integrated circuit modeling
David Walter
David Walter
Amazon (AWS S3), Senior SDE
Scott Little
Scott Little
Maxim Integrated, EDA

Related