Sciweavers

Share
ATVA
2007
Springer

Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver

10 years 4 months ago
Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver
This paper presents a bounded model checking algorithm for the verification of analog and mixed-signal (AMS) circuits using a satisfiability modulo theories (SMT) solver. The systems are modeled in VHDL-AMS, a hardware description language for AMS circuits. In this model, system safety properties are specified as assertion statements. The VHDL-AMS 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. The verification method begins by transforming the LHPN model into an SMT formula composed of the initial state, the transition relation unrolled for a specified number of iterations, and the complement of the assertion in each set of state variables. When this formula evaluates to true, this indicates a violation of the assertion and an error trace is reported. This method has been implemented and preliminary results are...
David Walter, Scott Little, Chris J. Myers
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where ATVA
Authors David Walter, Scott Little, Chris J. Myers
Comments (0)
books