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
|
----------------------------------------------------------------------
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
----------------------------------------------------------------------
queue2.lisp: a queue, Q2, of 2 links.
queue3.lisp: a queue, Q3, of 3 links.
queue4.lisp: a queue, Q4, of 4 links.
queue5.lisp: a queue, Q5, of 5 links.
queue10.lisp: a queue, Q10, of 10 links. It is constructed by
connecting Q4 with Q5 via a link.
queue3-l.lisp: a queue, Q3', of 3 links. It is designed as a
complex link.
queue4-l.lisp: a queue, Q4', of 4 links. It is designed as a
complex link.
queue5-l.lisp: a queue, Q5', of 5 links. It is designed as a
complex link.
queue8-l.lisp: a queue, Q8', of 8 links. It is designed as a
complex link and is composed of two instances of Q4'.
queue9-l.lisp: a queue, Q9', of 9 links. It is designed as a
complex link and is composed of Q4' and Q5'.
queue10-l.lisp: a queue, Q10', of 10 links. It is designed as a
complex link and is composed of two instances of Q5'.
queue11-l.lisp: a queue, Q11', of 11 links. It is designed as a
complex link and is composed of Q3' and Q8'.
queue20-l.lisp: a queue, Q20', of 20 links. It is designed as a
complex link and is composed of two instances of Q10'.
comp-v-or.lisp: a circuit, C-V-OR, performing the bitwise OR
operation. It contains Q2 and Q3 as submodules.
wig-wag.lisp: a wig-wag circuit, WW.
round-robin1.lisp: a round-robin circuit, RR1. It contains Q2 and Q3
as submodules.
round-robin2.lisp: a round-robin circuit, RR2. It contains Q4' and Q5'
as submodules.
round-robin3.lisp: a round-robin circuit, RR3. It contains Q8' and
Q10' as submodules.
|
