VIS
|
00001 00032 #include "fsmInt.h" 00033 #include "bdd.h" 00034 #include "ntm.h" 00035 #include "img.h" 00036 #include "sim.h" 00037 00038 static char rcsid[] UNUSED = "$Id: fsmReach.c,v 1.102 2009/04/11 01:40:54 fabio Exp $"; 00039 00040 /*---------------------------------------------------------------------------*/ 00041 /* Constant declarations */ 00042 /*---------------------------------------------------------------------------*/ 00043 /* HD constants */ 00044 #define FSM_HD_NONGREEDY 0 /* flag to indicate non-greedy computation at 00045 dead-ends */ 00046 #define FSM_HD_GREEDY 1 /* flag to indicate greedy computation at dead-ends */ 00047 #define FSM_HD_LARGE_SIZE 100000 /* size considered large for reached */ 00048 #define FSM_HD_MID_SIZE 50000 /* size considered medium for reached*/ 00049 #define FSM_HD_MINT_GROWTH 0.5 /* factor measuring minterm jump of reached*/ 00050 #define FSM_HD_GROWTH_RATE 0.04 /* Growth rate for reached in measuring slow 00051 * growth. */ 00052 #define FSM_MDD_DONT_FREE 0 /* flag to indicate that bdd should not be freed. */ 00053 #define FSM_MDD_FREE 1 /* flag to indicate that bdd should be freed.*/ 00054 #define FSM_HD_NUM_SLOW_GROWTHS 5 /* number of iterations of allowed 00055 * slow growth of reached. */ 00056 /*---------------------------------------------------------------------------*/ 00057 /* Structure declarations */ 00058 /*---------------------------------------------------------------------------*/ 00059 00062 /*---------------------------------------------------------------------------*/ 00063 /* Static function prototypes */ 00064 /*---------------------------------------------------------------------------*/ 00065 00066 static int CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t *domainVarMddIdArray, array_t *quantifyVarMddIdArray); 00067 static int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray); 00068 static mdd_t * AddStates(mdd_t *a, mdd_t *b, int freeA, int freeB); 00069 static void RandomSimulation(int simNVec, Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag, mdd_t *initialStates, mdd_t **reachableStates, mdd_t **fromLowerBound, FsmHdStruct_t *hdInfo); 00070 static void PrintStatsPerIteration(Fsm_RchType_t approxFlag, int nvars, int depth, FsmHdStruct_t *hdInfo, mdd_manager *mddManager, mdd_t *reachableStates, mdd_t *fromLowerBound, array_t *mintermVarArray); 00071 static void HdInduceFullDeadEndIfNecessary(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t **fromLowerBound, mdd_t **fromUpperBound, mdd_t **reachableStates, mdd_t **image, FsmHdStruct_t *hdInfo, int *depth, int shellFlag, array_t *onionRings, array_t *mintermVarArray, int oldSize, double oldMint, int verbosityLevel); 00072 static mdd_t * ComputeInitialStates(Fsm_Fsm_t *fsm, int shellFlag, boolean printWarning); 00073 static int CheckStatesContainedInInvariant(mdd_t *reachableStates, array_t *invarStates); 00074 static void HdComputeReachabilityParameters(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t **reachableStates, mdd_t **fromUpperBound, mdd_t **fromLowerBound, mdd_t **image, FsmHdStruct_t *hdInfo, mdd_t *initialStates, array_t *mintermVarArray, int *depth, int printStep, int shellFlag, array_t *onionRings, int verbosityLevel); 00075 static int InitializeIncrementalParameters(Fsm_Fsm_t *fsm, Ntk_Network_t *network, array_t **arrayOfRoots, st_table **tableOfLeaves); 00076 static mdd_t * IncrementalImageCompute(Ntk_Network_t *network, Fsm_Fsm_t *fsm, mdd_manager *mddManager, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet, array_t *arrayOfRoots, st_table *tableOfLeaves, array_t *smoothVarArray, array_t *relationArray, int numLatch); 00077 static void PrintOnionRings(Fsm_Fsm_t *fsm, int printStep, Fsm_RchType_t approxFlag, int nvars); 00078 static array_t * GenerateGuidedSearchSequenceArray(array_t *guideArray); 00079 static void ComputeReachabilityParameters(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, Fsm_RchType_t approxFlag, mdd_t **reachableStates, mdd_t **fromUpperBound, mdd_t **fromLowerBound, mdd_t **image, FsmHdStruct_t *hdInfo, mdd_t *initialStates, array_t *mintermVarArray, int *depth, int printStep, int shellFlag, array_t *onionRings, int verbosityLevel, boolean guidedSearchMode, mdd_t *hint, int *hintDepth, boolean *notConverged); 00080 00084 /*---------------------------------------------------------------------------*/ 00085 /* Definition of exported functions */ 00086 /*---------------------------------------------------------------------------*/ 00243 mdd_t * 00244 Fsm_FsmComputeReachableStates( 00245 Fsm_Fsm_t *fsm, 00246 int incrementalFlag, 00247 int verbosityLevel, 00248 int printStep, 00249 int depthValue, 00250 int shellFlag, 00251 int reorderFlag, 00252 int reorderThreshold, 00253 Fsm_RchType_t approxFlag, 00254 int ardc, 00255 int recompute, 00256 array_t *invarStates, 00257 boolean printWarning, 00258 array_t *guideArray) 00259 { 00260 /* BFS variables */ 00261 Img_ImageInfo_t *imageInfo = NIL(Img_ImageInfo_t); /* image info structure*/ 00262 Img_ImageInfo_t *oldImageInfo = NIL(Img_ImageInfo_t); 00263 mdd_t *reachableStates;/* reachable states */ 00264 mdd_t *unreachableStates; 00265 mdd_t *fromLowerBound; /* new states in each iteration */ 00266 mdd_t *fromUpperBound; /* set to reachable states */ 00267 mdd_t *image, *newImage;/* image computed at each iteration */ 00268 mdd_t *initialStates; /* initial states */ 00269 mdd_t *toCareSet; /* the complement of the reached set */ 00270 int depth = 0; /* depth upto which the computation is 00271 * performed. 00272 */ 00273 graph_t *partition, *oldPartition; 00274 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); /* mdd manager */ 00275 Ntk_Network_t *network = fsm->network; /* network */ 00276 bdd_reorder_type_t currentMethod = 00277 Ntk_NetworkReadDynamicVarOrderingMethod(network); /* current reordering 00278 * method */ 00279 int firstTimeFlag = TRUE, firstReorderFlag = FALSE; 00280 /* a flag to indicate the start of the computation */ 00281 Fsm_RchStatus_t rchStatus = Fsm_Rch_Under_c; 00282 /* under approximation of the reached set computed */ 00283 int reachableStateSetSize; /* bdd size of the reached set */ 00284 array_t *mintermVarArray; /* array of present state variables */ 00285 array_t *onionRings = NIL(array_t); 00286 /* onionringarray for shellFlag computation */ 00287 00288 /* Incremental flag variables */ 00289 array_t *arrayOfRoots = NIL(array_t); 00290 st_table *tableOfLeaves = NIL(st_table); 00291 int numLatch = 0; 00292 array_t *relationArray = NIL(array_t), *smoothVarArray = NIL(array_t); 00293 00294 boolean notConverged = FALSE; /* flag that says that the fixpoint procedure 00295 did not converge. */ 00296 /* HD variables */ 00297 FsmHdStruct_t *hdInfo = NULL; 00298 int nvars; /* number of present state variables */ 00299 00300 00301 /* Simulation variables */ 00302 int simNVec = 0; /* number of simulation vectors. */ 00303 char *simString = Cmd_FlagReadByName("rch_simulate"); 00304 00305 /* Guided Search */ 00306 array_t *hintDepthArray = NIL(array_t); 00307 int hintDepth = -1; 00308 mdd_t *hint = NIL(mdd_t); /* iterates over guide array */ 00309 int hintnr; /* idem */ 00310 boolean guidedSearchMode = FALSE; 00311 boolean guideArrayAllocated = FALSE; 00312 00313 boolean invariantFailed = FALSE; 00314 00315 /* initializations */ 00316 /* if fsm is a submachine, takes realPsVars to count minterm correctly. */ 00317 mintermVarArray = Fsm_FsmReadPresentStateVars(fsm); 00318 00319 /* compute number of present state variables */ 00320 nvars = ComputeNumberOfBinaryStateVariables(mddManager, mintermVarArray); 00321 assert(nvars > 0); 00322 00323 /* initializations */ 00324 if (recompute) { 00325 if (incrementalFlag && 00326 ((approxFlag == Fsm_Rch_Hd_c) || (approxFlag == Fsm_Rch_Oa_c))) { 00327 fprintf(vis_stdout, 00328 "** rch error: Incremental flag and HD computation are not compatible\n"); 00329 return NIL(mdd_t); 00330 } 00331 FsmResetReachabilityFields(fsm, approxFlag); 00332 } else if ((!shellFlag) || Fsm_FsmTestReachabilityOnionRingsUpToDate(fsm)) { 00333 /* If already computed and exact , just return a copy. */ 00334 reachableStates = Fsm_FsmReadReachableStates(fsm); 00335 if (reachableStates != NIL(mdd_t)){ 00336 if (printWarning) { 00337 fprintf(vis_stdout, "** rch info: Reachable states have been previously computed.\n"); 00338 fprintf(vis_stdout, "** rch info: Not recomputing reachable states.\n"); 00339 fprintf(vis_stdout, "** rch info: Use compute_reach -F to recompute if necessary.\n"); 00340 } 00341 if (!shellFlag) { 00342 if (printWarning) { 00343 if (FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Bfs_c) { 00344 fprintf(vis_stdout, "** rch info: All previous computations done using BFS (-A 0 option).\n"); 00345 } else { 00346 fprintf(vis_stdout, "** rch info: Some previous computations done using BFS/DFS mode (-A 1 or -g option).\n"); 00347 } 00348 } 00349 return (mdd_dup(reachableStates)); 00350 } else if (Fsm_FsmReadReachabilityOnionRings(fsm)) { 00351 /* if onion rings exist, since they are up-to-date, return the 00352 * reachable states 00353 */ 00354 if (printWarning) { 00355 if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Bfs_c) { 00356 fprintf(vis_stdout, "** rch info: Onion rings have been computed using BFS (-A 0 option)\n"); 00357 } else { 00358 fprintf(vis_stdout, "** rch info: Some onion rings have been computed using BFS/DFS (-A 1 or -g option)\n"); 00359 } 00360 } 00361 if (printStep) 00362 PrintOnionRings(fsm, printStep, approxFlag, nvars); 00363 return (mdd_dup(reachableStates)); 00364 } 00365 } 00366 00367 /* if some computed states exist and they violate an invariant, 00368 return the current set of reachable states */ 00369 reachableStates = Fsm_FsmReadCurrentReachableStates(fsm); 00370 if (reachableStates != NIL(mdd_t)) { 00371 if (!shellFlag) { 00372 /* if an underApprox exists, check invariant, if any */ 00373 if (invarStates != NIL(array_t)) { 00374 if (!CheckStatesContainedInInvariant(reachableStates, invarStates)) { 00375 if (printWarning) { 00376 fprintf(vis_stdout, "** rch info: Invariant violation using previously computed states\n"); 00377 } 00378 /* return violating reachable states */ 00379 return (mdd_dup(reachableStates)); 00380 } 00381 } 00382 } else if (Fsm_FsmReadReachabilityOnionRings(fsm)) { 00383 /* an invariant fails. */ 00384 if (invarStates != NIL(array_t)) { 00385 if (!CheckStatesContainedInInvariant(reachableStates, invarStates)) { 00386 if (printWarning) { 00387 fprintf(vis_stdout, "** rch info: Invariant violation using previously computed states\n"); 00388 if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Bfs_c) { 00389 fprintf(vis_stdout, "** rch info: Previous onion rings computed in BFS (-A 0 option).\n"); 00390 } else { 00391 fprintf(vis_stdout, "** rch info: Some set of onion rings have been computed using BFS/DFS (-A 1 or -g option)\n"); 00392 } 00393 fprintf(vis_stdout, "** rch info: Use compute_reach -F to recompute if necessary.\n"); 00394 } 00395 if (printStep) { 00396 PrintOnionRings(fsm, printStep, approxFlag, nvars); 00397 } 00398 return (mdd_dup(reachableStates)); 00399 } 00400 } 00401 } 00402 } 00403 /* if an over approx exists, check invariant, if any */ 00404 if ((invarStates != NIL(array_t)) && (!shellFlag) && (!depthValue) && 00405 (Fsm_FsmReadOverApproximateReachableStates(fsm) 00406 != NIL(array_t))) { 00407 if (FsmArdcCheckInvariant(fsm, invarStates)) { 00408 fprintf(vis_stdout, "** rch info: Over approximation exists, using over approximation for invariant checking.\n"); 00409 return(Fsm_ArdcGetMddOfOverApproximateReachableStates(fsm)); 00410 } 00411 } 00412 00413 if (incrementalFlag && 00414 ((approxFlag == Fsm_Rch_Hd_c) || (approxFlag == Fsm_Rch_Oa_c))) { 00415 fprintf(vis_stdout, 00416 "** rch error: Incremental flag and HD computation are not compatible\n"); 00417 00418 return NIL(mdd_t); 00419 } 00420 } 00421 /* onion rings make no sense with Over approx */ 00422 if (shellFlag && (approxFlag == Fsm_Rch_Oa_c)) { 00423 fprintf(vis_stdout, "** rch error: Can't generate onion rings with over approx\n"); 00424 return NIL(mdd_t); 00425 } 00426 00427 /* depth value makes no sense with over approximation */ 00428 if (depthValue && (approxFlag == Fsm_Rch_Oa_c)) { 00429 fprintf(vis_stdout, "** rch error: Can't generate over approx with depth Value\n"); 00430 return NIL(mdd_t); 00431 } 00432 00433 /* guided search cannot be done with Over approximation */ 00434 if ((guideArray != NIL(array_t)) && (approxFlag == Fsm_Rch_Oa_c)) { 00435 fprintf(vis_stdout, "Guided search is not implemented with Over approximations\n"); 00436 return NIL(mdd_t); 00437 } 00438 00439 /* initializations */ 00440 reachableStateSetSize = 0; 00441 if ((approxFlag == Fsm_Rch_Hd_c) || (guideArray != NIL(array_t))) { 00442 /* this structure is needed for HD and guidedSearch */ 00443 hdInfo = FsmHdStructAlloc(nvars); 00444 } 00445 00446 simNVec = 0; 00447 if (simString != NIL(char)) { 00448 simNVec = strtol(simString, NULL, 10); 00449 if (simNVec <= 0) simNVec = 0; 00450 } 00451 /* initialize onion ring array */ 00452 if (shellFlag) { 00453 if (Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t)) { 00454 onionRings = array_alloc(mdd_t *, 0); 00455 } else { 00456 onionRings = Fsm_FsmReadReachabilityOnionRings(fsm); 00457 } 00458 } 00459 00460 /* Computes ARDCs, and overapproximation by SSD traversal, if required. */ 00461 if (approxFlag == Fsm_Rch_Oa_c || ardc) { 00462 long initialTime = 0; 00463 long finalTime; 00464 00465 assert(!incrementalFlag); 00466 00467 if (verbosityLevel > 0) 00468 initialTime = util_cpu_time(); 00469 00470 (void)Fsm_FsmComputeOverApproximateReachableStates(fsm, incrementalFlag, 00471 verbosityLevel, printStep, depthValue, shellFlag, reorderFlag, 00472 reorderThreshold, recompute); 00473 00474 if (approxFlag == Fsm_Rch_Oa_c) { 00475 if (hdInfo != NIL(FsmHdStruct_t)) FsmHdStructFree(hdInfo); 00476 return(Fsm_ArdcGetMddOfOverApproximateReachableStates(fsm)); 00477 } 00478 00479 if (verbosityLevel > 0) { 00480 finalTime = util_cpu_time(); 00481 Fsm_ArdcPrintReachabilityResults(fsm, finalTime-initialTime); 00482 } 00483 } 00484 00485 if(Cmd_FlagReadByName("linear_compute_range")) { 00486 partition = Part_NetworkCreatePartition(network, 0, "temp", (lsList)0, 00487 (lsList)0, NIL(mdd_t), Part_Fine_c, 0, 0, 0, 0); 00488 oldPartition = fsm->partition; 00489 oldImageInfo = fsm->imageInfo; 00490 fsm->imageInfo = 0; 00491 imageInfo = Fsm_FsmReadOrCreateImageInfoForComputingRange(fsm, 0, 1); 00492 unreachableStates = Img_ImageGetUnreachableStates(imageInfo); 00493 fprintf(vis_stdout, "%-20s%10g\n", "reachable states =", 00494 mdd_count_onset(mddManager, unreachableStates, 00495 fsm->fsmData.presentStateVars)); 00496 fflush(vis_stdout); 00497 /* get unreachable states */ 00498 Img_ImageInfoFree(imageInfo); 00499 fsm->imageInfo = oldImageInfo; 00500 fsm->partition = oldPartition; 00501 Part_PartitionFree(partition); 00502 exit(0); 00503 } 00504 /* Compute the set of initial states. Start with the 00505 * underapproximation of Reached states if it exists or sum of 00506 * onion rings if shell flag is specified or the initial states of 00507 * the fsm. 00508 */ 00509 initialStates = ComputeInitialStates(fsm, shellFlag, printWarning); 00510 if (initialStates == NIL(mdd_t)) { 00511 fprintf(vis_stdout, "** rch error: No initial states computed."); 00512 fprintf(vis_stdout, " No reachability will be performed.\n"); 00513 if (hdInfo != NIL(FsmHdStruct_t)) FsmHdStructFree(hdInfo); 00514 return NIL(mdd_t); 00515 } 00516 00517 if (incrementalFlag){ 00518 /* Note: if incrementalflag is set, no imageinfo is created! */ 00519 numLatch = InitializeIncrementalParameters(fsm, network, &arrayOfRoots, 00520 &tableOfLeaves); 00521 smoothVarArray = array_join(fsm->fsmData.presentStateVars, 00522 fsm->fsmData.inputVars); 00523 relationArray = array_alloc(mdd_t *, numLatch+1); 00524 } else { 00525 /* Create an imageInfo for image computations, if not already created. */ 00526 imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, 0, 1); 00527 if (ardc) { 00528 Fsm_ArdcMinimizeTransitionRelation(fsm, Img_Forward_c); 00529 } 00530 } 00531 00532 /* Get approximate traversal options */ 00533 if ((!incrementalFlag) && (approxFlag == Fsm_Rch_Hd_c)) { 00534 /* only partial image allowed. No approximation of frontier set */ 00535 hdInfo->onlyPartialImage = Fsm_FsmHdOptionReadOnlyPartialImage(hdInfo->options); 00536 /* states which can produce no new successors. */ 00537 hdInfo->interiorStates = bdd_zero(mddManager); 00538 } 00539 00540 /* pertaining to simulation */ 00541 if (simNVec > 0) { 00542 RandomSimulation(simNVec, fsm, approxFlag, initialStates, 00543 &reachableStates, &fromLowerBound, hdInfo); 00544 } else { 00545 /* start reached set with initial states */ 00546 reachableStates = mdd_dup(initialStates); 00547 fromLowerBound = mdd_dup(reachableStates); 00548 } 00549 00550 /* initialize variables to print */ 00551 if ((!incrementalFlag) && (approxFlag == Fsm_Rch_Hd_c)) { 00552 00553 FsmHdStatsComputeSizeAndMinterms(mddManager, reachableStates, 00554 mintermVarArray, nvars, 00555 Fsm_Hd_Reached, hdInfo->stats); 00556 FsmHdStatsComputeSizeAndMinterms(mddManager, fromLowerBound, 00557 mintermVarArray, nvars, 00558 Fsm_Hd_From, hdInfo->stats); 00559 FsmHdStatsSetMintermFromSubset(hdInfo->stats, FsmHdStatsReadMintermFrom(hdInfo->stats)); 00560 FsmHdStatsSetSizeFromSubset(hdInfo->stats, FsmHdStatsReadSizeFrom(hdInfo->stats)); 00561 } 00562 00563 if (printStep && ((depth % printStep) == 0) && (approxFlag == Fsm_Rch_Hd_c)){ 00564 fprintf(vis_stdout, "\nIndex: R = Reached; I = Image, F = Frontier, FA = Approximation of Frontier\n"); 00565 fprintf(vis_stdout, " f = Minterms in f; |f| = Bdd nodes in f\n\n"); 00566 } 00567 /* initialize for the first iteration */ 00568 fromUpperBound = reachableStates; 00569 00570 /* hint array */ 00571 if (guideArray == NIL(array_t)) { 00572 guideArray = array_alloc(mdd_t *, 0); 00573 guideArrayAllocated = TRUE; 00574 } 00575 /* pad with 1 when no hints are provided */ 00576 if (array_n(guideArray) == 0) { 00577 array_insert_last(mdd_t *, guideArray, bdd_one(mddManager)); 00578 } 00579 /* depth sequence for hints. 1-to-1 correspondence with guidearray */ 00580 /* -1 implies apply hint to convergence. */ 00581 hintDepthArray = GenerateGuidedSearchSequenceArray(guideArray); 00582 00583 assert(array_n(hintDepthArray) == array_n(guideArray)); 00584 00585 if (array_n(guideArray) == 0) hint = mdd_one(mddManager); 00586 00587 arrayForEachItem(mdd_t *, guideArray, hintnr, hint){ 00588 00589 /* check the depth for which this hint is to be applied. */ 00590 hintDepth = array_fetch(int, hintDepthArray, hintnr); 00591 00592 if(hintnr == 0 && mdd_is_tautology(hint, 1) && array_n(guideArray) == 1){ 00593 assert(hintDepth == -1); 00594 } else { 00595 assert(!incrementalFlag); 00596 guidedSearchMode = TRUE; 00597 Fsm_InstantiateHint(fsm, hint, 1, 0, Ctlp_Underapprox_c, 00598 verbosityLevel > 1); 00599 if (hintnr < (array_n(guideArray)-1)) 00600 fprintf(vis_stdout, "**GS info: Instantiating hint number %d\n", hintnr+1); 00601 else 00602 fprintf(vis_stdout, "**GS info: Restoring original transition relation\n"); 00603 00604 if (approxFlag == Fsm_Rch_Hd_c) { 00605 /* clean up all the invalid state information */ 00606 if (hdInfo->interiorStates != NIL(mdd_t)) 00607 mdd_free(hdInfo->interiorStates); 00608 hdInfo->interiorStates = NIL(mdd_t); /* for every new hint, this is invalid. */ 00609 if (hdInfo->interiorStateCandidate != NIL(mdd_t)) 00610 mdd_free(hdInfo->interiorStateCandidate); 00611 hdInfo->interiorStateCandidate = NIL(mdd_t); /* for every new hint, this is invalid */ 00612 hdInfo->imageOfReachedComputed = FALSE; /* since it doesn't matter for every new hint */ 00613 if (hdInfo->deadEndResidue != NIL(mdd_t)) 00614 mdd_free(hdInfo->deadEndResidue); 00615 hdInfo->deadEndResidue = NIL(mdd_t); 00616 } 00617 /* generate a frontier by doing a dead-end computation if the 00618 frontier is empty. This is non-greedy for BFS and greedy for 00619 HD. */ 00620 if (mdd_is_tautology(fromLowerBound, 0)) { 00621 ComputeReachabilityParameters(mddManager, imageInfo, approxFlag, 00622 &reachableStates, &fromUpperBound, 00623 &fromLowerBound, &image, hdInfo, 00624 initialStates, 00625 mintermVarArray, 00626 &depth, printStep, 00627 shellFlag, onionRings, 00628 verbosityLevel, 00629 guidedSearchMode, hint, &hintDepth, 00630 ¬Converged); 00631 } 00632 } 00633 /* initialize */ 00634 notConverged = FALSE; 00635 if (!incrementalFlag) 00636 Img_ImageInfoResetUseOptimizedRelationFlag(imageInfo); 00637 /* Main loop of reachability computation. */ 00638 /* Iterate until fromLowerBound is empty or all states are reached. */ 00639 while (!mdd_is_tautology(fromLowerBound, 0)) { 00640 if(depth > 0 && !incrementalFlag) 00641 Img_ImageInfoSetUseOptimizedRelationFlag(imageInfo); 00642 /* fromLowerBound is the "onion shell" of states just reached. */ 00643 if ((shellFlag && (approxFlag != Fsm_Rch_Hd_c) && 00644 (!firstTimeFlag || 00645 (Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t)))) || 00646 (shellFlag && (approxFlag == Fsm_Rch_Hd_c) && 00647 (Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t)) && 00648 firstTimeFlag)) { 00649 array_insert_last(mdd_t*, onionRings, mdd_dup(fromLowerBound)); 00650 } 00651 00652 /* if it is the print step, print out the iteration and the */ 00653 if (printStep && ((depth % printStep) == 0)) { 00654 int step; 00655 /* for BFS, preserve earlier format of printing */ 00656 step = (shellFlag) ? array_n(onionRings) : Fsm_FsmGetReachableDepth(fsm)+depth; 00657 PrintStatsPerIteration(approxFlag, 00658 nvars, 00659 step, 00660 hdInfo, 00661 mddManager, 00662 reachableStates, 00663 fromLowerBound, 00664 mintermVarArray); 00665 } 00666 00667 /* Check if invariant contains the new states. In case of HD 00668 * computation, check the containment of the entire reached set. 00669 */ 00670 if (invarStates != NIL(array_t)) { 00671 mdd_t *temp; 00672 temp = (approxFlag == Fsm_Rch_Hd_c) ? reachableStates : fromLowerBound; 00673 if (!CheckStatesContainedInInvariant(temp, invarStates)) { 00674 notConverged = TRUE; 00675 invariantFailed = TRUE; /* flag used for early termination */ 00676 break; 00677 } 00678 } 00679 00680 if (mdd_is_tautology(reachableStates, 1)) { 00681 break; 00682 } 00683 00684 if ((depthValue && (depth == depthValue)) || 00685 /* limited depth hint is implemented this way */ 00686 (hintDepth == 0)) { 00687 /* No more steps */ 00688 notConverged = TRUE; 00689 break; 00690 } 00691 00692 if (reorderFlag && !firstReorderFlag && 00693 (reachableStateSetSize >= reorderThreshold )){ 00694 firstReorderFlag = TRUE; 00695 (void) fprintf(vis_stdout, "Dynamic variable ordering forced "); 00696 (void) fprintf(vis_stdout, "with method sift\n"); 00697 Ntk_NetworkSetDynamicVarOrderingMethod(network, 00698 BDD_REORDER_SIFT, 00699 BDD_REORDER_VERBOSITY_DEFAULT); 00700 bdd_reorder(Ntk_NetworkReadMddManager(network)); 00701 Ntk_NetworkSetDynamicVarOrderingMethod(network, currentMethod, 00702 BDD_REORDER_VERBOSITY_DEFAULT); 00703 } 00704 00705 firstTimeFlag = FALSE; 00706 /* careSet for image computation is the set of all states not reached 00707 * so far. 00708 */ 00709 toCareSet = mdd_not(reachableStates); 00710 00711 /* 00712 * Image of some set between lower and upper, where we care 00713 * about the image only on unreached states. 00714 */ 00715 if (incrementalFlag){ 00716 image = IncrementalImageCompute(network, fsm, mddManager, 00717 fromLowerBound, 00718 fromUpperBound, toCareSet, 00719 arrayOfRoots, tableOfLeaves, 00720 smoothVarArray, relationArray, 00721 numLatch); 00722 } else{ 00723 assert(!incrementalFlag); 00724 00725 if (approxFlag == Fsm_Rch_Hd_c) { 00726 /* allow partial image computation */ 00727 Img_ImageAllowPartialImage(imageInfo, TRUE); 00728 } 00729 00730 /* compute the image of this iteration */ 00731 image = Img_ImageInfoComputeFwdWithDomainVars(imageInfo, 00732 fromLowerBound, 00733 fromUpperBound, 00734 toCareSet); 00735 00736 00737 00738 /* record if partial image or not */ 00739 if (approxFlag == Fsm_Rch_Hd_c) { 00740 /* Check if partial image computation, disallow partial image 00741 * computation. 00742 */ 00743 hdInfo->partialImage = Img_ImageWasPartial(imageInfo); 00744 /* record this to prevent dead-end computation. */ 00745 hdInfo->imageOfReachedComputed = (!hdInfo->partialImage) && 00746 mdd_equal(reachableStates, fromLowerBound); 00747 /* potential candidates for interior states (only if not a 00748 * partial image) 00749 */ 00750 if (!hdInfo->partialImage) hdInfo->interiorStateCandidate = mdd_dup(fromLowerBound); 00751 } 00752 } 00753 00754 /* free the used bdds */ 00755 mdd_free(toCareSet); 00756 00757 /* New lower bound is the states just reached. */ 00758 mdd_free(fromLowerBound); 00759 fromLowerBound = mdd_and(image, reachableStates, 1, 0); 00760 depth++; 00761 hintDepth--; 00762 00763 00764 if ((!incrementalFlag) && (approxFlag == Fsm_Rch_Hd_c)) { 00765 FsmHdStatsComputeSizeAndMinterms(mddManager, image, 00766 mintermVarArray, nvars, 00767 Fsm_Hd_To, hdInfo->stats); 00768 } 00769 00770 /* need image only if HD and not dead-end */ 00771 if (approxFlag != Fsm_Rch_Hd_c) { 00772 mdd_free(image); 00773 image = NULL; 00774 } else { 00775 if (hdInfo->imageOfReachedComputed || hdInfo->onlyPartialImage || 00776 (hdInfo->slowGrowth >= FSM_HD_NUM_SLOW_GROWTHS) || 00777 mdd_is_tautology(fromLowerBound, 0)) { 00778 mdd_free(image); 00779 image = NULL; 00780 } 00781 } 00782 00783 /* computes reachable states, fromlowerBound and fromupperbound 00784 * for BFS. For HD it computes the above as well as interior 00785 * statess, dead-end residue, etc. All the other parameteres are 00786 * updated. For guided search, this call does not perform a 00787 * non-greedy dead-end computation, even if the frontier is 0. */ 00788 ComputeReachabilityParameters(mddManager, imageInfo, approxFlag, 00789 &reachableStates, 00790 &fromUpperBound, 00791 &fromLowerBound, 00792 &image, 00793 hdInfo, 00794 initialStates, 00795 mintermVarArray, 00796 &depth, printStep, 00797 shellFlag, onionRings, 00798 verbosityLevel, FALSE, hint, 00799 &hintDepth, 00800 ¬Converged); 00801 00802 00803 if (mdd_is_tautology(fromLowerBound, 0) && 00804 (approxFlag == Fsm_Rch_Bfs_c) && 00805 (!guidedSearchMode) && (!depthValue)) 00806 depth--; 00807 00808 } /* end of main while loop (while frontier != 0) */ 00809 00810 /* stop iterating over hint if invariants are violated or all 00811 states are reachable or limited depth value has been 00812 reached. */ 00813 if (invariantFailed) break; 00814 if (mdd_is_tautology(reachableStates, 1)) { 00815 break; 00816 } 00817 if (depthValue && (depth == depthValue)) { 00818 /* No more steps */ 00819 break; 00820 } 00821 00822 }/* for each hint */ 00823 00824 00825 if(!incrementalFlag && 00826 Img_ImageInfoObtainMethodType(imageInfo) == Img_Linear_c && 00827 Img_ImageInfoObtainOptimizeType(imageInfo) == Opt_NS && 00828 Img_IsTransitionRelationOptimized(imageInfo)) { 00829 Img_ImageInfoResetUseOptimizedRelationFlag(imageInfo); 00830 fprintf(vis_stdout, "%-20s%10g\n", "reachable states =", 00831 mdd_count_onset(mddManager, reachableStates, 00832 fsm->fsmData.presentStateVars)); 00833 fromLowerBound = mdd_dup(reachableStates); 00834 fromUpperBound = reachableStates; 00835 while (1) { 00836 toCareSet = mdd_dup(reachableStates); 00837 image = Img_ImageInfoComputeFwdWithDomainVars(imageInfo, 00838 fromLowerBound, 00839 fromUpperBound, 00840 toCareSet); 00841 newImage = bdd_or(image, initialStates, 1, 1); 00842 bdd_free(image); 00843 image = newImage; 00844 if(mdd_equal(fromLowerBound, image)) { 00845 mdd_free(toCareSet); 00846 mdd_free(fromLowerBound); 00847 mdd_free(reachableStates); 00848 fromLowerBound = image; 00849 reachableStates = mdd_dup(fromLowerBound); 00850 fromUpperBound = reachableStates; 00851 fprintf(vis_stdout, "%-20s%10g\n", "reachable states =", 00852 mdd_count_onset(mddManager, reachableStates, 00853 fsm->fsmData.presentStateVars)); 00854 break; 00855 } 00856 mdd_free(toCareSet); 00857 mdd_free(fromLowerBound); 00858 mdd_free(reachableStates); 00859 fromLowerBound = image; 00860 reachableStates = mdd_dup(fromLowerBound); 00861 fromUpperBound = reachableStates; 00862 00863 fprintf(vis_stdout, "%-20s%10g\n", "reachable states =", 00864 mdd_count_onset(mddManager, reachableStates, 00865 fsm->fsmData.presentStateVars)); 00866 } 00867 } 00868 00869 00870 /* clean up for Guided search mainly, only if needed */ 00871 /* we rely on the fact that the variable hint is set to the last hint from 00872 * the previous loop. 00873 */ 00874 if (guidedSearchMode && !mdd_is_tautology(hint, 1)) 00875 Fsm_CleanUpHints(fsm, 1, 0, printStep); 00876 array_free(hintDepthArray); 00877 00878 /* If (1) all states are reachable, or (2) not limited depth computation 00879 and not a converge with a hint, or (3) limited depth and not 00880 guided search mode and BFS and frontier = 0, or (4) in guided 00881 search, if limited depth and frontier = 0 then one full dead-end 00882 should have occured */ 00883 if(mdd_is_tautology(reachableStates, 1) || 00884 ((notConverged == FALSE) && mdd_is_tautology(hint, 1)) || 00885 (!guidedSearchMode && (notConverged == TRUE) && 00886 mdd_is_tautology(fromLowerBound, 0) && (approxFlag == Fsm_Rch_Bfs_c)) || 00887 (guidedSearchMode && hdInfo->deadEndWithOriginalTR && 00888 mdd_is_tautology(fromLowerBound, 0) && (approxFlag == Fsm_Rch_Bfs_c))) { 00889 00890 rchStatus = Fsm_Rch_Exact_c; 00891 if (mdd_is_tautology(reachableStates, 1) && 00892 !mdd_is_tautology(fromLowerBound, 0) && 00893 printStep && ((depth % printStep) == 0) ) { 00894 int step; 00895 /* for BFS, preserve earlier format of printing */ 00896 step = (shellFlag) ? 00897 array_n(onionRings) : 00898 Fsm_FsmGetReachableDepth(fsm)+depth; 00899 PrintStatsPerIteration(approxFlag, nvars, step, hdInfo, 00900 mddManager, reachableStates, 00901 fromLowerBound, mintermVarArray); 00902 } 00903 } 00904 00905 /* clean up the hints if allocated here */ 00906 if (guideArrayAllocated) mdd_array_free(guideArray); 00907 00908 if (hdInfo != NIL(FsmHdStruct_t)) { 00909 FsmHdStructFree(hdInfo); 00910 } 00911 00912 mdd_free(fromLowerBound); 00913 mdd_free(initialStates); 00914 00915 /* Update FSM reahcability fields */ 00916 00917 /* indicate whether the shells are consistent with the reachable states */ 00918 if (!shellFlag) { 00919 /* if any states were added from a previous computation, shells 00920 are not up-to-date */ 00921 if (Fsm_FsmReadCurrentReachableStates(fsm) != NIL(mdd_t)) { 00922 if (!mdd_lequal(reachableStates, Fsm_FsmReadCurrentReachableStates(fsm), 1, 1)) { 00923 FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE); 00924 } /* otherwise the previous iteration was computed with onion 00925 rings, in which case it is still up-to-date or the previous 00926 iteration was computed without onion rings and it was set to not 00927 up-to-date in the previous iteration */ 00928 } else { 00929 assert(Fsm_FsmReadReachabilityOnionRings(fsm) == NIL(array_t)); 00930 /* not up-to-date because no onion rings */ 00931 FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE); 00932 } 00933 00934 } else { 00935 /* shells are up to date only if current set adds upto previously 00936 computed states or more */ 00937 if (Fsm_FsmReadCurrentReachableStates(fsm)) { 00938 if (!mdd_lequal(Fsm_FsmReadCurrentReachableStates(fsm), 00939 reachableStates, 1, 1)) { 00940 FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE); 00941 } else { 00942 FsmSetReachabilityOnionRingsUpToDateFlag(fsm, TRUE); 00943 } 00944 00945 } else FsmSetReachabilityOnionRingsUpToDateFlag(fsm, TRUE); 00946 00947 /* Onion rings are not BFS, i.e., HD or Guided search. */ 00948 if ((approxFlag == Fsm_Rch_Hd_c) || 00949 (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Hd_c) || 00950 guidedSearchMode) 00951 FsmSetReachabilityOnionRingsMode(fsm, Fsm_Rch_Hd_c); 00952 00953 if (array_n(onionRings) == 0) { 00954 array_free(onionRings); 00955 onionRings = NIL(array_t); 00956 } 00957 FsmSetReachabilityOnionRings(fsm, onionRings); 00958 } 00959 00960 /* update fsm structure */ 00961 /* record depth of traversal, depth is consistent with reachable 00962 states, hence may not be consistent with the onion rings */ 00963 /* replace reachable states if only more states have been computed now */ 00964 if (Fsm_FsmReadCurrentReachableStates(fsm) != NIL(mdd_t)) { 00965 if (!mdd_lequal(reachableStates, Fsm_FsmReadCurrentReachableStates(fsm), 1, 1)) { 00966 Fsm_FsmFreeReachableStates(fsm); 00967 fsm->reachabilityInfo.reachableStates = mdd_dup(reachableStates); 00968 if (!shellFlag) fsm->reachabilityInfo.depth = Fsm_FsmGetReachableDepth(fsm) + depth; 00969 else if (Fsm_FsmReadReachabilityOnionRings(fsm)) 00970 fsm->reachabilityInfo.depth = array_n(Fsm_FsmReadReachabilityOnionRings(fsm)); 00971 /* set computation mode as HD if HD or Guided search, basically to indicate not BFS */ 00972 if ((approxFlag == Fsm_Rch_Hd_c) || 00973 (FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Hd_c) || 00974 guidedSearchMode) { 00975 FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Hd_c); 00976 } 00977 } 00978 } else { 00979 fsm->reachabilityInfo.reachableStates = mdd_dup(reachableStates); 00980 if (!shellFlag) fsm->reachabilityInfo.depth = depth; 00981 else if (Fsm_FsmReadReachabilityOnionRings(fsm)) 00982 fsm->reachabilityInfo.depth = array_n(Fsm_FsmReadReachabilityOnionRings(fsm)); 00983 /* set computation mode as HD if HD or Guided search, basically to indicate not BFS */ 00984 if ((approxFlag == Fsm_Rch_Hd_c) || guidedSearchMode) { 00985 FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Hd_c); 00986 } else { 00987 FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Bfs_c); 00988 } 00989 00990 } 00991 /* indicate whether reachability analysis is completed or not */ 00992 FsmSetReachabilityApproxComputationStatus(fsm, rchStatus); 00993 00994 if (incrementalFlag){ 00995 array_free(relationArray); 00996 array_free(arrayOfRoots); 00997 st_free_table(tableOfLeaves); 00998 array_free(smoothVarArray); 00999 /* Need to put in next state function data for the partition */ 01000 } 01001 01002 return reachableStates; 01003 } /* end of Fsm_FsmComputeReachableStates */ 01004 01005 01006 01019 mdd_t * 01020 Fsm_MddMultiwayAndSmooth(mdd_manager *mddManager, array_t *mddArray, 01021 array_t *smoothingVars) 01022 { 01023 int i; 01024 mdd_t *resultMdd; 01025 mdd_t *product = mdd_one(mddManager); 01026 01027 for (i = 0; i<array_n(mddArray); i++){ 01028 mdd_t *mdd = array_fetch(mdd_t*, mddArray, i); 01029 mdd_t *tempProduct = mdd_and(product, mdd, 1, 1); 01030 mdd_free(product); 01031 product = tempProduct; 01032 } 01033 01034 if (array_n(smoothingVars) == 0) { 01035 resultMdd = mdd_dup(product); 01036 } 01037 else{ 01038 resultMdd = mdd_smooth(mddManager, product, smoothingVars); 01039 } 01040 01041 mdd_free(product); 01042 return resultMdd; 01043 } 01044 01056 void 01057 Fsm_FsmReachabilityPrintResults( 01058 Fsm_Fsm_t *fsm, 01059 long elapseTime, 01060 int approxFlag) 01061 { 01062 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 01063 mdd_t *reachableStates = fsm->reachabilityInfo.reachableStates; 01064 array_t *psVarsArray; 01065 int nvars; 01066 01067 if (!reachableStates) 01068 return; 01069 01070 psVarsArray = Fsm_FsmReadPresentStateVars(fsm); 01071 /* compute number of present state variables */ 01072 nvars = ComputeNumberOfBinaryStateVariables(mddManager, psVarsArray); 01073 01074 (void) fprintf(vis_stdout,"********************************\n"); 01075 (void) fprintf(vis_stdout,"Reachability analysis results:\n"); 01076 if ((FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Bfs_c) && 01077 (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t))) { 01078 (void) fprintf(vis_stdout, "%-20s%10d\n", "FSM depth =", 01079 fsm->reachabilityInfo.depth); 01080 } else { 01081 (void) fprintf(vis_stdout, "%-20s%10d\n", "computation depth =", 01082 fsm->reachabilityInfo.depth); 01083 } 01084 if (nvars <= 1023) { 01085 (void) fprintf(vis_stdout, "%-20s%10g\n", "reachable states =", 01086 mdd_count_onset(mddManager, reachableStates, 01087 fsm->fsmData.presentStateVars)); 01088 } else { 01089 /* 01090 (void) fprintf(vis_stdout, "%-20s", "reachable states = "); 01091 bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6); 01092 */ 01093 EpDouble epd; 01094 char strValue[20]; 01095 01096 mdd_epd_count_onset(mddManager, reachableStates, 01097 fsm->fsmData.presentStateVars, &epd); 01098 EpdGetString(&epd, strValue); 01099 (void) fprintf(vis_stdout, "%-20s%10s\n", "reachable states =", strValue); 01100 } 01101 (void) fprintf(vis_stdout, "%-20s%10d\n", "BDD size =", 01102 mdd_size(reachableStates)); 01103 (void) fprintf(vis_stdout, "%-20s%10g\n", "analysis time =", 01104 (double)elapseTime/1000.0); 01105 if (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t)) { 01106 (void) fprintf(vis_stdout, "%-20s%10s\n", "reachability analysis = ", "complete"); 01107 } else { 01108 (void) fprintf(vis_stdout, "%-20s%10s\n", "reachability analysis = ", "incomplete"); 01109 } 01110 } 01111 01112 01113 /*---------------------------------------------------------------------------*/ 01114 /* Definition of static functions */ 01115 /*---------------------------------------------------------------------------*/ 01116 01128 static int 01129 CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t 01130 *domainVarMddIdArray, array_t *quantifyVarMddIdArray) 01131 { 01132 int i; 01133 array_t *imageSupportArray = mdd_get_support(mddManager, image); 01134 st_table *imageSupportTable = st_init_table(st_numcmp, st_numhash); 01135 for (i=0; i<array_n(imageSupportArray); i++){ 01136 int mddId = array_fetch(int, imageSupportArray, i); 01137 (void) st_insert(imageSupportTable, (char *) (long) mddId, NIL(char)); 01138 } 01139 for (i=0; i<array_n(domainVarMddIdArray); i++){ 01140 int domainVarId; 01141 domainVarId = array_fetch(int, domainVarMddIdArray, i); 01142 assert(st_is_member(imageSupportTable, (char *)(long)domainVarId) == 0); 01143 } 01144 for (i=0; i<array_n(quantifyVarMddIdArray); i++){ 01145 int quantifyVarId; 01146 quantifyVarId = array_fetch(int, quantifyVarMddIdArray, i); 01147 assert(st_is_member(imageSupportTable, (char *)(long)quantifyVarId) == 0); 01148 } 01149 st_free_table(imageSupportTable); 01150 array_free(imageSupportArray); 01151 return 1; 01152 } 01153 01164 static int 01165 ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, 01166 array_t *mddIdArray) 01167 { 01168 int mddId, i; 01169 mvar_type mddVar; 01170 int numEncodingBits, count = 0; 01171 array_t *mvar_list = mdd_ret_mvar_list(mddManager); 01172 01173 arrayForEachItem(int, mddIdArray, i, mddId) { 01174 mddVar = array_fetch(mvar_type, mvar_list, mddId); 01175 numEncodingBits = mddVar.encode_length; 01176 count += numEncodingBits; 01177 } 01178 return count; 01179 } /* end of ComputeNumberOfBinaryStateVariables */ 01180 01181 01191 static mdd_t * 01192 AddStates(mdd_t *a, mdd_t *b, int freeA, int freeB) 01193 { 01194 mdd_t *result; 01195 if ((a != NULL) && (b != NULL)) { 01196 result = mdd_or(a, b, 1, 1); 01197 } else if ((a == NULL) && (b == NULL)) { 01198 result = a; 01199 } else if (a == NULL) { 01200 result = mdd_dup(b); 01201 } else { 01202 result = mdd_dup(a); 01203 } 01204 if ((freeA == FSM_MDD_FREE) && (a != NULL)) mdd_free(a); 01205 if ((freeB == FSM_MDD_FREE) && (b != NULL)) mdd_free(b); 01206 return result; 01207 } /* end of AddStates */ 01208 01209 01219 static void 01220 RandomSimulation(int simNVec, 01221 Fsm_Fsm_t *fsm, 01222 Fsm_RchType_t approxFlag, 01223 mdd_t *initialStates, 01224 mdd_t **reachableStates, 01225 mdd_t **fromLowerBound, 01226 FsmHdStruct_t *hdInfo) 01227 { 01228 Ntk_Network_t *network = fsm->network; 01229 01230 /* Compute specified number of simulated states. */ 01231 *reachableStates = Sim_RandomSimulate(network, simNVec, 0); 01232 *reachableStates = AddStates(*reachableStates, initialStates, FSM_MDD_FREE, FSM_MDD_DONT_FREE); 01233 *fromLowerBound = mdd_dup(*reachableStates); 01234 01235 if (approxFlag == Fsm_Rch_Hd_c) { 01236 if (mdd_size(*fromLowerBound) > 01237 Fsm_FsmHdOptionReadFrontierApproxThreshold(hdInfo->options)) { 01238 /* Reset frontier if too large. */ 01239 mdd_free(*fromLowerBound); 01240 *fromLowerBound = bdd_between(initialStates, *reachableStates); 01241 if (!mdd_equal(*fromLowerBound, *reachableStates)) { 01242 hdInfo->firstSubset = FALSE; 01243 hdInfo->deadEndResidue = mdd_and(*reachableStates, 01244 *fromLowerBound, 1, 0); 01245 } 01246 } 01247 } 01248 return; 01249 } /* end of RandomSimulation */ 01250 01251 01261 static void 01262 PrintStatsPerIteration(Fsm_RchType_t approxFlag, 01263 int nvars, 01264 int depth, 01265 FsmHdStruct_t *hdInfo, 01266 mdd_manager *mddManager, 01267 mdd_t *reachableStates, 01268 mdd_t *fromLowerBound, 01269 array_t *mintermVarArray) 01270 { 01271 if (approxFlag != Fsm_Rch_Hd_c) { 01272 int reachableStateSetSize = mdd_size(reachableStates); 01273 if (nvars <= 1023) { 01274 (void)fprintf(vis_stdout, "BFS step = %d\t|states| = %8g\tBdd size = %8ld\n", 01275 depth, mdd_count_onset(mddManager, reachableStates, 01276 mintermVarArray), 01277 (long)reachableStateSetSize); 01278 /* bdd_print_minterm(reachableStates); */ 01279 } else { 01280 (void)fprintf(vis_stdout, "BFS step = %d\tBdd size = %8d\t|states| = ", 01281 depth, reachableStateSetSize); 01282 (void) bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6); 01283 } 01284 01285 } else { /* HD */ 01286 01287 if (nvars <= 1023) { 01288 (void)fprintf(vis_stdout, "Step = %d, R = %8g, |R| = %8d, I = %8g, |I| = %8d\n", 01289 depth, FsmHdStatsReadMintermReached(hdInfo->stats), 01290 FsmHdStatsReadSizeReached(hdInfo->stats), FsmHdStatsReadMintermTo(hdInfo->stats) , 01291 FsmHdStatsReadSizeTo(hdInfo->stats)); 01292 (void)fprintf(vis_stdout, "Completed iteration %d at %g seconds\n", 01293 depth, (util_cpu_time()/1000.0)); 01294 01295 (void)fprintf(vis_stdout, "Step = %d, F = %8g, |F| = %8d, FA = %8g, |FA| = %8d\n", 01296 depth+1, FsmHdStatsReadMintermFrom(hdInfo->stats), 01297 FsmHdStatsReadSizeFrom(hdInfo->stats), 01298 FsmHdStatsReadMintermFromSubset(hdInfo->stats), 01299 FsmHdStatsReadSizeFromSubset(hdInfo->stats)); 01300 } else { 01301 int status; 01302 (void)fprintf(vis_stdout, "Step = %d, |R| = %8d, R = ", 01303 depth, FsmHdStatsReadSizeReached(hdInfo->stats)); 01304 status = bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6); 01305 if (!status) { 01306 error_append("** rch error: Error in printing arbitrary precision minterm count of Reached"); 01307 } 01308 01309 (void)fprintf(vis_stdout, "Completed iteration %d at %g seconds\n", 01310 depth, (util_cpu_time()/1000.0)); 01311 (void)fprintf(vis_stdout, "Step = %d, |F| = %8d, F = %8g, |FA| = %8d, FA = ", 01312 depth, FsmHdStatsReadSizeFrom(hdInfo->stats), 0.0, 01313 FsmHdStatsReadSizeFromSubset(hdInfo->stats) ); 01314 status = bdd_print_apa_minterm(vis_stdout, fromLowerBound, nvars, 6); 01315 if (!status) { 01316 error_append("** rch error: Error in printing arbitrary precision minterm count of From"); 01317 } 01318 } 01319 } 01320 return; 01321 } /* end of PrintStatsPerIteration */ 01322 01338 static void 01339 HdInduceFullDeadEndIfNecessary(mdd_manager *mddManager, 01340 Img_ImageInfo_t *imageInfo, 01341 mdd_t **fromLowerBound, 01342 mdd_t **fromUpperBound, 01343 mdd_t **reachableStates, 01344 mdd_t **image, 01345 FsmHdStruct_t *hdInfo, 01346 int *depth, 01347 int shellFlag, 01348 array_t *onionRings, 01349 array_t *mintermVarArray, 01350 int oldSize, 01351 double oldMint, 01352 int verbosityLevel) 01353 { 01354 int nvars = Fsm_FsmHdOptionReadNumVars(hdInfo->options); 01355 /* 01356 * Compute a full (non-greedy) dead-end when a dead-end computation 01357 * hasn't occurred, and the jump in minterms is lower than MINT_GROWTH and 01358 * either the old reached size is between MID_SIZE and LARGE_SIZE and the 01359 * jump is MID_SIZE or the new size is larger than LARGE_SIZE and the jump 01360 * is LARGE_SIZE. 01361 */ 01362 if ((hdInfo->deadEndComputation == FALSE) && 01363 ((FsmHdStatsReadMintermReached(hdInfo->stats) - oldMint)/oldMint < FSM_HD_MINT_GROWTH) && 01364 (((FsmHdStatsReadSizeReached(hdInfo->stats) > FSM_HD_MID_SIZE) && 01365 (FsmHdStatsReadSizeReached(hdInfo->stats) - oldSize > FSM_HD_MID_SIZE) && 01366 (oldSize > FSM_HD_MID_SIZE) && (oldSize < FSM_HD_LARGE_SIZE)) || 01367 ((FsmHdStatsReadSizeReached(hdInfo->stats) > FSM_HD_LARGE_SIZE) && 01368 (FsmHdStatsReadSizeReached(hdInfo->stats) - oldSize > FSM_HD_LARGE_SIZE)))) { 01369 if (verbosityLevel >= 2) { 01370 fprintf(vis_stdout, "Full Dead End: New Reached = %d, Minterms = %g\n", 01371 FsmHdStatsReadSizeReached(hdInfo->stats), FsmHdStatsReadMintermReached(hdInfo->stats)); 01372 } 01373 01374 if (*image != NULL) { 01375 mdd_free(*image); 01376 *image = NULL; 01377 } 01378 /* throw away the reached with the jump in size */ 01379 mdd_free(*reachableStates); 01380 if (shellFlag && onionRings) { 01381 mdd_free(array_fetch(mdd_t *, onionRings, array_n(onionRings)-1)); 01382 array_insert(mdd_t *, onionRings, array_n(onionRings)-1, NIL(mdd_t)); 01383 } 01384 01385 *reachableStates = *fromUpperBound; 01386 /* throw away interior state candidates since we just threw away 01387 * the new states 01388 */ 01389 if (hdInfo->interiorStateCandidate != NIL(mdd_t)) { 01390 mdd_free(hdInfo->interiorStateCandidate); 01391 hdInfo->interiorStateCandidate = NIL(mdd_t); 01392 } 01393 01394 if (verbosityLevel >= 2) { 01395 /* record number of dead ends */ 01396 (hdInfo->numDeadEnds)++; 01397 fprintf(vis_stdout, "Dead-End %d at %g seconds - FULL\n", 01398 hdInfo->numDeadEnds, (util_cpu_time()/1000.0)); 01399 } 01400 01401 /* perform a full non-greedy dead-end computation */ 01402 *fromLowerBound = FsmHdDeadEnd(mddManager, imageInfo, *reachableStates, 01403 hdInfo, 01404 mintermVarArray, 01405 FSM_HD_NONGREEDY, verbosityLevel); 01406 (*depth)++; 01407 /* update reached since a new set of seeds have been found */ 01408 assert (!mdd_is_tautology(*fromLowerBound, 0)); 01409 if (shellFlag && onionRings) { 01410 mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0); 01411 if (!mdd_is_tautology(temp, 0)) 01412 array_insert(mdd_t *, onionRings, array_n(onionRings)-1, temp); 01413 else 01414 mdd_free(temp); 01415 } 01416 *fromUpperBound = *reachableStates; 01417 *reachableStates = mdd_or(*fromLowerBound, *fromUpperBound, 1, 1); 01418 FsmHdStatsComputeSizeAndMinterms(mddManager, *reachableStates, 01419 mintermVarArray, nvars, 01420 Fsm_Hd_Reached, hdInfo->stats); 01421 } /* end of if jump in Reached */ 01422 } /* end of HdInduceFullDeadEndIfNecessary */ 01423 01424 01436 static mdd_t * 01437 ComputeInitialStates(Fsm_Fsm_t *fsm, int shellFlag, boolean printWarning) 01438 { 01439 mdd_t *initialStates = NIL(mdd_t); 01440 boolean rings = FALSE; 01441 array_t *mintermVarArray = Fsm_FsmReadPresentStateVars(fsm); 01442 01443 if (Fsm_FsmReadCurrentReachableStates(fsm) == NIL(mdd_t)) { 01444 initialStates = Fsm_FsmComputeInitialStates(fsm); 01445 return (initialStates); 01446 } else if (shellFlag) { 01447 (void) Fsm_FsmReachabilityOnionRingsStates(fsm, &initialStates); 01448 if (initialStates == NIL(mdd_t)) { 01449 initialStates = Fsm_FsmComputeInitialStates(fsm); 01450 return (initialStates); 01451 } else if (mdd_is_tautology(initialStates, 0)) { 01452 initialStates = Fsm_FsmComputeInitialStates(fsm); 01453 return (initialStates); 01454 } 01455 /* some states are found in the onion rings */ 01456 rings = TRUE; 01457 } else { 01458 /* use previously computed states */ 01459 initialStates = mdd_dup(Fsm_FsmReadCurrentReachableStates(fsm)); 01460 } 01461 if (printWarning) { 01462 fprintf(vis_stdout, "** rch warning: Starting reachability analysis from previously computed states.\n"); 01463 fprintf(vis_stdout, "** rch warning: Use compute_reach -F to recompute if necessary.\n"); 01464 fprintf(vis_stdout, "** rch warning: Previously computed states = %g, Size = %d, computation depth = 0-%d\n", mdd_count_onset(Fsm_FsmReadMddManager(fsm), initialStates, mintermVarArray), mdd_size(initialStates), fsm->reachabilityInfo.depth); 01465 if (!rings) { 01466 if (FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Bfs_c) { 01467 fprintf(vis_stdout, "** rch warning: Previous computation done with BFS (-A 0 option)\n"); 01468 } else if (FsmReadReachabilityComputationMode(fsm) == Fsm_Rch_Hd_c) { 01469 fprintf(vis_stdout, "** rch warning: Some previous computations done using BFS/DFS mode (-A 1 or -g option)\n"); 01470 } 01471 } else { 01472 if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Bfs_c) { 01473 fprintf(vis_stdout, "** rch warning: Previous onion rings computed with BFS (-A 0 option)\n"); 01474 } else if (Fsm_FsmReadReachabilityOnionRingsMode(fsm) == Fsm_Rch_Hd_c) { 01475 fprintf(vis_stdout, "** rch warning: Some set of onion rings have been computed using BFS/DFS (-A 1 or -g option)\n"); 01476 } 01477 } 01478 } 01479 return (initialStates); 01480 } /* end of ComputeInitialStates */ 01481 01482 01495 static int 01496 CheckStatesContainedInInvariant(mdd_t *reachableStates, 01497 array_t *invarStates) 01498 { 01499 int i; 01500 mdd_t *invariant; 01501 01502 arrayForEachItem(mdd_t *, invarStates, i, invariant) { 01503 if (invariant == NIL(mdd_t)) continue; 01504 if (!mdd_lequal(reachableStates, invariant, 1, 1)) { 01505 return 0; 01506 } 01507 } 01508 return 1; 01509 } 01510 01542 static void 01543 HdComputeReachabilityParameters(mdd_manager *mddManager, 01544 Img_ImageInfo_t *imageInfo, 01545 mdd_t **reachableStates, 01546 mdd_t **fromUpperBound, 01547 mdd_t **fromLowerBound, 01548 mdd_t **image, 01549 FsmHdStruct_t *hdInfo, 01550 mdd_t *initialStates, 01551 array_t *mintermVarArray, 01552 int *depth, 01553 int printStep, 01554 int shellFlag, 01555 array_t *onionRings, 01556 int verbosityLevel) 01557 { 01558 float growth; 01559 boolean scrapStates; 01560 int nvars = Fsm_FsmHdOptionReadNumVars(hdInfo->options); 01561 int oldSize; 01562 double oldMint; 01563 int sizeOfOnionRings = 0; 01564 if (shellFlag && onionRings) { 01565 sizeOfOnionRings = array_n(onionRings); 01566 } 01567 01568 verbosityLevel = (printStep && (((*depth) % printStep) == 0)) ? verbosityLevel : 0; 01569 01570 /* keep image if small, record size of the image */ 01571 oldSize = FsmHdStatsReadSizeReached(hdInfo->stats); 01572 oldMint = FsmHdStatsReadMintermReached(hdInfo->stats); 01573 FsmHdStatsReset(hdInfo->stats, Fsm_Hd_Reached); 01574 FsmHdStatsReset(hdInfo->stats, Fsm_Hd_FromSubset); 01575 FsmHdStatsReset(hdInfo->stats, Fsm_Hd_From); 01576 01577 scrapStates = Fsm_FsmHdOptionReadScrapStates(hdInfo->options); 01578 hdInfo->onlyPartialImage = Fsm_FsmHdOptionReadOnlyPartialImage(hdInfo->options); 01579 01580 /* Step 1: Check comments at the top of this function */ 01581 /* Check if this is a dead end */ 01582 /* if growth rate of reached is really small, induce a dead-end */ 01583 hdInfo->deadEndComputation = FALSE; 01584 if ((hdInfo->imageOfReachedComputed) || 01585 (mdd_is_tautology(*fromLowerBound, 0)) || 01586 (hdInfo->slowGrowth >= 5)) { 01587 /* 01588 * if image of reached is computed, add to the dead states. 01589 * Set dead-end computation flag and add all new states to Reached. 01590 */ 01591 01592 /* add to interior states */ 01593 hdInfo->interiorStates = AddStates(hdInfo->interiorStates, 01594 hdInfo->interiorStateCandidate, 01595 FSM_MDD_FREE, FSM_MDD_FREE); 01596 hdInfo->interiorStateCandidate = NIL(mdd_t); 01597 if ((verbosityLevel >= 2) && (hdInfo->interiorStates != NIL(mdd_t))) { 01598 fprintf(vis_stdout, "Interior states added, Size = %d, Minterms = %g\n", 01599 mdd_size(hdInfo->interiorStates), mdd_count_onset(mddManager, 01600 hdInfo->interiorStates, mintermVarArray)); 01601 } 01602 01603 hdInfo->deadEndComputation = TRUE; 01604 hdInfo->firstSubset = FALSE; 01605 hdInfo->slowGrowth = 0; 01606 hdInfo->lastIter = *depth; 01607 01608 if (!hdInfo->imageOfReachedComputed) { 01609 /* Either slow growth or real dead-end */ 01610 if (verbosityLevel >= 2) { 01611 if (!mdd_is_tautology(*fromLowerBound, 0)) 01612 fprintf(vis_stdout, "Dead-End triggered by slow growth\n"); 01613 /* record number of dead ends */ 01614 (hdInfo->numDeadEnds)++; 01615 fprintf(vis_stdout, "Dead-End %d at %g seconds\n", hdInfo->numDeadEnds, 01616 (util_cpu_time()/1000.0)); 01617 } 01618 01619 /* add another onion ring. */ 01620 if (shellFlag && onionRings && !mdd_is_tautology(*fromLowerBound, 0)) { 01621 mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0); 01622 if (!mdd_is_tautology(temp, 0)) 01623 array_insert_last(mdd_t *, onionRings, temp); 01624 else 01625 mdd_free(temp); 01626 } 01627 *reachableStates = AddStates(*fromLowerBound, *reachableStates, 01628 FSM_MDD_FREE, FSM_MDD_FREE); 01629 *fromUpperBound = *reachableStates; 01630 01631 /* perform a dead-end computation */ 01632 *fromLowerBound = FsmHdDeadEnd(mddManager, imageInfo, *reachableStates, 01633 hdInfo, 01634 mintermVarArray, 01635 FSM_HD_GREEDY, verbosityLevel); 01636 01637 (*depth)++; 01638 } 01639 } /* end of if dead-end computation */ 01640 01641 /* Step 2: Check comments at the top of this function */ 01642 if (!mdd_is_tautology(*fromLowerBound, 0)) { 01643 /* add another onion ring. */ 01644 if (shellFlag && onionRings) { 01645 mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0); 01646 if (!mdd_is_tautology(temp, 0)) 01647 array_insert_last(mdd_t *, onionRings, temp); 01648 else 01649 mdd_free(temp); 01650 } 01651 /* compute reachable states with new states */ 01652 *fromUpperBound = *reachableStates; 01653 *reachableStates = mdd_or(*fromLowerBound, *fromUpperBound, 1, 1); 01654 FsmHdStatsComputeSizeAndMinterms(mddManager, *reachableStates, 01655 mintermVarArray, nvars, 01656 Fsm_Hd_Reached, hdInfo->stats); 01657 01658 01659 /* 01660 * induce a full dead-end computation if jump in size of Reached is 01661 * large. But when the image of Reached has been computed or a dead-end 01662 * computation was just done, this is not done because deadEndComputation 01663 * has been set to 1. 01664 */ 01665 HdInduceFullDeadEndIfNecessary(mddManager, imageInfo, fromLowerBound, 01666 fromUpperBound, reachableStates, image, 01667 hdInfo, depth, shellFlag, onionRings, 01668 mintermVarArray, oldSize, 01669 oldMint, verbosityLevel); 01670 } /* end of if (!mdd_is_tautology(fromLowerBound, 0)) */ 01671 01672 /* Step 3: Check comments at the top of this function */ 01673 /* Create subset if necessary */ 01674 if (!mdd_is_tautology(*fromLowerBound, 0)) { 01675 if (!hdInfo->onlyPartialImage) { 01676 mdd_t *newStates; 01677 /* 01678 * Now fromUpperBound has the old reached states, reachableStates 01679 * has the new set of states. 01680 */ 01681 newStates = mdd_dup(*fromLowerBound); 01682 FsmHdFromComputeDenseSubset(mddManager, fromLowerBound, 01683 fromUpperBound, reachableStates, 01684 image, initialStates, hdInfo, 01685 shellFlag, onionRings, sizeOfOnionRings, 01686 mintermVarArray); 01687 01688 /* if all new states are chosen from the previous iteration and 01689 * all these states have been added then add to interior states. 01690 * All new states are sometimes not added when 01691 * hdInfo->options->scrapStates is 0. Dead-end computations need not be 01692 * considered here since the interior states were already added then. 01693 */ 01694 if ((hdInfo->interiorStateCandidate != NIL(mdd_t)) && 01695 ((mdd_lequal(newStates, *fromLowerBound, 1, 1)) || 01696 (scrapStates == TRUE))) { 01697 hdInfo->interiorStates = AddStates(hdInfo->interiorStates, hdInfo->interiorStateCandidate, 01698 FSM_MDD_FREE, FSM_MDD_FREE); 01699 hdInfo->interiorStateCandidate = NIL(mdd_t); 01700 if (verbosityLevel >= 2) { 01701 fprintf(vis_stdout, 01702 "Interior states added, Size = %d, Minterms = %g\n", 01703 mdd_size(hdInfo->interiorStates), 01704 mdd_count_onset(mddManager, hdInfo->interiorStates, 01705 mintermVarArray)); 01706 } 01707 } 01708 mdd_free(newStates); 01709 01710 /* end of if fromLowerbound == 0 && subset Flag*/ 01711 } else { 01712 mdd_free(*fromUpperBound); 01713 if (printStep && ((*depth) % printStep == 0)) { 01714 FsmHdStatsComputeSizeAndMinterms(mddManager, *fromLowerBound, 01715 mintermVarArray, nvars, Fsm_Hd_From, hdInfo->stats); 01716 FsmHdStatsSetMintermFromSubset(hdInfo->stats, 0.0); 01717 FsmHdStatsSetSizeFromSubset(hdInfo->stats, 0); 01718 } 01719 *fromUpperBound = *reachableStates; 01720 } 01721 } /* end of if fromLowerBound == 0 */ 01722 if (hdInfo->interiorStateCandidate != NIL(mdd_t)) { 01723 mdd_free(hdInfo->interiorStateCandidate); 01724 hdInfo->interiorStateCandidate = NIL(mdd_t); 01725 } 01726 01727 /* monitor growth rate of reached, record if slow growth in consecutive 01728 * iterations 01729 */ 01730 if (!mdd_is_tautology(*fromLowerBound, 0)) { 01731 FsmHdStatsComputeSizeAndMinterms(mddManager, *reachableStates, 01732 mintermVarArray, nvars, Fsm_Hd_Reached, hdInfo->stats); 01733 growth = (float)(FsmHdStatsReadMintermReached(hdInfo->stats) - oldMint)/ 01734 (float)oldMint; 01735 if ((growth < FSM_HD_GROWTH_RATE) && 01736 (((hdInfo->slowGrowth) && ((*depth) == (hdInfo->lastIter) + 1)) || (!(hdInfo->slowGrowth)))) { 01737 if (verbosityLevel >= 2) { 01738 fprintf(vis_stdout, "Growth rate = %f\n", growth); 01739 } 01740 (hdInfo->slowGrowth)++; 01741 hdInfo->lastIter = *depth; 01742 } else { 01743 /* reset value */ 01744 hdInfo->slowGrowth = 0; 01745 } 01746 } 01747 return; 01748 } /* end of HdComputeReachabilityParameters */ 01749 01762 static int 01763 InitializeIncrementalParameters( 01764 Fsm_Fsm_t *fsm, 01765 Ntk_Network_t *network, 01766 array_t **arrayOfRoots, 01767 st_table **tableOfLeaves) 01768 { 01769 int numLatch; 01770 Ntk_Node_t *node; 01771 lsGen gen; 01772 int i, mddId; /* iterate over the nextStateVars of the fsm */ 01773 01774 numLatch = Ntk_NetworkReadNumLatches(network); 01775 01776 /* This changed to fix a bug. Instead of reading the roots using 01777 Ntk_NetworkForEachCombOutput, we now get them from 01778 fsm->fsdData.nextStateVars, which means that the order is consistent with 01779 the latter field, as required later on in the incremental reachability 01780 code 01781 01782 old code: 01783 *arrayOfRoots = array_alloc(Ntk_Node_t *, numLatch); 01784 Ntk_NetworkForEachCombOutput(network, gen, node) { 01785 if(Ntk_NodeTestIsLatchDataInput(node)){ 01786 array_insert_last(Ntk_Node_t *, *arrayOfRoots, node); 01787 } 01788 } 01789 */ 01790 01791 assert(numLatch == array_n(fsm->fsmData.nextStateVars)); 01792 *arrayOfRoots = array_alloc(Ntk_Node_t *, numLatch); 01793 01794 arrayForEachItem(int, fsm->fsmData.nextStateVars, i, mddId){ 01795 Ntk_Node_t *shadow; 01796 Ntk_Node_t *latch; 01797 Ntk_Node_t *dataInput; 01798 01799 shadow = Ntk_NetworkFindNodeByMddId(network, mddId); 01800 assert(Ntk_NodeTestIsShadow(shadow)); 01801 latch = Ntk_ShadowReadOrigin(shadow); 01802 assert(Ntk_NodeTestIsLatch(latch)); 01803 dataInput = Ntk_LatchReadDataInput(latch); 01804 assert(dataInput != NIL(Ntk_Node_t)); 01805 01806 array_insert(Ntk_Node_t *, *arrayOfRoots, i, dataInput); 01807 } 01808 01809 *tableOfLeaves = st_init_table(st_ptrcmp, st_ptrhash); 01810 Ntk_NetworkForEachCombInput(network, gen, node) { 01811 st_insert(*tableOfLeaves, (char *)node, (char *) (long) (-1) ); 01812 } 01813 return (numLatch); 01814 } 01815 01816 01826 static mdd_t * 01827 IncrementalImageCompute(Ntk_Network_t *network, 01828 Fsm_Fsm_t *fsm, 01829 mdd_manager *mddManager, 01830 mdd_t *fromLowerBound, 01831 mdd_t *fromUpperBound, 01832 mdd_t *toCareSet, 01833 array_t *arrayOfRoots, 01834 st_table *tableOfLeaves, 01835 array_t *smoothVarArray, 01836 array_t *relationArray, 01837 int numLatch) 01838 { 01839 Mvf_Function_t *function; 01840 mdd_t *relation, *optimizedRelation, *toCareSetRV, *imageRV; 01841 mdd_t *subOptimizedRelation, *image; 01842 int mddId, i; 01843 array_t *arrayOfMvf; 01844 mdd_t *frontierSet; 01845 01846 frontierSet = bdd_between(fromLowerBound, fromUpperBound); 01847 /* Create the array of transition relations */ 01848 toCareSetRV = mdd_substitute(mddManager, toCareSet, 01849 fsm->fsmData.presentStateVars, 01850 fsm->fsmData.nextStateVars); 01851 01852 arrayOfMvf = Ntm_NetworkBuildMvfs(network, arrayOfRoots, 01853 tableOfLeaves, frontierSet); 01854 for (i=0; i < numLatch; i++){ 01855 function = array_fetch(Mvf_Function_t *, arrayOfMvf, i); 01856 mddId = array_fetch(int, fsm->fsmData.nextStateVars, i); 01857 /* Since both arrayOfMvf and fsmData have been obtained from */ 01858 /* the same generator */ 01859 relation = Mvf_FunctionBuildRelationWithVariable(function, 01860 mddId); 01861 subOptimizedRelation = bdd_cofactor(relation, toCareSetRV); 01862 mdd_free(relation); 01863 optimizedRelation = bdd_cofactor(subOptimizedRelation, frontierSet); 01864 mdd_free(subOptimizedRelation); 01865 array_insert(mdd_t *, relationArray, i, optimizedRelation); 01866 } 01867 Mvf_FunctionArrayFree(arrayOfMvf); 01868 mdd_free(toCareSetRV); 01869 array_insert(mdd_t *, relationArray, numLatch, frontierSet); 01870 imageRV = Fsm_MddMultiwayAndSmooth(mddManager, relationArray, 01871 smoothVarArray); 01872 /* 01873 ** The above call can be substituted by more sophisticated 01874 ** Img_MultiwayLinearAndSmooth. However, that will have its 01875 ** associated overhead, and could offset any advantage. We 01876 ** expect that individual transition relation relations should 01877 ** be small and monolithic way to handle them would be ok. 01878 ** However, a good strategy would be find the quantification 01879 ** schedule which does not change with the computation of 01880 ** incremental transition relations. 01881 */ 01882 for (i = 0; i <= numLatch; i++){ 01883 mdd_free(array_fetch(mdd_t*, relationArray, i)); 01884 } 01885 assert(CheckImageValidity(mddManager, imageRV, 01886 fsm->fsmData.presentStateVars, 01887 fsm->fsmData.inputVars)); 01888 image = mdd_substitute(mddManager, imageRV, 01889 fsm->fsmData.nextStateVars, 01890 fsm->fsmData.presentStateVars); 01891 mdd_free(imageRV); 01892 assert(CheckImageValidity(mddManager, image, 01893 fsm->fsmData.nextStateVars, 01894 fsm->fsmData.inputVars)); 01895 return image; 01896 } 01897 01907 static void 01908 PrintOnionRings(Fsm_Fsm_t *fsm, int printStep, 01909 Fsm_RchType_t approxFlag, int nvars) 01910 { 01911 int i; 01912 mdd_t *reachableStates; 01913 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); 01914 array_t *mintermVarArray = Fsm_FsmReadPresentStateVars(fsm); 01915 01916 fprintf(vis_stdout, "** rch warning: Not possible to compute size of reachable states at every iteration\n"); 01917 if (Fsm_FsmReadReachabilityOnionRings(fsm) != NIL(array_t)) { 01918 arrayForEachItem(mdd_t *, Fsm_FsmReadReachabilityOnionRings(fsm), 01919 i, reachableStates) { 01920 if (printStep && (i % printStep == 0)) { 01921 if (approxFlag != Fsm_Rch_Hd_c) { 01922 if (nvars <= 1023) { 01923 (void)fprintf(vis_stdout, "BFS step = %d\t|onion ring states| = %8g", 01924 i, mdd_count_onset(mddManager, reachableStates, 01925 mintermVarArray)); 01926 if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) { 01927 fprintf(vis_stdout, "\n"); 01928 } else { 01929 fprintf(vis_stdout, "\tSize = %d\n", mdd_size(reachableStates)); 01930 } 01931 01932 } else { 01933 (void)fprintf(vis_stdout, "BFS step = %d\t|onion ring states| = ", 01934 i); 01935 (void) bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6); 01936 if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) { 01937 fprintf(vis_stdout, "Final Size = %d\n", mdd_size(reachableStates)); 01938 } 01939 } 01940 } else { 01941 01942 if (nvars <= 1023) { 01943 (void)fprintf(vis_stdout, "Step = %d\t|onion ring states| = %8g", 01944 i, mdd_count_onset(mddManager, reachableStates, 01945 mintermVarArray)); 01946 if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) { 01947 fprintf(vis_stdout, "\n"); 01948 } else { 01949 fprintf(vis_stdout, "\tSize = %d\n", mdd_size(reachableStates)); 01950 } 01951 } else { 01952 (void)fprintf(vis_stdout, "Step = %d\t|onion ring states| = ", 01953 i); 01954 (void) bdd_print_apa_minterm(vis_stdout, reachableStates, nvars, (long)6); 01955 if (i != array_n(Fsm_FsmReadReachabilityOnionRings(fsm))-1) { 01956 fprintf(vis_stdout, "Final Size = %d\n", mdd_size(reachableStates)); 01957 } 01958 } 01959 } 01960 } 01961 } 01962 } 01963 return; 01964 }/* printonionrings */ 01965 01982 static array_t * 01983 GenerateGuidedSearchSequenceArray(array_t *guideArray) 01984 { 01985 char *seqStr = Cmd_FlagReadByName("guided_search_sequence"); 01986 char *preStr; 01987 int intEntry; 01988 array_t *depthArray = array_alloc(int, 0); 01989 int i; 01990 01991 /* Skip parsing if we have no guided search sequence */ 01992 if (seqStr != NIL(char) && strcmp(seqStr, "") != 0){ 01993 preStr = strtok(seqStr, ","); 01994 01995 while(preStr != NIL(char)){ 01996 intEntry = strtol(preStr, (char **) NULL, 10); 01997 array_insert_last(int, depthArray, (intEntry == 0 ? -1 : intEntry)); 01998 preStr = strtok(NIL(char), ","); 01999 } 02000 } 02001 02002 if(array_n(depthArray) > array_n(guideArray)){ 02003 fprintf(vis_stdout, "** rch warning: guided_search_sequence has more entries\n"); 02004 fprintf(vis_stdout,"than there are hints. Extra entires will be ignored\n"); 02005 } 02006 02007 /* pad with -1s */ 02008 for (i = array_n(depthArray); i < array_n(guideArray); i++) { 02009 array_insert_last(int, depthArray, -1); 02010 } 02011 02012 assert(array_n(depthArray) >= array_n(guideArray)); 02013 02014 return depthArray; 02015 } 02016 02017 02034 static void 02035 ComputeReachabilityParameters(mdd_manager *mddManager, 02036 Img_ImageInfo_t *imageInfo, 02037 Fsm_RchType_t approxFlag, 02038 mdd_t **reachableStates, 02039 mdd_t **fromUpperBound, 02040 mdd_t **fromLowerBound, 02041 mdd_t **image, 02042 FsmHdStruct_t *hdInfo, 02043 mdd_t *initialStates, 02044 array_t *mintermVarArray, 02045 int *depth, 02046 int printStep, 02047 int shellFlag, 02048 array_t *onionRings, 02049 int verbosityLevel, 02050 boolean guidedSearchMode, 02051 mdd_t *hint, 02052 int *hintDepth, 02053 boolean *notConverged) 02054 { 02055 if (approxFlag == Fsm_Rch_Bfs_c) { 02056 /* New set of reachable states is old set plus new states in image. */ 02057 *reachableStates = AddStates(*fromLowerBound, *reachableStates, 02058 FSM_MDD_DONT_FREE, FSM_MDD_FREE); 02059 *fromUpperBound = *reachableStates; 02060 02061 /* in guided search, if the mode is to convergence or the 02062 limited depth has not been reached, and the frontier is empty, 02063 then generate a frontier in BFS mode (that is a full dead-end). */ 02064 if (guidedSearchMode && 02065 mdd_is_tautology(*fromLowerBound, 0) /* no frontier */ && 02066 (hdInfo->deadEndWithOriginalTR == FALSE) /* and guided search */ ) { 02067 assert(imageInfo != NIL(Img_ImageInfo_t)); 02068 if (*hintDepth != 0) { 02069 /* add another onion ring. */ 02070 if (shellFlag && onionRings) { 02071 mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0); 02072 if (!mdd_is_tautology(temp, 0)) 02073 array_insert_last(mdd_t *, onionRings, temp); 02074 else 02075 mdd_free(temp); 02076 } 02077 /* do a full dead-end (non-greedy), compute all the frontier states */ 02078 mdd_free(*fromLowerBound); 02079 *fromLowerBound = FsmHdDeadEnd(mddManager, imageInfo, *reachableStates, 02080 hdInfo, 02081 mintermVarArray, 02082 FSM_HD_NONGREEDY, verbosityLevel); 02083 mdd_free(hdInfo->interiorStates); 02084 hdInfo->interiorStates = NIL(mdd_t); 02085 *reachableStates = AddStates(*fromLowerBound, *reachableStates, 02086 FSM_MDD_DONT_FREE, FSM_MDD_FREE); 02087 *fromUpperBound = *reachableStates; 02088 (*hintDepth)--; 02089 (*depth)++; 02090 if (mdd_is_tautology(hint, 1)) hdInfo->deadEndWithOriginalTR = TRUE; 02091 } else { 02092 *notConverged = TRUE; 02093 /* set this flag for correct detection of convergence 02094 Corner case: when limited depth and frontier = 0 */ 02095 } 02096 } 02097 } else if (approxFlag == Fsm_Rch_Hd_c) { 02098 assert(imageInfo != NIL(Img_ImageInfo_t)); 02099 if (!guidedSearchMode || (*hintDepth != 0)) { 02100 /* computes reachable states, fromLowerBound and fromUpperBound. 02101 * Updates all other quantities such as interiorStates, 02102 * deadEndResidue. */ 02103 HdComputeReachabilityParameters(mddManager, imageInfo, 02104 reachableStates, 02105 fromUpperBound, 02106 fromLowerBound, 02107 image, 02108 hdInfo, 02109 initialStates, 02110 mintermVarArray, 02111 depth, printStep, 02112 shellFlag, onionRings, 02113 verbosityLevel); 02114 if (guidedSearchMode) (*hintDepth)--; 02115 02116 } else { /* guidedSearchMode and hint depth is 0 */ 02117 if (mdd_is_tautology(*fromLowerBound, 0)) { 02118 *notConverged = TRUE; 02119 /* set this flag for correct detection of convergence 02120 Corner case: when limited depth and frontier = 0 */ 02121 } 02122 /* add another onion ring. */ 02123 if (shellFlag && onionRings) { 02124 mdd_t *temp = mdd_and(*fromLowerBound, *reachableStates, 1, 0); 02125 if (!mdd_is_tautology(temp, 0)) 02126 array_insert_last(mdd_t *, onionRings, temp); 02127 else 02128 mdd_free(temp); 02129 } 02130 02131 } 02132 } 02133 return; 02134 } /* End of ComputeReachabilityParameters */