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.
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
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
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
approximately the first and second halves of the course.