TY - GEN
T1 - Equivalence checking of nonlinear analog circuits for hierarchical AMS system verification
AU - Steinhorst, Sebastian
AU - Hedrich, Lars
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84872196799&partnerID=8YFLogxK
U2 - 10.1109/VLSI-SoC.2012.6379019
DO - 10.1109/VLSI-SoC.2012.6379019
M3 - Conference contribution
AN - SCOPUS:84872196799
SN - 9781467326568
T3 - 20th IFIP/IEEE International Conference on Very Large Scale Integration, VLSI-SoC 2012 - Proceedings
SP - 135
EP - 140
BT - 20th IFIP/IEEE International Conference on Very Large Scale Integration, VLSI-SoC 2012 - Proceedings
T2 - 20th IFIP/IEEE International Conference on Very Large Scale Integration, VLSI-SoC 2012
Y2 - 7 October 2012 through 10 October 2012
ER -