cal.h: External header file
calInt.h: Internal header file
cal.c: Miscellaneous collection of exported BDD functions
calApplyReduce.c: Generic routines for processing temporary nodes during "apply" and "reduce" phases.
calAssociation.c: Contains the routines related to the variable association.
calBddCompose.c: Routine for composing one BDD into another.
calBddITE.c: Routine for computing ITE of 3 BDD operands.
calBddManager.c: Routines for maintaing the manager and creating variables etc.
calBddOp.c: Routines for performing simple boolean operations on a pair of BDDs or on an array of pair of BDDs or on an array of BDDs.
calBddReorderTest.c: A test routine for checking the functionality of dynamic reordering.
calBddSatisfy.c: Routines for BDD satisfying valuation.
calBddSize.c: BDD size and profile routines
calBddSubstitute.c: Routine for simultaneous substitution of an array of variables with an array of functions.
calBddSupport.c: Routines related to the support of a BDD.
calBddSwapVars.c: Routine for swapping two variables.
calBddVarSubstitute.c: Routine for simultaneous substitution of an array of variables with another array of variables.
calBlk.c: Routines for manipulating blocks of variables.
calCacheTableTwo.c: Functions to manage the Cache tables.
calDump.c: BDD library dump/undump routines
calGC.c: Garbage collection routines
calHashTable.c: Functions to manage the hash tables that are a part of 1. unique table 2. request queue
calHashTableOne.c: Routines for managing hash table with Bdd is a key and int, long, or double as a value
calHashTableThree.c: Functions to manage the hash tables that are a part of ITE operation
calInteract.c: Functions to manipulate the variable interaction matrix.
calMem.c: Routines for memory management.
calMemoryManagement.c: Special memory management routines specific to CAL.
calPerformanceTest.c: This file contains the performance test routines for the CAL package.
calPipeline.c: Routines for creating and managing the pipelined BDD operations.
calPrint.c: Routine for printing a BDD.
calPrintProfile.c: Routines for printing various profiles for a BDD.
calQuant.c: Routines for existential/universal quantification and relational product.
calReduce.c: Routines for optimizing a BDD with respect to a don't care set (cofactor and restrict).
calReorderBF.c: Routines for dynamic reordering of variables.
calReorderDF.c: Routines for dynamic reordering of variables.
calReorderUtil.c: Some utility routines used by both breadth-first and depth-first reordering techniques.
calTerminal.c: Contains the terminal function for various BDD operations.
calTest.c: This file contains the test routines for the CAL package.
calUtil.c: Utility functions for the Cal package.

cal.h

External header file

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu)

See Alsooptional

calInt.h

Internal header file

By: Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu Jagesh Sanghavi (sanghavi@ic.eecs.berkeley.edu)

See Alsocal.h

cal.c

Miscellaneous collection of exported BDD functions

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu

