/**CHeaderFile***************************************************************** FileName [fsmInt.h] PackageName [fsm] Synopsis [Internal declarations for fsm package.] Author [Shaker Sarwary, Tom Shiple, Rajeev Ranjan, Kavita Ravi, In-Ho Moon] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. 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 CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. THE UNIVERSITY OF CALIFORNIA 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 CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] Revision [$Id: fsmInt.h,v 1.45 2003/01/22 18:44:20 jinh Exp $] ******************************************************************************/ #ifndef _FSMINT #define _FSMINT #include "fsm.h" #include "ord.h" #include "part.h" #include "mc.h" #include /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [Canonical fairness constraint.] Description [Canonical fairness constraint. This is an array of arrays, where each entry is a pair of CTL formulas, S_ij and T_ij. Each CTL formula identifies a set of states of the FSM. The interpretation of this 2-D array is: (OR_i (AND_j (F-inf S_ij + G-inf T_ij))). Hence, disjunctArray is an array of array_t * of FairnessConjunct_t *.] SeeAlso [Fsm_FsmReadFairnessConstraint] ******************************************************************************/ struct FsmFairnessStruct { Fsm_Fsm_t *fsm; /* fsm to which the fairness constraint is associated */ array_t *disjunctArray; /* canonical fairness constraint */ }; /**Enum************************************************************************ Synopsis [Specifies type of status of overapproximate reached states.] Description [Specifies type of status of overapproximate reached states.] SideEffects [] SeeAlso [] ******************************************************************************/ typedef enum { Fsm_Ardc_NotConverged_c, Fsm_Ardc_Valid_c, Fsm_Ardc_Converged_c, Fsm_Ardc_Exact_c } Fsm_Ardc_StatusType_t; /**Struct********************************************************************** Synopsis [A finite state machine.] Description [A finite state machine. See fsm.h for an overview of the structure. Non-obvious fields are described here:

the ith entry of the array reachabilityInfo.onionRings contains the set of states reached in i steps from the initial states. The type of reachability computation may have been approximate. Therefore the distance from the initial state may not exactly be i. Further, these onion rings may not be consistent with the reachable states. But their sum will always be smaller than or equal to the reachableStates field.

The onionRingsUpToDate field indicates whether the onion rings are consistent with the reachable states.

The onionRingsBFS field indicates whether onion rings were generated with BFS.

The depth pertains to the depth of computation with respect to the reachableStates field. In case of approximate computation and reordering, the depth and the exact onion rings may not be reproducible.

The mode field indicates how the reachable states were generated. If they were ever generated using HD, this is marked.

FairnessInfo.states is the set of fair states (i.e. those states from which there exists a fair path). FairnessInfo.dbgArray is an array of array_t* of mdd_t*, where the jth MDD of the ith array gives the set of states that can reach the ith Buchi set in j or fewer steps.

FsmData.nextStateFunctions is an array of strings, containing the names of the nodes driving the data inputs of latches.

