Class meets, Thursdays, 6:30 - 9:30 pm, virtually on zoom (see Canvas for links)
INSTRUCTOR:
Office hours: Fridays 4:00 - 6:00 pm, or by appointment
E-mail:
Teaching Assistant:
Madhumitha Ramachandran
Office hours: Wednesday 4:00 - 6:00
E-mail:
PREREQUISITES:
VLSI Design, some object-oriented programming experience, computer architecture.
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 on verification tools currently used in industry.
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.
The fundamental concepts will be supplemented by examples of industry practice. These will include verification flows in industry, verification testbenches, Universal Verification Methodology (UVM), verifying memories, cache coherency, and semi-formal verification.
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, as well as novel techniques to expose subtle bugs 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. There will be one midterm exam (take-home with a time limit) on March 25. A semester-long 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.
LABORATORY EXERCISES:
Lab 1 - Logic Equivalence Checking (LEC)
LEC is an important part of the front end design verification flow, because synthesis often optimizes the design to meet constraints, and there may be manual changes to the synthesized logic for testability, power and performance. These processes may change the logic inadvertently. The goal of this lab will be to check the logical equivalence between a RTL module and its synthesized version, and remove any logic bugs. Conformal LEC from Cadence will be used for this lab.
Lab 2 - Assertion Based Verification (ABV)
Assertion based verification is a methodology in which designers use assertions to capture specific design intent and, either through simulation, formal verification, or emulation of these assertions, verify that the design correctly implements that intent. In this lab, assertions must be added to a testbench to check for the correct operation of a protocol during simulation of the design. Mentor Questa will be the simulator used for this purpose.
Lab 3 - Universal Verification Methodology (UVM)
Universal Verification Methodology (UVM) is a powerful standardized verification methodology that was architected to be able to verify a wide range of design sizes and design types. In this lab, a UVM testbench will be set up in SystemVerilog for the given design under test (DUT). Using constrained random verification, the design will be tested for functional bugs. Mentor Questa will again be used for this lab.
Lab 4 - Formal Verification
This lab is designed to use a formal verification tool, JasperGold from Cadence, to check specified properties for all possible states of the design. An important takeaway from this lab is the ease with which properties could cause the tool to give vacuous results, take a very long time to complete the analysis, or time out, unless the specified properties are representative of the real design intent. Some recent advances in exposing subtle bugs in a complex design will also be studied.
PROJECT:
Independent study of some aspect of verification, taking into account existing shortcomings of verification technology. Evaluate relevant publications and propose solutions to the problems addressed, or undertake a case study verifying a complex design.
Identify project teams, topic of project: February 18
One-page outline of project, deliverables: March 12
Project presentations in class: May 6
Final project report due: May 14
Date | Topic | Instructor | Labs | HW |
Jan. 21 | 1. Introduction to hardware verification | Jay Bhadra, AMD | ||
2. Industry verification flows | Vivek Vedula, ARM | |||
Jan. 28 | 3. Formal equivalence checking | Shaun Feng, Samsung | Lab. 1 assigned | |
4. Verifying clock domain crossings | Hary Mony, RealIntent | |||
Feb. 4 | 5. Assertion Based Verification | Harry Foster, Siemens | Lab. 1 due | HW 1 assigned |
6. System Verilog assertions | Harry Foster, Siemens | Lab. 2 assigned | ||
Feb. 11 | 7. Symbolic Trajectory evaluation, term rewriting | Shaun Feng, Samsung | HW 1 due | |
8. Machine Learning and AI in verification | Monica Farkash, AMD | |||
Feb. 25 | 9. Verification testbenches | Eric Harris, ARM | ||
10. UVM Basics | Sakar Jain, ARM | |||
Mar. 4 | 11. Finite Automata and Temporal Logic | Shobha Vasudevan, UIUC | Lab. 2 due | |
12. Model Checking | Amit Goel, Apple | Lab. 3 assigned | ||
Mar. 12 | 13. Analog/Mixed-Signal Verification | Mike Warner | ||
14. Use of ATPG algorithms, programmable hardware | Vivek Vedula, ARM | |||
Mar. 25 | 15. Semi-formal verification | Hary Mony, RealIntent | ||
16. Sequential equivalence checking | Shaun Feng, Samsung | |||
Apr. 1 | 17. GPU verification challenges | Zihno Jusufovic, Apple | Lab. 3 due | |
18. QED, Symbolic QED | Sandip Ray, Univ of FL | Lab. 4 assigned | ||
Apr. 8 | 19. Verification Efficiency | Mark Conklin, ARM | ||
Midterm Exam | ||||
Apr. 15 | 20. CPU verification challenges | Anshul Bhargava, Apple | Lab. 4 due | |
21. SoC verification | Harry Foster, Siemens | |||
Apr. 22 | 22. Cache Verification; ML/AI in Verif. | Monica Farkash, UT | ||
23. Security and Safety; Increase tool capacity | Vivek Vedula, ARM | |||
Apr. 29 | 24. Am I ready to be a verification engineer? | Ram Narayan, ARM | ||
25. New directions in verification | Sean Sun, NXP | |||
May 6 | Project Presentations | Jay Bhadra, AMD | ||
Project Presentations | Jay Bhadra, AMD |
GRADES:
Homework 10% Midterm Exam 10% Laboratory Exercises 1 10% Laboratory Exercises 2, 3 & 4 15% (each) Project 25%
Allegations of Scholastic Dishonesty will be dealt with according to the UT Honor Code. Although we encourage you to study together, your designs and examinations you take MUST be your own work. Providing information to another student where prohibited, or obtaining information from another student where prohibited is considered cheating. This includes the exchange of any information during an examination and any part of your design for the laboratory exercises. Allowing another student to read something on your paper during an examination is considered cheating. In fact, leaving information unprotected so it can be compromised by another student is considered cheating. This includes sheets of paper lying about in your dorm room, and computer files that are not properly protected.
The University of Texas at Austin provides, upon request, appropriate academic adjustments for qualified students with disabilities. who may request appropriate academic accommodations from the Division of Diversity and Community Engagement, Services for Students with Disabilities, 471-6259, http://ddce.utexas.edu/disability/accommodations-and-services/
By UT Austin policy, you must notify me of your pending absence at least fourteen days prior to the date of observance of a religious holy day. If you must miss a class, an examination, a work assignment, or a project in order to observe a religious holy day, you will be given an opportunity to complete the missed work within a reasonable time after the absence.
Classroom Evacuation for Students
All occupants of university buildings are required to evacuate a building when a fire alarm and/ or an official announcement is made indicating a potentially dangerous situation within the building.
Familiarize yourself with all exit doors of each classroom and building you may occupy. Remember that the nearest exit door may not be the one you used when entering the building.
If you require assistance in evacuation, inform your instructor in writing during the first week of class.
For evacuation in your classroom or building: