All microprocessors use a clock. This acts like a pulse within the system, making sure that all parts in the chip advance in unison. Faster systems come from quicker pulses - but today we have reached a crisis point. The time between pulses is now less than the time it takes the signal to travel from one side of the chip to another. So now the clock no longer keeps everybody `in line' and our systems fail. The AMULET group at Manchester University is a large research team funded by the EEC and managed by Professor Furber. We investigate asynchronous (clock-less) systems in which small sections of the chip co-ordinate control with their neighbours with a simple REQUEST - ACKNOWLEDGE protocol. To date the group has produced the worlds' first asynchronous microprocessor, AMULET1, which is a code compatible version of the ARM6 processor.

My P.hD. investigates the rare and fatal behaviour of asynchronous systems called deadlock, which is the electrical equivalent of gridlock. Early tests of the design showed it had the potential to seize without warning! Further tests demonstrated thats these deadlocks originated in obscure chains of REQUEST's which contained loops.

To discover whether AMULET1 is deadlock free involves considering every possible order of events that can happen in the chip. To do this a mathematical model of the chip has been built using Petri nets and its reachability tree (which expresses the possible event orders) generated. This tree is massive. Mathematical manipulations which exploit symmetries in the tree can then be applied to effectively fold the tree into a smaller, but sematically equivalent tree. This thesis is the first example of the practical benefits of these theoretical `folding' techniques.