Cal_BddIsEqual(): Returns 1 if argument BDDs are equal, 0 otherwise.
Cal_BddIsBddOne(): Returns 1 if the argument BDD is constant one, 0 otherwise.
Cal_BddIsBddZero(): Returns 1 if the argument BDD is constant zero, 0 otherwise.
Cal_BddIsBddNull(): Returns 1 if the argument BDD is NULL, 0 otherwise.
Cal_BddIsBddConst(): Returns 1 if the argument BDD is a constant, 0 otherwise.
Cal_BddIdentity(): Returns the duplicate BDD of the argument BDD.
Cal_BddOne(): Returns the BDD for the constant one
Cal_BddZero(): Returns the BDD for the constant zero
Cal_BddNot(): Returns the complement of the argument BDD.
Cal_BddGetIfIndex(): Returns the index of the top variable of the argument BDD.
Cal_BddGetIfId(): Returns the id of the top variable of the argument BDD.
Cal_BddIf(): Returns the BDD corresponding to the top variable of the argument BDD.
Cal_BddThen(): Returns the positive cofactor of the argument BDD with respect to the top variable of the BDD.
Cal_BddElse(): Returns the negative cofactor of the argument BDD with respect to the top variable of the BDD.
Cal_BddFree(): Frees the argument BDD.
Cal_BddUnFree(): Unfrees the argument BDD.
Cal_BddGetRegular(): Returns a BDD with positive from a given BDD with arbitrary phase
Cal_BddIntersects(): Computes a BDD that implies conjunction of f and g.
Cal_BddImplies(): Computes a BDD that implies conjunction of f and Cal_BddNot(g)
Cal_BddTotalSize(): Returns the number of nodes in the Unique table
Cal_BddStats(): Prints miscellaneous BDD statistics
Cal_BddDynamicReordering(): Specify dynamic reordering technique.
Cal_BddReorder(): Invoke the current dynamic reodering method.
Cal_BddType(): Returns type of a BDD ( 0, 1, +var, -var, ovrflow, nonterminal)
Cal_BddVars(): Returns the number of BDD variables
Cal_BddNodeLimit(): Sets the node limit to new_limit and returns the old limit.
Cal_BddOverflow(): Returns 1 if the node limit has been exceeded, 0 otherwise. The overflow flag is cleared.
Cal_BddIsCube(): Returns 1 if the argument BDD is a cube, 0 otherwise
Cal_BddManagerGetHooks(): Returns the hooks field of the manager.
Cal_BddManagerSetHooks(): Sets the hooks field of the manager.
CalBddIf(): Returns the BDD corresponding to the top variable of the argument BDD.
CalBddIsCubeStep(): Returns 1 if the argument BDD is a cube, 0 otherwise
CalBddTypeAux(): Returns the BDD type by recursively traversing the argument BDD
CalBddIdentity(): Returns the duplicate BDD of the argument BDD.
BddIntersectsStep(): Recursive routine to returns a BDD that implies conjunction of argument BDDs

calApplyReduce.c

Generic routines for processing temporary nodes during "apply" and "reduce" phases.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

See Alsooptional

CalHashTableApply(): required
CalHashTableReduce(): required

calAssociation.c

Contains the routines related to the variable association.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

optional

See Alsooptional

Cal_AssociationInit(): Creates or finds a variable association.
Cal_AssociationQuit(): Deletes the variable association given by id
Cal_AssociationSetCurrent(): Sets the current variable association to the one given by id and returns the ID of the old association.
Cal_TempAssociationAugment(): Adds to the temporary variable association.
Cal_TempAssociationInit(): Sets the temporary variable association.
Cal_TempAssociationQuit(): Cleans up temporary association
CalAssociationListFree(): Frees the variable associations
CalVarAssociationRepackUpdate(): Need to be called after repacking.
CalCheckAssociationValidity(): Checks the validity of association.
CalReorderAssociationFix(): required
AssociationIsEqual(): Checks for equality of two associations
CheckAssoc(): required

calBddCompose.c

Routine for composing one BDD into another.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

Cal_BddCompose(): composition - substitute a BDD variable by a function
CalRequestNodeListCompose(): required
CalHashTableComposeApply(): required
CalComposeRequestCreate(): required

calBddITE.c

Routine for computing ITE of 3 BDD operands.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

See Alsooptional

