Welcome to the course pages of 2IMF20 Hardware Verification!
Lectures are every Tue. 13:45--15:00 in LUNA 1.056 and every Thu. 08:45--10:30 in LUNA 1.056.
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.
The course has practical assignments. They will appear below when needed.
Below are some lectures notes (content of these chapters is subject to modifications):
We will discuss solutions to assignment 3 and have a general Q&A session.
** NO LECTURE **
Below are two examinations. We will do the one of last year. Examination 2015 and Examination 2016
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.
We will look at the solutions to assignment 2. We will look at the verification of communication fabrics. The slides are here
We will continue with Bounded Model Checking and start with assignment 3.
Invited lecture by Simon de Groot and Frank Elfrinkfrom Dialog Semiconductors. The slides will be accessible after the lecture.
We did some exercises about LTL. Here are the slides about the Kripke semantics for LTL and CTL: Slides. We then covered symbolic model-checking with BDD's. And started briefly with SAT-based bounded model-checking. Next week, we will continue with this. 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 check progress with the second assignment. We will shortly discuss about "to simulator or not to simuate". We will then cover temporal logics (LTL and CTL). Slides presented during the lecture are here. These slides correspond to Chapter 4 of the reader above.
*** Lecture from 09:45 to 10:30 **** Execptionally, the lecture will only start at 09:45. The session will be used to answer questions about Jasper Gold, SVA, and the second assignment. If needed, we can also take time to answer questions about BDD's.
** Bring your laptops ! ** We will have a quick at look at the solutions to the first assignment. We will then make groups and give logins and passwords for the server. You are required to work in pairs. 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. Depending on time, we will come back to BDD's. Below, you will find some materials about System Verilog Assertions:
We discussed k-induction in more details. We looked at how BDDs are used to perform symbolic reachability. Details over BDD's can also be found in Section 2.1.5 of Chapter 2 above. The slides can be found here.
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 assignment. 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. Finally, we will discuss sequential equivalence checking. The first paper closely relates to the lecture. The other two are providing you with more details about compositional approaches to verification. The slides about SAT are here. 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 presented 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 lik using UNIX-like operating systems and the Verilog Hardware Description Language. The slides presented during the lecture are available here.
Reading assignments Before Thursday September 7th 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.
|LUNA 1.056||05-09-17||Introduction. Slides|
|LUNA 1.056||07-09-17||Representing Boolean expressions and Combinatorial Equivalence. Slides|
|LUNA 1.056||12-09-17||Basic of SAT solving Slides + Reachability and Sequential Equivalence (SEC) Slides|
|LUNA 1.056||14-09-17||Continue SEC and k-induction. BDDs and reachability Slides.|
|LUNA 1.056||19-09-17||Practical session about Jasper and SVA.|
|LUNA 1.056||21-09-17||** from 09:45 to 10:30 ** Practical questions about Jasper, second assignment, and BDD's.|
|LUNA 1.056||26-09-17||Temporal Logics. Slides|
|LUNA 1.056||28-09-17||Continue Temporal Logics. Slides Symbolic and Bounded Model Checking Slides.|
|LUNA 1.056||03-10-17||Guest lecture Dialog Semiconductors.|
|LUNA 1.056||05-10-17||Continue with BMC.|
|LUNA 1.056||10-10-17||Verification of Communication Fabrics. Slides|
|LUNA 1.056||12-10-17||Practical session for assignment 3|
|LUNA 1.056||17-10-17||Previous Examination.|
|LUNA 1.056||19-10-17||No Lecture.|
|LUNA 1.056||24-10-17||Feedback assignment 3 + Q&A.|
|LUNA 1.056||26-10-17||No Lecture.|