A Journey to the Center of the State Space Formal & Semi-Formal Methods at IBM

Contents

1. A Journey to the Center of the State Space Formal & Semi-Formal Methods at IBM
   
2. Overview
   
3. The Hardware Design Cycle
   
4. The Hardware Design Cycle
   
5. The H/W Development Crisis (1)
   
6. Design Verification - The Traditional Approach
   
7. Paradigm Shift in Industry
   
8. Formal Verification in IBM Tool Strategy
   
9. Tool/Methodology Flow
   
10. Sugar- IBM's Specification Language
    
11. Sugar (cont.)
    
12. SEREs (Sugar Extended Regular Expressions)
    
13. Using SEREs in Sugar
    
14. Example
    
15. Syntactic Sugaring (1)
    
16. Syntactic Sugaring (II)
    
17. Syntactic Sugaring (III)
    
18. Tool Strategy
    
19. Model Checking - Main FV Workhorse
    
20. RuleBase - IBM Model Checker
    
21. Model Checking - Application Areas
    
22. The IBM Model Checker: Algorithmic Components
    
23. The State Space Explosion Challenge
    
24. Model Checking "On-the-Fly"
    
25. Algorithms for "Under-Approximated" Search
    
26. Algorithms for "Over-Approximated" Search
    
27. "Guided Search" Algorithms
    
28. SAT-Based Verification Algorithms
    
29. Algorithms for Model Reductions
    
30. Tool Strategy
    
31. Typical Simulation Testbench
    
32. FoCs Tool Flow
    
33. FOrmal CheckerS ("FoCs")
    
34. Synthesis of FoCs Checkers
    
35. Synthesis of FoCs Checkers (II)
    
36. Extremly Simple Flow
    
37. FoCs Experience
    
38. Tool Strategy
    
39. Design Exploration - Motivation
    
40. "Exploration" is a Facet of Design
    
41. "Exploration" is Not Extra Work
    
42. EXPLORATION vs. VERIFICATION
    
43. Can Existing Verification Technology be Exploited For "Exploration"? (1)
    
44. Can Existing Verification Technology be Exploited For "Exploration"? (2)
    
45. Can Existing Verification Technology be Exploited For "Exploration"? (3)
    
46. Current State of Affairs: Common Practice
    
47. Current State of Affairs: Results
    
48. The Software Analogue
    
49. Path Exploration Extension of Manual Simulation
    
50. PathFinder - a Design Exploration Tool
    
51. PathFinder GUI
    
52. Formal Verification - Capacity Statistics (ASCI Blue, '00)
    
53. Summary