Cal_BddITE(): Returns the BDD for logical If-Then-Else Description [Returns the BDD for the logical operation IF f THEN g ELSE h - f g + f' h
CalRequestNodeListArrayITE(): required
CalBddOpITEBF(): required
CalHashTableITEApply(): required
CalBddITE(): Returns the BDD for logical If-Then-Else Description [Returns the BDD for the logical operation IF f THEN g ELSE h - f g + f' h

calBddManager.c

Routines for maintaing the manager and creating variables etc.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

See Alsooptional

Cal_BddManagerInit(): Creates and initializes a new BDD manager.
Cal_BddManagerQuit(): Frees the BDD manager and all the associated allocations
Cal_BddManagerSetParameters(): Sets appropriate fields of BDD Manager.
Cal_BddManagerGetNumNodes(): Returns the number of BDD nodes
Cal_BddManagerCreateNewVarFirst(): Creates and returns a new variable at the start of the variable order.
Cal_BddManagerCreateNewVarLast(): Creates and returns a new variable at the end of the variable order.
Cal_BddManagerCreateNewVarBefore(): Creates and returns a new variable before the specified one in the variable order.
Cal_BddManagerCreateNewVarAfter(): Creates and returns a new variable after the specified one in the variable order.
Cal_BddManagerGetVarWithIndex(): Returns the variable with the specified index, null if no such variable exists
Cal_BddManagerGetVarWithId(): Returns the variable with the specified id, null if no such variable exists
CalBddManagerCreateNewVar(): This function creates and returns a new variable with given index value.
BddDefaultTransformFn(): required
CalBddManagerPrint(): required

calBddOp.c

Routines for performing simple boolean operations on a pair of BDDs or on an array of pair of BDDs or on an array of BDDs.

By: Rajeev Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

The "cal" specific routines are "Cal_BddPairwiseAnd/Or", "Cal_BddMultiwayAnd/Or".

See Alsooptional

Cal_BddAnd(): Returns the BDD for logical AND of argument BDDs
Cal_BddNand(): Returns the BDD for logical NAND of argument BDDs
Cal_BddOr(): Returns the BDD for logical OR of argument BDDs
Cal_BddNor(): Returns the BDD for logical NOR of argument BDDs
Cal_BddXor(): Returns the BDD for logical exclusive OR of argument BDDs
Cal_BddXnor(): Returns the BDD for logical exclusive NOR of argument BDDs
Cal_BddPairwiseAnd(): Returns an array of BDDs obtained by logical AND of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array
Cal_BddPairwiseOr(): Returns an array of BDDs obtained by logical OR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array
Cal_BddPairwiseXor(): Returns an array of BDDs obtained by logical XOR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array
Cal_BddMultiwayAnd(): Returns the BDD for logical AND of argument BDDs
Cal_BddMultiwayOr(): Returns the BDD for logical OR of argument BDDs
Cal_BddMultiwayXor(): Returns the BDD for logical XOR of argument BDDs
CalRequestNodeListArrayOp(): Computes result BDDs for an array of lists, each entry of which is pair of pointers, each of which points to a operand BDD or an entry in another list with a smaller array index
CalBddOpBF(): Internal routine to compute a logical operation on a pair of BDDs
BddArrayOpBF(): Internal common routine for Cal_BddPairwiseAnd and Cal_BddPairwiseOr
BddMultiwayOp(): Internal routine for multiway operations
BddArrayToRequestNodeListArray(): Converts an array of BDDs to a list of requests representing BDD pairs
CeilLog2(): Returns the smallest integer greater than or equal to log2 of a number

calBddReorderTest.c

A test routine for checking the functionality of dynamic reordering.

By: Wilsin Gosti (wilsin@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

See Alsooptional

main(): required
cpuTime(): required
elapsedTime(): Computes the time.

calBddSatisfy.c

Routines for BDD satisfying valuation.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

See Alsooptional

Cal_BddSatisfy(): Returns a BDD which implies f, true for some valuation on which f is true, and which has at most one node at each level
Cal_BddSatisfySupport(): Returns a special cube contained in f.
Cal_BddSatisfyingFraction(): Returns the fraction of valuations which make f true. (Note that this fraction is independent of whatever set of variables f is supposed to be a function of)
BddSatisfyStep(): Returns a BDD which implies f, is true for some valuation on which f is true, and which has at most one node at each level
BddSatisfySupportStep()
IndexCmp()
BddSatisfyingFractionStep()

calBddSize.c

BDD size and profile routines

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Originally written by David Long.

See Alsooptional

Cal_BddSize(): Returns the number of nodes in f when negout is nonzero. If negout is zero, we pretend that the BDDs don't have negative-output pointers.
Cal_BddSizeMultiple(): The routine is like Cal_BddSize, but takes a null-terminated array of BDDs and accounts for sharing of nodes.
Cal_BddProfile(): Returns a "node profile" of f, i.e., the number of nodes at each level in f.
Cal_BddProfileMultiple()
Cal_BddFunctionProfile(): Returns a "function profile" for f.
Cal_BddFunctionProfileMultiple(): Returns a "function profile" for fArray.
BddMarkBdd()
BddCountNoNodes()
BddCountNodes()
BddSizeStep()
BddProfileStep()
BddHighestRefStep()
BddDominatedStep()

calBddSubstitute.c

Routine for simultaneous substitution of an array of variables with an array of functions.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

Routine for simultaneous substitution of an array of variables with an array of functions.

See Alsooptional

Cal_BddSubstitute(): Substitute a set of variables by functions
CalHashTableSubstituteApply(): required
CalHashTableSubstituteReduce(): required

calBddSupport.c

Routines related to the support of a BDD.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Originally written by David Long.

See Alsooptional

Cal_BddSupport(): returns the support of f as a null-terminated array of variables
Cal_BddDependsOn(): Returns 1 if f depends on var and returns 0 otherwise.
CalBddSupportStep(): returns the support of f as a null-terminated array of variables
CalBddUnmarkNodes(): recursively unmarks the nodes
CalBddDependsOnStep(): required

calBddSwapVars.c

Routine for swapping two variables.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

Routine for swapping two variables.

See AlsoNone

Cal_BddSwapVars(): Return a function obtained by swapping two variables
CalHashTableSwapVarsApply(): required
CalHashTableSwapVarsPlusApply(): required
CalHashTableSwapVarsMinusApply(): required

calBddVarSubstitute.c

Routine for simultaneous substitution of an array of variables with another array of variables.

By: Rajeev Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

See Alsooptional

Cal_BddVarSubstitute(): Substitute a set of variables by set of another variables.
CalBddVarSubstitute(): Substitute a set of variables by functions
CalOpBddVarSubstitute(): required
CalHashTableSubstituteApply(): required
CalHashTableSubstituteReduce(): required

calBlk.c

Routines for manipulating blocks of variables.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu). Modelled on the BDD package developed by David Long.

Routines for manipulating blocks of variables.

Cal_BddNewVarBlock(): Creates and returns a variable block used for controlling dynamic reordering.
Cal_BddVarBlockReorderable(): Sets the reoderability of a particular block.
CalBddFindBlock(): required
CalBddBlockDelta(): required
CalBddShiftBlock(): required
CalBlockMemoryConsumption(): required
CalFreeBlockRecursively(): required
AddBlock(): required

calCacheTableTwo.c

Functions to manage the Cache tables.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

See Alsooptional

CalCacheTableTwoInit(): Initialize a Cache table using default parameters.
CalCacheTableTwoQuit(): Free a Cache table along with the associated storage.
CalCacheTableTwoInsert(): Directly insert a BDD node in the Cache table.
CalCacheTableTwoLookup(): required
CalCacheTableTwoFlush(): Free a Cache table along with the associated storage.
CalCacheTableTwoFlushAll(): Free a Cache table along with the associated storage.
CalCacheTableTwoGCFlush(): required
CalCacheTableTwoRepackUpdate(): required
CalCheckCacheTableValidity(): required
CalCacheTableTwoFixResultPointers(): required
CalCacheTablePrint(): required
CalBddManagerGetCacheTableData(): required
CalCacheTableRehash(): required
CalCacheTableTwoFlushAssociationId(): Flushes the entries from the cache which correspond to the given associationId.
CalCacheTableMemoryConsumption(): required
CacheTableTwoRehash(): required
CacheTablePrint(): required

calDump.c

BDD library dump/undump routines

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Originally written by David Long.

See Alsooptional

Cal_BddUndumpBdd(): Reads a BDD from a file
Cal_BddDumpBdd(): Write a BDD to a file
Write()
BddDumpBddStep()
Read()
BddUndumpBddStep()
BytesNeeded()

calGC.c

Garbage collection routines

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

optional

See Alsooptional

Cal_BddSetGCMode(): Sets the garbage collection mode, 0 means the garbage collection should be turned off, 1 means garbage collection should be on.
Cal_BddManagerGC(): Invokes the garbage collection at the manager level.
Cal_BddManagerSetGCLimit(): Sets the limit of the garbage collection.
CalBddManagerGCCheck(): required
CalHashTableGC(): This function performs the garbage collection operation for a particular index.
CalRepackNodesAfterGC(): required
CeilLog2(): Returns the smallest integer greater than or equal to log2 of a number

calHashTable.c

Functions to manage the hash tables that are a part of 1. unique table 2. request queue

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

CalHashTableInit(): Initialize a hash table using default parameters.
CalHashTableQuit(): Free a hash table along with the associated storage.
CalHashTableAddDirect(): Directly insert a BDD node in the hash table.
CalHashTableFindOrAdd(): required
CalHashTableAddDirectAux(): required
CalHashTableCleanUp(): required
CalHashTableLookup(): required
CalHashTableDelete(): Deletes a BDD node in the hash table.
CalUniqueTableForIdLookup(): Lookup unique table for id.
CalUniqueTableForIdFindOrAdd(): find or add in the unique table for id.
CalHashTableRehash(): required
CalUniqueTableForIdRehashNode(): required
CalBddUniqueTableNumLockedNodes(): required
CalPackNodes(): required
CalBddPackNodesForSingleId(): required
CalBddPackNodesAfterReorderForSingleId(): Packs the nodes if the variables which has just been sifted.
CalBddPackNodesForMultipleIds(): required
CeilLog2(): Returns the smallest integer greater than or equal to log2 of a number

calHashTableOne.c

Routines for managing hash table with Bdd is a key and int, long, or double as a value

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

See Alsooptional

CalHashTableOneInit(): Initialize a hash table using default parameters.
CalHashTableOneQuit(): Free a hash table along with the associated storage.
CalHashTableOneInsert(): Directly insert a BDD node in the hash table.
CalHashTableOneLookup(): required
HashTableOneRehash(): required

calHashTableThree.c

Functions to manage the hash tables that are a part of ITE operation

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

CalHashTableThreeFindOrAdd

See Alsooptional

CalHashTableThreeFindOrAdd(): required
CalHashTableThreeRehash(): required

calInteract.c

Functions to manipulate the variable interaction matrix.

By: Original author:Fabio Somenzi. Modified for CAL package by Rajeev K. Ranjan

The interaction matrix tells whether two variables are both in the support of some function of the DD. The main use of the interaction matrix is in the in-place swapping. Indeed, if two variables do not interact, there is no arc connecting the two layers; therefore, the swap can be performed in constant time, without scanning the subtables. Another use of the interaction matrix is in the computation of the lower bounds for sifting. Finally, the interaction matrix can be used to speed up aggregation checks in symmetric and group sifting.

The computation of the interaction matrix is done with a series of depth-first searches. The searches start from those nodes that have only external references. The matrix is stored as a packed array of bits; since it is symmetric, only the upper triangle is kept in memory. As a final remark, we note that there may be variables that do intercat, but that for a given variable order have no arc connecting their layers when they are adjacent.

CalSetInteract(): Set interaction matrix entries.
CalTestInteract(): Test interaction matrix entries.
CalInitInteract(): Initializes the interaction matrix.
ddSuppInteract(): Find the support of f.
ddClearLocal(): Performs a DFS from f, clearing the LSB of the then pointers.
ddUpdateInteract(): Marks as interacting all pairs of variables that appear in support.

calMem.c

Routines for memory management.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu). Originally written by David Long.

Contains allocation, free, resize routines. Also has routines for managing records of fixed size.

See Alsooptional

Cal_MemFatal(): Prints an error message and exits.
Cal_MemAllocation(): Returns the memory allocated.
Cal_MemGetBlock(): Allocates a new block of the specified size.
Cal_MemFreeBlock(): Frees the block.
Cal_MemResizeBlock(): Expands or contracts the block to a new size. We try to avoid moving the block if possible.
Cal_MemNewRec(): Allocates a record from the specified record manager.
Cal_MemFreeRec(): Frees a record managed by the indicated record manager.
Cal_MemNewRecMgr(): Creates a new record manager with the given record size.
Cal_MemFreeRecMgr(): Frees all the storage associated with the specified record manager.
CeilingLog2(): required
BlockSizeIndex(): required
AddToFreeList(): required
RemoveFromFreeList(): required
Buddy(): required
TrimToSize(): required
MergeAndFree(): required

calMemoryManagement.c

Special memory management routines specific to CAL.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu)

