Dr. Jay Bhadra
Class meets Tuesdays and Thursdays 6:30 - 8:00 pm;
Classroom: Engineering Science Building, ENS 126 ( Engineering area map)
Teaching Assistant supported by ARM: Shahrzad Mirkhani TA Office hours: (Tue/Thu 5:30 - 6:30 pm)
You must have: VLSI Design and programing experience.
Will help a great deal if you have: some background in Mathematical logic and Abstract Algebra.
This course will cover the basics of verifying digital systems, from theory to industry practice. Laboratory exercises will deal with applications of the ideas in the lectures and these will be based primarily on commercial verification tools.
The lectures will discuss the basics of verification, starting with logic and include function representations based on binary decision diagrams, as well as satisfiability techniques. This will be followed by a comprehensive overview of assertion-based verification. Key topics then covered include formal methods of checking the equivalence of two designs, new directions in checking the equivalence of combinational and sequential designs, and fundamentals of temporal logic.
With the basic understanding of these fundamental concepts, we will move on to applying them in practise. The practical applications will be based on the Universal Verification Methodology (UVM) being developed in industry for System Verilog interoperability. Testbench architectures and assertion-based verification in the UVM framework will be studied.
The class will also study model checking and its applications to property checking of real designs. Techniques for managing the complexity of verification using compositional techniques and abstractions will also be studied. The ideas will be applied to the verification of pipelined processors. New directions in verification will also be discussed.
Homework problems and laboratory exercises using commercial tools will be assigned to reinforce the concepts discussed in class. In homework assignments some of the theoretical aspects of verification will be practiced, while lab assignments focus more on learning various aspects of verification tools. In the lab assignments we will make use of an ARM core (or parts of it) to exercise concepts such as equivalence checking, assertion-based verification and model checking among other concepts. There will be one midterm exam in class before the Spring Break. A team project, dealing with some aspect of verification, will be required in the class. Teams will present the results of their project to the entire class.
Identify project teams, topic of project: February 6
One-page outline of project, deliverables: March 4
Interim project report: April 4
Final project report, demonstrations and presentations: April 17, 22, 24, 29 and May 1
|Jan. 14 & Jan. 16||1. Introduction to hardware verification||Bhadra|
|Jan. 21 & Jan. 23||2. Logic basics -- Binary Decision Diagrams (BDDs) and Satisfiability (SAT) solvers||Bhadra|
|Jan. 28 & Jan. 30||3. Formal equivalence checking, dealing with complexity, and an industry application||Bhadra|
|Feb. 4||4. Finite automata||Bhadra|
|Feb. 6||5. Temporal Logic||Bhadra|
|Feb. 11||6. Assertion-based verification (ABV)||Harry Foster, Mentor Graphics|
|Feb. 13||7. System Verilog Assertions (SVA)||Harry Foster, Mentor Graphics|
|Feb. 18||8. Term rewriting systems for equivalence checking||Shaun Feng, NVIDIA|
|Feb. 20||9. Model Checking||Bhadra|
|Feb. 25||10. Sequential equivalence checking||Shaun Feng, NVIDIA|
|Feb. 27||11. Abstractions||Bhadra|
|Mar. 4||12. Modeling, Abstracting and Verifying Memories||Bhadra|
|Mar. 6||Midterm Exam||Bhadra|
|Mar. 18||13. Functional Coverage (SystemVerilog LRM section 20)||Bhadra|
|Mar. 20||14. Semi-formal verification||Hari Mony, IBM|
|Mar. 25||15. Introduction to Symbolic Trajectory Evaluation||Bhadra|
|Mar. 27||16. Use of test generation algorithms and programmable hardware||Bhadra|
|Apr. 1||17a. Introduction to Cache Coherency, 17b. Industrial Cache Coherency Verification||Bhadra|
|Apr. 3||18. Introduction to Verification Testbenches||Prashant Naphade, Freescale|
|Apr. 8||19. Introduction to Data Mining applications in verification and analog circuit Verification||Bhadra|
|Apr. 10||20. Applications of Verification||Bhadra|
|Apr. 15||21. Slicing techniques||Vivek Vedula, U. Connecticut|
|Apr. 17||Project Presentations||Bhadra|
|Apr. 22||Project Presentations||Bhadra|
|Apr. 24||Project Presentations||Bhadra|
|Apr. 29||Project Presentations||Bhadra|
|May 1||Project Presentations||Bhadra|
Homework + Lab Exercises 25% Midterm Exam 25% Project 50%
Allegations of Scholastic Dishonesty will be dealt with according to the
procedures outlined in Appendix C, Chapter 11, of the General Information
The University of Texas at Austin provides, upon request, appropriate academic adjustments for qualified students with disabilities. For more information, contact the Office of the Dean of Students at 471-6259, 471-4241 TDD, or the College of Engineering Director of Students with Disabilities, 471-4321.