WEDNESDAY February 27, 3:00pm - 4:30pm | Fir
EVENT TYPE: REGULAR SESSION
Erik Seligman - Intel Corp.
Applying formal verification for real-world applications.
|12.1||Connectivity and Beyond|
|We present an innovative workflow to deploy connectivity tools in the chip design. The process start with designers creating connectivity specifications at the full chip and partition level. These specifications are used to generate connectivity checks on the evolving RTL. A weekly formal tool based regression ensures that as chip design evolves, the connectivity remain intact. Furthermore, the workflow also verifies the completeness of the connectivity specification through fault injection verification. Next, we processes these specifications to generate higher level connectivity checks. These high-level specifications are verified using Static tools. A number of bugs were found and fixed.|
|Speaker:||Shahid Ikram - Cavium
|Authors:||Shahid Ikram - Cavium
Joseph DEricco - Marvell Semiconductor, Inc.
Jim Ellis - Marvell Semiconductor, Inc.
Yasmin Farhan - Marvell Semiconductor, Inc.
Tushar Parikh - Synopsys, Inc.
|12.2||Formal Bug Hunting with “River Fishing” Techniques|
|Formal verification has been used successfully to verify today’s SOC designs. Traditional formal verification that starts from time 0 is good for early design verification, but it is inefficient for hunting complex functional bugs. Based on our experience, complex bugs happen when there are multiple interactions of events happening under uncommon scenarios. Our methodology leverage the functional simulation activities and starts formal verification from interesting “fishing spots” in the simulation traces. In this paper, we are going to share the interesting “fishing spots” and explain how formal engine health is used to priori-tize and guide the process.|
|Speaker:||Ping Yeung - Mentor, A Siemens Business
|Authors:||Mark Eslinger - Mentor, A Siemens Business
Ping Yeung - Mentor, A Siemens Business
|12.3||Smart Formal for Scalable Verification|
|Verifying serial designs is a challenge for both simulation and formal verification. The complexity stems from the serialized nature where the state of each packet depends upon the history of all the previous packets. In this paper, we show a smart, scalable formal verification methodology for verifying serial designs. Our smart solution using abstraction and assume-guarantee reasoning finds bugs in multi-packet serial designs with 10 to the power 40,000 states in under 40 minutes, and exhaustively proves bug absence in designs with 10 to the power 7397 states in 35 minutes on a tablet PC with 6 GB memory.|
|Speaker:||Ashish Darbari - Axiomise Ltd.
|Author:||Ashish Darbari - Axiomise Ltd.