Overview
The main focus of this seminar will be formal hardware verification.
We will discuss methods, tools, and, algorithms, that enable exhaustive functional verification of chip or FPGA designs,
w.r.t. a given specification (either as a property or a golden model of the desired behaviour).
The core components of formal verification are so called formal methods, like SAT, BDDs, or symbolic computer algebra.
The methods that will be subject of this seminar build around these formal methods.
We distinguish between the following main areas of application:
- Combinational equivalence checking (proving equivalence between two circuits without memory)
- Sequential equivalence checking (proving equivalence between two circuits with memory)
- Sequential property checking (proving properties specified in a formal language / temporal logic, for circuits with memory)
It is strongly recommended that students have attended the "Verification of Digital Circuits", because the topics will be based on these foundations.
It is however not mandatory.
Time table
- April 22, 17:15h: Intro meeting: organizational issues, etc.
- April 29, 17:15h: Presentation of Topics.
- May 6, 17:15h: Topic Assignment and "How to give a talk"
- July 1, 17:15h: presentations
- July 8, 17:15h: presentations
- July 15, 17:15h: presentations
- July 22, 17:15h: presentations
Prüfungsleistung / exam
Students will work in groups of two persons.
Students will be assigned advisors with whom they will meet 2-3 (not more, not less) times
and discuss their work.
For the first appointment, students will have their outline ready. For the second, their slides.
The third appointment might be used for rehearsal of open questions.
- one 30 minute talk + 10 minutes of discussion
- slides and backup slides will be submitted to us, their quality will be taken into account.
They will also be distributed to the participants of the seminar as a summary of the topic.
Another option will be to write a separate summary paper instead, but this is not needed
from our side, if the slides and backup slides are ok..
- Participation in the oral discussions following the other presentations will also be taken into account when determining the grade
|
