Hardware Description and Verification TDA956, LP4, VT2009

2009 Schedule
Monday
13 - 15
Tuesday
13-15
Thursday
10 - 12
1.
16/3-20/3
Course Introduction in EB
Course overview by TH
[Slides]

Intro. to industrial formal verification using JasperGold by ØK
[Slides: pdf]

in EA by TH
Formal hardware verification (some key ideas)
[Slides: pdf, pdf 2 per page]
Background reading: the paper by Hu and the paper by Seger.
No lecture
2.
23/3-27/3
in EB by TH
Specifying circuit properties, I & II
[Slides I: pdf, pdf 2 per page
[Slides II: pdf, pdf 2 per page]
No lecture in EB by MB
More about PSL, examples, common errors
[Slides: pdf]
3.
30/3- 3/4
in EB by TH
PSL and Temporal Logic
[Slides]

Model Checking 1
[Slides: pdf, pdf 2 per page]

in EA by TH
Model Checking 2
[Slides: pdf, pdf 2 per page]

A simple model checker in Haskell

No lecture
Lab Deadline I (friday April 3, 23:59)
6/4- Easter Holiday
14/4- Re-sit examination days Easter
4.
20/4-24/4
in EB by KC
BMC and temporal induction
[2008 slides: pdf, pdf 2 per page]
Our paper on SAT-solving in practice
No lecture No lecture

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

5.
27/4-1/5
in EB by TH
Hardware Description in Functional Languages
Lava 1: Introduction
[Slides]
Example file: LavaIntro.hs
See also the Lava Tutorial
in EA by TH
Lava 2 [Slides]
Example file: Lava2.hs
no lecture

6.
4/5-8/5
in EB by WK
Formal Verification of Systems-on-Chip - Industrial Practices
[Slides: pdf 2 per page]
in EA by TH
Lava 3 [Slides]
Example file: Lava3.hs
Hawk slides (see John Matthew's publications for more info)
No lecture
7.
11/5-15/5
in EB by TH
Lava 4 (relevant to take home exam)
[Slides]
Example file: Lava4.hs
in EA by SS
Kiwi: Synthesis of FPGA Circuits from Multi-Threaded
[Slides: pptx]
in EB by JS/EA
Obsidian [slides: pdf]
Wired [slides: pdf]
Lab Deadline II (friday May 15, 23:59)
8.
18/5-22/5
in EB
Discussion & exam prep.
No lecture
No lecture

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

Lecturers:

Additional information:


Home | Schedule | Literature | Assignments | Tools | Links | Course Thomas H March 30, 2009