EFFICIENT MODELING AND VERIFICATION OF ANALOG/MIXED-SIGNAL CIRCUITS USING LABELED HYBRID PETRI NETS by Scott R. Little A dissertation submitted to the faculty of The University of Utah in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Computer Science School of Computing The University of Utah December 2008 Copyright (cid:13)c Scott R. Little 2008 All Rights Reserved THE UNIVERSITY OF UTAH GRADUATE SCHOOL SUPERVISORY COMMITTEE APPROVAL of a dissertation submitted by Scott R. Little This dissertation has been read by each member of the following supervisory committee and by majority vote has been found to be satisfactory. Chair: Chris J. Myers Ganesh Gopalakrishnan Priyank Kalla John Regehr Ken Stevens THE UNIVERSITY OF UTAH GRADUATE SCHOOL FINAL READING APPROVAL To the Graduate Council of the University of Utah: I have read the dissertation of Scott R. Little in its final form and have found that (1) its format, citations, and bibliographic style are consistent and acceptable; (2) its illustrative materials including figures, tables, and charts are in place; and (3) the final manuscript is satisfactory to the Supervisory Committee and is ready for submission to The Graduate School. Date Chris J. Myers Chair, Supervisory Committee Approved for the Major Department Martin Berzins Chair/Dean Approved for the Graduate Council David S. Chapman Dean of The Graduate School ABSTRACT Analog circuit design is traditionally done by expert designers in an ad hoc manner heavily dependent on simulation. This methodology has worked successfully for many years,butprocessvariationanddesigncomplexityarepromptingdesignerstoexplorenew techniques. Formal methods are being used successfully to aid in the complex validation problem for digital circuits. This dissertation presents formal methods for analog and mixed-signal (AMS) circuits. This dissertation describes the development of a formal model, labeled hybrid Petri nets (LHPNs),appropriateforthemodelingandverificationofAMScircuits. AnLHPNis a Petri net variant capable of modeling both continuous and discrete quantities. Creating an LHPN model of an AMS circuit by hand is a complicated and error prone exercise that requires expert knowledge. This is unacceptable for practical adoption of the LHPN model and its associated analysis methods. For this reason, this dissertation introduces an automatic LHPN model generation method. The method uses a set of simulation traces and a desired system property to generate an LHPN modeling the behavior of the simulationtraces. ThemodelgeneratorcanalsobeusedtogenerateabstractVerilog-AMS or VHDL-AMS models suitable for use in system-level simulations. FormalverificationofapropertyovertheentirestatespaceofanLHPNmodeliscom- plicatedbytheinfinitestateofthemodel. Forthisreason, theinfinitestatesofthemodel are grouped into potentially finite groups of equivalent states for verification. Difference bound matrices (DBMs), arestrictedformofconvexpolygons, areusedtorepresentthese equivalent classes of infinite states. Reachability analysis using DBMs is very efficient at the cost of exactness. This dissertation presents algorithms for conservative state space analysis and verification of LHPNs. Finally, these methods are demonstrated on several case studies of AMS circuits from both academia and industry. The formal verification methods demonstrate the ability to find bugs missed by standard simulations. The abstract modeling methods show the promise of using automatically generated abstract models by demonstrating up to 40x speedup for some examples. To good light and the landscape... CONTENTS ABSTRACT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iv LIST OF FIGURES . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ix LIST OF TABLES. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xiii LIST OF ALGORITHMS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xiv ACKNOWLEDGEMENTS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xv CHAPTERS 1. INTRODUCTION . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.1 AMS Circuit Design and Verification Methodology . . . . . . . . . . . . . . . . . . 1 1.2 AMS Circuit Modeling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2.1 Linear Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.2.2 Nonlinear Systems. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.3 AMS Circuit Verification. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.3.1 Automated Theorem Proving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.3.2 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.3.3 Equivalence Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.3.4 Lightweight Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.4 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 1.5 Dissertation Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2. LABELED HYBRID PETRI NETS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.1 Motivating Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.2.1 Hybrid Systems Modeling Languages . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.2.2 Automata Based Models. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.2.3 Petri Net Based Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.3 Labeled Hybrid Petri Nets: Syntax. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2.4 Labeled Hybrid Petri Nets: VHDL-AMS Compiler . . . . . . . . . . . . . . . . . . 34 2.5 Labeled Hybrid Petri Nets: Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2.6 LHPN Expansion for Constant Rates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3. ABSTRACT MODEL GENERATION . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 3.1 Motivating Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 3.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 3.3 Abstract Model Generation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 3.3.1 Assigning the Regions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 3.3.2 Calculating the Rates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 3.3.3 Extracting Discrete Multivalued Variables . . . . . . . . . . . . . . . . . . . . . 62 3.3.4 LHPN Generation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 3.3.5 Pseudo-regions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 3.3.6 Writing Normalized LHPN Models. . . . . . . . . . . . . . . . . . . . . . . . . . . 71 3.3.7 Writing VHDL-AMS Models. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 3.3.8 Writing Verilog-AMS Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 3.4 Coverage Metrics. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4. DIFFERENCE BOUND MATRICES . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 4.1 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 4.2 State Representation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 4.3 Difference Bound Matrices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 4.4 Warping DBMs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 4.5 Updating the State Set . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 5. DBM-BASED MODEL CHECKER . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 5.1 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 5.2 Reachability Analysis of LHPNs Using DBMs . . . . . . . . . . . . . . . . . . . . . . 100 5.2.1 Initial State Set Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 5.2.2 Finding Possible Events . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 5.2.3 Updating the State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 5.2.4 Firing a Transition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 5.2.5 Advancing Time . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 5.2.6 Error Trace Generation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 5.3 Reachability Analysis Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 6. RESULTS. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 6.1 Hybrid Systems Examples. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 6.1.1 Water Level Monitor. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 6.1.2 Temperature Controller . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 6.1.3 Billiards Game . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125 6.2 Tunnel Diode Oscillator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 6.3 Switched Capacitor Integrator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 6.4 PLL Phase Detector . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139 6.5 CMOS Ring Oscillator with Feedforward Inverters. . . . . . . . . . . . . . . . . . . 142 7. CONCLUSIONS. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150 7.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150 7.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151 7.2.1 Automated Model Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151 7.2.2 Coverage Metrics for AMS Circuits . . . . . . . . . . . . . . . . . . . . . . . . . . 153 7.2.3 Counter-Example Guided Abstraction-Refinement. . . . . . . . . . . . . . . 153 7.2.4 False Negative Detection. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154 7.2.5 AMS Property Specification Language . . . . . . . . . . . . . . . . . . . . . . . . 154 7.2.6 Assertion Based Verification for AMS Circuits. . . . . . . . . . . . . . . . . . 155 7.2.7 Automatic Stability Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 vii 7.2.8 Embedded Software Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 REFERENCES . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157 viii LIST OF FIGURES 1.1 A block diagram describing the analog design process. . . . . . . . . . . . . . . . . . 4 1.2 A block diagram describing LEMA. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.1 A schematic diagram of a switched capacitor integrator circuit. . . . . . . . . . . 19 2.2 A simulation of the switched capacitor integrator circuit under nominal conditions, an output slew rate of ±20 mV/µs.. . . . . . . . . . . . . . . . . . . . . . . 20 2.3 A simulation of the switched capacitor integrator circuit with an output slew rate of ±22 mV/µs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.4 A simulation of the switched capacitor integrator circuit with an output slew rate of ±18 mV/µs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.5 A random simulation of the switched capacitor integrator circuit with a variable output slew rate. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.6 A worst case simulation of the switched capacitor integrator circuit showing saturation of the op amp. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.7 A behavioral VHDL-AMS description of the switched capacitor integrator circuit. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.8 A behavioral Verilog-AMS of the the switched capacitor integrator circuit. . 26 2.9 A hybrid automata model of the switched capacitor integrator circuit. . . . . 28 2.10 A THPN model of the switched capacitor integrator circuit. . . . . . . . . . . . . 30 2.11 AnLHPNmodeloftheswitchedcapacitorintegratorcircuit. (a)TheLHPN controlling the rate of change for variable V . (b) The LHPN changing out the Boolean signal V . (c) The LHPN checking for saturation. (d) The in initial values for V , its rate of change, and the Boolean signals. . . . . . . . . 33 out 2.12 VHDL-AMS code for the span procedure. . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.13 An example of the piecewise approximation used by LHPN expansion for nonnegative and nonpositive ranges of rates.. . . . . . . . . . . . . . . . . . . . . . . . . 40 2.14 A template for transforming LHPNs where the range of rates are nonnega- tive or nonpositive. (a) Original LHPN. (b) Transformed LHPN. . . . . . . . . 41 2.15 AtemplatefortransformingLHPNswheretherangeofratesisnonpositive. (a) Original LHPN. (b) Transformed LHPN without using absolute value before comparison. (c) Transformed LHPN using a correct transform.. . . . . 41 2.16 An example of the piecewise approximation used by LHPN expansion for ranges of rate that span zero. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43