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

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.