-
Notifications
You must be signed in to change notification settings - Fork 1
/
README
144 lines (105 loc) · 5.22 KB
/
README
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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
Modification of CUDD 3.0.0 to support chaining of BDDs and ZDDs
Only a subset of the functions have been updated to make use of
chaining. As a result, some of the functionality of CUDD will not
work properly here. In general, those that support Boolean operations
on BDDs, ZDDs, and ADDs work properly. Most arithmetic operations on
ADDs should also work. Those that involve quantification do not.
Dynamic variable ordering is not supported.
INSTALLATION NOTE:
If you retrieved the code via git, then the file dates will be
incorrect. This can lead to problems with autoconfiguration, and
possibly cause the make command to fail. The quick work around is to
execute the command:
touch Makefile.am Makefile.in aclocal.m4
before executing the make command.
--------------------------------------------------------------------
Original README file
--------------------------------------------------------------------
The CUDD package is a package written in C for the manipulation of
decision diagrams. It supports binary decision diagrams (BDDs),
algebraic decision diagrams (ADDs), and Zero-Suppressed BDDs (ZDDs).
This directory contains a set of packages that allow you to build a test
application based on the CUDD package.
The test application provided in this kit is called nanotrav and is a
simple-minded FSM traversal program. (See the README file and the man
page nanotrav.1 in the nanotrav directory for the details.) It is
included so that you can run a sanity check on your installation.
Also included in this distribution are the dddmp libray by Giampiero
Cabodi and Stefano Quer and a C++ object-oriented wrapper for CUDD.
BUILD AND INSTALLATION
In the simplest form, you can build the static libraries with:
./configure
make
make check
The configure script provides a few options, which can be listed with
./configure --help
Notable options include
--enable-silent-rules
--enable-shared
--enable-dddmp
--enable-obj
--with-system-qsort
The --enable-silent-rules option is a standard option that streamlines the
messages produced by the build process. The remaining options are specific
to CUDD.
The three "enable" options control the build of shared libraries. By
default, only static libraries are built. With --enable-shared, a
shared library for libcudd is built. (Before installation, it can be
found in cudd/.libs.)
The last two "enable" options control the inclusion of the dddmp
library and C++ wrapper in the shared library, which by default only
contains the core CUDD library.
The --with-system-qsort option requests use of the qsort from the
standard library instead of the portable one shipped with CUDD. This
option is provided for backward compatibility and is not otherwise
recommended. Some of the tests of "make check" may fail with the
system qsort because variable orders may be generated that are
different from the reference ones.
As an example, a more elaborate build command sequence may be:
./configure CC=clang CXX=clang++ --enable-silent-rules \
--enable-shared --enable-obj
make -j4 check
make install
which selects alternate compilers instead of gcc and g++, causes the
C++ wrapper to be included in the shared library, enables parallel
compilation (with -j4) and finally installs the shared library using
the default prefix /usr/local.
For those unfamiliar with libtool it may be worth noting that the
libraries it builds go in .libs subdirectories. One should also note
that with shared libraries enabled, the test programs immediately
visible to the user are shell scripts that make sure dynamic linking
works before installation. If you want to run valgrind on, say, a
dynamically linked nanotrav, specify the option --trace-children=yes.
PLATFORMS
This kit has been successfully built on the following configurations:
PC (x86 and x86_64) running Ubuntu with gcc and clang
PC (x86 and x86_64) running Ubuntu with g++
PC (x86 and x86_64) running Linux RedHat with gcc
PC (x86 and x86_64) running Linux RedHat with g++
PC (x86_64) running 32-bit Cygwin on Windows 7 and Vista with gcc
PC (x86_64) running 32-bit Cygwin on Windows 7 and Vista with g++
PC (x86_64) running 64-bit Cygwin on Windows 8.1 with gcc and g++
PC (x86_64) running MinGW-w64 on Windows 8.1 with gcc
In all these cases, the C++ wrapper was compiled with the matching C++
compiler (g++ for gcc and clang++ for clang). To compile under MSYS2
(MinGW-w64) one has to pass --build=x86_64-w64-mingw32 to ./configure.
SANITY CHECK
The directory `nanotrav' contains a simple application based on the
CUDD package. The `nanotrav' directory contains a man page that
describes the options nanotrav supports. The files *.blif are sample
input files for nanotrav. The *.out files are the reference output
files.
DOCUMENTATION
If doxygen is installed, running "make" puts HTML documentation for
the CUDD package in directory cudd-3.0.0/cudd/html. The recommended
starting point is index.html. The user's manual in PDF format is
built in cudd-3.0.0/doc if pdflatex and makeindex are installed.
Documentation for the dddmp library is in the dddmp/doc subdirectory.
FEEDBACK:
Send feedback to:
Fabio Somenzi
University of Colorado at Boulder
ECE Dept.
Boulder, CO 80309-0425
http://vlsi.colorado.edu/~fabio