From owner-qed Wed Nov 23 09:09:35 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id JAA20681 for qed-out; Wed, 23 Nov 1994 09:06:10 -0600 Received: from ultrastar.EE.CORNELL.EDU (ULTRASTAR.EE.CORNELL.EDU [128.84.240.36]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id JAA20675 for ; Wed, 23 Nov 1994 09:06:03 -0600 Date: Wed, 23 Nov 94 10:05:46 EST From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser) Received: by ultrastar.EE.CORNELL.EDU (4.1/1.6.10+n-y-Cornell-Electrical-Engineering) id AA21875; Wed, 23 Nov 94 10:05:46 EST Message-Id: <9411231505.AA21875@ultrastar.EE.CORNELL.EDU> To: yodaiken@sphinx.nmt.edu Cc: windley@leopard.cs.byu.edu, qed@mcs.anl.gov, yodaiken@sphinx.nmt.edu, markaa@ultrastar.EE.CORNELL.EDU Subject: Mark Aagaard's work on verifying pipelines Sender: owner-qed@mcs.anl.gov Precedence: bulk I don't think Mark did sufficient justice to his research on pipeline verification. 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