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:

EX1.1 (Tarred, gzipped directory can be found here .)
EX1.2 (Tarred, gzipped directory can be found here .)
EX1.1 with derived CFs (Tarred, gzipped directory can be found here .)
EX2.2 (Tarred, gzipped directory can be found here .)
EX3.1 (Tarred, gzipped directory can be found here .)
EX3.2 (Tarred, gzipped directory can be found here .)

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:

The DLX processor specification and proofs can be found here.
The superscalar DLX specification and proofs can be found here.
The details of the DLX processor verified using the hybrid approach can be found here.
The details of the processor with out-of-order execution and its proof can be found here.

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.