Functions for managing the system memory using a set of nodeManagers. Each nodeManager manages a set of fixed size nodes obtained from a set of pages. When additional memory is required, nodeManager obtains a new page from the pageManager. The new page is divided into ( PAGE_SIZE/NODE_SIZE ) number of nodes.

CalPageManagerInit(): Initializes a pageManager.
CalPageManagerQuit(): Frees pageManager and associated pages.
CalPageManagerPrint(): Prints address of each memory segment and address of each page.
CalNodeManagerInit(): Initializes a node manager.
CalNodeManagerQuit(): Frees a node manager.
CalNodeManagerPrint(): Prints address of each free node.
CalPageManagerAllocPage(): Allocs a new page.
CalPageManagerFreePage(): Free a page.
PageManagerExpandStorage(): Allocates a segment of memory to expand the storage managed by pageManager. The allocated segment is divided into free pages which are linked as a freePageList.
PageAlign(): Return page aligned address greater than or equal to the pointer.
SegmentToPageList(): Converts a memory segment into a linked list of pages. if p is a pointer to a page, *p contains address of the next page if p is a pointer to the last page, *p contains lastPointer.

calPerformanceTest.c

This file contains the performance test routines for the CAL package.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

optional

See Alsooptional

Cal_PerformanceTest(): Main routine for testing performances of various routines.
CalIncreasingOrderCompare(): required
CalDecreasingOrderCompare(): required
CalPerformanceTestAnd(): Performance test routine for quantify (all variables at the same time).
CalPerformanceMemoryOverhead(): Performance test routine for quantify (all variables at the same time).
CalPerformaceTestSuperscalar(): Performance test routine for quantify (all variables at the same time).
CalPerformanceTestNonSuperscalar(): Performance test routine for quantify (all variables at the same time).
CalPerformanceTestMultiway(): Performance test routine for quantify (all variables at the same time).
CalPerformanceTestOneway(): Performance test routine for quantify (all variables at the same time).
CalPerformanceTestCompose(): Performance test routine for quantify (all variables at the same time).
CalPerformanceTestQuantifyAllTogether(): Performance test routine for quantify (all variables at the same time).
CalQuantifySanityCheck(): Performance test routine for quantify (all variables at the same time).
CalPerformanceTestRelProd(): Performance test routine for quantify (all variables at the same time).
CalPerformanceTestSubstitute(): Performance test routine for quantify (all variables at the same time).
CalPerformanceTestSwapVars(): Performance test routine for quantify (all variables at the same time).
elapsedTime(): Computes the time.
cpuTime(): Computes the number of page faults.
pageFaults(): Computes the number of page faults.
GetRandomNumbers(): Generates "count" many random numbers ranging between "lowerBound" and "upperBound".

