Specifying and Verifying TK

Graham Birtwistle

(University of Leeds)

The talk will present work nigh completed on designing, specifying and verifying the major subsystems of an AMULET-like micro in CCS. Like AMULET1 our micro is 2-phase, but like StrongARM, we have separate instruction memories, and like AMULET3, a wide arithmetic pipeline for greater parallelism. By following an obvious design discipline, and making use of some old theorems on the register bank (from previous work on AMULET1) and some obvious recent ones on pipelines, we have reduced the state minimisation problem by a handsome factor and the whole model now fits comfortably on the Edinburgh CWB. The pipeline theorems hold for 4-phase too.

The talk will cover the basic architecture, enough on CCS to get you by, and then detail the 3 major system blocks (fetch unit, arithmetic pipeline, and writeback unit) at the RT level, and how instruction colouring was fettled.

The work is being carried out with Matt Morley and Chris Tofts at Leeds University with plenty of help from young Jim Garside at Manchester.
Tuesday 19th January 1999, 15:00
Seminar Room 322
Department of Computer Science