AMULET1: SPECIFICATION AND VERIFICATION IN CCS

Abstract

There has been a dramatic resurgence of asynchronous hardware designs in recent years. Since state spaces multiply, asynchronous systems can be extremely state rich and it is correspondingly difficult to reason about their characteristic properties with the traditional techniques of simulation. The alternative, adopted here, is to use formal techniques of specification and property checking to reason about asynchronous designs and to test them thoroughly for desired behaviours. This dissertation explores the feasibility of applying the CCS process algebra and its supporting tool, the Edinburgh Concurrency Workbench (CWB), to the formal specification and verification of a specific asynchronous microprocessor (AMULET1) developed by the AMULET group at Manchester University. AMULET1 is modeled at both the system level and the floor plan level. The system level model shows how each instruction class flows through the major components of the processor, and can be used outwards in modeling embedded applications and inwards to document the roles of the floor plan elements. The subsystem level modeling presents register transfer level detail of the floor plan elements and serves as an implementation guide to designers. This is the first attempt to apply formal techniques to a full scale, practical, industrial-strength asynchronous design. CCS is demonstrated to be an appropriate and efficient notation for modeling such complex designs. In the main, property checking on the CWB proved to be a reliable and robust way of detecting and repairing specification flaws. Although this work is \fIpost facto\fR, it suggests that the systematic incorporation of formal specification and verification techniques into the design cycle could shorten the overall design window and help reduce fabrication iterations.