AMULET1: SPECIFICATION AND VERIFICATION IN CCS

Simple item page
dc.contributor.authorLiu, Yingeng
dc.date.accessioned2008-05-20T23:31:47Z
dc.date.available2008-05-20T23:31:47Z
dc.date.computerscience1999-05-27eng
dc.date.issued1995-09-01eng
dc.description.abstractThere 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.eng
dc.description.notesWe are currently acquiring citations for the work deposited into this collection. We recognize the distribution rights of this item may have been assigned to another entity, other than the author(s) of the work.If you can provide the citation for this work or you think you own the distribution rights to this work please contact the Institutional Repository Administrator at digitize@ucalgary.caeng
dc.identifier.department1995-573-25eng
dc.identifier.doihttp://dx.doi.org/10.11575/PRISM/31270
dc.identifier.urihttp://hdl.handle.net/1880/46560
dc.language.isoEngeng
dc.publisher.corporateUniversity of Calgaryeng
dc.publisher.facultyScienceeng
dc.subjectComputer Scienceeng
dc.titleAMULET1: SPECIFICATION AND VERIFICATION IN CCSeng
dc.typeunknown
thesis.degree.disciplineComputer Scienceeng
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
1995-573-25.pdf
Size:
14.11 MB
Format:
Adobe Portable Document Format
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.86 KB
Format:
Plain Text
Description:
Download
Collections
Science Research & Publications