Joint Property Specification for Transient Simulation and Formal Verification of Analog Circuits

Abstract:
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.