|
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 sys tem, the verification proceeded with minimal time and effort.
Because this work is directly associated with the asynchronous processor design technology currently being investigated in the Labs, this report was printed as a courtesy by Sun Microsystems Laboratories.
|
