Welcome to the course pages of 2IMF20 Hardware Verification!
Lectures are every Tue. 13:30--15:15 in TR VAN TRIER and every Thu. 08:45--10:30 in AUD 13.
Examination is on November 6th from 9:00 to 12:00 in room TBA.
On this website you will find materials like slides, assigments, and pointers to papers. Regarding papers, we will point to the publisher website. The TU/e digital library should give you access to these papers. Let me know if you have troubles downloading any paper.
The teaching materials will consist of lecture notes (short) and slides. Still, I used (at least) the following three books to prepare the lectures:
Note that these books are mentioned to give you pointers. It is absolutely not mandatory to buy them. But, if like me you like books, then having one will not hurt !
The course will do its best to be self-contained. But, we assume you are familiar with:
Relevant bachelor courses tought in Eindhoven would be Logic and Set Theory, Computer Systems, Automata and Process Theory, Data Structures and Algorithms.
At the master level, related courses are Automated Reasoning, System Validation, Algorithms for Model Checking, Process algebra, Program verification techniques, VLSI Programming, Electronic Design Automation, Digital circuit design.
You will here find two preparation exercises. These exercises are meant for you to practice and learn necessary knowledge before tackling the design project (see below). These exercises will not be graded. Solutions will be discussed during lectures.
You will find here the design project:
You fill find here papers describing NoC architectures. If you feel you need to be more challenged in this course, you can select one of these designs instead of the processor described above.
Below are some lectures notes (content of these chapters is subject to modifications):
Here are old examinations so that you can practice. Examination 2015 and Examination 2016 and Examination 2017.
No lecture.
We will have a Q&A sessions. Come with your questions !
No lecture.
Feedback assignment 3, previous examination, Q&A. Below are old examinations. We will do the one from 2017. Examination 2015 and Examination 2016 and Examination 2017 .
Practical session to help with the assignment.
Guest lecture by Martin Barnasconi (NXP) over verification for AMS (Analog Mixed Signals) designs. Slides: see CANVAS.
We will have a pracical session about assignment 3. You will be able to ask questions and get help with Jasper and the small micro-processor.
Guest lecture from Simon de Groot and Frank Elfrink from Dialog Semiconductors. Slides: see CANVAS.
** NO LECTURE **
We will continue the lecture about Bounded Model Checking.
Here are slides about the Kripke semantics for LTL and CTL: Slides. We will then cover symbolic model-checking with BDD's. Next week, we will continue with SAT-based bounded model-checking. The slides about Symbolic and SAT-based bounded model-checking are here. Chapter-5 of the reader above covers these topics.
Reading Assignment Here is the original paper about bounded model checking. The lecture is basically based on this paper:
We will cover temporal logics (LTL and CTL). Slides are here. These slides correspond to Chapter 4 of the reader above.
** Bring your laptops ! ** We will then make groups and give logins and passwords for the server. You are required to work in teams of 2 or 3 students. This is mainly due to the limited number of licenses (20) for Jasper Gold. We will give a short demo about the tool Jasper Gold and System Verilog Assertions. You will then work on the second preparation exercise, namely, a tutorial to Jasper Gold. Below, you will find some materials about System Verilog Assertions:
** NO LECTURE **.
We continued about reachability, SEC, and BDD's. We will have a quick look at the solutions to the first preparation exercise. We also talked about reachability using k-induction and SAT. For more detail about this, please look at section IV of the paper titled "SAT-solving in practice" below.
Reading Assignment Here is a good paper summarizing the use of BDDs in hardware verification, a good definition of the k-induction principle, and a paper summarizing the practice of SAT solving.
We will check how things are going with the first preparation exercise. We will then have a look at the basics of SAT solvers. A description of the SAT algorithm can also be found in Section 2.2. of Chapter 2 above. The slides about SAT are here. Finally, we will discuss sequential equivalence checking and reachability using BDD's. BDD's are detailed in Section 2.1.5 of Chapter 2 above. We provide you with a reference below for the lecture materials. The slides about SEC are here.
Reading assignment Before the next lecture, you should read the following papers:
The second lecture will be about representations for Boolean functions and Combinational Equivalence checking. Slides that I plan to present during the lecture are available here. This lecture will cover Chapter 2 of the reader (see above). We will postpone sections 2.1.5 and 2.2 to another lecture.
Reading assignment The lecture will be based on Chapter 2 of the reader (see above) and the paper. Before or after the lecture, you should read it. It will give your more details about AIGs and their use in CEC, in particular, following the FRAIG approach.
This first lecture will be an introduction to formal verification. We will also do a quick check about the course pre-requisites, and other topics like using UNIX-like operating systems and the Verilog Hardware Description Language. The slides I am planning to present during the lecture are available here.
Reading assignments Before Thursday September 6th you should have read the following papers:
Below you will find the course schedule and the slides used during the lecture. Note that most of the schedule is tentative and might be modified.
| Location | Date | Topic |
| TR VAN TRIER | 04-09-18 | Introduction. Slides |
| AUD 13 | 06-09-18 | Representing Boolean expressions and Combinatorial Equivalence. Slides |
| TR VAN TRIER | 11-09-18 | Basic of SAT solving Slides + Reachability and Sequential Equivalence (SEC) Slides. |
| AUD 13 | 13-09-18 | Continue SEC, BDDs, and k-induction. |
| TR VAN TRIER | 18-09-18 | ** NO LECTURE ** |
| AUD 13 | 20-09-18 | Tutorial about Jasper Gold. Bring your laptop. |
| TR VAN TRIER | 25-09-18 | Temporal Logics. Slides |
| AUD 13 | 27-09-18 | Continue Temporal Logics. Slides Symbolic and Bounded Model Checking Slides. |
| TR VAN TRIER | 02-10-18 | Continue with BMC. |
| AUD 13 | 04-10-18 | ** NO LECTURE ** |
| TR VAN TRIER | 9-10-18 | Guest lecture Dialog Semiconductors. Slides are available on CANVAS. |
| AUD 13 | 11-10-18 | Practical session to help with design project. |
| TR VAN TRIER | 16-10-18 | Guest lecture NXP. Slides are available on CANVAS. |
| AUD 13 | 18-10-18 | Practical session to help with design project. |
| TR VAN TRIER | 23-10-18 | Feedback design project + Look at a previous Examination + Q&A. |
| AUD 13 | 25-10-18 | No lecture. |
| TR VAN TRIER | 30-10-18 | Q&A. Come and ask questions ! |
| AUD 13 | 01-11-18 | No lecture. |