Aagaard Leeser 2012a - Revision history

Scipediacontent at 12:49, 21 January 2021

2021-01-21T12:49:16Z

Scipediacontent: Scipediacontent moved page Draft Content 846794348 to Aagaard Leeser 2012a

2020-09-29T07:48:24Z

Scipediacontent moved page Draft Content 846794348 to Aagaard Leeser 2012a

Scipediacontent: Created page with " == Abstract == We have developed a formal definition of correctness for pipelines that ensures that transactions terminate and satisfy a functional specification. This defin..."

2020-09-29T07:48:22Z

Created page with " == Abstract == We have developed a formal definition of correctness for pipelines that ensures that transactions terminate and satisfy a functional specification. This defin..."

New page

== Abstract ==

We have developed a formal definition of correctness for pipelines that ensures that transactions terminate and satisfy a functional specification. This definition separates the correctness criteria associated with the pipelining aspects of a design from the functional relationship between input and output transactions. Using this definition, we developed and formally verified a technique that divides the verification of a pipeline into two separate tasks: proving that the pipelining circuitry meets the pipelining correctness criteria and that the datapath and control circuitry meet the functional specification. The first proof is data independent (except for pipelines that use data-dependent control). The second proof is purely combinational: there is no notion of time and each possible input transaction can be dealt with independently. In addition, we have created a framework that structures and simplifies the proof of the pipelining circuitry.

Document type: Part of book or chapter of book

== Full document ==
<pdf>Media:Draft_Content_846794348-beopen5619-2967-document.pdf</pdf>

== Original document ==

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

* [https://link.springer.com/content/pdf/10.1007%2F3-540-59047-1_40.pdf https://link.springer.com/content/pdf/10.1007%2F3-540-59047-1_40.pdf]

* [http://www.springerlink.com/index/pdf/10.1007/3-540-59047-1_40 http://www.springerlink.com/index/pdf/10.1007/3-540-59047-1_40],[http://dx.doi.org/10.1007/3-540-59047-1_40 http://dx.doi.org/10.1007/3-540-59047-1_40]

* [https://link.springer.com/chapter/10.1007/3-540-59047-1_40 https://link.springer.com/chapter/10.1007/3-540-59047-1_40],[https://academic.microsoft.com/#/detail/1493191709 https://academic.microsoft.com/#/detail/1493191709]

@@ Line 3: / Line 3: @@
 We have developed a formal definition of correctness for pipelines that ensures that transactions terminate and satisfy a functional specification. This definition separates the correctness criteria associated with the pipelining aspects of a design from the functional relationship between input and output transactions. Using this definition, we developed and formally verified a technique that divides the verification of a pipeline into two separate tasks: proving that the pipelining circuitry meets the pipelining correctness criteria and that the datapath and control circuitry meet the functional specification. The first proof is data independent (except for pipelines that use data-dependent control). The second proof is purely combinational: there is no notion of time and each possible input transaction can be dealt with independently. In addition, we have created a framework that structures and simplifies the proof of the pipelining circuitry.
@@ Line 16: / Line 11: @@
 * [https://link.springer.com/content/pdf/10.1007%2F3-540-59047-1_40.pdf https://link.springer.com/content/pdf/10.1007%2F3-540-59047-1_40.pdf]
-* [http://www.springerlink.com/index/pdf/10.1007/3-540-59047-1_40 http://www.springerlink.com/index/pdf/10.1007/3-540-59047-1_40],[http://dx.doi.org/10.1007/3-540-59047-1_40 http://dx.doi.org/10.1007/3-540-59047-1_40]
+* [http://link.springer.com/content/pdf/10.1007/3-540-59047-1_40.pdf http://link.springer.com/content/pdf/10.1007/3-540-59047-1_40.pdf],
-* [https://link.springer.com/chapter/10.1007/3-540-59047-1_40 https://link.springer.com/chapter/10.1007/3-540-59047-1_40],[https://academic.microsoft.com/#/detail/1493191709 https://academic.microsoft.com/#/detail/1493191709]
+* [https://link.springer.com/chapter/10.1007/3-540-59047-1_40 https://link.springer.com/chapter/10.1007/3-540-59047-1_40],

← Older revision	Revision as of 07:48, 29 September 2020
(No difference)