1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
; RTL - A Formal Theory of Register-Transfer Logic and Computer Arithmetic
; Copyright (C) 1995-2013 Advanced Mirco Devices, Inc.
;
; Contact:
; David Russinoff
; 1106 W 9th St., Austin, TX 78703
; http://www.russsinoff.com/
;
; See license file books/rtl/rel9/license.txt.
;
; Author: David M. Russinoff (david@russinoff.com)
(in-package "ACL2")
(set-enforce-redundancy t)
; Optionally, one may wish to consider:
; (include-book "../../../misc/rtl-untranslate")
; to inhibit expansion of macros in proof output.
; We deliberately exclude any *-helpers.lisp books that may appear here.
(include-book "../lib2.delta1/rtl") ;semantics of the basic RTL primitives
(include-book "../lib2.delta1/rtlarr") ;semantics RTL array primitives
(include-book "../lib2/basic") ;properties of basic arithmetic functions: floor, ceiling,
; exponential, and remainder;; Wed Feb 4 16:40:37 2009
;(include-book "../lib1/bits") ;bit vectors
(include-book "../lib2.delta2/bits") ;bit vectors ;; Tue Feb 24 09:33:20 2009
(include-book "../lib2.delta2/log") ;logical operations ;; Tue Feb 24 09:33:47 2009
(include-book "../lib2.delta1/float") ;floating-point numbers
(include-book "../lib2.delta1/reps") ;floating-point formats and representations
(include-book "../lib2.delta1/round") ;floating-point rounding
(include-book "../lib2.delta2/add") ;support for reasoning about floating-point addition
; (leading one prediction and sticky bit computation)
; Users may prefer to replace the (include-book "arith") below with:
; (include-book "../arithmetic/top")
(include-book "../lib2.delta1/mult") ; integerp multiplier
(include-book "../lib2.delta1/arith") ;general arithmetic package
;
; let go Thu Feb 19 09:43:32 2009
(include-book "../lib2.delta1/util") ;misc helpful stuff including a few macros
(include-book "../lib2.delta1/bvecp-raw-helpers")
;; ; better bvecp-raw-helpers.lisp, Fri Jun 29 10:13:32 2007
(include-book "../lib2.delta1/simple-loop-helpers")
(include-book "../lib2/rom-helpers")
(include-book "../lib2.delta1/bvecp-helpers")
(include-book "../lib2.delta1/logn")
(include-book "../lib2.delta3/simplify-model-helpers") ; Tue Feb 8 15:06:05
; 2011. export new lemma.
(include-book "../lib2.delta1/logn2log")
|
