Hardware Description and Verification

2010 Schedule

Note: links to slides from previous years may be updated.
Monday
13:15-15:00 in EL41
Tuesday
10:00-11:45 in EL41
Thursday
10:00-11:45 in EL41
1.
15/3-19/3
No lecture Course Introduction
Course overview by TH
[Slides]

Intro. to industrial formal verification using JasperGold by LL
[2009 Slides: pdf]

by EA
Formal hardware verification (some key ideas)
[Slides: pdf, pdf 2 per page]
Background reading: the paper by Hu and the paper by Seger.
2.
22/3-26/3
by TH
Specifying circuit properties, I
[Slides I: pdf, pdf 2 per page

Specifying circuit properties, II
[Slides II: pdf, pdf 2 per page]

by TH
PSL and Temporal Logic
[Slides]

Circuit verification in Jasper Gold (quick demo)

by TH
More about PSL, examples, common errors (from chapter 12-13 in the PSL book)
[Slides: pdf]
29/3- Easter Holiday
5/4- Re-sit examination days Easter
3.
12/4-16/4
by TH
Model Checking 1
[Slides: pdf]
by TH
Model Checking 2
[Slides: pdf, pdf 2 per page]

A simple model checker in Haskell

No lecture
Lab Deadline I (Friday April 16, 23:59)
4.
19/4-23/4
No lecture by KC
Bounded Model Checking and safety properties
[2008 slides: pdf, pdf 2 per page]
by NS
Temporal Induction and SAT solving
[Slides: pdf]

Our paper on SAT-solving in practice

Exam Deadline I (friday April 23, 23:59)

5.
26/4-30/4
by LA
BlueSpec
by TH
Hardware Description in Functional Languages
Lava 1: Introduction
[Slides]
Example file: LavaIntro.hs
See also the Lava Tutorial (PDF)
by WK
Formal Verification of Systems-on-Chip - Industrial Practices
[2009 Slides: pdf 2 per page]
6.
3/5-7/5
by TH
Lava 2 [Slides]
Example file: Lava2.hs
by TH
Lava 3 [Slides]
Example file: Lava3.hs
Hawk slides (see John Matthew's publications for more info)
7.
10/5-14/5
by TH
Lava 4 (relevant to take home exam)
[Slides]
Example file: Lava4.hs
No lecture (Ascension Day)
Lab Deadline II (friday May 14, 23:59)
8.
17/5-21/5
by KPS
Constructing Circuits from Wired Descriptions
[Slides: pdf]
Discussion & exam prep. No lecture

Exam Deadline II (Saturday May 22, 23:59)

Lecturers:

Additional information:

[ Home | News | Schedule | Literature | Assignments | Tools | Links | Course ] TH, March 2010