Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets

Scott Little, David Walter, Nicholas Seegmiller, Chris Myers, Tomohiro Yoneda
November 2004
DOI

Abstract

Embedded systems are composed of a heterogeneous collection of digital, analog, and mixed-signal hardware components. This paper presents a method for the verification of systems composed of such a variety of components. This method utilizes a new model, timed hybrid Petri nets (THPN), to model these circuits. In particular, this paper describes an efficient, approximate algorithm to find the reachable states of a THPN model. Using this state space, desired properties specified in ACTL are verified. To demonstrate these methodologies, a few hybrid automata benchmarks, a tunnel diode oscillator, and a phase-locked loop are modeled and analyzed using THPNs.

Type
Conference paper
Publication
Automated Technology for Verification and Analysis
Discrete Transition reachability analysis analog circuit reachable state hybrid automaton
Scott Little
Scott Little
Maxim Integrated, EDA
David Walter
David Walter
Amazon (AWS S3), Senior SDE
Chris Myers
Chris Myers
Department Chair / Professor

Related