Formal Verification of Asynchronous Hardware

This unfunded project is carried out in cooperation with the Advanced Computing Research Centre, University of South Australia, Adelaide, and with the Department of Computer Science and Software Engineering, The University of Western Australia, Perth.

We have developped an approach to the integrated verification of timing, performance and correctness properties of concurrent systems. We have chosen as the application domain to demonstrate such an approach a subset of asynchronous logic circuits called micropipelines. The advantages of this domain are that it illustrates both practical and interesting concurrency situations where performance and timing are issues. The circuit we analyse is motivated by the implementation of the AMULET2e asynchronous RISC processor, which has demonstrated some significant performance advantages over existing embedded processors including reduce interrupt latency related to low power modes.

In a RISC processor the instruction pipeline is composed of logic stages and latches. Progress through a synchronous pipeline is managed by the clock; once the logic has completed evaluation all the latches are clocked at the same time effectively moving all the instructions to the next pipeline stage simultaneously. In an asynchronous micropipelined processor the evaluation of a pipeline stage is governed by local interactions with its neighbours using a request acknowledge handshaking protocol. Thus it is possible that one stage is evaluating whilst at the same time a stage further on is transferring an instruction to its neighbour. Thus whilst the performance of a synchronous pipeline is governed entirely by the clock rate that can be achieved with a particular logic design the performance of an asynchronous pipeline depends as well on the design of the handshaking controls for each stage. In particular if the asynchronous logic pipeline is to be as fast as the synchronous one it must be possible for all the evaluation of logic stages to overlap as in the synchronous case.

We have introduced our methodology [2,3] an applied it to real micropipeline a four-phase handshake protocols [1] presented by Furber and Day [4]. In our examples the datapath consists of just a sequence of latches without logic stages in betweens. The whole micropipeline can then be seen as a FIFO.