Specification and Verification II

Lecturer: Mike Gordon
Taken by: Part II
Number of lectures: 12 (Note: there will be no lecture on Wednesday March 3, 2010)
Lecture location: Lecture Theatre 2, WGB
Lecture times: 12:00 on Mon, Wed & Thu starting Fri Feb 12, 2010

Summary: Hoare Logic and hardware. Describing hardware directly in higher order logic. Theory of words (bitstrings). Representing behaviour with predicates. Combinational and sequential behaviour. Simple CMOS examples. Edge-triggered D-type register. Verification of adder and multiplier circuits. Discussion of various transistor models. Temporal abstraction. Transition systems. Modelling with BDDs. Disjunctive partitioning (early quantification). Expressing properties in temporal logics (CTL, LTL, ITL, PSL/Sugar). Model checking. Assertion based verification (ABV). Hoare logic applied to HDL verification. Event, trace and cycle semantics of a simple Verilog-like HDL.
(Official syllabus)

Material is examinable if it is presented in lectures!
Past exam questions (warning: old questions may contain material not examinable in the current course)

Course notes [ps | ps.gz | pdf ]
These notes contain general and background material for the course. Some of the material in them may not be covered in the lectures, and some additional detail and examples are only presented in the lectures. The online notes may change, and so differ from the printed version.

Slides [A4 pdf (4 slides per page)] (warning: slides for lectures not yet given might change or be omitted)

Hoare Logic for hardware
[ A3 postscript for projection | A4x4 postscript for printing | A4x4 pdf for printing]
Introduction to hardware verification using higher order logic (slides from T. Melham and M. Norrish)
[ A4 postscript for projection | A4x4 postscript for printing | A4x4 pdf for printing]
Specification and verification of adders and multipliers
[ A3 postscript for projection | A4x4 postscript for printing | A4x4 pdf for printing]
Dtype and parity checker examples, temporal abstraction, transistor models. Introduction to property checking, reachability and CTL
[ A3 postscript for projection | A4x4 postscript for printing | A4x4 pdf for printing]
Model checking CTL. Other temporal logics: LTL, CTL*, ITL. Industrial assertion languages: PSL/Sugar
[ A3 postscript for projection | A4x4 postscript for printing | A4x4 pdf for printing]
Details of PSL. Comparing static and dynamic semantic models.
[ A3 postscript for projection | A4x4 postscript for printing | A4x4 pdf for printing]

Exercises: the two sets of exercises below cover approximately the first and second halves of the course.