Главная
Study mode:
on
1
Intro
2
A Modern Microprocessor
3
And Hard to Get Right
4
Back in 1985...
5
Advance to 2009
6
Back to 1985
7
Symbolic Trajectory Evaluation
8
Combination of Two Good Ideas
9
State Space Abstraction
10
Guard Expressions E
11
Result - Partitioned Abstraction
12
Key Technical Idea - Exploit Symmetry
13
Intel's Forte Tool
14
Forte Methodology
15
Key Drivers of Progress
16
Formal Verification in Practice
17
Problems, problems...
18
Region of Productivity
19
Life in the Region of Innovation
20
Example - SoC Formal Verification
21
Potential Roadblocks
22
Overcoming Roadblocks
23
Forte Data Points
24
Region of Research?
25
Software - A Much Bigger Problem
26
Embedded Software
27
Working Definition
28
Effective Validation of Low-Level Firmware
29
Ongoing Work
Description:
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.

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

Alan Turing Institute
Add to list