The pressing need for the verification of analog and mixed-signal (AMS) designs is driven by increased design complexity and the integration of such circuits into SoCs. However, verification of AMS circuits remains a significant challenge. This paper proposes a simulation-assisted formal verification methodology that leverages SMT-based satisfiability techniques to tackle the challenges arising from the inherent analog and/or hybrid nature of AMS systems. Although state-of-the-art SMT solvers, in the worst-case scenario, still have exponential complexity in the number of constraints, the main focus of this paper is to first formally formulate the verification task into an SMT problem, then accelerate the verification by using simulation assistance. To verify the nonlinear dynamics, randomly sampled simulations are first applied to quickly explore the reachable state space, and then a nonlinear SMT solver is invoked to ensure the conservativeness. To achieve optimal efficiency, the tradeoff between the runtime costs of simulation and SMT solving is analyzed by means of a Bayesian inference-based technique that dynamically learns from the simulation history. This paper demonstrates the feasibility and efficacy of the proposed methodology on conservative verification of dynamic properties of nonlinear AMS circuits.

The pressing need for the verification of analog and mixed-signal (AMS) designs is driven by increased design complexity and the integration of such circuits into SoCs. However, verification of AMS circuits remains as a significant challenge. We propose a methodology that leverages SMT-based Satisfiability techniques to tackle the challenges arising from the inherent analog and/or hybrid natures of AMS systems. We demonstrate the feasibility and efficacy of the proposed methodology on conservative verification of dynamic properties of nonlinear AMS circuits.

A novel built-in jitter characterization architecture combining quantization noise shaping and a partial Vernier delay structure is proposed for high resolution jitter measurement. The effective resolution is optimized at the system level as well as the circuit level. Using 90nm CMOS technology, an area of 0.008mm2 is occupied. The power consumption is 1.85mW. An effective resolution of 1.5ps is achieved.

We exploit the reconfigurability of recent all-digital PLL designs to provide novel in-situ output jitter test and diagnosis abilities under multiple parametric variations of key analog building blocks. Digital signatures are collected and processed under specifically designed loop filter configurations to facilitate low-cost high-accuracy performance prediction and diagnosis.