(Created page with " == Abstract == We describe a methodology for the formal verification of complex out-of-order pipelines as they may be used as execution units in out-of-order processors. The...")
 
 
(One intermediate revision by the same user not shown)
Line 3: Line 3:
  
 
We describe a methodology for the formal verification of complex out-of-order pipelines as they may be used as execution units in out-of-order processors. The pipelines may process multiple instructions simultaneously, may have branches and cycles in the pipeline structure, may have variable latency, and may reorder instructions internally. The methodology combines model-checking for the verification of the pipeline control, and theorem proving for the verification of the pipeline functionality. In order to combine both techniques, we formally verify that the FairCTL operators defined in ?-calculus match their intended semantics expressed in a form where computation traces are explicit, since this form is better suited for theorem proving. This allows the formally safe translation of model-checked properties of the pipeline control into a theorem-proving friendly form, which is used for the verification of the overall correctness, including the functionality. As an example we prove the correctness of the pipeline of a multiplication/division floating point unit with all the features mentioned above.
 
We describe a methodology for the formal verification of complex out-of-order pipelines as they may be used as execution units in out-of-order processors. The pipelines may process multiple instructions simultaneously, may have branches and cycles in the pipeline structure, may have variable latency, and may reorder instructions internally. The methodology combines model-checking for the verification of the pipeline control, and theorem proving for the verification of the pipeline functionality. In order to combine both techniques, we formally verify that the FairCTL operators defined in ?-calculus match their intended semantics expressed in a form where computation traces are explicit, since this form is better suited for theorem proving. This allows the formally safe translation of model-checked properties of the pipeline control into a theorem-proving friendly form, which is used for the verification of the overall correctness, including the functionality. As an example we prove the correctness of the pipeline of a multiplication/division floating point unit with all the features mentioned above.
 
Document type: Part of book or chapter of book
 
 
== Full document ==
 
<pdf>Media:Draft_Content_888766987-beopen294-3001-document.pdf</pdf>
 
  
  
Line 15: Line 10:
  
 
* [https://link.springer.com/content/pdf/10.1007%2F3-540-45657-0_23.pdf https://link.springer.com/content/pdf/10.1007%2F3-540-45657-0_23.pdf]
 
* [https://link.springer.com/content/pdf/10.1007%2F3-540-45657-0_23.pdf https://link.springer.com/content/pdf/10.1007%2F3-540-45657-0_23.pdf]
 +
 +
* [http://link.springer.com/content/pdf/10.1007/3-540-45657-0_23 http://link.springer.com/content/pdf/10.1007/3-540-45657-0_23],
 +
: [http://dx.doi.org/10.1007/3-540-45657-0_23 http://dx.doi.org/10.1007/3-540-45657-0_23]
 +
 +
* [https://link.springer.com/chapter/10.1007/3-540-45657-0_23 https://link.springer.com/chapter/10.1007/3-540-45657-0_23],
 +
: [http://core.ac.uk/display/24487249 http://core.ac.uk/display/24487249],
 +
: [https://www.scipedia.com/public/Jacobi_2007a https://www.scipedia.com/public/Jacobi_2007a],
 +
: [https://dblp.uni-trier.de/db/conf/cav/cav2002.html#Jacobi02 https://dblp.uni-trier.de/db/conf/cav/cav2002.html#Jacobi02],
 +
: [https://dl.acm.org/citation.cfm?id=734283 https://dl.acm.org/citation.cfm?id=734283],
 +
: [https://www.oocities.org/de/christian_jacobi/publications/cj02_pipe.pdf https://www.oocities.org/de/christian_jacobi/publications/cj02_pipe.pdf],
 +
: [https://rd.springer.com/chapter/10.1007/3-540-45657-0_23 https://rd.springer.com/chapter/10.1007/3-540-45657-0_23],
 +
: [http://busserver.cs.uni-sb.de/publikationen/Ja02.pdf http://busserver.cs.uni-sb.de/publikationen/Ja02.pdf],
 +
: [https://academic.microsoft.com/#/detail/2157202675 https://academic.microsoft.com/#/detail/2157202675]

Latest revision as of 15:06, 21 January 2021

Abstract

We describe a methodology for the formal verification of complex out-of-order pipelines as they may be used as execution units in out-of-order processors. The pipelines may process multiple instructions simultaneously, may have branches and cycles in the pipeline structure, may have variable latency, and may reorder instructions internally. The methodology combines model-checking for the verification of the pipeline control, and theorem proving for the verification of the pipeline functionality. In order to combine both techniques, we formally verify that the FairCTL operators defined in ?-calculus match their intended semantics expressed in a form where computation traces are explicit, since this form is better suited for theorem proving. This allows the formally safe translation of model-checked properties of the pipeline control into a theorem-proving friendly form, which is used for the verification of the overall correctness, including the functionality. As an example we prove the correctness of the pipeline of a multiplication/division floating point unit with all the features mentioned above.


Original document

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

http://dx.doi.org/10.1007/3-540-45657-0_23
http://core.ac.uk/display/24487249,
https://www.scipedia.com/public/Jacobi_2007a,
https://dblp.uni-trier.de/db/conf/cav/cav2002.html#Jacobi02,
https://dl.acm.org/citation.cfm?id=734283,
https://www.oocities.org/de/christian_jacobi/publications/cj02_pipe.pdf,
https://rd.springer.com/chapter/10.1007/3-540-45657-0_23,
http://busserver.cs.uni-sb.de/publikationen/Ja02.pdf,
https://academic.microsoft.com/#/detail/2157202675
Back to Top

Document information

Published on 01/01/2007

Volume 2007, 2007
DOI: 10.1007/3-540-45657-0_23
Licence: CC BY-NC-SA license

Document Score

0

Views 0
Recommendations 0

Share this document

claim authorship

Are you one of the authors of this document?