calPipeline.c

Routines for creating and managing the pipelined BDD operations.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)

Eventually we would like to have this feature transparent to the user.

See Alsooptional

Cal_PipelineSetDepth(): Set depth of a BDD pipeline.
Cal_PipelineInit(): Initialize a BDD pipeline.
Cal_PipelineCreateProvisionalBdd(): Create a provisional BDD in the pipeline.
Cal_PipelineExecute(): Executes a pipeline.
Cal_PipelineUpdateProvisionalBdd(): Update a provisional Bdd obtained during pipelining.
Cal_BddIsProvisional(): Returns 1, if the given user BDD contains provisional BDD node.
Cal_PipelineQuit(): Resets the pipeline freeing all resources.
CalBddReorderFixProvisionalNodes(): required
CalCheckPipelineValidity(): required

calPrint.c

Routine for printing a BDD.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu) Originally written by David Long.

See AlsoNone

Cal_BddPrintBdd(): Prints a BDD in the human readable form.
CalBddVarName(): required
CalBddNumberSharedNodes(): required
CalBddMarkSharedNodes(): required
Chars(): required
BddPrintTopVar(): required
BddPrintBddStep(): required
BddTerminalId(): required
BddTerminalValueAux(): required

calPrintProfile.c

Routines for printing various profiles for a BDD.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Originally written by David Long.

