|
| Tudsday
13:15-15:00 in ES51
| Wednesday
10:00-11:45 in ES51
| Friday
10:00-11:45 in ES51
|
1.
21/3-25/3
|
Course Introduction by MS
Course overview
[2011 slides: pdf,
pdf 2 per page]
Discussion with those students who do not already know VHDL
[2011 Slides: pdf
Background reading: the paper by Schubert and
the paper by Paruthi.
|
Intro. to industrial formal verification using JasperGold by MAB
[2011 Slides: pdf]
|
by MS
Formal hardware verification (some key ideas)
(will probably overflow into tues. week 3)
[2011 Slides: pdf]
Background reading: the paper by Hu and
the paper by Seger.
See also Bryant's 1992 paper on links page.
|
2.
28/3-1/4
|
by MS
Specifying circuit properties, I
[2011 Slides I: pdf]
Specifying circuit properties, II
[2011 Slides II: pdf]
|
by MS
PSL (continued)
[2011 Slides: pdf]
|
No Lecture
|
3.
4/4-8/4
|
by MS
Model Checking 1
[2011 Slides: pdf]
|
by MS
Model Checking 2
[2011 Slides: pdf]
A simple model checker in Haskell
|
by KC
Bounded Model Checking and safety properties
[2008 slides: pdf,
pdf 2 per page]
Our paper on SAT-solving in practice
The BMC Journal paper
PSL semantics paper
The MiniSat paper
Lab Deadline I (Friday April 8, 23:59)
|
4.
11/4-15/4
|
No lecture
|
No lecture
|
by MS
Temporal Induction
[2011 Slides: pdf]
Induction paper (SSS00)
Temporal induction + SAT paper
Exam Deadline I (friday April 15, 23:59)
|
| 18/4- |
Easter Holiday |
| 25/4-
| Re-sit examination days Easter
|
5.
2/5-6/5
|
by MS
Hardware Description in Functional Languages
Lava 1: Introduction
[2011 Slides]
Example file: LavaIntro.hs
See also the Lava Tutorial (PDF)
|
by MS
Lava 2 [2011 Slides]
Example file: Lava2.hs
file for slightly better VHDL gen.: VhdlNew11.hs
|
by MS
Lava 3 [2011 Slides]
Example file: Lava3.hs
|
6.
9/5-13/5
|
No lecture
|
by SS
The hardware / software divide
Slides
|
by MS
Lava 4 (relevant to TH exam)
[2011 slides: pdf]
Lab Deadline II (friday May 13, 23:59)
|
7.
16/5-20/5
|
No Lecture
|
No Lecture
|
No lecture
Exam Deadline II (friday May 20, 23:59)
|