TY - JOUR
T1 - Advanced methods for equivalence checking of analog circuits with strong nonlinearities
AU - Steinhorst, Sebastian
AU - Hedrich, Lars
N1 - Funding Information:
This work was partly developed within the project VeronA (project label 01 M 3079) which is funded within the Research Program ICT 2020 by the German Federal Ministry of Education and Research (BMBF).
PY - 2010/6
Y1 - 2010/6
N2 - In this contribution two extensions for an analog equivalence checking method are proposed, enabling the checking of strongly nonlinear circuits with floating nodes such as digital library cells. Therefore, a structural recognition and mapping of eigenvalues, representing the dynamics, to circuit elements via circuit variables is presented. Additionally, the introduction of reachability analysis is significantly restricting the investigated state space to the relevant parts, avoiding false negatives. The newly introduced methods are compared to existing ones by application to industrial examples.
AB - In this contribution two extensions for an analog equivalence checking method are proposed, enabling the checking of strongly nonlinear circuits with floating nodes such as digital library cells. Therefore, a structural recognition and mapping of eigenvalues, representing the dynamics, to circuit elements via circuit variables is presented. Additionally, the introduction of reachability analysis is significantly restricting the investigated state space to the relevant parts, avoiding false negatives. The newly introduced methods are compared to existing ones by application to industrial examples.
KW - Analog circuits
KW - Equivalence checking
KW - Formal verification
UR - http://www.scopus.com/inward/record.url?scp=77955713997&partnerID=8YFLogxK
U2 - 10.1007/s10703-009-0086-9
DO - 10.1007/s10703-009-0086-9
M3 - Article
AN - SCOPUS:77955713997
SN - 0925-9856
VL - 36
SP - 131
EP - 147
JO - Formal Methods in System Design
JF - Formal Methods in System Design
IS - 2
ER -