2IMF20 Hardware Verification

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:

The first one is very practical. That would be my first suggestion. The second one has more theoretical background but is still short and focused. The third one is theoretically oriented. It covers many topics and is therefore quite thick. Its advantage that it contains (almost) everything.

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 !


Pre-requisities

The course will do its best to be self-contained. But, we assume you are familiar with:

If you have a bachelor in Computer Science, you should have most of these pre-requisites.

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.


Practical Assignments

The course has practical assignments. They will appear below when needed.


READER

Below are some lectures notes (content of these chapters is subject to modifications):


Tuesday 24.10.2017

We will discuss solutions to assignment 3 and have a general Q&A session.


Thursday 19.10.2017

** NO LECTURE **


Tuesday 17.10.2017

Below are two examinations. We will do the one of last year. Examination 2015 and Examination 2016


Thursday 12.10.2017

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.


Tuesday 10.10.2017

We will look at the solutions to assignment 2. We will look at the verification of communication fabrics. The slides are here


Thursday 05.10.2017

We will continue with Bounded Model Checking and start with assignment 3.


Tuesday 03.10.2017

Invited lecture by Simon de Groot and Frank Elfrinkfrom Dialog Semiconductors. The slides will be accessible after the lecture.


Thursday 28.09.2017

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:


Tuesday 26.09.2017

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.


Thursday 21.09.2017

*** 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.


Tuesday 19.09.2017

** 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:


Thursday 14.09.2017

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.


Tuesday 12.09.2017

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:


Thursday 07.09.2017

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.


Tuesday 05.09.2017

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.

Location Date Topic
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.