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

Scott Little, David Walter, Chris Myers, Robert Thacker, Satish Batchu, Tomohiro Yoneda
April 2011
DOI

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.

Type
Journal article
analog/mixed-signal circuits mixed analogue-digital integrated circuits formal verification Integrated circuit modeling analog circuit verification electronic engineering computing formal methods hybrid Petri nets LHPN mixed-signal circuit verification zone-based state space exploration labeled hybrid Petri net model space exploration petri nets capacitor clock data model upper bound
Scott Little
Scott Little
Maxim Integrated, EDA
David Walter
David Walter
Amazon (AWS S3), Senior SDE
Chris Myers
Chris Myers
Department Chair / Professor
Robert Thacker
Robert Thacker
AMD, MTS Silicon Design Engineer
Satish Batchu
Satish Batchu
Apple, Design Verification Engineer

Related