C.: Application of automated model generation techniques to analog/mixed-signal circuits

Abstract—Abstract models of analog/mixed-signal (AMS) cir-cuits can be used for formal verification and system-level sim-ulation. The difficulty of creating these models precludes their widespread use. This paper presents an automated method to generate abstract models appropriate for system-level simulation and formal verification. This method uses simulation traces and thresholds on the design variables to generate a piecewise-linear representation of the system. This piecewise-linear representation can be converted to a Verilog-AMS model or a Labeled Hybrid Petri Net formal model. Results are presented for the model generation, simulation, and verification of a PLL phase detector circuit. I