Composable specifications for asynchronous systems using UNITY

Using UNITY as a model for asynchronous hardware systems, we give a generic specification of a device that obeys a four phase protocol. The specification is general enough to allow devices with bundled data as well as dual-rail coded ports, and two phase signalling can be seen as a special case. We give a generic implementation of a function cell and show that A. Martin´s Adder cell is an instance. Finally, we prove two composition theorems that allow four phase devices to be combined into larger four phase devices. All stated theorems were checked using a mechanical theorem prover and we give complete definitions for all the concepts used in the generic specification