Equivalence checking of nonlinear analog circuits for hierarchical AMS System Verification

In this contribution a novel formal methodology for equivalence checking of analog circuits is proposed. In order to prove the behavioral equivalence of two circuit implementations such as a transistor netlist and a corresponding behavioral model, guaranteed coverage of the complete reachable state space for each of the two circuits under verification is obtained by an efficient input stimuli generation algorithm. These input stimuli are processed by a conventional circuit simulator to obtain simulation results covering each system's complete dynamic behavior. By automatically comparing the simulation results using specific error measures, the level of equivalence of both systems is determined. Simulation by complete state space-covering input stimuli guarantees the equivalence checking results to be sound for every possible state and input stimulus of the circuits under verification, which allows safe application of analog behavioral models in hierarchical AMS system simulation flows. The application to example circuits shows the feasibility of the approach.