sym.h
External header file
symInt.h
Internal header file
sym.c
symAssignMdd.c
routines to build mdd for an assignment
symBitvec.c
provides utilities to build transition relation for bit vector operations
symExprMdd.c
routines to build mdd for boolean expressions
symIntf.c
Tcl/Tk interface to image computation
symMV.c
Builds the MDDs for the multi-valued expressions.
symMddArray.c
routines to manage an array of MDDs
symUtil.c
utilities provided by sym package

sym.h

External header file

By: Sriram K. Rajamani

See Alsooptional


symInt.h

Internal header file

By: Sriram K. Rajamani


sym.c

By: Sriram K. Rajamani

Sym_ModulePerformBFS()
do invariant checking
Sym_DebugTracePrint()
print debug trace for an invariant
Sym_ModuleBuildTransitionRelation()
build symbolic transtion relation for a module
Sym_ModuleBuildInitialRegion()
build mdd for initial region of module
Sym_AtomBuildTransitionRelation()
build transition relation for an atom
Sym_AtomBuildInitialRegion()
build initial region for an atom
SymModuleSearch()
do reachability + invariant checking
MddGroupVariables()
Group all bdd vars corresponding to mdd vars initMddId to initMddId + (blockSize-1) in a block which will not be split in reordering.

symAssignMdd.c

routines to build mdd for an assignment

By: Sriram K. Rajamani

An assignment has an LHS var and an RHS expression. Assignments can be classified based on the type of LHS. This file has routines to build MDDs corresponding to assignments. (1) If the LHS is boolean, MDDs are created separately for LHS and RHS, and are then xnored. (2) If the LHS is bitvector or multivalued specialized functions (implemented on symMV.c or symBitVector.c) are called.

See AlsoSymExprMdd.c

Sym_AssignmentBuildMdd()
build MDD for an assignment
SymAssignmentBuildMddStandard()
build MDD for a standard asssignment
SymAssignmentBuildMddBoolean()
Build MDD for boolean assignment with LHS and RHS of type boolean

symBitvec.c

provides utilities to build transition relation for bit vector operations

By: Sriram K. Rajamani

optional

See Alsooptional

SymBitVectorBuildAssignmentMdd()
build MDD for bit vector assignment
SymBitVectorBuildBooleanExpressionMdd()
build MDD for a boolean expression of bit vectors
SymBitVectorBuildMddArray()
build MDD array for bit vector expression
SymBitVectorBuildMddArrayForVar()
return and mdd array for a bitvector variable

symExprMdd.c

routines to build mdd for boolean expressions

By: Sriram K. Rajamani

This file containes routies that are used to build MDDs corresponding to boolean expressions. Note that the boolean expressions can have multi valued variables e.g: (x < 5) & (y > x + 5)

See AlsoSymAssignMdd.c

Sym_ExprBuildMdd()
build MDD for an expression
SymExprBuildExprConstMdd()
build MDD for an expression-constant equality

symIntf.c

Tcl/Tk interface to image computation

By: Sriram Rajamani

Sym_Init()
Initilization function for sym package
Sym_Reinit()
Re-initialization function for sym package
Sym_End()
Termination function for sym package
Sym_RegionManagerReadRegionTable()
Read region manager's region table
Sym_RegionManagerReadCounter()
Read region manager's region counter
Sym_RegionManagerIncrementCounter()
Increment region manager's region counter
Sym_RegionAlloc()
Allocate a region struct
Sym_RegionFree()
required
Sym_RegionManagerAlloc()
Allocate a region manager
Sym_RegionManagerFree()
required
Sym_RegionManagerReadSymInfo()
Find the symInfo for the given module
Sym_RegionManagerAddModuleToSymInfo()
Add a module and symInfo pair to the moduleToSymInfo table
Sym_RegionManagerDeleteModuleToSymInfo()
Delete a module-syminfo pair from moduleToSymInfo table
SymWriteOrder()
Write variable order for symInfo into a file
SymReadOrder()
Read variable order for module from a file
CommandComputeReachSet()
driver for building reached set
CommandComputeInitSet()
driver for building initial state
CommandBuildTrans()
driver for building transition relation
CommandComputePostSet()
compute the post set of a given set
CommandComputeUnion()
compute the union of two regions
CommandPrintRegion()
Print the given region
CommandDynamicVarOrdering()
Implements the dynamic_var_ordering command.
CommandWriteOrder()
Write the current ordering of the module into a file
CommandReadOrder()
Order the MDD variables of a module as specified by a file
VarBuildBddIdArray()
Gets the levels of the BDD variables corresponding to the MDD variable of a node.
VarOrdersCompareBddIdArray()
Used to sort an array of nodes in ascending order of lowest BDD level.
IntegersCompare()
Used to sort an array of integers in ascending order.
StringConvertToDynOrderType()
Converts a string to a dynamic ordering method type.
DynOrderTypeConvertToString()
Converts a dynamic ordering method type to a string.
ModuleTotalOrderVariables()
Convert an ordering of a subset of variables to a total ordering
VarOrderIsInArray()
check if a variable is in a varOrderArray
ModuleAssignMddIdsToVariables()
Create MDD variables according to the specified total ordering

