Bruce Krogh Professor and Associate Department Head, Department of Electrical and Computer Engineering, Carnegie Mellon
Verification of Analog and Mixed Signal Designs Using Iterative Refinement
Analog and mixed signal circuit designs can be verified formally by over-approximating continuous dynamic elements with a class of linear hybrid systems for which algorithmically sound verification methods are known. The over-approximation error is bounded by identifying the discrete states of the linear hybrid system with the elements of a sufficiently refined partition of the continuous state space, but attempting to bound the error uniformly throughout the state space can make this approach intractable. In many applications, however, highly accurate partitioning is actually required in only a small portion of the state space to verify the properties of interest. These critical regions can be identified by focused forward and backward reachability computations. The procedure is a variant of counterexample-guided abstraction refinement (CEGAR) developed originally for discrete transition systems. The effectiveness of the approach is illustrated by the analysis of an oscillator circuit using the PHAVer hybrid system verification tool. This work was done in collaboration with Rob Rutenbar (CMU) and Goran Frehse (Verimag).