DIT780 TDA956, LP4, VT2012

Hardware Description and Verification

2012 Schedule

Note: This is a preliminary schedule. Slides may be updated during the course (and this will be clearly marked).
Tudsday
13:15-15:00 in ES51 		Wednesday
10:00-11:45 in ES51 		Friday
10:00-11:45 in ES51
1.
12/3-16/3 		Course Introduction by EA
Course overview
[2012 slides: pdf]

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
[2012 Slides: part 1, part 2] 		by EA
Formal hardware verification: getting started

[2011 Slides: pdf]

Background reading: the paper by Hu and the paper by Seger.
See also Bryant's 1992 paper on links page.

2.
19/3-23/3 		by EA
Specifying circuit properties, I
[2012 Slides I: pdf]

Specifying circuit properties, II
[2012 Slides II: pdf]

No Lecture
 by EA
PSL (continued)
[2012 Slides: pdf]
3.
26/3-30/3 		by EA
Model Checking 1
[2012 Slides: pdf]

Syntax and semantics of CTL* in Haskell

No Lecture
 by EA
Model Checking 2
[2012 Slides: pdf]

A simple model checker in Haskell

Lab Deadline I (Friday March 30, 23:59)

2/4- Easter Holiday
9/4- Re-sit examination days Easter
4.
16/4-20/4 		by EA
Hardware Description in Functional Languages
Lava 1: Introduction
[2012 Slides]

Example file: LavaIntro.hs
See also the Lava Tutorial (PDF)

(Exam I starts at 18:00.)

No Lecture
 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

5.
23/4-27/4 		by EA
Temporal Induction
[2012 Slides: pdf]

Induction paper (SSS00)

Temporal induction + SAT paper

Exam Deadline I (Tuesday April 24, 18:00)

No Lecture
 by EA
Lava 2 [2012 Slides]
Example file: Lava2.hs
file for slightly better VHDL gen.: VhdlNew11.hs
6.
30/4-4/5 		No lecture (May 1st)
 No Lecture
 by EA
Lava 3 [2012 Slides]
Example file2: Lava3.hs, Lava3_mult.hs

7.
7/5-11/5 		Guest lecture by Richard Bramley from ARM

Lab Deadline II (Tuesday May 8, 23:59)

No Lecture
 by EA Lava 4 (relevant to TH exam)
[2012 slides: pdf]
Code: EFile12.hs and DrawPP12.hs

(Exam II starts at 18:00.)

8.
14/5-18/5 		No Lecture
 Guest lecture by Wolfgang Kunz
Formal Verification of Systems-on-Chip – Industrial Practices 		No lecture

Exam Deadline II (Friday May 18, 18:00)

Lecturers:

Additional information:

  • The timeedit schedule also shows the supervised lab sessions on friday mornings. You are also expected to use the labs unsupervised or log in remotely.
[ Home | News | Schedule | Literature | Assignments | Tools | Links | Course ] emax, spring 2012