#include "fsmInt.h"#include "ntm.h"
Include dependency graph for fsmArdc.c:
Go to the source code of this file.
Defines | |
| #define | ARDC_MAX_LINE_LEN 4096 |
Functions | |
| static void | SortSubFsmsForApproximateTraversal (array_t **subFsmArray, array_t **fanInsIndexArray, array_t **fanOutsIndexArray, int verbosityLevel) |
| static array_t * | ArdcMbmTraversal (Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, array_t *fanOutsIndexArray, mdd_t ***subReached, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options, boolean lfpFlag) |
| static array_t * | ArdcRfbfTraversal (Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options) |
| static array_t * | ArdcTfbfTraversal (Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, mdd_t ***subReached, mdd_t ***subTo, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options) |
| static array_t * | ArdcTmbmTraversal (Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, array_t *fanOutsIndexArray, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options, boolean lfpFlag) |
| static array_t * | ArdcSimpleTraversal (Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options, int setFlag) |
| static void | ComputeFaninConstrainArray (array_t *faninConstrainArray, mdd_t **constraint, int current, array_t *fans, int decomposeFlag, int faninConstrainMode) |
| static void | MinimizeTransitionRelationWithFaninConstraint (Img_ImageInfo_t *imageInfo, array_t *faninConstrainArray, Img_MinimizeType constrainMethod, boolean reorderPtrFlag, boolean duplicate) |
| static void | ComputeConstrainedInitialStates (Fsm_Fsm_t *subFsm, array_t *faninConstrainArray, Img_MinimizeType constrainMethod) |
| static void | ComputeApproximateReachableStatesArray (mdd_manager *mddManager, array_t *reachedArray, mdd_t **reached, mdd_t ***subReached, int nSubFsms, int decomposeFlag) |
| static array_t * | ArdcCopyOverApproxReachableStatesFromExact (Fsm_Fsm_t *fsm) |
| static void | PrintCurrentReachedStates (mdd_manager *mddManager, Fsm_Fsm_t **subFsm, mdd_t **reached, Fsm_Ardc_TraversalType_t method, int nSubFsms, int iteration, int nvars, int ardcVerbosity, boolean supportCheckFlag) |
| static void | PrintBddWithName (Fsm_Fsm_t *fsm, array_t *mddIdArr, mdd_t *node) |
| static void | ArdcReadGroup (Ntk_Network_t *network, FILE *groupFile, array_t *latchNameArray, array_t *groupIndexArray) |
| static void | ArdcWriteOneGroup (Part_Subsystem_t *partitionSubsystem, FILE *groupFile, int i) |
| static void | ArdcPrintOneGroup (Part_Subsystem_t *partitionSubsystem, int i, int nLatches, array_t *fanIns, array_t *fanOuts) |
| static int | GetArdcSetIntValue (char *string, int l, int u, int defaultValue) |
| static void | ArdcEpdCountOnsetOfOverApproximateReachableStates (Fsm_Fsm_t *fsm, EpDouble *epd) |
| static mdd_t * | QuantifyVariables (mdd_t *state, array_t *smoothArray, mdd_t *smoothCube) |
| static void | UpdateMbmEventSchedule (Fsm_Fsm_t **subFsm, array_t *fanOutIndices, int *traverse, int lfpFlag) |
| static void | PrintTfmStatistics (array_t *subFsmArray) |
| void | Fsm_ArdcMinimizeTransitionRelation (Fsm_Fsm_t *fsm, Img_DirectionType fwdbwd) |
| mdd_t * | Fsm_ArdcComputeImage (Fsm_Fsm_t *fsm, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) |
| array_t * | Fsm_FsmComputeOverApproximateReachableStates (Fsm_Fsm_t *fsm, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, int recompute) |
| array_t * | Fsm_ArdcComputeOverApproximateReachableStates (Fsm_Fsm_t *fsm, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, int recompute, Fsm_ArdcOptions_t *options) |
| array_t * | Fsm_ArdcDecomposeStateSpace (Ntk_Network_t *network, array_t *presentStateVars, array_t *nextStateFunctions, Fsm_ArdcOptions_t *options) |
| Fsm_ArdcOptions_t * | Fsm_ArdcAllocOptionsStruct (void) |
| void | Fsm_ArdcGetDefaultOptions (Fsm_ArdcOptions_t *options) |
| Fsm_Ardc_TraversalType_t | Fsm_ArdcOptionsReadTraversalMethod (Fsm_ArdcOptions_t *options) |
| int | Fsm_ArdcOptionsReadGroupSize (Fsm_ArdcOptions_t *options) |
| float | Fsm_ArdcOptionsReadAffinityFactor (Fsm_ArdcOptions_t *options) |
| Img_MinimizeType | Fsm_ArdcOptionsReadConstrainMethod (Fsm_ArdcOptions_t *options) |
| Fsm_Ardc_ConstrainTargetType_t | Fsm_ArdcOptionsReadConstrainTarget (Fsm_ArdcOptions_t *options) |
| int | Fsm_ArdcOptionsReadMaxIteration (Fsm_ArdcOptions_t *options) |
| Fsm_Ardc_AbstPpiType_t | Fsm_ArdcOptionsReadAbstractPseudoInput (Fsm_ArdcOptions_t *options) |
| boolean | Fsm_ArdcOptionsReadDecomposeFlag (Fsm_ArdcOptions_t *options) |
| boolean | Fsm_ArdcOptionsReadProjectedInitialFlag (Fsm_ArdcOptions_t *options) |
| boolean | Fsm_ArdcOptionsReadConstrainReorderFlag (Fsm_ArdcOptions_t *options) |
| Img_MethodType | Fsm_ArdcOptionsReadImageMethod (Fsm_ArdcOptions_t *options) |
| boolean | Fsm_ArdcOptionsReadUseHighDensity (Fsm_ArdcOptions_t *options) |
| int | Fsm_ArdcOptionsReadVerbosity (Fsm_ArdcOptions_t *options) |
| void | Fsm_ArdcOptionsSetTraversalMethod (Fsm_ArdcOptions_t *options, Fsm_Ardc_TraversalType_t traversalMethod) |
| void | Fsm_ArdcOptionsSetGroupSize (Fsm_ArdcOptions_t *options, int groupSize) |
| void | Fsm_ArdcOptionsSetAffinityFactor (Fsm_ArdcOptions_t *options, float affinityFactor) |
| void | Fsm_ArdcOptionsSetConstrainMethod (Fsm_ArdcOptions_t *options, Img_MinimizeType constrainMethod) |
| void | Fsm_ArdcOptionsSetConstrainTarget (Fsm_ArdcOptions_t *options, Fsm_Ardc_ConstrainTargetType_t constrainTarget) |
| void | Fsm_ArdcOptionsSetMaxIteration (Fsm_ArdcOptions_t *options, int maxIteration) |
| void | Fsm_ArdcOptionsSetAbstractPseudoInput (Fsm_ArdcOptions_t *options, Fsm_Ardc_AbstPpiType_t abstractPseudoInput) |
| void | Fsm_ArdcOptionsSetDecomposeFlag (Fsm_ArdcOptions_t *options, boolean decomposeFlag) |
| void | Fsm_ArdcOptionsSetProjectedInitialFlag (Fsm_ArdcOptions_t *options, boolean projectedInitialFlag) |
| void | Fsm_ArdcOptionsSetConstrainReorderFlag (Fsm_ArdcOptions_t *options, int constrainReorderFlag) |
| void | Fsm_ArdcOptionsSetImageMethod (Fsm_ArdcOptions_t *options, Img_MethodType ardcImageMethod) |
| void | Fsm_ArdcOptionsSetUseHighDensity (Fsm_ArdcOptions_t *options, boolean useHighDensity) |
| void | Fsm_ArdcOptionsSetVerbosity (Fsm_ArdcOptions_t *options, int verbosity) |
| double | Fsm_ArdcCountOnsetOfOverApproximateReachableStates (Fsm_Fsm_t *fsm) |
| int | Fsm_ArdcBddSizeOfOverApproximateReachableStates (Fsm_Fsm_t *fsm) |
| mdd_t * | Fsm_ArdcGetMddOfOverApproximateReachableStates (Fsm_Fsm_t *fsm) |
| void | Fsm_ArdcPrintReachabilityResults (Fsm_Fsm_t *fsm, long elapseTime) |
| int | Fsm_ArdcReadVerbosity (void) |
| int | FsmArdcCheckInvariant (Fsm_Fsm_t *fsm, array_t *invarStates) |
| void | FsmArdcPrintOptions (void) |
| void | FsmArdcPrintOverApproximateReachableStates (Fsm_Fsm_t *fsm) |
| void | FsmArdcPrintExactReachableStates (Fsm_Fsm_t *fsm) |
| void | FsmArdcPrintBddOfNode (Fsm_Fsm_t *fsm, mdd_t *node) |
| void | FsmArdcPrintArrayOfArrayInt (array_t *arrayOfArray) |
| boolean | FsmGetArdcSetBooleanValue (char *string, boolean defaultValue) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: fsmArdc.c,v 1.86 2009/04/12 00:44:04 fabio Exp $" |
Define Documentation
Function Documentation
| static array_t * ArdcCopyOverApproxReachableStatesFromExact | ( | Fsm_Fsm_t * | fsm | ) | [static] |
Function********************************************************************
Synopsis [Copy exact reached states to overapproximate.]
Description [Copy exact reached states to overapproximate.]
SideEffects []
SeeAlso []
Definition at line 3946 of file fsmArdc.c.
{
array_t *reachableStatesArray;
if (Fsm_FsmReadReachableStates(fsm) == NIL(mdd_t))
return(NIL(array_t));
reachableStatesArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, reachableStatesArray,
mdd_dup(Fsm_FsmReadReachableStates(fsm)));
FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Exact_c);
fsm->reachabilityInfo.apprReachableStates = reachableStatesArray;
fsm->reachabilityInfo.subPsVars = array_alloc(array_t *, 0);
array_insert_last(array_t *, fsm->reachabilityInfo.subPsVars,
array_dup(fsm->fsmData.presentStateVars));
return(reachableStatesArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void ArdcEpdCountOnsetOfOverApproximateReachableStates | ( | Fsm_Fsm_t * | fsm, |
| EpDouble * | epd | ||
| ) | [static] |
Function********************************************************************
Synopsis [Returns the number of approximate reachable states of an FSM.]
Description [Returns the number of approximate reachable states of an FSM.]
SideEffects []
SeeAlso []
Definition at line 4264 of file fsmArdc.c.
{
mdd_t *reached;
array_t *psVars, *reachedArray;
mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
double tmpReached;
int i;
EpdMakeZero(epd, 0);
if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm))
return;
EpdConvert((double)1.0, epd);
reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm);
arrayForEachItem(mdd_t *, reachedArray, i, reached) {
psVars = array_fetch(array_t *, fsm->reachabilityInfo.subPsVars, i);
tmpReached = mdd_count_onset(mddManager, reached, psVars);
EpdMultiply(epd, tmpReached);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static array_t * ArdcMbmTraversal | ( | Fsm_Fsm_t * | fsm, |
| int | nvars, | ||
| array_t * | subFsmArray, | ||
| array_t * | fanInsIndexArray, | ||
| array_t * | fanOutsIndexArray, | ||
| mdd_t *** | subReached, | ||
| int | incrementalFlag, | ||
| int | verbosityLevel, | ||
| int | printStep, | ||
| int | depthValue, | ||
| int | shellFlag, | ||
| int | reorderFlag, | ||
| int | reorderThreshold, | ||
| Fsm_RchType_t | approxFlag, | ||
| Fsm_ArdcOptions_t * | options, | ||
| boolean | lfpFlag | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes an upper bound to the reachable states of an FSM by MBM.]
Description [Computes an upper bound to the reachable states of an FSM by MBM or LMBM. This computation proceeds in an event-driven manner. First it computes the reachable states of all submachines, then only for those submachines such that any of their fanin submachine's reachable states have changed. It recomputes reachable states by constraining the transition relation with respect to the reached states of all fanin submachines. This is iterated until it converges. The basic algorithm for MBM is almost same as the one in Hyunwoo Cho's paper in TCAD96, except as noted below. 0. Cho's algorithm uses transition function for image computation, whereas we use either the transition function or the transition relation depending on the image computation method. 1. constrainTarget In Cho's papers, there are two versions of algorithms: one is constraining transition relation, the other is initial states, so this function includes these two as well as the case of both. 0) Fsm_Ardc_Constrain_Tr_c : constrain transition relation (default). 1) Fsm_Ardc_Constrain_Initial_c : constrain initial state. 2) Fsm_Ardc_Constrain_Both_c : constrain both. 2. decomposeFlag To perform the above constraining operation, we can make the constraint either conjoined (as single bdd) or decomposed (as array of bdds) from the reachable states of fanin submachines of the current submachine. To have same interface for these two, array of constraints is used. 3. dynamic variable reordering In Cho's algorithm, dynamic variable ordering is not allowed, but it is here. Also, refer to 5. (restore-containment). 4. abstractPseudoInput To make faster convergence, we can abstract pseudo primary input variables early, but refer to 5. (restore-containment). 0) Fsm_Ardc_Abst_Ppi_No_c : do not abstract pseudo-input variables. 1) Fsm_Ardc_Abst_Ppi_Before_Image_c : abstract before image computation (default). 2) Fsm_Ardc_Abst_Ppi_After_Image_c : abstract after image computation. 3) Fsm_Ardc_Abst_Ppi_At_End_c : abstract at the end of approximate traversal. 5. restore-constainment Due to 3 (dynamic variable reordering) and 4 (abstractPseudoInput), current reachable states may not be a subset of previous reachable states. In this case, we correct current reachable state to the intersection of current and previous reachable states. But, in FBF, we need to take the union of the two. 6. projectedInitialFlag When we do reachability analysis of submachines, initial states of a submachine can be one of the following. In Cho's paper, projected initial states was used. 0) FALSE : use original initial states for submachine 1) TRUE : use projected initial states for submachine (default) ]
SideEffects []
SeeAlso [ArdcRfbfTraversal ArdcTfbfTraversal ArdcTmbmTraversal ArdcSimpleTraversal]
Definition at line 2401 of file fsmArdc.c.
{
mdd_manager *mddManager;
int i, n = array_n(subFsmArray);
int *traverse;
mdd_t **reached, **constraint;
mdd_t **oldReached;
mdd_t **frontier;
int converged = 0;
Fsm_Fsm_t **subFsm;
array_t *fans;
mdd_t *tmp;
int iteration = 0;
mdd_t **initial = NIL(mdd_t *);
array_t *reachedArray = array_alloc(mdd_t *, 0);
array_t *faninConstrainArray;
Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t);
int dynStatus;
bdd_reorder_type_t dynMethod;
boolean restoreContainmentFlag;
boolean reuseTrFlag = FALSE;
/* If set, just update the transition relation
without copying the original transition relation */
boolean reused = FALSE;
boolean duplicate;
boolean tmpReorderPtrFlag;
int nConstrainOps = 0;
long tImgComps = 0;
long tConstrainOps = 0;
long tRestoreContainment = 0;
long tAbstractVars = 0;
long tBuildTr = 0;
long initialTime = 0, finalTime;
int maxIteration = options->maxIteration;
int constrainTarget = options->constrainTarget;
boolean decomposeFlag = options->decomposeFlag;
int abstractPseudoInput = options->abstractPseudoInput;
Img_MinimizeType constrainMethod = options->constrainMethod;
boolean projectedInitialFlag = options->projectedInitialFlag;
int ardcVerbosity = options->verbosity;
boolean constrainReorderFlag = options->constrainReorderFlag;
boolean reorderPtrFlag = options->reorderPtrFlag;
int faninConstrainMode = options->faninConstrainMode;
int lmbmInitialStatesMode = options->lmbmInitialStatesMode;
reuseTrFlag = FsmGetArdcSetBooleanValue("ardc_mbm_reuse_tr", reuseTrFlag);
if (reuseTrFlag && lfpFlag) {
/* This is to use the i-th constrained transition relation in
* the (i+1)-th iteration, instead of the original transition relation.
* Therefore, the i-th constraint should be a superset of the (i+1)-th. */
fprintf(vis_stderr,
"** ardc error : can't reuse transition relation in LMBM. **\n");
reuseTrFlag = FALSE;
}
Img_ResetNumberOfImageComputation(Img_Forward_c);
reached = ALLOC(mdd_t *, n);
constraint = ALLOC(mdd_t *, n);
traverse = ALLOC(int, n); /* array used for scheduling */
subFsm = ALLOC(Fsm_Fsm_t *, n);
oldReached = ALLOC(mdd_t *, n);
mddManager = Fsm_FsmReadMddManager(fsm);
for (i = 0; i < n; i++) {
subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
oldReached[i] = NIL(mdd_t);
}
/* Set up. */
if (lfpFlag) { /* LMBM */
initial = ALLOC(mdd_t *, n);
for (i = 0; i < n; i++)
initial[i] = Fsm_FsmComputeInitialStates(subFsm[i]);
if (lmbmInitialStatesMode >= 1) /* restart from frontier states */
frontier = ALLOC(mdd_t *, n);
else
frontier = NIL(mdd_t *);
for (i = 0; i < n; i++) {
reached[i] = mdd_dup(initial[i]);
constraint[i] = mdd_dup(initial[i]);
traverse[i] = 1;
if (frontier)
frontier[i] = NIL(mdd_t);
}
} else { /* MBM */
for (i = 0; i < n; i++) {
reached[i] = mdd_one(mddManager);
constraint[i] = mdd_one(mddManager);
traverse[i] = 1;
}
if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
constrainTarget == Fsm_Ardc_Constrain_Both_c) {
initial = ALLOC(mdd_t *, n);
for (i = 0; i < n; i++)
initial[i] = Fsm_FsmComputeInitialStates(subFsm[i]);
}
frontier = NIL(mdd_t *);
}
/* Set the flag for containment restoration according to the options. */
if (constrainMethod == Img_Constrain_c &&
constrainReorderFlag == FALSE &&
abstractPseudoInput == Fsm_Ardc_Abst_Ppi_No_c) {
restoreContainmentFlag = FALSE;
} else
restoreContainmentFlag = TRUE;
/* Compute fixpoint. */
do {
converged = 1;
for (i = 0; i < n; i++) {
if (!traverse[i])
continue;
if (ardcVerbosity > 1)
fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
if (oldReached[i])
mdd_free(oldReached[i]);
oldReached[i] = reached[i];
/* Build constraint array. */
faninConstrainArray = array_alloc(mdd_t *, 0);
fans = array_fetch(array_t *, fanInsIndexArray, i);
ComputeFaninConstrainArray(faninConstrainArray, constraint,
i, fans, decomposeFlag, faninConstrainMode);
/* Build constrained transition relation. */
dynStatus = bdd_reordering_status(mddManager, &dynMethod);
if (dynStatus != 0 && constrainReorderFlag == 0)
bdd_dynamic_reordering_disable(mddManager);
if (ardcVerbosity > 0)
initialTime = util_cpu_time();
imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1); /* forward */
if (ardcVerbosity > 0) {
finalTime = util_cpu_time();
tBuildTr += finalTime - initialTime;
}
/* Minimize the transition relation of the current submachine w.r.t.
* the reached set of its fanin submachines.
*/
if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) {
int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
if (ardcVerbosity > 2)
Img_SetPrintMinimizeStatus(imageInfo, 2);
else if (ardcVerbosity > 0)
Img_SetPrintMinimizeStatus(imageInfo, 1);
else
Img_SetPrintMinimizeStatus(imageInfo, 0);
if (reuseTrFlag) {
if (reused)
duplicate = FALSE;
else
duplicate = TRUE;
} else
duplicate = TRUE;
if (reorderPtrFlag &&
abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) {
tmpReorderPtrFlag = 1;
} else
tmpReorderPtrFlag = 0;
if (ardcVerbosity > 0)
initialTime = util_cpu_time();
MinimizeTransitionRelationWithFaninConstraint(imageInfo,
faninConstrainArray, constrainMethod, tmpReorderPtrFlag,
duplicate);
if (ardcVerbosity > 0) {
finalTime = util_cpu_time();
tConstrainOps += finalTime - initialTime;
}
Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
}
if (constrainTarget != Fsm_Ardc_Constrain_Tr_c) {
ComputeConstrainedInitialStates(subFsm[i], faninConstrainArray,
constrainMethod);
}
nConstrainOps++;
mdd_array_free(faninConstrainArray);
/* Restore dynamic reordering options if they had been changed. */
if (dynStatus != 0 && constrainReorderFlag == 0) {
bdd_dynamic_reordering(mddManager, dynMethod,
BDD_REORDER_VERBOSITY_DEFAULT);
}
/* Quantify pseudo-input variables from the transition relation. */
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
if (ardcVerbosity > 2)
Img_SetPrintMinimizeStatus(imageInfo, 2);
else if (ardcVerbosity > 0)
Img_SetPrintMinimizeStatus(imageInfo, 1);
else
Img_SetPrintMinimizeStatus(imageInfo, 0);
if (ardcVerbosity > 0)
initialTime = util_cpu_time();
Img_AbstractTransitionRelation(imageInfo,
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube, Img_Forward_c);
if (reorderPtrFlag)
Img_ReorderPartitionedTransitionRelation(imageInfo, Img_Forward_c);
if (ardcVerbosity > 0) {
finalTime = util_cpu_time();
tAbstractVars += finalTime - initialTime;
}
Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
}
if (lfpFlag && lmbmInitialStatesMode > 0 && iteration > 0) {
/* Update the initial states to either reached or frontier. */
FsmSetReachabilityApproxComputationStatus(subFsm[i], Fsm_Rch_Under_c);
mdd_free(subFsm[i]->reachabilityInfo.initialStates);
if (lmbmInitialStatesMode == 1)
subFsm[i]->reachabilityInfo.initialStates = mdd_dup(reached[i]);
else
subFsm[i]->reachabilityInfo.initialStates = mdd_dup(frontier[i]);
} else {
/* Reset the reachable states for a new reachability. */
if (subFsm[i]->reachabilityInfo.reachableStates) {
mdd_free(subFsm[i]->reachabilityInfo.reachableStates);
subFsm[i]->reachabilityInfo.reachableStates = NIL(mdd_t);
}
subFsm[i]->reachabilityInfo.depth = 0;
}
/* Traverse this submachine. */
if (ardcVerbosity > 0)
initialTime = util_cpu_time();
reached[i] = Fsm_FsmComputeReachableStates(subFsm[i],
incrementalFlag, verbosityLevel, printStep, depthValue,
shellFlag, reorderFlag, reorderThreshold,
approxFlag, 0, 0, NIL(array_t), FALSE, NIL(array_t));
if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
Img_TfmFlushCache(imageInfo, FALSE);
}
if (ardcVerbosity > 0) {
finalTime = util_cpu_time();
tImgComps += finalTime - initialTime;
}
/* Compute the frontier for LMBM. */
if (lfpFlag && lmbmInitialStatesMode > 0) {
if (lmbmInitialStatesMode >= 1) {
if (iteration == 0)
frontier[i] = mdd_dup(reached[i]);
else {
mdd_t *fromLowerBound;
fromLowerBound = mdd_and(reached[i], oldReached[i], 1, 0);
tmp = reached[i];
reached[i] = mdd_or(oldReached[i], tmp, 1, 1);
mdd_free(tmp);
mdd_free(frontier[i]);
if (lmbmInitialStatesMode == 2) {
frontier[i] = bdd_between(fromLowerBound, reached[i]);
mdd_free(fromLowerBound);
} else
frontier[i] = fromLowerBound;
}
}
if (iteration > 0) {
mdd_free(subFsm[i]->reachabilityInfo.initialStates);
subFsm[i]->reachabilityInfo.initialStates = mdd_dup(initial[i]);
}
}
/* Restore the original transition relation. */
if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) {
if (!reuseTrFlag)
Img_RestoreTransitionRelation(imageInfo, Img_Forward_c);
}
/* Quantify the pseudo-input variables from reached. */
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) {
if (ardcVerbosity > 0)
initialTime = util_cpu_time();
if (n > 1) {
tmp = reached[i];
reached[i] = QuantifyVariables(reached[i],
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube);
mdd_free(tmp);
}
if (ardcVerbosity > 0) {
finalTime = util_cpu_time();
tAbstractVars += finalTime - initialTime;
}
}
mdd_free(constraint[i]);
constraint[i] = mdd_dup(reached[i]);
/* Update traversal schedule and possibly restore containment. */
traverse[i] = 0;
if (!mdd_equal(oldReached[i], reached[i])) {
if (ardcVerbosity > 2) {
double r1, r2;
r1 = mdd_count_onset(mddManager, reached[i],
subFsm[i]->fsmData.presentStateVars);
r2 = mdd_count_onset(mddManager, oldReached[i],
subFsm[i]->fsmData.presentStateVars);
fprintf(vis_stdout, "oldReached = %g, reached = %g\n", r2, r1);
}
/* Restore-containment operation. */
if (restoreContainmentFlag) {
if (ardcVerbosity > 0)
initialTime = util_cpu_time();
if (lfpFlag) { /* LMBM */
if (mdd_lequal(oldReached[i], reached[i], 1, 1)) {
/* Containment OK. */
fans = array_fetch(array_t *, fanOutsIndexArray, i);
UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag);
} else {
/* Restoration needed. */
if (ardcVerbosity > 1) {
fprintf(vis_stdout,
"** ardc info: reached is not superset of oldReached in subFsm[%d] **\n",
i);
}
mdd_free(reached[i]);
reached[i] = mdd_or(oldReached[i],
subFsm[i]->reachabilityInfo.reachableStates, 1, 1);
mdd_free(subFsm[i]->reachabilityInfo.reachableStates);
subFsm[i]->reachabilityInfo.reachableStates = mdd_dup(reached[i]);
mdd_free(constraint[i]);
constraint[i] = mdd_dup(reached[i]);
if (!mdd_equal(oldReached[i], reached[i])) {
fans = array_fetch(array_t *, fanOutsIndexArray, i);
UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag);
}
}
} else { /* MBM */
if (!mdd_lequal(reached[i], oldReached[i], 1, 1)) {
/* Restoration needed. */
if (ardcVerbosity > 1) {
fprintf(vis_stdout,
"** ardc info: reached is not subset of oldReached in subFsm[%d] **\n", i);
}
mdd_free(reached[i]);
reached[i] = mdd_and(oldReached[i],
subFsm[i]->reachabilityInfo.reachableStates, 1, 1);
mdd_free(subFsm[i]->reachabilityInfo.reachableStates);
subFsm[i]->reachabilityInfo.reachableStates = mdd_dup(reached[i]);
mdd_free(constraint[i]);
constraint[i] = mdd_dup(reached[i]);
if (!mdd_equal(oldReached[i], reached[i])) {
fans = array_fetch(array_t *, fanOutsIndexArray, i);
UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag);
}
} else {
/* Containment OK. */
fans = array_fetch(array_t *, fanOutsIndexArray, i);
UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag);
}
}
if (ardcVerbosity > 0) {
finalTime = util_cpu_time();
tRestoreContainment += finalTime - initialTime;
}
} else { /* no containment restoration needed */
fans = array_fetch(array_t *, fanOutsIndexArray, i);
UpdateMbmEventSchedule(subFsm, fans, traverse, lfpFlag);
}
}
}
/* Check for convergence. */
for (i = 0; i < n; i++) {
if (traverse[i]) {
converged = 0;
break;
}
}
iteration++;
if (ardcVerbosity > 0) {
boolean supportCheckFlag = FALSE;
/* Print the current reached states and check the supports. */
if (projectedInitialFlag ||
abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
supportCheckFlag = TRUE;
}
if (lfpFlag) {
PrintCurrentReachedStates(mddManager, subFsm, reached,
Fsm_Ardc_Traversal_Lmbm_c,
n, iteration, nvars, ardcVerbosity,
supportCheckFlag);
} else {
PrintCurrentReachedStates(mddManager, subFsm, reached,
Fsm_Ardc_Traversal_Mbm_c,
n, iteration, nvars, ardcVerbosity,
supportCheckFlag);
}
}
if (iteration == maxIteration)
break;
} while (!converged);
/* Restore the original transtion relation. */
if (reuseTrFlag) {
if (constrainTarget != Fsm_Ardc_Constrain_Initial_c)
Img_RestoreTransitionRelation(imageInfo, Img_Forward_c);
}
if (ardcVerbosity > 0) {
if (lfpFlag)
fprintf(vis_stdout, "LMBM : total iterations %d\n", iteration);
else
fprintf(vis_stdout, "MBM : total iterations %d\n", iteration);
}
/* Reset the initial states to the original. */
if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
constrainTarget == Fsm_Ardc_Constrain_Both_c || lfpFlag) {
for (i = 0; i < n; i++) {
mdd_free(subFsm[i]->reachabilityInfo.initialStates);
subFsm[i]->reachabilityInfo.initialStates = initial[i];
}
FREE(initial);
}
/* Quantify the pseudo-input variables from reached. */
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) {
if (ardcVerbosity > 0)
initialTime = util_cpu_time();
for (i = 0; i < n; i++) {
tmp = reached[i];
reached[i] = QuantifyVariables(reached[i],
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube);
mdd_free(tmp);
}
if (ardcVerbosity > 0) {
finalTime = util_cpu_time();
tAbstractVars += finalTime - initialTime;
}
}
/* Set the status of current overapproximate reached states. */
if (converged)
FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c);
else if (lfpFlag)
FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c);
else
FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Valid_c);
ComputeApproximateReachableStatesArray(mddManager, reachedArray,
reached, subReached, n,
decomposeFlag);
/* Clean up. */
if (decomposeFlag) {
for (i = 0; i < n; i++) {
mdd_free(oldReached[i]);
mdd_free(constraint[i]);
}
} else {
for (i = 0; i < n; i++) {
mdd_free(oldReached[i]);
if (subReached == NULL)
mdd_free(reached[i]);
mdd_free(constraint[i]);
}
}
if (subReached)
*subReached = reached;
else
FREE(reached);
FREE(traverse);
FREE(constraint);
FREE(subFsm);
FREE(oldReached);
if (lfpFlag && lmbmInitialStatesMode >= 1) {/*consistent:from >1 to >=1 C.W*/
for (i = 0; i < n; i++) {
if (frontier[i])
mdd_free(frontier[i]);
}
FREE(frontier);
}
/* Print final stats. */
if (ardcVerbosity > 0) {
fprintf(vis_stdout, "%d image computations, %d constrain operations\n",
Img_GetNumberOfImageComputation(Img_Forward_c), nConstrainOps);
fprintf(vis_stdout,
"image computation time = %g, constrain operation time = %g\n",
(double)tImgComps / 1000.0, (double)tConstrainOps / 1000.0);
fprintf(vis_stdout, "restore-containment time = %g\n",
(double)tRestoreContainment / 1000.0);
fprintf(vis_stdout, "abstract variables time = %g\n",
(double)tAbstractVars / 1000.0);
fprintf(vis_stdout, "build TR time = %g\n",
(double)tBuildTr / 1000.0);
}
return(reachedArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void ArdcPrintOneGroup | ( | Part_Subsystem_t * | partitionSubsystem, |
| int | i, | ||
| int | nLatches, | ||
| array_t * | fanIns, | ||
| array_t * | fanOuts | ||
| ) | [static] |
Function********************************************************************
Synopsis [Prints one grouping information.]
Description [Prints one grouping information.]
SideEffects []
SeeAlso []
Definition at line 4188 of file fsmArdc.c.
{
int j, k;
st_generator *stGen;
st_table *vertexNameTable;
char *latchName;
fprintf(vis_stdout, "SUB-FSM [%d]\n", i);
fprintf(vis_stdout, "== latches(%d) :", nLatches);
vertexNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
st_foreach_item(vertexNameTable, stGen, &latchName, NIL(char *)) {
fprintf(vis_stdout, " %s", latchName);
}
fprintf(vis_stdout, "\n");
fprintf(vis_stdout, "== fanins(%d) :", array_n(fanIns));
for (j = 0; j < array_n(fanIns); j++) {
k = array_fetch(int, fanIns, j);
fprintf(vis_stdout, " %d", k);
}
fprintf(vis_stdout, "\n");
fprintf(vis_stdout, "== fanouts(%d) :", array_n(fanOuts));
for (j = 0; j < array_n(fanOuts); j++) {
k = array_fetch(int, fanOuts, j);
fprintf(vis_stdout, " %d", k);
}
fprintf(vis_stdout, "\n");
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void ArdcReadGroup | ( | Ntk_Network_t * | network, |
| FILE * | groupFile, | ||
| array_t * | latchNameArray, | ||
| array_t * | groupIndexArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Reads grouping information.]
Description [Reads grouping information.]
SideEffects []
SeeAlso []
Definition at line 4118 of file fsmArdc.c.
{
char line[ARDC_MAX_LINE_LEN];
char *latchName, *name, *group;
int groupIndex = 0;
while (fgets(line, ARDC_MAX_LINE_LEN, groupFile)) {
if (strlen(line) == 0)
continue;
if (line[0] == '#')
continue;
if (line[strlen(line) - 1] == '\n')
line[strlen(line) - 1] = '\0';
group = strtok(line, " ");
if (strncmp(group, "GROUP[", 6) == 0)
sscanf(group, "GROUP[%d]:", &groupIndex);
else {
latchName = util_strsav(group);
array_insert_last(char *, latchNameArray, latchName);
array_insert_last(int, groupIndexArray, groupIndex);
}
while ((name = strtok(NIL(char), " \t")) != NIL(char)) {
latchName = util_strsav(name);
array_insert_last(char *, latchNameArray, latchName);
array_insert_last(int, groupIndexArray, groupIndex);
}
}
}
Here is the caller graph for this function:
| static array_t * ArdcRfbfTraversal | ( | Fsm_Fsm_t * | fsm, |
| int | nvars, | ||
| array_t * | subFsmArray, | ||
| array_t * | fanInsIndexArray, | ||
| int | incrementalFlag, | ||
| int | verbosityLevel, | ||
| int | printStep, | ||
| int | depthValue, | ||
| int | shellFlag, | ||
| int | reorderFlag, | ||
| int | reorderThreshold, | ||
| Fsm_RchType_t | approxFlag, | ||
| Fsm_ArdcOptions_t * | options | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes an upperbound of an FSM by RFBF.]
Description [Computes an upperbound of an FSM by RFBF. It first sets all constraints to initial states, then does one image computation, then updates constraints with reached states. This is iteratively done until it gets converged. Refer the description of ArdcMbmTraversal(MBM).]
SideEffects []
SeeAlso [ArdcMbmTraversal ArdcTfbfTraversal ArdcTmbmTraversal ArdcSimpleTraversal]
Definition at line 2931 of file fsmArdc.c.
{
mdd_manager *mddManager;
int i, n = array_n(subFsmArray);
mdd_t **reached, **constraint, **newConstraint;
mdd_t **newReached, *to;
int converged = 0;
Fsm_Fsm_t **subFsm;
array_t *fans;
mdd_t *tmp;
mdd_t *initialStates;
int iteration = 0;
mdd_t **initial = NIL(mdd_t *);
array_t *reachedArray = array_alloc(mdd_t *, 0);
array_t *faninConstrainArray;
Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t);
int dynStatus;
bdd_reorder_type_t dynMethod;
boolean restoreContainmentFlag;
mdd_t *toCareSet;
array_t *toCareSetArray = array_alloc(mdd_t *, 0);
int depth = 0;
boolean tmpReorderPtrFlag;
long tImgComps = 0;
long tConstrainOps = 0;
long initialTime = 0, finalTime;
int maxIteration = options->maxIteration;
int constrainTarget = options->constrainTarget;
boolean decomposeFlag = options->decomposeFlag;
int abstractPseudoInput = options->abstractPseudoInput;
Img_MinimizeType constrainMethod = options->constrainMethod;
boolean projectedInitialFlag = options->projectedInitialFlag;
int ardcVerbosity = options->verbosity;
boolean constrainReorderFlag = options->constrainReorderFlag;
boolean reorderPtrFlag = options->reorderPtrFlag;
int faninConstrainMode = options->faninConstrainMode;
Img_ResetNumberOfImageComputation(Img_Forward_c);
reached = ALLOC(mdd_t *, n);
constraint = ALLOC(mdd_t *, n);
newConstraint = ALLOC(mdd_t *, n);
subFsm = ALLOC(Fsm_Fsm_t *, n);
newReached = ALLOC(mdd_t *, n);
mddManager = Fsm_FsmReadMddManager(fsm);
for (i = 0; i < n; i++) {
subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
initialStates = Fsm_FsmComputeInitialStates(subFsm[i]);
reached[i] = initialStates;
constraint[i] = mdd_dup(initialStates);
if (printStep && ((depth % printStep) == 0)) {
if (ardcVerbosity > 1)
fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
(void)fprintf(vis_stdout,
"BFS step = %d\t|states| = %8g\tBdd size = %8ld\n", depth,
mdd_count_onset(mddManager, reached[i],
subFsm[i]->fsmData.presentStateVars),
(long)mdd_size(reached[i]));
}
}
if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
constrainTarget == Fsm_Ardc_Constrain_Both_c) {
initial = ALLOC(mdd_t *, n);
for (i = 0; i < n; i++)
initial[i] = mdd_dup(reached[i]);
}
if (constrainMethod != Img_Constrain_c ||
constrainReorderFlag == TRUE ||
abstractPseudoInput != Fsm_Ardc_Abst_Ppi_No_c) {
restoreContainmentFlag = TRUE;
} else
restoreContainmentFlag = FALSE;
converged = 0;
do {
depth++;
for (i = 0; i < n; i++) {
if (ardcVerbosity > 1)
fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
faninConstrainArray = array_alloc(mdd_t *, 0);
fans = array_fetch(array_t *, fanInsIndexArray, i);
ComputeFaninConstrainArray(faninConstrainArray, constraint,
i, fans, decomposeFlag, faninConstrainMode);
dynStatus = bdd_reordering_status(mddManager, &dynMethod);
if (dynStatus != 0 && constrainReorderFlag == 0)
bdd_dynamic_reordering_disable(mddManager);
imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1);
if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) {
int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
if (ardcVerbosity > 2)
Img_SetPrintMinimizeStatus(imageInfo, 2);
else if (ardcVerbosity > 0)
Img_SetPrintMinimizeStatus(imageInfo, 1);
else
Img_SetPrintMinimizeStatus(imageInfo, 0);
if (reorderPtrFlag &&
abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) {
tmpReorderPtrFlag = 1;
} else
tmpReorderPtrFlag = 0;
if (ardcVerbosity > 0)
initialTime = util_cpu_time();
MinimizeTransitionRelationWithFaninConstraint(imageInfo,
faninConstrainArray, constrainMethod, tmpReorderPtrFlag,
TRUE);
if (ardcVerbosity > 0) {
finalTime = util_cpu_time();
tConstrainOps += finalTime - initialTime;
}
Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
}
if (constrainTarget != Fsm_Ardc_Constrain_Tr_c) {
ComputeConstrainedInitialStates(subFsm[i], faninConstrainArray,
constrainMethod);
}
mdd_array_free(faninConstrainArray);
if (dynStatus != 0 && constrainReorderFlag == 0) {
bdd_dynamic_reordering(mddManager, dynMethod,
BDD_REORDER_VERBOSITY_DEFAULT);
}
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
if (ardcVerbosity > 2)
Img_SetPrintMinimizeStatus(imageInfo, 2);
else if (ardcVerbosity > 0)
Img_SetPrintMinimizeStatus(imageInfo, 1);
else
Img_SetPrintMinimizeStatus(imageInfo, 0);
Img_AbstractTransitionRelation(imageInfo,
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube, Img_Forward_c);
if (reorderPtrFlag)
Img_ReorderPartitionedTransitionRelation(imageInfo, Img_Forward_c);
Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
}
toCareSet = mdd_not(reached[i]);
array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
if (ardcVerbosity > 0)
initialTime = util_cpu_time();
to = Fsm_ArdcComputeImage(subFsm[i], reached[i], reached[i],
toCareSetArray);
if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
Img_TfmFlushCache(imageInfo, FALSE);
}
if (ardcVerbosity > 0) {
finalTime = util_cpu_time();
tImgComps += finalTime - initialTime;
}
mdd_free(toCareSet);
newReached[i] = mdd_or(reached[i], to, 1, 1);
mdd_free(to);
if (constrainTarget != Fsm_Ardc_Constrain_Initial_c)
Img_RestoreTransitionRelation(imageInfo, Img_Forward_c);
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) {
tmp = newReached[i];
newReached[i] = QuantifyVariables(newReached[i],
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube);
mdd_free(tmp);
}
/* restore-containment operation */
if (restoreContainmentFlag) {
if (!mdd_lequal(reached[i], newReached[i], 1, 1)) {
if (ardcVerbosity > 2) {
double r1, r2;
fprintf(vis_stdout,
"** ardc warning : newReached is not superset of reached in subFsm[%d] **\n",
i);
r1 = mdd_count_onset(mddManager, reached[i],
subFsm[i]->fsmData.presentStateVars);
r2 = mdd_count_onset(mddManager, newReached[i],
subFsm[i]->fsmData.presentStateVars);
fprintf(vis_stdout, "reached = %g, newReached = %g\n", r1, r2);
}
tmp = newReached[i];
newReached[i] = mdd_or(newReached[i], reached[i], 1, 1);
mdd_free(tmp);
}
}
newConstraint[i] = mdd_dup(newReached[i]);
if (printStep && ((depth % printStep) == 0)) {
(void)fprintf(vis_stdout,
"BFS step = %d\t|states| = %8g\tBdd size = %8ld\n",
depth, mdd_count_onset(mddManager, newReached[i],
subFsm[i]->fsmData.presentStateVars),
(long)mdd_size(newReached[i]));
}
}
converged = 1;
for (i = 0; i < n; i++) {
if (mdd_equal(reached[i], newReached[i]))
mdd_free(newReached[i]);
else {
converged = 0;
mdd_free(reached[i]);
reached[i] = newReached[i];
}
}
iteration++;
if (ardcVerbosity > 0) {
boolean supportCheckFlag = FALSE;
if (projectedInitialFlag ||
abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
supportCheckFlag = TRUE;
}
PrintCurrentReachedStates(mddManager, subFsm, reached,
Fsm_Ardc_Traversal_Rfbf_c,
n, iteration, nvars, ardcVerbosity,
supportCheckFlag);
}
/* update constraints */
for (i = 0; i < n; i++) {
mdd_free(constraint[i]);
constraint[i] = newConstraint[i];
newConstraint[i] = NIL(mdd_t);
}
if (iteration == maxIteration)
break;
} while (!converged);
if (ardcVerbosity > 0) {
fprintf(vis_stdout, "RFBF : total iteration %d\n", iteration);
fprintf(vis_stdout, "%d image computations, %d constrain operations\n",
Img_GetNumberOfImageComputation(Img_Forward_c), n * iteration);
fprintf(vis_stdout,
"image computation time = %g, constrain operation time = %g\n",
(double)tImgComps / 1000.0, (double)tConstrainOps / 1000.0);
}
if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
constrainTarget == Fsm_Ardc_Constrain_Both_c) {
for (i = 0; i < n; i++) {
mdd_free(subFsm[i]->reachabilityInfo.initialStates);
subFsm[i]->reachabilityInfo.initialStates = initial[i];
}
FREE(initial);
}
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) {
for (i = 0; i < n; i++) {
tmp = reached[i];
reached[i] = QuantifyVariables(reached[i],
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube);
mdd_free(tmp);
}
}
/* sets the status of current overapproximate reached states */
if (converged)
FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c);
else
FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c);
ComputeApproximateReachableStatesArray(mddManager, reachedArray,
reached, NULL, n, decomposeFlag);
if (decomposeFlag) {
for (i = 0; i < n; i++) {
mdd_free(constraint[i]);
}
} else {
for (i = 0; i < n; i++) {
mdd_free(reached[i]);
mdd_free(constraint[i]);
}
}
FREE(reached);
FREE(constraint);
FREE(newConstraint);
FREE(subFsm);
FREE(newReached);
array_free(toCareSetArray);
return(reachedArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static array_t * ArdcSimpleTraversal | ( | Fsm_Fsm_t * | fsm, |
| int | nvars, | ||
| array_t * | subFsmArray, | ||
| int | incrementalFlag, | ||
| int | verbosityLevel, | ||
| int | printStep, | ||
| int | depthValue, | ||
| int | shellFlag, | ||
| int | reorderFlag, | ||
| int | reorderThreshold, | ||
| Fsm_RchType_t | approxFlag, | ||
| Fsm_ArdcOptions_t * | options, | ||
| int | setFlag | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes a very rough upperbound in short time.]
Description [Computes a very rough upperbound in short time. It is very simplified version of MBM, no iteration and no constrain operation.]
SideEffects []
SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal ArdcTmbmTraversal]
Definition at line 3685 of file fsmArdc.c.
{
mdd_manager *mddManager;
int i, n = array_n(subFsmArray);
mdd_t **reached;
Fsm_Fsm_t **subFsm;
mdd_t *tmp;
array_t *reachedArray = array_alloc(mdd_t *, 0);
Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t);
boolean decomposeFlag = options->decomposeFlag;
int abstractPseudoInput = options->abstractPseudoInput;
boolean projectedInitialFlag = options->projectedInitialFlag;
int ardcVerbosity = options->verbosity;
reached = ALLOC(mdd_t *, n);
subFsm = ALLOC(Fsm_Fsm_t *, n);
for (i = 0; i < n; i++)
subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
mddManager = Fsm_FsmReadMddManager(subFsm[0]);
for (i = 0; i < n; i++) {
if (printStep && ardcVerbosity > 1)
fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
if (ardcVerbosity > 2)
Img_SetPrintMinimizeStatus(imageInfo, 2);
else if (ardcVerbosity > 0)
Img_SetPrintMinimizeStatus(imageInfo, 1);
else
Img_SetPrintMinimizeStatus(imageInfo, 0);
imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1);
Img_AbstractTransitionRelation(imageInfo,
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube,
Img_Forward_c);
Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
}
reached[i] = Fsm_FsmComputeReachableStates(subFsm[i],
incrementalFlag, verbosityLevel, printStep, depthValue,
shellFlag, reorderFlag, reorderThreshold,
approxFlag, 0, 0, NIL(array_t), FALSE, NIL(array_t));
if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
Img_TfmFlushCache(imageInfo, FALSE);
}
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) {
if (n > 1) {
tmp = reached[i];
reached[i] = QuantifyVariables(reached[i],
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube);
mdd_free(tmp);
}
}
}
if (ardcVerbosity > 0) {
boolean supportCheckFlag = FALSE;
if (projectedInitialFlag ||
abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
supportCheckFlag = TRUE;
}
PrintCurrentReachedStates(mddManager, subFsm, reached,
Fsm_Ardc_Traversal_Simple_c,
n, 0, nvars, ardcVerbosity,
supportCheckFlag);
}
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) {
for (i = 0; i < n; i++) {
tmp = reached[i];
reached[i] = QuantifyVariables(reached[i],
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube);
mdd_free(tmp);
}
}
/* sets the status of current overapproximate reached states */
if (setFlag)
FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c);
ComputeApproximateReachableStatesArray(mddManager, reachedArray,
reached, NULL, n, decomposeFlag);
FREE(reached);
FREE(subFsm);
return(reachedArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static array_t * ArdcTfbfTraversal | ( | Fsm_Fsm_t * | fsm, |
| int | nvars, | ||
| array_t * | subFsmArray, | ||
| array_t * | fanInsIndexArray, | ||
| mdd_t *** | subReached, | ||
| mdd_t *** | subTo, | ||
| int | incrementalFlag, | ||
| int | verbosityLevel, | ||
| int | printStep, | ||
| int | depthValue, | ||
| int | shellFlag, | ||
| int | reorderFlag, | ||
| int | reorderThreshold, | ||
| Fsm_RchType_t | approxFlag, | ||
| Fsm_ArdcOptions_t * | options | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes an upperbound of an FSM by TFBF.]
Description [Computes an upperbound of an FSM by TFBF. It first sets all constraints to initial states, then does one image computation, then updates constraints with the results of image computations. This is iteratively done until it gets converged. Refer the description of ArdcMbmTraversal(MBM).]
SideEffects []
SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTmbmTraversal ArdcSimpleTraversal]
Definition at line 3243 of file fsmArdc.c.
{
mdd_manager *mddManager = NIL(mdd_manager);
int i, j, n = array_n(subFsmArray);
mdd_t **reached, **constraint, **newConstraint;
mdd_t **to, **old_to;
int converged = 0;
Fsm_Fsm_t **subFsm;
array_t *pi_to;
mdd_t *tmp;
array_t *fans;
mdd_t *initialStates;
int iteration = 0;
mdd_t **initial = NIL(mdd_t *);
array_t *reachedArray = array_alloc(mdd_t *, 0);
array_t *faninConstrainArray;
Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t);
int dynStatus;
bdd_reorder_type_t dynMethod;
mdd_t *toCareSet;
array_t *toCareSetArray = array_alloc(mdd_t *, 0);
int depth = 0;
boolean tmpReorderPtrFlag;
long tImgComps = 0;
long tConstrainOps = 0;
long initialTime = 0, finalTime;
int maxIteration = options->maxIteration;
int constrainTarget = options->constrainTarget;
boolean decomposeFlag = options->decomposeFlag;
int abstractPseudoInput = options->abstractPseudoInput;
Img_MinimizeType constrainMethod = options->constrainMethod;
boolean projectedInitialFlag = options->projectedInitialFlag;
int ardcVerbosity = options->verbosity;
boolean constrainReorderFlag = options->constrainReorderFlag;
boolean reorderPtrFlag = options->reorderPtrFlag;
int faninConstrainMode = options->faninConstrainMode;
Img_ResetNumberOfImageComputation(Img_Forward_c);
reached = ALLOC(mdd_t *, n);
constraint = ALLOC(mdd_t *, n);
newConstraint = ALLOC(mdd_t *, n);
subFsm = ALLOC(Fsm_Fsm_t *, n);
pi_to = array_alloc(mdd_t *, 0);
to = ALLOC(mdd_t *, n);
array_insert_last(mdd_t **, pi_to, to);
mddManager = Fsm_FsmReadMddManager(fsm);
for (i = 0; i < n; i++) {
subFsm[i] = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
initialStates = Fsm_FsmComputeInitialStates(subFsm[i]);
reached[i] = initialStates;
constraint[i] = mdd_dup(initialStates);
to[i] = mdd_zero(mddManager);
if (printStep && ((depth % printStep) == 0)) {
if (ardcVerbosity > 1)
fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
(void)fprintf(vis_stdout,
"BFS step = %d\t|states| = %8g\tBdd size = %8ld\n", depth,
mdd_count_onset(mddManager, reached[i],
subFsm[i]->fsmData.presentStateVars),
(long)mdd_size(reached[i]));
}
}
if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
constrainTarget == Fsm_Ardc_Constrain_Both_c) {
initial = ALLOC(mdd_t *, n);
for (i = 0; i < n; i++)
initial[i] = Fsm_FsmComputeInitialStates(subFsm[i]);
}
converged = 0;
do {
depth++;
to = ALLOC(mdd_t *, n);
for (i = 0; i < n; i++) {
if (ardcVerbosity > 1)
fprintf(vis_stdout, "--- sub fsm [%d] ---\n", i);
faninConstrainArray = array_alloc(mdd_t *, 0);
fans = array_fetch(array_t *, fanInsIndexArray, i);
ComputeFaninConstrainArray(faninConstrainArray, constraint,
i, fans, decomposeFlag, faninConstrainMode);
dynStatus = bdd_reordering_status(mddManager, &dynMethod);
if (dynStatus != 0 && constrainReorderFlag == 0)
bdd_dynamic_reordering_disable(mddManager);
imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm[i], 0, 1);
if (constrainTarget != Fsm_Ardc_Constrain_Initial_c) {
int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
if (ardcVerbosity > 2)
Img_SetPrintMinimizeStatus(imageInfo, 2);
else if (ardcVerbosity > 0)
Img_SetPrintMinimizeStatus(imageInfo, 1);
else
Img_SetPrintMinimizeStatus(imageInfo, 0);
if (reorderPtrFlag &&
abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) {
tmpReorderPtrFlag = 1;
} else
tmpReorderPtrFlag = 0;
if (ardcVerbosity > 0)
initialTime = util_cpu_time();
MinimizeTransitionRelationWithFaninConstraint(imageInfo,
faninConstrainArray, constrainMethod, tmpReorderPtrFlag,
TRUE);
if (ardcVerbosity > 0) {
finalTime = util_cpu_time();
tConstrainOps += finalTime - initialTime;
}
Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
}
if (constrainTarget != Fsm_Ardc_Constrain_Tr_c) {
ComputeConstrainedInitialStates(subFsm[i], faninConstrainArray,
constrainMethod);
}
mdd_array_free(faninConstrainArray);
if (dynStatus != 0 && constrainReorderFlag == 0) {
bdd_dynamic_reordering(mddManager, dynMethod,
BDD_REORDER_VERBOSITY_DEFAULT);
}
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
int saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
if (ardcVerbosity > 2)
Img_SetPrintMinimizeStatus(imageInfo, 2);
else if (ardcVerbosity > 0)
Img_SetPrintMinimizeStatus(imageInfo, 1);
else
Img_SetPrintMinimizeStatus(imageInfo, 0);
Img_AbstractTransitionRelation(imageInfo,
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube, Img_Forward_c);
if (reorderPtrFlag)
Img_ReorderPartitionedTransitionRelation(imageInfo, Img_Forward_c);
Img_SetPrintMinimizeStatus(imageInfo, saveStatus);
}
toCareSet = mdd_not(reached[i]);
array_insert(mdd_t *, toCareSetArray, 0, toCareSet);
if (ardcVerbosity > 0)
initialTime = util_cpu_time();
to[i] = Fsm_ArdcComputeImage(subFsm[i], constraint[i],
constraint[i], toCareSetArray);
if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
Img_TfmFlushCache(imageInfo, FALSE);
}
if (ardcVerbosity > 0) {
finalTime = util_cpu_time();
tImgComps += finalTime - initialTime;
}
mdd_free(toCareSet);
if (constrainTarget != Fsm_Ardc_Constrain_Initial_c)
Img_RestoreTransitionRelation(imageInfo, Img_Forward_c);
tmp = reached[i];
reached[i] = mdd_or(reached[i], to[i], 1, 1);
mdd_free(tmp);
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_After_Image_c) {
tmp = reached[i];
reached[i] = QuantifyVariables(reached[i],
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube);
mdd_free(tmp);
}
newConstraint[i] = mdd_dup(to[i]);
if (printStep && ((depth % printStep) == 0)) {
(void)fprintf(vis_stdout,
"BFS step = %d\t|states| = %8g\tBdd size = %8ld\n",
depth, mdd_count_onset(mddManager, reached[i],
subFsm[i]->fsmData.presentStateVars),
(long)mdd_size(reached[i]));
}
}
for (i = 0; i < array_n(pi_to); i++) {
old_to = array_fetch(mdd_t **, pi_to, i);
for (j = 0; j < n; j++) {
if (!mdd_equal(old_to[j], to[j]))
break;
}
if (j == n)
break;
}
if (i == array_n(pi_to))
converged = 0;
else {
converged = 1;
if (ardcVerbosity > 0) {
fprintf(vis_stdout,
"** ardc info : TFBF converged at iteration %d(=%d).\n",
iteration + 1, i);
}
}
iteration++;
if (ardcVerbosity > 0) {
boolean supportCheckFlag = FALSE;
if (projectedInitialFlag ||
abstractPseudoInput == Fsm_Ardc_Abst_Ppi_Before_Image_c) {
supportCheckFlag = TRUE;
}
PrintCurrentReachedStates(mddManager, subFsm, reached,
Fsm_Ardc_Traversal_Tfbf_c,
n, iteration, nvars, ardcVerbosity,
supportCheckFlag);
}
/* update constraints */
for (i = 0; i < n; i++) {
mdd_free(constraint[i]);
constraint[i] = newConstraint[i];
newConstraint[i] = NIL(mdd_t);
}
if (converged || iteration == maxIteration) {
if (subTo)
*subTo = to;
else {
for (i = 0; i < n; i++)
mdd_free(to[i]);
FREE(to);
}
break;
}
array_insert_last(mdd_t **, pi_to, to);
} while (!converged);
if (ardcVerbosity > 0) {
fprintf(vis_stdout, "TFBF : total iteration %d\n", iteration);
fprintf(vis_stdout, "%d image computations, %d constrain operations\n",
Img_GetNumberOfImageComputation(Img_Forward_c), n * iteration);
fprintf(vis_stdout,
"image computation time = %g, constrain operation time = %g\n",
(double)tImgComps / 1000.0, (double)tConstrainOps / 1000.0);
}
if (constrainTarget == Fsm_Ardc_Constrain_Initial_c ||
constrainTarget == Fsm_Ardc_Constrain_Both_c) {
for (i = 0; i < n; i++) {
mdd_free(subFsm[i]->reachabilityInfo.initialStates);
subFsm[i]->reachabilityInfo.initialStates = initial[i];
}
FREE(initial);
}
if (abstractPseudoInput == Fsm_Ardc_Abst_Ppi_At_End_c) {
for (i = 0; i < n; i++) {
tmp = reached[i];
reached[i] = QuantifyVariables(reached[i],
subFsm[i]->fsmData.pseudoInputBddVars,
subFsm[i]->fsmData.pseudoInputCube);
mdd_free(tmp);
}
}
/* sets the status of current overapproximate reached states */
if (converged)
FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_Converged_c);
else
FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c);
ComputeApproximateReachableStatesArray(mddManager, reachedArray,
reached, subReached, n, decomposeFlag);
if (decomposeFlag) {
for (i = 0; i < n; i++) {
mdd_free(constraint[i]);
}
} else {
for (i = 0; i < n; i++) {
if (subReached == NULL)
mdd_free(reached[i]);
mdd_free(constraint[i]);
}
}
if (subReached)
*subReached = reached;
else
FREE(reached);
FREE(constraint);
FREE(newConstraint);
FREE(subFsm);
for (i = 0; i < array_n(pi_to); i++) {
to = array_fetch(mdd_t **, pi_to, i);
for (j = 0; j < n; j++)
mdd_free(to[j]);
FREE(to);
}
array_free(pi_to);
array_free(toCareSetArray);
return(reachedArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static array_t * ArdcTmbmTraversal | ( | Fsm_Fsm_t * | fsm, |
| int | nvars, | ||
| array_t * | subFsmArray, | ||
| array_t * | fanInsIndexArray, | ||
| array_t * | fanOutsIndexArray, | ||
| int | incrementalFlag, | ||
| int | verbosityLevel, | ||
| int | printStep, | ||
| int | depthValue, | ||
| int | shellFlag, | ||
| int | reorderFlag, | ||
| int | reorderThreshold, | ||
| Fsm_RchType_t | approxFlag, | ||
| Fsm_ArdcOptions_t * | options, | ||
| boolean | lfpFlag | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes an upperbound of an FSM by TMBM.]
Description [Computes an upperbound of an FSM by TMBM. TMBM is a combination of TFBF and MBM. It first calls TFBF with max iteration number(given by ardc_max_iteration set option). Then if the reached states are not converged yet, it calls MBM by using current reached states as initial states.]
SideEffects []
SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal ArdcSimpleTraversal]
Definition at line 3560 of file fsmArdc.c.
{
mdd_manager *mddManager;
int i, n = array_n(subFsmArray);
mdd_t **reached, **tfbf_reached;
mdd_t **to, **initial;
Fsm_Fsm_t *subFsm = NIL(Fsm_Fsm_t);
mdd_t *tmp;
array_t *reachedArray;
int saveMaxIteration;
saveMaxIteration = options->maxIteration;
if (options->maxIteration == 0)
options->maxIteration = 10; /* default */
/* Try TFBF for the presecribed number of steps. */
reachedArray = ArdcTfbfTraversal(fsm, nvars, subFsmArray, fanInsIndexArray,
&tfbf_reached, &to,
incrementalFlag, verbosityLevel, printStep,
depthValue, shellFlag, reorderFlag,
reorderThreshold, approxFlag, options);
/* If TFBF converged in the allotted number of iterations, clean up and
* return. */
if (FsmReadReachabilityOverApproxComputationStatus(fsm) >=
Fsm_Ardc_Converged_c) {
for (i = 0; i < n; i++) {
mdd_free(tfbf_reached[i]);
mdd_free(to[i]);
}
FREE(tfbf_reached);
FREE(to);
return(reachedArray);
}
mdd_array_free(reachedArray);
/* Save the initial states of each submachine in "initial"; thenset it
* to the "to" states returned by TFBF. */
initial = ALLOC(mdd_t *, n);
for (i = 0; i < n; i++) {
subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
initial[i] = subFsm->reachabilityInfo.initialStates;
subFsm->reachabilityInfo.initialStates = mdd_dup(to[i]);
}
/* Apply either MBM or LMBM starting from the "to" states returned by
* TFBF. */
options->maxIteration = 0;
reachedArray = ArdcMbmTraversal(fsm, nvars, subFsmArray,
fanInsIndexArray, fanOutsIndexArray, &reached,
incrementalFlag, verbosityLevel, printStep,
depthValue, shellFlag, reorderFlag, reorderThreshold,
approxFlag, options, lfpFlag);
options->maxIteration = saveMaxIteration;
mdd_array_free(reachedArray);
/* Combine the reachability results of TFBF and (L)MBM and restore
* the initial states of the submachines. */
for (i = 0; i < n; i++) {
tmp = reached[i];
reached[i] = mdd_or(tfbf_reached[i], reached[i], 1, 1);
mdd_free(tmp);
subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
mdd_free(subFsm->reachabilityInfo.initialStates);
subFsm->reachabilityInfo.initialStates = initial[i];
}
/* Build the array of reachable states in either monolithic or decomposed
* form depending on the value of decomposeFlag. */
reachedArray = array_alloc(mdd_t *, 0);
mddManager = Fsm_FsmReadMddManager(subFsm);
ComputeApproximateReachableStatesArray(mddManager, reachedArray,
reached, NULL, n,
options->decomposeFlag);
if (!options->decomposeFlag) {
for (i = 0; i < n; i++)
mdd_free(reached[i]);
}
/* Clean up. */
for (i = 0; i < n; i++) {
mdd_free(tfbf_reached[i]);
mdd_free(to[i]);
}
FREE(reached);
FREE(tfbf_reached);
FREE(to);
FREE(initial);
return(reachedArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void ArdcWriteOneGroup | ( | Part_Subsystem_t * | partitionSubsystem, |
| FILE * | groupFile, | ||
| int | i | ||
| ) | [static] |
Function********************************************************************
Synopsis [Writes one grouping information.]
Description [Writes one grouping information.]
SideEffects []
SeeAlso []
Definition at line 4161 of file fsmArdc.c.
{
st_generator *stGen;
st_table *vertexNameTable;
char *latchName;
fprintf(groupFile, "GROUP[%d]:", i);
vertexNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
st_foreach_item(vertexNameTable, stGen, &latchName, NIL(char *)) {
fprintf(groupFile, " %s", latchName);
}
fprintf(groupFile, "\n");
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void ComputeApproximateReachableStatesArray | ( | mdd_manager * | mddManager, |
| array_t * | reachedArray, | ||
| mdd_t ** | reached, | ||
| mdd_t *** | subReached, | ||
| int | nSubFsms, | ||
| int | decomposeFlag | ||
| ) | [static] |
Function********************************************************************
Synopsis [Makes an array of approximate reachable states.]
Description [Makes an array of approximate reachable states.]
SideEffects []
SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal]
Definition at line 3906 of file fsmArdc.c.
{
int i;
if (decomposeFlag) {
for (i = 0; i < nSubFsms; i++) {
if (subReached)
array_insert_last(mdd_t *, reachedArray, mdd_dup(reached[i]));
else
array_insert_last(mdd_t *, reachedArray, reached[i]);
}
} else {
mdd_t *reachedSet = mdd_one(mddManager);
for (i = 0; i < nSubFsms; i++) {
mdd_t *tmp = reachedSet;
reachedSet = mdd_and(reachedSet, reached[i], 1, 1);
mdd_free(tmp);
}
array_insert_last(mdd_t *, reachedArray, reachedSet);
}
}
Here is the caller graph for this function:
| static void ComputeConstrainedInitialStates | ( | Fsm_Fsm_t * | subFsm, |
| array_t * | faninConstrainArray, | ||
| Img_MinimizeType | constrainMethod | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes constrained initial states.]
Description [Computes constrained initial states.]
SideEffects [This function just update a new constrained initial states, so caller should take care of this.]
SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal]
Definition at line 3874 of file fsmArdc.c.
{
int i;
mdd_t *faninConstrain, *tmp, *constrainedInitial;
constrainedInitial = subFsm->reachabilityInfo.initialStates;
for (i = 0; i < array_n(faninConstrainArray); i++) {
faninConstrain = array_fetch(mdd_t *, faninConstrainArray, i);
tmp = constrainedInitial;
constrainedInitial = Img_MinimizeImage(constrainedInitial,
faninConstrain, constrainMethod,
TRUE);
mdd_free(tmp);
}
subFsm->reachabilityInfo.initialStates = constrainedInitial;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void ComputeFaninConstrainArray | ( | array_t * | faninConstrainArray, |
| mdd_t ** | constraint, | ||
| int | current, | ||
| array_t * | fans, | ||
| int | decomposeFlag, | ||
| int | faninConstrainMode | ||
| ) | [static] |
Function********************************************************************
Synopsis [Computes fanin constraint with the reached states of fanin submachines.]
Description [Computes fanin constraint with the reached states of fanin submachines.]
SideEffects []
SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal]
Definition at line 3799 of file fsmArdc.c.
{
mdd_t *faninConstrain, *tmp;
int i, fanin;
if (decomposeFlag) {
if (faninConstrainMode == 1) {
array_insert_last(mdd_t *, faninConstrainArray,
mdd_dup(constraint[current]));
}
arrayForEachItem(int, fans, i, fanin) {
array_insert_last(mdd_t *, faninConstrainArray,
mdd_dup(constraint[fanin]));
}
} else {
if (faninConstrainMode == 1)
faninConstrain = mdd_dup(constraint[current]);
else
faninConstrain = NIL(mdd_t);
arrayForEachItem(int, fans, i, fanin) {
if (faninConstrain) {
tmp = faninConstrain;
faninConstrain = mdd_and(faninConstrain, constraint[fanin], 1, 1);
mdd_free(tmp);
} else
faninConstrain = mdd_dup(constraint[fanin]);
}
array_insert_last(mdd_t *, faninConstrainArray, faninConstrain);
}
}
Here is the caller graph for this function:
| Fsm_ArdcOptions_t* Fsm_ArdcAllocOptionsStruct | ( | void | ) |
Function********************************************************************
Synopsis [Allocates an ARDC option structure.]
Description [Allocates an ARDC option structure.]
SideEffects []
SeeAlso []
Definition at line 795 of file fsmArdc.c.
{
Fsm_ArdcOptions_t *options;
options = ALLOC(Fsm_ArdcOptions_t, 1);
(void)memset((void *)options, 0, sizeof(Fsm_ArdcOptions_t));
return(options);
}
Here is the caller graph for this function:
| int Fsm_ArdcBddSizeOfOverApproximateReachableStates | ( | Fsm_Fsm_t * | fsm | ) |
Function********************************************************************
Synopsis [Returns the bdd size of the set of approximate reachable states of an FSM.]
Description [Returns the bdd size of the set of approximate reachable states of an FSM.]
SideEffects []
SeeAlso []
Definition at line 1669 of file fsmArdc.c.
{
mdd_t *reached;
array_t *reachedArray;
int i, size = 0;
if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm))
return(0);
reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm);
arrayForEachItem(mdd_t *, reachedArray, i, reached) {
size += mdd_size(reached);
}
return(size);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Fsm_ArdcComputeImage | ( | Fsm_Fsm_t * | fsm, |
| mdd_t * | fromLowerBound, | ||
| mdd_t * | fromUpperBound, | ||
| array_t * | toCareSetArray | ||
| ) |
Function********************************************************************
Synopsis [Computes the image of current reachable states of an FSM.]
Description [Computes the image of current reachable states of an FSM. It calls Fsm_FsmComputeReachableStates by setting depthValue to 1.]
SideEffects []
SeeAlso []
Definition at line 215 of file fsmArdc.c.
{
Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t);
mdd_t *image;
/* Create an imageInfo for image computations, if not already created. */
imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, 0, 1);
/* Compute the image */
image = Img_ImageInfoComputeImageWithDomainVars(imageInfo,
fromLowerBound, fromUpperBound, toCareSetArray);
return(image);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Fsm_ArdcComputeOverApproximateReachableStates | ( | Fsm_Fsm_t * | fsm, |
| int | incrementalFlag, | ||
| int | verbosityLevel, | ||
| int | printStep, | ||
| int | depthValue, | ||
| int | shellFlag, | ||
| int | reorderFlag, | ||
| int | reorderThreshold, | ||
| int | recompute, | ||
| Fsm_ArdcOptions_t * | options | ||
| ) |
Function********************************************************************
Synopsis [Computes the set of approximate reachable states of an FSM.]
Description [Computes the set of approximate reachable states of an FSM. If this set has already been computed, then just returns the result of the previous computation. The computations starts by creating partitions (based on either hierarchy or state space decomposition [TCAD96]). The submachines are created for each of these partitions. Then approximate traversal is performed by one of the supported methods (MBM, RFBF, TFBF, TMBM, LMBM, and TLMBM). The approximate reachable set is returned in a conjunctive decomposed form in an array.]
SideEffects []
SeeAlso [Fsm_FsmComputeInitialStates Fsm_FsmComputeReachableStates]
Definition at line 286 of file fsmArdc.c.
{
array_t *reachableStatesArray = NIL(array_t);
mdd_t *reachableStates = NIL(mdd_t);
mdd_t *initialStates;
Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm);
Part_Subsystem_t *partitionSubsystem;
array_t *partitionArray;
int i;
graph_t *partition = Part_NetworkReadPartition(network);
st_table *vertexTable;
Fsm_Fsm_t *subFsm;
array_t *subFsmArray;
array_t *fanIns, *fanOuts;
array_t *fanInsIndexArray, *fanOutsIndexArray;
array_t *fans;
array_t *psVars;
mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
char *flagValue;
Fsm_RchType_t approxFlag;
int nvars; /* the number of binary variables of the fsm */
FILE *groupFile = NIL(FILE);
Img_MethodType imageMethod = Img_Default_c;
Img_MethodType saveImageMethod = Img_Default_c;
char *imageMethodString;
Fsm_Ardc_AbstPpiType_t saveAbstractPseudoInput;
if (recompute)
FsmResetReachabilityFields(fsm, Fsm_Rch_Oa_c);
/* If exact is already computed, copy exact to overapproximate. */
if (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t)) {
if (Fsm_FsmReadCurrentOverApproximateReachableStates(fsm) != NIL(array_t)) {
/* If the overapproximation is already the exact set, return it,
* otherwise discard it. */
if (FsmReadReachabilityOverApproxComputationStatus(fsm) ==
Fsm_Ardc_Exact_c) {
return(Fsm_FsmReadOverApproximateReachableStates(fsm));
} else {
fprintf(vis_stdout,
"** ardc warning : ignoring previous computation.\n");
Fsm_FsmFreeOverApproximateReachableStates(fsm);
}
}
if (verbosityLevel > 0 || options->verbosity > 0) {
fprintf(vis_stdout,
"** ardc info : exact reached states are already computed.\n");
}
/* Either we had no overapproximation, or it was not the exact set, and
* hence it was discarded. Copy from exact to overapproximate. */
reachableStatesArray = ArdcCopyOverApproxReachableStatesFromExact(fsm);
return(reachableStatesArray);
}
/* If already computed, just return the array. */
if (Fsm_FsmReadCurrentOverApproximateReachableStates(fsm) != NIL(array_t)) {
if (FsmReadReachabilityOverApproxComputationStatus(fsm) >=
Fsm_Ardc_Converged_c) {
return(Fsm_FsmReadOverApproximateReachableStates(fsm));
} else {
/* Here, at this time, we just throw away current approximate
* reachable states which is not converged yet, then restart.
*/
fprintf(vis_stdout,
"** ardc warning : ignoring previous computation.\n");
Fsm_FsmFreeOverApproximateReachableStates(fsm);
}
}
/* Perform state space decomposition. */
partitionArray = Fsm_ArdcDecomposeStateSpace(network,
fsm->fsmData.presentStateVars,
fsm->fsmData.nextStateFunctions,
options);
/* If there is only one group, call exact reachability analysis. */
if (array_n(partitionArray) == 1) {
if (options->verbosity > 0) {
fprintf(vis_stdout,
"** ardc info : changing to exact reachability analysis.\n");
}
arrayForEachItem(Part_Subsystem_t *, partitionArray, i,
partitionSubsystem) {
Part_PartitionSubsystemFree(partitionSubsystem);
}
array_free(partitionArray);
if (options->useHighDensity)
approxFlag = Fsm_Rch_Hd_c;
else
approxFlag = Fsm_Rch_Bfs_c;
reachableStates = Fsm_FsmComputeReachableStates(fsm,
0, verbosityLevel, printStep, 0,
0, reorderFlag, reorderThreshold,
approxFlag, 0, 0, NIL(array_t), (verbosityLevel > 1),
NIL(array_t));
mdd_free(reachableStates);
reachableStatesArray = ArdcCopyOverApproxReachableStatesFromExact(fsm);
return(reachableStatesArray);
}
/* Read the image_method flag, and save its value in imageMethodString. */
flagValue = Cmd_FlagReadByName("image_method");
if (flagValue != NIL(char)) {
if (strcmp(flagValue, "iwls95") == 0 || strcmp(flagValue, "default") == 0)
imageMethod = Img_Iwls95_c;
else if (strcmp(flagValue, "monolithic") == 0)
imageMethod = Img_Monolithic_c;
else if (strcmp(flagValue, "tfm") == 0)
imageMethod = Img_Tfm_c;
else if (strcmp(flagValue, "hybrid") == 0)
imageMethod = Img_Hybrid_c;
else if (strcmp(flagValue, "mlp") == 0)
imageMethod = Img_Mlp_c;
else {
fprintf(vis_stderr, "** ardc error: invalid image method %s.\n",
flagValue);
}
}
imageMethodString = flagValue;
/* Update the image_method flag to the method specified for approximate
* reachability. */
if (options->ardcImageMethod != Img_Default_c &&
options->ardcImageMethod != imageMethod) {
saveImageMethod = imageMethod;
if (options->ardcImageMethod == Img_Monolithic_c) {
Cmd_FlagUpdateValue("image_method", "monolithic");
imageMethod = Img_Monolithic_c;
} else if (options->ardcImageMethod == Img_Iwls95_c) {
Cmd_FlagUpdateValue("image_method", "iwls95");
imageMethod = Img_Iwls95_c;
} else if (options->ardcImageMethod == Img_Tfm_c) {
Cmd_FlagUpdateValue("image_method", "tfm");
imageMethod = Img_Tfm_c;
} else if (options->ardcImageMethod == Img_Hybrid_c) {
Cmd_FlagUpdateValue("image_method", "hybrid");
imageMethod = Img_Hybrid_c;
} else if (options->ardcImageMethod == Img_Mlp_c) {
Cmd_FlagUpdateValue("image_method", "mlp");
imageMethod = Img_Mlp_c;
}
}
/* Open the file where to save the result of partitioning is so requested. */
if (options->writeGroupFile) {
groupFile = Cmd_FileOpen(options->writeGroupFile, "w", NIL(char *), 0);
if (groupFile == NIL(FILE)) {
fprintf(vis_stderr, "** ardc error : can't open file [%s] to write.\n",
options->writeGroupFile);
}
}
/* Compute the set of initial states, if not already computed. */
initialStates = Fsm_FsmComputeInitialStates(fsm);
subFsmArray = array_alloc(Fsm_Fsm_t *, 0);
fanInsIndexArray = array_alloc(array_t *, 0);
fanOutsIndexArray = array_alloc(array_t *, 0);
/* For each partitioned submachines build an FSM. */
arrayForEachItem(Part_Subsystem_t *, partitionArray, i, partitionSubsystem) {
vertexTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
fanIns = Part_PartitionSubsystemReadFanIn(partitionSubsystem);
fanOuts = Part_PartitionSubsystemReadFanOut(partitionSubsystem);
subFsm = Fsm_FsmCreateSubsystemFromNetwork(network, partition,
vertexTable, TRUE,
options->createPseudoVarMode);
/* Depending on the options, the initial states of each submachine
* are either the states of the entire system or their projection
* on the subspace of the submachine. */
if (!options->projectedInitialFlag &&
options->abstractPseudoInput != Fsm_Ardc_Abst_Ppi_Before_Image_c) {
subFsm->reachabilityInfo.initialStates = mdd_dup(initialStates);
} else {
mdd_t *dummy;
dummy = Fsm_FsmComputeInitialStates(subFsm);
mdd_free(dummy);
}
array_insert_last(Fsm_Fsm_t *, subFsmArray, subFsm);
array_insert_last(array_t *, fanInsIndexArray, fanIns);
array_insert_last(array_t *, fanOutsIndexArray, fanOuts);
if (options->verbosity > 1) {
int nLatches;
nLatches = mdd_get_number_of_bdd_vars(mddManager,
subFsm->fsmData.presentStateVars);
ArdcPrintOneGroup(partitionSubsystem, i, nLatches, fanIns, fanOuts);
}
if (groupFile)
ArdcWriteOneGroup(partitionSubsystem, groupFile, i);
st_free_table(vertexTable);
} /* end of arrayForEachItem(partitionArray) */
mdd_free(initialStates);
if (groupFile)
fclose(groupFile);
/* Sort submachines to find the order in which to traverse them. */
SortSubFsmsForApproximateTraversal(&subFsmArray, &fanInsIndexArray,
&fanOutsIndexArray, options->verbosity);
/* Optimize pseudo-input variables to contain only the variables of fanin
* submachines. If createPseudoVarMode is 0, the set of pseudo-input
* variables is just the collection of the variables of all other
* submachines.
* If createPseudoVarMode is 1, the set is the collection of the variables
* of only its fanin submachines. If createPseudoVarMode is 2, the set is
* the collection of the support variables that appear in other submachines.
*/
if (options->createPseudoVarMode == 0) {
arrayForEachItem(Fsm_Fsm_t *, subFsmArray, i, subFsm) {
Fsm_Fsm_t *faninSubfsm;
int j, fanin;
subFsm->fsmData.primaryInputVars = array_dup(subFsm->fsmData.inputVars);
subFsm->fsmData.pseudoInputVars = array_alloc(int, 0);
fanIns = array_fetch(array_t *, fanInsIndexArray, i);
arrayForEachItem(int, fanIns, j, fanin) {
if (fanin == i)
continue;
faninSubfsm = array_fetch(Fsm_Fsm_t *, subFsmArray, fanin);
array_append(subFsm->fsmData.pseudoInputVars,
faninSubfsm->fsmData.presentStateVars);
}
subFsm->fsmData.globalPsVars = array_dup(
subFsm->fsmData.presentStateVars);
array_append(subFsm->fsmData.globalPsVars,
subFsm->fsmData.pseudoInputVars);
array_append(subFsm->fsmData.inputVars, subFsm->fsmData.pseudoInputVars);
subFsm->fsmData.pseudoInputBddVars = mdd_id_array_to_bdd_array(mddManager,
subFsm->fsmData.pseudoInputVars);
if (subFsm->fsmData.createVarCubesFlag) {
subFsm->fsmData.pseudoInputCube = mdd_id_array_to_bdd_cube(mddManager,
subFsm->fsmData.pseudoInputVars);
subFsm->fsmData.primaryInputCube = subFsm->fsmData.inputCube;
subFsm->fsmData.inputCube = mdd_id_array_to_bdd_cube(mddManager,
subFsm->fsmData.inputVars);
subFsm->fsmData.globalPsCube = mdd_id_array_to_bdd_cube(mddManager,
subFsm->fsmData.globalPsVars);
}
}
}
if (options->useHighDensity)
approxFlag = Fsm_Rch_Hd_c;
else
approxFlag = Fsm_Rch_Bfs_c;
/* In case of transition function method, since quantification doesn't
* make any sense, we turn it off. We turn quantification off also for the
* hybrid method, because it starts with tfm.
*/
saveAbstractPseudoInput = options->abstractPseudoInput;
if (imageMethod == Img_Tfm_c || imageMethod == Img_Hybrid_c)
options->abstractPseudoInput = Fsm_Ardc_Abst_Ppi_No_c;
nvars = mdd_get_number_of_bdd_vars(mddManager, fsm->fsmData.presentStateVars);
if (options->traversalMethod == Fsm_Ardc_Traversal_Mbm_c) {
reachableStatesArray = ArdcMbmTraversal(fsm, nvars, subFsmArray,
fanInsIndexArray, fanOutsIndexArray, NULL,
incrementalFlag, verbosityLevel, printStep,
depthValue, shellFlag, reorderFlag,
reorderThreshold, approxFlag, options, FALSE);
} else if (options->traversalMethod == Fsm_Ardc_Traversal_Rfbf_c) {
if (approxFlag == Fsm_Rch_Hd_c) {
fprintf(vis_stderr,
"** ardc error : High Density Traversal is not allowed in FBF.\n");
}
reachableStatesArray = ArdcRfbfTraversal(fsm, nvars, subFsmArray,
fanInsIndexArray,
incrementalFlag, verbosityLevel, printStep,
depthValue, shellFlag, reorderFlag, reorderThreshold,
approxFlag, options);
} else if (options->traversalMethod == Fsm_Ardc_Traversal_Tfbf_c) {
if (approxFlag == Fsm_Rch_Hd_c) {
fprintf(vis_stderr,
"** ardc error : High Density Traversal is not allowed in FBF.\n");
}
reachableStatesArray = ArdcTfbfTraversal(fsm, nvars, subFsmArray,
fanInsIndexArray, NULL, NULL,
incrementalFlag, verbosityLevel, printStep,
depthValue, shellFlag, reorderFlag, reorderThreshold,
approxFlag, options);
} else if (options->traversalMethod == Fsm_Ardc_Traversal_Tmbm_c) {
reachableStatesArray = ArdcTmbmTraversal(fsm, nvars, subFsmArray,
fanInsIndexArray, fanOutsIndexArray,
incrementalFlag, verbosityLevel, printStep,
depthValue, shellFlag, reorderFlag, reorderThreshold,
approxFlag, options, FALSE);
} else if (options->traversalMethod == Fsm_Ardc_Traversal_Lmbm_c) {
reachableStatesArray = ArdcMbmTraversal(fsm, nvars, subFsmArray,
fanInsIndexArray, fanOutsIndexArray, NULL,
incrementalFlag, verbosityLevel, printStep,
depthValue, shellFlag, reorderFlag,
reorderThreshold, approxFlag, options, TRUE);
} else if (options->traversalMethod == Fsm_Ardc_Traversal_Tlmbm_c) {
reachableStatesArray = ArdcTmbmTraversal(fsm, nvars, subFsmArray,
fanInsIndexArray, fanOutsIndexArray,
incrementalFlag, verbosityLevel, printStep,
depthValue, shellFlag, reorderFlag, reorderThreshold,
approxFlag, options, TRUE);
} else {
reachableStatesArray = ArdcSimpleTraversal(fsm, nvars, subFsmArray,
incrementalFlag, verbosityLevel, printStep,
depthValue, shellFlag, reorderFlag, reorderThreshold,
approxFlag, options, TRUE);
}
options->abstractPseudoInput = saveAbstractPseudoInput;
if (options->verbosity &&
(options->ardcImageMethod == Img_Tfm_c ||
options->ardcImageMethod == Img_Hybrid_c)) {
PrintTfmStatistics(subFsmArray);
}
fsm->reachabilityInfo.subPsVars = array_alloc(array_t *, 0);
if (options->decomposeFlag) {
for (i = 0; i < array_n(subFsmArray); i++) {
subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
psVars = array_dup(subFsm->fsmData.presentStateVars);
array_insert_last(array_t *, fsm->reachabilityInfo.subPsVars, psVars);
}
} else {
psVars = array_dup(fsm->fsmData.presentStateVars);
array_insert_last(array_t *, fsm->reachabilityInfo.subPsVars, psVars);
}
arrayForEachItem(array_t *, fanInsIndexArray, i, fans) {
array_free(fans);
}
array_free(fanInsIndexArray);
arrayForEachItem(array_t *, fanOutsIndexArray, i, fans) {
array_free(fans);
}
array_free(fanOutsIndexArray);
arrayForEachItem(Part_Subsystem_t *, partitionArray, i, partitionSubsystem) {
FREE(partitionSubsystem);
}
array_free(partitionArray);
arrayForEachItem(Fsm_Fsm_t *, subFsmArray, i, subFsm) {
Fsm_FsmSubsystemFree(subFsm);
}
array_free(subFsmArray);
/* Restore value of image_method flag. */
if (options->ardcImageMethod != Img_Default_c &&
options->ardcImageMethod != saveImageMethod) {
if (imageMethodString) {
if (saveImageMethod == Img_Monolithic_c)
Cmd_FlagUpdateValue("image_method", "monolithic");
else if (saveImageMethod == Img_Iwls95_c)
Cmd_FlagUpdateValue("image_method", "iwls95");
else if (saveImageMethod == Img_Tfm_c)
Cmd_FlagUpdateValue("image_method", "tfm");
else if (saveImageMethod == Img_Hybrid_c)
Cmd_FlagUpdateValue("image_method", "hybrid");
else if (saveImageMethod == Img_Mlp_c)
Cmd_FlagUpdateValue("image_method", "mlp");
} else
Cmd_FlagDeleteByName("image_method");
}
fsm->reachabilityInfo.apprReachableStates = reachableStatesArray;
return(reachableStatesArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| double Fsm_ArdcCountOnsetOfOverApproximateReachableStates | ( | Fsm_Fsm_t * | fsm | ) |
Function********************************************************************
Synopsis [Returns the number of approximate reachable states of an FSM.]
Description [Returns the number of approximate reachable states of an FSM.]
SideEffects []
SeeAlso []
Definition at line 1634 of file fsmArdc.c.
{
mdd_t *reached;
array_t *psVars, *reachedArray;
mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
double numReached = 1.0, tmpReached;
int i;
if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm))
return(0.0);
reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm);
arrayForEachItem(mdd_t *, reachedArray, i, reached) {
psVars = array_fetch(array_t *, fsm->reachabilityInfo.subPsVars, i);
tmpReached = mdd_count_onset(mddManager, reached, psVars);
numReached *= tmpReached;
}
return(numReached);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* Fsm_ArdcDecomposeStateSpace | ( | Ntk_Network_t * | network, |
| array_t * | presentStateVars, | ||
| array_t * | nextStateFunctions, | ||
| Fsm_ArdcOptions_t * | options | ||
| ) |
Function********************************************************************
Synopsis [Performs state space decomposition.]
Description [Performs state space decomposition.]
SideEffects []
SeeAlso []
Definition at line 678 of file fsmArdc.c.
{
array_t *latchNameArray;
array_t *groupIndexArray;
char *name;
Ntk_Node_t *latch;
int i, mddId;
Part_SubsystemInfo_t *subsystemInfo;
array_t *partitionArray;
FILE *groupFile = NIL(FILE);
long initialTime = 0, finalTime;
int verbosity = 0;
float affinityFactor = 0.5;
int groupSize = 8;
if (options) {
verbosity = options->verbosity;
affinityFactor = options->affinityFactor;
groupSize = options->groupSize;
} else {
char *flagValue;
flagValue = Cmd_FlagReadByName("ardc_group_size");
if (flagValue != NIL(char)) {
sscanf(flagValue, "%d", &groupSize);
if (groupSize <= 0) {
fprintf(vis_stderr,
"** ardc error: invalid value %s for ardc_group_size[>0]. **\n",
flagValue);
groupSize = 8;
}
}
flagValue = Cmd_FlagReadByName("ardc_verbosity");
if (flagValue != NIL(char))
sscanf(flagValue, "%d", &verbosity);
flagValue = Cmd_FlagReadByName("ardc_affinity_factor");
if (flagValue != NIL(char)) {
sscanf(flagValue, "%f", &affinityFactor);
if (affinityFactor < 0.0 || affinityFactor > 1.0) {
fprintf(vis_stderr,
"** ardc error :invalid value %s for ardc_affinity_factor[0.0-1.0]. **\n",
flagValue);
affinityFactor = 0.5;
}
}
}
if (verbosity > 0)
initialTime = util_cpu_time();
if (options && options->readGroupFile) {
groupFile = Cmd_FileOpen(options->readGroupFile, "r", NIL(char *), 1);
if (groupFile == NIL(FILE)) {
fprintf(vis_stderr, "** ardc error : can't open file [%s] to read.\n",
options->readGroupFile);
}
}
if (groupFile) {
latchNameArray = array_alloc(char *, 0);
groupIndexArray = array_alloc(int, 0);
ArdcReadGroup(network, groupFile, latchNameArray, groupIndexArray);
subsystemInfo = Part_PartitionSubsystemInfoInit(network);
partitionArray = Part_PartCreateSubsystems(subsystemInfo,
latchNameArray, groupIndexArray);
Part_PartitionSubsystemInfoFree(subsystemInfo);
arrayForEachItem(char *, latchNameArray, i, name) {
FREE(name);
}
array_free(latchNameArray);
array_free(groupIndexArray);
fclose(groupFile);
groupFile = NIL(FILE);
} else if (groupSize > 0) {
subsystemInfo = Part_PartitionSubsystemInfoInit(network);
/*
Part_PartitionSubsystemInfoSetVerbosity(subsystemInfo, verbosity);
*/
Part_PartitionSubsystemInfoSetBound(subsystemInfo, groupSize);
Part_PartitionSubsystemInfoSetAffinityFactor(subsystemInfo, affinityFactor);
latchNameArray = array_alloc(char *, 0);
arrayForEachItem(int, presentStateVars, i, mddId) {
latch = Ntk_NetworkFindNodeByMddId(network, mddId);
name = Ntk_NodeReadName(latch);
array_insert_last(char *, latchNameArray, name);
}
partitionArray = Part_PartCreateSubsystems(subsystemInfo,
latchNameArray, NIL(array_t));
array_free(latchNameArray);
Part_PartitionSubsystemInfoFree(subsystemInfo);
} else {
partitionArray = Part_PartGroupVeriticesBasedOnHierarchy(network,
nextStateFunctions);
}
if (verbosity > 0) {
finalTime = util_cpu_time();
fprintf(vis_stdout, "grouping(state space decomposition) time = %g\n",
(double)(finalTime - initialTime) / 1000.0);
}
return(partitionArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Fsm_ArdcGetDefaultOptions | ( | Fsm_ArdcOptions_t * | options | ) |
Function********************************************************************
Synopsis [Gets default values for ARDC computatiion.]
Description [Gets default values for ARDC computatiion. Options are as follows.
set ardc_traversal_method <m> m = 0 : MBM (machine by machine, default) m = 1 : RFBF(reached frame by frame) m = 2 : TFBF(to frame by frame) m = 3 : TMBM(TFBF + MBM) m = 4 : LMBM(least fixpoint MBM) set ardc_group_size <n> n (default = 8) set ardc_affinity_factor <f> f = 0.0 - 1.0 (default = 0.5) set ardc_max_iteration <n> n (default = 0(infinity)) set ardc_constrain_target <m> m = 0 : constrain transition relation (default) m = 1 : constrain initial states m = 2 : constrain both set ardc_constrain_method <m> m = 0 : restrict (default) m = 1 : constrain m = 2 : compact (currently supported by only CUDD) m = 3 : squeeze (currently supported by only CUDD) set ardc_constrain_reorder <m> m = yes : allow variable reorderings during consecutive image constraining operations (default) m = no : don't allow variable reorderings during consecutive image constraining operations set ardc_abstract_pseudo_input <m> m = 0 : do not abstract pseudo input variables m = 1 : abstract pseudo inputs before image computation (default) m = 2 : abstract pseudo inputs at every end of image computation m = 3 : abstract pseudo inputs at the end of approximate traversal set ardc_decompose_flag <m> m = yes : keep decomposed reachable stateses (default) m = no : make a conjunction of reachable states of all submachines set ardc_projected_initial_flag <m> m = yes : use projected initial states for submachine (default) m = no : use original initial states for submachine set ardc_image_method <m> m = monolithic : use monolithic image computation for submachines m = iwls95 : use iwls95 image computation for submachines (default) m = tfm : use tfm image computation for submachines m = hybrid : use hybrid image computation for submachines set ardc_use_high_density <m> m = yes : use High Density for reachable states of submachines m = no : use BFS for reachable states of submachines (default) set ardc_create_pseudo_var_mode <m> m = 0 : makes pseudo input variables with exact support (default) m = 1 : makes pseudo input variables from all state variables of the other machines m = 2 : makes pseudo input variables from all state variables of fanin machines set ardc_reorder_ptr <m> m = yes : whenever partitioned transition relation changes, reorders partitioned transition relation m = no : no reordering of partitioned transition relation (default) set ardc_fanin_constrain_mode <m> m = 0 : constrains w.r.t. the reachable states of fanin machines (default) m = 1 : constrains w.r.t. the reachable states of both fanin machines and itself set ardc_lmbm_initial_mode <m> m = 0 : use given initial states all the time m = 1 : use current reached states as initial states (default) m = 2 : use current frontier as initial states set ardc_mbm_reuse_tr <m> m = yes : use constrained transition relation for next iteration m = no : use original transition relation for next iteration (default) set ardc_read_group <filename> <filename> file containing grouping information set ardc_write_group <filename> <filename> file to write grouping information set ardc_verbosity <n> n = 0 - 3 (default = 0) ]
SideEffects []
SeeAlso []
Definition at line 893 of file fsmArdc.c.
{
int groupSize = 8;
float affinityFactor = 0.5;
Fsm_Ardc_TraversalType_t traversalMethod = Fsm_Ardc_Traversal_Lmbm_c;
int maxIteration = 0;
Fsm_Ardc_ConstrainTargetType_t constrainTarget = Fsm_Ardc_Constrain_Tr_c;
Img_MinimizeType constrainMethod = Img_Restrict_c;
boolean decomposeFlag = TRUE;
Fsm_Ardc_AbstPpiType_t abstractPseudoInput = Fsm_Ardc_Abst_Ppi_Before_Image_c;
boolean projectedInitialFlag = TRUE;
boolean constrainReorderFlag = TRUE;
Img_MethodType ardcImageMethod = Img_Default_c;
boolean useHighDensity = FALSE;
int createPseudoVarMode = 0;
int verbosity = 0;
char *flagValue;
int value;
float affinity;
boolean reorderPtrFlag = FALSE;
int faninConstrainMode = 0;
int lmbmInitialStatesMode = 1;
int mbmReuseTrFlag = 0;
flagValue = Cmd_FlagReadByName("ardc_traversal_method");
if (flagValue != NIL(char)) {
sscanf(flagValue, "%d", &value);
switch (value) {
case 0 :
traversalMethod = Fsm_Ardc_Traversal_Mbm_c;
break;
case 1 :
traversalMethod = Fsm_Ardc_Traversal_Rfbf_c;
break;
case 2 :
traversalMethod = Fsm_Ardc_Traversal_Tfbf_c;
break;
case 3 :
traversalMethod = Fsm_Ardc_Traversal_Tmbm_c;
break;
case 4 :
traversalMethod = Fsm_Ardc_Traversal_Lmbm_c;
break;
case 5 :
traversalMethod = Fsm_Ardc_Traversal_Tlmbm_c;
break;
case 6 : /* hidden option */
traversalMethod = Fsm_Ardc_Traversal_Simple_c;
break;
default :
fprintf(vis_stderr, "** ardc error : invalid value %s", flagValue);
fprintf(vis_stderr, " for ardc_traversal_method[0-5]. **\n");
break;
}
}
options->traversalMethod = traversalMethod;
flagValue = Cmd_FlagReadByName("ardc_group_size");
if (flagValue != NIL(char)) {
sscanf(flagValue, "%d", &value);
if (value > 0)
groupSize = value;
else {
fprintf(vis_stderr,
"** ardc error : invalid value %s for ardc_group_size[>0]. **\n",
flagValue);
}
}
options->groupSize = groupSize;
flagValue = Cmd_FlagReadByName("ardc_affinity_factor");
if (flagValue != NIL(char)) {
sscanf(flagValue, "%f", &affinity);
if (affinity >= 0.0 && affinity <= 1.0)
affinityFactor = affinity;
else {
fprintf(vis_stderr,
"** ardc error : invalid value %s for ardc_affinity_factor[0.0-1.0]. **\n",
flagValue);
}
}
options->affinityFactor = affinityFactor;
flagValue = Cmd_FlagReadByName("ardc_constrain_method");
if (flagValue != NIL(char)) {
sscanf(flagValue, "%d", &value);
switch (value) {
case 0 :
constrainMethod = Img_Restrict_c;
break;
case 1 :
constrainMethod = Img_Constrain_c;
break;
case 2 :
if (bdd_get_package_name() != CUDD) {
fprintf(vis_stderr, "** ardc error : Compact in ardc_constrain_method");
fprintf(vis_stderr, " is currently supported by only CUDD. **\n");
break;
}
constrainMethod = Img_Compact_c;
break;
case 3 :
if (bdd_get_package_name() != CUDD) {
fprintf(vis_stderr, "** ardc error : Squeeze in ardc_constrain_method");
fprintf(vis_stderr, " is currently supported by only CUDD. **\n");
break;
}
constrainMethod = Img_Squeeze_c;
break;
case 4 :
constrainMethod = Img_And_c;
break;
default :
fprintf(vis_stderr,
"** ardc error : invalid value %s for ardc_constrain_method[0-4]. **\n",
flagValue);
break;
}
}
options->constrainMethod = constrainMethod;
flagValue = Cmd_FlagReadByName("ardc_constran_to");
if (flagValue != NIL(char)) {
sscanf(flagValue, "%d", &value);
switch (value) {
case 0 :
constrainTarget = Fsm_Ardc_Constrain_Tr_c;
break;
case 1 :
constrainTarget = Fsm_Ardc_Constrain_Initial_c;
break;
case 2 :
constrainTarget = Fsm_Ardc_Constrain_Both_c;
break;
default :
fprintf(vis_stderr,
"** ardc error : invalid value %s for ardc_constrain_target[0-2]. **\n",
flagValue);
break;
}
}
options->constrainTarget = constrainTarget;
flagValue = Cmd_FlagReadByName("ardc_max_iteration");
if (flagValue != NIL(char)) {
sscanf(flagValue, "%d", &value);
if (value >= 0)
maxIteration = value;
else {
fprintf(vis_stderr,
"** ardc error : invalid value %s for ardc_max_iteration[>=0]. **\n",
flagValue);
}
}
options->maxIteration = maxIteration;
flagValue = Cmd_FlagReadByName("ardc_abstract_pseudo_input");
if (flagValue != NIL(char)) {
sscanf(flagValue, "%d", &value);
switch (value) {
case 0 :
abstractPseudoInput = Fsm_Ardc_Abst_Ppi_No_c;
break;
case 1 :
abstractPseudoInput = Fsm_Ardc_Abst_Ppi_Before_Image_c;
break;
case 2 :
abstractPseudoInput = Fsm_Ardc_Abst_Ppi_After_Image_c;
break;
case 3 :
abstractPseudoInput = Fsm_Ardc_Abst_Ppi_At_End_c;
break;
default :
fprintf(vis_stderr, "** ardc error : invalid value %s", flagValue);
fprintf(vis_stderr, " for ardc_abstract_pseudo_input[0-3]. **\n");
break;
}
}
options->abstractPseudoInput = abstractPseudoInput;
decomposeFlag = FsmGetArdcSetBooleanValue("ardc_decompose_flag",
decomposeFlag);
options->decomposeFlag = decomposeFlag;
projectedInitialFlag =
FsmGetArdcSetBooleanValue("ardc_projected_initial_flag",
projectedInitialFlag);
options->projectedInitialFlag = projectedInitialFlag;
constrainReorderFlag = FsmGetArdcSetBooleanValue("ardc_constrain_reorder",
constrainReorderFlag);
options->constrainReorderFlag = constrainReorderFlag;
flagValue = Cmd_FlagReadByName("ardc_image_method");
if (flagValue != NIL(char)) {
if (strcmp(flagValue, "monolithic") == 0)
ardcImageMethod = Img_Monolithic_c;
else if (strcmp(flagValue, "iwls95") == 0)
ardcImageMethod = Img_Iwls95_c;
else if (strcmp(flagValue, "mlp") == 0)
ardcImageMethod = Img_Mlp_c;
else if (strcmp(flagValue, "tfm") == 0)
ardcImageMethod = Img_Tfm_c;
else if (strcmp(flagValue, "hybrid") == 0)
ardcImageMethod = Img_Hybrid_c;
else
fprintf(vis_stderr, "** ardc error : invalid value %s\n", flagValue);
}
options->ardcImageMethod = ardcImageMethod;
useHighDensity = FsmGetArdcSetBooleanValue("ardc_use_high_density",
useHighDensity);
options->useHighDensity = useHighDensity;
createPseudoVarMode = GetArdcSetIntValue("ardc_create_pseudo_var_mode", 0, 2,
createPseudoVarMode);
options->createPseudoVarMode = createPseudoVarMode;
reorderPtrFlag = FsmGetArdcSetBooleanValue("ardc_reorder_ptr",
reorderPtrFlag);
options->reorderPtrFlag = reorderPtrFlag;
faninConstrainMode = GetArdcSetIntValue("ardc_fanin_constrain_mode", 0, 1,
faninConstrainMode);
options->faninConstrainMode = faninConstrainMode;
flagValue = Cmd_FlagReadByName("ardc_read_group");
if (flagValue)
options->readGroupFile = flagValue;
else
options->readGroupFile = NIL(char);
flagValue = Cmd_FlagReadByName("ardc_write_group");
if (flagValue)
options->writeGroupFile = flagValue;
else
options->writeGroupFile = NIL(char);
lmbmInitialStatesMode = GetArdcSetIntValue("ardc_lmbm_initial_mode", 0, 2,
lmbmInitialStatesMode);
options->lmbmInitialStatesMode = lmbmInitialStatesMode;
mbmReuseTrFlag = FsmGetArdcSetBooleanValue("ardc_mbm_reuse_tr",
mbmReuseTrFlag);
options->mbmReuseTrFlag = mbmReuseTrFlag;
verbosity = GetArdcSetIntValue("ardc_verbosity", 0, 3, verbosity);
options->verbosity = verbosity;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Fsm_ArdcGetMddOfOverApproximateReachableStates | ( | Fsm_Fsm_t * | fsm | ) |
Function********************************************************************
Synopsis [Returns the conjunction of approximate reachable states of an FSM.]
Description [Returns the conjunction of approximate reachable states of an FSM.]
SideEffects []
SeeAlso []
Definition at line 1700 of file fsmArdc.c.
{
mdd_t *reached, *reachedSet, *tmp;
mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
array_t *reachedArray;
int i;
if (!Fsm_FsmReadCurrentOverApproximateReachableStates(fsm))
return(NIL(mdd_t));
reachedSet = mdd_one(mddManager);
reachedArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm);
arrayForEachItem(mdd_t *, reachedArray, i, reached) {
tmp = reachedSet;
reachedSet = mdd_and(reachedSet, reached, 1, 1);
mdd_free(tmp);
}
return(reachedSet);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Fsm_ArdcMinimizeTransitionRelation | ( | Fsm_Fsm_t * | fsm, |
| Img_DirectionType | fwdbwd | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Minimize transition relation of a submachine with ARDC.]
Description [Minimize transition relation of a submachine with ARDC. Direction of traversal is specified by forward(1) or backward(2) or both(3).
This function is internal to the ardc sub-package.
Perhaps you should use Fsm_MinimizeTransitionRelationWithReachabilityInfo. That function will minimize wrt exact RDCs if available. ]
SideEffects []
Definition at line 154 of file fsmArdc.c.
{
char *flagValue;
int value = 0;
int fwd = 0;
int bwd = 0;
Img_ImageInfo_t *imageInfo;
int saveStatus;
boolean reorderPtrFlag = FALSE;
switch (fwdbwd) {
case Img_Forward_c:
fwd = 1;
break;
case Img_Backward_c:
bwd = 1;
break;
case Img_Both_c:
fwd = 1;
bwd= 1;
break;
}
imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, bwd, fwd);
saveStatus = 0;
flagValue = Cmd_FlagReadByName("ardc_verbosity");
if (flagValue != NIL(char)) {
sscanf(flagValue, "%d", &value);
if (value > 1) {
saveStatus = Img_ReadPrintMinimizeStatus(imageInfo);
Img_SetPrintMinimizeStatus(imageInfo, 1);
}
}
reorderPtrFlag = FsmGetArdcSetBooleanValue("ardc_reorder_ptr",
reorderPtrFlag);
Img_MinimizeTransitionRelation(
imageInfo,
Fsm_FsmReadCurrentOverApproximateReachableStates(fsm),
Img_DefaultMinimizeMethod_c, fwdbwd, reorderPtrFlag);
if (value > 1)
Img_SetPrintMinimizeStatus(fsm->imageInfo, saveStatus);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Fsm_Ardc_AbstPpiType_t Fsm_ArdcOptionsReadAbstractPseudoInput | ( | Fsm_ArdcOptions_t * | options | ) |
| float Fsm_ArdcOptionsReadAffinityFactor | ( | Fsm_ArdcOptions_t * | options | ) |
| Img_MinimizeType Fsm_ArdcOptionsReadConstrainMethod | ( | Fsm_ArdcOptions_t * | options | ) |
| boolean Fsm_ArdcOptionsReadConstrainReorderFlag | ( | Fsm_ArdcOptions_t * | options | ) |
| Fsm_Ardc_ConstrainTargetType_t Fsm_ArdcOptionsReadConstrainTarget | ( | Fsm_ArdcOptions_t * | options | ) |
| boolean Fsm_ArdcOptionsReadDecomposeFlag | ( | Fsm_ArdcOptions_t * | options | ) |
| int Fsm_ArdcOptionsReadGroupSize | ( | Fsm_ArdcOptions_t * | options | ) |
| Img_MethodType Fsm_ArdcOptionsReadImageMethod | ( | Fsm_ArdcOptions_t * | options | ) |
| int Fsm_ArdcOptionsReadMaxIteration | ( | Fsm_ArdcOptions_t * | options | ) |
| boolean Fsm_ArdcOptionsReadProjectedInitialFlag | ( | Fsm_ArdcOptions_t * | options | ) |
| Fsm_Ardc_TraversalType_t Fsm_ArdcOptionsReadTraversalMethod | ( | Fsm_ArdcOptions_t * | options | ) |
| boolean Fsm_ArdcOptionsReadUseHighDensity | ( | Fsm_ArdcOptions_t * | options | ) |
| int Fsm_ArdcOptionsReadVerbosity | ( | Fsm_ArdcOptions_t * | options | ) |
| void Fsm_ArdcOptionsSetAbstractPseudoInput | ( | Fsm_ArdcOptions_t * | options, |
| Fsm_Ardc_AbstPpiType_t | abstractPseudoInput | ||
| ) |
| void Fsm_ArdcOptionsSetAffinityFactor | ( | Fsm_ArdcOptions_t * | options, |
| float | affinityFactor | ||
| ) |
| void Fsm_ArdcOptionsSetConstrainMethod | ( | Fsm_ArdcOptions_t * | options, |
| Img_MinimizeType | constrainMethod | ||
| ) |
| void Fsm_ArdcOptionsSetConstrainReorderFlag | ( | Fsm_ArdcOptions_t * | options, |
| int | constrainReorderFlag | ||
| ) |
Function********************************************************************
Synopsis [Sets constrain reorder flag option.]
Description [Sets constrain reorder flag option.]
SideEffects []
SeeAlso []
Definition at line 1559 of file fsmArdc.c.
{
options->constrainReorderFlag = constrainReorderFlag;
}
| void Fsm_ArdcOptionsSetConstrainTarget | ( | Fsm_ArdcOptions_t * | options, |
| Fsm_Ardc_ConstrainTargetType_t | constrainTarget | ||
| ) |
| void Fsm_ArdcOptionsSetDecomposeFlag | ( | Fsm_ArdcOptions_t * | options, |
| boolean | decomposeFlag | ||
| ) |
| void Fsm_ArdcOptionsSetGroupSize | ( | Fsm_ArdcOptions_t * | options, |
| int | groupSize | ||
| ) |
| void Fsm_ArdcOptionsSetImageMethod | ( | Fsm_ArdcOptions_t * | options, |
| Img_MethodType | ardcImageMethod | ||
| ) |
| void Fsm_ArdcOptionsSetMaxIteration | ( | Fsm_ArdcOptions_t * | options, |
| int | maxIteration | ||
| ) |
| void Fsm_ArdcOptionsSetProjectedInitialFlag | ( | Fsm_ArdcOptions_t * | options, |
| boolean | projectedInitialFlag | ||
| ) |
| void Fsm_ArdcOptionsSetTraversalMethod | ( | Fsm_ArdcOptions_t * | options, |
| Fsm_Ardc_TraversalType_t | traversalMethod | ||
| ) |
| void Fsm_ArdcOptionsSetUseHighDensity | ( | Fsm_ArdcOptions_t * | options, |
| boolean | useHighDensity | ||
| ) |
| void Fsm_ArdcOptionsSetVerbosity | ( | Fsm_ArdcOptions_t * | options, |
| int | verbosity | ||
| ) |
| void Fsm_ArdcPrintReachabilityResults | ( | Fsm_Fsm_t * | fsm, |
| long | elapseTime | ||
| ) |
Function********************************************************************
Synopsis [Prints info about overapproximate reachable states.]
Description [Prints info about overapproximate reachable states.]
SideEffects []
SeeAlso []
Definition at line 1733 of file fsmArdc.c.
{
array_t *psVars = Fsm_FsmReadPresentStateVars(fsm);
mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm);
int nvars = mdd_get_number_of_bdd_vars(mddMgr, psVars);
char apprStr[24], ardcStr[24];
if (nvars <= EPD_MAX_BIN) {
double mintermAppr, mintermArdc;
mintermAppr = Fsm_ArdcCountOnsetOfOverApproximateReachableStates(fsm);
sprintf(apprStr, "%10g", mintermAppr);
mintermArdc = pow((double)2.0, (double)nvars) - mintermAppr;
sprintf(ardcStr, "%10g", mintermArdc);
} else {
EpDouble apprEpd, ardcEpd;
ArdcEpdCountOnsetOfOverApproximateReachableStates(fsm, &apprEpd);
EpdPow2(nvars, &ardcEpd);
EpdSubtract2(&ardcEpd, &apprEpd);
EpdGetString(&apprEpd, apprStr);
EpdGetString(&ardcEpd, ardcStr);
}
(void)fprintf(vis_stdout,"***********************************************\n");
(void)fprintf(vis_stdout,"Over-approximate Reachability analysis results:\n");
(void)fprintf(vis_stdout, "%-30s%s\n", "reachable states = ", apprStr);
(void)fprintf(vis_stdout, "%-30s%s\n", "unreachable states(ARDCs) = ",
ardcStr);
(void)fprintf(vis_stdout, "%-30s%10d\n", "BDD size = ",
Fsm_ArdcBddSizeOfOverApproximateReachableStates(fsm));
(void)fprintf(vis_stdout, "%-30s%10g\n", "analysis time = ",
(double)elapseTime / 1000.0);
switch (FsmReadReachabilityOverApproxComputationStatus(fsm)) {
case Fsm_Ardc_NotConverged_c :
(void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ",
"not converged(invalid)");
break;
case Fsm_Ardc_Valid_c :
(void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ",
"not converged(valid)");
break;
case Fsm_Ardc_Converged_c :
(void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ",
"converged");
break;
case Fsm_Ardc_Exact_c :
(void) fprintf(vis_stdout, "%-30s%10s\n", "reachability status = ",
"exact");
break;
default :
break;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int Fsm_ArdcReadVerbosity | ( | void | ) |
Function********************************************************************
Synopsis [Reads ARDC verbosity option.]
Description [Reads ARDC verbosity option.]
SideEffects []
SeeAlso []
Definition at line 1800 of file fsmArdc.c.
{
char *flagValue;
int verbosity = 0;
flagValue = Cmd_FlagReadByName("ardc_verbosity");
if (flagValue != NIL(char))
sscanf(flagValue, "%d", &verbosity);
return(verbosity);
}
Here is the call graph for this function:
| array_t* Fsm_FsmComputeOverApproximateReachableStates | ( | Fsm_Fsm_t * | fsm, |
| int | incrementalFlag, | ||
| int | verbosityLevel, | ||
| int | printStep, | ||
| int | depthValue, | ||
| int | shellFlag, | ||
| int | reorderFlag, | ||
| int | reorderThreshold, | ||
| int | recompute | ||
| ) |
Function********************************************************************
Synopsis [Computes overapproximate reachable states.]
Description [Computes overapproximate reachable states. This function is a wrapper around Fsm_ArdcComputeOverApproximateReachableStates.]
SideEffects []
SeeAlso [Fsm_ArdcComputeOverApproximateReachableStates]
Definition at line 247 of file fsmArdc.c.
{
array_t *apprReachableStates;
Fsm_ArdcOptions_t options;
Fsm_ArdcGetDefaultOptions(&options);
if (printStep && options.verbosity < 2)
printStep = 0;
apprReachableStates = Fsm_ArdcComputeOverApproximateReachableStates(fsm,
incrementalFlag, verbosityLevel, printStep, depthValue, shellFlag,
reorderFlag, reorderThreshold, recompute, &options);
return(apprReachableStates);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int FsmArdcCheckInvariant | ( | Fsm_Fsm_t * | fsm, |
| array_t * | invarStates | ||
| ) |
Function********************************************************************
Synopsis [Check if each conjunct is contained in the invariant.]
Description [Check if each conjunct is contained in the invariant.]
SideEffects []
SeeAlso []
Definition at line 1828 of file fsmArdc.c.
{
array_t *overApproxArray;
mdd_t *conjunct;
int i, j;
mdd_t *invariant;
overApproxArray = Fsm_ArdcComputeOverApproximateReachableStates(fsm,
0, 0, 0, 0, 0, 0, 0, 0, NIL(Fsm_ArdcOptions_t));
/* for each invariant check if the over approx holds */
arrayForEachItem(mdd_t *, invarStates, i, invariant) {
arrayForEachItem(mdd_t *, overApproxArray, j, conjunct) {
if (conjunct == NIL(mdd_t))
continue;
if (!mdd_lequal(conjunct, invariant, 1, 1))
return 0;
}
}
return 1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void FsmArdcPrintArrayOfArrayInt | ( | array_t * | arrayOfArray | ) |
Function********************************************************************
Synopsis [Prints array of array of integer.]
Description [Prints array of array of integer.]
SideEffects []
SeeAlso []
Definition at line 2124 of file fsmArdc.c.
{
int i, j, n;
array_t *array;
for (i = 0; i < array_n(arrayOfArray); i++) {
array = array_fetch(array_t *, arrayOfArray, i);
fprintf(vis_stdout, "array[%d] =", i);
for (j = 0; j < array_n(array); j++) {
n = array_fetch(int, array, j);
fprintf(vis_stdout, " %d", n);
}
fprintf(vis_stdout, "\n");
}
}
| void FsmArdcPrintBddOfNode | ( | Fsm_Fsm_t * | fsm, |
| mdd_t * | node | ||
| ) |
Function********************************************************************
Synopsis [Prints BDDs of a node.]
Description [Prints BDDs of a node.]
SideEffects []
SeeAlso []
Definition at line 2106 of file fsmArdc.c.
{
PrintBddWithName(fsm, NIL(array_t), node);
}
Here is the call graph for this function:
| void FsmArdcPrintExactReachableStates | ( | Fsm_Fsm_t * | fsm | ) |
Function********************************************************************
Synopsis [Prints BDDS of exact reachable states of an FSM.]
Description [Prints BDDS of exact reachable states of an FSM.]
SideEffects []
SeeAlso []
Definition at line 2079 of file fsmArdc.c.
{
mdd_t *reachableStates;
array_t *mddIdArr;
if (!Fsm_FsmTestIsReachabilityDone(fsm)) {
fprintf(vis_stdout, "** ardc warning : no reachable states **\n");
return;
}
reachableStates = Fsm_FsmReadReachableStates(fsm);
mddIdArr = Fsm_FsmReadPresentStateVars(fsm);
PrintBddWithName(fsm, mddIdArr, reachableStates);
}
Here is the call graph for this function:
| void FsmArdcPrintOptions | ( | void | ) |
Function********************************************************************
Synopsis [Prints ARDC options currently in use.]
Description [Prints ARDC options currently in use.]
SideEffects []
SeeAlso []
Definition at line 1863 of file fsmArdc.c.
{
Fsm_ArdcOptions_t options;
char dummy[31];
Fsm_ArdcGetDefaultOptions(&options);
switch (options.traversalMethod) {
case Fsm_Ardc_Traversal_Mbm_c :
sprintf(dummy, "MBM");
break;
case Fsm_Ardc_Traversal_Rfbf_c :
sprintf(dummy, "RFBF");
break;
case Fsm_Ardc_Traversal_Tfbf_c :
sprintf(dummy, "TFBF");
break;
case Fsm_Ardc_Traversal_Tmbm_c :
sprintf(dummy, "TMBM");
break;
case Fsm_Ardc_Traversal_Lmbm_c :
sprintf(dummy, "LMBM");
break;
case Fsm_Ardc_Traversal_Tlmbm_c :
sprintf(dummy, "TLMBM");
break;
case Fsm_Ardc_Traversal_Simple_c :
sprintf(dummy, "SIMPLE");
break;
default :
sprintf(dummy, "invalid");
break;
}
fprintf(vis_stdout, "ARDC: ardc_traversal_method = %d (%s)\n",
options.traversalMethod, dummy);
fprintf(vis_stdout, "ARDC: ardc_group_size = %d\n", options.groupSize);
fprintf(vis_stdout, "ARDC: ardc_affinity_factor = %f\n",
options.affinityFactor);
fprintf(vis_stdout, "ARDC: ardc_max_iteration = %d\n", options.maxIteration);
switch (options.constrainTarget) {
case Fsm_Ardc_Constrain_Tr_c :
sprintf(dummy, "transition relation");
break;
case Fsm_Ardc_Constrain_Initial_c :
sprintf(dummy, "initial");
break;
case Fsm_Ardc_Constrain_Both_c :
sprintf(dummy, "both");
break;
default :
sprintf(dummy, "invalid");
break;
}
fprintf(vis_stdout, "ARDC: ardc_constrain_target = %d (%s)\n",
options.constrainTarget, dummy);
switch (options.constrainMethod) {
case Img_Restrict_c :
sprintf(dummy, "restrict");
break;
case Img_Constrain_c :
sprintf(dummy, "constrain");
break;
case Img_Compact_c :
sprintf(dummy, "compact");
break;
case Img_Squeeze_c :
sprintf(dummy, "squeeze");
break;
case Img_And_c :
sprintf(dummy, "and");
break;
case Img_DefaultMinimizeMethod_c :
sprintf(dummy, "restrict");
break;
default :
sprintf(dummy, "invalid");
break;
}
fprintf(vis_stdout, "ARDC: ardc_constrain_method = %d (%s)\n",
options.constrainMethod, dummy);
if (options.constrainReorderFlag)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "ARDC: ardc_constrain_reorder = %s\n", dummy);
if (options.decomposeFlag)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "ARDC: ardc_decompose_flag = %s\n", dummy);
switch (options.abstractPseudoInput) {
case Fsm_Ardc_Abst_Ppi_No_c :
sprintf(dummy, "no");
break;
case Fsm_Ardc_Abst_Ppi_Before_Image_c :
sprintf(dummy, "before image");
break;
case Fsm_Ardc_Abst_Ppi_After_Image_c :
sprintf(dummy, "after image");
break;
case Fsm_Ardc_Abst_Ppi_At_End_c :
sprintf(dummy, "at end");
break;
default :
sprintf(dummy, "invalid");
break;
}
fprintf(vis_stdout, "ARDC: ardc_abstract_pseudo_input = %d (%s)\n",
options.abstractPseudoInput, dummy);
if (options.projectedInitialFlag)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "ARDC: ardc_projected_initial_flag = %s\n", dummy);
if (options.ardcImageMethod == Img_Monolithic_c)
sprintf(dummy, "monolithic");
else if (options.ardcImageMethod == Img_Tfm_c)
sprintf(dummy, "tfm");
else if (options.ardcImageMethod == Img_Hybrid_c)
sprintf(dummy, "hybrid");
else if (options.ardcImageMethod == Img_Mlp_c)
sprintf(dummy, "mlp");
else
sprintf(dummy, "iwls95");
fprintf(vis_stdout, "ARDC: ardc_image_method = %s\n", dummy);
if (options.useHighDensity)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "ARDC: ardc_use_high_density = %s\n", dummy);
if (options.reorderPtrFlag)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "ARDC: ardc_reorder_ptr = %s\n", dummy);
if (options.faninConstrainMode == 0)
sprintf(dummy, "only fanin");
else
sprintf(dummy, "fanin + itself");
fprintf(vis_stdout, "ARDC: ardc_fanin_constrain_mode = %d (%s)\n",
options.faninConstrainMode, dummy);
if (options.createPseudoVarMode == 0)
sprintf(dummy, "with exact support");
else if (options.createPseudoVarMode == 1)
sprintf(dummy, "all the other submachines");
else
sprintf(dummy, "only fanin submachines");
fprintf(vis_stdout, "ARDC: ardc_create_pseudo_var_mode = %d (%s)\n",
options.createPseudoVarMode, dummy);
if (options.lmbmInitialStatesMode == 0)
sprintf(dummy, "given initial");
else if (options.lmbmInitialStatesMode == 1)
sprintf(dummy, "reached set");
else
sprintf(dummy, "frontier set");
fprintf(vis_stdout, "ARDC: ardc_lmbm_initial_mode = %d (%s)\n",
options.lmbmInitialStatesMode, dummy);
if (options.mbmReuseTrFlag)
sprintf(dummy, "yes");
else
sprintf(dummy, "no");
fprintf(vis_stdout, "ARDC: ardc_mbm_reuse_tr = %s\n", dummy);
if (options.readGroupFile)
fprintf(vis_stdout, "ARDC: ardc_read_group = %s\n", options.readGroupFile);
else
fprintf(vis_stdout, "ARDC: ardc_read_group = nil\n");
if (options.writeGroupFile) {
fprintf(vis_stdout, "ARDC: ardc_write_group = %s\n",
options.writeGroupFile);
} else
fprintf(vis_stdout, "ARDC: ardc_write_group = nil\n");
fprintf(vis_stdout, "ARDC: ardc_verbosity = %d\n", options.verbosity);
fprintf(vis_stdout,
"See help page on print_ardc_options for setting these options\n");
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void FsmArdcPrintOverApproximateReachableStates | ( | Fsm_Fsm_t * | fsm | ) |
Function********************************************************************
Synopsis [Prints BDDS of approximate reachable states of an FSM.]
Description [Prints BDDS of approximate reachable states of an FSM.]
SideEffects []
SeeAlso []
Definition at line 2053 of file fsmArdc.c.
{
mdd_t *appr;
array_t *mddIdArr;
if (!Fsm_FsmTestIsOverApproximateReachabilityDone(fsm)) {
fprintf(vis_stdout, "** ardc warning : no approximate reachable states **\n");
return;
}
appr = Fsm_ArdcGetMddOfOverApproximateReachableStates(fsm);
mddIdArr = Fsm_FsmReadPresentStateVars(fsm);
PrintBddWithName(fsm, mddIdArr, appr);
}
Here is the call graph for this function:
| boolean FsmGetArdcSetBooleanValue | ( | char * | string, |
| boolean | defaultValue | ||
| ) |
Function********************************************************************
Synopsis [Returns a set Boolean value related ARDC computation.]
Description [Returns a set Boolean value related ARDC computation.]
SideEffects []
SeeAlso []
Definition at line 2152 of file fsmArdc.c.
{
char *flagValue;
boolean value = defaultValue;
flagValue = Cmd_FlagReadByName(string);
if (flagValue != NIL(char)) {
if (strcmp(flagValue, "yes") == 0)
value = TRUE;
else if (strcmp(flagValue, "no") == 0)
value = FALSE;
else {
fprintf(vis_stderr,
"** ardc error : invalid value %s for %s[yes/no]. **\n",
flagValue, string);
}
}
return(value);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int GetArdcSetIntValue | ( | char * | string, |
| int | l, | ||
| int | u, | ||
| int | defaultValue | ||
| ) | [static] |
Function********************************************************************
Synopsis [Returns a set integer value related ARDC computation.]
Description [Returns a set integer value related ARDC computation.]
SideEffects []
SeeAlso []
Definition at line 4230 of file fsmArdc.c.
{
char *flagValue;
int tmp;
int value = defaultValue;
flagValue = Cmd_FlagReadByName(string);
if (flagValue != NIL(char)) {
sscanf(flagValue, "%d", &tmp);
if (tmp >= l && (tmp <= u || u == 0))
value = tmp;
else {
fprintf(vis_stderr,
"** ardc error : invalid value %d for %s[%d-%d]. **\n", tmp, string,
l, u);
}
}
return(value);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void MinimizeTransitionRelationWithFaninConstraint | ( | Img_ImageInfo_t * | imageInfo, |
| array_t * | faninConstrainArray, | ||
| Img_MinimizeType | constrainMethod, | ||
| boolean | reorderPtrFlag, | ||
| boolean | duplicate | ||
| ) | [static] |
Function********************************************************************
Synopsis [Minimizes transition relation with fanin constraint.]
Description [Minimizes transition relation with fanin constraint.]
SideEffects []
SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal]
Definition at line 3845 of file fsmArdc.c.
{
if (duplicate) {
Img_DupTransitionRelation(imageInfo, Img_Forward_c);
Img_ResetTrMinimizedFlag(imageInfo, Img_Forward_c);
}
Img_MinimizeTransitionRelation(imageInfo, faninConstrainArray,
constrainMethod, Img_Forward_c,
reorderPtrFlag);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void PrintBddWithName | ( | Fsm_Fsm_t * | fsm, |
| array_t * | mddIdArr, | ||
| mdd_t * | node | ||
| ) | [static] |
Function********************************************************************
Synopsis [Prints bdd variable names and levels of mddIdArr, and minterms.]
Description [Prints bdd variable names and levels of mddIdArr, and minterms.]
SideEffects []
SeeAlso []
Definition at line 4070 of file fsmArdc.c.
{
int i, j, size;
mdd_manager *mddManager;
array_t *mvarArray;
mvar_type mv;
int bddId, mddId, varLevel;
bdd_t *varBdd;
if (!node)
return;
mddManager = Fsm_FsmReadMddManager(fsm);
if (!mddIdArr)
mddIdArr = mdd_get_support(mddManager, node);
mvarArray = mdd_ret_mvar_list(mddManager);
size = array_n(mddIdArr);
for (i = 0; i < size; i++) {
mddId = array_fetch(int, mddIdArr, i);
mv = array_fetch(mvar_type, mvarArray, mddId);
for (j = 0; j < mv.encode_length; j++) {
bddId = mdd_ret_bvar_id(&mv, j);
varBdd = bdd_get_variable(mddManager, bddId);
varLevel = bdd_top_var_level(mddManager, varBdd);
if (mv.encode_length == 1)
fprintf(vis_stdout, "%s %d\n", mv.name, varLevel);
else
fprintf(vis_stdout, "%s[%d] %d\n", mv.name, j, varLevel);
bdd_free(varBdd);
}
}
bdd_print_minterm(node);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void PrintCurrentReachedStates | ( | mdd_manager * | mddManager, |
| Fsm_Fsm_t ** | subFsm, | ||
| mdd_t ** | reached, | ||
| Fsm_Ardc_TraversalType_t | method, | ||
| int | nSubFsms, | ||
| int | iteration, | ||
| int | nvars, | ||
| int | ardcVerbosity, | ||
| boolean | supportCheckFlag | ||
| ) | [static] |
Function********************************************************************
Synopsis [Prints current approximate reached states.]
Description [Prints current approximate reached states.]
SideEffects []
SeeAlso []
Definition at line 3977 of file fsmArdc.c.
{
int i;
char string[24];
double tmpReached;
if (nvars <= EPD_MAX_BIN) {
double numReached = 1.0, tmpReached;
for (i = 0; i < nSubFsms; i++) {
tmpReached = mdd_count_onset(mddManager, reached[i],
subFsm[i]->fsmData.presentStateVars);
if (ardcVerbosity > 1) {
if (ardcVerbosity > 2 && supportCheckFlag) {
assert(mdd_check_support(mddManager, reached[i],
subFsm[i]->fsmData.presentStateVars));
}
fprintf(vis_stdout, "# of reached for subFsm[%d] = %g\n",
i, tmpReached);
}
numReached *= tmpReached;
}
sprintf(string, "%g", numReached);
} else {
EpDouble epd;
EpdConvert((double)1.0, &epd);
for (i = 0; i < nSubFsms; i++) {
tmpReached = mdd_count_onset(mddManager, reached[i],
subFsm[i]->fsmData.presentStateVars);
if (ardcVerbosity > 1) {
if (ardcVerbosity > 2 && supportCheckFlag) {
assert(mdd_check_support(mddManager, reached[i],
subFsm[i]->fsmData.presentStateVars));
}
fprintf(vis_stdout, "# of reached for subFsm[%d] = %g\n",
i, tmpReached);
}
EpdMultiply(&epd, tmpReached);
}
EpdGetString(&epd, string);
}
switch (method) {
case Fsm_Ardc_Traversal_Mbm_c :
fprintf(vis_stdout, "MBM : iteration %d, # of reached = %s\n",
iteration, string);
break;
case Fsm_Ardc_Traversal_Rfbf_c :
fprintf(vis_stdout, "RFBF : iteration %d, # of reached = %s\n",
iteration, string);
break;
case Fsm_Ardc_Traversal_Tfbf_c :
fprintf(vis_stdout, "TFBF : iteration %d, # of reached = %s\n",
iteration, string);
break;
case Fsm_Ardc_Traversal_Tmbm_c :
fprintf(vis_stdout, "TMBM : iteration %d, # of reached = %s\n",
iteration, string);
break;
case Fsm_Ardc_Traversal_Lmbm_c :
fprintf(vis_stdout, "LMBM : iteration %d, # of reached = %s\n",
iteration, string);
break;
case Fsm_Ardc_Traversal_Tlmbm_c :
fprintf(vis_stdout, "TLMBM : iteration %d, # of reached = %s\n",
iteration, string);
break;
case Fsm_Ardc_Traversal_Simple_c :
fprintf(vis_stdout, "SIMPLE : # of reached = %s\n", string);
break;
default :
break;
}
}
Here is the caller graph for this function:
| static void PrintTfmStatistics | ( | array_t * | subFsmArray | ) | [static] |
Function********************************************************************
Synopsis [Prints statistics of transition function method.]
Description [Prints statistics of transition function method.]
SideEffects []
SeeAlso []
Definition at line 4352 of file fsmArdc.c.
{
int i;
Img_ImageInfo_t *imageInfo;
Fsm_Fsm_t *subFsm;
double tInserts, tLookups, tHits, tEntries;
double inserts, lookups, hits, entries;
int nSlots, tSlots, maxChainLength;
float avgDepth, tAvgDepth, avgDecomp, tAvgDecomp;
int tRecurs, tLeaves, tTurns, tDecomps, minDecomp;
int nRecurs, nLeaves, nTurns;
int nDecomps, topDecomp, maxDecomp, tMaxDecomp;
int maxDepth, tMaxDepth;
int flag, globalCache;
tInserts = tLookups = tHits = tEntries = 0.0;
tSlots = 0;
tRecurs = tLeaves = tTurns = tDecomps = 0;
tAvgDepth = tAvgDecomp = 0.0;
tMaxDecomp = tMaxDepth = 0;
minDecomp = 10000000; /* arbitrarily large number */
globalCache = Img_TfmCheckGlobalCache(0);
if (globalCache) {
flag = Img_TfmGetCacheStatistics(NIL(Img_ImageInfo_t), 0, &inserts,
&lookups, &hits, &entries, &nSlots,
&maxChainLength);
tInserts = inserts;
tLookups = lookups;
tHits = hits;
tEntries = entries;
tSlots = nSlots;
}
for (i = 0; i < array_n(subFsmArray); i++) {
subFsm = array_fetch(Fsm_Fsm_t *, subFsmArray, i);
imageInfo = Fsm_FsmReadOrCreateImageInfo(subFsm, 0, 1);
if (!globalCache) {
flag = Img_TfmGetCacheStatistics(imageInfo, 0, &inserts, &lookups, &hits,
&entries, &nSlots, &maxChainLength);
if (flag) {
tInserts += inserts;
tLookups += lookups;
tHits += hits;
tEntries += entries;
tSlots += nSlots;
}
}
flag = Img_TfmGetRecursionStatistics(imageInfo, 0, &nRecurs, &nLeaves,
&nTurns, &avgDepth, &maxDepth, &nDecomps,
&topDecomp, &maxDecomp, &avgDecomp);
if (flag) {
tAvgDepth = (tAvgDepth * (float)tLeaves + avgDepth * (float)nLeaves) /
(float)(tLeaves + nLeaves);
tRecurs += nRecurs;
tLeaves += nLeaves;
tTurns += nTurns;
tAvgDecomp = (tAvgDecomp * (float)tDecomps +
avgDecomp * (float)nDecomps) / (float)(tDecomps + nDecomps);
tDecomps += nDecomps;
if (topDecomp < minDecomp)
minDecomp = topDecomp;
if (maxDecomp > tMaxDecomp)
tMaxDecomp = maxDecomp;
if (maxDepth > tMaxDepth)
tMaxDepth = maxDepth;
}
}
if (tInserts != 0.0) {
if (globalCache) {
fprintf(vis_stdout,
"** global cache statistics of transition function **\n");
} else
fprintf(vis_stdout, "** cache statistics of transition function **\n");
fprintf(vis_stdout, "# insertions = %g\n", tInserts);
fprintf(vis_stdout, "# lookups = %g\n", tLookups);
fprintf(vis_stdout, "# hits = %g (%.2f%%)\n", tHits,
tHits / tLookups * 100.0);
fprintf(vis_stdout, "# misses = %g (%.2f%%)\n", tLookups - tHits,
(tLookups - tHits) / tLookups * 100.0);
fprintf(vis_stdout, "# entries = %g\n", tEntries);
if (tSlots > 0) {
fprintf(vis_stdout, "# slots = %d\n", tSlots);
fprintf(vis_stdout, "maxChainLength = %d\n", maxChainLength);
}
}
if (tRecurs != 0) {
fprintf(vis_stdout, "** recursion statistics of transition function **\n");
fprintf(vis_stdout, "# recursions = %d\n", tRecurs);
fprintf(vis_stdout, "# leaves = %d\n", tLeaves);
fprintf(vis_stdout, "# turns = %d\n", tTurns);
fprintf(vis_stdout, "# average recursion depth = %g (max = %d)\n",
tAvgDepth, tMaxDepth);
fprintf(vis_stdout,
"# decompositions = %d (top = %d, max = %d, average = %g)\n",
tDecomps, minDecomp, tMaxDecomp, tAvgDecomp);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static mdd_t * QuantifyVariables | ( | mdd_t * | state, |
| array_t * | smoothArray, | ||
| mdd_t * | smoothCube | ||
| ) | [static] |
Function********************************************************************
Synopsis [Quantifies out smoothing variables.]
Description [Quantifies out smoothing variables. If the bdd package is CUDD, it performs with a cube for better efficiency. Otherwise, it uses conventional mdd id array. smoothArray should be an array of bdd variables.]
SideEffects []
SeeAlso []
Definition at line 4301 of file fsmArdc.c.
{
if (smoothCube)
return(bdd_smooth_with_cube(state, smoothCube));
else
return(bdd_smooth(state, smoothArray));
}
Here is the caller graph for this function:
| static void SortSubFsmsForApproximateTraversal | ( | array_t ** | subFsmArray, |
| array_t ** | fanInsIndexArray, | ||
| array_t ** | fanOutsIndexArray, | ||
| int | verbosityLevel | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Sorts subfsms so that a subfsm with smaller fanins comes first.]
Description [Sorts subfsms so that a subfsm with smaller fanins comes first.]
SideEffects []
SeeAlso []
Definition at line 2192 of file fsmArdc.c.
{
int n = array_n(*subFsmArray);
array_t *newSubFsmArray;
array_t *newFanInsIndexArray;
array_t *newFanOutsIndexArray;
int i, j, smallest;
Fsm_Fsm_t *subFsm;
array_t *fanIns, *fanOuts;
Fsm_Fsm_t *smallestSubFsm = NIL(Fsm_Fsm_t);
array_t *smallestFanIns = NIL(array_t);
array_t *smallestFanOuts = NIL(array_t);
int *flag;
int *nFanIns, *nFanOuts;
int fanIn, fanOut;
int *order = NIL(int);
int *target;
newSubFsmArray = array_alloc(Fsm_Fsm_t *, 0);
newFanInsIndexArray = array_alloc(array_t *, 0);
newFanOutsIndexArray = array_alloc(array_t *, 0);
flag = ALLOC(int, n);
(void)memset((void *)flag, 0, sizeof(int) * n);
if (verbosityLevel > 1)
order = ALLOC(int, n);
target = ALLOC(int, n);
nFanIns = ALLOC(int, n);
nFanOuts = ALLOC(int, n);
for (i = 0; i < n; i++) {
fanIns = array_fetch(array_t *, *fanInsIndexArray, i);
nFanIns[i] = array_n(fanIns);
fanOuts = array_fetch(array_t *, *fanOutsIndexArray, i);
nFanOuts[i] = array_n(fanOuts);
}
for (i = 0; i < n; i++) {
/*
** finds a submachine which has the smallest number of fanins
** if tie, use number of fanouts
*/
smallest = -1;
for (j = 0; j < n; j++) {
if (flag[j])
continue;
subFsm = array_fetch(Fsm_Fsm_t *, *subFsmArray, j);
fanIns = array_fetch(array_t *, *fanInsIndexArray, j);
fanOuts = array_fetch(array_t *, *fanOutsIndexArray, j);
if (smallest == -1 || nFanIns[j] < nFanIns[smallest] ||
(nFanIns[j] == nFanIns[smallest] &&
nFanOuts[j] < nFanOuts[smallest])) {
smallest = j;
smallestSubFsm = subFsm;
smallestFanIns = fanIns;
smallestFanOuts = fanOuts;
}
}
target[smallest] = i;
if (verbosityLevel > 1)
order[i] = smallest;
flag[smallest] = 1;
array_insert_last(Fsm_Fsm_t *, newSubFsmArray, smallestSubFsm);
array_insert_last(array_t *, newFanInsIndexArray, smallestFanIns);
array_insert_last(array_t *, newFanOutsIndexArray, smallestFanOuts);
/*
** decrease number of fanouts by 1 from each submachine
** which is not chosen yet
*/
for (j = 0; j < array_n(smallestFanIns); j++) {
fanIn = array_fetch(int, smallestFanIns, j);
if (flag[fanIn])
continue;
nFanOuts[fanIn]--;
}
/*
** decrease number of fanins by 1 from each submachine
** which is not chosen yet
*/
for (j = 0; j < array_n(smallestFanOuts); j++) {
fanOut = array_fetch(int, smallestFanOuts, j);
if (flag[fanOut])
continue;
nFanIns[fanOut]--;
}
}
/* make new fanins & fanouts index array according to new order */
for (i = 0; i < n; i++) {
fanIns = array_fetch(array_t *, newFanInsIndexArray, i);
for (j = 0; j < array_n(fanIns); j++) {
fanIn = array_fetch(int, fanIns, j);
array_insert(int, fanIns, j, target[fanIn]);
}
fanOuts = array_fetch(array_t *, newFanOutsIndexArray, i);
for (j = 0; j < array_n(fanOuts); j++) {
fanOut = array_fetch(int, fanOuts, j);
array_insert(int, fanOuts, j, target[fanOut]);
}
}
if (verbosityLevel > 1) {
int k;
fprintf(vis_stdout, "=== sorted sub-fsm order ===\n");
for (i = 0; i < n; i++)
fprintf(vis_stdout, " %d", order[i]);
fprintf(vis_stdout, "\n");
for (i = 0; i < n; i++) {
fprintf(vis_stdout, "SUB-FSM [%d]\n", i);
fanIns = array_fetch(array_t *, newFanInsIndexArray, i);
fanOuts = array_fetch(array_t *, newFanOutsIndexArray, i);
fprintf(vis_stdout, "== fanins(%d) :", array_n(fanIns));
for (j = 0; j < array_n(fanIns); j++) {
k = array_fetch(int, fanIns, j);
fprintf(vis_stdout, " %d", k);
}
fprintf(vis_stdout, "\n");
fprintf(vis_stdout, "== fanouts(%d) :", array_n(fanOuts));
for (j = 0; j < array_n(fanOuts); j++) {
k = array_fetch(int, fanOuts, j);
fprintf(vis_stdout, " %d", k);
}
fprintf(vis_stdout, "\n");
}
}
FREE(flag);
FREE(nFanIns);
FREE(nFanOuts);
if (verbosityLevel > 1)
FREE(order);
FREE(target);
array_free(*subFsmArray);
array_free(*fanInsIndexArray);
array_free(*fanOutsIndexArray);
*subFsmArray = newSubFsmArray;
*fanInsIndexArray = newFanInsIndexArray;
*fanOutsIndexArray = newFanOutsIndexArray;
}
Here is the caller graph for this function:
| static void UpdateMbmEventSchedule | ( | Fsm_Fsm_t ** | subFsm, |
| array_t * | fanOutIndices, | ||
| int * | traverse, | ||
| int | lfpFlag | ||
| ) | [static] |
Function********************************************************************
Synopsis [Updates event scheduling of submachines for traversal.]
Description [Updates event scheduling of submachines for traversal.]
SideEffects []
SeeAlso []
Definition at line 4322 of file fsmArdc.c.
{
int i, fanout;
arrayForEachItem(int, fanOutIndices, i, fanout) {
if (lfpFlag) {
if (!subFsm[fanout]->reachabilityInfo.reachableStates ||
!bdd_is_tautology(subFsm[fanout]->reachabilityInfo.reachableStates,
1)) {
traverse[fanout] = 1;
}
} else
traverse[fanout] = 1;
}
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: fsmArdc.c,v 1.86 2009/04/12 00:44:04 fabio Exp $" [static] |
CFile***********************************************************************
FileName [fsmArdc.c]
PackageName [fsm]
Synopsis [Routines to perform overapproximate reachability on the FSM structure.]
Description [The basic algorithms are almost same as the one in Hyunwoo Cho's paper in TCAD96, except as noted below. To read the functions in this file, it is strongly recommended to read that paper first and In-Ho Moon's paper in ICCAD98.
0. Cho's algorithm uses transition function for image computation, whereas we use transition relation. 1. constrainTarget In Cho's papers, there are two versions of algorithms: one is constraining transition relation, the other is initial states, so this function includes these two as well as the case of both. 0) Fsm_Ardc_Constrain_Tr_c : constrain transition relation (default). 1) Fsm_Ardc_Constrain_Initial_c : constrain initial state. 2) Fsm_Ardc_Constrain_Both_c : constrain both. 2. decomposeFlag To do above constraining operation, we can make the constraint either conjoined (as single bdd) or decomposed (as array of bdds) from the reachable states of fanin submachines of the current submachine. To have same interface for these two, array of constraints is used. 3. dynamic variable reordering In Cho's algorithm, dynamic variable ordering is not allowed, but it is allowed here. Also, refer to 5. restore-containment. 4. abstractPseudoInput To make convergence faster, we can abstract pseudo primary input variables early, but refer to 5. restore-containment. 0) Fsm_Ardc_Abst_Ppi_No_c : do not abstract pseudo input variables. 1) Fsm_Ardc_Abst_Ppi_Before_Image_c : abstract before image computation (default). 2) Fsm_Ardc_Abst_Ppi_After_Image_c : abstract after image computation. 3) Fsm_Ardc_Abst_Ppi_At_End_c : abstract at the end of approximate traversal. 5. restore-constainment Due to 3 (dynamic variable reordering) and 4 (abstractPseudoInput), current reachable states may not be subset of previous reachable states. In this case, we correct current reachable states to the intersection of current and previous reachable states in MBM. However, in FBF, we need to take union of the two. 6. projectedInitialFlag When we do reachability analysis of submachines, initial states of a submachine can be one of the followings. In Cho's paper, projected initial states was used. 0) FALSE : use original initial states for submachine 1) TRUE : use projected initial states for submachine (default) ]
Author [In-Ho Moon]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
