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
|
----------------------------------------------------------------------
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
----------------------------------------------------------------------
The modeling and verification of the old 32-bit self-timed serial
adder are implemented in
32-bit-serial-adder-old/32-bit-serial-adder.lisp.
piso-sreg.lisp: a parallel-in, serial-out (PISO) shift register model.
piso2-sreg.lisp: a module consists of two PISO shift registers that
share the same communication signal at their input ports.
sipo-sreg.lisp: a serial-in, parallel-out (SIPO) shift register model.
serial-add.lisp: a serial adder model serial-add.
serial-sub.lisp: a serial subtractor model serial-sub.
|
