Cross-level verification of analog circuits

The verification of electronic circuits and devices is crucial to ensuring correct functionality, thereby preventing unintended, unreliable, and inconsistent behavior. However, established practices for verifying analog circuits struggle to meet the demands of emerging technologies and use cases.
For instance, the increasing integration efforts within the electronics ecosystem necessitates the use of Analog / Mixed Signal (AMS) circuits. These circuits, integrating both analog and digital components, in larger System-on-Chip (SoC) units, require simultaneous co-verification of the analog and digital parts.
Moreover, new use cases for analog circuits are emerging, which require verification tools that can scale with their large designs. Examples include analog computers and analog Matrix-Vector Multipliers (MVMs), which are used to reduce energy consumption in internet of things devices and hardware accelerators for artificial neural networks.

The current standard approach for analog verification, which involves SPICE simulations and manual inspection of the simulation results, is incompatible with advanced verification methods used for digital designs. Furthermore, achieving comprehensive verification coverage through simulation requires extensive and time-consuming analyses, with complete coverage being unachievable due to the infinite range of possible state values in analog circuits.

Cross-level design and verification can be used to address these issues. On the one hand, designs implemented in high-level AMS frameworks, such as SystemC AMS and Verilog-A, can be embedded into SoC virtual prototypes, thereby enabling AMS co-verification. On the other hand, the more abstract representations used in high-level designs allow faster simulations for better verification coverage and enable proof-based formal verification of designs.

However, these advantages come with trade-offs. Abstract models are less accurate than detailed, low-level models such as SPICE models. Furthermore, designers that create these models can make mistakes. Therefore, cross-level equivalence checking methodologies are needed to assess whether the abstract model is equivalent to the low-level model.

This thesis employs high-level verification techniques to formally determine error margins for multilevel MVMs and introduces a range of methodologies for equivalence checking between high-level and low-level analog models.

For the high-level verification of multilevel MVMs, proof-based formal verification is employed to determine the maximum possible error. By leveraging a mathematical high-level description of multilevel MVMs, an efficient algorithm has been developed for this purpose. Furthermore, the method incorporates a tracing feature for error source identification, which enables targeted improvements to the design. To demonstrate the methodology’s efficiency and effectiveness, a timing analysis is performed, and a case study is conducted on a fabricated multilevel MVM. This approach provides a formal verification methodology for multilevel MVMs, thereby paving the way for their adoption in safety-critical applications.

For equivalence checking, a variety of methods are developed, each offering distinct advantages. Initially, a graph-based equivalence-checking method for linear models is introduced, utilizing symbolic manipulation to address the coverage limitations inherent in simulation-based methods.
Subsequently, this approach is extended to introduce a graph-based methodology for equivalence checking of static nonlinear models. In both methodologies, the linear graph modeling technique is utilized in an innovative way to construct signal-flow graphs, while symbolic manipulation is applied to simplify these graphs.

Finally, an optimized methodology for state-space-based equivalence checking of nonlinear circuits is introduced, utilizing a gradient-ascent-based search algorithm. This algorithm systematically explores a shared state space between the models being compared to identify critical states that result in the greatest functional divergence. Several key challenges are addressed, including the mapping of both circuits onto a common state space, the calculation of the gradient, and the exclusion of unreachable states from the analysis. By employing the gradient-ascent-based search, the methodology overcomes the coverage limitations inherent in simulation-based approaches and achieves a speed improvement of up to 468 times compared to traditional grid-based checking methods.

The applicability of the proposed methodologies is demonstrated across a diverse set of examples, from analog computers and multilevel MVMs to conventional analog circuits like filters and amplifiers. These examples are implemented at multiple abstraction levels, including behavioral models, simplified SPICE models, and SPICE models incorporating full BSIM transistor models. Additionally, a series of experiments is conducted to compare the advantages offered by the different equivalence checking approaches and to analyze both the timing performance and scalability of the methodologies.