Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sat, 8 May 1993 16:42:51 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA01793;
          Sat, 8 May 93 08:26:49 -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 AA01788;
          Sat, 8 May 93 08:26:38 -0700
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Sat, 8 May 1993 16:26:18 +0100
To: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Cc: info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk
Subject: Re: Parity example
In-Reply-To: Your message of Fri, 07 May 93 14:10:01 -0400. <9305071810.AA07108@ultrastar.EE.CORNELL.EDU>
Date: Sat, 08 May 93 16:26:13 +0100
From: Tom Melham <Tom.Melham@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:024930:930508152626"@cl.cam.ac.uk>


> Their is an example of a parity circuit I have seen in several papers
> (bibtex entries below).  Can someone tell me what the source of this
> circuit is?

The parity checker circuit appeared (I think, for the first time) in
section 8 of the following paper:

    M. J. C. Gordon,
    `HOL: A Proof Generating System for Higher-Order Logic',
    in VLSI Specification, Verification and Synthesis,
    edited by G. Birtwistle and P. A. Subrahmanyam,
    Kluwer International Series in Engineering and Computer Science
    (Kluwer, 1988), pp. 73--128.

It was later adapted for a stand-alone case-study, distributed with the first
edition of the TUTORIAL volume of the HOL documentation.  This document was
then incorporated into the TUTORIAL proper for the current edition of the
manual.  The curcuit also appears in the C.U.P. book on HOL.

Still, the parity checker has not appeared in as many places as the
multiplier circuit used as the HOL benchmark...

Tom