The University of Texas at Austin
Department of Electrical and Computer Engineering

EE 382M-11, Verification of Digital Systems, Spring Semester (Unique number 17270)

INSTRUCTOR:

Dr. Jay Bhadra
Adjunct Associate Professor, Computer Engineering, University of Texas at Austin;
Hardware System Design and Verification WW R&D Manager NXP Semiconductor
Phone: (512) 895-8229
Office hours: by appointment
E-mail:

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)

PREREQUISITES:

You must have: VLSI Design and programing experience.
Will help a great deal if you have: some background in Mathematical logic and Abstract Algebra.

OUTLINE:

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.

PROJECT

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

Tentative Course Outline (subject to change without prior notice)

Date Topic Instructor
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

GRADES:

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 Bulletin, http://www.utexas.edu/student/registrar/catalogs/
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.