← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/README

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/README
 
1
This directory contains an ACL2 library of register-transfer logic, developed
 
2
at AMD from 1996 to the present in support of the mechanical verification of 
 
3
various components of the AMD microprocessors that were designed during that 
 
4
period, especially their floating-point arithmetic units.
 
5
 
 
6
This library is a work in progress.  Its primary author is David Russinoff.
 
7
Matt Kaufmann and Eric Smith have made significant contributions.  Development
 
8
continues by Russinoff and by Hanbing Liu, who joined AMD in 2006.
 
9
 
 
10
The library's core definitions and lemmas are contained in the subdirectory
 
11
"lib/".  A parallel subdirectory, "support/", contains a superset of these
 
12
events, including all sublemmas that were required for the proofs of the
 
13
library lemmas.  The "support/" directory is organized in such a way to allow
 
14
for the evolution of "lib/".  Read the following section "How to add new
 
15
theorems to lib/" and "support/README" to learn how to "evolve" the "lib/" and
 
16
"support/" directories.  Users should consider that "lib/" is the RTL library,
 
17
and are discouraged from accessing "support/" directly.
 
18
 
 
19
A more powerful (but perhaps more risky) arithmetic library is available in the
 
20
directory "arithmetic/".  To use this library, we recommend including the book
 
21
"arithmetic/top".
 
22
 
 
23
The library contains another subdirectory, "user/".  "user/" contains many good
 
24
rules which we haven't included in "lib/" because we wanted to keep "lib/"
 
25
uncluttered.  The rules in "user/" are more risky than those in "lib/".  Use
 
26
them at your own risk.  
 
27
 
 
28
The books of each directory may be certified by loading the file "cert.lsp" in
 
29
that directory (some of which may be out of date! -- we generally expect people
 
30
to use "make").
 
31
 
 
32
See the comments in lib/top.lisp for information on what each book in lib/
 
33
contains. 
 
34
 
 
35
The library files contain virtually no documentation.  A detailed companion
 
36
document is available online.
 
37
 
 
38
    D.M. Russinoff, A formal theory of register-transfer logic and computer
 
39
    arithmetic, 2006.  
 
40
 
 
41
    http://www.russinoff.com/libman/
 
42
 
 
43
Many of the interesting events are formal versions of definitions and lemmas
 
44
that are stated and proved in the earlier sections of the following papers,
 
45
which document various applications of the library:
 
46
 
 
47
  D.M. Russinoff, A mechanically checked proof of correctness of the AMD-K5
 
48
  floating point square root microcode, Formal Methods in System Design 14, 
 
49
  75-125 (1999).  See
 
50
  http://www.onr.com/user/russ/david/fsqrt.html.
 
51
 
 
52
  D.M. Russinoff, A mechanically checked proof of IEEE compliance of the AMD-K7
 
53
  floating point multiplication, division, and square root instructions,
 
54
  London Mathematical Society Journal of Computation and Mathematics (1), 
 
55
  pp. 148-200, December, 1998.  See
 
56
  http://www.russinoff.com/david/k7-div-sqrt.html.
 
57
 
 
58
  D.M. Russinoff, A case study in formal verification of register-transfer 
 
59
  logic with ACL2: the floating point adder of the AMD Athlon processor,
 
60
  invited paper, FMCAD 2000.  See
 
61
  http://www.russinoff.com/david/fadd.html.
 
62
 
 
63
For a discussion of our pipeline verification methodology:
 
64
 
 
65
  M. Kaufmann and D. M. Russinoff, Verification of Pipeline circuits.  See
 
66
  http://www.russinoff.com/david/pipeline.html.
 
67
 
 
68
=========================================================================
 
69
 
 
70
How to add new theorems to lib/:
 
71
 
 
72
Suppose you want to make changes to books in "lib/"
 
73
 
 
74
We first make changes to the books in "lib/".  We then need to update the
 
75
"support/" directory to make "lib/" recertifiable again.  We also want to
 
76
maintain the "invariants" on the "support/" directory (see support/README).
 
77
 
 
78
The ground rules are
 
79
 
 
80
   (1) Avoid changing any of the existing files in "support/"
 
81
 
 
82
   (2) Create new directories and new books as necessary.
 
83
 
 
84
   (3) Make creative use of local include-book of the existing
 
85
       books to do new proofs.
 
86
 
 
87
   (4) But keep the dependencies between books simple
 
88
 
 
89
 
 
90
Unless the updates to the lib books are really really trivial (adding
 
91
documentation), we recommend the following approach.
 
92
 
 
93
If the updates are simple (say, we only add or remove exported events):
 
94
 
 
95
   We create a new directory of "lib<n>.delta<m+1>", where n and m is the
 
96
   largest index of libN.deltaM style directories in support/.
 
97
 
 
98
   Suwppose the float.lisp in the lib/ is being updated.  We first create a new
 
99
   book, say, float-extra.lisp in lib<n>.delta<m+1>/" directory. The
 
100
   float-extra.lisp will start with a '(include-book "../lib<n>/top")'.  We
 
