Abstract

We develop a formal verification procedure to check that elastic pipelined processor designs correctly implement their instruction set architecture (ISA) specifications. The notion of correctness we use is based on refinement. Refinement proofs are based on refinement maps, which—in the context of this problem—are functions that map elastic processor states to states of the ISA specification model. Data flow in elastic architectures is complicated by the insertion of any number of buffers in any place in the design, making it hard to construct refinement maps for elastic systems in a systematic manner. We introduce token-aware completion functions, which incorporate a mechanism to track the flow of data in elastic pipelines, as a highly automated and systematic approach to construct refinement maps. We demonstrate the efficiency of the overall verification procedure based on token-aware completion functions using six elastic pipelined processor models based on the DLX architecture.

Document type: Article

Full document

The PDF file did not load properly or your web browser does not support viewing PDF files. Download directly to your device: Download PDF document

Original document

The different versions of the original document can be found in:

http://downloads.hindawi.com/journals/jece/2009/480740.xml,
http://dx.doi.org/10.1155/2009/480740 under the license cc-by
https://doaj.org/toc/1687-6784,
https://doaj.org/toc/1687-6792 under the license http://creativecommons.org/licenses/by/3.0/
http://downloads.hindawi.com/journals/jece/2009/480740.pdf,
https://dblp.uni-trier.de/db/journals/jece/jece2009.html#SrinivasanSK09,
https://academic.microsoft.com/#/detail/2098800299
Back to Top

Document information

Published on 01/01/2009

Volume 2009, 2009
DOI: 10.1155/2009/480740
Licence: Other

Document Score

0

Views 0
Recommendations 0

Share this document

claim authorship

Are you one of the authors of this document?