← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/rtl/rel9/README

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel9/README
1
1
This directory contains an ACL2 library of register-transfer logic, developed
2
 
at AMD from 1995 to the present in support of the mechanical verification of 
3
 
various components of the AMD microprocessors that were designed during that 
 
2
at AMD from 1995 to the present in support of the mechanical verification of
 
3
various components of the AMD microprocessors that were designed during that
4
4
period, especially their floating-point arithmetic units.
5
5
 
6
6
This library is a work in progress.  Its primary author is David Russinoff.
7
7
Matt Kaufmann and Eric Smith have made significant contributions.  Development
8
 
continues by Russinoff and assisted by Hanbing Liu.
 
8
continues by Russinoff and is assisted by Hanbing Liu.
9
9
 
10
10
The library's core definitions and lemmas are contained in the subdirectory
11
11
"lib/".  A parallel subdirectory, "support/", contains a superset of these
12
12
events, including all sublemmas that were required for the proofs of the
13
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
 
14
for the evolution of "lib/".  Read the following sections "How to add new
15
15
theorems to lib/" and "support/README" to learn how to "evolve" the "lib/" and
16
16
"support/" directories.  Users should consider that "lib/" is the RTL library,
17
17
and are discouraged from accessing "support/" directly.
22
22
 
23
23
Previous releases (before rel8) of this library contain another subdirectory,
24
24
"user/".  "user/" contains many good rules which we haven't included in "lib/"
25
 
because we wanted to keep "lib/" uncluttered.  We have not update and maintain
26
 
it. We do not include it in this release. 
 
25
because we wanted to keep "lib/" uncluttered.  We have not maintained
 
26
the user directory, and we do not include it in rel9.
27
27
 
28
28
 
29
29
See the comments in lib/top.lisp for information on what each book in lib/
30
 
contains. 
 
30
contains.
31
31
 
32
32
The library files contain virtually no documentation.  A detailed companion
33
33
document is available online as follows, and can also be accessed through
34
34
the documentation topic, RTL, in the acl2+books combined manual.
35
35
 
36
36
    D.M. Russinoff, A formal theory of register-transfer logic and computer
37
 
    arithmetic, 2006.  
 
37
    arithmetic, 2006.
38
38
 
39
39
    http://www.russinoff.com/libman/
40
40
 
43
43
which document various applications of the library:
44
44
 
45
45
  D.M. Russinoff, A mechanically checked proof of correctness of the AMD-K5
46
 
  floating point square root microcode, Formal Methods in System Design 14, 
 
46
  floating point square root microcode, Formal Methods in System Design 14,
47
47
  75-125 (1999).  See
48
48
  http://www.onr.com/user/russ/david/fsqrt.html.
49
49
 
50
50
  D.M. Russinoff, A mechanically checked proof of IEEE compliance of the AMD-K7
51
51
  floating point multiplication, division, and square root instructions,
52
 
  London Mathematical Society Journal of Computation and Mathematics (1), 
 
52
  London Mathematical Society Journal of Computation and Mathematics (1),
53
53
  pp. 148-200, December, 1998.  See
54
54
  http://www.russinoff.com/david/k7-div-sqrt.html.
55
55
 
56
 
  D.M. Russinoff, A case study in formal verification of register-transfer 
 
56
  D.M. Russinoff, A case study in formal verification of register-transfer
57
57
  logic with ACL2: the floating point adder of the AMD Athlon processor,
58
58
  invited paper, FMCAD 2000.  See
59
59
  http://www.russinoff.com/david/fadd.html.
126
126
To see what we mean by "creative use of local include-book", we give the
127
127
following example:
128
128
 
129
 
Suppose we need to update lib/round.lisp by strengthening a theorem foo. 
 
129
Suppose we need to update lib/round.lisp by strengthening a theorem foo.
130
130
 
131
131
Suppose in "support/" that we have "lib1" through "lib8", and "lib8.delta1"
132
132
through "lib8.delta3".
133
133
 
134
134
If none of the lib8.delta<n> contains an updated round.lisp, we can
135
 
 
136
 
   Create a directory lib8.delta4/ 
 
135
 
 
136
   Create a directory lib8.delta4/
137
137
 
138
138
   Create the following books.
139
139
 
141
141
    ; book lib8.delta4/foo-new.lisp
142
142
 
143
143
    ; Here, prove stronger version of foo; but call it foo-new.
144
 
    ; We may find that the original version of foo is useful, 
145
 
    ; We can do something like. 
 
144
    ; We may find that the original version of foo is useful,
 
145
    ; We can do something like.
146
146
 
147
 
     (local 
148
 
      (encapsulate () 
 
147
     (local
 
148
      (encapsulate ()
149
149
         (local (include-book "../lib8/round"))
150
150
         (defthm foo
151
 
                 ....)))   ; extract the original foo theorem. 
152
 
 
153
 
     (defthm foo-new 
 
151
                 ....)))   ; extract the original foo theorem.
 
