Joint Property Specification for Transient Simulation and Formal Verification of Analog Circuits
Konferenz: edaWorkshop 09 - Workshop 2009 - Electronic Design Automation (EDA)
26.05.2009 - 28.05.2009 in Dresden, Germany
Tagungsband: edaWorkshop 09
Seiten: 6Sprache: EnglischTyp: PDFPersönliche VDE-Mitglieder erhalten auf diesen Artikel 10% Rabatt
Steinhorst, Sebastian; Hedrich, Lars (Electronic Design Methodology, Department of Computer Science, University of Frankfurt/Main, Germany)
Verification is considered as a bottleneck in the analog circuit design flow. While formalized property specification and its automated evaluation is common for formal verification approaches, but is not yet available for industrial applications, the established transient circuit characterization is mainly based on manual inspection of simulation waveforms. This paper extends a specification and verification methodology originally developed for state space-based formalmodel checking towards application to conventional transient simulation results. Property specifications written in the Analog Specification Language (ASL) and the corresponding verification algorithms can now be applied to these simulation results by transferring the simulation waveforms to a state space representation. This allows to use the same property specification for formal verification as well as for automated evaluation of transient simulation results. Application to example circuits demonstrates the practicability of the approach.