Huvudbild (750px bred, 340px hög)
Huvudbildens bildtext
Huvudbildens upphovsman
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:
- Introduction to modern hardware design and the verification challenge
- Traditional verification methods with their strength and weaknesses.
- High-level overview of formal verification methods and the history of the field
- Underlying technologies:
- Ordered binary decision diagrams
- SAT solvers
- Model checking
- Symbolic simulation
- Formal equivalence verification
- Reference model verification
- Property verification
- 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.
- Alternative verification methodologies
- Designer driven design exploration
- Integrated design and verification
- Goals of verification:
- Cost of verification and how to pick the approach with highest return-of-investment.
Conference and journal articles made available on line.
|
|