See Alsooptional

Cal_BddPrintProfile(): Displays the node profile for f on fp. lineLength specifies the maximum line length. varNamingFn is as in Cal_BddPrintBdd.
Cal_BddPrintProfileMultiple(): Cal_BddPrintProfileMultiple is like Cal_BddPrintProfile except it displays the profile for a set of BDDs
Cal_BddPrintFunctionProfile(): Cal_BddPrintFunctionProfile is like Cal_BddPrintProfile except it displays a function profile for f
Cal_BddPrintFunctionProfileMultiple(): Cal_BddPrintFunctionProfileMultiple is like Cal_BddPrintFunctionProfile except for multiple BDDs
CalBddPrintProfileAux(): Prints a profile to the file given by fp. The varNamingProc is as in Cal_BddPrintBdd. lineLength gives the line width to scale the profile to.
chars()

calQuant.c

Routines for existential/universal quantification and relational product.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu)

See AlsoNone

Cal_BddExists(): Returns the result of existentially quantifying some variables from the given BDD.
Cal_BddRelProd(): Returns the result of taking the logical AND of the argument BDDs and existentially quantifying some variables from the product.
Cal_BddForAll(): Returns the result of universally quantifying some variables from the given BDD.
CalOpExists(): required
CalOpRelProd(): required
BddExistsStep(): required
BddRelProdStep(): required
BddDFStep(): required
HashTableApply(): required
HashTableReduce(): required
BddExistsApply(): required
BddExistsBFAux(): required
BddExistsReduce(): required
BddExistsBFPlusDF(): required
BddRelProdApply(): required
BddRelProdReduce(): required
BddRelProdBFAux(): required
BddRelProdBFPlusDF(): required

