Completion Functions Approach


My Ph.D. dissertation "Systematic Verification of Pipelined Microprocessors" in PS format or in PDF format . Gzipped PS version or gzipped PDF version is also available.

The accompanying PVS (Version 2.3, patch level 0) files:
The earlier versions of these examples presented in the different conferences are available below.

Specification and proofs of the example with speculation and exceptions can be found here . Tarred, gzipped directory can be found here .
A version of the paper can be obtained here.
The paper is © Springer-Verlag. See the LNCS series Homepage.

Will be presented at CAV 00 (CAV2k).
Last updated on April 18, 2000.
This section contains the PVS specification and proofs of the example processor implementing Tomasulo's algorithm without a reorder buffer.

A version of the paper can be obtained here.
The paper is © Springer-Verlag. See the LNCS series Homepage.

Will be presented at CHARME 99.
Last updated on June 26, 1999.
This section contains the PVS specification and proofs of the example processor with a reorder buffer.

A version of the paper can be obtained here.
The paper is © Springer-Verlag. See the LNCS series Homepage.

Presented in the Conference on Computer Aided Verification, 1999.
Last updated on March 24, 1999.

This section contains the PVS specification and proofs of three examples:

A version of the paper can be obtained here.
The paper is © Springer-Verlag. See the LNCS series Homepage.

Presented in Conference on Computer Aided Verification, 1998.
Last updated on June 25, 1998.