Personal tools
You are here: Home Events Abstract Archives 1998 Model Checking, Abstraction and Proof in a Microprocessor Design Project

Model Checking, Abstraction and Proof in a Microprocessor Design Project

Anthony McIsaac SGS-Thomson Microelectronics 4pm Monday 30 March 1998 Room 2511, JCMB, King's Buildings This seminar is being organised jointly with the SLI (Systems Level Integration) seminar series.

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.

Document Actions