Welcome To The ECE 5506 Home Page

Verification of Digital Systems

INSTRUCTOR:
Michael Hsiao

Office: Durham 355 Phone: (540) 231-9254 Email: mhsiao@vt.edu
PREREQUISITES:
1. Logic Design
2. Data Structures and Graph Algorithms
3. Discrete Math (undergrad level)
OPTIONAL TEXT:
- Logic Synthesis and Verification Algorithms, Hachtel and Somenzi, Kluwer Academic Publishers
- Advanced Formal Verification Drechsler, Kluwer.
COURSE OBJECTIVES:
To address fundamental issues in design verification for complex, high-performance digital systems.
LECTURE OUTLINE:
1. Intro and Background (2 lectures)
2. Combinational Logic Verification (7 lectures)
  1. 2-level logic verification
  2. Multi-level verification using SAT
  3. Multi-level verification using BDDs
  4. Incremental verification
3. Sequential Logic Verification (7 lectures)
  1. Image and pre-image computation
  2. Projection and reachability analysis
  3. Fixed point computation
  4. Approximate techniques
  5. Incremental techniques
4. Model Checking (5 lectures)
  1. Computational Tree Logic (CTL)
  2. Property checking
  3. Symbolic model checking
  4. Bounded model checking and induction
5. Simulation-Based Verification (5 lectures)
  1. Coverage metrics
  2. Error-oriented verification
  3. Coverage-directed simulation
  4. Symbolic simulation
  5. Software metrics
6. Error Diagnosis (4 lectures)
  1. Static diagnosis
  2. Dynamic diagnosis