Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 4 May 1993 09:43:13 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15974; Tue, 4 May 93 01:33:02 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA15969; Tue, 4 May 93 01:32:50 -0700 Received: from heron.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 4 May 1993 09:32:17 +0100 To: hug93 Cc: info-hol@ted.cs.uidaho.edu, Wai.Wong@cl.cam.ac.uk Subject: Re: HOL Workshop Papers -- Last Call In-Reply-To: Your message of 01 May 93 10:59:00 -0700. <44*hug93@cs.ubc.ca> Date: Tue, 04 May 93 09:32:01 +0100 From: Wai Wong Message-Id: <"swan.cl.cam.:225560:930504083229"@cl.cam.ac.uk> Hi, I sent the submission message followed by the PostScript files about a week ago, but I still have not received any acknownledgement. I assume they have gone astray. I'm sending the PostScript files again. Wai ------------- included message--------- Return-Path: Delivery-Date: Received: from heron.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 23 Apr 1993 09:18:04 +0100 To: hug93@cs.ubc.ca cc: Wai.Wong@cl.cam.ac.uk Subject: Submission Date: Fri, 23 Apr 93 09:17:32 +0100 From: Wai Wong Message-ID: <"swan.cl.cam.:217370:930423081829"@cl.cam.ac.uk> Hi, Carl and Jeff, I am submitting two papers for HUG93. The PostScript files will be in separate messages following this. Below are the titles and abstracts of the papers. TITLE: Modelling Bit Vectors in HOL: the word Library ABSTRACT: The bit vector is one of the fundamental data objects in hardware specification and verification. The modelling of bit vectors is a key to the success of a hardware verification project. This paper describes a pragmatic approach to modelling bit vectors in Higher-order logic and an implementation as a system library in the \HOL\ theorem prover. In this approach, bit vectors are represented using a polymorphic type. Restricted quantifications are used to simulate dependent types to model the sizes of the vectors. The library consists of many theorems asserting the basic properties of the bit vectors and some useful tools for reasoning about them. Simple examples showing the effective use of the library are described. TITLE: Formal Verification of a Bit Slice ALU ABSTRACT: This research report describes the formal verification of an arithmetic logic unit. 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. It has demonstrated that the \HOL\ system is powerful and efficient enough to perform formal verification of realistic hardware design. --------------------------------- Wai Wong ww@cl.cam.ac.uk University of Cambridge Computer laboratory New Museums Site Pembroke Street Cambridge CB2 3QG Tel:+44 223 334688 England =========================================================================