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
|
----------------------------------------------------------------------
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
----------------------------------------------------------------------
arb-merge1.lisp: a simple, combinational arbitrated merge joint
arb-merge1.
arb-merge2.lisp: a more complex, sequential arbitrated merge joint
arb-merge2 that supports fairness.
interl1.lisp: a circuit family, interl1, that connects two instances
of Q20' to the two input ports of arb-merge1.
interl2.lisp: a circuit family, interl2, that connects two instances
of Q20' to the two input ports of arb-merge2.
interl-ll.lisp: a circuit family, interl-ll, that connects Q9' and
Q11' to the two input ports of arb-merge2. It is designed as a left
half-complex link.
igcd1.lisp: a circuit family, igcd1, that concatenates interl1 and gcd.
igcd2.lisp: a circuit family, igcd2, that concatenates interl2 and gcd.
comp-interl1.lisp: a circuit family, comp-interl1, that connects the
outputs from two instances of interl1 to the inputs of a third
instance of interl1.
comp-interl2.lisp: a circuit family, comp-interl2, that connects the
outputs from two instances of interl2 to the inputs of a third
instance of interl2.
comp-interl.lisp: a circuit family, comp-interl, that connects the
outputs from two instances of interl2 to the inputs of an instance of
interl-ll.
|
