Specifying and Verifying TK

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.

Bio:
Graham Birtwistle's research interests include asynchronous hardware design, and the design and application of simulation languages. Ever the man to catch the tidal wave of research, his chief claim to fame is that of being the first person to give up object oriented programming (1983).

LS Home page or Talks in 1998/99