[8] | 1 | <HTML> |
---|
| 2 | <HEAD><TITLE>The cal package: files</TITLE></HEAD> |
---|
| 3 | <BODY> |
---|
| 4 | |
---|
| 5 | <DL> |
---|
| 6 | <DT> <A HREF="#cal.h"><CODE>cal.h</CODE></A> |
---|
| 7 | <DD> External header file |
---|
| 8 | <DT> <A HREF="#calInt.h"><CODE>calInt.h</CODE></A> |
---|
| 9 | <DD> Internal header file |
---|
| 10 | <DT> <A HREF="#cal.c"><CODE>cal.c</CODE></A> |
---|
| 11 | <DD> Miscellaneous collection of exported BDD functions |
---|
| 12 | <DT> <A HREF="#calApplyReduce.c"><CODE>calApplyReduce.c</CODE></A> |
---|
| 13 | <DD> Generic routines for processing temporary nodes during |
---|
| 14 | "apply" and "reduce" phases. |
---|
| 15 | <DT> <A HREF="#calAssociation.c"><CODE>calAssociation.c</CODE></A> |
---|
| 16 | <DD> Contains the routines related to the variable association. |
---|
| 17 | <DT> <A HREF="#calBddCompose.c"><CODE>calBddCompose.c</CODE></A> |
---|
| 18 | <DD> Routine for composing one BDD into another. |
---|
| 19 | <DT> <A HREF="#calBddITE.c"><CODE>calBddITE.c</CODE></A> |
---|
| 20 | <DD> Routine for computing ITE of 3 BDD operands. |
---|
| 21 | <DT> <A HREF="#calBddManager.c"><CODE>calBddManager.c</CODE></A> |
---|
| 22 | <DD> Routines for maintaing the manager and creating |
---|
| 23 | variables etc. |
---|
| 24 | <DT> <A HREF="#calBddOp.c"><CODE>calBddOp.c</CODE></A> |
---|
| 25 | <DD> Routines for performing simple boolean operations on a |
---|
| 26 | pair of BDDs or on an array of pair of BDDs or on an array of BDDs. |
---|
| 27 | <DT> <A HREF="#calBddReorderTest.c"><CODE>calBddReorderTest.c</CODE></A> |
---|
| 28 | <DD> A test routine for checking the functionality of |
---|
| 29 | dynamic reordering. |
---|
| 30 | <DT> <A HREF="#calBddSatisfy.c"><CODE>calBddSatisfy.c</CODE></A> |
---|
| 31 | <DD> Routines for BDD satisfying valuation. |
---|
| 32 | <DT> <A HREF="#calBddSize.c"><CODE>calBddSize.c</CODE></A> |
---|
| 33 | <DD> BDD size and profile routines |
---|
| 34 | <DT> <A HREF="#calBddSubstitute.c"><CODE>calBddSubstitute.c</CODE></A> |
---|
| 35 | <DD> Routine for simultaneous substitution of an array of |
---|
| 36 | variables with an array of functions. |
---|
| 37 | <DT> <A HREF="#calBddSupport.c"><CODE>calBddSupport.c</CODE></A> |
---|
| 38 | <DD> Routines related to the support of a BDD. |
---|
| 39 | <DT> <A HREF="#calBddSwapVars.c"><CODE>calBddSwapVars.c</CODE></A> |
---|
| 40 | <DD> Routine for swapping two variables. |
---|
| 41 | <DT> <A HREF="#calBddVarSubstitute.c"><CODE>calBddVarSubstitute.c</CODE></A> |
---|
| 42 | <DD> Routine for simultaneous substitution of an array of |
---|
| 43 | variables with another array of variables. |
---|
| 44 | <DT> <A HREF="#calBlk.c"><CODE>calBlk.c</CODE></A> |
---|
| 45 | <DD> Routines for manipulating blocks of variables. |
---|
| 46 | <DT> <A HREF="#calCacheTableTwo.c"><CODE>calCacheTableTwo.c</CODE></A> |
---|
| 47 | <DD> Functions to manage the Cache tables. |
---|
| 48 | <DT> <A HREF="#calDump.c"><CODE>calDump.c</CODE></A> |
---|
| 49 | <DD> BDD library dump/undump routines |
---|
| 50 | <DT> <A HREF="#calGC.c"><CODE>calGC.c</CODE></A> |
---|
| 51 | <DD> Garbage collection routines |
---|
| 52 | <DT> <A HREF="#calHashTable.c"><CODE>calHashTable.c</CODE></A> |
---|
| 53 | <DD> Functions to manage the hash tables that are a part of |
---|
| 54 | 1. unique table |
---|
| 55 | 2. request queue |
---|
| 56 | <DT> <A HREF="#calHashTableOne.c"><CODE>calHashTableOne.c</CODE></A> |
---|
| 57 | <DD> Routines for managing hash table with Bdd is a key and |
---|
| 58 | int, long, or double as a value |
---|
| 59 | <DT> <A HREF="#calHashTableThree.c"><CODE>calHashTableThree.c</CODE></A> |
---|
| 60 | <DD> Functions to manage the hash tables that are a part of |
---|
| 61 | ITE operation |
---|
| 62 | <DT> <A HREF="#calInteract.c"><CODE>calInteract.c</CODE></A> |
---|
| 63 | <DD> Functions to manipulate the variable interaction matrix. |
---|
| 64 | <DT> <A HREF="#calMem.c"><CODE>calMem.c</CODE></A> |
---|
| 65 | <DD> Routines for memory management. |
---|
| 66 | <DT> <A HREF="#calMemoryManagement.c"><CODE>calMemoryManagement.c</CODE></A> |
---|
| 67 | <DD> Special memory management routines specific to CAL. |
---|
| 68 | <DT> <A HREF="#calPerformanceTest.c"><CODE>calPerformanceTest.c</CODE></A> |
---|
| 69 | <DD> This file contains the performance test routines for |
---|
| 70 | the CAL package. |
---|
| 71 | <DT> <A HREF="#calPipeline.c"><CODE>calPipeline.c</CODE></A> |
---|
| 72 | <DD> Routines for creating and managing the pipelined BDD |
---|
| 73 | operations. |
---|
| 74 | <DT> <A HREF="#calPrint.c"><CODE>calPrint.c</CODE></A> |
---|
| 75 | <DD> Routine for printing a BDD. |
---|
| 76 | <DT> <A HREF="#calPrintProfile.c"><CODE>calPrintProfile.c</CODE></A> |
---|
| 77 | <DD> Routines for printing various profiles for a BDD. |
---|
| 78 | <DT> <A HREF="#calQuant.c"><CODE>calQuant.c</CODE></A> |
---|
| 79 | <DD> Routines for existential/universal quantification and |
---|
| 80 | relational product. |
---|
| 81 | <DT> <A HREF="#calReduce.c"><CODE>calReduce.c</CODE></A> |
---|
| 82 | <DD> Routines for optimizing a BDD with respect to a don't |
---|
| 83 | care set (cofactor and restrict). |
---|
| 84 | <DT> <A HREF="#calReorderBF.c"><CODE>calReorderBF.c</CODE></A> |
---|
| 85 | <DD> Routines for dynamic reordering of variables. |
---|
| 86 | <DT> <A HREF="#calReorderDF.c"><CODE>calReorderDF.c</CODE></A> |
---|
| 87 | <DD> Routines for dynamic reordering of variables. |
---|
| 88 | <DT> <A HREF="#calReorderUtil.c"><CODE>calReorderUtil.c</CODE></A> |
---|
| 89 | <DD> Some utility routines used by both breadth-first and |
---|
| 90 | depth-first reordering techniques. |
---|
| 91 | <DT> <A HREF="#calTerminal.c"><CODE>calTerminal.c</CODE></A> |
---|
| 92 | <DD> Contains the terminal function for various BDD operations. |
---|
| 93 | <DT> <A HREF="#calTest.c"><CODE>calTest.c</CODE></A> |
---|
| 94 | <DD> This file contains the test routines for the CAL package. |
---|
| 95 | <DT> <A HREF="#calUtil.c"><CODE>calUtil.c</CODE></A> |
---|
| 96 | <DD> Utility functions for the Cal package. |
---|
| 97 | </DL><HR> |
---|
| 98 | <A NAME="cal.h"><H1>cal.h</H1></A> |
---|
| 99 | External header file <P> |
---|
| 100 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 101 | Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu)</B><P> |
---|
| 102 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 103 | <DL> |
---|
| 104 | </DL> |
---|
| 105 | <HR> |
---|
| 106 | <A NAME="calInt.h"><H1>calInt.h</H1></A> |
---|
| 107 | Internal header file <P> |
---|
| 108 | <B>By: Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu |
---|
| 109 | Jagesh Sanghavi (sanghavi@ic.eecs.berkeley.edu)</B><P> |
---|
| 110 | <P><B>See Also</B><A HREF="#cal.h"><CODE>cal.h</CODE></A> |
---|
| 111 | <DL> |
---|
| 112 | </DL> |
---|
| 113 | <HR> |
---|
| 114 | <A NAME="cal.c"><H1>cal.c</H1></A> |
---|
| 115 | Miscellaneous collection of exported BDD functions <P> |
---|
| 116 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and |
---|
| 117 | Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu</B><P> |
---|
| 118 | <DL> |
---|
| 119 | <DT> <A HREF="calAllDet.html#Cal_BddIsEqual" TARGET="MAIN"><CODE>Cal_BddIsEqual()</CODE></A> |
---|
| 120 | <DD> Returns 1 if argument BDDs are equal, 0 otherwise. |
---|
| 121 | |
---|
| 122 | <DT> <A HREF="calAllDet.html#Cal_BddIsBddOne" TARGET="MAIN"><CODE>Cal_BddIsBddOne()</CODE></A> |
---|
| 123 | <DD> Returns 1 if the argument BDD is constant one, 0 otherwise. |
---|
| 124 | |
---|
| 125 | <DT> <A HREF="calAllDet.html#Cal_BddIsBddZero" TARGET="MAIN"><CODE>Cal_BddIsBddZero()</CODE></A> |
---|
| 126 | <DD> Returns 1 if the argument BDD is constant zero, 0 otherwise. |
---|
| 127 | |
---|
| 128 | <DT> <A HREF="calAllDet.html#Cal_BddIsBddNull" TARGET="MAIN"><CODE>Cal_BddIsBddNull()</CODE></A> |
---|
| 129 | <DD> Returns 1 if the argument BDD is NULL, 0 otherwise. |
---|
| 130 | |
---|
| 131 | <DT> <A HREF="calAllDet.html#Cal_BddIsBddConst" TARGET="MAIN"><CODE>Cal_BddIsBddConst()</CODE></A> |
---|
| 132 | <DD> Returns 1 if the argument BDD is a constant, 0 otherwise. |
---|
| 133 | |
---|
| 134 | <DT> <A HREF="calAllDet.html#Cal_BddIdentity" TARGET="MAIN"><CODE>Cal_BddIdentity()</CODE></A> |
---|
| 135 | <DD> Returns the duplicate BDD of the argument BDD. |
---|
| 136 | |
---|
| 137 | <DT> <A HREF="calAllDet.html#Cal_BddOne" TARGET="MAIN"><CODE>Cal_BddOne()</CODE></A> |
---|
| 138 | <DD> Returns the BDD for the constant one |
---|
| 139 | |
---|
| 140 | <DT> <A HREF="calAllDet.html#Cal_BddZero" TARGET="MAIN"><CODE>Cal_BddZero()</CODE></A> |
---|
| 141 | <DD> Returns the BDD for the constant zero |
---|
| 142 | |
---|
| 143 | <DT> <A HREF="calAllDet.html#Cal_BddNot" TARGET="MAIN"><CODE>Cal_BddNot()</CODE></A> |
---|
| 144 | <DD> Returns the complement of the argument BDD. |
---|
| 145 | |
---|
| 146 | <DT> <A HREF="calAllDet.html#Cal_BddGetIfIndex" TARGET="MAIN"><CODE>Cal_BddGetIfIndex()</CODE></A> |
---|
| 147 | <DD> Returns the index of the top variable of the argument BDD. |
---|
| 148 | |
---|
| 149 | <DT> <A HREF="calAllDet.html#Cal_BddGetIfId" TARGET="MAIN"><CODE>Cal_BddGetIfId()</CODE></A> |
---|
| 150 | <DD> Returns the id of the top variable of the argument BDD. |
---|
| 151 | |
---|
| 152 | <DT> <A HREF="calAllDet.html#Cal_BddIf" TARGET="MAIN"><CODE>Cal_BddIf()</CODE></A> |
---|
| 153 | <DD> Returns the BDD corresponding to the top variable of |
---|
| 154 | the argument BDD. |
---|
| 155 | |
---|
| 156 | <DT> <A HREF="calAllDet.html#Cal_BddThen" TARGET="MAIN"><CODE>Cal_BddThen()</CODE></A> |
---|
| 157 | <DD> Returns the positive cofactor of the argument BDD with |
---|
| 158 | respect to the top variable of the BDD. |
---|
| 159 | |
---|
| 160 | <DT> <A HREF="calAllDet.html#Cal_BddElse" TARGET="MAIN"><CODE>Cal_BddElse()</CODE></A> |
---|
| 161 | <DD> Returns the negative cofactor of the argument BDD with |
---|
| 162 | respect to the top variable of the BDD. |
---|
| 163 | |
---|
| 164 | <DT> <A HREF="calAllDet.html#Cal_BddFree" TARGET="MAIN"><CODE>Cal_BddFree()</CODE></A> |
---|
| 165 | <DD> Frees the argument BDD. |
---|
| 166 | |
---|
| 167 | <DT> <A HREF="calAllDet.html#Cal_BddUnFree" TARGET="MAIN"><CODE>Cal_BddUnFree()</CODE></A> |
---|
| 168 | <DD> Unfrees the argument BDD. |
---|
| 169 | |
---|
| 170 | <DT> <A HREF="calAllDet.html#Cal_BddGetRegular" TARGET="MAIN"><CODE>Cal_BddGetRegular()</CODE></A> |
---|
| 171 | <DD> Returns a BDD with positive from a given BDD with arbitrary phase |
---|
| 172 | |
---|
| 173 | <DT> <A HREF="calAllDet.html#Cal_BddIntersects" TARGET="MAIN"><CODE>Cal_BddIntersects()</CODE></A> |
---|
| 174 | <DD> Computes a BDD that implies conjunction of f and g. |
---|
| 175 | |
---|
| 176 | <DT> <A HREF="calAllDet.html#Cal_BddImplies" TARGET="MAIN"><CODE>Cal_BddImplies()</CODE></A> |
---|
| 177 | <DD> Computes a BDD that implies conjunction of f and Cal_BddNot(g) |
---|
| 178 | |
---|
| 179 | <DT> <A HREF="calAllDet.html#Cal_BddTotalSize" TARGET="MAIN"><CODE>Cal_BddTotalSize()</CODE></A> |
---|
| 180 | <DD> Returns the number of nodes in the Unique table |
---|
| 181 | |
---|
| 182 | <DT> <A HREF="calAllDet.html#Cal_BddStats" TARGET="MAIN"><CODE>Cal_BddStats()</CODE></A> |
---|
| 183 | <DD> Prints miscellaneous BDD statistics |
---|
| 184 | |
---|
| 185 | <DT> <A HREF="calAllDet.html#Cal_BddDynamicReordering" TARGET="MAIN"><CODE>Cal_BddDynamicReordering()</CODE></A> |
---|
| 186 | <DD> Specify dynamic reordering technique. |
---|
| 187 | |
---|
| 188 | <DT> <A HREF="calAllDet.html#Cal_BddReorder" TARGET="MAIN"><CODE>Cal_BddReorder()</CODE></A> |
---|
| 189 | <DD> Invoke the current dynamic reodering method. |
---|
| 190 | |
---|
| 191 | <DT> <A HREF="calAllDet.html#Cal_BddType" TARGET="MAIN"><CODE>Cal_BddType()</CODE></A> |
---|
| 192 | <DD> Returns type of a BDD ( 0, 1, +var, -var, ovrflow, nonterminal) |
---|
| 193 | |
---|
| 194 | <DT> <A HREF="calAllDet.html#Cal_BddVars" TARGET="MAIN"><CODE>Cal_BddVars()</CODE></A> |
---|
| 195 | <DD> Returns the number of BDD variables |
---|
| 196 | |
---|
| 197 | <DT> <A HREF="calAllDet.html#Cal_BddNodeLimit" TARGET="MAIN"><CODE>Cal_BddNodeLimit()</CODE></A> |
---|
| 198 | <DD> Sets the node limit to new_limit and returns the old limit. |
---|
| 199 | |
---|
| 200 | <DT> <A HREF="calAllDet.html#Cal_BddOverflow" TARGET="MAIN"><CODE>Cal_BddOverflow()</CODE></A> |
---|
| 201 | <DD> Returns 1 if the node limit has been exceeded, 0 otherwise. The |
---|
| 202 | overflow flag is cleared. |
---|
| 203 | |
---|
| 204 | <DT> <A HREF="calAllDet.html#Cal_BddIsCube" TARGET="MAIN"><CODE>Cal_BddIsCube()</CODE></A> |
---|
| 205 | <DD> Returns 1 if the argument BDD is a cube, 0 otherwise |
---|
| 206 | |
---|
| 207 | <DT> <A HREF="calAllDet.html#Cal_BddManagerGetHooks" TARGET="MAIN"><CODE>Cal_BddManagerGetHooks()</CODE></A> |
---|
| 208 | <DD> Returns the hooks field of the manager. |
---|
| 209 | |
---|
| 210 | <DT> <A HREF="calAllDet.html#Cal_BddManagerSetHooks" TARGET="MAIN"><CODE>Cal_BddManagerSetHooks()</CODE></A> |
---|
| 211 | <DD> Sets the hooks field of the manager. |
---|
| 212 | |
---|
| 213 | <DT> <A HREF="calAllDet.html#CalBddIf" TARGET="MAIN"><CODE>CalBddIf()</CODE></A> |
---|
| 214 | <DD> Returns the BDD corresponding to the top variable of |
---|
| 215 | the argument BDD. |
---|
| 216 | |
---|
| 217 | <DT> <A HREF="calAllDet.html#CalBddIsCubeStep" TARGET="MAIN"><CODE>CalBddIsCubeStep()</CODE></A> |
---|
| 218 | <DD> Returns 1 if the argument BDD is a cube, 0 otherwise |
---|
| 219 | |
---|
| 220 | <DT> <A HREF="calAllDet.html#CalBddTypeAux" TARGET="MAIN"><CODE>CalBddTypeAux()</CODE></A> |
---|
| 221 | <DD> Returns the BDD type by recursively traversing the argument BDD |
---|
| 222 | |
---|
| 223 | <DT> <A HREF="calAllDet.html#CalBddIdentity" TARGET="MAIN"><CODE>CalBddIdentity()</CODE></A> |
---|
| 224 | <DD> Returns the duplicate BDD of the argument BDD. |
---|
| 225 | |
---|
| 226 | <DT> <A HREF="calAllDet.html#BddIntersectsStep" TARGET="MAIN"><CODE>BddIntersectsStep()</CODE></A> |
---|
| 227 | <DD> Recursive routine to returns a BDD that implies conjunction of |
---|
| 228 | argument BDDs |
---|
| 229 | |
---|
| 230 | </DL> |
---|
| 231 | <HR> |
---|
| 232 | <A NAME="calApplyReduce.c"><H1>calApplyReduce.c</H1></A> |
---|
| 233 | Generic routines for processing temporary nodes during |
---|
| 234 | "apply" and "reduce" phases. <P> |
---|
| 235 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 236 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 237 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 238 | <DL> |
---|
| 239 | <DT> <A HREF="calAllDet.html#CalHashTableApply" TARGET="MAIN"><CODE>CalHashTableApply()</CODE></A> |
---|
| 240 | <DD> required |
---|
| 241 | |
---|
| 242 | <DT> <A HREF="calAllDet.html#CalHashTableReduce" TARGET="MAIN"><CODE>CalHashTableReduce()</CODE></A> |
---|
| 243 | <DD> required |
---|
| 244 | |
---|
| 245 | </DL> |
---|
| 246 | <HR> |
---|
| 247 | <A NAME="calAssociation.c"><H1>calAssociation.c</H1></A> |
---|
| 248 | Contains the routines related to the variable association. <P> |
---|
| 249 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 250 | Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)</B><P> |
---|
| 251 | optional <P> |
---|
| 252 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 253 | <DL> |
---|
| 254 | <DT> <A HREF="calAllDet.html#Cal_AssociationInit" TARGET="MAIN"><CODE>Cal_AssociationInit()</CODE></A> |
---|
| 255 | <DD> Creates or finds a variable association. |
---|
| 256 | |
---|
| 257 | <DT> <A HREF="calAllDet.html#Cal_AssociationQuit" TARGET="MAIN"><CODE>Cal_AssociationQuit()</CODE></A> |
---|
| 258 | <DD> Deletes the variable association given by id |
---|
| 259 | |
---|
| 260 | <DT> <A HREF="calAllDet.html#Cal_AssociationSetCurrent" TARGET="MAIN"><CODE>Cal_AssociationSetCurrent()</CODE></A> |
---|
| 261 | <DD> Sets the current variable association to the one given by id and |
---|
| 262 | returns the ID of the old association. |
---|
| 263 | |
---|
| 264 | <DT> <A HREF="calAllDet.html#Cal_TempAssociationAugment" TARGET="MAIN"><CODE>Cal_TempAssociationAugment()</CODE></A> |
---|
| 265 | <DD> Adds to the temporary variable association. |
---|
| 266 | |
---|
| 267 | <DT> <A HREF="calAllDet.html#Cal_TempAssociationInit" TARGET="MAIN"><CODE>Cal_TempAssociationInit()</CODE></A> |
---|
| 268 | <DD> Sets the temporary variable association. |
---|
| 269 | |
---|
| 270 | <DT> <A HREF="calAllDet.html#Cal_TempAssociationQuit" TARGET="MAIN"><CODE>Cal_TempAssociationQuit()</CODE></A> |
---|
| 271 | <DD> Cleans up temporary association |
---|
| 272 | |
---|
| 273 | <DT> <A HREF="calAllDet.html#CalAssociationListFree" TARGET="MAIN"><CODE>CalAssociationListFree()</CODE></A> |
---|
| 274 | <DD> Frees the variable associations |
---|
| 275 | |
---|
| 276 | <DT> <A HREF="calAllDet.html#CalVarAssociationRepackUpdate" TARGET="MAIN"><CODE>CalVarAssociationRepackUpdate()</CODE></A> |
---|
| 277 | <DD> Need to be called after repacking. |
---|
| 278 | |
---|
| 279 | <DT> <A HREF="calAllDet.html#CalCheckAssociationValidity" TARGET="MAIN"><CODE>CalCheckAssociationValidity()</CODE></A> |
---|
| 280 | <DD> Checks the validity of association. |
---|
| 281 | |
---|
| 282 | <DT> <A HREF="calAllDet.html#CalReorderAssociationFix" TARGET="MAIN"><CODE>CalReorderAssociationFix()</CODE></A> |
---|
| 283 | <DD> required |
---|
| 284 | |
---|
| 285 | <DT> <A HREF="calAllDet.html#AssociationIsEqual" TARGET="MAIN"><CODE>AssociationIsEqual()</CODE></A> |
---|
| 286 | <DD> Checks for equality of two associations |
---|
| 287 | |
---|
| 288 | <DT> <A HREF="calAllDet.html#CheckAssoc" TARGET="MAIN"><CODE>CheckAssoc()</CODE></A> |
---|
| 289 | <DD> required |
---|
| 290 | |
---|
| 291 | </DL> |
---|
| 292 | <HR> |
---|
| 293 | <A NAME="calBddCompose.c"><H1>calBddCompose.c</H1></A> |
---|
| 294 | Routine for composing one BDD into another. <P> |
---|
| 295 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 296 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 297 | <DL> |
---|
| 298 | <DT> <A HREF="calAllDet.html#Cal_BddCompose" TARGET="MAIN"><CODE>Cal_BddCompose()</CODE></A> |
---|
| 299 | <DD> composition - substitute a BDD variable by a function |
---|
| 300 | |
---|
| 301 | <DT> <A HREF="calAllDet.html#CalRequestNodeListCompose" TARGET="MAIN"><CODE>CalRequestNodeListCompose()</CODE></A> |
---|
| 302 | <DD> required |
---|
| 303 | |
---|
| 304 | <DT> <A HREF="calAllDet.html#CalHashTableComposeApply" TARGET="MAIN"><CODE>CalHashTableComposeApply()</CODE></A> |
---|
| 305 | <DD> required |
---|
| 306 | |
---|
| 307 | <DT> <A HREF="calAllDet.html#CalComposeRequestCreate" TARGET="MAIN"><CODE>CalComposeRequestCreate()</CODE></A> |
---|
| 308 | <DD> required |
---|
| 309 | |
---|
| 310 | </DL> |
---|
| 311 | <HR> |
---|
| 312 | <A NAME="calBddITE.c"><H1>calBddITE.c</H1></A> |
---|
| 313 | Routine for computing ITE of 3 BDD operands. <P> |
---|
| 314 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 315 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 316 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 317 | <DL> |
---|
| 318 | <DT> <A HREF="calAllDet.html#Cal_BddITE" TARGET="MAIN"><CODE>Cal_BddITE()</CODE></A> |
---|
| 319 | <DD> Returns the BDD for logical If-Then-Else |
---|
| 320 | |
---|
| 321 | Description [Returns the BDD for the logical operation IF f THEN g ELSE h |
---|
| 322 | - f g + f' h |
---|
| 323 | |
---|
| 324 | <DT> <A HREF="calAllDet.html#CalRequestNodeListArrayITE" TARGET="MAIN"><CODE>CalRequestNodeListArrayITE()</CODE></A> |
---|
| 325 | <DD> required |
---|
| 326 | |
---|
| 327 | <DT> <A HREF="calAllDet.html#CalBddOpITEBF" TARGET="MAIN"><CODE>CalBddOpITEBF()</CODE></A> |
---|
| 328 | <DD> required |
---|
| 329 | |
---|
| 330 | <DT> <A HREF="calAllDet.html#CalHashTableITEApply" TARGET="MAIN"><CODE>CalHashTableITEApply()</CODE></A> |
---|
| 331 | <DD> required |
---|
| 332 | |
---|
| 333 | <DT> <A HREF="calAllDet.html#CalBddITE" TARGET="MAIN"><CODE>CalBddITE()</CODE></A> |
---|
| 334 | <DD> Returns the BDD for logical If-Then-Else |
---|
| 335 | |
---|
| 336 | Description [Returns the BDD for the logical operation IF f THEN g ELSE h |
---|
| 337 | - f g + f' h |
---|
| 338 | |
---|
| 339 | </DL> |
---|
| 340 | <HR> |
---|
| 341 | <A NAME="calBddManager.c"><H1>calBddManager.c</H1></A> |
---|
| 342 | Routines for maintaing the manager and creating |
---|
| 343 | variables etc. <P> |
---|
| 344 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 345 | Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)</B><P> |
---|
| 346 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 347 | <DL> |
---|
| 348 | <DT> <A HREF="calAllDet.html#Cal_BddManagerInit" TARGET="MAIN"><CODE>Cal_BddManagerInit()</CODE></A> |
---|
| 349 | <DD> Creates and initializes a new BDD manager. |
---|
| 350 | |
---|
| 351 | <DT> <A HREF="calAllDet.html#Cal_BddManagerQuit" TARGET="MAIN"><CODE>Cal_BddManagerQuit()</CODE></A> |
---|
| 352 | <DD> Frees the BDD manager and all the associated allocations |
---|
| 353 | |
---|
| 354 | <DT> <A HREF="calAllDet.html#Cal_BddManagerSetParameters" TARGET="MAIN"><CODE>Cal_BddManagerSetParameters()</CODE></A> |
---|
| 355 | <DD> Sets appropriate fields of BDD Manager. |
---|
| 356 | |
---|
| 357 | <DT> <A HREF="calAllDet.html#Cal_BddManagerGetNumNodes" TARGET="MAIN"><CODE>Cal_BddManagerGetNumNodes()</CODE></A> |
---|
| 358 | <DD> Returns the number of BDD nodes |
---|
| 359 | |
---|
| 360 | <DT> <A HREF="calAllDet.html#Cal_BddManagerCreateNewVarFirst" TARGET="MAIN"><CODE>Cal_BddManagerCreateNewVarFirst()</CODE></A> |
---|
| 361 | <DD> Creates and returns a new variable at the start of the variable |
---|
| 362 | order. |
---|
| 363 | |
---|
| 364 | <DT> <A HREF="calAllDet.html#Cal_BddManagerCreateNewVarLast" TARGET="MAIN"><CODE>Cal_BddManagerCreateNewVarLast()</CODE></A> |
---|
| 365 | <DD> Creates and returns a new variable at the end of the variable |
---|
| 366 | order. |
---|
| 367 | |
---|
| 368 | <DT> <A HREF="calAllDet.html#Cal_BddManagerCreateNewVarBefore" TARGET="MAIN"><CODE>Cal_BddManagerCreateNewVarBefore()</CODE></A> |
---|
| 369 | <DD> Creates and returns a new variable before the specified one in |
---|
| 370 | the variable order. |
---|
| 371 | |
---|
| 372 | <DT> <A HREF="calAllDet.html#Cal_BddManagerCreateNewVarAfter" TARGET="MAIN"><CODE>Cal_BddManagerCreateNewVarAfter()</CODE></A> |
---|
| 373 | <DD> Creates and returns a new variable after the specified one in |
---|
| 374 | the variable order. |
---|
| 375 | |
---|
| 376 | <DT> <A HREF="calAllDet.html#Cal_BddManagerGetVarWithIndex" TARGET="MAIN"><CODE>Cal_BddManagerGetVarWithIndex()</CODE></A> |
---|
| 377 | <DD> Returns the variable with the specified index, null if no |
---|
| 378 | such variable exists |
---|
| 379 | |
---|
| 380 | <DT> <A HREF="calAllDet.html#Cal_BddManagerGetVarWithId" TARGET="MAIN"><CODE>Cal_BddManagerGetVarWithId()</CODE></A> |
---|
| 381 | <DD> Returns the variable with the specified id, null if no |
---|
| 382 | such variable exists |
---|
| 383 | |
---|
| 384 | <DT> <A HREF="calAllDet.html#CalBddManagerCreateNewVar" TARGET="MAIN"><CODE>CalBddManagerCreateNewVar()</CODE></A> |
---|
| 385 | <DD> This function creates and returns a new variable with given |
---|
| 386 | index value. |
---|
| 387 | |
---|
| 388 | <DT> <A HREF="calAllDet.html#BddDefaultTransformFn" TARGET="MAIN"><CODE>BddDefaultTransformFn()</CODE></A> |
---|
| 389 | <DD> required |
---|
| 390 | |
---|
| 391 | <DT> <A HREF="calAllDet.html#CalBddManagerPrint" TARGET="MAIN"><CODE>CalBddManagerPrint()</CODE></A> |
---|
| 392 | <DD> required |
---|
| 393 | |
---|
| 394 | </DL> |
---|
| 395 | <HR> |
---|
| 396 | <A NAME="calBddOp.c"><H1>calBddOp.c</H1></A> |
---|
| 397 | Routines for performing simple boolean operations on a |
---|
| 398 | pair of BDDs or on an array of pair of BDDs or on an array of BDDs. <P> |
---|
| 399 | <B>By: Rajeev Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 400 | Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)</B><P> |
---|
| 401 | The "cal" specific routines are "Cal_BddPairwiseAnd/Or", |
---|
| 402 | "Cal_BddMultiwayAnd/Or". <P> |
---|
| 403 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 404 | <DL> |
---|
| 405 | <DT> <A HREF="calAllDet.html#Cal_BddAnd" TARGET="MAIN"><CODE>Cal_BddAnd()</CODE></A> |
---|
| 406 | <DD> Returns the BDD for logical AND of argument BDDs |
---|
| 407 | |
---|
| 408 | <DT> <A HREF="calAllDet.html#Cal_BddNand" TARGET="MAIN"><CODE>Cal_BddNand()</CODE></A> |
---|
| 409 | <DD> Returns the BDD for logical NAND of argument BDDs |
---|
| 410 | |
---|
| 411 | <DT> <A HREF="calAllDet.html#Cal_BddOr" TARGET="MAIN"><CODE>Cal_BddOr()</CODE></A> |
---|
| 412 | <DD> Returns the BDD for logical OR of argument BDDs |
---|
| 413 | |
---|
| 414 | <DT> <A HREF="calAllDet.html#Cal_BddNor" TARGET="MAIN"><CODE>Cal_BddNor()</CODE></A> |
---|
| 415 | <DD> Returns the BDD for logical NOR of argument BDDs |
---|
| 416 | |
---|
| 417 | <DT> <A HREF="calAllDet.html#Cal_BddXor" TARGET="MAIN"><CODE>Cal_BddXor()</CODE></A> |
---|
| 418 | <DD> Returns the BDD for logical exclusive OR of argument BDDs |
---|
| 419 | |
---|
| 420 | <DT> <A HREF="calAllDet.html#Cal_BddXnor" TARGET="MAIN"><CODE>Cal_BddXnor()</CODE></A> |
---|
| 421 | <DD> Returns the BDD for logical exclusive NOR of argument BDDs |
---|
| 422 | |
---|
| 423 | <DT> <A HREF="calAllDet.html#Cal_BddPairwiseAnd" TARGET="MAIN"><CODE>Cal_BddPairwiseAnd()</CODE></A> |
---|
| 424 | <DD> Returns an array of BDDs obtained by logical AND of BDD pairs |
---|
| 425 | specified by an BDD array in which a BDD at an even location is paired with |
---|
| 426 | a BDD at an odd location of the array |
---|
| 427 | |
---|
| 428 | <DT> <A HREF="calAllDet.html#Cal_BddPairwiseOr" TARGET="MAIN"><CODE>Cal_BddPairwiseOr()</CODE></A> |
---|
| 429 | <DD> Returns an array of BDDs obtained by logical OR of BDD pairs |
---|
| 430 | specified by an BDD array in which a BDD at an even location is paired with |
---|
| 431 | a BDD at an odd location of the array |
---|
| 432 | |
---|
| 433 | <DT> <A HREF="calAllDet.html#Cal_BddPairwiseXor" TARGET="MAIN"><CODE>Cal_BddPairwiseXor()</CODE></A> |
---|
| 434 | <DD> Returns an array of BDDs obtained by logical XOR of BDD pairs |
---|
| 435 | specified by an BDD array in which a BDD at an even location is paired with |
---|
| 436 | a BDD at an odd location of the array |
---|
| 437 | |
---|
| 438 | <DT> <A HREF="calAllDet.html#Cal_BddMultiwayAnd" TARGET="MAIN"><CODE>Cal_BddMultiwayAnd()</CODE></A> |
---|
| 439 | <DD> Returns the BDD for logical AND of argument BDDs |
---|
| 440 | |
---|
| 441 | <DT> <A HREF="calAllDet.html#Cal_BddMultiwayOr" TARGET="MAIN"><CODE>Cal_BddMultiwayOr()</CODE></A> |
---|
| 442 | <DD> Returns the BDD for logical OR of argument BDDs |
---|
| 443 | |
---|
| 444 | <DT> <A HREF="calAllDet.html#Cal_BddMultiwayXor" TARGET="MAIN"><CODE>Cal_BddMultiwayXor()</CODE></A> |
---|
| 445 | <DD> Returns the BDD for logical XOR of argument BDDs |
---|
| 446 | |
---|
| 447 | <DT> <A HREF="calAllDet.html#CalRequestNodeListArrayOp" TARGET="MAIN"><CODE>CalRequestNodeListArrayOp()</CODE></A> |
---|
| 448 | <DD> Computes result BDDs for an array of lists, each entry of which |
---|
| 449 | is pair of pointers, each of which points to a operand BDD or an entry in |
---|
| 450 | another list with a smaller array index |
---|
| 451 | |
---|
| 452 | <DT> <A HREF="calAllDet.html#CalBddOpBF" TARGET="MAIN"><CODE>CalBddOpBF()</CODE></A> |
---|
| 453 | <DD> Internal routine to compute a logical operation on a pair of BDDs |
---|
| 454 | |
---|
| 455 | <DT> <A HREF="calAllDet.html#BddArrayOpBF" TARGET="MAIN"><CODE>BddArrayOpBF()</CODE></A> |
---|
| 456 | <DD> Internal common routine for Cal_BddPairwiseAnd and Cal_BddPairwiseOr |
---|
| 457 | |
---|
| 458 | <DT> <A HREF="calAllDet.html#BddMultiwayOp" TARGET="MAIN"><CODE>BddMultiwayOp()</CODE></A> |
---|
| 459 | <DD> Internal routine for multiway operations |
---|
| 460 | |
---|
| 461 | <DT> <A HREF="calAllDet.html#BddArrayToRequestNodeListArray" TARGET="MAIN"><CODE>BddArrayToRequestNodeListArray()</CODE></A> |
---|
| 462 | <DD> Converts an array of BDDs to a list of requests representing BDD |
---|
| 463 | pairs |
---|
| 464 | |
---|
| 465 | <DT> <A HREF="calAllDet.html#CeilLog2" TARGET="MAIN"><CODE>CeilLog2()</CODE></A> |
---|
| 466 | <DD> Returns the smallest integer greater than or equal to log2 of a |
---|
| 467 | number |
---|
| 468 | |
---|
| 469 | </DL> |
---|
| 470 | <HR> |
---|
| 471 | <A NAME="calBddReorderTest.c"><H1>calBddReorderTest.c</H1></A> |
---|
| 472 | A test routine for checking the functionality of |
---|
| 473 | dynamic reordering. <P> |
---|
| 474 | <B>By: Wilsin Gosti (wilsin@eecs.berkeley.edu) |
---|
| 475 | Rajeev Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 476 | Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)</B><P> |
---|
| 477 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 478 | <DL> |
---|
| 479 | <DT> <A HREF="calAllDet.html#main" TARGET="MAIN"><CODE>main()</CODE></A> |
---|
| 480 | <DD> required |
---|
| 481 | |
---|
| 482 | <DT> <A HREF="calAllDet.html#cpuTime" TARGET="MAIN"><CODE>cpuTime()</CODE></A> |
---|
| 483 | <DD> required |
---|
| 484 | |
---|
| 485 | <DT> <A HREF="calAllDet.html#elapsedTime" TARGET="MAIN"><CODE>elapsedTime()</CODE></A> |
---|
| 486 | <DD> Computes the time. |
---|
| 487 | |
---|
| 488 | </DL> |
---|
| 489 | <HR> |
---|
| 490 | <A NAME="calBddSatisfy.c"><H1>calBddSatisfy.c</H1></A> |
---|
| 491 | Routines for BDD satisfying valuation. <P> |
---|
| 492 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 493 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 494 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 495 | <DL> |
---|
| 496 | <DT> <A HREF="calAllDet.html#Cal_BddSatisfy" TARGET="MAIN"><CODE>Cal_BddSatisfy()</CODE></A> |
---|
| 497 | <DD> Returns a BDD which implies f, true for |
---|
| 498 | some valuation on which f is true, and which has at most |
---|
| 499 | one node at each level |
---|
| 500 | |
---|
| 501 | <DT> <A HREF="calAllDet.html#Cal_BddSatisfySupport" TARGET="MAIN"><CODE>Cal_BddSatisfySupport()</CODE></A> |
---|
| 502 | <DD> Returns a special cube contained in f. |
---|
| 503 | |
---|
| 504 | <DT> <A HREF="calAllDet.html#Cal_BddSatisfyingFraction" TARGET="MAIN"><CODE>Cal_BddSatisfyingFraction()</CODE></A> |
---|
| 505 | <DD> Returns the fraction of valuations which make f true. (Note that |
---|
| 506 | this fraction is independent of whatever set of variables f is supposed to be |
---|
| 507 | a function of) |
---|
| 508 | |
---|
| 509 | <DT> <A HREF="calAllDet.html#BddSatisfyStep" TARGET="MAIN"><CODE>BddSatisfyStep()</CODE></A> |
---|
| 510 | <DD> Returns a BDD which implies f, is true for some valuation |
---|
| 511 | on which f is true, and which has at most one node at each level |
---|
| 512 | |
---|
| 513 | <DT> <A HREF="calAllDet.html#BddSatisfySupportStep" TARGET="MAIN"><CODE>BddSatisfySupportStep()</CODE></A> |
---|
| 514 | <DD> |
---|
| 515 | |
---|
| 516 | <DT> <A HREF="calAllDet.html#IndexCmp" TARGET="MAIN"><CODE>IndexCmp()</CODE></A> |
---|
| 517 | <DD> |
---|
| 518 | |
---|
| 519 | <DT> <A HREF="calAllDet.html#BddSatisfyingFractionStep" TARGET="MAIN"><CODE>BddSatisfyingFractionStep()</CODE></A> |
---|
| 520 | <DD> |
---|
| 521 | |
---|
| 522 | </DL> |
---|
| 523 | <HR> |
---|
| 524 | <A NAME="calBddSize.c"><H1>calBddSize.c</H1></A> |
---|
| 525 | BDD size and profile routines <P> |
---|
| 526 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 527 | Rajeev Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 528 | Originally written by David Long.</B><P> |
---|
| 529 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 530 | <DL> |
---|
| 531 | <DT> <A HREF="calAllDet.html#Cal_BddSize" TARGET="MAIN"><CODE>Cal_BddSize()</CODE></A> |
---|
| 532 | <DD> Returns the number of nodes in f when negout is nonzero. If |
---|
| 533 | negout is zero, we pretend that the BDDs don't have negative-output pointers. |
---|
| 534 | |
---|
| 535 | <DT> <A HREF="calAllDet.html#Cal_BddSizeMultiple" TARGET="MAIN"><CODE>Cal_BddSizeMultiple()</CODE></A> |
---|
| 536 | <DD> The routine is like Cal_BddSize, but takes a null-terminated |
---|
| 537 | array of BDDs and accounts for sharing of nodes. |
---|
| 538 | |
---|
| 539 | <DT> <A HREF="calAllDet.html#Cal_BddProfile" TARGET="MAIN"><CODE>Cal_BddProfile()</CODE></A> |
---|
| 540 | <DD> Returns a "node profile" of f, i.e., the number of nodes at each |
---|
| 541 | level in f. |
---|
| 542 | |
---|
| 543 | <DT> <A HREF="calAllDet.html#Cal_BddProfileMultiple" TARGET="MAIN"><CODE>Cal_BddProfileMultiple()</CODE></A> |
---|
| 544 | <DD> |
---|
| 545 | |
---|
| 546 | <DT> <A HREF="calAllDet.html#Cal_BddFunctionProfile" TARGET="MAIN"><CODE>Cal_BddFunctionProfile()</CODE></A> |
---|
| 547 | <DD> Returns a "function profile" for f. |
---|
| 548 | |
---|
| 549 | <DT> <A HREF="calAllDet.html#Cal_BddFunctionProfileMultiple" TARGET="MAIN"><CODE>Cal_BddFunctionProfileMultiple()</CODE></A> |
---|
| 550 | <DD> Returns a "function profile" for fArray. |
---|
| 551 | |
---|
| 552 | <DT> <A HREF="calAllDet.html#BddMarkBdd" TARGET="MAIN"><CODE>BddMarkBdd()</CODE></A> |
---|
| 553 | <DD> |
---|
| 554 | |
---|
| 555 | <DT> <A HREF="calAllDet.html#BddCountNoNodes" TARGET="MAIN"><CODE>BddCountNoNodes()</CODE></A> |
---|
| 556 | <DD> |
---|
| 557 | |
---|
| 558 | <DT> <A HREF="calAllDet.html#BddCountNodes" TARGET="MAIN"><CODE>BddCountNodes()</CODE></A> |
---|
| 559 | <DD> |
---|
| 560 | |
---|
| 561 | <DT> <A HREF="calAllDet.html#BddSizeStep" TARGET="MAIN"><CODE>BddSizeStep()</CODE></A> |
---|
| 562 | <DD> |
---|
| 563 | |
---|
| 564 | <DT> <A HREF="calAllDet.html#BddProfileStep" TARGET="MAIN"><CODE>BddProfileStep()</CODE></A> |
---|
| 565 | <DD> |
---|
| 566 | |
---|
| 567 | <DT> <A HREF="calAllDet.html#BddHighestRefStep" TARGET="MAIN"><CODE>BddHighestRefStep()</CODE></A> |
---|
| 568 | <DD> |
---|
| 569 | |
---|
| 570 | <DT> <A HREF="calAllDet.html#BddDominatedStep" TARGET="MAIN"><CODE>BddDominatedStep()</CODE></A> |
---|
| 571 | <DD> |
---|
| 572 | |
---|
| 573 | </DL> |
---|
| 574 | <HR> |
---|
| 575 | <A NAME="calBddSubstitute.c"><H1>calBddSubstitute.c</H1></A> |
---|
| 576 | Routine for simultaneous substitution of an array of |
---|
| 577 | variables with an array of functions. <P> |
---|
| 578 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 579 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 580 | Routine for simultaneous substitution of an array of |
---|
| 581 | variables with an array of functions. <P> |
---|
| 582 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 583 | <DL> |
---|
| 584 | <DT> <A HREF="calAllDet.html#Cal_BddSubstitute" TARGET="MAIN"><CODE>Cal_BddSubstitute()</CODE></A> |
---|
| 585 | <DD> Substitute a set of variables by functions |
---|
| 586 | |
---|
| 587 | <DT> <A HREF="calAllDet.html#CalHashTableSubstituteApply" TARGET="MAIN"><CODE>CalHashTableSubstituteApply()</CODE></A> |
---|
| 588 | <DD> required |
---|
| 589 | |
---|
| 590 | <DT> <A HREF="calAllDet.html#CalHashTableSubstituteReduce" TARGET="MAIN"><CODE>CalHashTableSubstituteReduce()</CODE></A> |
---|
| 591 | <DD> required |
---|
| 592 | |
---|
| 593 | </DL> |
---|
| 594 | <HR> |
---|
| 595 | <A NAME="calBddSupport.c"><H1>calBddSupport.c</H1></A> |
---|
| 596 | Routines related to the support of a BDD. <P> |
---|
| 597 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 598 | Rajeev Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 599 | Originally written by David Long.</B><P> |
---|
| 600 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 601 | <DL> |
---|
| 602 | <DT> <A HREF="calAllDet.html#Cal_BddSupport" TARGET="MAIN"><CODE>Cal_BddSupport()</CODE></A> |
---|
| 603 | <DD> returns the support of f as a null-terminated array of variables |
---|
| 604 | |
---|
| 605 | <DT> <A HREF="calAllDet.html#Cal_BddDependsOn" TARGET="MAIN"><CODE>Cal_BddDependsOn()</CODE></A> |
---|
| 606 | <DD> Returns 1 if f depends on var and returns 0 otherwise. |
---|
| 607 | |
---|
| 608 | <DT> <A HREF="calAllDet.html#CalBddSupportStep" TARGET="MAIN"><CODE>CalBddSupportStep()</CODE></A> |
---|
| 609 | <DD> returns the support of f as a null-terminated array of variables |
---|
| 610 | |
---|
| 611 | <DT> <A HREF="calAllDet.html#CalBddUnmarkNodes" TARGET="MAIN"><CODE>CalBddUnmarkNodes()</CODE></A> |
---|
| 612 | <DD> recursively unmarks the nodes |
---|
| 613 | |
---|
| 614 | <DT> <A HREF="calAllDet.html#CalBddDependsOnStep" TARGET="MAIN"><CODE>CalBddDependsOnStep()</CODE></A> |
---|
| 615 | <DD> required |
---|
| 616 | |
---|
| 617 | </DL> |
---|
| 618 | <HR> |
---|
| 619 | <A NAME="calBddSwapVars.c"><H1>calBddSwapVars.c</H1></A> |
---|
| 620 | Routine for swapping two variables. <P> |
---|
| 621 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 622 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 623 | Routine for swapping two variables. <P> |
---|
| 624 | <P><B>See Also</B><A HREF="#None"><CODE>None</CODE></A> |
---|
| 625 | <DL> |
---|
| 626 | <DT> <A HREF="calAllDet.html#Cal_BddSwapVars" TARGET="MAIN"><CODE>Cal_BddSwapVars()</CODE></A> |
---|
| 627 | <DD> Return a function obtained by swapping two variables |
---|
| 628 | |
---|
| 629 | <DT> <A HREF="calAllDet.html#CalHashTableSwapVarsApply" TARGET="MAIN"><CODE>CalHashTableSwapVarsApply()</CODE></A> |
---|
| 630 | <DD> required |
---|
| 631 | |
---|
| 632 | <DT> <A HREF="calAllDet.html#CalHashTableSwapVarsPlusApply" TARGET="MAIN"><CODE>CalHashTableSwapVarsPlusApply()</CODE></A> |
---|
| 633 | <DD> required |
---|
| 634 | |
---|
| 635 | <DT> <A HREF="calAllDet.html#CalHashTableSwapVarsMinusApply" TARGET="MAIN"><CODE>CalHashTableSwapVarsMinusApply()</CODE></A> |
---|
| 636 | <DD> required |
---|
| 637 | |
---|
| 638 | </DL> |
---|
| 639 | <HR> |
---|
| 640 | <A NAME="calBddVarSubstitute.c"><H1>calBddVarSubstitute.c</H1></A> |
---|
| 641 | Routine for simultaneous substitution of an array of |
---|
| 642 | variables with another array of variables. <P> |
---|
| 643 | <B>By: Rajeev Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 644 | Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)</B><P> |
---|
| 645 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 646 | <DL> |
---|
| 647 | <DT> <A HREF="calAllDet.html#Cal_BddVarSubstitute" TARGET="MAIN"><CODE>Cal_BddVarSubstitute()</CODE></A> |
---|
| 648 | <DD> Substitute a set of variables by set of another variables. |
---|
| 649 | |
---|
| 650 | <DT> <A HREF="calAllDet.html#CalBddVarSubstitute" TARGET="MAIN"><CODE>CalBddVarSubstitute()</CODE></A> |
---|
| 651 | <DD> Substitute a set of variables by functions |
---|
| 652 | |
---|
| 653 | <DT> <A HREF="calAllDet.html#CalOpBddVarSubstitute" TARGET="MAIN"><CODE>CalOpBddVarSubstitute()</CODE></A> |
---|
| 654 | <DD> required |
---|
| 655 | |
---|
| 656 | <DT> <A HREF="calAllDet.html#CalHashTableSubstituteApply" TARGET="MAIN"><CODE>CalHashTableSubstituteApply()</CODE></A> |
---|
| 657 | <DD> required |
---|
| 658 | |
---|
| 659 | <DT> <A HREF="calAllDet.html#CalHashTableSubstituteReduce" TARGET="MAIN"><CODE>CalHashTableSubstituteReduce()</CODE></A> |
---|
| 660 | <DD> required |
---|
| 661 | |
---|
| 662 | </DL> |
---|
| 663 | <HR> |
---|
| 664 | <A NAME="calBlk.c"><H1>calBlk.c</H1></A> |
---|
| 665 | Routines for manipulating blocks of variables. <P> |
---|
| 666 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu). Modelled on the BDD package |
---|
| 667 | developed by David Long.</B><P> |
---|
| 668 | Routines for manipulating blocks of variables. <P> |
---|
| 669 | <DL> |
---|
| 670 | <DT> <A HREF="calAllDet.html#Cal_BddNewVarBlock" TARGET="MAIN"><CODE>Cal_BddNewVarBlock()</CODE></A> |
---|
| 671 | <DD> Creates and returns a variable block used for |
---|
| 672 | controlling dynamic reordering. |
---|
| 673 | |
---|
| 674 | <DT> <A HREF="calAllDet.html#Cal_BddVarBlockReorderable" TARGET="MAIN"><CODE>Cal_BddVarBlockReorderable()</CODE></A> |
---|
| 675 | <DD> Sets the reoderability of a particular block. |
---|
| 676 | |
---|
| 677 | <DT> <A HREF="calAllDet.html#CalBddFindBlock" TARGET="MAIN"><CODE>CalBddFindBlock()</CODE></A> |
---|
| 678 | <DD> required |
---|
| 679 | |
---|
| 680 | <DT> <A HREF="calAllDet.html#CalBddBlockDelta" TARGET="MAIN"><CODE>CalBddBlockDelta()</CODE></A> |
---|
| 681 | <DD> required |
---|
| 682 | |
---|
| 683 | <DT> <A HREF="calAllDet.html#CalBddShiftBlock" TARGET="MAIN"><CODE>CalBddShiftBlock()</CODE></A> |
---|
| 684 | <DD> required |
---|
| 685 | |
---|
| 686 | <DT> <A HREF="calAllDet.html#CalBlockMemoryConsumption" TARGET="MAIN"><CODE>CalBlockMemoryConsumption()</CODE></A> |
---|
| 687 | <DD> required |
---|
| 688 | |
---|
| 689 | <DT> <A HREF="calAllDet.html#CalFreeBlockRecursively" TARGET="MAIN"><CODE>CalFreeBlockRecursively()</CODE></A> |
---|
| 690 | <DD> required |
---|
| 691 | |
---|
| 692 | <DT> <A HREF="calAllDet.html#AddBlock" TARGET="MAIN"><CODE>AddBlock()</CODE></A> |
---|
| 693 | <DD> required |
---|
| 694 | |
---|
| 695 | </DL> |
---|
| 696 | <HR> |
---|
| 697 | <A NAME="calCacheTableTwo.c"><H1>calCacheTableTwo.c</H1></A> |
---|
| 698 | Functions to manage the Cache tables. <P> |
---|
| 699 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 700 | Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)</B><P> |
---|
| 701 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 702 | <DL> |
---|
| 703 | <DT> <A HREF="calAllDet.html#CalCacheTableTwoInit" TARGET="MAIN"><CODE>CalCacheTableTwoInit()</CODE></A> |
---|
| 704 | <DD> Initialize a Cache table using default parameters. |
---|
| 705 | |
---|
| 706 | <DT> <A HREF="calAllDet.html#CalCacheTableTwoQuit" TARGET="MAIN"><CODE>CalCacheTableTwoQuit()</CODE></A> |
---|
| 707 | <DD> Free a Cache table along with the associated storage. |
---|
| 708 | |
---|
| 709 | <DT> <A HREF="calAllDet.html#CalCacheTableTwoInsert" TARGET="MAIN"><CODE>CalCacheTableTwoInsert()</CODE></A> |
---|
| 710 | <DD> Directly insert a BDD node in the Cache table. |
---|
| 711 | |
---|
| 712 | <DT> <A HREF="calAllDet.html#CalCacheTableTwoLookup" TARGET="MAIN"><CODE>CalCacheTableTwoLookup()</CODE></A> |
---|
| 713 | <DD> required |
---|
| 714 | |
---|
| 715 | <DT> <A HREF="calAllDet.html#CalCacheTableTwoFlush" TARGET="MAIN"><CODE>CalCacheTableTwoFlush()</CODE></A> |
---|
| 716 | <DD> Free a Cache table along with the associated storage. |
---|
| 717 | |
---|
| 718 | <DT> <A HREF="calAllDet.html#CalCacheTableTwoFlushAll" TARGET="MAIN"><CODE>CalCacheTableTwoFlushAll()</CODE></A> |
---|
| 719 | <DD> Free a Cache table along with the associated storage. |
---|
| 720 | |
---|
| 721 | <DT> <A HREF="calAllDet.html#CalCacheTableTwoGCFlush" TARGET="MAIN"><CODE>CalCacheTableTwoGCFlush()</CODE></A> |
---|
| 722 | <DD> required |
---|
| 723 | |
---|
| 724 | <DT> <A HREF="calAllDet.html#CalCacheTableTwoRepackUpdate" TARGET="MAIN"><CODE>CalCacheTableTwoRepackUpdate()</CODE></A> |
---|
| 725 | <DD> required |
---|
| 726 | |
---|
| 727 | <DT> <A HREF="calAllDet.html#CalCheckCacheTableValidity" TARGET="MAIN"><CODE>CalCheckCacheTableValidity()</CODE></A> |
---|
| 728 | <DD> required |
---|
| 729 | |
---|
| 730 | <DT> <A HREF="calAllDet.html#CalCacheTableTwoFixResultPointers" TARGET="MAIN"><CODE>CalCacheTableTwoFixResultPointers()</CODE></A> |
---|
| 731 | <DD> required |
---|
| 732 | |
---|
| 733 | <DT> <A HREF="calAllDet.html#CalCacheTablePrint" TARGET="MAIN"><CODE>CalCacheTablePrint()</CODE></A> |
---|
| 734 | <DD> required |
---|
| 735 | |
---|
| 736 | <DT> <A HREF="calAllDet.html#CalBddManagerGetCacheTableData" TARGET="MAIN"><CODE>CalBddManagerGetCacheTableData()</CODE></A> |
---|
| 737 | <DD> required |
---|
| 738 | |
---|
| 739 | <DT> <A HREF="calAllDet.html#CalCacheTableRehash" TARGET="MAIN"><CODE>CalCacheTableRehash()</CODE></A> |
---|
| 740 | <DD> required |
---|
| 741 | |
---|
| 742 | <DT> <A HREF="calAllDet.html#CalCacheTableTwoFlushAssociationId" TARGET="MAIN"><CODE>CalCacheTableTwoFlushAssociationId()</CODE></A> |
---|
| 743 | <DD> Flushes the entries from the cache which |
---|
| 744 | correspond to the given associationId. |
---|
| 745 | |
---|
| 746 | <DT> <A HREF="calAllDet.html#CalCacheTableMemoryConsumption" TARGET="MAIN"><CODE>CalCacheTableMemoryConsumption()</CODE></A> |
---|
| 747 | <DD> required |
---|
| 748 | |
---|
| 749 | <DT> <A HREF="calAllDet.html#CacheTableTwoRehash" TARGET="MAIN"><CODE>CacheTableTwoRehash()</CODE></A> |
---|
| 750 | <DD> required |
---|
| 751 | |
---|
| 752 | <DT> <A HREF="calAllDet.html#CacheTablePrint" TARGET="MAIN"><CODE>CacheTablePrint()</CODE></A> |
---|
| 753 | <DD> required |
---|
| 754 | |
---|
| 755 | </DL> |
---|
| 756 | <HR> |
---|
| 757 | <A NAME="calDump.c"><H1>calDump.c</H1></A> |
---|
| 758 | BDD library dump/undump routines <P> |
---|
| 759 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 760 | Rajeev Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 761 | Originally written by David Long.</B><P> |
---|
| 762 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 763 | <DL> |
---|
| 764 | <DT> <A HREF="calAllDet.html#Cal_BddUndumpBdd" TARGET="MAIN"><CODE>Cal_BddUndumpBdd()</CODE></A> |
---|
| 765 | <DD> Reads a BDD from a file |
---|
| 766 | |
---|
| 767 | <DT> <A HREF="calAllDet.html#Cal_BddDumpBdd" TARGET="MAIN"><CODE>Cal_BddDumpBdd()</CODE></A> |
---|
| 768 | <DD> Write a BDD to a file |
---|
| 769 | |
---|
| 770 | <DT> <A HREF="calAllDet.html#Write" TARGET="MAIN"><CODE>Write()</CODE></A> |
---|
| 771 | <DD> |
---|
| 772 | |
---|
| 773 | <DT> <A HREF="calAllDet.html#BddDumpBddStep" TARGET="MAIN"><CODE>BddDumpBddStep()</CODE></A> |
---|
| 774 | <DD> |
---|
| 775 | |
---|
| 776 | <DT> <A HREF="calAllDet.html#Read" TARGET="MAIN"><CODE>Read()</CODE></A> |
---|
| 777 | <DD> |
---|
| 778 | |
---|
| 779 | <DT> <A HREF="calAllDet.html#BddUndumpBddStep" TARGET="MAIN"><CODE>BddUndumpBddStep()</CODE></A> |
---|
| 780 | <DD> |
---|
| 781 | |
---|
| 782 | <DT> <A HREF="calAllDet.html#BytesNeeded" TARGET="MAIN"><CODE>BytesNeeded()</CODE></A> |
---|
| 783 | <DD> |
---|
| 784 | |
---|
| 785 | </DL> |
---|
| 786 | <HR> |
---|
| 787 | <A NAME="calGC.c"><H1>calGC.c</H1></A> |
---|
| 788 | Garbage collection routines <P> |
---|
| 789 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 790 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 791 | optional <P> |
---|
| 792 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 793 | <DL> |
---|
| 794 | <DT> <A HREF="calAllDet.html#Cal_BddSetGCMode" TARGET="MAIN"><CODE>Cal_BddSetGCMode()</CODE></A> |
---|
| 795 | <DD> Sets the garbage collection mode, 0 means the garbage |
---|
| 796 | collection should be turned off, 1 means garbage collection should |
---|
| 797 | be on. |
---|
| 798 | |
---|
| 799 | <DT> <A HREF="calAllDet.html#Cal_BddManagerGC" TARGET="MAIN"><CODE>Cal_BddManagerGC()</CODE></A> |
---|
| 800 | <DD> Invokes the garbage collection at the manager level. |
---|
| 801 | |
---|
| 802 | <DT> <A HREF="calAllDet.html#Cal_BddManagerSetGCLimit" TARGET="MAIN"><CODE>Cal_BddManagerSetGCLimit()</CODE></A> |
---|
| 803 | <DD> Sets the limit of the garbage collection. |
---|
| 804 | |
---|
| 805 | <DT> <A HREF="calAllDet.html#CalBddManagerGCCheck" TARGET="MAIN"><CODE>CalBddManagerGCCheck()</CODE></A> |
---|
| 806 | <DD> required |
---|
| 807 | |
---|
| 808 | <DT> <A HREF="calAllDet.html#CalHashTableGC" TARGET="MAIN"><CODE>CalHashTableGC()</CODE></A> |
---|
| 809 | <DD> This function performs the garbage collection operation |
---|
| 810 | for a particular index. |
---|
| 811 | |
---|
| 812 | <DT> <A HREF="calAllDet.html#CalRepackNodesAfterGC" TARGET="MAIN"><CODE>CalRepackNodesAfterGC()</CODE></A> |
---|
| 813 | <DD> required |
---|
| 814 | |
---|
| 815 | <DT> <A HREF="calAllDet.html#CeilLog2" TARGET="MAIN"><CODE>CeilLog2()</CODE></A> |
---|
| 816 | <DD> Returns the smallest integer greater than or equal to log2 of a |
---|
| 817 | number |
---|
| 818 | |
---|
| 819 | </DL> |
---|
| 820 | <HR> |
---|
| 821 | <A NAME="calHashTable.c"><H1>calHashTable.c</H1></A> |
---|
| 822 | Functions to manage the hash tables that are a part of |
---|
| 823 | 1. unique table |
---|
| 824 | 2. request queue <P> |
---|
| 825 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 826 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 827 | <DL> |
---|
| 828 | <DT> <A HREF="calAllDet.html#CalHashTableInit" TARGET="MAIN"><CODE>CalHashTableInit()</CODE></A> |
---|
| 829 | <DD> Initialize a hash table using default parameters. |
---|
| 830 | |
---|
| 831 | <DT> <A HREF="calAllDet.html#CalHashTableQuit" TARGET="MAIN"><CODE>CalHashTableQuit()</CODE></A> |
---|
| 832 | <DD> Free a hash table along with the associated storage. |
---|
| 833 | |
---|
| 834 | <DT> <A HREF="calAllDet.html#CalHashTableAddDirect" TARGET="MAIN"><CODE>CalHashTableAddDirect()</CODE></A> |
---|
| 835 | <DD> Directly insert a BDD node in the hash table. |
---|
| 836 | |
---|
| 837 | <DT> <A HREF="calAllDet.html#CalHashTableFindOrAdd" TARGET="MAIN"><CODE>CalHashTableFindOrAdd()</CODE></A> |
---|
| 838 | <DD> required |
---|
| 839 | |
---|
| 840 | <DT> <A HREF="calAllDet.html#CalHashTableAddDirectAux" TARGET="MAIN"><CODE>CalHashTableAddDirectAux()</CODE></A> |
---|
| 841 | <DD> required |
---|
| 842 | |
---|
| 843 | <DT> <A HREF="calAllDet.html#CalHashTableCleanUp" TARGET="MAIN"><CODE>CalHashTableCleanUp()</CODE></A> |
---|
| 844 | <DD> required |
---|
| 845 | |
---|
| 846 | <DT> <A HREF="calAllDet.html#CalHashTableLookup" TARGET="MAIN"><CODE>CalHashTableLookup()</CODE></A> |
---|
| 847 | <DD> required |
---|
| 848 | |
---|
| 849 | <DT> <A HREF="calAllDet.html#CalHashTableDelete" TARGET="MAIN"><CODE>CalHashTableDelete()</CODE></A> |
---|
| 850 | <DD> Deletes a BDD node in the hash table. |
---|
| 851 | |
---|
| 852 | <DT> <A HREF="calAllDet.html#CalUniqueTableForIdLookup" TARGET="MAIN"><CODE>CalUniqueTableForIdLookup()</CODE></A> |
---|
| 853 | <DD> Lookup unique table for id. |
---|
| 854 | |
---|
| 855 | <DT> <A HREF="calAllDet.html#CalUniqueTableForIdFindOrAdd" TARGET="MAIN"><CODE>CalUniqueTableForIdFindOrAdd()</CODE></A> |
---|
| 856 | <DD> find or add in the unique table for id. |
---|
| 857 | |
---|
| 858 | <DT> <A HREF="calAllDet.html#CalHashTableRehash" TARGET="MAIN"><CODE>CalHashTableRehash()</CODE></A> |
---|
| 859 | <DD> required |
---|
| 860 | |
---|
| 861 | <DT> <A HREF="calAllDet.html#CalUniqueTableForIdRehashNode" TARGET="MAIN"><CODE>CalUniqueTableForIdRehashNode()</CODE></A> |
---|
| 862 | <DD> required |
---|
| 863 | |
---|
| 864 | <DT> <A HREF="calAllDet.html#CalBddUniqueTableNumLockedNodes" TARGET="MAIN"><CODE>CalBddUniqueTableNumLockedNodes()</CODE></A> |
---|
| 865 | <DD> required |
---|
| 866 | |
---|
| 867 | <DT> <A HREF="calAllDet.html#CalPackNodes" TARGET="MAIN"><CODE>CalPackNodes()</CODE></A> |
---|
| 868 | <DD> required |
---|
| 869 | |
---|
| 870 | <DT> <A HREF="calAllDet.html#CalBddPackNodesForSingleId" TARGET="MAIN"><CODE>CalBddPackNodesForSingleId()</CODE></A> |
---|
| 871 | <DD> required |
---|
| 872 | |
---|
| 873 | <DT> <A HREF="calAllDet.html#CalBddPackNodesAfterReorderForSingleId" TARGET="MAIN"><CODE>CalBddPackNodesAfterReorderForSingleId()</CODE></A> |
---|
| 874 | <DD> Packs the nodes if the variables which has just |
---|
| 875 | been sifted. |
---|
| 876 | |
---|
| 877 | <DT> <A HREF="calAllDet.html#CalBddPackNodesForMultipleIds" TARGET="MAIN"><CODE>CalBddPackNodesForMultipleIds()</CODE></A> |
---|
| 878 | <DD> required |
---|
| 879 | |
---|
| 880 | <DT> <A HREF="calAllDet.html#CeilLog2" TARGET="MAIN"><CODE>CeilLog2()</CODE></A> |
---|
| 881 | <DD> Returns the smallest integer greater than or equal to log2 of a |
---|
| 882 | number |
---|
| 883 | |
---|
| 884 | </DL> |
---|
| 885 | <HR> |
---|
| 886 | <A NAME="calHashTableOne.c"><H1>calHashTableOne.c</H1></A> |
---|
| 887 | Routines for managing hash table with Bdd is a key and |
---|
| 888 | int, long, or double as a value <P> |
---|
| 889 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 890 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 891 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 892 | <DL> |
---|
| 893 | <DT> <A HREF="calAllDet.html#CalHashTableOneInit" TARGET="MAIN"><CODE>CalHashTableOneInit()</CODE></A> |
---|
| 894 | <DD> Initialize a hash table using default parameters. |
---|
| 895 | |
---|
| 896 | <DT> <A HREF="calAllDet.html#CalHashTableOneQuit" TARGET="MAIN"><CODE>CalHashTableOneQuit()</CODE></A> |
---|
| 897 | <DD> Free a hash table along with the associated storage. |
---|
| 898 | |
---|
| 899 | <DT> <A HREF="calAllDet.html#CalHashTableOneInsert" TARGET="MAIN"><CODE>CalHashTableOneInsert()</CODE></A> |
---|
| 900 | <DD> Directly insert a BDD node in the hash table. |
---|
| 901 | |
---|
| 902 | <DT> <A HREF="calAllDet.html#CalHashTableOneLookup" TARGET="MAIN"><CODE>CalHashTableOneLookup()</CODE></A> |
---|
| 903 | <DD> required |
---|
| 904 | |
---|
| 905 | <DT> <A HREF="calAllDet.html#HashTableOneRehash" TARGET="MAIN"><CODE>HashTableOneRehash()</CODE></A> |
---|
| 906 | <DD> required |
---|
| 907 | |
---|
| 908 | </DL> |
---|
| 909 | <HR> |
---|
| 910 | <A NAME="calHashTableThree.c"><H1>calHashTableThree.c</H1></A> |
---|
| 911 | Functions to manage the hash tables that are a part of |
---|
| 912 | ITE operation <P> |
---|
| 913 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 914 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 915 | CalHashTableThreeFindOrAdd <P> |
---|
| 916 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 917 | <DL> |
---|
| 918 | <DT> <A HREF="calAllDet.html#CalHashTableThreeFindOrAdd" TARGET="MAIN"><CODE>CalHashTableThreeFindOrAdd()</CODE></A> |
---|
| 919 | <DD> required |
---|
| 920 | |
---|
| 921 | <DT> <A HREF="calAllDet.html#CalHashTableThreeRehash" TARGET="MAIN"><CODE>CalHashTableThreeRehash()</CODE></A> |
---|
| 922 | <DD> required |
---|
| 923 | |
---|
| 924 | </DL> |
---|
| 925 | <HR> |
---|
| 926 | <A NAME="calInteract.c"><H1>calInteract.c</H1></A> |
---|
| 927 | Functions to manipulate the variable interaction matrix. <P> |
---|
| 928 | <B>By: Original author:Fabio Somenzi. Modified for CAL package |
---|
| 929 | by Rajeev K. Ranjan</B><P> |
---|
| 930 | The interaction matrix tells whether two variables are |
---|
| 931 | both in the support of some function of the DD. The main use of the |
---|
| 932 | interaction matrix is in the in-place swapping. Indeed, if two |
---|
| 933 | variables do not interact, there is no arc connecting the two layers; |
---|
| 934 | therefore, the swap can be performed in constant time, without |
---|
| 935 | scanning the subtables. Another use of the interaction matrix is in |
---|
| 936 | the computation of the lower bounds for sifting. Finally, the |
---|
| 937 | interaction matrix can be used to speed up aggregation checks in |
---|
| 938 | symmetric and group sifting.<p> |
---|
| 939 | The computation of the interaction matrix is done with a series of |
---|
| 940 | depth-first searches. The searches start from those nodes that have |
---|
| 941 | only external references. The matrix is stored as a packed array of bits; |
---|
| 942 | since it is symmetric, only the upper triangle is kept in memory. |
---|
| 943 | As a final remark, we note that there may be variables that do |
---|
| 944 | intercat, but that for a given variable order have no arc connecting |
---|
| 945 | their layers when they are adjacent. <P> |
---|
| 946 | <DL> |
---|
| 947 | <DT> <A HREF="calAllDet.html#CalSetInteract" TARGET="MAIN"><CODE>CalSetInteract()</CODE></A> |
---|
| 948 | <DD> Set interaction matrix entries. |
---|
| 949 | |
---|
| 950 | <DT> <A HREF="calAllDet.html#CalTestInteract" TARGET="MAIN"><CODE>CalTestInteract()</CODE></A> |
---|
| 951 | <DD> Test interaction matrix entries. |
---|
| 952 | |
---|
| 953 | <DT> <A HREF="calAllDet.html#CalInitInteract" TARGET="MAIN"><CODE>CalInitInteract()</CODE></A> |
---|
| 954 | <DD> Initializes the interaction matrix. |
---|
| 955 | |
---|
| 956 | <DT> <A HREF="calAllDet.html#ddSuppInteract" TARGET="MAIN"><CODE>ddSuppInteract()</CODE></A> |
---|
| 957 | <DD> Find the support of f. |
---|
| 958 | |
---|
| 959 | <DT> <A HREF="calAllDet.html#ddClearLocal" TARGET="MAIN"><CODE>ddClearLocal()</CODE></A> |
---|
| 960 | <DD> Performs a DFS from f, clearing the LSB of the then pointers. |
---|
| 961 | |
---|
| 962 | <DT> <A HREF="calAllDet.html#ddUpdateInteract" TARGET="MAIN"><CODE>ddUpdateInteract()</CODE></A> |
---|
| 963 | <DD> Marks as interacting all pairs of variables that appear in |
---|
| 964 | support. |
---|
| 965 | |
---|
| 966 | </DL> |
---|
| 967 | <HR> |
---|
| 968 | <A NAME="calMem.c"><H1>calMem.c</H1></A> |
---|
| 969 | Routines for memory management. <P> |
---|
| 970 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu). Originally |
---|
| 971 | written by David Long.</B><P> |
---|
| 972 | Contains allocation, free, resize routines. Also has |
---|
| 973 | routines for managing records of fixed size. <P> |
---|
| 974 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 975 | <DL> |
---|
| 976 | <DT> <A HREF="calAllDet.html#Cal_MemFatal" TARGET="MAIN"><CODE>Cal_MemFatal()</CODE></A> |
---|
| 977 | <DD> Prints an error message and exits. |
---|
| 978 | |
---|
| 979 | <DT> <A HREF="calAllDet.html#Cal_MemAllocation" TARGET="MAIN"><CODE>Cal_MemAllocation()</CODE></A> |
---|
| 980 | <DD> Returns the memory allocated. |
---|
| 981 | |
---|
| 982 | <DT> <A HREF="calAllDet.html#Cal_MemGetBlock" TARGET="MAIN"><CODE>Cal_MemGetBlock()</CODE></A> |
---|
| 983 | <DD> Allocates a new block of the specified size. |
---|
| 984 | |
---|
| 985 | <DT> <A HREF="calAllDet.html#Cal_MemFreeBlock" TARGET="MAIN"><CODE>Cal_MemFreeBlock()</CODE></A> |
---|
| 986 | <DD> Frees the block. |
---|
| 987 | |
---|
| 988 | <DT> <A HREF="calAllDet.html#Cal_MemResizeBlock" TARGET="MAIN"><CODE>Cal_MemResizeBlock()</CODE></A> |
---|
| 989 | <DD> Expands or contracts the block to a new size. |
---|
| 990 | We try to avoid moving the block if possible. |
---|
| 991 | |
---|
| 992 | <DT> <A HREF="calAllDet.html#Cal_MemNewRec" TARGET="MAIN"><CODE>Cal_MemNewRec()</CODE></A> |
---|
| 993 | <DD> Allocates a record from the specified record manager. |
---|
| 994 | |
---|
| 995 | <DT> <A HREF="calAllDet.html#Cal_MemFreeRec" TARGET="MAIN"><CODE>Cal_MemFreeRec()</CODE></A> |
---|
| 996 | <DD> Frees a record managed by the indicated record manager. |
---|
| 997 | |
---|
| 998 | <DT> <A HREF="calAllDet.html#Cal_MemNewRecMgr" TARGET="MAIN"><CODE>Cal_MemNewRecMgr()</CODE></A> |
---|
| 999 | <DD> Creates a new record manager with the given record size. |
---|
| 1000 | |
---|
| 1001 | <DT> <A HREF="calAllDet.html#Cal_MemFreeRecMgr" TARGET="MAIN"><CODE>Cal_MemFreeRecMgr()</CODE></A> |
---|
| 1002 | <DD> Frees all the storage associated with the specified record manager. |
---|
| 1003 | |
---|
| 1004 | <DT> <A HREF="calAllDet.html#CeilingLog2" TARGET="MAIN"><CODE>CeilingLog2()</CODE></A> |
---|
| 1005 | <DD> required |
---|
| 1006 | |
---|
| 1007 | <DT> <A HREF="calAllDet.html#BlockSizeIndex" TARGET="MAIN"><CODE>BlockSizeIndex()</CODE></A> |
---|
| 1008 | <DD> required |
---|
| 1009 | |
---|
| 1010 | <DT> <A HREF="calAllDet.html#AddToFreeList" TARGET="MAIN"><CODE>AddToFreeList()</CODE></A> |
---|
| 1011 | <DD> required |
---|
| 1012 | |
---|
| 1013 | <DT> <A HREF="calAllDet.html#RemoveFromFreeList" TARGET="MAIN"><CODE>RemoveFromFreeList()</CODE></A> |
---|
| 1014 | <DD> required |
---|
| 1015 | |
---|
| 1016 | <DT> <A HREF="calAllDet.html#Buddy" TARGET="MAIN"><CODE>Buddy()</CODE></A> |
---|
| 1017 | <DD> required |
---|
| 1018 | |
---|
| 1019 | <DT> <A HREF="calAllDet.html#TrimToSize" TARGET="MAIN"><CODE>TrimToSize()</CODE></A> |
---|
| 1020 | <DD> required |
---|
| 1021 | |
---|
| 1022 | <DT> <A HREF="calAllDet.html#MergeAndFree" TARGET="MAIN"><CODE>MergeAndFree()</CODE></A> |
---|
| 1023 | <DD> required |
---|
| 1024 | |
---|
| 1025 | </DL> |
---|
| 1026 | <HR> |
---|
| 1027 | <A NAME="calMemoryManagement.c"><H1>calMemoryManagement.c</H1></A> |
---|
| 1028 | Special memory management routines specific to CAL. <P> |
---|
| 1029 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 1030 | Rajeev Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 1031 | Functions for managing the system memory using a set of |
---|
| 1032 | nodeManagers. Each nodeManager manages a set of fixed size |
---|
| 1033 | nodes obtained from a set of pages. When additional memory |
---|
| 1034 | is required, nodeManager obtains a new page from the pageManager. |
---|
| 1035 | The new page is divided into ( PAGE_SIZE/NODE_SIZE ) number of |
---|
| 1036 | nodes. <P> |
---|
| 1037 | <DL> |
---|
| 1038 | <DT> <A HREF="calAllDet.html#CalPageManagerInit" TARGET="MAIN"><CODE>CalPageManagerInit()</CODE></A> |
---|
| 1039 | <DD> Initializes a pageManager. |
---|
| 1040 | |
---|
| 1041 | <DT> <A HREF="calAllDet.html#CalPageManagerQuit" TARGET="MAIN"><CODE>CalPageManagerQuit()</CODE></A> |
---|
| 1042 | <DD> Frees pageManager and associated pages. |
---|
| 1043 | |
---|
| 1044 | <DT> <A HREF="calAllDet.html#CalPageManagerPrint" TARGET="MAIN"><CODE>CalPageManagerPrint()</CODE></A> |
---|
| 1045 | <DD> Prints address of each memory segment and address of each page. |
---|
| 1046 | |
---|
| 1047 | <DT> <A HREF="calAllDet.html#CalNodeManagerInit" TARGET="MAIN"><CODE>CalNodeManagerInit()</CODE></A> |
---|
| 1048 | <DD> Initializes a node manager. |
---|
| 1049 | |
---|
| 1050 | <DT> <A HREF="calAllDet.html#CalNodeManagerQuit" TARGET="MAIN"><CODE>CalNodeManagerQuit()</CODE></A> |
---|
| 1051 | <DD> Frees a node manager. |
---|
| 1052 | |
---|
| 1053 | <DT> <A HREF="calAllDet.html#CalNodeManagerPrint" TARGET="MAIN"><CODE>CalNodeManagerPrint()</CODE></A> |
---|
| 1054 | <DD> Prints address of each free node. |
---|
| 1055 | |
---|
| 1056 | <DT> <A HREF="calAllDet.html#CalPageManagerAllocPage" TARGET="MAIN"><CODE>CalPageManagerAllocPage()</CODE></A> |
---|
| 1057 | <DD> Allocs a new page. |
---|
| 1058 | |
---|
| 1059 | <DT> <A HREF="calAllDet.html#CalPageManagerFreePage" TARGET="MAIN"><CODE>CalPageManagerFreePage()</CODE></A> |
---|
| 1060 | <DD> Free a page. |
---|
| 1061 | |
---|
| 1062 | <DT> <A HREF="calAllDet.html#PageManagerExpandStorage" TARGET="MAIN"><CODE>PageManagerExpandStorage()</CODE></A> |
---|
| 1063 | <DD> Allocates a segment of memory to expand the storage managed by |
---|
| 1064 | pageManager. The allocated segment is divided into free pages |
---|
| 1065 | which are linked as a freePageList. |
---|
| 1066 | |
---|
| 1067 | <DT> <A HREF="calAllDet.html#PageAlign" TARGET="MAIN"><CODE>PageAlign()</CODE></A> |
---|
| 1068 | <DD> Return page aligned address greater than or equal to |
---|
| 1069 | the pointer. |
---|
| 1070 | |
---|
| 1071 | <DT> <A HREF="calAllDet.html#SegmentToPageList" TARGET="MAIN"><CODE>SegmentToPageList()</CODE></A> |
---|
| 1072 | <DD> Converts a memory segment into a linked list of pages. |
---|
| 1073 | if p is a pointer to a page, *p contains address of the next page |
---|
| 1074 | if p is a pointer to the last page, *p contains lastPointer. |
---|
| 1075 | |
---|
| 1076 | </DL> |
---|
| 1077 | <HR> |
---|
| 1078 | <A NAME="calPerformanceTest.c"><H1>calPerformanceTest.c</H1></A> |
---|
| 1079 | This file contains the performance test routines for |
---|
| 1080 | the CAL package. <P> |
---|
| 1081 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 1082 | Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)</B><P> |
---|
| 1083 | optional <P> |
---|
| 1084 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 1085 | <DL> |
---|
| 1086 | <DT> <A HREF="calAllDet.html#Cal_PerformanceTest" TARGET="MAIN"><CODE>Cal_PerformanceTest()</CODE></A> |
---|
| 1087 | <DD> Main routine for testing performances of various routines. |
---|
| 1088 | |
---|
| 1089 | <DT> <A HREF="calAllDet.html#CalIncreasingOrderCompare" TARGET="MAIN"><CODE>CalIncreasingOrderCompare()</CODE></A> |
---|
| 1090 | <DD> required |
---|
| 1091 | |
---|
| 1092 | <DT> <A HREF="calAllDet.html#CalDecreasingOrderCompare" TARGET="MAIN"><CODE>CalDecreasingOrderCompare()</CODE></A> |
---|
| 1093 | <DD> required |
---|
| 1094 | |
---|
| 1095 | <DT> <A HREF="calAllDet.html#CalPerformanceTestAnd" TARGET="MAIN"><CODE>CalPerformanceTestAnd()</CODE></A> |
---|
| 1096 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1097 | time). |
---|
| 1098 | |
---|
| 1099 | <DT> <A HREF="calAllDet.html#CalPerformanceMemoryOverhead" TARGET="MAIN"><CODE>CalPerformanceMemoryOverhead()</CODE></A> |
---|
| 1100 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1101 | time). |
---|
| 1102 | |
---|
| 1103 | <DT> <A HREF="calAllDet.html#CalPerformaceTestSuperscalar" TARGET="MAIN"><CODE>CalPerformaceTestSuperscalar()</CODE></A> |
---|
| 1104 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1105 | time). |
---|
| 1106 | |
---|
| 1107 | <DT> <A HREF="calAllDet.html#CalPerformanceTestNonSuperscalar" TARGET="MAIN"><CODE>CalPerformanceTestNonSuperscalar()</CODE></A> |
---|
| 1108 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1109 | time). |
---|
| 1110 | |
---|
| 1111 | <DT> <A HREF="calAllDet.html#CalPerformanceTestMultiway" TARGET="MAIN"><CODE>CalPerformanceTestMultiway()</CODE></A> |
---|
| 1112 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1113 | time). |
---|
| 1114 | |
---|
| 1115 | <DT> <A HREF="calAllDet.html#CalPerformanceTestOneway" TARGET="MAIN"><CODE>CalPerformanceTestOneway()</CODE></A> |
---|
| 1116 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1117 | time). |
---|
| 1118 | |
---|
| 1119 | <DT> <A HREF="calAllDet.html#CalPerformanceTestCompose" TARGET="MAIN"><CODE>CalPerformanceTestCompose()</CODE></A> |
---|
| 1120 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1121 | time). |
---|
| 1122 | |
---|
| 1123 | <DT> <A HREF="calAllDet.html#CalPerformanceTestQuantifyAllTogether" TARGET="MAIN"><CODE>CalPerformanceTestQuantifyAllTogether()</CODE></A> |
---|
| 1124 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1125 | time). |
---|
| 1126 | |
---|
| 1127 | <DT> <A HREF="calAllDet.html#CalQuantifySanityCheck" TARGET="MAIN"><CODE>CalQuantifySanityCheck()</CODE></A> |
---|
| 1128 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1129 | time). |
---|
| 1130 | |
---|
| 1131 | <DT> <A HREF="calAllDet.html#CalPerformanceTestRelProd" TARGET="MAIN"><CODE>CalPerformanceTestRelProd()</CODE></A> |
---|
| 1132 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1133 | time). |
---|
| 1134 | |
---|
| 1135 | <DT> <A HREF="calAllDet.html#CalPerformanceTestSubstitute" TARGET="MAIN"><CODE>CalPerformanceTestSubstitute()</CODE></A> |
---|
| 1136 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1137 | time). |
---|
| 1138 | |
---|
| 1139 | <DT> <A HREF="calAllDet.html#CalPerformanceTestSwapVars" TARGET="MAIN"><CODE>CalPerformanceTestSwapVars()</CODE></A> |
---|
| 1140 | <DD> Performance test routine for quantify (all variables at the same |
---|
| 1141 | time). |
---|
| 1142 | |
---|
| 1143 | <DT> <A HREF="calAllDet.html#elapsedTime" TARGET="MAIN"><CODE>elapsedTime()</CODE></A> |
---|
| 1144 | <DD> Computes the time. |
---|
| 1145 | |
---|
| 1146 | <DT> <A HREF="calAllDet.html#cpuTime" TARGET="MAIN"><CODE>cpuTime()</CODE></A> |
---|
| 1147 | <DD> Computes the number of page faults. |
---|
| 1148 | |
---|
| 1149 | <DT> <A HREF="calAllDet.html#pageFaults" TARGET="MAIN"><CODE>pageFaults()</CODE></A> |
---|
| 1150 | <DD> Computes the number of page faults. |
---|
| 1151 | |
---|
| 1152 | <DT> <A HREF="calAllDet.html#GetRandomNumbers" TARGET="MAIN"><CODE>GetRandomNumbers()</CODE></A> |
---|
| 1153 | <DD> Generates "count" many random numbers ranging between |
---|
| 1154 | "lowerBound" and "upperBound". |
---|
| 1155 | |
---|
| 1156 | </DL> |
---|
| 1157 | <HR> |
---|
| 1158 | <A NAME="calPipeline.c"><H1>calPipeline.c</H1></A> |
---|
| 1159 | Routines for creating and managing the pipelined BDD |
---|
| 1160 | operations. <P> |
---|
| 1161 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 1162 | Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)</B><P> |
---|
| 1163 | Eventually we would like to have this feature |
---|
| 1164 | transparent to the user. <P> |
---|
| 1165 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 1166 | <DL> |
---|
| 1167 | <DT> <A HREF="calAllDet.html#Cal_PipelineSetDepth" TARGET="MAIN"><CODE>Cal_PipelineSetDepth()</CODE></A> |
---|
| 1168 | <DD> Set depth of a BDD pipeline. |
---|
| 1169 | |
---|
| 1170 | <DT> <A HREF="calAllDet.html#Cal_PipelineInit" TARGET="MAIN"><CODE>Cal_PipelineInit()</CODE></A> |
---|
| 1171 | <DD> Initialize a BDD pipeline. |
---|
| 1172 | |
---|
| 1173 | <DT> <A HREF="calAllDet.html#Cal_PipelineCreateProvisionalBdd" TARGET="MAIN"><CODE>Cal_PipelineCreateProvisionalBdd()</CODE></A> |
---|
| 1174 | <DD> Create a provisional BDD in the pipeline. |
---|
| 1175 | |
---|
| 1176 | <DT> <A HREF="calAllDet.html#Cal_PipelineExecute" TARGET="MAIN"><CODE>Cal_PipelineExecute()</CODE></A> |
---|
| 1177 | <DD> Executes a pipeline. |
---|
| 1178 | |
---|
| 1179 | <DT> <A HREF="calAllDet.html#Cal_PipelineUpdateProvisionalBdd" TARGET="MAIN"><CODE>Cal_PipelineUpdateProvisionalBdd()</CODE></A> |
---|
| 1180 | <DD> Update a provisional Bdd obtained during pipelining. |
---|
| 1181 | |
---|
| 1182 | <DT> <A HREF="calAllDet.html#Cal_BddIsProvisional" TARGET="MAIN"><CODE>Cal_BddIsProvisional()</CODE></A> |
---|
| 1183 | <DD> Returns 1, if the given user BDD contains |
---|
| 1184 | provisional BDD node. |
---|
| 1185 | |
---|
| 1186 | <DT> <A HREF="calAllDet.html#Cal_PipelineQuit" TARGET="MAIN"><CODE>Cal_PipelineQuit()</CODE></A> |
---|
| 1187 | <DD> Resets the pipeline freeing all resources. |
---|
| 1188 | |
---|
| 1189 | <DT> <A HREF="calAllDet.html#CalBddReorderFixProvisionalNodes" TARGET="MAIN"><CODE>CalBddReorderFixProvisionalNodes()</CODE></A> |
---|
| 1190 | <DD> required |
---|
| 1191 | |
---|
| 1192 | <DT> <A HREF="calAllDet.html#CalCheckPipelineValidity" TARGET="MAIN"><CODE>CalCheckPipelineValidity()</CODE></A> |
---|
| 1193 | <DD> required |
---|
| 1194 | |
---|
| 1195 | </DL> |
---|
| 1196 | <HR> |
---|
| 1197 | <A NAME="calPrint.c"><H1>calPrint.c</H1></A> |
---|
| 1198 | Routine for printing a BDD. <P> |
---|
| 1199 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and |
---|
| 1200 | Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 1201 | Originally written by David Long.</B><P> |
---|
| 1202 | <P><B>See Also</B><A HREF="#None"><CODE>None</CODE></A> |
---|
| 1203 | <DL> |
---|
| 1204 | <DT> <A HREF="calAllDet.html#Cal_BddPrintBdd" TARGET="MAIN"><CODE>Cal_BddPrintBdd()</CODE></A> |
---|
| 1205 | <DD> Prints a BDD in the human readable form. |
---|
| 1206 | |
---|
| 1207 | <DT> <A HREF="calAllDet.html#CalBddVarName" TARGET="MAIN"><CODE>CalBddVarName()</CODE></A> |
---|
| 1208 | <DD> required |
---|
| 1209 | |
---|
| 1210 | <DT> <A HREF="calAllDet.html#CalBddNumberSharedNodes" TARGET="MAIN"><CODE>CalBddNumberSharedNodes()</CODE></A> |
---|
| 1211 | <DD> required |
---|
| 1212 | |
---|
| 1213 | <DT> <A HREF="calAllDet.html#CalBddMarkSharedNodes" TARGET="MAIN"><CODE>CalBddMarkSharedNodes()</CODE></A> |
---|
| 1214 | <DD> required |
---|
| 1215 | |
---|
| 1216 | <DT> <A HREF="calAllDet.html#Chars" TARGET="MAIN"><CODE>Chars()</CODE></A> |
---|
| 1217 | <DD> required |
---|
| 1218 | |
---|
| 1219 | <DT> <A HREF="calAllDet.html#BddPrintTopVar" TARGET="MAIN"><CODE>BddPrintTopVar()</CODE></A> |
---|
| 1220 | <DD> required |
---|
| 1221 | |
---|
| 1222 | <DT> <A HREF="calAllDet.html#BddPrintBddStep" TARGET="MAIN"><CODE>BddPrintBddStep()</CODE></A> |
---|
| 1223 | <DD> required |
---|
| 1224 | |
---|
| 1225 | <DT> <A HREF="calAllDet.html#BddTerminalId" TARGET="MAIN"><CODE>BddTerminalId()</CODE></A> |
---|
| 1226 | <DD> required |
---|
| 1227 | |
---|
| 1228 | <DT> <A HREF="calAllDet.html#BddTerminalValueAux" TARGET="MAIN"><CODE>BddTerminalValueAux()</CODE></A> |
---|
| 1229 | <DD> required |
---|
| 1230 | |
---|
| 1231 | </DL> |
---|
| 1232 | <HR> |
---|
| 1233 | <A NAME="calPrintProfile.c"><H1>calPrintProfile.c</H1></A> |
---|
| 1234 | Routines for printing various profiles for a BDD. <P> |
---|
| 1235 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 1236 | Rajeev Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 1237 | Originally written by David Long.</B><P> |
---|
| 1238 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 1239 | <DL> |
---|
| 1240 | <DT> <A HREF="calAllDet.html#Cal_BddPrintProfile" TARGET="MAIN"><CODE>Cal_BddPrintProfile()</CODE></A> |
---|
| 1241 | <DD> Displays the node profile for f on fp. lineLength specifies |
---|
| 1242 | the maximum line length. varNamingFn is as in |
---|
| 1243 | Cal_BddPrintBdd. |
---|
| 1244 | |
---|
| 1245 | <DT> <A HREF="calAllDet.html#Cal_BddPrintProfileMultiple" TARGET="MAIN"><CODE>Cal_BddPrintProfileMultiple()</CODE></A> |
---|
| 1246 | <DD> Cal_BddPrintProfileMultiple is like Cal_BddPrintProfile except |
---|
| 1247 | it displays the profile for a set of BDDs |
---|
| 1248 | |
---|
| 1249 | <DT> <A HREF="calAllDet.html#Cal_BddPrintFunctionProfile" TARGET="MAIN"><CODE>Cal_BddPrintFunctionProfile()</CODE></A> |
---|
| 1250 | <DD> Cal_BddPrintFunctionProfile is like Cal_BddPrintProfile except |
---|
| 1251 | it displays a function profile for f |
---|
| 1252 | |
---|
| 1253 | <DT> <A HREF="calAllDet.html#Cal_BddPrintFunctionProfileMultiple" TARGET="MAIN"><CODE>Cal_BddPrintFunctionProfileMultiple()</CODE></A> |
---|
| 1254 | <DD> Cal_BddPrintFunctionProfileMultiple is like |
---|
| 1255 | Cal_BddPrintFunctionProfile except for multiple BDDs |
---|
| 1256 | |
---|
| 1257 | <DT> <A HREF="calAllDet.html#CalBddPrintProfileAux" TARGET="MAIN"><CODE>CalBddPrintProfileAux()</CODE></A> |
---|
| 1258 | <DD> Prints a profile to the file given by fp. The varNamingProc |
---|
| 1259 | is as in Cal_BddPrintBdd. lineLength gives the line width to scale |
---|
| 1260 | the profile to. |
---|
| 1261 | |
---|
| 1262 | <DT> <A HREF="calAllDet.html#chars" TARGET="MAIN"><CODE>chars()</CODE></A> |
---|
| 1263 | <DD> |
---|
| 1264 | |
---|
| 1265 | </DL> |
---|
| 1266 | <HR> |
---|
| 1267 | <A NAME="calQuant.c"><H1>calQuant.c</H1></A> |
---|
| 1268 | Routines for existential/universal quantification and |
---|
| 1269 | relational product. <P> |
---|
| 1270 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and |
---|
| 1271 | Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu)</B><P> |
---|
| 1272 | <P><B>See Also</B><A HREF="#None"><CODE>None</CODE></A> |
---|
| 1273 | <DL> |
---|
| 1274 | <DT> <A HREF="calAllDet.html#Cal_BddExists" TARGET="MAIN"><CODE>Cal_BddExists()</CODE></A> |
---|
| 1275 | <DD> Returns the result of existentially quantifying some |
---|
| 1276 | variables from the given BDD. |
---|
| 1277 | |
---|
| 1278 | <DT> <A HREF="calAllDet.html#Cal_BddRelProd" TARGET="MAIN"><CODE>Cal_BddRelProd()</CODE></A> |
---|
| 1279 | <DD> Returns the result of taking the logical AND of the |
---|
| 1280 | argument BDDs and existentially quantifying some variables from the |
---|
| 1281 | product. |
---|
| 1282 | |
---|
| 1283 | <DT> <A HREF="calAllDet.html#Cal_BddForAll" TARGET="MAIN"><CODE>Cal_BddForAll()</CODE></A> |
---|
| 1284 | <DD> Returns the result of universally quantifying some |
---|
| 1285 | variables from the given BDD. |
---|
| 1286 | |
---|
| 1287 | <DT> <A HREF="calAllDet.html#CalOpExists" TARGET="MAIN"><CODE>CalOpExists()</CODE></A> |
---|
| 1288 | <DD> required |
---|
| 1289 | |
---|
| 1290 | <DT> <A HREF="calAllDet.html#CalOpRelProd" TARGET="MAIN"><CODE>CalOpRelProd()</CODE></A> |
---|
| 1291 | <DD> required |
---|
| 1292 | |
---|
| 1293 | <DT> <A HREF="calAllDet.html#BddExistsStep" TARGET="MAIN"><CODE>BddExistsStep()</CODE></A> |
---|
| 1294 | <DD> required |
---|
| 1295 | |
---|
| 1296 | <DT> <A HREF="calAllDet.html#BddRelProdStep" TARGET="MAIN"><CODE>BddRelProdStep()</CODE></A> |
---|
| 1297 | <DD> required |
---|
| 1298 | |
---|
| 1299 | <DT> <A HREF="calAllDet.html#BddDFStep" TARGET="MAIN"><CODE>BddDFStep()</CODE></A> |
---|
| 1300 | <DD> required |
---|
| 1301 | |
---|
| 1302 | <DT> <A HREF="calAllDet.html#HashTableApply" TARGET="MAIN"><CODE>HashTableApply()</CODE></A> |
---|
| 1303 | <DD> required |
---|
| 1304 | |
---|
| 1305 | <DT> <A HREF="calAllDet.html#HashTableReduce" TARGET="MAIN"><CODE>HashTableReduce()</CODE></A> |
---|
| 1306 | <DD> required |
---|
| 1307 | |
---|
| 1308 | <DT> <A HREF="calAllDet.html#BddExistsApply" TARGET="MAIN"><CODE>BddExistsApply()</CODE></A> |
---|
| 1309 | <DD> required |
---|
| 1310 | |
---|
| 1311 | <DT> <A HREF="calAllDet.html#BddExistsBFAux" TARGET="MAIN"><CODE>BddExistsBFAux()</CODE></A> |
---|
| 1312 | <DD> required |
---|
| 1313 | |
---|
| 1314 | <DT> <A HREF="calAllDet.html#BddExistsReduce" TARGET="MAIN"><CODE>BddExistsReduce()</CODE></A> |
---|
| 1315 | <DD> required |
---|
| 1316 | |
---|
| 1317 | <DT> <A HREF="calAllDet.html#BddExistsBFPlusDF" TARGET="MAIN"><CODE>BddExistsBFPlusDF()</CODE></A> |
---|
| 1318 | <DD> required |
---|
| 1319 | |
---|
| 1320 | <DT> <A HREF="calAllDet.html#BddRelProdApply" TARGET="MAIN"><CODE>BddRelProdApply()</CODE></A> |
---|
| 1321 | <DD> required |
---|
| 1322 | |
---|
| 1323 | <DT> <A HREF="calAllDet.html#BddRelProdReduce" TARGET="MAIN"><CODE>BddRelProdReduce()</CODE></A> |
---|
| 1324 | <DD> required |
---|
| 1325 | |
---|
| 1326 | <DT> <A HREF="calAllDet.html#BddRelProdBFAux" TARGET="MAIN"><CODE>BddRelProdBFAux()</CODE></A> |
---|
| 1327 | <DD> required |
---|
| 1328 | |
---|
| 1329 | <DT> <A HREF="calAllDet.html#BddRelProdBFPlusDF" TARGET="MAIN"><CODE>BddRelProdBFPlusDF()</CODE></A> |
---|
| 1330 | <DD> required |
---|
| 1331 | |
---|
| 1332 | </DL> |
---|
| 1333 | <HR> |
---|
| 1334 | <A NAME="calReduce.c"><H1>calReduce.c</H1></A> |
---|
| 1335 | Routines for optimizing a BDD with respect to a don't |
---|
| 1336 | care set (cofactor and restrict). <P> |
---|
| 1337 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and |
---|
| 1338 | Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu</B><P> |
---|
| 1339 | <P><B>See Also</B><A HREF="#None"><CODE>None</CODE></A> |
---|
| 1340 | <DL> |
---|
| 1341 | <DT> <A HREF="calAllDet.html#Cal_BddCofactor" TARGET="MAIN"><CODE>Cal_BddCofactor()</CODE></A> |
---|
| 1342 | <DD> Returns the generalized cofactor of BDD f with respect |
---|
| 1343 | to BDD c. |
---|
| 1344 | |
---|
| 1345 | <DT> <A HREF="calAllDet.html#Cal_BddReduce" TARGET="MAIN"><CODE>Cal_BddReduce()</CODE></A> |
---|
| 1346 | <DD> Returns a BDD which agrees with f for all valuations |
---|
| 1347 | which satisfy c. |
---|
| 1348 | |
---|
| 1349 | <DT> <A HREF="calAllDet.html#Cal_BddBetween" TARGET="MAIN"><CODE>Cal_BddBetween()</CODE></A> |
---|
| 1350 | <DD> Returns a minimal BDD whose function contains fMin and is |
---|
| 1351 | contained in fMax. |
---|
| 1352 | |
---|
| 1353 | <DT> <A HREF="calAllDet.html#CalOpCofactor" TARGET="MAIN"><CODE>CalOpCofactor()</CODE></A> |
---|
| 1354 | <DD> required |
---|
| 1355 | |
---|
| 1356 | <DT> <A HREF="calAllDet.html#BddReduceBF" TARGET="MAIN"><CODE>BddReduceBF()</CODE></A> |
---|
| 1357 | <DD> required |
---|
| 1358 | |
---|
| 1359 | <DT> <A HREF="calAllDet.html#BddCofactorBF" TARGET="MAIN"><CODE>BddCofactorBF()</CODE></A> |
---|
| 1360 | <DD> required |
---|
| 1361 | |
---|
| 1362 | <DT> <A HREF="calAllDet.html#HashTableReduceApply" TARGET="MAIN"><CODE>HashTableReduceApply()</CODE></A> |
---|
| 1363 | <DD> required |
---|
| 1364 | |
---|
| 1365 | <DT> <A HREF="calAllDet.html#HashTableCofactorApply" TARGET="MAIN"><CODE>HashTableCofactorApply()</CODE></A> |
---|
| 1366 | <DD> required |
---|
| 1367 | |
---|
| 1368 | <DT> <A HREF="calAllDet.html#HashTableCofactorReduce" TARGET="MAIN"><CODE>HashTableCofactorReduce()</CODE></A> |
---|
| 1369 | <DD> required |
---|
| 1370 | |
---|
| 1371 | </DL> |
---|
| 1372 | <HR> |
---|
| 1373 | <A NAME="calReorderBF.c"><H1>calReorderBF.c</H1></A> |
---|
| 1374 | Routines for dynamic reordering of variables. <P> |
---|
| 1375 | <B>By: Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu) |
---|
| 1376 | Wilsin Gosti (wilsin@ic.eecs.berkeley.edu)</B><P> |
---|
| 1377 | This method dynamically reorders variables while |
---|
| 1378 | preserving their locality. This entails both memory and |
---|
| 1379 | computational overheads. Conceptually and experimentally it has |
---|
| 1380 | been observed that these overheads lead to poorer performance |
---|
| 1381 | compared to the traditional reordering methods. For details, please |
---|
| 1382 | refer to the work by Rajeev K. Ranjan et al - "Dynamic variable |
---|
| 1383 | reordering in a breadth-first manipulation based package: Challenges |
---|
| 1384 | and Solutions"- Proceedings of ICCD'97. <P> |
---|
| 1385 | <P><B>See Also</B><A HREF="#calReorderDF.c"><CODE>calReorderDF.c</CODE></A> |
---|
| 1386 | <A HREF="#calReorderUtil.c"><CODE>calReorderUtil.c</CODE></A> |
---|
| 1387 | <DL> |
---|
| 1388 | <DT> <A HREF="calAllDet.html#CalBddReorderAuxBF" TARGET="MAIN"><CODE>CalBddReorderAuxBF()</CODE></A> |
---|
| 1389 | <DD> required |
---|
| 1390 | |
---|
| 1391 | <DT> <A HREF="calAllDet.html#BddReorderFixForwardingNodes" TARGET="MAIN"><CODE>BddReorderFixForwardingNodes()</CODE></A> |
---|
| 1392 | <DD> Fixes the forwarding nodes in a unique table. |
---|
| 1393 | |
---|
| 1394 | <DT> <A HREF="calAllDet.html#BddReorderFixAndFreeForwardingNodes" TARGET="MAIN"><CODE>BddReorderFixAndFreeForwardingNodes()</CODE></A> |
---|
| 1395 | <DD> Traverses the forwarding node lists of index, |
---|
| 1396 | index+1 .. up to index+level. Frees the intermediate forwarding nodes. |
---|
| 1397 | |
---|
| 1398 | <DT> <A HREF="calAllDet.html#BddReorderSwapVarIndex" TARGET="MAIN"><CODE>BddReorderSwapVarIndex()</CODE></A> |
---|
| 1399 | <DD> required |
---|
| 1400 | |
---|
| 1401 | <DT> <A HREF="calAllDet.html#CofactorFixAndReclaimForwardedNodes" TARGET="MAIN"><CODE>CofactorFixAndReclaimForwardedNodes()</CODE></A> |
---|
| 1402 | <DD> required |
---|
| 1403 | |
---|
| 1404 | <DT> <A HREF="calAllDet.html#BddReorderFreeNodes" TARGET="MAIN"><CODE>BddReorderFreeNodes()</CODE></A> |
---|
| 1405 | <DD> required |
---|
| 1406 | |
---|
| 1407 | <DT> <A HREF="calAllDet.html#PrintBddProfileAfterReorder" TARGET="MAIN"><CODE>PrintBddProfileAfterReorder()</CODE></A> |
---|
| 1408 | <DD> required |
---|
| 1409 | |
---|
| 1410 | <DT> <A HREF="calAllDet.html#BddReorderVarSift" TARGET="MAIN"><CODE>BddReorderVarSift()</CODE></A> |
---|
| 1411 | <DD> Reorder variables using "sift" algorithm. |
---|
| 1412 | |
---|
| 1413 | <DT> <A HREF="calAllDet.html#BddReorderSiftToBestPos" TARGET="MAIN"><CODE>BddReorderSiftToBestPos()</CODE></A> |
---|
| 1414 | <DD> required |
---|
| 1415 | |
---|
| 1416 | <DT> <A HREF="calAllDet.html#BddSiftPerfromPhaseIV" TARGET="MAIN"><CODE>BddSiftPerfromPhaseIV()</CODE></A> |
---|
| 1417 | <DD> required |
---|
| 1418 | |
---|
| 1419 | <DT> <A HREF="calAllDet.html#BddReorderVarWindow" TARGET="MAIN"><CODE>BddReorderVarWindow()</CODE></A> |
---|
| 1420 | <DD> required |
---|
| 1421 | |
---|
| 1422 | <DT> <A HREF="calAllDet.html#BddReorderWindow2" TARGET="MAIN"><CODE>BddReorderWindow2()</CODE></A> |
---|
| 1423 | <DD> required |
---|
| 1424 | |
---|
| 1425 | <DT> <A HREF="calAllDet.html#BddReorderWindow3" TARGET="MAIN"><CODE>BddReorderWindow3()</CODE></A> |
---|
| 1426 | <DD> required |
---|
| 1427 | |
---|
| 1428 | </DL> |
---|
| 1429 | <HR> |
---|
| 1430 | <A NAME="calReorderDF.c"><H1>calReorderDF.c</H1></A> |
---|
| 1431 | Routines for dynamic reordering of variables. <P> |
---|
| 1432 | <B>By: Rajeev K. Ranjan (rajeev@@ic. eecs.berkeley.edu)</B><P> |
---|
| 1433 | This method is based on traditional dynamic reordering |
---|
| 1434 | technique found in depth-first based packages. The data structure is |
---|
| 1435 | first converted to conform to traditional one and then reordering is |
---|
| 1436 | performed. At the end the nodes are arranged back on the pages. The |
---|
| 1437 | computational overheads are in terms of converting the data |
---|
| 1438 | structure back and forth and the memory overhead due to the extra |
---|
| 1439 | space needed to arrange the nodes. This overhead can be eliminated |
---|
| 1440 | by proper implementation. For details, please refer to the work by |
---|
| 1441 | Rajeev K. Ranjan et al - "Dynamic variable reordering in a |
---|
| 1442 | breadth-first manipulation based package: Challenges and Solutions"- |
---|
| 1443 | Proceedings of ICCD'97. <P> |
---|
| 1444 | <P><B>See Also</B><A HREF="#calReorderBF.c"><CODE>calReorderBF.c</CODE></A> |
---|
| 1445 | <A HREF="#calReorderUtil.c"><CODE>calReorderUtil.c</CODE></A> |
---|
| 1446 | <DL> |
---|
| 1447 | <DT> <A HREF="calAllDet.html#CalBddReorderAuxDF" TARGET="MAIN"><CODE>CalBddReorderAuxDF()</CODE></A> |
---|
| 1448 | <DD> required |
---|
| 1449 | |
---|
| 1450 | <DT> <A HREF="calAllDet.html#UniqueTableForIdFindOrAdd" TARGET="MAIN"><CODE>UniqueTableForIdFindOrAdd()</CODE></A> |
---|
| 1451 | <DD> find or add in the unique table for id. |
---|
| 1452 | |
---|
| 1453 | <DT> <A HREF="calAllDet.html#HashTableAddDirect" TARGET="MAIN"><CODE>HashTableAddDirect()</CODE></A> |
---|
| 1454 | <DD> Directly insert a BDD node in the hash table. |
---|
| 1455 | |
---|
| 1456 | <DT> <A HREF="calAllDet.html#HashTableFindOrAdd" TARGET="MAIN"><CODE>HashTableFindOrAdd()</CODE></A> |
---|
| 1457 | <DD> required |
---|
| 1458 | |
---|
| 1459 | <DT> <A HREF="calAllDet.html#BddConvertDataStruct" TARGET="MAIN"><CODE>BddConvertDataStruct()</CODE></A> |
---|
| 1460 | <DD> Changes the data structure of the bdd nodes. |
---|
| 1461 | |
---|
| 1462 | <DT> <A HREF="calAllDet.html#BddConvertDataStructBack" TARGET="MAIN"><CODE>BddConvertDataStructBack()</CODE></A> |
---|
| 1463 | <DD> Changes the data structure of the bdd nodes to |
---|
| 1464 | the original one. |
---|
| 1465 | |
---|
| 1466 | <DT> <A HREF="calAllDet.html#BddReallocateNodesInPlace" TARGET="MAIN"><CODE>BddReallocateNodesInPlace()</CODE></A> |
---|
| 1467 | <DD> required |
---|
| 1468 | |
---|
| 1469 | <DT> <A HREF="calAllDet.html#CalAlignCollisionChains" TARGET="MAIN"><CODE>CalAlignCollisionChains()</CODE></A> |
---|
| 1470 | <DD> required |
---|
| 1471 | |
---|
| 1472 | <DT> <A HREF="calAllDet.html#BddReallocateNodes" TARGET="MAIN"><CODE>BddReallocateNodes()</CODE></A> |
---|
| 1473 | <DD> required |
---|
| 1474 | |
---|
| 1475 | <DT> <A HREF="calAllDet.html#BddExchangeAux" TARGET="MAIN"><CODE>BddExchangeAux()</CODE></A> |
---|
| 1476 | <DD> required |
---|
| 1477 | |
---|
| 1478 | <DT> <A HREF="calAllDet.html#CheckValidityOfNodes" TARGET="MAIN"><CODE>CheckValidityOfNodes()</CODE></A> |
---|
| 1479 | <DD> required |
---|
| 1480 | |
---|
| 1481 | <DT> <A HREF="calAllDet.html#SweepVarTable" TARGET="MAIN"><CODE>SweepVarTable()</CODE></A> |
---|
| 1482 | <DD> required |
---|
| 1483 | |
---|
| 1484 | <DT> <A HREF="calAllDet.html#BddExchange" TARGET="MAIN"><CODE>BddExchange()</CODE></A> |
---|
| 1485 | <DD> required |
---|
| 1486 | |
---|
| 1487 | <DT> <A HREF="calAllDet.html#BddExchangeVarBlocks" TARGET="MAIN"><CODE>BddExchangeVarBlocks()</CODE></A> |
---|
| 1488 | <DD> required |
---|
| 1489 | |
---|
| 1490 | <DT> <A HREF="calAllDet.html#BddReorderWindow2" TARGET="MAIN"><CODE>BddReorderWindow2()</CODE></A> |
---|
| 1491 | <DD> required |
---|
| 1492 | |
---|
| 1493 | <DT> <A HREF="calAllDet.html#BddReorderWindow3" TARGET="MAIN"><CODE>BddReorderWindow3()</CODE></A> |
---|
| 1494 | <DD> required |
---|
| 1495 | |
---|
| 1496 | <DT> <A HREF="calAllDet.html#BddReorderStableWindow3Aux" TARGET="MAIN"><CODE>BddReorderStableWindow3Aux()</CODE></A> |
---|
| 1497 | <DD> required |
---|
| 1498 | |
---|
| 1499 | <DT> <A HREF="calAllDet.html#BddReorderStableWindow3" TARGET="MAIN"><CODE>BddReorderStableWindow3()</CODE></A> |
---|
| 1500 | <DD> required |
---|
| 1501 | |
---|
| 1502 | <DT> <A HREF="calAllDet.html#BddSiftBlock" TARGET="MAIN"><CODE>BddSiftBlock()</CODE></A> |
---|
| 1503 | <DD> required |
---|
| 1504 | |
---|
| 1505 | <DT> <A HREF="calAllDet.html#BddReorderSiftAux" TARGET="MAIN"><CODE>BddReorderSiftAux()</CODE></A> |
---|
| 1506 | <DD> Reorder variables using "sift" algorithm. |
---|
| 1507 | |
---|
| 1508 | <DT> <A HREF="calAllDet.html#BddReorderSift" TARGET="MAIN"><CODE>BddReorderSift()</CODE></A> |
---|
| 1509 | <DD> required |
---|
| 1510 | |
---|
| 1511 | <DT> <A HREF="calAllDet.html#BddAddInternalReferences" TARGET="MAIN"><CODE>BddAddInternalReferences()</CODE></A> |
---|
| 1512 | <DD> required |
---|
| 1513 | |
---|
| 1514 | <DT> <A HREF="calAllDet.html#BddNukeInternalReferences" TARGET="MAIN"><CODE>BddNukeInternalReferences()</CODE></A> |
---|
| 1515 | <DD> required |
---|
| 1516 | |
---|
| 1517 | <DT> <A HREF="calAllDet.html#CeilLog2" TARGET="MAIN"><CODE>CeilLog2()</CODE></A> |
---|
| 1518 | <DD> Returns the smallest integer greater than or equal to log2 of a |
---|
| 1519 | number |
---|
| 1520 | |
---|
| 1521 | </DL> |
---|
| 1522 | <HR> |
---|
| 1523 | <A NAME="calReorderUtil.c"><H1>calReorderUtil.c</H1></A> |
---|
| 1524 | Some utility routines used by both breadth-first and |
---|
| 1525 | depth-first reordering techniques. <P> |
---|
| 1526 | <B>By: Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu) |
---|
| 1527 | Wilsin Gosti (wilsin@ic.eecs.berkeley.edu)</B><P> |
---|
| 1528 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 1529 | <DL> |
---|
| 1530 | <DT> <A HREF="calAllDet.html#CalBddReorderFixUserBddPtrs" TARGET="MAIN"><CODE>CalBddReorderFixUserBddPtrs()</CODE></A> |
---|
| 1531 | <DD> required |
---|
| 1532 | |
---|
| 1533 | <DT> <A HREF="calAllDet.html#CalCheckAllValidity" TARGET="MAIN"><CODE>CalCheckAllValidity()</CODE></A> |
---|
| 1534 | <DD> required |
---|
| 1535 | |
---|
| 1536 | <DT> <A HREF="calAllDet.html#CalCheckValidityOfNodesForId" TARGET="MAIN"><CODE>CalCheckValidityOfNodesForId()</CODE></A> |
---|
| 1537 | <DD> required |
---|
| 1538 | |
---|
| 1539 | <DT> <A HREF="calAllDet.html#CalCheckValidityOfNodesForWindow" TARGET="MAIN"><CODE>CalCheckValidityOfNodesForWindow()</CODE></A> |
---|
| 1540 | <DD> required |
---|
| 1541 | |
---|
| 1542 | <DT> <A HREF="calAllDet.html#CalCheckValidityOfANode" TARGET="MAIN"><CODE>CalCheckValidityOfANode()</CODE></A> |
---|
| 1543 | <DD> required |
---|
| 1544 | |
---|
| 1545 | <DT> <A HREF="calAllDet.html#CalCheckRefCountValidity" TARGET="MAIN"><CODE>CalCheckRefCountValidity()</CODE></A> |
---|
| 1546 | <DD> required |
---|
| 1547 | |
---|
| 1548 | <DT> <A HREF="calAllDet.html#CalCheckAssoc" TARGET="MAIN"><CODE>CalCheckAssoc()</CODE></A> |
---|
| 1549 | <DD> required |
---|
| 1550 | |
---|
| 1551 | <DT> <A HREF="calAllDet.html#CalFixupAssoc" TARGET="MAIN"><CODE>CalFixupAssoc()</CODE></A> |
---|
| 1552 | <DD> required |
---|
| 1553 | |
---|
| 1554 | <DT> <A HREF="calAllDet.html#CalBddReorderFixCofactors" TARGET="MAIN"><CODE>CalBddReorderFixCofactors()</CODE></A> |
---|
| 1555 | <DD> Fixes the cofactors of the nodes belonging to |
---|
| 1556 | the given index. |
---|
| 1557 | |
---|
| 1558 | <DT> <A HREF="calAllDet.html#CalBddReorderReclaimForwardedNodes" TARGET="MAIN"><CODE>CalBddReorderReclaimForwardedNodes()</CODE></A> |
---|
| 1559 | <DD> required |
---|
| 1560 | |
---|
| 1561 | </DL> |
---|
| 1562 | <HR> |
---|
| 1563 | <A NAME="calTerminal.c"><H1>calTerminal.c</H1></A> |
---|
| 1564 | Contains the terminal function for various BDD operations. <P> |
---|
| 1565 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and |
---|
| 1566 | Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu</B><P> |
---|
| 1567 | <DL> |
---|
| 1568 | <DT> <A HREF="calAllDet.html#CalOpAnd" TARGET="MAIN"><CODE>CalOpAnd()</CODE></A> |
---|
| 1569 | <DD> required |
---|
| 1570 | |
---|
| 1571 | <DT> <A HREF="calAllDet.html#CalOpNand" TARGET="MAIN"><CODE>CalOpNand()</CODE></A> |
---|
| 1572 | <DD> required |
---|
| 1573 | |
---|
| 1574 | <DT> <A HREF="calAllDet.html#CalOpOr" TARGET="MAIN"><CODE>CalOpOr()</CODE></A> |
---|
| 1575 | <DD> required |
---|
| 1576 | |
---|
| 1577 | <DT> <A HREF="calAllDet.html#CalOpXor" TARGET="MAIN"><CODE>CalOpXor()</CODE></A> |
---|
| 1578 | <DD> required |
---|
| 1579 | |
---|
| 1580 | <DT> <A HREF="calAllDet.html#CalOpITE" TARGET="MAIN"><CODE>CalOpITE()</CODE></A> |
---|
| 1581 | <DD> required |
---|
| 1582 | |
---|
| 1583 | </DL> |
---|
| 1584 | <HR> |
---|
| 1585 | <A NAME="calTest.c"><H1>calTest.c</H1></A> |
---|
| 1586 | This file contains the test routines for the CAL package. <P> |
---|
| 1587 | <B>By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) |
---|
| 1588 | Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 1589 | Modified and extended from the original version written |
---|
| 1590 | by David Long.</B><P> |
---|
| 1591 | optional <P> |
---|
| 1592 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 1593 | <DL> |
---|
| 1594 | <DT> <A HREF="calAllDet.html#main" TARGET="MAIN"><CODE>main()</CODE></A> |
---|
| 1595 | <DD> required |
---|
| 1596 | |
---|
| 1597 | <DT> <A HREF="calAllDet.html#asDouble" TARGET="MAIN"><CODE>asDouble()</CODE></A> |
---|
| 1598 | <DD> required |
---|
| 1599 | |
---|
| 1600 | <DT> <A HREF="calAllDet.html#asAddress" TARGET="MAIN"><CODE>asAddress()</CODE></A> |
---|
| 1601 | <DD> required |
---|
| 1602 | |
---|
| 1603 | <DT> <A HREF="calAllDet.html#terminalIdFn" TARGET="MAIN"><CODE>terminalIdFn()</CODE></A> |
---|
| 1604 | <DD> required |
---|
| 1605 | |
---|
| 1606 | <DT> <A HREF="calAllDet.html#PrintBdd" TARGET="MAIN"><CODE>PrintBdd()</CODE></A> |
---|
| 1607 | <DD> required |
---|
| 1608 | |
---|
| 1609 | <DT> <A HREF="calAllDet.html#Error" TARGET="MAIN"><CODE>Error()</CODE></A> |
---|
| 1610 | <DD> required |
---|
| 1611 | |
---|
| 1612 | <DT> <A HREF="calAllDet.html#Cofactor" TARGET="MAIN"><CODE>Cofactor()</CODE></A> |
---|
| 1613 | <DD> required |
---|
| 1614 | |
---|
| 1615 | <DT> <A HREF="calAllDet.html#Decode" TARGET="MAIN"><CODE>Decode()</CODE></A> |
---|
| 1616 | <DD> required |
---|
| 1617 | |
---|
| 1618 | <DT> <A HREF="calAllDet.html#TestAnd" TARGET="MAIN"><CODE>TestAnd()</CODE></A> |
---|
| 1619 | <DD> required |
---|
| 1620 | |
---|
| 1621 | <DT> <A HREF="calAllDet.html#TestNand" TARGET="MAIN"><CODE>TestNand()</CODE></A> |
---|
| 1622 | <DD> required |
---|
| 1623 | |
---|
| 1624 | <DT> <A HREF="calAllDet.html#TestOr" TARGET="MAIN"><CODE>TestOr()</CODE></A> |
---|
| 1625 | <DD> required |
---|
| 1626 | |
---|
| 1627 | <DT> <A HREF="calAllDet.html#TestITE" TARGET="MAIN"><CODE>TestITE()</CODE></A> |
---|
| 1628 | <DD> required |
---|
| 1629 | |
---|
| 1630 | <DT> <A HREF="calAllDet.html#TestXor" TARGET="MAIN"><CODE>TestXor()</CODE></A> |
---|
| 1631 | <DD> required |
---|
| 1632 | |
---|
| 1633 | <DT> <A HREF="calAllDet.html#TestIdNot" TARGET="MAIN"><CODE>TestIdNot()</CODE></A> |
---|
| 1634 | <DD> required |
---|
| 1635 | |
---|
| 1636 | <DT> <A HREF="calAllDet.html#TestCompose" TARGET="MAIN"><CODE>TestCompose()</CODE></A> |
---|
| 1637 | <DD> required |
---|
| 1638 | |
---|
| 1639 | <DT> <A HREF="calAllDet.html#TestSubstitute" TARGET="MAIN"><CODE>TestSubstitute()</CODE></A> |
---|
| 1640 | <DD> required |
---|
| 1641 | |
---|
| 1642 | <DT> <A HREF="calAllDet.html#TestVarSubstitute" TARGET="MAIN"><CODE>TestVarSubstitute()</CODE></A> |
---|
| 1643 | <DD> required |
---|
| 1644 | |
---|
| 1645 | <DT> <A HREF="calAllDet.html#TestSwapVars" TARGET="MAIN"><CODE>TestSwapVars()</CODE></A> |
---|
| 1646 | <DD> required |
---|
| 1647 | |
---|
| 1648 | <DT> <A HREF="calAllDet.html#TestMultiwayAnd" TARGET="MAIN"><CODE>TestMultiwayAnd()</CODE></A> |
---|
| 1649 | <DD> required |
---|
| 1650 | |
---|
| 1651 | <DT> <A HREF="calAllDet.html#TestMultiwayOr" TARGET="MAIN"><CODE>TestMultiwayOr()</CODE></A> |
---|
| 1652 | <DD> required |
---|
| 1653 | |
---|
| 1654 | <DT> <A HREF="calAllDet.html#TestMultiwayLarge" TARGET="MAIN"><CODE>TestMultiwayLarge()</CODE></A> |
---|
| 1655 | <DD> required |
---|
| 1656 | |
---|
| 1657 | <DT> <A HREF="calAllDet.html#TestArrayOp" TARGET="MAIN"><CODE>TestArrayOp()</CODE></A> |
---|
| 1658 | <DD> required |
---|
| 1659 | |
---|
| 1660 | <DT> <A HREF="calAllDet.html#TestInterImpl" TARGET="MAIN"><CODE>TestInterImpl()</CODE></A> |
---|
| 1661 | <DD> required |
---|
| 1662 | |
---|
| 1663 | <DT> <A HREF="calAllDet.html#TestQnt" TARGET="MAIN"><CODE>TestQnt()</CODE></A> |
---|
| 1664 | <DD> required |
---|
| 1665 | |
---|
| 1666 | <DT> <A HREF="calAllDet.html#TestAssoc" TARGET="MAIN"><CODE>TestAssoc()</CODE></A> |
---|
| 1667 | <DD> required |
---|
| 1668 | |
---|
| 1669 | <DT> <A HREF="calAllDet.html#TestRelProd" TARGET="MAIN"><CODE>TestRelProd()</CODE></A> |
---|
| 1670 | <DD> required |
---|
| 1671 | |
---|
| 1672 | <DT> <A HREF="calAllDet.html#TestReduce" TARGET="MAIN"><CODE>TestReduce()</CODE></A> |
---|
| 1673 | <DD> required |
---|
| 1674 | |
---|
| 1675 | <DT> <A HREF="calAllDet.html#TestGenCof" TARGET="MAIN"><CODE>TestGenCof()</CODE></A> |
---|
| 1676 | <DD> required |
---|
| 1677 | |
---|
| 1678 | <DT> <A HREF="calAllDet.html#TestSize" TARGET="MAIN"><CODE>TestSize()</CODE></A> |
---|
| 1679 | <DD> required |
---|
| 1680 | |
---|
| 1681 | <DT> <A HREF="calAllDet.html#TestSatisfy" TARGET="MAIN"><CODE>TestSatisfy()</CODE></A> |
---|
| 1682 | <DD> required |
---|
| 1683 | |
---|
| 1684 | <DT> <A HREF="calAllDet.html#TestPipeline" TARGET="MAIN"><CODE>TestPipeline()</CODE></A> |
---|
| 1685 | <DD> required |
---|
| 1686 | |
---|
| 1687 | <DT> <A HREF="calAllDet.html#TestDump" TARGET="MAIN"><CODE>TestDump()</CODE></A> |
---|
| 1688 | <DD> required |
---|
| 1689 | |
---|
| 1690 | <DT> <A HREF="calAllDet.html#TestReorderBlock" TARGET="MAIN"><CODE>TestReorderBlock()</CODE></A> |
---|
| 1691 | <DD> required |
---|
| 1692 | |
---|
| 1693 | <DT> <A HREF="calAllDet.html#TestReorder" TARGET="MAIN"><CODE>TestReorder()</CODE></A> |
---|
| 1694 | <DD> required |
---|
| 1695 | |
---|
| 1696 | <DT> <A HREF="calAllDet.html#handler" TARGET="MAIN"><CODE>handler()</CODE></A> |
---|
| 1697 | <DD> required |
---|
| 1698 | |
---|
| 1699 | <DT> <A HREF="calAllDet.html#RandomTests" TARGET="MAIN"><CODE>RandomTests()</CODE></A> |
---|
| 1700 | <DD> required |
---|
| 1701 | |
---|
| 1702 | </DL> |
---|
| 1703 | <HR> |
---|
| 1704 | <A NAME="calUtil.c"><H1>calUtil.c</H1></A> |
---|
| 1705 | Utility functions for the Cal package. <P> |
---|
| 1706 | <B>By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) |
---|
| 1707 | Rajeev K. Ranjan (rajeev@eecs.berkeley.edu)</B><P> |
---|
| 1708 | Utility functions used in the Cal package. <P> |
---|
| 1709 | <P><B>See Also</B><A HREF="#optional"><CODE>optional</CODE></A> |
---|
| 1710 | <DL> |
---|
| 1711 | <DT> <A HREF="calAllDet.html#Cal_BddFunctionPrint" TARGET="MAIN"><CODE>Cal_BddFunctionPrint()</CODE></A> |
---|
| 1712 | <DD> Prints the function implemented by the argument BDD |
---|
| 1713 | |
---|
| 1714 | <DT> <A HREF="calAllDet.html#CalUniqueTablePrint" TARGET="MAIN"><CODE>CalUniqueTablePrint()</CODE></A> |
---|
| 1715 | <DD> required |
---|
| 1716 | |
---|
| 1717 | <DT> <A HREF="calAllDet.html#CalBddFunctionPrint" TARGET="MAIN"><CODE>CalBddFunctionPrint()</CODE></A> |
---|
| 1718 | <DD> Prints the function implemented by the argument BDD |
---|
| 1719 | |
---|
| 1720 | <DT> <A HREF="calAllDet.html#CalBddPreProcessing" TARGET="MAIN"><CODE>CalBddPreProcessing()</CODE></A> |
---|
| 1721 | <DD> required |
---|
| 1722 | |
---|
| 1723 | <DT> <A HREF="calAllDet.html#CalBddPostProcessing" TARGET="MAIN"><CODE>CalBddPostProcessing()</CODE></A> |
---|
| 1724 | <DD> required |
---|
| 1725 | |
---|
| 1726 | <DT> <A HREF="calAllDet.html#CalBddArrayPreProcessing" TARGET="MAIN"><CODE>CalBddArrayPreProcessing()</CODE></A> |
---|
| 1727 | <DD> required |
---|
| 1728 | |
---|
| 1729 | <DT> <A HREF="calAllDet.html#CalBddGetInternalBdd" TARGET="MAIN"><CODE>CalBddGetInternalBdd()</CODE></A> |
---|
| 1730 | <DD> Prints fatal message and exits. |
---|
| 1731 | |
---|
| 1732 | <DT> <A HREF="calAllDet.html#CalBddGetExternalBdd" TARGET="MAIN"><CODE>CalBddGetExternalBdd()</CODE></A> |
---|
| 1733 | <DD> Prints fatal message and exits. |
---|
| 1734 | |
---|
| 1735 | <DT> <A HREF="calAllDet.html#CalBddFatalMessage" TARGET="MAIN"><CODE>CalBddFatalMessage()</CODE></A> |
---|
| 1736 | <DD> Prints fatal message and exits. |
---|
| 1737 | |
---|
| 1738 | <DT> <A HREF="calAllDet.html#CalBddWarningMessage" TARGET="MAIN"><CODE>CalBddWarningMessage()</CODE></A> |
---|
| 1739 | <DD> Prints warning message. |
---|
| 1740 | |
---|
| 1741 | <DT> <A HREF="calAllDet.html#CalBddNodePrint" TARGET="MAIN"><CODE>CalBddNodePrint()</CODE></A> |
---|
| 1742 | <DD> required |
---|
| 1743 | |
---|
| 1744 | <DT> <A HREF="calAllDet.html#CalBddPrint" TARGET="MAIN"><CODE>CalBddPrint()</CODE></A> |
---|
| 1745 | <DD> required |
---|
| 1746 | |
---|
| 1747 | <DT> <A HREF="calAllDet.html#CalHashTablePrint" TARGET="MAIN"><CODE>CalHashTablePrint()</CODE></A> |
---|
| 1748 | <DD> Prints a hash table. |
---|
| 1749 | |
---|
| 1750 | <DT> <A HREF="calAllDet.html#CalHashTableOnePrint" TARGET="MAIN"><CODE>CalHashTableOnePrint()</CODE></A> |
---|
| 1751 | <DD> required |
---|
| 1752 | |
---|
| 1753 | </DL> |
---|
| 1754 | <HR> |
---|
| 1755 | Last updated on 970711 20h11 |
---|
| 1756 | </BODY></HTML> |
---|