Text: "Logic Synthesis and Verification Algorithms", Hachtel and
Somenzi
Notes:
Introduction
BDD/Symmetric Functions
BDD Implementation
BDD Decomposition
Sequential Machines
State Assignment
SAT-Stalmarck Method
SAT-Zchaff
References:
BDD Implicit Traversal 1 (Includes Restrict)
BDD Implicit Traversal 2
BDS
Homework:
HW2 Solutions
HW6
Files:
FORTE.tgz
CUDD 2.4.0
Pycudd 2.0
abc51205 logic synthesizer source code
Pycudd Notes: To install cudd or pycudd, refer to the included Install
files, be sure to
avoid too specific machine optimizations (i.e. don't use -mcpu=pentium4
unless you know
you are running a p4). To run from ~forrest/pycudd directory, you
need to set:
PYTHONPATH ~forrest/pycudd/pycudd
LD_LIBRARY_PATH ~forrest/pycudd/cudd-2.4.0/lib
Note that you need to make sharable object libraries from CUDD to run
PYCUDD --
read the PYCUDD documentation. To test, after setting the above
variables, run
example1.py and example2.py. Note we do not yet have permission to
distribute BREL.
BerkMin SAT package
BerkMin notes: executable only -- needs libstdc++-libc6.1-1.so.2 this is
provided by
compatability libraries.
Zchaff source distribution
Zchaff is easy to compile, just unpack and type 'make all'