Institutionernas doktorandkurser

Startdatum och periodicitet för kurser kan variera. Se detaljer för respektive kurs för aktuell information. För anmälan, kontakta respektive kursansvarig. 

Formell verifiering av hårdvara: var, när och hur?

  • Kurskod: FDAT105
  • ECTS-poäng: 7,5
  • Institution: DATA- OCH INFORMATIONSTEKNIK
  • Forskarskola: Data- och informationsteknik
  • Startdatum: 2017-03-20
  • Slutdatum: 2017-05-26
  • Periodicitet: Ej återkommande.
  • Undervisningsspråk: Kursen kommer att ges på engelska
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.
Litteratur
Conference and journal articles made available on line.
Föreläsare
Carl Seger
Mer information

Sidansvarig Publicerad: on 10 feb 2021.