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.