Formal Modelling and Verification of an Asynchronous DLX Pipeline

A five stage pipeline of an asynchronous DLX processor is modelled and its control flow is verified. The model is built using an asynchronous pipeline of latches separated by processing logic. We model two versions of this pipeline: one using latch controllers with four-phase semi-decoupled and another using fully-decoupled protocol. All the processing units are modelled as processes in the PROMELA language of the Spin tool. The model is verified in Spin by means of assertions, LTL properties and progress labels. A useful observation obtained from the study is that: although the semi-decoupled protocol has the potential to hold a data item in every latch, in the presence of processing logic, at most alternate stages can execute at a given time. Its implication being, in the case of control and data hazards no pipeline stalls are necessary, in the case of fully decoupled version, all stages could execute valid instructions at the same time. All the models were verified to be free from deadlock