Access Restriction

Author Tasiran, S. ♦ Yuan Yu ♦ Batson, B.
Source IEEE Xplore Digital Library
Content type Text
Publisher Institute of Electrical and Electronics Engineers, Inc. (IEEE)
File Format PDF
Copyright Year ©2003
Language English
Subject Domain (in DDC) Technology ♦ Engineering & allied operations
Subject Keyword Formal specifications ♦ Monitoring ♦ Protocols ♦ Hardware ♦ Design methodology ♦ Permission ♦ Formal verification ♦ State-space methods ♦ Microprocessors ♦ Coherence
Abstract We describe a technique for verifying that a hardware design correctly implements a protocol-level format specification. Simulation steps are translated to protocol state transitions using a refinement map and then verified against the specification using a model checker. On the specification state space, the model checker collects coverage information and identifies states violating certain properties. It then generates protocol-level traces to these coverage gaps and error states. This technique was applied to the multiprocessing hardware of the Alpha 21364 microprocessor and the cache coherence protocol. We were able to generate an error trace which exercised a bug in the implementation that had not been discovered before a prototype was built.
Description Author affiliation: Koc Univ., Istanbul, Turkey (Tasiran, S.)
ISBN 1581136889
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research ♦ Reading
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2003-06-02
Publisher Place USA
Rights Holder Association for Computing Machinery, Inc. (ACM)
Size (in Bytes) 750.05 kB
Page Count 6
Starting Page 356
Ending Page 361

Source: IEEE Xplore Digital Library