Paper Info
Title
Bounded model checking of analog and mixed-signal circuits using an SMT solver
Abstract
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 promising.
Year
DOI
Venue
2007
10.1007/978-3-540-75596-8_7
ATVA
Keywords
Field
DocType
hardware description language,mixed-signal circuit,smt formula,lhpn model,initial state,analog value,bounded model checking algorithm,ams circuit,smt solver,assertion statement,vhdl-ams description,bounded range,satisfiability modulo theories
Discrete mathematics,Petri net,Model checking,Computer science,Algorithm,Theoretical computer science,Solver,Boolean data type,Hybrid automaton,Satisfiability modulo theories,Hardware description language,Bounded function
Conference
Volume
ISSN
ISBN
4762
0302-9743
3-540-75595-0
Citations 
PageRank 
References 
8
0.64
24
Authors
3
Name
Order
Citations
PageRank
David Walter1985.38
Scott Little21329.42
Chris Myers37210.44