Shanghai, China


Event Details

MP Associates, Inc.
WEDNESDAY April 17, 14:15 - 15:15 | Ballroom A
Formal & Requirement Driven Verification Methodologies
Roman Wang - Advanced Micro Devices, Inc.
Using formal verification and assertions to strengthen your methodology.

4.1Handling Inconclusive Assertions in Formal with “River Fishing” Techniques
Handling inconclusive assertions in formal verification is one of the significant challenges faced by project teams deploying formal verification on their designs. Traditional formal verification that starts from time 0 is good for early design verification. It can fully verify the functions of a design if all of the associated assertions converge. However, due to the complexity of designs, almost inevi-tably there are inconclusive assertions which occur when the tools are unable to find either proofs or error traces. In this article, we are going to describe a new methodology that will improve the initial state for formal verification. “River fishing” is a good metaphor for our methodology: by identifying good “fishing spots,” we can significantly increase the number of fishes we catch. Instead of using one initial state to start formal verification, we pick out interesting states from functional simulation traces, and start formal verification from those “fishing spots.”
 Speaker: Jin Hou - Mentor, A Siemens Business
 Authors: Ping Yeung - Mentor, A Siemens Business
Jin Hou - Mentor, A Siemens Business
Yuxin You - Mentor, A Siemens Business
4.2How To Close the Design-Verification Gap with a Requirements-Driven Reset Domain Crossing Methodology
Modern System-on-a-Chip (SoC) designs incorporate hundreds of Semiconductor Intellectual Property blocks, resulting in complex reset architectures, with many asynchronous reset domains. These designs enable transmission of data across sequential elements reset by different asynchronous reset domains thereby causing reset domain crossings (RDC) paths. Incorrect reset logic design will cause metastability and will prevent designs to reset to a known good state which makes device power-up unreliable. This paper presents a requirements-driven methodology for the design and verification of RDC paths in real-world SoC designs. This methodology demonstrates the use of requirements specifications for both design and verification. This methodology is a systematic and repeatable solution that includes RDC design requirements specification and verification plan, RDC design and verification, and RDC results progress tracking and completion metrics. The RDC design requirements usage improves the design and verification process and creates a systematic approach for designing and verifying the reset architecture.
 Speaker: Yuxin You - Mentor, A Siemens Business
 Authors: Yuxin You - Mentor, A Siemens Business
Kurt Takara - Mentor, A Siemens Business
Priya Viswanathan - Mentor, A Siemens Business
Chris Kwok - Mentor, A Siemens Business
Islam Ahmed - Mentor, A Siemens Business