2IMF20 Hardware Verification

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:

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

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.


READER

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


PREVIOUS EXAMINATIONS

Here are old examinations so that you can practice. Examination 2015 and Examination 2016 and Examination 2017.


Thursday 01.11.2018

No lecture.


Tuesday 30.10.2018

We will have a Q&A sessions. Come with your questions !


Thursday 25.10.2018

No lecture.


Tuesday 23.10.2018

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 .


Thursday 18.10.2018

Practical session to help with the assignment.


Tuesday 16.10.2018

Guest lecture by Martin Barnasconi (NXP) over verification for AMS (Analog Mixed Signals) designs. Slides: see CANVAS.


Thursday 11.10.2018

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 9.10.2018

Guest lecture from Simon de Groot and Frank Elfrink from Dialog Semiconductors. Slides: see CANVAS.


Thursday 04.10.2018

** NO LECTURE **


Tuesday 02.10.2018

We will continue the lecture about Bounded Model Checking.


Thursday 27.09.2018

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:


Tuesday 25.09.2018

We will cover temporal logics (LTL and CTL). Slides are here. These slides correspond to Chapter 4 of the reader above.


Thursday 20.09.2018

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


Tuesday 18.09.2018

** NO LECTURE **.


Thursday 13.09.2018

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.


Tuesday 11.09.2018

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:


Thursday 06.09.2018

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.


Tuesday 04.09.2018

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.