This seminar is being organised jointly with the SLI (Systems Level Integration) seminar series.

Abstract

I shall first give a general account of the ways in which formal methods were (and were not!) used in a large-scale microprocessor development project at SGS-Thomson. This will be followed by an account of the formal verification of its internal bus system. This was specified in temporal logic, but its implementation was too complex to be verified directly by model checking. Instead, "abstract views" of the system, from the point of view of one or two bus users, were constructed. Automated model checking was used to verify that these views were indeed abstractions of the implementation, in a certain precise sense; and proof was used to deduce that the system met its temporal logic specification.