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.