152
 
 
153
     (defthm foo-new
154
154
             ...
155
155
             )
156
156
 
171
171
     give the hint :by foo-new.>
172
172
 
173
173
    ============================================================
174
 
    ; book top.lisp 
175
 
     change 
 
174
    ; book top.lisp
 
175
     change
176
176
        (include-book "lib8/round.lisp")
177
 
     into 
 
177
     into
178
178
        (include-book "lib8.delta4/round")
179
179
 
180
180
 
181
181
If one of the lib8.delta1-3 contains an updated round.lisp already, and we feel
182
 
that changing foo into the new version may affect other existing lemma, we can
183
 
chose to take a "snapshot" of current lib by creating a "lib9" and make
184
 
modification in the "lib9.delta1" instead.
 
182
that changing foo into the new version may affect other existing lemmas, we can
 
183
choose to take a "snapshot" of current lib by creating a "lib9" and make
 
184
modifications in the "lib9.delta1" instead.
185
185
 
186
 
   Create a directory lib9/  
 
186
   Create a directory lib9/
187
187
 
188
188
        1) copy current ../lib/* into lib9/
189
 
        2) copy top.lisp into lib9/base.lisp 
190
 
        3) update lib9/* to adjust the pathname in include-book forms. 
191
 
         
192
 
   
193
 
   Create a directory lib9.delta1/  
194
 
  
 
189
        2) copy top.lisp into lib9/base.lisp
 
190
        3) update lib9/* to adjust the pathname in include-book forms.
 
191
 
 
192
 
 
193
   Create a directory lib9.delta1/
 
194
 
195
195
    ============================================================
196
196
    ; book lib9.delta1/foo-new.lisp
197
197
 
198
198
    ; Here, prove stronger version of foo; but call it foo-new.
199
 
    ; We may find that the original version of foo is useful, 
200
 
    ; We can do something like. 
 
199
    ; We may find that the original version of foo is useful,
 
200
    ; We can do something like.
201
201
 
202
 
     (local 
203
 
      (encapsulate () 
 
202
     (local
 
203
      (encapsulate ()
204
204
         (local (include-book "../lib9/round"))
205
205
         (defthm foo
206
 
                 ....)))   ; extract the original foo theorem. 
207
 
 
208
 
     (defthm foo-new 
 
206
                 ....)))   ; extract the original foo theorem.
 
207
 
 
208
     (defthm foo-new
209
209
             ...
210
210
             )
211
211
 
227
227
     give the hint :by foo-new.>
228
228
 
229
229
    ============================================================
230
 
    ; book top.lisp 
 
230
    ; book top.lisp
231
231
 
232
 
     change 
 
232
     change
233
233
        (include-book "lib9/round")
234
 
     into 
 
234
     into
235
235
        (include-book "lib9.delta1/round")
236
236
 
237
237
 
238
238
=========================================================================
239
239
 
240
 
Beginning of Eric's notes for users of the library [This is still a work in
241
 
progress]:
 
240
Beginning of Eric Smith's notes for users of the library [This is
 
241
still a work in progress]:
242
242
 
243
243
Personally, I wouldn't include lib/top since it includes lib/arith (which
244
244
contains the old arithmetic rules) and also includes other books you probably
268
268
more lemmas about the functions mentioned in basic, especially mod, fl, and
269
269
expt.
270
270
 
271
 
You probably don't need lib/fadd.  
 
271
You probably don't need lib/fadd.
272
272
 
273
273
You'll also need an arithmetic book (or books).  The safest course would be to
274
274
include lib/arith.  However, I have lots of arithmetic books that you might
286
286
arithmetic/mod2.lisp?  [I should probably combine mod.lisp and mod2.lisp.
287
287
Mod.lisp contains "Doc's" lemmas, and "mod2.lisp" contains Eric's lemmas.  Once
288
288
I get all of support working with mod2.lisp included, I can combine it with
289
 
mod.lisp.]  For some books, I've pulled out the proofs in to a separate book
 
289
mod.lisp.]  For some books, I've pulled out the proofs into a separate book
290
290
(e.g., expo2-proofs.lisp).
291
291
 
292
292
For a quick overview of the books in arithmetic, see the comments in
299
299
"about".  I tend to rely on a rough mental picture of the directed acyclic
300
300
graph created by the definitions of the functions we use.  Thus if FOO calls
301
301
BAR, a lemma about FOO and BAR goes in the FOO book.  Also, I tend to classify
302
 
a lemma as being "about" to most complicated function it mentions. So a lemma
 
302
a lemma as being "about" the most complicated function it mentions.  So a lemma
303
303
about mod of a sum, goes in the mod book since mod is more complicated than
304
 
+. (+ is used to define mod!).  Sometimes it's not clear where to put a lemma
 
304
+. (+ is used to define mod!).  Sometimes it's not clear where to put a lemma,
305
305
and I create a special book, such as "arithmetic/mod-expt.lisp", which contains
306
306
lemmas mixing mod and expt.
307
307