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)

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