presentStateVars, nextStateVars, and nextStateFunctions are all in one-to-one correspondence.] ******************************************************************************/ struct FsmFsmStruct { Ntk_Network_t *network; /* corresponding network */ graph_t *partition; /* DAG of MVFs giving the next state fns */ Img_ImageInfo_t *imageInfo; Img_ImageInfo_t *unquantifiedImageInfo; bdd_t *extQuantifyInputCube; bdd_t *uniQuantifyInputCube; boolean useUnquantifiedFlag; boolean FAFWFlag; struct { mdd_t *initialStates; mdd_t *reachableStates; /* reachable states or an under-approximation */ int depth; /* depth upto which the traversal was carried out. */ Fsm_RchType_t reachabilityMode; /* indicates what mode(BFS/HD) was applied to reachability. */ Fsm_RchStatus_t rchStatus; /* specified whether the reachable states is exact or an under approximation or an over aproximation. */ Fsm_Ardc_StatusType_t overApprox; /* status of current overapproximate reached states. */ array_t *apprReachableStates; /* to store overapproximate reachable states*/ array_t *subPsVars; /* to store real present state variables of submachines in over-approximate reachability computation */ array_t *onionRings; /* array of mdd_t* */ Fsm_RchType_t onionRingsMode; /* indicates whether onion rings were generated with BFS or some approximate method */ boolean onionRingsUpToDate; /* flag which indicates whether the sum of onion rings is equal to reachable states */ } reachabilityInfo; struct { mdd_t *states; Fsm_Fairness_t *constraint; array_t *dbgArray; /* array of array_t* of mdd_t* */ } fairnessInfo; struct { array_t *presentStateVars; /* array of MDD id's */ array_t *nextStateVars; /* array of MDD id's */ array_t *inputVars; /* array of MDD id's */ array_t *nextStateFunctions; /* array of char* */ /* The following 3 are just for subsystems. * inputVars = primaryInputVars + pseudoInputVars * globalPsVars = presentStateVars + pseudoInputVars */ array_t *pseudoInputVars; /* array of MDD id's */ array_t *primaryInputVars; /* array of MDD id's */ array_t *globalPsVars; /* array of MDD id's */ mdd_t *presentStateCube; mdd_t *nextStateCube; mdd_t *inputCube; mdd_t *pseudoInputCube; mdd_t *primaryInputCube; mdd_t *globalPsCube; array_t *presentStateBddVars; /* array of bdd variables */ array_t *pseudoInputBddVars; /* array of bdd variables */ boolean createVarCubesFlag; } fsmData; // For robustness computation struct { mdd_t * originalreachableStates; mdd_t * Safe; FILE* fSafe; mdd_t * Forb; FILE* fForb; mdd_t * Req; FILE* fReq; } RobSets; }; /**Struct********************************************************************** Synopsis [Specifies options for ARDC computation.] Description [Specifies options for ARDC computation.] SideEffects [] SeeAlso [] ******************************************************************************/ struct FsmArdcOptionsStruct { Fsm_Ardc_TraversalType_t traversalMethod; /* one of MBM, RFBF, TFBF, TMBM, LMBM, SIMPLE */ int groupSize; /* number of latches per group in state space decomposition */ float affinityFactor; /* controls weight between dependency and correlation in state space decomposition */ Img_MinimizeType constrainMethod; /* which operator is going to be used for image constraining ** operation among restrict, constrain, compact, and squeeze */ Fsm_Ardc_ConstrainTargetType_t constrainTarget; /* where to apply image constraining between ** transition relation and initial states */ int maxIteration; /* maximum iteration number in approximate traversal */ Fsm_Ardc_AbstPpiType_t abstractPseudoInput; /* when to abstract pseudo input variables ** from transition relation or reachable states */ boolean decomposeFlag; /* whether to use single conjuncted approximate reachable ** states or decomposed approximate reachable states */ boolean projectedInitialFlag; /* whether to use original initial states or projected initial states */ boolean constrainReorderFlag; /* if set, allow variable reorderings during image constraining operation */ Img_MethodType ardcImageMethod; boolean useHighDensity; /* if set, use high density */ boolean reorderPtrFlag; int faninConstrainMode; char *readGroupFile; char *writeGroupFile; int lmbmInitialStatesMode; boolean mbmReuseTrFlag; int createPseudoVarMode; int verbosity; /* print more information */ }; /**Struct********************************************************************** Synopsis [Approximate Traversal option structure.] Description [Approximate Traversal option structure. Set by set commands. See help in CommandPrintHdOptions.] SideEffects [] SeeAlso [] ******************************************************************************/ struct FsmHdTravOptions { int nvars; /* number of bdd state variables */ bdd_approx_type_t frontierApproxMethod; /* type of approximation to use to extract subset of from */ int frontierApproxThreshold; /* threshold for approximation */ Fsm_HdDeadEndType_t deadEnd; /* kind of dead-end method to use */ bdd_approx_type_t deadEndSubsetMethod; /* which approximation method to use in dead-ends */ double quality; /* quality factor for bdd_apprxo_remap_ua method */ double qualityBias; /* quality factor for bdd_approx_remap_ua method */ boolean scrapStates; /* option to not add scrap states */ boolean newOnly; /* option to pick frontier from the new states only */ boolean onlyPartialImage; /* option to only use partial image computation */ }; /**Struct********************************************************************** Synopsis [Stats structure to store size and minterm count] Description [Stats structure to store size and minterm count] SideEffects [] SeeAlso [] ******************************************************************************/ struct FsmHdMintSizeStats { int sizeTo; /* size of image */ double mintermTo; /* minterms of image */ int sizeFrom; /* size of from (frontier) */ double mintermFrom; /* minterms of from (frontier) */ int sizeFromSubset; /* size of subset of frontier */ double mintermFromSubset; /* minterms of subset of frontier */ int sizeReached; /* size of reached set */ double mintermReached; /* minterms of reached set */ }; /**Struct********************************************************************** Synopsis [Structure to store HD related information.] Description [Structure to store HD related information.] SideEffects [] SeeAlso [] ******************************************************************************/ struct FsmHdStruct { int numDeadEnds; /* number of dead computations performed. */ boolean firstSubset; /* indicates that first subset has been computed*/ int lastIter; /* indicates the last iteration in which a slow growth * of reached was recorded. */ boolean partialImage;/* iff partial image computation was performed */ int residueCount;/* number of times the residue has been used in a dead end*/ mdd_t *interiorStates; /* states which cannot produce any new states */ mdd_t *interiorStateCandidate; /* states which could potentially belong to * interior states. */ mdd_t *deadEndResidue; /* states which do not lie in dense subset * of "from" after dead-end computation */ struct FsmHdTravOptions *options; /* options for HD traversal */ struct FsmHdMintSizeStats *stats; /* structure storing minterms and sizes of the * various BDDs of traversal. */ boolean imageOfReachedComputed; /* iff image of reached set was computed.*/ boolean onlyPartialImage; /* flag indicating that only partial image * should be used during traversal. */ int slowGrowth; /* number of successive iterations of slow growth of * reached */ boolean deadEndWithOriginalTR; /* this flag allows computing a dead end at * the end if all the frontier under the original * TR is generated at some point. */ boolean deadEndComputation; }; /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ typedef struct FsmHdMintSizeStats FsmHdMintSizeStats_t; typedef struct FsmHdStruct FsmHdStruct_t; /**Struct********************************************************************** Synopsis [Enumerated type to specify various quantities in HD] ******************************************************************************/ typedef enum { Fsm_Hd_From, Fsm_Hd_To, Fsm_Hd_FromSubset, Fsm_Hd_Reached } Fsm_Hd_Quant_t; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [Read Minterms of Reached from stats structure] ******************************************************************************/ #define FsmHdStatsReadMintermReached(stats) (stats->mintermReached) /**Struct********************************************************************** Synopsis [Read Minterms of To from stats structure] ******************************************************************************/ #define FsmHdStatsReadMintermTo(stats) (stats->mintermTo) /**Struct********************************************************************** Synopsis [Read Minterms of From from stats structure] ******************************************************************************/ #define FsmHdStatsReadMintermFrom(stats) (stats->mintermFrom) /**Struct********************************************************************** Synopsis [Read Minterms of FromSubset from stats structure] ******************************************************************************/ #define FsmHdStatsReadMintermFromSubset(stats) (stats->mintermFromSubset) /**Struct********************************************************************** Synopsis [Read Size of Reached from stats structure] ******************************************************************************/ #define FsmHdStatsReadSizeReached(stats) (stats->sizeReached) /**Struct********************************************************************** Synopsis [Read Size of To from stats structure] ******************************************************************************/ #define FsmHdStatsReadSizeTo(stats) (stats->sizeTo) /**Struct********************************************************************** Synopsis [Read Size of From from stats structure] ******************************************************************************/ #define FsmHdStatsReadSizeFrom(stats) (stats->sizeFrom) /**Struct********************************************************************** Synopsis [Read Size of FromSubset from stats structure] ******************************************************************************/ #define FsmHdStatsReadSizeFromSubset(stats) (stats->sizeFromSubset) /**Struct********************************************************************** Synopsis [Read Density of From from stats structure] ******************************************************************************/ #define FsmHdStatsReadDensityFrom(stats) \ (FsmHdStatsReadMintermFrom(stats)/FsmHdStatsReadSizeFrom(stats)) /**Struct********************************************************************** Synopsis [Read Density of FromSubset from stats structure] ******************************************************************************/ #define FsmHdStatsReadDensityFromSubset(stats) \ (FsmHdStatsReadMintermFromSubset(stats)/FsmHdStatsReadSizeFromSubset(stats)) /**Struct********************************************************************** Synopsis [Read Density of Reached from stats structure] ******************************************************************************/ #define FsmHdStatsReadDensityReached(stats) \ (FsmHdStatsReadMintermReached(stats)/FsmHdStatsReadSizeReached(stats)) /**Struct********************************************************************** Synopsis [Set Size of From from stats structure] ******************************************************************************/ #define FsmHdStatsSetSizeFrom(stats, value) (stats->sizeFrom = value) /**Struct********************************************************************** Synopsis [Set Minterm of From from stats structure] ******************************************************************************/ #define FsmHdStatsSetMintermFrom(stats, value) (stats->mintermFrom = value) /**Struct********************************************************************** Synopsis [Set Size of FromSubset from stats structure] ******************************************************************************/ #define FsmHdStatsSetSizeFromSubset(stats, value) \ (stats->sizeFromSubset = value) /**Struct********************************************************************** Synopsis [Set Minterm of FromSubset from stats structure] ******************************************************************************/ #define FsmHdStatsSetMintermFromSubset(stats, value) \ (stats->mintermFromSubset = value) /**Struct********************************************************************** Synopsis [Set Size of Reached from stats structure] ******************************************************************************/ #define FsmHdStatsSetSizeReached(stats, value) (stats->sizeReached = value) /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN int FsmArdcCheckInvariant(Fsm_Fsm_t *fsm, array_t *invarStates); EXTERN void FsmArdcPrintOptions(void); EXTERN void FsmArdcPrintOverApproximateReachableStates(Fsm_Fsm_t *fsm); EXTERN void FsmArdcPrintExactReachableStates(Fsm_Fsm_t *fsm); EXTERN void FsmArdcPrintBddOfNode(Fsm_Fsm_t *fsm, mdd_t *node); EXTERN void FsmArdcPrintArrayOfArrayInt(array_t *arrayOfArray); EXTERN boolean FsmGetArdcSetBooleanValue(char *string, boolean defaultValue); EXTERN Fsm_Fairness_t * FsmFsmCreateDefaultFairnessConstraint(Fsm_Fsm_t *fsm); EXTERN boolean FsmFairnessConstraintIsDefault(Fsm_Fairness_t *fairness); EXTERN void FsmFairnessFree(Fsm_Fairness_t *fairness); EXTERN Fsm_Fairness_t * FsmFairnessAlloc(Fsm_Fsm_t *fsm); EXTERN void FsmFairnessAddConjunct(Fsm_Fairness_t *fairness, Ctlp_Formula_t *finallyInf, Ctlp_Formula_t *globallyInf, int i, int j); EXTERN void FsmFsmFairnessInfoUpdate(Fsm_Fsm_t *fsm, mdd_t *states, Fsm_Fairness_t *constraint, array_t *dbgArray); EXTERN void FsmSetReachabilityOnionRings(Fsm_Fsm_t *fsm, array_t *onionRings); EXTERN void FsmSetReachabilityOnionRingsMode(Fsm_Fsm_t *fsm, Fsm_RchType_t value); EXTERN void FsmSetReachabilityOnionRingsUpToDateFlag(Fsm_Fsm_t *fsm, boolean value); EXTERN void FsmSetReachabilityApproxComputationStatus(Fsm_Fsm_t *fsm, Fsm_RchStatus_t value); EXTERN void FsmSetReachabilityOverApproxComputationStatus(Fsm_Fsm_t *fsm, Fsm_Ardc_StatusType_t status); EXTERN Fsm_Ardc_StatusType_t FsmReadReachabilityOverApproxComputationStatus(Fsm_Fsm_t *fsm); EXTERN void FsmSetReachabilityComputationMode(Fsm_Fsm_t *fsm, Fsm_RchType_t value); EXTERN Fsm_RchType_t FsmReadReachabilityComputationMode(Fsm_Fsm_t *fsm); EXTERN void FsmResetReachabilityFields(Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag); EXTERN FsmHdStruct_t * FsmHdStructAlloc(int nvars); EXTERN void FsmHdStructFree(FsmHdStruct_t *hdInfo); EXTERN void FsmGuidedSearchPrintOptions(void); EXTERN FsmHdMintSizeStats_t * FsmHdStatsStructAlloc(void); EXTERN void FsmHdStatsStructFree(FsmHdMintSizeStats_t *stats); EXTERN void FsmHdStatsComputeSizeAndMinterms(mdd_manager *mddManager, mdd_t *f, array_t *varArray, int nvars, Fsm_Hd_Quant_t field, FsmHdMintSizeStats_t *stats); EXTERN void FsmHdStatsReset(FsmHdMintSizeStats_t *stats, Fsm_Hd_Quant_t field); EXTERN void FsmHdPrintOptions(void); EXTERN mdd_t * FsmHdDeadEnd(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t *reachableStates, FsmHdStruct_t *hdInfo, array_t *varArray, int greedy, int verbosity); EXTERN void FsmHdFromComputeDenseSubset(mdd_manager *mddManager, mdd_t **fromLowerBound, mdd_t **fromUpperBound, mdd_t **reachableStates, mdd_t **image, mdd_t *initialStates, FsmHdStruct_t *hdInfo, int shellFlag, array_t *onionRings, int sizeOfOnionRings, array_t *varArray); /**AutomaticEnd***************************************************************/ #endif /* _FSMINT */