Asynchronous hardware design is attracting renewed research and industrial interest because of its compositional properties and potential for low power consumption (much of today's hardware is battery driven and asynchronous circuits only do work when there is work to do).
AMULET is an (already working) asynchronous version of the ARM micro designed by Steve Furber's team at Manchester University. ARM is now a standard TI cell, used by IBM to control disks, and in the Apple Newton. Its outstanding characteristic is perhaps its very low power consumption (132 MIPS per watt). The medium term expectation is that AMULET will fare even better.
The talk will present work completed on specifying and verifying the major subsystems of AMULET (address interface, register bank, execution pipeline, data interface) in CCS and modal mu respectively at the RTL. CCS does not handle data well, so we concentrated our efforts on the way blocks (a)synchronise. Once the major subsystems were specified they were tested for deadlock and livelock, bus contention, etc. using modal mu.
The work was carried out with Ms Ying Liu (now at BNR) and with the full cooperation of the Manchester AMULET team.