Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 12 Sep 1995 11:05:09 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA145048209;
          Tue, 12 Sep 1995 03:30:09 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA144908184;
          Tue, 12 Sep 1995 03:29:44 -0600
Received: from albatross.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 12 Sep 1995 10:28:57 +0100
Received: by albatross.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA16017;
          Tue, 12 Sep 95 10:28:43 BST
Date: Tue, 12 Sep 95 10:28:43 BST
From: Mike.Gordon@cl.cam.ac.uk
Message-Id: <9509120928.AA16017@albatross.cl.cam.ac.uk>
To: info-hol@leopard.cs.byu.edu
Subject: Simple proof of add/shift multiplication wanted



I am in the process of revising the undergraduate course on hardware
verification that I teach at Cambridge:

   http://www.cl.cam.ac.uk/users/mjcg/Teaching/SpecVer2/SpecVer2.html

I would like to present (on slides and/or blackboard) a simple proof
of the standard algorithm for multiplication by iterated addition and
shifting:

   http://www.cl.cam.ac.uk/users/mjcg/Verilog/LICSTalkSlides/Slide19.ps

My hope was to present a proof of this in an informal Hoare Logic
style, as part of the transition from program verification to
hardware verification. Unfortunately, I have not managed to come up
with an invariant that is simple enough. I was wondering if anyone has
a nice proof of this algorithm they can share with me. I'd also be
interested in hearing from anyone with experience teaching this sort
of stuff and for general advice and/or teaching materials I can
plunder.

Mike Gordon
http://www.cl.cam.ac.uk/users/mjcg/