Scipediacontent: Scipediacontent moved page Draft Content 861426488 to Katti et al 2009a

2021-02-12T13:01:32Z

Scipediacontent moved page Draft Content 861426488 to Katti et al 2009a

Scipediacontent: Created page with " == Abstract == We develop a formal verification procedure to check that elastic pipelined processor designs correctly implement their instruction set architecture (ISA) spec..."

2021-02-12T13:01:29Z

Created page with " == Abstract == We develop a formal verification procedure to check that elastic pipelined processor designs correctly implement their instruction set architecture (ISA) spec..."

New page

== 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 ==
<pdf>Media:Draft_Content_861426488-beopen260-7053-document.pdf</pdf>

== Original document ==

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

* [http://downloads.hindawi.com/journals/jece/2009/480740.pdf http://downloads.hindawi.com/journals/jece/2009/480740.pdf] under the license https://creativecommons.org/licenses/by

* [http://downloads.hindawi.com/journals/jece/2009/480740.pdf http://downloads.hindawi.com/journals/jece/2009/480740.pdf],
: [http://downloads.hindawi.com/journals/jece/2009/480740.xml http://downloads.hindawi.com/journals/jece/2009/480740.xml],
: [http://dx.doi.org/10.1155/2009/480740 http://dx.doi.org/10.1155/2009/480740] under the license cc-by

* [http://dx.doi.org/10.1155/2009/480740 http://dx.doi.org/10.1155/2009/480740],
: [https://doaj.org/toc/1687-6784 https://doaj.org/toc/1687-6784],
: [https://doaj.org/toc/1687-6792 https://doaj.org/toc/1687-6792] under the license http://creativecommons.org/licenses/by/3.0/

* [https://www.hindawi.com/journals/jece/2009/480740 https://www.hindawi.com/journals/jece/2009/480740],
: [http://downloads.hindawi.com/journals/jece/2009/480740.pdf http://downloads.hindawi.com/journals/jece/2009/480740.pdf],
: [https://dblp.uni-trier.de/db/journals/jece/jece2009.html#SrinivasanSK09 https://dblp.uni-trier.de/db/journals/jece/jece2009.html#SrinivasanSK09],
: [https://academic.microsoft.com/#/detail/2098800299 https://academic.microsoft.com/#/detail/2098800299]

← Older revision	Revision as of 13:01, 12 February 2021
(No difference)

Katti et al 2009a - Revision history

Scipediacontent: Scipediacontent moved page Draft Content 861426488 to Katti et al 2009a

Scipediacontent: Created page with " == Abstract == We develop a formal verification procedure to check that elastic pipelined processor designs correctly implement their instruction set architecture (ISA) spec..."