CONVENED THURSDAY June 12, 2:00pm - 4:00pm | 207ABC
TOPIC AREA: VERIFICATION AND TEST
SESSION 44
SPECIAL SESSION: Formal Verification: Dude or Dud? Experiences from the Trenches
Chair: Alan Hu - Univ. of British Columbia, Vancouver, British Columbia, Canada
Organizer: Anmol Mathur - Calypto Design Systems, Inc., Santa Clara, CA
Formal verification has held out the promise of reducing the need to simulate billions of vectors through designs by comprehensively verifying properties of the design or equivalence checking a design against a golden model. Several techniques based on formal methods have been deployed for RTL verification and for verification of more abstract system models. These include: (1) Assertion-based verification of RTL
(2) Sequential equivalence checking between RTL and system-level models
(3) Combinational equivalence checking from RTL to gate-level. Combinational equivalence checking is well established in design flows and has eliminated the need for gate-level simulations. However, design teams are still in the process of figuring out how to use assertion-based verification and sequential equivalence checking effectively to get to high quality, bug free RTL quicker. This session will focus on : (1) Real-world experiences in deploying FV-based verification in design teams. What works and what does not? What is the real return on investment to designers and design managers? What methodology needs to be in place to leverage FV-based tools? How can formal methods be put together with simulation-based techniques in a synergistic fashion? (2) Looking forward, what are some of the key lessons from the past and what capabilities are needed in FV tools as well as design flows to fully exploit formal techniques in design verification?
| 44.1 | Strategies for Mainstream Usage of Formal Verification | |
| Speaker: | Raj S. Mitra - Texas Instruments, Inc., Bangalore, India |
|
| Author: | Raj S. Mitra - Texas Instruments, Inc., Bangalore, India |
|
| 44.2 | Pre-RTL Formal Verification: An Intel Experience | |
| Speaker: | Robert Beers - Intel Corp., Hillsboro, OR |
|
| Author: | Robert Beers - Intel Corp., Hillsboro, OR |
|
| 44.3 | Challenges in Using System-level Models for RTL Verification | |
| Speaker: | Kelvin Ng - NVIDIA Corp., Santa Clara, CA |
|
| Author: | Kelvin Ng - NVIDIA Corp., Santa Clara, CA |
|
| 44.4 | Leveraging Sequential Equivalence Checking to Enable System-level to RTL Flows | |
| Speaker: | Nitin Chawla - STMicroelectronics, Greater Noida, India |
|
| Authors: | Pascal Urard - STMicroelectronics, Crolles, France Asma Maalej - STMicroelectronics, Crolles, France Roberto Guizzetti - STMicroelectronics, Crolles, France Nitin Chawla - STMicroelectronics, Greater Noida, India Venkatram Krishnaswamy - Calypto Design Systems, Inc., Santa Clara, CA |
|