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
|
----------------------------------------------------------------------
Book Certification
----------------------------------------------------------------------
To certify books, execute the following:
make ACL2=<Path of the ACL2 image>
To remove certificate files, etc., execute the following:
make clean ACL2=<Path of the ACL2 image>
See Makefile file for the detail.
----------------------------------------------------------------------
Book Organization
----------------------------------------------------------------------
gcd-alg.lisp: a GCD algorithm and its correctness theorems.
gcd-spec.lisp: a GCD specification at the bit-vector level.
gcd-body1.lisp: a combinational circuit model, gcd-body1, performing
the GCD operation in one iteration. It is constructed using the
ripple-carry subtractor ripple-sub.
gcd1.lisp: a circuit model, gcd1, computing the Greatest Common Divisor
(GCD) of two natural numbers.
gcd-body2.lisp: a sequential circuit model, gcd-body2, performing the
GCD operation in one iteration. It is constructed using the
ripple-carry subtractor ripple-sub.
gcd2.lisp: a GCD circuit model, gcd2, that contains gcd-body2 as a
submodule.
gcd-body3.lisp: a sequential circuit model, gcd-body3, performing the
GCD operation in one iteration. It is constructed using the
self-timed serial subtractor serial-sub.
gcd3.lisp: a GCD circuit model, gcd3, that contains gcd-body3 as a
submodule.
comp-gcd-cond.lisp: a circuit model, comp-gcd-cond, performing the
GCD condition. It contains Q2 and Q3 as submodules.
comp-gcd.lisp: a GCD circuit model, c-gcd, that contains comp-gcd-cond
as a submodule.
q10-gcd1.lisp: a GCD circuit model, q10-gcd1, that concatenates Q10 and
gcd1.
q10-comp-gcd.lisp: a GCD circuit model, q10-c-gcd, that concatenates
Q10 and c-gcd.
|