101
   then do our proofs in the theory of "../libn/top".
 
102
 
 
103
   We update support/top.lisp in such a way that the resulting support/top.lisp
 
104
   contains the exact the same list of events as the "lib/top.lisp".  To
 
105
   maintain this invariant, we often need to include a copy updated
 
106
   "float.lisp" in "support/lib<n>.delta<m+1>/", that incorporates the new
 
107
   results from float-extra.lisp.
 
108
 
 
109
 
 
110
If the updates are difficult (say, either the new lib/ redefines more than a
 
111
few functions and theorems, or we have already accumulated a large number of
 
112
deltas to current support/lib<n>/):
 
113
 
 
114
   In these cases, the list of events from "lib/top.lisp" is quite different
 
115
   from those of "suppport/lib<n>/top.lisp".
 
116
 
 
117
   We create a support/lib<n+1> directory, where the n is largest of existing
 
118
   lib<n> style directories.  We copy lib/* into support/lib<n+1>/.  We copy
 
119
   "support/top.lisp" to support/lib<n+1>/base.lisp. We update include-book
 
120
   forms in those books as necessary.
 
121
 
 
122
   We create a support/lib<n+1>.delta1, and do all our proofs in this directory
 
123
   and these proofs may be done in a theory of "support/lib<n+1>/top".
 
124
 
 
125
   We update support/top.lisp as necessary.
 
126
 
 
127
 
 
128
To see what we mean by "creative use of local include-book", we give the
 
129
following example:
 
130
 
 
131
Suppose we need to update lib/round.lisp by strengthening a theorem foo. 
 
132
 
 
133
Suppose in "support/" that we have "lib1" through "lib8", and "lib8.delta1"
 
134
through "lib8.delta3".
 
135
 
 
136
If none of the lib8.delta<n> contains an updated round.lisp, we can
 
137
 
 
138
   Create a directory lib8.delta4/ 
 
139
 
 
140
   Create the following books.
 
141
 
 
142
    ============================================================
 
143
    ; book lib8.delta4/foo-new.lisp
 
144
 
 
145
    ; Here, prove stronger version of foo; but call it foo-new.
 
146
    ; We may find that the original version of foo is useful, 
 
147
    ; We can do something like. 
 
148
 
 
149
     (local 
 
150
      (encapsulate () 
 
151
         (local (include-book "../lib8/round"))
 
152
         (defthm foo
 
153
                 ....)))   ; extract the original foo theorem. 
 
154
 
 
155
     (defthm foo-new 
 
156
             ...
 
157
             )
 
158
 
 
159
    ============================================================
 
160
    ; book lib8.delta4/round-partial.lisp
 
161
 
 
162
    (local (include-book "../lib8/round"))
 
163
    (local (include-book "foo-new"))
 
164
    <Insert all of round.lisp, except delete foo.>
 
165
 
 
166
    ============================================================
 
167
    ; book lib8.delta4/round.lisp
 
168
 
 
169
    (local (include-book "round-partial"))
 
170
    (local (include-book "foo-new"))
 
171
    <Insert ../lib8/round.lisp, but replace the original foo with foo-new
 
172
     proved in foo-new.lisp, where however we rename foo-new to foo and
 
173
     give the hint :by foo-new.>
 
174
 
 
175
    ============================================================
 
176
    ; book top.lisp 
 
177
     change 
 
178
        (include-book "lib8/round.lisp")
 
179
     into 
 
180
        (include-book "lib8.delta4/round")
 
181
 
 
182
 
 
183
If one of the lib8.delta1-3 contains an updated round.lisp already, and we feel
 
184
that changing foo into the new version may affect other existing lemma, we can
 
185
chose to take a "snapshot" of current lib by creating a "lib9" and make
 
186
modification in the "lib9.delta1" instead.
 
187
 
 
188
   Create a directory lib9/  
 
189
 
 
190
        1) copy current ../lib/* into lib9/
 
191
        2) copy top.lisp into lib9/base.lisp 
 
192
        3) update lib9/* to adjust the pathname in include-book forms. 
 
193
         
 
194
   
 
195
   Create a directory lib9.delta1/  
 
196
  
 
197
    ============================================================
 
198
    ; book lib9.delta1/foo-new.lisp
 
199
 
 
200
    ; Here, prove stronger version of foo; but call it foo-new.
 
201
    ; We may find that the original version of foo is useful, 
 
202
    ; We can do something like. 
 
203
 
 
204
     (local 
 
205
      (encapsulate () 
 
206
         (local (include-book "../lib9/round"))
 
207
         (defthm foo
 
208
                 ....)))   ; extract the original foo theorem. 
 
209
 
 
210
     (defthm foo-new 
 
211
             ...
 
212
             )
 
213
 
 
214
 
 
215
    ============================================================
 
216
    ; book lib9/round-partial.lisp
 
217
 
 
218
    (local (include-book "../lib9/round"))
 
219
    (local (include-book "foo-new"))
 
220
    <Insert all of round.lisp, except delete foo.>
 
221
 
 
222
    ============================================================
 
223
    ; book lib9.delta1/round.lisp
 
224
 
 
225
    (local (include-book "round-partial"))
 
226
    (local (include-book "foo-new"))
 
227
    <Insert ../lib8/round.lisp, but replace the original foo with foo-new
 
228
     proved in foo-new.lisp, where however we rename foo-new to foo and
 
229
     give the hint :by foo-new.>
 
230
 
 
231
    ============================================================
 
232
    ; book top.lisp 
 
233
 
 
234
     change 
 
235
        (include-book "lib9/round")
 
236
     into 
 
237
        (include-book "lib9.delta1/round")
 
238
 
 
239
 
 
240
=========================================================================
 
241
 
 
242
Beginning of Eric's notes for users of the library [This is still a work in
 
243
progress]:
 
244
 
 
245
Personally, I wouldn't include lib/top since it includes lib/arith (which
 
246
contains the old arithmetic rules) and also includes other books you probably
 
247
don't need (e.g., fadd lemmas, maybe brat).  (But maybe including lib/top is
 
248
okay, since I expect the arithmetic rules to at least be somewhat compatible
 
249
with mine.  [At least, lib/arith and arithmetic/top can both be included in one
 
250
session.] But maybe you don't want both, because I may have essentially the
 
251
same rule under a better name, and the duplication may slow down the rewriter
 
252
and be a pain if you have to disable a rule -- since you'd have to disable both
 
253
mine and the one in lib/arith.)
 
254
 
 
255
Of the lib/ books, including your certified model.lisp should include
 
256
lib/rtl
 
257
lib/rtl-arr
 
258
lib/util
 
259
lib/clocks2
 
260
lib/package-defs
 
261
 
 
262
To start doing proofs, I'd include:
 
263
 
 
264
lib/bits - which itself includes lib/rtl
 
265
lib/round - since you'll be reasoning about rounding
 
266
lib/reps - you will be reasoning about floating-point representations, right?
 
267
 
 
268
You'll probably also want lib/basic and lib/float, at least until I can come up
 
269
with a replacement for these books.  But note that arithmetic/ contains many
 
270
more lemmas about the functions mentioned in basic, especially mod, fl, and
 
271
expt.
 
272
 
 
273
You probably don't need lib/fadd.  
 
274
 
 
275
You'll also need an arithmetic book (or books).  The safest course would be to
 
276
include lib/arith.  However, I have lots of arithmetic books that you might
 
277
want to use instead.  (I think my books and lib/arith are compatible [check
 
278
this?], so it's probably safe to include both.)  Actually, many of the rules in
 
279
lib/arith exist in arithmetic/ too.
 
280
 
 
281
The books in arithmetic/ are far from finished, but there is a lot of good
 
282
stuff in there.  There may be looping rules, but there are also powerful rules
 
283
which can save you a lot of hassle.  I should probably spend more time
 
284
separating the safe stuff from the potentially dangerous stuff.
 
285
 
 
286
It might help to read through some of the books in arithmetic/.  For example,
 
287
if you'll be proving a lot of stuff about mod, you should read through
 
288
arithmetic/mod2.lisp?  [I should probably combine mod.lisp and mod2.lisp.
 
289
Mod.lisp contains "Doc's" lemmas, and "mod2.lisp" contains Eric's lemmas.  Once
 
290
I get all of support working with mod2.lisp included, I can combine it with
 
291
mod.lisp.]  For some books, I've pulled out the proofs in to a separate book
 
292
(e.g., expo2-proofs.lisp).
 
293
 
 
294
For a quick overview of the books in arithmetic, see the comments in
 
295
arithmetic/top.lisp.
 
296
 
 
297
Misc notes: Generally, I assign a lemma to a book based on which function the
 
298
lemma is "about".  So if you're missing a fact about bvecp, look in
 
299
support/bvecp.lisp.  Or if you're missing a lemma about mod, look in
 
300
arithmetic/mod.lisp.  Sometimes it's hard to tell which function a lemma is
 
301
"about".  I tend to rely on a rough mental picture of the directed acyclic
 
302
graph created by the definitions of the functions we use.  Thus if FOO calls
 
303
BAR, a lemma about FOO and BAR goes in the FOO book.  Also, I tend to classify
 
304
a lemma as being "about" to most complicated function it mentions. So a lemma
 
305
about mod of a sum, goes in the mod book since mod is more complicated than
 
306
+. (+ is used to define mod!).  Sometimes it's not clear where to put a lemma
 
307
and I create a special book, such as "arithmetic/mod-expt.lisp", which contains
 
308
lemmas mixing mod and expt.
 
309
 
 
310
See also arithmetic/README.
 
311
 
 
312
Examples of two useful greps (modify appropriately):
 
313
 
 
314
Find all mentions of "mod-equal" in .lisp files:
 
315
 
 
316
  grep -i "mod-equal" */*.lisp
 
317
 
 
318
Find all mentions of the rule "mod-equal" in .out files (including all the
 
319
times it was used in proofs):
 
320
 
 
321
  grep -i "mod-equal" */*.out