calReduce.c

Routines for optimizing a BDD with respect to a don't care set (cofactor and restrict).

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu

See AlsoNone

Cal_BddCofactor(): Returns the generalized cofactor of BDD f with respect to BDD c.
Cal_BddReduce(): Returns a BDD which agrees with f for all valuations which satisfy c.
Cal_BddBetween(): Returns a minimal BDD whose function contains fMin and is contained in fMax.
CalOpCofactor(): required
BddReduceBF(): required
BddCofactorBF(): required
HashTableReduceApply(): required
HashTableCofactorApply(): required
HashTableCofactorReduce(): required

calReorderBF.c

Routines for dynamic reordering of variables.

By: Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu) Wilsin Gosti (wilsin@ic.eecs.berkeley.edu)

This method dynamically reorders variables while preserving their locality. This entails both memory and computational overheads. Conceptually and experimentally it has been observed that these overheads lead to poorer performance compared to the traditional reordering methods. For details, please refer to the work by Rajeev K. Ranjan et al - "Dynamic variable reordering in a breadth-first manipulation based package: Challenges and Solutions"- Proceedings of ICCD'97.

CalBddReorderAuxBF(): required
BddReorderFixForwardingNodes(): Fixes the forwarding nodes in a unique table.
BddReorderFixAndFreeForwardingNodes(): Traverses the forwarding node lists of index, index+1 .. up to index+level. Frees the intermediate forwarding nodes.
BddReorderSwapVarIndex(): required
CofactorFixAndReclaimForwardedNodes(): required
BddReorderFreeNodes(): required
PrintBddProfileAfterReorder(): required
BddReorderVarSift(): Reorder variables using "sift" algorithm.
BddReorderSiftToBestPos(): required
BddSiftPerfromPhaseIV(): required
BddReorderVarWindow(): required
BddReorderWindow2(): required
BddReorderWindow3(): required

calReorderDF.c

Routines for dynamic reordering of variables.

By: Rajeev K. Ranjan (rajeev@@ic. eecs.berkeley.edu)

This method is based on traditional dynamic reordering technique found in depth-first based packages. The data structure is first converted to conform to traditional one and then reordering is performed. At the end the nodes are arranged back on the pages. The computational overheads are in terms of converting the data structure back and forth and the memory overhead due to the extra space needed to arrange the nodes. This overhead can be eliminated by proper implementation. For details, please refer to the work by Rajeev K. Ranjan et al - "Dynamic variable reordering in a breadth-first manipulation based package: Challenges and Solutions"- Proceedings of ICCD'97.

