Analog assertion-based verification on partial state space representations using ASL

In this contribution a novel approach to assertion-based analog property verification by considering state space property specification is introduced. In order to apply a formal property specification of complex analog circuit properties to transient simulation waveforms using the Analog Specification Language (ASL), a partial analog state space model is developed to which the simulation waveforms are transferred. In contrast to other approaches operating directly on transient waveforms, on the partial state space model, properties such as periodic behavior, startup times and other complex analog behavior can be systematically specified and automatically verified. Due to the different perspective of state space property specification compared to approaches considering only time signal properties, critical behavior that may be overlooked in time domain signals can be detected in the state space domain. A verification methodology is introduced and a case study on complex properties of a CMOS charge pump shows the feasibility and practicability of the approach for improving the automation of analog verification.