CONCORDIA UNIVERSITY
Department of Electrical & Computer Engineering
COEN 6551 - Formal Hardware
Verification
Summer 2023
Instructor:
Dr. S. Tahar
- Office: EV016.179
- Phone: 848-2424 ext. 3114
- Email: tahar@ece.concordia.ca
Lectures:
- Time: Mondays & Wednedays -- 16:15-19:00
- Location: FB-S143
Querries: By email to
coen6551@encs.concordia.ca
Office Hours: Mondays & Wednesdays -- 15:00-16:00
Course Objective: Introduction to formal verification of digital hardware
Prerequisites: COEN6501 or COEN6541; familiarity with digital
hardware design, hardware description languages (e.g. VHDL, Verilog), finite automata theory, logic and mathematical
reasoning.
Textbook: T. Kropf: Introduction to Formal Hardware
Verification, Springer Verlag, 1999. (ISBN: 3540654453)
Course Outline:
- System design and verification flow
- Overview of formal verification techniques
- System modeling and BDDs
- Combinational equivalence checking
- Sequential equivalence checking
- Temporal logic and properties specification
- Verification with model checking
- System modeling with predicate logic
- Verification with theorem proving
- Formal verification systems (e.g. VIS, SMV, HOL, PVS, FormalCheck, Formality,
Conformal)
- Verification case studies (e.g. pipelined processors, ATM switches)
Reference Books:
1. W.K. Lam: Hardware Design Verification: Simulation and Formal Method-Based
Approaches. Prentice Hall, 2005. (ISBN: 0131433474)
2. M.R.A Huth and M.D. Ryan: Logic in Computer Science. Modelling and
Reasoning about Systems. Cambridge University Press, 2000. (ISBN: 0521652006/0521656028)
3. C. Baier, J.-P. Katoen: Principles of Model Checking, MIT Press, 2008
(ISBN: 0262026499)
4. T.F. Melham: Higher Order Logic and Hardware Verification,
Cambridge Tracts in Theoretical Computer Science, No 31, Cambridge
University Press, 1993. (ISBN: 052141718X)
Grading Scheme:
- Exam 1: 30% (Wed. May 29 @ 16:15)
- Exam 2: 30% (TBD during Exams's period)
- CAD Project: 40% (groups of 2)
Course Web Page:
http://www.ece.concordia.ca/~tahar/coen6551.html