CalBddReorderAuxDF(): required
UniqueTableForIdFindOrAdd(): find or add in the unique table for id.
HashTableAddDirect(): Directly insert a BDD node in the hash table.
HashTableFindOrAdd(): required
BddConvertDataStruct(): Changes the data structure of the bdd nodes.
BddConvertDataStructBack(): Changes the data structure of the bdd nodes to the original one.
BddReallocateNodesInPlace(): required
CalAlignCollisionChains(): required
BddReallocateNodes(): required
BddExchangeAux(): required
CheckValidityOfNodes(): required
SweepVarTable(): required
BddExchange(): required
BddExchangeVarBlocks(): required
BddReorderWindow2(): required
BddReorderWindow3(): required
BddReorderStableWindow3Aux(): required
BddReorderStableWindow3(): required
BddSiftBlock(): required
BddReorderSiftAux(): Reorder variables using "sift" algorithm.
BddReorderSift(): required
BddAddInternalReferences(): required
BddNukeInternalReferences(): required
CeilLog2(): Returns the smallest integer greater than or equal to log2 of a number

calReorderUtil.c

Some utility routines used by both breadth-first and depth-first reordering techniques.

By: Rajeev K. Ranjan (rajeev@ic.eecs.berkeley.edu) Wilsin Gosti (wilsin@ic.eecs.berkeley.edu)

See Alsooptional

CalBddReorderFixUserBddPtrs(): required
CalCheckAllValidity(): required
CalCheckValidityOfNodesForId(): required
CalCheckValidityOfNodesForWindow(): required
CalCheckValidityOfANode(): required
CalCheckRefCountValidity(): required
CalCheckAssoc(): required
CalFixupAssoc(): required
CalBddReorderFixCofactors(): Fixes the cofactors of the nodes belonging to the given index.
CalBddReorderReclaimForwardedNodes(): required

calTerminal.c

Contains the terminal function for various BDD operations.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu

CalOpAnd(): required
CalOpNand(): required
CalOpOr(): required
CalOpXor(): required
CalOpITE(): required

calTest.c

This file contains the test routines for the CAL package.

By: Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Modified and extended from the original version written by David Long.

optional

See Alsooptional

main(): required
asDouble(): required
asAddress(): required
terminalIdFn(): required
PrintBdd(): required
Error(): required
Cofactor(): required
Decode(): required
TestAnd(): required
TestNand(): required
TestOr(): required
TestITE(): required
TestXor(): required
TestIdNot(): required
TestCompose(): required
TestSubstitute(): required
TestVarSubstitute(): required
TestSwapVars(): required
TestMultiwayAnd(): required
TestMultiwayOr(): required
TestMultiwayLarge(): required
TestArrayOp(): required
TestInterImpl(): required
TestQnt(): required
TestAssoc(): required
TestRelProd(): required
TestReduce(): required
TestGenCof(): required
TestSize(): required
TestSatisfy(): required
TestPipeline(): required
TestDump(): required
TestReorderBlock(): required
TestReorder(): required
handler(): required
RandomTests(): required

calUtil.c

Utility functions for the Cal package.

By: Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev K. Ranjan (rajeev@eecs.berkeley.edu)

Utility functions used in the Cal package.

See Alsooptional

Cal_BddFunctionPrint(): Prints the function implemented by the argument BDD
CalUniqueTablePrint(): required
CalBddFunctionPrint(): Prints the function implemented by the argument BDD
CalBddPreProcessing(): required
CalBddPostProcessing(): required
CalBddArrayPreProcessing(): required
CalBddGetInternalBdd(): Prints fatal message and exits.
CalBddGetExternalBdd(): Prints fatal message and exits.
CalBddFatalMessage(): Prints fatal message and exits.
CalBddWarningMessage(): Prints warning message.
CalBddNodePrint(): required
CalBddPrint(): required
CalHashTablePrint(): Prints a hash table.
CalHashTableOnePrint(): required

Last updated on 970711 20h11