symMV.c

Builds the MDDs for the multi-valued expressions.

By: Shaz Qadeer

optional

See Alsooptional

SymExprBuildMvf()
Given a parse tree for a multivalued expression compute its mvf
SymMVBuildBooleanExpressionMdd()
Given a boolean expression involving multivalued variables, build mdd for it
SymMVBuildAssignmentMdd()
Build MDD for multi valued assignment

symMddArray.c

routines to manage an array of MDDs

By: Sriram K. Rajamani

optional

See Alsooptional

SymMddArrayObtainConstant()
Obtain constant MDD array
SymMddArrayOrMdd()
Door "or" on all components of MDD array with given mdd
SymMddArrayAndMdd()
Does "and" on all components of MDD array with given mdd
SymMddArrayImpliesMddArray()
do "implies" on two MDD arrays
SymMddArrayOrMddArray()
do "or" on two MDD arrays
SymMddArrayAndMddArray()
do "and" on two MDD arrays
SymMddArrayXnorMddArray()
do "xnor" on two MDD arrays
SymMddArrayPlusMddArray()
do "add" on two MDD arrays
SymMddArrayMinusMddArray()
do "subtract" on two MDD arrays
SymMddArrayNot()
do "not" on MDD array
SymMddArrayAndComponents()
do "and" of all MDD array components
SymMddArrayCompareEqual()
do equality check on two MDD arrays
SymMddArrayCompareGreater()
do greater than check on two MDD arrays
SymMddArrayCompareLesser()
do lesser than check on two MDD arrays
SymMddArrayCompareGreaterEqual()
do greater than or equal check on two MDD arrays
SymMddArrayCompareLesserEqual()
do lesser than or equal check on two MDD arrays
SymMddArrayFree()
free MDD array
SymMddArrayPrint()
print MDD array

symUtil.c

utilities provided by sym package

By: Sriram K. Rajamani

This file contains utilities that are used both by other files of the sym package, as well as by users of sym package

See Alsosym.c

Sym_SymInfoAlloc()
Allocate and return a symInfo struct
SymRangeReadDummyId()
Utility to access a dummyId for a range
Sym_SymInfoFree()
Utility to free symInfo
Sym_MddPrintCubes()
Utility to dump mdds
Sym_MddPrintCubesImplSpec()
Utility to dump mdds
Sym_MddPrintStateForErrorTrace()
Utility to generate a state string for Tcl/Tk error trace display
Sym_MddPrintRawCubes()
Utility to dump mdds - in terms of raw mdd ids
Sym_ModuleMatchMddIds()
match mdd ids of two modules
Sym_SymInfoBuildFlatTrans()
Utility to build a flat transition relation
Sym_SymInfoReadVarToUnprimedId()
read the varToUnprimedId st_table
Sym_SymInfoReadVarToPrimedId()
read the varToPrimedId st_table
Sym_SymInfoReadUnprimedIdArray()
read the unprimedIdArray array
Sym_SymInfoReadPrimedIdArray()
read the primedIdArray array
Sym_SymInfoReadQuantifyIdArray()
read the quantifyIdArray array
Sym_SymInfoReadImgInfo()
read the image info from symInfo
Sym_SymInfoReadIdToVar()
read the idToVar table from symInfo
Sym_SymInfoSetImgInfo()
read the image info from symInfo
Sym_SymInfoReadConjuncts()
read the conjuncts from symInfo
Sym_SymInfoReadManager()
read the mdd manager from symInfo
Sym_SymInfoReadConjunctForAtom()
read the conjunct (transtion relation) for the given atom
Sym_SymInfoSetConjunctForAtom()
set the conjunct (transtion relation) for the given atom
Sym_SymInfoLookupPrimedVariableId()
lookup primed mdd id for a variable
Sym_SymInfoLookupUnprimedVariableId()
lookup unprimed mdd id for a variable
Sym_MddPickMinterm()
utility to pick a minterm form a MDD
Sym_AtomsComputePartialImage()
Compute partial image with respect to a set of atoms
Sym_AtomsBuildPartialInitialRegion()
build mdd for partial initial region
SymIsUnprimedId()
does this id belong to a primed or unprimed variable
SymCreateMddVariable()
utility to create an MDD variable
SymGetNvals()
utility to get the number of possible values of a multi valued variable
SymMddInTrueSupport()
Check if the given variable is in the true support of the given mdd
SymGetTopMddId()
get top mdd id
SymGetMddLiteral()
utility to get and MDD literal
SymGetConstant()
utility to get a constant value from an expression
SymIsNumEnumRangeConstant()
utility to check if a given expression is a num or enum or range constant
SymGetVariableId()
utility to get the mdd variable id corresponding to the expression
SymGetVariableIdConstantAndPlus()
utility to get the components of an expression of the form v + c or v - c
SymIsMultiValuedVariable()
is the given expression a multi-valued variable?
SymGetArrayElementVar()
required
SymGetArrayId()
required
SymGetArrayNvals()
required
SymInfoReadModule()
required
SymGetRelExprMdd()
required

Last updated on 980624 22h11