This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
cs-486:tools [2018/09/04 10:15] egm [Spin] |
cs-486:tools [2021/04/09 08:47] egm [Graphviz] |
||
---|---|---|---|
Line 21: | Line 21: | ||
== Cudd == | == Cudd == | ||
- | The newest version of [ftp://vlsi.colorado.edu/pub/cudd-3.0.0.tar.gz CUDD] includes a configure script. For the OS X build, I did the following: | + | The [https://davidkebo.com/cudd CUDD Tutorials] detail various ways to get CUDD with the easiest being the [https://davidkebo.com/source/cudd_versions/cudd-3.0.0.tar.gz CUDD 3.0.0] direct link. There is also a [https://github.com/ivmai/cudd GitHub CUDD 3.0.0] snapshot for cloning. |
+ | |||
+ | |||
+ | For the OS X build, I did the following: | ||
$ ./configure CC=clang CXX=clang++ | $ ./configure CC=clang CXX=clang++ | ||
Line 53: | Line 56: | ||
Install [http://www.graphviz.org Graphviz] to visualize BDDs. Once it is installed, '''Cudd::DumpDot''' will generate DOT files. These files are converted to PDF with | Install [http://www.graphviz.org Graphviz] to visualize BDDs. Once it is installed, '''Cudd::DumpDot''' will generate DOT files. These files are converted to PDF with | ||
$ dot -Tpdf -o file.pdf file.dot | $ dot -Tpdf -o file.pdf file.dot | ||
- | Please note that CUDD uses complement edges. These are depicted as short-dash lines as opposed to long-dash lines. If you traverse each time you traverse a complement edge on the way to the terminal, you complement that terminal. Thus, an even number of complement edges leaves the terminal unchanged (i.e., terminal one) while an odd number of complement edges flips the terminal to zero. | + | Please note that CUDD uses complement edges. These are depicted as doted lines as opposed to long-dash lines. You have to traverse from the label to the root node as that edge may be a complement edge. In the BDD, the complement edge has the same meaning as the dashed edge: set the variable low. Additionally, the complement edge tells you if you need to complement the terminal when you reach the terminal. If the path being considered from the function label includes an ever number of complement edges, then the terminal is unchanged. If the path from the function label being considered includes an odd number of complement edges, then the terminal is complimented (i.e., terminal one with an even number of compliment edges in the path and terminal zero with an odd number of edges in the path). |