AMULET1: SPECIFICATION AND VERIFICATION IN CCS
Date
1995-09-01
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
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.
Description
Keywords
Computer Science