Specifying and property checking the AMULET1 address interface

We describe work completed on the specification and verification of the address interface of AMULET1, an industrial strength asynchronous microprocessor designed, fabricated and tested by Manchester University. AMULET1 is an asynchronous version of ARM, the best selling RISC chip in the 1980's, and now a leading macro-cell. The address interface is a substantial floor plan element, shared by several processes, which acts as a filter into memory for pc-values, memory swap, and single and multiple load/store operations. The specification is at the register transfer level and is sufficiently detailed to detect the known deadlocks in earlier designs and verify that the final version is deadlock free. The specification work was carried out in Milner's Calculus of Communicating Systems (CCS) and property checked using the ConcurrencyWorkbench (CWB). The work described is post facto--it was started after the AMULET1 chip had been sent for fabrication.