|
| 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)
|