/**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.] ******************************************************************************/ #include "fsmInt.h" #include "ntm.h" static char rcsid[] UNUSED = "$Id: fsmArdc.c,v 1.86 2009/04/12 00:44:04 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ #define ARDC_MAX_LINE_LEN 4096 /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ 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); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ void Fsm_ArdcMinimizeTransitionRelation(Fsm_Fsm_t *fsm, Img_DirectionType fwdbwd) { 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; } /**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 [] ******************************************************************************/ mdd_t * Fsm_ArdcComputeImage(Fsm_Fsm_t *fsm, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) { 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); } /**Function******************************************************************** Synopsis [Computes overapproximate reachable states.] Description [Computes overapproximate reachable states. This function is a wrapper around Fsm_ArdcComputeOverApproximateReachableStates.] SideEffects [] SeeAlso [Fsm_ArdcComputeOverApproximateReachableStates] ******************************************************************************/ 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 *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); } /**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] ******************************************************************************/ 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 *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); } /**Function******************************************************************** Synopsis [Performs state space decomposition.] Description [Performs state space decomposition.] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * Fsm_ArdcDecomposeStateSpace(Ntk_Network_t *network, array_t *presentStateVars, array_t *nextStateFunctions, Fsm_ArdcOptions_t *options) { 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); } /**Function******************************************************************** Synopsis [Allocates an ARDC option structure.] Description [Allocates an ARDC option structure.] SideEffects [] SeeAlso [] ******************************************************************************/ Fsm_ArdcOptions_t * Fsm_ArdcAllocOptionsStruct(void) { Fsm_ArdcOptions_t *options; options = ALLOC(Fsm_ArdcOptions_t, 1); (void)memset((void *)options, 0, sizeof(Fsm_ArdcOptions_t)); return(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 = 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 (default = 8) set ardc_affinity_factor f = 0.0 - 1.0 (default = 0.5) set ardc_max_iteration n (default = 0(infinity)) set ardc_constrain_target m = 0 : constrain transition relation (default) m = 1 : constrain initial states m = 2 : constrain both set ardc_constrain_method 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 = 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 = 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 = yes : keep decomposed reachable stateses (default) m = no : make a conjunction of reachable states of all submachines set ardc_projected_initial_flag m = yes : use projected initial states for submachine (default) m = no : use original initial states for submachine set ardc_image_method 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 = 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 = 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 = 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 = 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 = 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 = yes : use constrained transition relation for next iteration m = no : use original transition relation for next iteration (default) set ardc_read_group file containing grouping information set ardc_write_group file to write grouping information set ardc_verbosity n = 0 - 3 (default = 0) ] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcGetDefaultOptions(Fsm_ArdcOptions_t *options) { 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; } /**Function******************************************************************** Synopsis [Reads traversal method option.] Description [Reads traversal method option.] SideEffects [] SeeAlso [] ******************************************************************************/ Fsm_Ardc_TraversalType_t Fsm_ArdcOptionsReadTraversalMethod(Fsm_ArdcOptions_t *options) { return(options->traversalMethod); } /**Function******************************************************************** Synopsis [Reads group size option.] Description [Reads group size option.] SideEffects [] SeeAlso [] ******************************************************************************/ int Fsm_ArdcOptionsReadGroupSize(Fsm_ArdcOptions_t *options) { return(options->groupSize); } /**Function******************************************************************** Synopsis [Reads affinity factor option.] Description [Reads affinity factor option.] SideEffects [] SeeAlso [] ******************************************************************************/ float Fsm_ArdcOptionsReadAffinityFactor(Fsm_ArdcOptions_t *options) { return(options->affinityFactor); } /**Function******************************************************************** Synopsis [Reads constrain method option.] Description [Reads constrain method option.] SideEffects [] SeeAlso [] ******************************************************************************/ Img_MinimizeType Fsm_ArdcOptionsReadConstrainMethod(Fsm_ArdcOptions_t *options) { return(options->constrainMethod); } /**Function******************************************************************** Synopsis [Reads constrain option.] Description [Reads constrain option.] SideEffects [] SeeAlso [] ******************************************************************************/ Fsm_Ardc_ConstrainTargetType_t Fsm_ArdcOptionsReadConstrainTarget(Fsm_ArdcOptions_t *options) { return(options->constrainTarget); } /**Function******************************************************************** Synopsis [Reads max iteration option.] Description [Reads max iteration option.] SideEffects [] SeeAlso [] ******************************************************************************/ int Fsm_ArdcOptionsReadMaxIteration(Fsm_ArdcOptions_t *options) { return(options->maxIteration); } /**Function******************************************************************** Synopsis [Reads abstract pseudo input option.] Description [Reads abstract pseudo input option.] SideEffects [] SeeAlso [] ******************************************************************************/ Fsm_Ardc_AbstPpiType_t Fsm_ArdcOptionsReadAbstractPseudoInput(Fsm_ArdcOptions_t *options) { return(options->abstractPseudoInput); } /**Function******************************************************************** Synopsis [Reads decomposed constraint option.] Description [Reads decomposed constraint option.] SideEffects [] SeeAlso [] ******************************************************************************/ boolean Fsm_ArdcOptionsReadDecomposeFlag(Fsm_ArdcOptions_t *options) { return(options->decomposeFlag); } /**Function******************************************************************** Synopsis [Reads initial states mode option.] Description [Reads initial states mode option.] SideEffects [] SeeAlso [] ******************************************************************************/ boolean Fsm_ArdcOptionsReadProjectedInitialFlag(Fsm_ArdcOptions_t *options) { return(options->projectedInitialFlag); } /**Function******************************************************************** Synopsis [Reads constrain reorder flag option.] Description [Reads constrain reorder flag option.] SideEffects [] SeeAlso [] ******************************************************************************/ boolean Fsm_ArdcOptionsReadConstrainReorderFlag(Fsm_ArdcOptions_t *options) { return(options->constrainReorderFlag); } /**Function******************************************************************** Synopsis [Reads image method for ARDC computation.] Description [Reads image method for ARDC computation.] SideEffects [] SeeAlso [] ******************************************************************************/ Img_MethodType Fsm_ArdcOptionsReadImageMethod(Fsm_ArdcOptions_t *options) { return(options->ardcImageMethod); } /**Function******************************************************************** Synopsis [Reads use high density option.] Description [Reads use high density option.] SideEffects [] SeeAlso [] ******************************************************************************/ boolean Fsm_ArdcOptionsReadUseHighDensity(Fsm_ArdcOptions_t *options) { return(options->useHighDensity); } /**Function******************************************************************** Synopsis [Reads verbosity option.] Description [Reads verbosity option.] SideEffects [] SeeAlso [] ******************************************************************************/ int Fsm_ArdcOptionsReadVerbosity(Fsm_ArdcOptions_t *options) { return(options->verbosity); } /**Function******************************************************************** Synopsis [Sets traversal method option.] Description [Sets traversal method option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetTraversalMethod(Fsm_ArdcOptions_t *options, Fsm_Ardc_TraversalType_t traversalMethod) { options->traversalMethod = traversalMethod; } /**Function******************************************************************** Synopsis [Sets group size option.] Description [Sets group size option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetGroupSize(Fsm_ArdcOptions_t *options, int groupSize) { options->groupSize = groupSize; } /**Function******************************************************************** Synopsis [Sets affinity factor option.] Description [Sets affinity factor option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetAffinityFactor(Fsm_ArdcOptions_t *options, float affinityFactor) { options->affinityFactor = affinityFactor; } /**Function******************************************************************** Synopsis [Sets constrain method option.] Description [Sets constrain method option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetConstrainMethod(Fsm_ArdcOptions_t *options, Img_MinimizeType constrainMethod) { options->constrainMethod = constrainMethod; } /**Function******************************************************************** Synopsis [Sets constrain option.] Description [Sets constrain option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetConstrainTarget(Fsm_ArdcOptions_t *options, Fsm_Ardc_ConstrainTargetType_t constrainTarget) { options->constrainTarget = constrainTarget; } /**Function******************************************************************** Synopsis [Sets max iteration option.] Description [Sets max iteration option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetMaxIteration(Fsm_ArdcOptions_t *options, int maxIteration) { options->maxIteration = maxIteration; } /**Function******************************************************************** Synopsis [Sets abstract pseudo input option.] Description [Sets abstract pseudo input option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetAbstractPseudoInput(Fsm_ArdcOptions_t *options, Fsm_Ardc_AbstPpiType_t abstractPseudoInput) { options->abstractPseudoInput = abstractPseudoInput; } /**Function******************************************************************** Synopsis [Sets decomposed constraint option.] Description [Sets decomposed constraint option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetDecomposeFlag(Fsm_ArdcOptions_t *options, boolean decomposeFlag) { options->decomposeFlag = decomposeFlag; } /**Function******************************************************************** Synopsis [Sets initial states mode option.] Description [Sets initial states mode option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetProjectedInitialFlag(Fsm_ArdcOptions_t *options, boolean projectedInitialFlag) { options->projectedInitialFlag = projectedInitialFlag; } /**Function******************************************************************** Synopsis [Sets constrain reorder flag option.] Description [Sets constrain reorder flag option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetConstrainReorderFlag(Fsm_ArdcOptions_t *options, int constrainReorderFlag) { options->constrainReorderFlag = constrainReorderFlag; } /**Function******************************************************************** Synopsis [Sets image method for ARDC computation.] Description [Sets image method for ARDC computation.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetImageMethod(Fsm_ArdcOptions_t *options, Img_MethodType ardcImageMethod) { options->ardcImageMethod = ardcImageMethod; } /**Function******************************************************************** Synopsis [Sets use high density option.] Description [Sets use high density option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetUseHighDensity(Fsm_ArdcOptions_t *options, boolean useHighDensity) { options->useHighDensity = useHighDensity; } /**Function******************************************************************** Synopsis [Sets verbosity option.] Description [Sets verbosity option.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcOptionsSetVerbosity(Fsm_ArdcOptions_t *options, int verbosity) { options->verbosity = verbosity; } /**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 [] ******************************************************************************/ double Fsm_ArdcCountOnsetOfOverApproximateReachableStates(Fsm_Fsm_t *fsm) { 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); } /**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 [] ******************************************************************************/ int Fsm_ArdcBddSizeOfOverApproximateReachableStates(Fsm_Fsm_t *fsm) { 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); } /**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 [] ******************************************************************************/ mdd_t * Fsm_ArdcGetMddOfOverApproximateReachableStates(Fsm_Fsm_t *fsm) { 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); } /**Function******************************************************************** Synopsis [Prints info about overapproximate reachable states.] Description [Prints info about overapproximate reachable states.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_ArdcPrintReachabilityResults(Fsm_Fsm_t *fsm, long elapseTime) { 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; } } /**Function******************************************************************** Synopsis [Reads ARDC verbosity option.] Description [Reads ARDC verbosity option.] SideEffects [] SeeAlso [] ******************************************************************************/ int Fsm_ArdcReadVerbosity(void) { char *flagValue; int verbosity = 0; flagValue = Cmd_FlagReadByName("ardc_verbosity"); if (flagValue != NIL(char)) sscanf(flagValue, "%d", &verbosity); return(verbosity); } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Check if each conjunct is contained in the invariant.] Description [Check if each conjunct is contained in the invariant.] SideEffects [] SeeAlso [] ******************************************************************************/ int FsmArdcCheckInvariant(Fsm_Fsm_t *fsm, array_t *invarStates) { 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; } /**Function******************************************************************** Synopsis [Prints ARDC options currently in use.] Description [Prints ARDC options currently in use.] SideEffects [] SeeAlso [] ******************************************************************************/ void FsmArdcPrintOptions(void) { 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"); } /**Function******************************************************************** Synopsis [Prints BDDS of approximate reachable states of an FSM.] Description [Prints BDDS of approximate reachable states of an FSM.] SideEffects [] SeeAlso [] ******************************************************************************/ void FsmArdcPrintOverApproximateReachableStates(Fsm_Fsm_t *fsm) { 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); } /**Function******************************************************************** Synopsis [Prints BDDS of exact reachable states of an FSM.] Description [Prints BDDS of exact reachable states of an FSM.] SideEffects [] SeeAlso [] ******************************************************************************/ void FsmArdcPrintExactReachableStates(Fsm_Fsm_t *fsm) { 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); } /**Function******************************************************************** Synopsis [Prints BDDs of a node.] Description [Prints BDDs of a node.] SideEffects [] SeeAlso [] ******************************************************************************/ void FsmArdcPrintBddOfNode(Fsm_Fsm_t *fsm, mdd_t *node) { PrintBddWithName(fsm, NIL(array_t), node); } /**Function******************************************************************** Synopsis [Prints array of array of integer.] Description [Prints array of array of integer.] SideEffects [] SeeAlso [] ******************************************************************************/ void FsmArdcPrintArrayOfArrayInt(array_t *arrayOfArray) { 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"); } } /**Function******************************************************************** Synopsis [Returns a set Boolean value related ARDC computation.] Description [Returns a set Boolean value related ARDC computation.] SideEffects [] SeeAlso [] ******************************************************************************/ boolean FsmGetArdcSetBooleanValue(char *string, boolean defaultValue) { 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); } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ static void SortSubFsmsForApproximateTraversal(array_t **subFsmArray, array_t **fanInsIndexArray, array_t **fanOutsIndexArray, int verbosityLevel) { 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; } /**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] ******************************************************************************/ static array_t * ArdcMbmTraversal( Fsm_Fsm_t *fsm, int nvars, array_t *subFsmArray, array_t *fanInsIndexArray, array_t *fanOutsIndexArray, mdd_t ***subReached /* sub-result for TMBM, pointer of bdd array */, /* The following arguments up to approxFlag are passed for exact * reachability. */ int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, Fsm_ArdcOptions_t *options, boolean lfpFlag /* If TRUE, performs LMBM */ ) { 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); } /**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] ******************************************************************************/ 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) { 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); } /**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] ******************************************************************************/ 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) { 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); } /**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] ******************************************************************************/ 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) { 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); } /**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] ******************************************************************************/ 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) { 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); } /**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] ******************************************************************************/ static void ComputeFaninConstrainArray(array_t *faninConstrainArray, mdd_t **constraint, int current, array_t *fans, int decomposeFlag, int faninConstrainMode) { 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); } } /**Function******************************************************************** Synopsis [Minimizes transition relation with fanin constraint.] Description [Minimizes transition relation with fanin constraint.] SideEffects [] SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal] ******************************************************************************/ static void MinimizeTransitionRelationWithFaninConstraint(Img_ImageInfo_t *imageInfo, array_t *faninConstrainArray, Img_MinimizeType constrainMethod, boolean reorderPtrFlag, boolean duplicate) { if (duplicate) { Img_DupTransitionRelation(imageInfo, Img_Forward_c); Img_ResetTrMinimizedFlag(imageInfo, Img_Forward_c); } Img_MinimizeTransitionRelation(imageInfo, faninConstrainArray, constrainMethod, Img_Forward_c, reorderPtrFlag); } /**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] ******************************************************************************/ static void ComputeConstrainedInitialStates(Fsm_Fsm_t *subFsm, array_t *faninConstrainArray, Img_MinimizeType constrainMethod) { 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; } /**Function******************************************************************** Synopsis [Makes an array of approximate reachable states.] Description [Makes an array of approximate reachable states.] SideEffects [] SeeAlso [ArdcMbmTraversal ArdcRfbfTraversal ArdcTfbfTraversal] ******************************************************************************/ static void ComputeApproximateReachableStatesArray(mdd_manager *mddManager, array_t *reachedArray, mdd_t **reached, mdd_t ***subReached, int nSubFsms, int decomposeFlag) { 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); } } /**Function******************************************************************** Synopsis [Copy exact reached states to overapproximate.] Description [Copy exact reached states to overapproximate.] SideEffects [] SeeAlso [] ******************************************************************************/ static array_t * ArdcCopyOverApproxReachableStatesFromExact(Fsm_Fsm_t *fsm) { 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); } /**Function******************************************************************** Synopsis [Prints current approximate reached states.] Description [Prints current approximate reached states.] SideEffects [] SeeAlso [] ******************************************************************************/ 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) { 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; } } /**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 [] ******************************************************************************/ static void PrintBddWithName(Fsm_Fsm_t *fsm, array_t *mddIdArr, mdd_t *node) { 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); } /**Function******************************************************************** Synopsis [Reads grouping information.] Description [Reads grouping information.] SideEffects [] SeeAlso [] ******************************************************************************/ static void ArdcReadGroup(Ntk_Network_t *network, FILE *groupFile, array_t *latchNameArray, array_t *groupIndexArray) { 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); } } } /**Function******************************************************************** Synopsis [Writes one grouping information.] Description [Writes one grouping information.] SideEffects [] SeeAlso [] ******************************************************************************/ static void ArdcWriteOneGroup(Part_Subsystem_t *partitionSubsystem, FILE *groupFile, int i) { 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"); } /**Function******************************************************************** Synopsis [Prints one grouping information.] Description [Prints one grouping information.] SideEffects [] SeeAlso [] ******************************************************************************/ static void ArdcPrintOneGroup(Part_Subsystem_t *partitionSubsystem, int i, int nLatches, array_t *fanIns, array_t *fanOuts) { 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"); } /**Function******************************************************************** Synopsis [Returns a set integer value related ARDC computation.] Description [Returns a set integer value related ARDC computation.] SideEffects [] SeeAlso [] ******************************************************************************/ static int GetArdcSetIntValue(char *string, int l, int u, int defaultValue) { 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); } /**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 [] ******************************************************************************/ static void ArdcEpdCountOnsetOfOverApproximateReachableStates(Fsm_Fsm_t *fsm, EpDouble *epd) { 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); } } /**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 [] ******************************************************************************/ static mdd_t * QuantifyVariables(mdd_t *state, array_t *smoothArray, mdd_t *smoothCube) { if (smoothCube) return(bdd_smooth_with_cube(state, smoothCube)); else return(bdd_smooth(state, smoothArray)); } /**Function******************************************************************** Synopsis [Updates event scheduling of submachines for traversal.] Description [Updates event scheduling of submachines for traversal.] SideEffects [] SeeAlso [] ******************************************************************************/ static void UpdateMbmEventSchedule(Fsm_Fsm_t **subFsm, array_t *fanOutIndices, int *traverse, int lfpFlag) { 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; } } /**Function******************************************************************** Synopsis [Prints statistics of transition function method.] Description [Prints statistics of transition function method.] SideEffects [] SeeAlso [] ******************************************************************************/ static void PrintTfmStatistics(array_t *subFsmArray) { 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); } }