In an earlier message Victor Yodaiken wrote:
>"Verifying" the behavior of a very simplified textbook example that
>omits, for example, the complex timing that makes these things
>tough is still the material of research papers.
>...
>But it is important to note the immense
>gap between a verification of an example pipeline when such issues
>as setup time and interrupts are abstracted out and a
>verification of an actual processor. Does your pipleline allow
>forwarding? Aliasing? Branch predication?
Mark has not verified a specific pipeline. Instead he has defined a
framework for describing pipelines that identifies the proof
obligations required to show that the pipelining behavior is correct.
In addition, he has a proof that shows that you can separately reason
about the pipelined and non-pipelined behavior of the circuit. This
significantly simplifies the proof of pipelines.
His framework handles complex pipelines with structural hazards --
including stalls, out of order execution and loops. It can be applied
to state of the art microprocessor pipelines including the
instruction, integer, and floating point pipelines in the HP 7100, DEC
21064, and Intel Pentium Processor among others. The framework also
handles hierarchical pipelines.
This approach is building infrastructure that will allow others to
verify real pipelined circuits in the future.
The paper on this is available by anonymous ftp from:
tesla.ee.cornell.edu:~ftp/pub/hw-verify/pipes-tpcd94.ps.Z