At-Scale Formal Verification for Industrial Semiconductor Designs - Professor Tom Melham

Explore a comprehensive lecture on large-scale formal verification techniques for industrial semiconductor designs. Delve into the evolution of microprocessor complexity and verification methods, from 1985 to modern times. Learn about Symbolic Trajectory Evaluation, state space abstraction, and guard expressions. Discover Intel's Forte tool and methodology, examining key drivers of progress in formal verification. Analyze the challenges and solutions in practical implementation, including the concept of "Region of Productivity" and innovation. Investigate potential roadblocks and strategies to overcome them in SoC formal verification. Consider the broader implications for software verification, particularly in embedded systems and low-level firmware. Gain insights into ongoing research and future directions in this critical field of computer science and engineering.

Intro
A Modern Microprocessor
And Hard to Get Right
Back in 1985...
Advance to 2009
Back to 1985
Symbolic Trajectory Evaluation
Combination of Two Good Ideas
State Space Abstraction
Guard Expressions E
Result - Partitioned Abstraction
Key Technical Idea - Exploit Symmetry
Intel's Forte Tool
Forte Methodology
Key Drivers of Progress
Formal Verification in Practice
Problems, problems...
Region of Productivity
Life in the Region of Innovation
Example - SoC Formal Verification
Potential Roadblocks
Overcoming Roadblocks
Forte Data Points
Region of Research?
Software - A Much Bigger Problem
Embedded Software
Working Definition
Effective Validation of Low-Level Firmware
Ongoing Work