Jacobi 2007a - Revision history

Scipediacontent at 14:06, 21 January 2021

2021-01-21T14:06:07Z

Scipediacontent: Scipediacontent moved page Draft Content 888766987 to Jacobi 2007a

2020-10-14T11:08:03Z

Scipediacontent moved page Draft Content 888766987 to Jacobi 2007a

Scipediacontent: 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..."

2020-10-14T11:08:00Z

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..."

New page

== 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.

Document type: Part of book or chapter of book

== Full document ==
<pdf>Media:Draft_Content_888766987-beopen294-3001-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-45657-0_23.pdf https://link.springer.com/content/pdf/10.1007%2F3-540-45657-0_23.pdf]

← Older revision		Revision as of 14:06, 21 January 2021
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]

← Older revision	Revision as of 11:08, 14 October 2020
(No difference)