/**CHeaderFile***************************************************************** FileName [imcInt.h] PackageName [imc] Synopsis [Internal data type definitions and macros to handle the structures of the imc package.] Author [Jae-Young Jang ] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] Revision [$Id:] ******************************************************************************/ #ifndef _IMCINT #define _IMCINT /*---------------------------------------------------------------------------*/ /* Nested includes */ /*---------------------------------------------------------------------------*/ #include "imc.h" #include "fsm.h" #include /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [Information for a total system.] Description [Information for a total system.] SeeAlso [ImcInfoStruct] ******************************************************************************/ struct ImcSystemInfo{ st_table *latchNameTable; /* Names of latches in a system */ array_t *latchNameArray; array_t *latchNodeArray; array_t *nsMddIdArray; array_t *psMddIdArray; array_t *inputMddIdArray; array_t *TRArray; array_t *lowerTRArray; array_t *mvfArray; array_t *latchSizeArray; st_table *nsMddIdToIndex; st_table *psMddIdToIndex; array_t *includedPsMddId; array_t *includedNsMddId; array_t *includedLatchIndex; array_t *excludedPsMddId; array_t *excludedNsMddId; array_t *excludedLatchIndex; st_table *excludedPsMddIdTable; }; /**Struct********************************************************************** Synopsis [Information for an upper-bound approximate system.] Description [Information for an upper-bound approximate system.] SeeAlso [ImcInfoStruct] ******************************************************************************/ struct ImcUpperSystemInfo{ Imc_SystemInfo_t *systemInfo; mdd_t *careStates; array_t *fwdRealationArray; array_t *fwdSmoothVarsArray; array_t *bwdRealationArray; array_t *bwdMinimizedRealationArray; array_t *bwdSmoothVarsArray; }; /**Struct********************************************************************** Synopsis [Information for an upper-bound approximate system.] Description [Information for an upper-bound approximate system.] SeeAlso [ImcInfoStruct] ******************************************************************************/ struct ImcLowerSystemInfo{ Imc_SystemInfo_t *systemInfo; mdd_t *careStates; array_t *bwdRealationArray; array_t *bwdMinimizedRealationArray; array_t *bwdSmoothVarsArray; }; /**Struct********************************************************************** Synopsis [Information for nodes in opeerational graph.] Description [Information for nodes in opeerational graph.] SeeAlso [ImcInfoStruct] ******************************************************************************/ struct ImcNodeInfo{ boolean polarity; boolean isExact; mdd_t *upperSat; /* upper satisfying set */ mdd_t *lowerSat; /* lower satisfying set */ boolean upperDone; boolean lowerDone; mdd_t *propagatedGoalSet; mdd_t *propagatedGoalSetTrue; mdd_t *goalSet; mdd_t *goalSetTrue; mdd_t *pseudoEdges; Imc_VerificationResult answer; }; /**Struct********************************************************************** Synopsis [Information regarding the imc package.] Description [This is a higher level of information related to the imc verification.] SeeAlso [ImcSubsystemInfo] ******************************************************************************/ struct ImcInfoStruct{ /* General Info */ Ntk_Network_t *network; /* Corresponding network */ Fsm_Fsm_t *globalFsm; /* Global FSM */ boolean useLocalFsm; Imc_DcLevel dcLevel; /* Don't care level */ mdd_t *initialStates; /* Initial states */ Ctlp_FormulaClass formulaClass; /* ECTL, ACTL, MIXED, QuantifierFree */ mdd_t *modelCareStates; /* Global care states */ Imc_VerbosityLevel verbosity; /* Verbosity */ Imc_RefineMethod refine; /* Refinement method */ Imc_VerificationResult result; /* Verification Result */ mdd_manager *mddMgr; /* MDD Manager */ Imc_PartMethod partMethod; char *modelName; Hrc_Node_t *currentNode; /* Image, Preimage computation Info */ array_t *supportMddIdArray; /* don't free */ array_t *preQMddIdArray; /* don't free */ array_t *imgQMddIdArray; /* don't free */ /* Operational graph Info */ Imc_GraphType graphType; /* pDOG, nDOG, MOG */ st_table *nodeInfoTable; /* node info table */ boolean needLower; boolean needUpper; /* Incremental Verification dependent info */ Imc_SystemInfo_t *systemInfo; /* System info of total system */ int incrementalSize; /* Number of transition sub-relations to be refined at each refinement */ /* approximation and Dynamic Refinement dependent Info */ Imc_LowerMethod lowerMethod; /* Lower-bound approximation method */ Imc_UpperMethod upperMethod; /* Upper-bound approximation method */ Imc_UpperSystemInfo_t *upperSystemInfo; /* Upper-bound approximate system */ Imc_LowerSystemInfo_t *lowerSystemInfo; /* Lower-bound approximate system */ mdd_t *edges; /* for edge traversal refinement */ /* approximation and Static Refinement dependent Info */ Part_CMethod correlationMethod; array_t *staticRefineSchedule; /* Static refinement schedule */ }; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN array_t * ImcCreateScheduleArray(Ntk_Network_t *network, Ctlp_Formula_t *formula, boolean dynamicIncrease, Imc_RefineMethod refine, int verbosity, int incrementalSize, Part_CMethod correlationMethod); EXTERN int ImcModelCheckAtomicFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula); EXTERN int ImcModelCheckTrueFalseFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isTrue); EXTERN int ImcModelCheckNotFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper); EXTERN int ImcModelCheckAndFormula(Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper); EXTERN void ImcPrintLatchInApproxSystem(Imc_Info_t *imcInfo); EXTERN void ImcNodeInfoTableFree(st_table *nodeInfoTable); /**AutomaticEnd***************************************************************/ #endif /* _IMCINT */