Lecture 01 Fri Apr 25 Lecture 02 Mon Apr 28 Lecture 03 Wed Apr 30 Lecture 04 Thu May 01 Lecture 05 Fri May 02 Lecture 06 Mon May 05 Lecture 07 Wed May 07 Lecture 08 Fri May 09 Lecture 09 Mon May 12 Lecture 10 Tue May 13 Lecture 11 Wed May 14 Lecture 12 Fri May 16
Prerequisites: Specification and Verification I
Syllabus: Hoare Logic and hardware. Theory of words (bitstrings). Describing hardware directly in higher order logic. Representing behaviour with predicates. Combinational and sequential behaviour. Simple CMOS examples. Edge-triggered D-type register. Verification of adder and multiplier circuits. Comparison with HDL verification. Discussion of various transistor models. Temporal abstraction. Transition systems. Modelling with BDDs. Disjunctive partitioning (early quantification). Expressing properties in temporal logics (CTL, LTL, ITL, Sugar/PSL). Model checking. Event, trace and cycle semantics of a simple Verilog-like HDL.
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.
The examinable material is what is actually covered in the lectures.
Online slides:
(warning: slides for lectures not yet given might change)
Exercises: the two sets of exercises below cover approximately the first and second halves of the course.
Examples classes: examples classes will be run by Joe Hurd in FW11 at the following times:Monday 19 May between 2-4pm Monday 26 May between 2-4pmIn the second class Joe will also provide revision support for Specification and Verification 1.