Verification of Analog/Mixed-Signal Circuits Using Labeled Hybrid Petri Nets

Author

Little, Scott ; Walter, David ; Myers, Chris ; Thacker, Robert ; Batchu, Satish ; Yoneda, Tomohiro

Author_Institution

Freescale Semicond., Inc., Austin, TX, USA

Volume

30

Issue

4

fYear

2011

fDate

4/1/2011 12:00:00 AM

Firstpage

617

Lastpage

630

Abstract

Mixed-signal designs integrate digital and analog circuits which complicates the already difficult verification problem. This paper presents a model, labeled hybrid Petri nets (LHPNs), that is developed to model this heterogeneous set of components. To support formal verification, this paper presents an efficient zone-based state space exploration algorithm for LHPNs. This algorithm uses a process known as warping which allows zones to describe continuous variables changing at variable rates. Finally, this paper describes the application of this algorithm to analog/mixed-signal circuit examples.

Keywords

Petri nets; electronic engineering computing; formal verification; mixed analogue-digital integrated circuits; LHPN; analog circuit verification; formal verification; labeled hybrid Petri nets; mixed-signal circuit verification; zone-based state space exploration algorithm; Capacitors; Clocks; Data models; Integrated circuit modeling; Petri nets; Space exploration; Upper bound; Analog/mixed-signal circuits; formal methods; hybrid Petri nets;

fLanguage

English

Journal_Title

Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on

Publisher

ieee

ISSN

0278-0070

Type

jour

DOI

10.1109/TCAD.2010.2097450

Filename

5737853