INTRODUCTION TO FORMAL VERIFICATION AND DESIGN OF DIGITAL SYSTEMS.
Marek A. Perkowski, Professor of Electrical Engineering.
Taught at OCATE, Tuesdays and Thursdays, 6:40 - 8:20 p.m. Starts on March 30.
Prerequisities: graduate standing in Electrical Engineering.
This new class is unique because it covers all three approaches to formal
verification used nowadays in both industry and academia:
logic based verification, model checking and automated theorem proving.
We concentrate on a sequence of small examples and demonstrate
various verification systems at work.
Fundamentals of Functional Verification.
(In)famous Intel's bug and how it may have been avoided.
Binary Decision Diagrams and their extensions.
Practical examples of verification of combinational circuits using rule-based and
theorem-proving methods: ALU, multiplier.
Temporal logic and Model checking approach.
Complete Verification of iterative combinational circuit.
Practical examples of verification of sequential controllers with data paths, using rule-based and
theorem-proving methods: Multiplication by counting, Multiplication by addition and shift,
Parallel circuit for calculated delay, Central Data Registration and Processing System,
Machine to sell tickets, a simple controller proposed by students.
Testability versus verification.
Verification using PROLOG language. Verification using decision diagrams. New
approaches based on multi-valued diagrams. Introduction to HOL language.
Comparison of Boyer-Moore and HOL systems.
Current approaches to comphrehensive hardware validation, industrial companies: Synopsys,
Chrysalis, Abstract Hardware Limited.
Industrial success stories of total system verification.
Practical student projects: cache coherence, multiplier, industrial controller.
Students are welcome to bring their own circuits for verification.
Software use: Prolog, Boyer-Moore theorem prover, Higher Order Logic (HOL).
Grading: homeworks, projects, class presentations, no exams.