Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 1 Sep 1993 15:10:31 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA12566; Wed, 1 Sep 93 06:59:27 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA12562; Wed, 1 Sep 93 06:59:23 -0700 Received: from skua.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 1 Sep 1993 14:57:12 +0100 To: info-hol@dworshak.cs.uidaho.edu Cc: Wai.Wong@cl.cam.ac.uk Subject: Technical Reports Available Date: Wed, 01 Sep 93 14:56:59 +0100 From: Wai Wong Message-Id: <"swan.cl.cam.:268030:930901135728"@cl.cam.ac.uk> A N N O U N C E M E N T Technical Reports Available ============================= University of Cambridge Computer Laboratory Technical report No. 300 TITLE: Formal Verification of VIPER's ALU ABSTRACT: This research report describes the formal verification of an arithmetic logic unit of the VIPER microprocessor. VIPER is one of the first processors designed using formal methods. A formal model in HOL has been created which models the ALU at two levels: on the higher level, the ALU is specified as a function taking two 32-bit operands and returning a result; on the lower level, the ALU is implemented by a number of 4-bit slices which should takes the same operands and returns the same result. The ALU is capable of performing thirteen different operations. A formal proof of functional equivalence of these two levels has been completed successfully. The complete HOL text of the ALU formal model and details of the proof procedures are included in this report. It has demonstrated that the HOL system is powerful and efficient enough to perform formal verification of realistic hardware design. University of Cambridge Computer Laboratory Technical report No. 306 TITLE: Recording HOL Proofs ABSTRACT: This paper describes a text file format for recording HOL proofs. It is intended to become an interface between HOL and proof checkers. Modification to HOL88 has been carried out to incorporate a proof recorder to generate a proof file in this format. The usage of this new feature is explained by a simple example. A more substantial proof has been recorded, and benchmark data is presented here. The above technical reports are now available 1) in Postscript files by anonymous ftp from ftp.cl.cam.ac.uk [128.232.0.56] in directory "hvg/papers" with file names "WW_report_300.ps.gz" and "WW_report_306.ps.gz"; or 2) in hardcopy from Reception, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England. Tel: +44 223 334600. E-mail: Reception@ucs.cam.ac.uk