Departments' graduate courses

Course start and periodicity may vary. Please see details for each course for up-to-date information. The courses are managed and administered by the respective departments. For more information about the courses, how to sign up, and other practical issues, please contact the examiner or course contact to be found in the course information.


Formal Verification of Hardware: Why, When, How?

  • Course code: FDAT105
  • Course higher education credits: 7.5
  • Department: COMPUTER SCIENCE AND ENGINEERING
  • Graduate school: Computer Science and Engineering
  • Course start: 2017-03-20
  • Course end: 2017-05-26
  • Course is normally given: Not regular.
  • Language: The course will be given in English
The course consist of one lecture (2 x 45 minutes) per week, 2-3 assignments, and a fairly significant project that can be done individually or in a small team.
Course outline:

  1. Introduction to modern hardware design and the verification challenge
  2. Traditional verification methods with their strength and weaknesses.
  3. High-level overview of formal verification methods and the history of the field
  4. Underlying technologies:
    • Ordered binary decision diagrams
    • SAT solvers
    • Model checking
    • Symbolic simulation
  5. Formal equivalence verification
    • Combinational
    • Sequential
  6. Reference model verification
  7. Property verification
  8. Typical formal verification methodology:
    • Specification creation and maintenance.
    • Initial wiggling of design
    • First formal verification attempts
    • Debugging of failed verification attempts
    • Environment assumption creation
    • Generalization of verification results
    • Invariant properties creation
    • Regression of proofs, or how to make proofs robust to changing designs.
  9. Alternative verification methodologies
    • Designer driven design exploration
    • Integrated design and verification
  10. Goals of verification:
    • Bug hunting
    • Full proofs
  11. Cost of verification and how to pick the approach with highest return-of-investment.
Literature
Conference and journal articles made available on line.
Lecturers
Carl Seger
More information

Published: Tue 22 Aug 2017.