The Center for Education and Research in Information Assurance and Security (CERIAS)

The Center for Education and Research in
Information Assurance and Security (CERIAS)
Center for Education and Research in Information Assurance and Security

Formal Verification of Counterflow Pipeline Architecture

Author

Paul N. Loewenstein

Entry type

techreport

Abstract

Some properties of the Sproull counterflow pipeline architecture are formally verified using automata theory and higher order logic in the HOL theorem prover. The proof steps are presented. Despite the pipeline being a non-deterministic asynchronous system, the verification proceeded with minimal time and effort. Because this work is directly associated with the asynchronous processor design technology currently being invesigated in the Labs, this report was printed as a courtesy by Sun Microsystems Laboratories.

Date

1996

Address

Mountain View, CA, USA

Key alpha

Loewenstein

Publisher

Sun Microsystems Laboratories

Affiliation

Sun Microsystems Computer Company

Publication Date

1996-00-00

Contents

1 Introduction 2 Motivation 3 Counterflow Pipeline Processor Architecture 4 The Automaton Model 5 Modelling the Pipeline in HOL 6 Proving Properties of the Pipeline 7 Results 8 Conclusion

Copyright

1996

Language

English

Location

A hard-copy of this is in the Papers Cabinet

BibTex-formatted data

To refer to this entry, you may select and copy the text below and paste it into your BibTex document. Note that the text may not contain all macros that BibTex supports.