Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <29446-0@swan.cl.cam.ac.uk>; Tue, 21 Jan 1992 18:06:55 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10583; Tue, 21 Jan 92 08:23:16 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from tesla.oracorp.com by ted.cs.uidaho.edu (16.6/1.34) id AA10579; Tue, 21 Jan 92 08:22:56 -0800 Date: Tue, 21 Jan 92 11:24:08 EST From: srivas@com.oracorp.tesla Received: by tesla.oracorp.com (4.1/1.3-ORA Corporation) id AA01556; Tue, 21 Jan 92 11:24:08 EST Message-Id: <9201211624.AA01556@tesla.oracorp.com> To: info-hol@edu.uidaho.cs.ted Subject: re: verification of pipelines >Sender: info-hol-request@ted.cs.uidaho.edu >Date: Fri, 17 Jan 92 21:51:47 -0500 >From: markaa@ultrastar.EE.CORNELL.EDU (Mark D. Aagaard) >To: info-hol@ted.cs.uidaho.edu >Subject: verification of pipelines >I am beginning to look at verifying pipelines in the Nuprl proof >development system. If anyone knows of any previous work >in pipeline verification (in HOL, any other system, or on paper) >I would appreciate it they would send the references to me. If there is >... Formal Verification of a Pipelined Microprocessor Mandayam Srivas and Mark Bickford IEEE Software, September 1990. Describes the verification of a 3-stage instruction pipelined RISC-like microprocessor design described at a register transfer level. The verification was done using a higher-order functional language based verification system called Clio.