Path: neptune!arp.anu.edu.au!reasoning-owner
Posted-Date: Thu, 11 Apr 91 08:15:23 -0800
Message-ID: <9104111515.AA22981@cheetah.cs.uidaho.edu>
Original-To: info-hol<@@ted.cs.uidaho.edu>
Original-Cc: matute@eng.sun.com (Matute)
Subject: Re: bit manipulation 
References: Your message of Thu, 11 Apr 91 01:43:10 -0800.
             <9104110843.AA01763@cilantro.Eng.Sun.COM> 
Date: Thu, 11 Apr 91 08:15:23 -0800
From: windley@cheetah.cs.uidaho.edu (Phil Windley)
Original-Resent-To: reasoning-people
Original-Resent-Reply-To: Phil Windley <windley@cheetah.cs.uidaho.edu>
Newsgroups: anu.reasoning
Distribution: anu
Sender: postmaster@arp.anu.edu.au
Approved: anu.reasoning@arp.anu.edu.au



Matute wrote:
|-------------------*
| Can someone update me on the status of bit manipulation libraries for
| hardware specification.  There are some warnings about "eval"'s
| theoretical soundness.  Is there something that supersedes it?
|-------------------*


I can't comment on the status of the new n-bit word package that Tom Melham
has in the works (perhaps he can),  For some levels of the verification,
namely those above what is commonly called the electronic block model, you
can use an abstract n-bit word package.  This seperates out the
proofs about n-bit words and simplifies the proof considerably.  For more
information, see Jeff Joyce's or my PhD dissertations.  

--phil--