Sciweavers

Share
ASPDAC
2007
ACM

Symbolic Model Checking of Analog/Mixed-Signal Circuits

9 years 3 months ago
Symbolic Model Checking of Analog/Mixed-Signal Circuits
This paper presents a Boolean based symbolic model checking algorithm for the verification of analog/mixedsignal (AMS) circuits. The systems are modeled in VHDL-AMS, a hardware description language for AMS circuits. The VHDLAMS description is compiled into labeled hybrid Petri nets (LHPNs) 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.
David Walter, Scott Little, Nicholas Seegmiller, C
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where ASPDAC
Authors David Walter, Scott Little, Nicholas Seegmiller, Chris J. Myers, Tomohiro Yoneda
Comments (0)
books