Tags:AMS modelling, Formal verification and Metamodel
Abstract:
The complexity of modern-day System-on-Chips (SoCs) is continually increasing, and it becomes evident to deliver dependable and credible chips in a short time-to-market. Especially in the case of test chips, where the aim is to study the feasibility of the design, time is a crucial factor. Pre-silicon functional verification is one of the main contributors that makes up a large portion of the product development cycle. Verification engineers often loosely verify test chips that turn out to be non-functional on the silicon, ultimately resulting in expensive re-spins. To left-shift the verification efforts, formal verification is a powerful methodology that aims to exhaustively verify designs, giving better confidence in the overall quality. This paper focuses on the pragmatic formal verification of a mixed signal Intellectual Property (IP) that has a combination of digital and analog blocks and including the analog behavioral model into the formal verification set-up. Digital and Analog being the complete opposite of each other and still align for a formal verification setup, thus "Analogous Alignments". The Formal setup leverages powerful formal techniques such as Formal Property Verification (FPV), Control/Status Register (CSR) verification and connectivity checks. The properties used for FPV are auto-generated using a metamodeling framework. We also discuss the challenges faced especially related to state-space explosion, non-compatibility of formal with Analog Mixed Signal (AMS) models and techniques to mitigate them such as k-induction. With this verification approach, we were able to exhaustively verify the design within a reasonable time and sufficient coverage. We also reported several bugs at an early stage making the complete design verification process iterative and effective.
Analogous Alignments: Digital "Formally" Meets Analog