/**CFile*********************************************************************** FileName [imcImc.c] PackageName [imc] Synopsis [Incremental Model Checker.] 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.] ******************************************************************************/ #include "imcInt.h" #include "part.h" #include "img.h" #include "ntm.h" static char rcsid[] UNUSED = "$Id: imcImc.c,v 1.21 2005/04/27 00:13:01 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static int stringCompare(const void * s1, const void * s2); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Verify a formula with incremental refinement.] Description [Verify a formula with incremental refinement.] SideEffects [] SeeAlso [] ******************************************************************************/ Imc_VerificationResult Imc_ImcEvaluateFormulaLinearRefine( Ntk_Network_t *network, Ctlp_Formula_t *orgFormula, Ctlp_Formula_t *formula, Ctlp_FormulaClass formulaClass, int incrementalSize, Imc_VerbosityLevel verbosity, Imc_RefineMethod refine, mdd_t *careStates, Fsm_Fsm_t *exactFsm, Imc_DcLevel dcLevel, Imc_GraphType graphType, Imc_LowerMethod lowerMethod, Imc_UpperMethod upperMethod, boolean computeExact, boolean needLower, boolean needUpper, Imc_PartMethod partMethod, Hrc_Node_t *currentNode, char *modelName) { Imc_Info_t *imcInfo; st_table *latchNameTable; int numberOfLatches, numberOfIncludedLatches; int iterationCount; Imc_VerificationResult verification = Imc_VerificationError_c; /* * Initialize data structures. */ imcInfo = Imc_ImcInfoInitialize(network, formula, formulaClass, verbosity, refine, careStates, dcLevel, incrementalSize, graphType, exactFsm, lowerMethod, upperMethod, computeExact, needLower, needUpper, partMethod, currentNode, modelName); if (imcInfo == NIL(Imc_Info_t))return(Imc_VerificationError_c); /* FIXED */ numberOfLatches = array_n(imcInfo->systemInfo->latchNameArray); iterationCount = 1; numberOfIncludedLatches = array_n(imcInfo->systemInfo->includedLatchIndex); if (verbosity != Imc_VerbosityNone_c) { fprintf(vis_stdout, "IMC : Reduced system has "); Imc_ImcPrintSystemSize(imcInfo); } if(verbosity != Imc_VerbosityNone_c) { fprintf(vis_stdout, "IMC : Approximate system has "); Imc_ImcPrintApproxSystemSize(imcInfo); } assert(numberOfLatches >= numberOfIncludedLatches); while(numberOfLatches >= numberOfIncludedLatches) { /* * verification is one of {Imc_VerificationTrue_c, Imc_VerificationFalse_c, * Imc_VerificationInconclusive_c}. */ verification = Imc_ImcVerifyFormula(imcInfo, formula); if (verification == Imc_VerificationError_c) { (void)fprintf(vis_stdout, "# IMC: formula inconclusive.\n"); /* Free all */ Imc_ImcInfoFree(imcInfo); return verification; }else if (verification != Imc_VerificationInconclusive_c){ if ((verification == Imc_VerificationTrue_c)) { (void) fprintf(vis_stdout, "# IMC: formula passed.\n"); }else{ (void) fprintf(vis_stdout, "# IMC: formula failed.\n"); } fprintf(vis_stdout, "IMC : "); Ctlp_FormulaPrint( vis_stdout, orgFormula ); fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "IMC : "); Ctlp_FormulaPrint( vis_stdout, formula); fprintf(vis_stdout, "\n"); Imc_ImcInfoFree(imcInfo); return verification; }else{ if (numberOfLatches == numberOfIncludedLatches){ if (imcInfo->graphType == Imc_GraphPDOG_c){ (void) fprintf(vis_stdout, "# IMC: formula passed.\n"); }else if (imcInfo->graphType == Imc_GraphNDOG_c){ (void) fprintf(vis_stdout, "# IMC: formula failed.\n"); } fprintf(vis_stdout, "IMC : "); Ctlp_FormulaPrint( vis_stdout,orgFormula); fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "IMC : "); Ctlp_FormulaPrint( vis_stdout, formula); fprintf(vis_stdout, "\n"); Imc_ImcInfoFree(imcInfo); return verification; } } latchNameTable = array_fetch(st_table *, imcInfo->staticRefineSchedule, iterationCount); Imc_ImcSystemInfoUpdate(imcInfo, latchNameTable); /* * Refine the approximate system. */ if (imcInfo->needUpper){ Imc_UpperSystemInfoFree(imcInfo->upperSystemInfo); Imc_UpperSystemInfoInitialize(imcInfo, latchNameTable); } if (imcInfo->needLower){ Imc_LowerSystemInfoFree(imcInfo->lowerSystemInfo); Imc_LowerSystemInfoInitialize(imcInfo, latchNameTable); } Imc_NodeInfoReset(imcInfo); numberOfIncludedLatches = array_n(imcInfo->systemInfo->includedLatchIndex); iterationCount++; if(verbosity != Imc_VerbosityNone_c) { fprintf(vis_stdout, "IMC : Approximate system has "); Imc_ImcPrintApproxSystemSize(imcInfo); } } /* end of while(numberOfLatches >= numberOfIncludedLatches) */ return(verification); /* FIXED */ } /**Function******************************************************************** Synopsis [Verify a formula.] Description [Verify a formula.] SideEffects [] SeeAlso [] ******************************************************************************/ Imc_VerificationResult Imc_ImcVerifyFormula( Imc_Info_t *imcInfo, Ctlp_Formula_t *formula) { Imc_VerificationResult result; if (!Imc_ImcEvaluateCTLFormula(imcInfo, formula, Imc_PolarityPos_c)){ return Imc_VerificationError_c; } result = Imc_SatCheck(imcInfo, formula); return result; } /**Function******************************************************************** Synopsis [Check if a formula is true or false.] Description [Check if a formula is true or false. If all initial states are contained in a lowerbound satisfying states, a formula is true. If any of initial states is not contained by a upperbound satisfying states, a formula is false. Otherwise, inconclusive.] SideEffects [] SeeAlso [] ******************************************************************************/ Imc_VerificationResult Imc_SatCheck( Imc_Info_t *imcInfo, Ctlp_Formula_t *formula) { mdd_t *initialStates = imcInfo->initialStates; Imc_NodeInfo_t *nodeInfo; if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){ return Imc_VerificationError_c; /* FIXED */ } if (nodeInfo->lowerSat != NIL(mdd_t)){ if (mdd_lequal(initialStates, nodeInfo->lowerSat, 1, 1)){ return Imc_VerificationTrue_c; } } if (nodeInfo->upperSat != NIL(mdd_t)){ if (!mdd_lequal_mod_care_set(initialStates, nodeInfo->upperSat, 1, 1, imcInfo->modelCareStates)){ /* FIXED */ return Imc_VerificationFalse_c; } } return Imc_VerificationInconclusive_c; } /**Function******************************************************************** Synopsis [Initializes an imcInfo structure for the given method.] Description [Regardless of the method type, the initialization procedure starts from constructing set of subsystems. A subsystem contains a subset of vertices of the partition. Based on the subset of vertices, subFSM is created. The subsystems are stored as an array. After the creation of the subsystem array, the function initializes remaining field of (Imc_Info_t *) imcInfo. The function returns initialized (Imc_Info_t *) imcInfo.] SideEffects [] SeeAlso [] ******************************************************************************/ Imc_Info_t * Imc_ImcInfoInitialize( Ntk_Network_t *network, Ctlp_Formula_t *formula, Ctlp_FormulaClass formulaClass, Imc_VerbosityLevel verbosity, Imc_RefineMethod refine, mdd_t *careStates, Imc_DcLevel dcLevel, int incrementalSize, Imc_GraphType graphType, Fsm_Fsm_t *exactFsm, Imc_LowerMethod lowerMethod, Imc_UpperMethod upperMethod, boolean computeExact, boolean needLower, boolean needUpper, Imc_PartMethod partMethod, Hrc_Node_t *currentNode, char *modelName) { int i; char *flagValue; Imc_Info_t *imcInfo; mdd_t *initialStates; array_t *scheduleArray; st_table *latchNameTable; st_table *newLatchNameTable; st_table *globalLatchNameTable; array_t *psMddIdArray; array_t *nsMddIdArray; array_t *inputMddIdArray; array_t *supportMddIdArray; array_t *preQMddIdArray; array_t *imgQMddIdArray; Part_CMethod correlationMethod; Ntk_Node_t *latch, *input; lsGen gen; array_t *latchNameArray; imcInfo = ALLOC(Imc_Info_t, 1); /* * Initialize */ imcInfo->network = network; imcInfo->globalFsm = exactFsm; imcInfo->formulaClass = formulaClass; imcInfo->incrementalSize = incrementalSize; imcInfo->dcLevel = dcLevel; imcInfo->refine = refine; imcInfo->verbosity = verbosity; imcInfo->upperSystemInfo = NIL(Imc_UpperSystemInfo_t); imcInfo->lowerSystemInfo = NIL(Imc_LowerSystemInfo_t); imcInfo->initialStates = NIL(mdd_t); imcInfo->nodeInfoTable = NIL(st_table); imcInfo->graphType = graphType; imcInfo->nodeInfoTable = st_init_table(st_ptrcmp , st_ptrhash); imcInfo->mddMgr = Ntk_NetworkReadMddManager(network); imcInfo->lowerMethod = lowerMethod; imcInfo->upperMethod = upperMethod; imcInfo->currentNode = currentNode; imcInfo->modelName = modelName; if (exactFsm == NIL(Fsm_Fsm_t)){ imcInfo->useLocalFsm = TRUE; }else{ imcInfo->useLocalFsm = FALSE; } /* * Initialize image and preimage computation info. */ if (exactFsm != NIL(Fsm_Fsm_t)){ psMddIdArray = array_dup(Fsm_FsmReadPresentStateVars(exactFsm)); nsMddIdArray = array_dup(Fsm_FsmReadNextStateVars(exactFsm)); inputMddIdArray = array_dup(Fsm_FsmReadInputVars(exactFsm)); }else{ latchNameArray = array_alloc(char *, 0); psMddIdArray = array_alloc(int, 0); nsMddIdArray = array_alloc(int, 0); inputMddIdArray = array_alloc(int, 0); /* sort by name of latch */ Ntk_NetworkForEachLatch(network, gen, latch){ array_insert_last(char*, latchNameArray, Ntk_NodeReadName(latch)); } array_sort(latchNameArray, stringCompare); for (i = 0; i < array_n(latchNameArray); i++) { char *nodeName; nodeName = array_fetch(char *, latchNameArray, i); latch = Ntk_NetworkFindNodeByName(network, nodeName); array_insert_last(int, psMddIdArray, Ntk_NodeReadMddId(latch)); array_insert_last(int, nsMddIdArray, Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch))); } array_free(latchNameArray); Ntk_NetworkForEachInput(network, gen, input){ array_insert_last(int, inputMddIdArray, Ntk_NodeReadMddId(input)); } } imgQMddIdArray = array_dup(psMddIdArray); array_append(imgQMddIdArray,inputMddIdArray); supportMddIdArray = array_dup(imgQMddIdArray); array_append(supportMddIdArray,nsMddIdArray); preQMddIdArray = array_dup(nsMddIdArray); array_append(preQMddIdArray,inputMddIdArray); array_free(psMddIdArray); array_free(nsMddIdArray); array_free(inputMddIdArray); imcInfo->supportMddIdArray = supportMddIdArray; imcInfo->imgQMddIdArray = imgQMddIdArray; imcInfo->preQMddIdArray = preQMddIdArray; imcInfo->needLower = needLower; imcInfo->needUpper = needUpper; imcInfo->partMethod = partMethod; if (careStates == NIL(mdd_t)){ imcInfo->modelCareStates = mdd_one(imcInfo->mddMgr); }else{ imcInfo->modelCareStates = mdd_dup(careStates); } /* * If refine oprion is Imc_RefineLatchRelation_c, * correlation method should be defined. */ flagValue = Cmd_FlagReadByName("part_group_correlation_method"); if(flagValue == NIL(char)){ correlationMethod = Part_CorrelationWithBDD; }else if (strcmp(flagValue, "support") == 0){ correlationMethod = Part_CorrelationWithSupport; }else if (strcmp(flagValue, "mdd") == 0){ correlationMethod = Part_CorrelationWithBDD; }else{ correlationMethod = Part_CorrelationWithSupport; } if ((refine == Imc_RefineLatchRelation_c) && (correlationMethod == Part_CorrelationWithBDD) && (partMethod == Imc_PartInc_c)){ correlationMethod = Part_CorrelationWithSupport; } imcInfo->correlationMethod = correlationMethod; if (computeExact){ scheduleArray = ImcCreateScheduleArray(network, formula, TRUE, Imc_RefineLatchRelation_c, verbosity, incrementalSize, correlationMethod); imcInfo->staticRefineSchedule = NIL(array_t); latchNameTable = array_fetch(st_table *, scheduleArray, 0); st_free_table(latchNameTable); latchNameTable = array_fetch(st_table *, scheduleArray, 1); newLatchNameTable = st_copy(latchNameTable); array_insert(st_table *, scheduleArray, 0, newLatchNameTable); }else if (refine == Imc_RefineLatchRelation_c){ scheduleArray = ImcCreateScheduleArray(network, formula, FALSE, refine, verbosity, incrementalSize, correlationMethod); imcInfo->staticRefineSchedule = scheduleArray; }else if (refine == Imc_RefineSort_c){ scheduleArray = ImcCreateScheduleArray(network, formula, TRUE, refine, verbosity, incrementalSize, correlationMethod); imcInfo->staticRefineSchedule = scheduleArray; }else{ fprintf(vis_stdout, "** imc error: Unkown refinement method.\n"); Imc_ImcInfoFree(imcInfo); return NIL(Imc_Info_t); } if (scheduleArray == NIL(array_t)){ fprintf(vis_stdout, "** imc error: Can't get an initial system.\n"); Imc_ImcInfoFree(imcInfo); return NIL(Imc_Info_t); } globalLatchNameTable = array_fetch(st_table *, scheduleArray, array_n(scheduleArray)-1); latchNameTable = array_fetch(st_table *, scheduleArray, 0); /* * Initialize a total system info. */ Imc_SystemInfoInitialize(imcInfo, globalLatchNameTable, latchNameTable); /* * Initialize an initial approximate system info. */ if (needUpper){ Imc_UpperSystemInfoInitialize(imcInfo,latchNameTable); } if (needLower){ Imc_LowerSystemInfoInitialize(imcInfo,latchNameTable); } initialStates = Fsm_FsmComputeInitialStates(imcInfo->globalFsm); if (initialStates == NIL(mdd_t)){ fprintf(vis_stdout,"** imc error : System has no initial state.\n"); Imc_ImcInfoFree(imcInfo); return NIL(Imc_Info_t); } imcInfo->initialStates = initialStates; if (computeExact){ arrayForEachItem(st_table *, scheduleArray, i, latchNameTable){ st_free_table(latchNameTable); } array_free(scheduleArray); } return(imcInfo); } /**Function******************************************************************** Synopsis [Free an imcInfo structure for the given method.] Description [Free an imcInfo structure for the given method.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_ImcInfoFree( Imc_Info_t *imcInfo) { int i; st_table *latchNameTable; Imc_UpperSystemInfoFree(imcInfo->upperSystemInfo); Imc_LowerSystemInfoFree(imcInfo->lowerSystemInfo); ImcNodeInfoTableFree(imcInfo->nodeInfoTable); if (imcInfo->initialStates != NIL(mdd_t)) mdd_free(imcInfo->initialStates); if (imcInfo->modelCareStates!=NIL(mdd_t)) mdd_free(imcInfo->modelCareStates); if (imcInfo->staticRefineSchedule != NIL(array_t)){ arrayForEachItem(st_table *,imcInfo->staticRefineSchedule, i, latchNameTable){ st_free_table(latchNameTable); } array_free(imcInfo->staticRefineSchedule); } if (imcInfo->supportMddIdArray != NIL(array_t)) array_free(imcInfo->supportMddIdArray); if (imcInfo->imgQMddIdArray != NIL(array_t)) array_free(imcInfo->imgQMddIdArray); if (imcInfo->preQMddIdArray != NIL(array_t)) array_free(imcInfo->preQMddIdArray); if ((imcInfo->useLocalFsm) && (imcInfo->globalFsm != NIL(Fsm_Fsm_t))){ Fsm_FsmSubsystemFree(imcInfo->globalFsm); } Imc_SystemInfoFree(imcInfo->systemInfo); FREE(imcInfo); } /**Function******************************************************************** Synopsis [Initilalize a system info.] Description [Initilalize a system info.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_SystemInfoInitialize( Imc_Info_t *imcInfo, st_table *globalLatchNameTable, st_table *initialLatchNameTable) { int i, psMddId, nsMddId, latchSize; char *name, *dataInputName; Ntk_Node_t *node, *latchInput; Ntk_Network_t *network = imcInfo->network; graph_t *partition = Part_NetworkReadPartition(network); vertex_t *vertex; Mvf_Function_t *mvf; mdd_t *singleTR, *subTR, *tempMdd; st_generator *stGen; lsList latchInputList; lsGen gen; st_table *partNameTable; Imc_SystemInfo_t *systemInfo; array_t *bddIdArray; array_t *latchNameArray = array_alloc(char *, st_count(globalLatchNameTable)); st_table *latchNameTable = st_init_table(strcmp, st_strhash ); st_table *latchInputTable = st_init_table(st_ptrcmp, st_ptrhash ); st_table *nsMddIdToIndex = st_init_table(st_numcmp, st_numhash); st_table *psMddIdToIndex = st_init_table(st_numcmp, st_numhash); array_t *latchNodeArray = array_alloc(Ntk_Node_t *, st_count(globalLatchNameTable)); array_t *nsMddIdArray = array_alloc(int,st_count(globalLatchNameTable)); array_t *psMddIdArray = array_alloc(int,st_count(globalLatchNameTable)); array_t *TRArray = array_alloc(mdd_t *,st_count(globalLatchNameTable)); array_t *lowerTRArray = array_alloc(mdd_t *,st_count(globalLatchNameTable)); array_t *mvfArray = array_alloc(mdd_t *,st_count(globalLatchNameTable)); array_t *latchSizeArray = array_alloc(int,st_count(globalLatchNameTable)); array_t *includedLatchIndex = array_alloc(int, 0); array_t *includedNsMddId = array_alloc(int, 0); array_t *excludedLatchIndex = array_alloc(int, 0); array_t *excludedNsMddId = array_alloc(int, 0); array_t *excludedPsMddId = array_alloc(int, 0); array_t *includedPsMddId = array_alloc(int, 0); st_table *excludedPsMddIdTable = st_init_table(st_numcmp, st_numhash); systemInfo = ALLOC(Imc_SystemInfo_t, 1); st_foreach_item(globalLatchNameTable, stGen, &name, NIL(char *)){ array_insert_last(char *, latchNameArray, name); } array_sort(latchNameArray, stringCompare); if (partition == NIL(graph_t)){ if ((imcInfo->partMethod == Imc_PartInc_c) && !((imcInfo->needLower) && (imcInfo->lowerMethod != Imc_LowerUniversalQuantification_c))){ partNameTable = initialLatchNameTable; }else{ partNameTable = globalLatchNameTable; } st_foreach_item(partNameTable, stGen, &name, NIL(char *)){ node = Ntk_NetworkFindNodeByName(network, name); latchInput = Ntk_LatchReadDataInput(node); st_insert(latchInputTable, (char *)latchInput, (char *)(long)(-1)); } latchInputList = lsCreate(); st_foreach_item(latchInputTable, stGen, &node, NULL){ lsNewEnd(latchInputList, (lsGeneric)node, LS_NH); } st_free_table(latchInputTable); Ntk_NetworkForEachCombOutput(network, gen, node){ if (Ntk_NodeTestIsLatchInitialInput(node)){ lsNewEnd(latchInputList, (lsGeneric)node, LS_NH); } } partition = Part_NetworkCreatePartition(network, imcInfo->currentNode, imcInfo->modelName, latchInputList, (lsList)0, NIL(mdd_t), Part_InOut_c, (lsList)0, FALSE, 0, 0); lsDestroy(latchInputList, (void (*)(lsGeneric))0); Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY, (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback, (void *) partition); imcInfo->globalFsm = Fsm_FsmCreateSubsystemFromNetwork(network,partition, partNameTable, FALSE, 0); imcInfo->useLocalFsm = TRUE; }else{ st_foreach_item(initialLatchNameTable, stGen, &name, NIL(char *)){ node = Ntk_NetworkFindNodeByName(network, name); latchInput = Ntk_LatchReadDataInput(node); st_insert(latchInputTable, (char *)latchInput, (char *)(long)(-1)); } latchInputList = lsCreate(); st_foreach_item(latchInputTable, stGen, &node, NIL(char *)){ lsNewEnd(latchInputList, (lsGeneric)node, LS_NH); } st_free_table(latchInputTable); Ntk_NetworkForEachCombOutput(network, gen, node){ if (Ntk_NodeTestIsLatchInitialInput(node)){ lsNewEnd(latchInputList, (lsGeneric)node, LS_NH); } } (void) Part_PartitionChangeRoots(network, partition, latchInputList, 0); lsDestroy(latchInputList, (void (*)(lsGeneric))0); } for (i=0;imodelCareStates)); array_insert(mdd_t *, lowerTRArray, i, NIL(mdd_t)); array_insert(Mvf_Function_t *, mvfArray, i, NIL(Mvf_Function_t)); mdd_free(singleTR); }else{ array_insert(Mvf_Function_t *, mvfArray, i, NIL(Mvf_Function_t)); array_insert(mdd_t *, lowerTRArray, i, NIL(mdd_t)); array_insert(mdd_t *, TRArray, i, NIL(mdd_t)); } if (!st_is_member(initialLatchNameTable, name)){ if (imcInfo->needLower && imcInfo->lowerMethod != Imc_LowerUniversalQuantification_c){ singleTR = array_fetch(mdd_t *, TRArray, i); if (singleTR == NIL(mdd_t)){ vertex = Part_PartitionFindVertexByName(partition, dataInputName); mvf = Part_VertexReadFunction(vertex); singleTR = Mvf_FunctionBuildRelationWithVariable(mvf, nsMddId); tempMdd = mdd_and(singleTR, imcInfo->modelCareStates, 1, 1); mdd_free(singleTR); }else{ tempMdd = mdd_and(singleTR, imcInfo->modelCareStates, 1, 1); } subTR = bdd_approx_remap_ua(tempMdd,(bdd_approx_dir_t)BDD_UNDER_APPROX, array_n(imcInfo->supportMddIdArray), 0, 1.0); mdd_free(tempMdd); tempMdd = bdd_minimize(subTR, imcInfo->modelCareStates); mdd_free(subTR); subTR = tempMdd; array_insert(mdd_t *, lowerTRArray, i, subTR); array_insert(Mvf_Function_t *, mvfArray, i, NIL(Mvf_Function_t)); } } if (st_is_member(initialLatchNameTable, name)){ array_insert_last(int, includedLatchIndex, i); array_insert_last(int, includedNsMddId, nsMddId); array_insert_last(int, includedPsMddId, psMddId); }else{ array_insert_last(int, excludedLatchIndex, i); array_insert_last(int, excludedNsMddId, nsMddId); array_insert_last(int, excludedPsMddId, psMddId); st_insert(excludedPsMddIdTable, (char *)(long)psMddId, (char *)0); } bddIdArray = mdd_id_to_bdd_id_array(imcInfo->mddMgr, nsMddId); latchSize = array_n(bddIdArray); array_free(bddIdArray); st_insert(latchNameTable, name, (char *)(long)i); st_insert(nsMddIdToIndex,(char *)(long)nsMddId, (char *)(long)i); st_insert(psMddIdToIndex,(char *)(long)psMddId, (char *)(long)i); array_insert(Ntk_Node_t *, latchNodeArray, i, node); array_insert(int, latchSizeArray, i, latchSize); array_insert(int, nsMddIdArray, i, nsMddId); array_insert(int, psMddIdArray, i, psMddId); } systemInfo->latchNameTable = latchNameTable; systemInfo->latchNameArray = latchNameArray; systemInfo->latchNodeArray = latchNodeArray; systemInfo->nsMddIdArray = nsMddIdArray; systemInfo->psMddIdArray = psMddIdArray; systemInfo->inputMddIdArray = array_dup(Fsm_FsmReadInputVars(imcInfo->globalFsm)); systemInfo->TRArray = TRArray; systemInfo->lowerTRArray = lowerTRArray; systemInfo->mvfArray = mvfArray; systemInfo->latchSizeArray = latchSizeArray; systemInfo->nsMddIdToIndex = nsMddIdToIndex; systemInfo->psMddIdToIndex = psMddIdToIndex; systemInfo->excludedLatchIndex = excludedLatchIndex; systemInfo->includedLatchIndex = includedLatchIndex; systemInfo->excludedNsMddId = excludedNsMddId; systemInfo->includedNsMddId = includedNsMddId; systemInfo->excludedPsMddId = excludedPsMddId; systemInfo->includedPsMddId = includedPsMddId; systemInfo->excludedPsMddIdTable = excludedPsMddIdTable; imcInfo->systemInfo = systemInfo; } /**Function******************************************************************** Synopsis [Free a system info.] Description [Free a system info.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_SystemInfoFree( Imc_SystemInfo_t *systemInfo) { int i; mdd_t *singleTR; if (systemInfo->latchNameTable != NIL(st_table)) st_free_table(systemInfo->latchNameTable); if (systemInfo->latchNameArray != NIL(array_t)) array_free(systemInfo->latchNameArray); if (systemInfo->latchNodeArray != NIL(array_t)) array_free(systemInfo->latchNodeArray); if (systemInfo->nsMddIdArray != NIL(array_t)) array_free(systemInfo->nsMddIdArray); if (systemInfo->psMddIdArray != NIL(array_t)) array_free(systemInfo->psMddIdArray); if (systemInfo->inputMddIdArray != NIL(array_t)) array_free(systemInfo->inputMddIdArray); if (systemInfo->TRArray != NIL(array_t)){ for(i=0;iTRArray);i++){ singleTR = array_fetch(mdd_t *, systemInfo->TRArray, i); if (singleTR != NIL(mdd_t)){ mdd_free(singleTR); } } array_free(systemInfo->TRArray); } if (systemInfo->lowerTRArray != NIL(array_t)){ for(i=0;ilowerTRArray);i++){ singleTR = array_fetch(mdd_t *, systemInfo->lowerTRArray, i); if (singleTR != NIL(mdd_t)){ mdd_free(singleTR); } } array_free(systemInfo->lowerTRArray); } if (systemInfo->mvfArray != NIL(array_t)) array_free(systemInfo->mvfArray); if (systemInfo->latchSizeArray != NIL(array_t)) array_free(systemInfo->latchSizeArray); if (systemInfo->nsMddIdToIndex != NIL(st_table)) st_free_table(systemInfo->nsMddIdToIndex); if (systemInfo->psMddIdToIndex != NIL(st_table)) st_free_table(systemInfo->psMddIdToIndex); if (systemInfo->excludedLatchIndex != NIL(array_t)) array_free(systemInfo->excludedLatchIndex); if (systemInfo->includedLatchIndex != NIL(array_t)) array_free(systemInfo->includedLatchIndex); if (systemInfo->excludedNsMddId != NIL(array_t)) array_free(systemInfo->excludedNsMddId); if (systemInfo->includedNsMddId != NIL(array_t)) array_free(systemInfo->includedNsMddId); if (systemInfo->excludedPsMddId != NIL(array_t)) array_free(systemInfo->excludedPsMddId); if (systemInfo->includedPsMddId != NIL(array_t)) array_free(systemInfo->includedPsMddId); if (systemInfo->excludedPsMddIdTable != NIL(st_table)) st_free_table(systemInfo->excludedPsMddIdTable); FREE(systemInfo); } /**Function******************************************************************** Synopsis [Update a system info.] Description [Update a system info. All variables in newLatchNameTable are now computed exactly.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_ImcSystemInfoUpdate( Imc_Info_t *imcInfo, st_table *newLatchNameTable) { int i, nsMddId, psMddId, index; char *name, *dataInputName; mdd_t *singleTR; st_generator *stGen; Ntk_Node_t *node, *latchInput; Mvf_Function_t *mvf; vertex_t *vertex; lsList latchInputList; lsGen gen; graph_t *partition = Part_NetworkReadPartition(imcInfo->network); st_table *latchInputTable; Imc_SystemInfo_t *systemInfo = imcInfo->systemInfo; if ((imcInfo->partMethod == Imc_PartInc_c) && !(imcInfo->needLower && imcInfo->lowerMethod != Imc_LowerUniversalQuantification_c)){ latchInputTable = st_init_table(st_ptrcmp, st_ptrhash ); st_foreach_item(newLatchNameTable, stGen, &name, NIL(char *)){ node = Ntk_NetworkFindNodeByName(imcInfo->network, name); latchInput = Ntk_LatchReadDataInput(node); st_insert(latchInputTable, (char *)latchInput, (char *)(long)(-1)); } latchInputList = lsCreate(); st_foreach_item(latchInputTable, stGen, &node, NULL){ lsNewEnd(latchInputList, (lsGeneric)node, LS_NH); } st_free_table(latchInputTable); Ntk_NetworkForEachCombOutput(imcInfo->network, gen, node){ if (Ntk_NodeTestIsLatchInitialInput(node)){ lsNewEnd(latchInputList, (lsGeneric)node, LS_NH); } } (void) Part_PartitionChangeRoots(imcInfo->network, partition, latchInputList, 0); lsDestroy(latchInputList, (void (*)(lsGeneric))0); } if (systemInfo->excludedLatchIndex != NIL(array_t)){ array_free(systemInfo->excludedLatchIndex); systemInfo->excludedLatchIndex = array_alloc(int, 0); } if (systemInfo->includedLatchIndex != NIL(array_t)){ array_free(systemInfo->includedLatchIndex); systemInfo->includedLatchIndex = array_alloc(int, 0); } if (systemInfo->excludedNsMddId != NIL(array_t)){ array_free(systemInfo->excludedNsMddId); systemInfo->excludedNsMddId = array_alloc(int, 0); } if (systemInfo->includedNsMddId != NIL(array_t)){ array_free(systemInfo->includedNsMddId); systemInfo->includedNsMddId = array_alloc(int, 0); } if (systemInfo->excludedPsMddId != NIL(array_t)){ array_free(systemInfo->excludedPsMddId); systemInfo->excludedPsMddId = array_alloc(int, 0); } if (systemInfo->includedPsMddId != NIL(array_t)){ array_free(systemInfo->includedPsMddId); systemInfo->includedPsMddId = array_alloc(int, 0); } if (systemInfo->excludedPsMddIdTable != NIL(st_table)){ st_free_table(systemInfo->excludedPsMddIdTable); systemInfo->excludedPsMddIdTable = st_init_table(st_numcmp, st_numhash); } for(i=0;isystemInfo->latchNameArray);i++){ name = array_fetch(char *,imcInfo->systemInfo->latchNameArray,i); node = Ntk_NetworkFindNodeByName(imcInfo->network, name); psMddId = Ntk_NodeReadMddId(node); nsMddId = Ntk_NodeReadMddId(Ntk_NodeReadShadow(node)); if (st_is_member(newLatchNameTable, name)){ array_insert_last(int, systemInfo->includedLatchIndex, i); array_insert_last(int, systemInfo->includedNsMddId, nsMddId); array_insert_last(int, systemInfo->includedPsMddId, psMddId); }else{ array_insert_last(int, systemInfo->excludedLatchIndex, i); array_insert_last(int, systemInfo->excludedNsMddId, nsMddId); array_insert_last(int, systemInfo->excludedPsMddId, psMddId); st_insert(systemInfo->excludedPsMddIdTable, (char *)(long)psMddId, (char *)0); } } st_foreach_item(newLatchNameTable, stGen, &name, NIL(char *)){ st_lookup_int(imcInfo->systemInfo->latchNameTable,name, &index); nsMddId = array_fetch(int, imcInfo->systemInfo->nsMddIdArray, index); psMddId = array_fetch(int, imcInfo->systemInfo->psMddIdArray, index); mvf = array_fetch(Mvf_Function_t *, imcInfo->systemInfo->mvfArray, index); if (mvf == NIL(Mvf_Function_t)){ node = Ntk_NetworkFindNodeByName(imcInfo->network, name); latchInput = Ntk_LatchReadDataInput(node); dataInputName = Ntk_NodeReadName(Ntk_LatchReadDataInput(node)); vertex = Part_PartitionFindVertexByName(partition, dataInputName); mvf = Part_VertexReadFunction(vertex); } singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->TRArray, index); if (singleTR == NIL(mdd_t)){ singleTR = Mvf_FunctionBuildRelationWithVariable(mvf, nsMddId); array_insert(mdd_t *, imcInfo->systemInfo->TRArray, index, bdd_minimize(singleTR, imcInfo->modelCareStates)); array_insert(Mvf_Function_t *, imcInfo->systemInfo->mvfArray, index, NIL(Mvf_Function_t)); mdd_free(singleTR); } singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->lowerTRArray, index); if (singleTR != NIL(mdd_t)){ mdd_free(singleTR); array_insert(mdd_t *,imcInfo->systemInfo->lowerTRArray,index,NIL(mdd_t)); } } } /**Function******************************************************************** Synopsis [Initilalize an upper-bound approximate system info.] Description [Initilalize an upper-bound approximate system info.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_UpperSystemInfoInitialize( Imc_Info_t *imcInfo, st_table *latchNameTable) { int i, index; int count; char *name; Imc_UpperSystemInfo_t *upperSystem; st_table *globalLatchNameTable; array_t *globalLatchNameArray; array_t *relationArray; mdd_t *singleTR; upperSystem = ALLOC(Imc_UpperSystemInfo_t, 1); upperSystem->systemInfo = imcInfo->systemInfo; globalLatchNameTable = imcInfo->systemInfo->latchNameTable; globalLatchNameArray = imcInfo->systemInfo->latchNameArray; relationArray = array_alloc(mdd_t *, st_count(latchNameTable)); count = 0; for (i=0;isystemInfo->TRArray, index); array_insert(mdd_t *, relationArray, count++, singleTR); } } Img_ClusterRelationArray(imcInfo->mddMgr, Img_Iwls95_c, Img_Backward_c, relationArray, imcInfo->systemInfo->psMddIdArray, imcInfo->systemInfo->nsMddIdArray, imcInfo->systemInfo->inputMddIdArray, &upperSystem->bwdRealationArray, &upperSystem->bwdSmoothVarsArray, NIL(array_t *), 0); /* FIXED */ upperSystem->fwdRealationArray = NIL(array_t); upperSystem->fwdSmoothVarsArray = NIL(array_t); upperSystem->bwdMinimizedRealationArray = NIL(array_t); upperSystem->careStates = mdd_dup(imcInfo->modelCareStates); array_free(relationArray); imcInfo->upperSystemInfo = upperSystem; if ((imcInfo->verbosity == Imc_VerbosityMin_c) || (imcInfo->verbosity == Imc_VerbosityMax_c)){ fprintf(vis_stdout, "IMC: |BWD Upper T| = %10ld BDD nodes (%-4d components)\n", bdd_size_multiple(upperSystem->bwdRealationArray), array_n(upperSystem->bwdRealationArray)); } return; } /**Function******************************************************************** Synopsis [Minimize the size of a upper-bound transition relation.] Description [Minimize the size of a upper-bound transition relation with respect to a given care states.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_UpperSystemMinimize( Imc_Info_t *imcInfo, mdd_t *careStates) { int i; mdd_t *singleTR; mdd_t *tempMdd; Imc_UpperSystemInfo_t *upperSystem = imcInfo->upperSystemInfo; if (mdd_equal(careStates,upperSystem->careStates)) return; if (upperSystem->bwdMinimizedRealationArray == NIL(array_t)){ upperSystem->bwdMinimizedRealationArray = array_alloc(mdd_t *, array_n(upperSystem->bwdRealationArray)); for (i=0;ibwdRealationArray);i++){ array_insert(mdd_t *, upperSystem->bwdMinimizedRealationArray, i, NIL(mdd_t)); } } for (i=0;ibwdRealationArray);i++){ singleTR = array_fetch(mdd_t *, upperSystem->bwdMinimizedRealationArray, i); if (singleTR != NIL(mdd_t)){ mdd_free(singleTR); } singleTR = array_fetch(mdd_t *, upperSystem->bwdRealationArray, i); tempMdd = bdd_minimize(singleTR, careStates); array_insert(mdd_t *, upperSystem->bwdMinimizedRealationArray, i, tempMdd); } if (upperSystem->careStates != NIL(mdd_t)){ mdd_free(upperSystem->careStates); } upperSystem->careStates = mdd_dup(careStates); if ((imcInfo->verbosity == Imc_VerbosityMin_c) || (imcInfo->verbosity == Imc_VerbosityMax_c)){ fprintf(vis_stdout, "IMC: |Minimized BWD Upper T| = %10ld BDD nodes (%-4d components)\n", bdd_size_multiple(upperSystem->bwdMinimizedRealationArray), array_n(upperSystem->bwdMinimizedRealationArray)); } return; } /**Function******************************************************************** Synopsis [Free a upper-bound approximate system info.] Description [Free a upper-bound approximate system info.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_UpperSystemInfoFree( Imc_UpperSystemInfo_t *upperSystem) { int i; array_t *tempArray; if (upperSystem == NIL(Imc_UpperSystemInfo_t)) return; if (upperSystem->careStates != NIL(mdd_t)){ mdd_free(upperSystem->careStates); } if (upperSystem->fwdRealationArray != NIL(array_t)){ mdd_array_free(upperSystem->fwdRealationArray); upperSystem->fwdRealationArray = NIL(array_t); } if (upperSystem->fwdSmoothVarsArray != NIL(array_t)){ array_free(upperSystem->fwdSmoothVarsArray); upperSystem->fwdSmoothVarsArray = NIL(array_t); } if (upperSystem->bwdRealationArray != NIL(array_t)){ mdd_array_free(upperSystem->bwdRealationArray); upperSystem->bwdRealationArray = NIL(array_t); } if (upperSystem->bwdMinimizedRealationArray != NIL(array_t)){ mdd_array_free(upperSystem->bwdMinimizedRealationArray); upperSystem->bwdMinimizedRealationArray = NIL(array_t); } if (upperSystem->bwdSmoothVarsArray != NIL(array_t)){ for (i=0; ibwdSmoothVarsArray);i++){ tempArray = array_fetch(array_t *, upperSystem->bwdSmoothVarsArray, i); mdd_array_free(tempArray); } array_free(upperSystem->bwdSmoothVarsArray); upperSystem->bwdSmoothVarsArray = NIL(array_t); } FREE(upperSystem); return; } /**Function******************************************************************** Synopsis [Initilalize a lower-bound approximate system info.] Description [Initilalize a lower-bound approximate system info.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_LowerSystemInfoInitialize( Imc_Info_t *imcInfo, st_table *latchNameTable) { int i, index; char *name; st_generator *stGen; mdd_t *singleTR; Imc_LowerSystemInfo_t *lowerSystem; array_t *tempArray; array_t *relationArray; st_table *globalLatchNameTable; array_t *latchNameArray; lowerSystem = ALLOC(Imc_LowerSystemInfo_t, 1); if ((imcInfo->lowerMethod == Imc_LowerUniversalQuantification_c) && (imcInfo->upperSystemInfo != NIL(Imc_UpperSystemInfo_t))){ lowerSystem->bwdRealationArray = mdd_array_duplicate( imcInfo->upperSystemInfo->bwdRealationArray); lowerSystem->bwdSmoothVarsArray = array_alloc(array_t *, array_n(imcInfo->upperSystemInfo->bwdSmoothVarsArray)); for (i=0;iupperSystemInfo->bwdSmoothVarsArray);i++){ tempArray = array_fetch(array_t *, imcInfo->upperSystemInfo->bwdSmoothVarsArray, i); array_insert(array_t *, lowerSystem->bwdSmoothVarsArray, i, mdd_array_duplicate(tempArray)); } lowerSystem->careStates = mdd_dup(imcInfo->modelCareStates); lowerSystem->bwdMinimizedRealationArray = NIL(array_t); imcInfo->lowerSystemInfo = lowerSystem; return; } globalLatchNameTable = imcInfo->systemInfo->latchNameTable; latchNameArray = array_alloc(char *, 0); st_foreach_item(globalLatchNameTable, stGen, &name, NIL(char *)){ array_insert_last(char *, latchNameArray, name); } array_sort(latchNameArray, stringCompare); relationArray = array_alloc(mdd_t *, 0); for (i=0;isystemInfo->TRArray, index); }else{ singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->lowerTRArray, index); } if (singleTR != NIL(mdd_t)){ array_insert_last(mdd_t *, relationArray, singleTR); } } array_free(latchNameArray); Img_ClusterRelationArray(imcInfo->mddMgr, Img_Iwls95_c, Img_Backward_c, relationArray, imcInfo->systemInfo->psMddIdArray, imcInfo->systemInfo->nsMddIdArray, imcInfo->systemInfo->inputMddIdArray, &lowerSystem->bwdRealationArray, &lowerSystem->bwdSmoothVarsArray, NIL(array_t *), 0); /* FIXED */ lowerSystem->bwdMinimizedRealationArray = NIL(array_t); lowerSystem->careStates = mdd_dup(imcInfo->modelCareStates);; imcInfo->lowerSystemInfo = lowerSystem; if ((imcInfo->verbosity == Imc_VerbosityMin_c) || (imcInfo->verbosity == Imc_VerbosityMax_c)){ fprintf(vis_stdout, "IMC: |BWD Lower T| = %10ld BDD nodes (%-4d components)\n", bdd_size_multiple(lowerSystem->bwdRealationArray), array_n(lowerSystem->bwdRealationArray)); } array_free(relationArray); /* Should be freed here, I guess, Chao Wang */ return; } /**Function******************************************************************** Synopsis [Minimize the size of a lower-bound transition relation.] Description [Minimize the size of a lower-bound transition relation with respect to a given care states.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_LowerSystemMinimize( Imc_Info_t *imcInfo, mdd_t *careStates) { int i; mdd_t *singleTR; mdd_t *tempMdd; Imc_LowerSystemInfo_t *lowerSystem = imcInfo->lowerSystemInfo; if (mdd_equal(careStates,lowerSystem->careStates)) return; if (lowerSystem->bwdMinimizedRealationArray == NIL(array_t)){ lowerSystem->bwdMinimizedRealationArray = array_alloc(mdd_t *, array_n(lowerSystem->bwdRealationArray)); for (i=0;ibwdRealationArray);i++){ array_insert(mdd_t *, lowerSystem->bwdMinimizedRealationArray, i, NIL(mdd_t)); } } for (i=0;ibwdRealationArray);i++){ singleTR = array_fetch(mdd_t *, lowerSystem->bwdMinimizedRealationArray, i); if (singleTR != NIL(mdd_t)){ mdd_free(singleTR); } singleTR = array_fetch(mdd_t *, lowerSystem->bwdRealationArray, i); tempMdd = bdd_minimize(singleTR, careStates); array_insert(mdd_t *, lowerSystem->bwdMinimizedRealationArray, i, tempMdd); } if (lowerSystem->careStates != NIL(mdd_t)){ mdd_free(lowerSystem->careStates); } lowerSystem->careStates = mdd_dup(careStates); if ((imcInfo->verbosity == Imc_VerbosityMin_c) || (imcInfo->verbosity == Imc_VerbosityMax_c)){ fprintf(vis_stdout, "IMC: |Minimized BWD Lower T| = %10ld BDD nodes (%-4d components)\n", bdd_size_multiple(lowerSystem->bwdMinimizedRealationArray), array_n(lowerSystem->bwdMinimizedRealationArray)); } } /**Function******************************************************************** Synopsis [Free a lower-bound approximate system info.] Description [Free a lower-bound approximate system info.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_LowerSystemInfoFree( Imc_LowerSystemInfo_t *lowerSystem) { int i; array_t *tempArray; if (lowerSystem == NIL(Imc_LowerSystemInfo_t)) return; if (lowerSystem->careStates != NIL(mdd_t)){ mdd_free(lowerSystem->careStates); } if (lowerSystem->bwdRealationArray != NIL(array_t)){ mdd_array_free(lowerSystem->bwdRealationArray); lowerSystem->bwdRealationArray = NIL(array_t); } if (lowerSystem->bwdMinimizedRealationArray != NIL(array_t)){ mdd_array_free(lowerSystem->bwdMinimizedRealationArray); lowerSystem->bwdMinimizedRealationArray = NIL(array_t); } if (lowerSystem->bwdSmoothVarsArray != NIL(array_t)){ for (i=0; ibwdSmoothVarsArray);i++){ tempArray = array_fetch(array_t *, lowerSystem->bwdSmoothVarsArray, i); mdd_array_free(tempArray); } array_free(lowerSystem->bwdSmoothVarsArray); lowerSystem->bwdSmoothVarsArray = NIL(array_t); /* FIXED */ } FREE(lowerSystem); return; } /**Function******************************************************************** Synopsis [Initilalize node info.] Description [Initilalize node info.] SideEffects [] SeeAlso [] ******************************************************************************/ Imc_NodeInfo_t * Imc_NodeInfoInitialize( Imc_Polarity polarity) { Imc_NodeInfo_t *nodeInfo; nodeInfo = ALLOC(Imc_NodeInfo_t, 1); nodeInfo->isExact = FALSE; nodeInfo->polarity = polarity; nodeInfo->upperSat = NIL(mdd_t); nodeInfo->lowerSat = NIL(mdd_t); nodeInfo->propagatedGoalSet = NIL(mdd_t); nodeInfo->propagatedGoalSetTrue = NIL(mdd_t); nodeInfo->goalSet = NIL(mdd_t); nodeInfo->goalSetTrue = NIL(mdd_t); nodeInfo->answer = Imc_VerificationInconclusive_c; nodeInfo->upperDone = FALSE; nodeInfo->lowerDone = FALSE; nodeInfo->pseudoEdges = NIL(mdd_t); return nodeInfo; } /**Function******************************************************************** Synopsis [Reset node info.] Description [Reset node info.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_NodeInfoReset( Imc_Info_t *imcInfo) { Ctlp_Formula_t *formula; st_table *nodeInfoTable = imcInfo->nodeInfoTable; st_generator *stGen; Imc_NodeInfo_t *nodeInfo; st_foreach_item(nodeInfoTable, stGen, &formula, &nodeInfo){ if (!nodeInfo->isExact){ nodeInfo->lowerDone = FALSE; nodeInfo->upperDone = FALSE; } if (nodeInfo->propagatedGoalSet != NIL(mdd_t)){ mdd_free(nodeInfo->propagatedGoalSet); nodeInfo->propagatedGoalSet = NIL(mdd_t); } if (nodeInfo->propagatedGoalSetTrue != NIL(mdd_t)){ mdd_free(nodeInfo->propagatedGoalSetTrue); nodeInfo->propagatedGoalSetTrue = NIL(mdd_t); } if (nodeInfo->goalSet != NIL(mdd_t)){ mdd_free(nodeInfo->goalSet); nodeInfo->goalSet = NIL(mdd_t); } if (nodeInfo->goalSetTrue != NIL(mdd_t)){ mdd_free(nodeInfo->goalSetTrue); nodeInfo->goalSetTrue = NIL(mdd_t); } if (nodeInfo->pseudoEdges != NIL(mdd_t)){ mdd_free(nodeInfo->pseudoEdges); nodeInfo->pseudoEdges = NIL(mdd_t); } } } /**Function******************************************************************** Synopsis [Free node info.] Description [Free node info.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_NodeInfoFree( Imc_NodeInfo_t *nodeInfo) { if (nodeInfo->upperSat != NIL(mdd_t)){ mdd_free(nodeInfo->upperSat); } if (nodeInfo->lowerSat != NIL(mdd_t)){ mdd_free(nodeInfo->lowerSat); } if (nodeInfo->goalSet != NIL(mdd_t)){ mdd_free(nodeInfo->goalSet); } if (nodeInfo->goalSetTrue != NIL(mdd_t)){ mdd_free(nodeInfo->goalSetTrue); } if (nodeInfo->propagatedGoalSet != NIL(mdd_t)){ mdd_free(nodeInfo->propagatedGoalSet); } if (nodeInfo->propagatedGoalSetTrue != NIL(mdd_t)){ mdd_free(nodeInfo->propagatedGoalSetTrue); } if (nodeInfo->pseudoEdges != NIL(mdd_t)){ mdd_free(nodeInfo->pseudoEdges); } FREE(nodeInfo); } /**Function******************************************************************** Synopsis [Print global system size.] Description [Print global system size by multi-value and boolean value latch.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_ImcPrintSystemSize( Imc_Info_t *imcInfo) { array_t *includedBooleanVars; array_t *psMddIdArray = imcInfo->systemInfo->psMddIdArray; includedBooleanVars = mdd_id_array_to_bdd_id_array(imcInfo->mddMgr, psMddIdArray); fprintf(vis_stdout, "%d(%d) ", array_n(psMddIdArray), array_n(includedBooleanVars)); fprintf(vis_stdout, "multi-value(boolean) latches.\n"); array_free(includedBooleanVars); } /**Function******************************************************************** Synopsis [Print upper-system size.] Description [Print upper-system size by multi-value and boolean value latch.] SideEffects [] SeeAlso [] ******************************************************************************/ void Imc_ImcPrintApproxSystemSize( Imc_Info_t *imcInfo) { int i, index, psMddId; array_t *includedBooleanVars; array_t *includedPsMddIdArray; array_t *psMddIdArray = imcInfo->systemInfo->psMddIdArray; array_t *includedLatchIndex = imcInfo->systemInfo->includedLatchIndex; includedPsMddIdArray = array_alloc(int,array_n(includedLatchIndex)); for(i=0;imddMgr, includedPsMddIdArray); fprintf(vis_stdout, "%d(%d) ", array_n(includedPsMddIdArray), array_n(includedBooleanVars)); fprintf(vis_stdout, "multi-value(boolean) latches.\n"); array_free(includedPsMddIdArray); array_free(includedBooleanVars); } /**Function******************************************************************** Synopsis [Get a upperbound satisfying states of a given formula.] Description [Get a upperbound satisfying states of a given formula if is is already computed.] Comment [] SideEffects [] ******************************************************************************/ mdd_t * Imc_GetUpperSat( Imc_Info_t *imcInfo, Ctlp_Formula_t *formula) { Imc_NodeInfo_t *nodeInfo; if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){ return NIL(mdd_t); } return nodeInfo->upperSat; } /**Function******************************************************************** Synopsis [Get a lowerbound satisfying states of a given formula.] Description [Get a lowerbound satisfying states of a given formula if is is already computed.] Comment [] SideEffects [] ******************************************************************************/ mdd_t * Imc_GetLowerSat( Imc_Info_t *imcInfo, Ctlp_Formula_t *formula) { Imc_NodeInfo_t *nodeInfo; if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){ return NIL(mdd_t); } return nodeInfo->lowerSat; } /**Function******************************************************************** Synopsis [Model check formula with approxmiations.] Description [The routine evaluates given formula with approximations. If polarity is set, upper approximation is computed. Otherwise, lower approximation is computed.] Comment [] SideEffects [] ******************************************************************************/ int Imc_ImcEvaluateCTLFormula( Imc_Info_t *imcInfo, Ctlp_Formula_t *ctlFormula, Imc_Polarity polarity) { Imc_Polarity newPolarity, approxPolarity; Ctlp_Formula_t *leftChild, *rightChild; Imc_NodeInfo_t *nodeInfo; Imc_GraphType graphType = imcInfo->graphType; if (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_NOT_c){ newPolarity = (polarity == Imc_PolarityNeg_c) ? Imc_PolarityPos_c: (polarity == Imc_PolarityPos_c) ? Imc_PolarityNeg_c: polarity; }else{ newPolarity = polarity; } if (graphType == Imc_GraphNDOG_c){ /* In-Ho : Why change the polarity ? */ approxPolarity = (polarity == Imc_PolarityNeg_c) ? Imc_PolarityPos_c: Imc_PolarityNeg_c; }else{ approxPolarity = polarity; } if (!st_lookup(imcInfo->nodeInfoTable, ctlFormula, &nodeInfo)){ nodeInfo = Imc_NodeInfoInitialize(polarity); st_insert(imcInfo->nodeInfoTable, ctlFormula, nodeInfo); }else if ((nodeInfo->isExact) || ((approxPolarity == Imc_PolarityNeg_c) && (nodeInfo->lowerDone)) || ((approxPolarity == Imc_PolarityPos_c) && (nodeInfo->upperDone))){ if (imcInfo->verbosity == Imc_VerbosityMax_c){ if ((Ctlp_FormulaReadType( ctlFormula ) == Ctlp_ID_c ) || (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_TRUE_c ) || (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_FALSE_c )){ fprintf(vis_stdout, "IMC : node simple already computed.\n"); }else if ((Ctlp_FormulaReadType( ctlFormula ) == Ctlp_AND_c ) || (Ctlp_FormulaReadType( ctlFormula ) == Ctlp_NOT_c )){ fprintf(vis_stdout, "IMC : node boolean already computed.\n"); }else{ /* In-Ho : Why only ECTL? */ fprintf(vis_stdout, "IMC : node ECTL already computed.\n"); } } return 1; } leftChild = Ctlp_FormulaReadLeftChild(ctlFormula); if (leftChild) { if (!Imc_ImcEvaluateCTLFormula(imcInfo,leftChild,newPolarity)){ return 0; } } rightChild = Ctlp_FormulaReadRightChild(ctlFormula); if (rightChild) { if (!Imc_ImcEvaluateCTLFormula(imcInfo,rightChild,newPolarity)){ return 0; } } switch ( Ctlp_FormulaReadType( ctlFormula ) ) { case Ctlp_ID_c : if (!ImcModelCheckAtomicFormula(imcInfo,ctlFormula)) return 0; break; case Ctlp_TRUE_c : if (!ImcModelCheckTrueFalseFormula(imcInfo,ctlFormula, TRUE)) return 0; break; case Ctlp_FALSE_c : if (!ImcModelCheckTrueFalseFormula(imcInfo,ctlFormula, FALSE)) return 0; break; case Ctlp_NOT_c : if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){ if (!ImcModelCheckNotFormula(imcInfo,ctlFormula, TRUE)) return 0; } if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){ if(!ImcModelCheckNotFormula(imcInfo,ctlFormula, FALSE)) return 0; } break; case Ctlp_AND_c : if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){ if (!ImcModelCheckAndFormula(imcInfo,ctlFormula,TRUE))return 0; } if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){ if (!ImcModelCheckAndFormula(imcInfo,ctlFormula,FALSE)) return 0; } break; case Ctlp_EX_c : if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){ if (!Imc_ImcEvaluateEXApprox(imcInfo,ctlFormula, TRUE, FALSE)) return 0; } if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){ if (!Imc_ImcEvaluateEXApprox(imcInfo,ctlFormula, FALSE, FALSE)) return 0; } break; case Ctlp_EU_c : if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){ if (!Imc_ImcEvaluateEUApprox(imcInfo,ctlFormula,TRUE, FALSE)) return 0; } if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){ if (!Imc_ImcEvaluateEUApprox(imcInfo,ctlFormula, FALSE, FALSE)) return 0; } break; case Ctlp_EG_c : if ((approxPolarity == Imc_PolarityPos_c) || (graphType == Imc_GraphMOG_c)){ if (!Imc_ImcEvaluateEGApprox(imcInfo,ctlFormula,TRUE, FALSE)) return 0; } if ((approxPolarity == Imc_PolarityNeg_c) || (graphType == Imc_GraphMOG_c)){ if (!Imc_ImcEvaluateEGApprox(imcInfo,ctlFormula, FALSE, FALSE)) return 0; } break; default: fail("Encountered unknown type of CTL formula\n"); } if (nodeInfo->upperDone && nodeInfo->lowerDone){ if (!nodeInfo->isExact && mdd_equal_mod_care_set(nodeInfo->upperSat, nodeInfo->lowerSat, imcInfo->modelCareStates)){ /* FIXED */ nodeInfo->isExact = TRUE; } } return 1; } /**Function******************************************************************** Synopsis [Evaluate EX formula with approximations.] Description [Evaluate EX formula with approximations. If isUpper is set, a superset of exact satisfying states of EG formula is computed. Otherwise, a subset is computed.] SideEffects [] SeeAlso [] ******************************************************************************/ int Imc_ImcEvaluateEXApprox( Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation) { mdd_t *targetStates; Ctlp_Formula_t *leftChild; mdd_t *result = NIL(mdd_t); mdd_t *tempResult; mdd_t *localCareStates; mdd_t *globalCareStates; boolean useLocalCare = FALSE; Imc_NodeInfo_t *nodeInfo, *lNodeInfo; boolean isExact; globalCareStates = imcInfo->modelCareStates; if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){ fprintf(vis_stdout, "** imc error : EX nodeinfo is not initilize.\n"); return 0; } leftChild = Ctlp_FormulaReadLeftChild(formula); if (!st_lookup(imcInfo->nodeInfoTable, leftChild, &lNodeInfo)){ fprintf(vis_stdout, "** imc error : EX left nodeinfo is not initilize.\n"); return 0; } if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EX)+ computation start.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EX)- computation start.\n"); } } /* * If exact sat is already computed from other side of approximation, * use it. */ if (nodeInfo->isExact){ if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EX)+ computation end.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EX)- computation end.\n"); } } return 1; } /* * If this is not for recomputation, do general satisfying states computation. * Otherwise, compute the subset of the propagated goalset where the formula * satisfies. * Test if tighter satisfying don't care states(ASDC) can be used to reduce * transition sub-relations. */ if (nodeInfo->upperSat != NIL(mdd_t)){ localCareStates = mdd_and(nodeInfo->upperSat,globalCareStates, 1, 1); }else{ localCareStates = mdd_dup(globalCareStates); } if ((mdd_lequal(localCareStates,globalCareStates, 1, 1)) && (!mdd_equal(localCareStates,globalCareStates))){ useLocalCare = TRUE; } if (!isRecomputation){ if (isUpper){ targetStates = lNodeInfo->upperSat; }else{ targetStates = lNodeInfo->lowerSat; } }else{ targetStates = lNodeInfo->propagatedGoalSetTrue; } if (targetStates == NIL(mdd_t)) return 0; if ((isUpper)|| (isRecomputation)) Imc_UpperSystemMinimize(imcInfo, localCareStates); else Imc_LowerSystemMinimize(imcInfo, localCareStates); if ((isUpper) || (isRecomputation)){ tempResult = Imc_ComputeUpperPreimage(imcInfo, localCareStates, targetStates, &isExact); }else{ tempResult = Imc_ComputeLowerPreimage(imcInfo, localCareStates, targetStates, &isExact); } if (tempResult == NIL(mdd_t)) return 0; if ((imcInfo->verbosity == Imc_VerbosityMax_c) || (imcInfo->verbosity == Imc_VerbosityMin_c)) { mdd_t *tmpMdd = mdd_and(tempResult, localCareStates, 1, 1 ); double minterm = mdd_count_onset(imcInfo->mddMgr, tmpMdd, imcInfo->systemInfo->psMddIdArray); if (isUpper){ fprintf(vis_stdout, "IMC : |SAT(EX)+| = %.0f (%10g)\n", minterm, minterm); }else{ fprintf(vis_stdout, "IMC : |SAT(EX)-| = %.0f (%10g)\n", minterm, minterm); } mdd_free(tmpMdd); } if (useLocalCare){ result = mdd_and(tempResult, localCareStates, 1, 1); mdd_free(tempResult); tempResult = bdd_minimize(result, globalCareStates); mdd_free(result); result = tempResult; }else{ result = tempResult; } mdd_free(localCareStates); if (isRecomputation){ tempResult = mdd_and(nodeInfo->goalSet, result, 1, 1); mdd_free(result); nodeInfo->propagatedGoalSetTrue = mdd_or(nodeInfo->goalSetTrue, tempResult, 1, 1); mdd_free(tempResult); return 1; } if (isUpper){ if (nodeInfo->upperSat != NIL(mdd_t)){ mdd_free(nodeInfo->upperSat); } nodeInfo->upperSat = result; nodeInfo->upperDone = TRUE; }else{ if (nodeInfo->lowerSat != NIL(mdd_t)){ tempResult = mdd_or(nodeInfo->lowerSat, result, 1, 1); mdd_free(nodeInfo->lowerSat); mdd_free(result); result = tempResult; } nodeInfo->lowerSat = result; nodeInfo->lowerDone = TRUE; } if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EX)+ computation end.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EX)- computation end.\n"); } } if (lNodeInfo->isExact && isExact){ nodeInfo->isExact = TRUE; if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EX)+ computation is exact.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EX)- computation is exact.\n"); } } if (isUpper){ if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat); nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat); nodeInfo->lowerDone = TRUE; }else{ if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat); nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat); nodeInfo->upperDone = TRUE; } }else{ nodeInfo->isExact = FALSE; } return 1; } /**Function******************************************************************** Synopsis [Evaluate EU formula with approximations.] Description [Evaluate EU formula with approximations. If isUpper is set, a superset of exact satisfying states of EG formula is computed. Otherwise, a subset is computed.] Comment [] SideEffects [] ******************************************************************************/ int Imc_ImcEvaluateEUApprox( Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation) { mdd_t *localCareStates; mdd_t *targetStates, *invariantStates; mdd_t *aMdd, *bMdd, *cMdd; mdd_t *result; mdd_t *tmpMdd1, *tmpMdd2; mdd_t * globalCareStates; double size1, size2; Ctlp_Formula_t *lFormula, *rFormula; Imc_NodeInfo_t *nodeInfo, *lNodeInfo, *rNodeInfo; boolean isExact, globalIsExact; globalIsExact = TRUE; globalCareStates = imcInfo->modelCareStates; lFormula = Ctlp_FormulaReadLeftChild(formula); rFormula = Ctlp_FormulaReadRightChild(formula); if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){ fprintf(vis_stdout, "** imc error : EU nodeinfo is not initilize.\n"); return 0; } if (!st_lookup(imcInfo->nodeInfoTable, lFormula, &lNodeInfo)){ fprintf(vis_stdout, "** imc error : EU left nodeinfo is not initilize.\n"); return 0; } if (!st_lookup(imcInfo->nodeInfoTable, rFormula, &rNodeInfo)){ fprintf(vis_stdout, "** imc error : EU right nodeinfo is not initilize.\n"); return 0; } if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EU)+ computation start.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EU)- computation start.\n"); } } /* * If exact sat is already computed from other side of approximation, * use it. */ if (nodeInfo->isExact){ if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EU)+ computation end.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EU)- computation end.\n"); } } return 1; } /* * Test if tighter satisfying don't care states(ASDC) can be used to reduce * transition sub-relations. */ if (nodeInfo->upperSat != NIL(mdd_t)){ localCareStates = mdd_and(nodeInfo->upperSat,globalCareStates, 1, 1); }else{ localCareStates = mdd_dup(globalCareStates); } if ((mdd_lequal(localCareStates,globalCareStates, 1, 1)) && (!mdd_equal(localCareStates,globalCareStates))){ } if (!isRecomputation){ if (isUpper){ if (nodeInfo->lowerSat != NIL(mdd_t)){ targetStates = mdd_or(rNodeInfo->upperSat, nodeInfo->lowerSat, 1, 1); }else{ targetStates = mdd_dup(rNodeInfo->upperSat); } invariantStates = lNodeInfo->upperSat; }else{ targetStates = mdd_dup(rNodeInfo->lowerSat); invariantStates = lNodeInfo->lowerSat; } }else{ targetStates = mdd_dup(rNodeInfo->propagatedGoalSetTrue); invariantStates = lNodeInfo->propagatedGoalSetTrue; } result = targetStates; if ((isUpper) || (isRecomputation)) Imc_UpperSystemMinimize(imcInfo, localCareStates); else Imc_LowerSystemMinimize(imcInfo, localCareStates); while (TRUE) { if (isUpper){ aMdd = Imc_ComputeUpperPreimage(imcInfo, localCareStates, result, &isExact); }else{ aMdd = Imc_ComputeLowerPreimage(imcInfo, localCareStates, result, &isExact); } if (aMdd == NIL(mdd_t)) return 0; globalIsExact = (globalIsExact && isExact); bMdd = mdd_and( aMdd, invariantStates, 1, 1 ); mdd_free( aMdd ); aMdd = mdd_and(bMdd, localCareStates, 1, 1); mdd_free(bMdd); bMdd = bdd_minimize(aMdd, globalCareStates); mdd_free(aMdd); cMdd = mdd_or(result, bMdd, 1, 1); mdd_free( bMdd ); tmpMdd1 = mdd_and( result, globalCareStates, 1, 1 ); tmpMdd2 = mdd_and( cMdd, globalCareStates, 1, 1 ); if (mdd_equal(tmpMdd1, tmpMdd2)){ mdd_free(cMdd); break; }else if (mdd_equal(tmpMdd2, localCareStates)){ mdd_free(result); result = cMdd; break; }else if (( imcInfo->verbosity == Imc_VerbosityMax_c ) || (imcInfo->verbosity == Imc_VerbosityMin_c)) { size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1, imcInfo->systemInfo->psMddIdArray); size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2, imcInfo->systemInfo->psMddIdArray); if (isUpper){ fprintf(vis_stdout, "IMC : |SAT(EU)+| = %.0f (%10g)-> %.0f (%10g)\n", size1, size1, size2, size2); }else{ fprintf(vis_stdout, "IMC : |SAT(EU)-| = %.0f (%10g)-> %.0f (%10g)\n", size1, size1, size2, size2); } } mdd_free(tmpMdd1); mdd_free(tmpMdd2); mdd_free( result ); result = bdd_minimize(cMdd, globalCareStates); mdd_free(cMdd); } if ((imcInfo->verbosity == Imc_VerbosityMax_c) || (imcInfo->verbosity == Imc_VerbosityMin_c)) { size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1, imcInfo->systemInfo->psMddIdArray); size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2, imcInfo->systemInfo->psMddIdArray); if (isUpper){ fprintf(vis_stdout, "IMC : |SAT(EU)+| = %.0f (%10g)-> %.0f (%10g)\n", size1, size1, size2, size2); }else{ fprintf(vis_stdout, "IMC : |SAT(EU)-| = %.0f (%10g)-> %.0f (%10g)\n", size1, size1, size2, size2); } } mdd_free(tmpMdd1); mdd_free(tmpMdd2); mdd_free(localCareStates); if (isRecomputation){ tmpMdd1 = mdd_and(nodeInfo->goalSet, result, 1, 1); mdd_free(result); nodeInfo->propagatedGoalSetTrue = mdd_or(nodeInfo->goalSetTrue, tmpMdd1, 1, 1); mdd_free(tmpMdd1); return 1; } if (isUpper){ if (nodeInfo->upperSat != NIL(mdd_t)){ mdd_free(nodeInfo->upperSat); } nodeInfo->upperSat = result; nodeInfo->upperDone = TRUE; }else{ if (nodeInfo->lowerSat != NIL(mdd_t)){ tmpMdd1 = mdd_or(nodeInfo->lowerSat, result, 1, 1); mdd_free(nodeInfo->lowerSat); mdd_free(result); result = tmpMdd1; } nodeInfo->lowerSat = result; nodeInfo->lowerDone = TRUE; } if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EU)+ computation end.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EU)- computation end.\n"); } } if (lNodeInfo->isExact && rNodeInfo->isExact && globalIsExact){ nodeInfo->isExact = TRUE; if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EU)+ computation is exact.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EU)- computation is exact.\n"); } } if (isUpper){ if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat); nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat); nodeInfo->lowerDone = TRUE; }else{ if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat); nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat); nodeInfo->upperDone = TRUE; } }else{ nodeInfo->isExact = FALSE; } return 1; } /**Function******************************************************************** Synopsis [Evaluate EG formula with approximations.] Description [Evaluate EG formula with approximations. If isUpper is set, a superset of exact satisfying states of EG formula is computed. Otherwise, a subset is computed.] SideEffects [] ******************************************************************************/ int Imc_ImcEvaluateEGApprox( Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation) { mdd_t *Zmdd; mdd_t *bMdd; mdd_t *ZprimeMdd; mdd_t *tmpMdd1, *tmpMdd2; mdd_t *result; mdd_t *localCareStates; mdd_t *globalCareStates; mdd_t *invariantStates; double size1, size2; Ctlp_Formula_t *lFormula; Imc_NodeInfo_t *nodeInfo, *lNodeInfo; boolean isExact, globalIsExact; lFormula = Ctlp_FormulaReadLeftChild(formula); if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){ fprintf(vis_stdout, "** imc error : EG nodeinfo is not initilize.\n"); return 0; } if (!st_lookup(imcInfo->nodeInfoTable, lFormula, &lNodeInfo)){ fprintf(vis_stdout, "** imc error : EG left nodeinfo is not initilize.\n"); return 0; } if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EG)+ computation start.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EG)- computation start.\n"); } } /* * If exact sat is already computed from other side of approximation, * use it. */ if (nodeInfo->isExact){ if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EG)+ computation end.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EG)- computation end.\n"); } } return 1; } globalCareStates = imcInfo->modelCareStates; /* * Test if tighter satisfying don't care states(ASDC) can be used to reduce * transition sub-relations. */ if (nodeInfo->upperSat != NIL(mdd_t)){ localCareStates = mdd_and(nodeInfo->upperSat,globalCareStates, 1, 1); }else{ localCareStates = mdd_dup(globalCareStates); } if ((mdd_lequal(localCareStates,globalCareStates, 1, 1)) && (!mdd_equal(localCareStates,globalCareStates))){ } if (!isRecomputation){ if (isUpper){ if (nodeInfo->upperSat != NIL(mdd_t)){ invariantStates = mdd_and(lNodeInfo->upperSat, nodeInfo->upperSat,1,1); }else{ invariantStates = mdd_dup(lNodeInfo->upperSat); } }else{ if (nodeInfo->upperSat != NIL(mdd_t)){ invariantStates = mdd_and(lNodeInfo->lowerSat, nodeInfo->upperSat,1,1); }else{ invariantStates = mdd_dup(lNodeInfo->lowerSat); } } }else{ invariantStates = mdd_dup(lNodeInfo->propagatedGoalSetTrue); } Zmdd = mdd_dup(invariantStates); ZprimeMdd = NIL(mdd_t); globalIsExact = TRUE; if ((isUpper) || (isRecomputation)) Imc_UpperSystemMinimize(imcInfo, localCareStates); else Imc_LowerSystemMinimize(imcInfo, localCareStates); while (TRUE) { if (isUpper){ bMdd = Imc_ComputeUpperPreimage(imcInfo, localCareStates, Zmdd, &isExact); }else{ bMdd = Imc_ComputeLowerPreimage(imcInfo, localCareStates, Zmdd, &isExact); } if (bMdd == NIL(mdd_t)){ mdd_free(invariantStates); mdd_free(Zmdd); if (ZprimeMdd !=NIL(mdd_t)) mdd_free(ZprimeMdd); return 0; } ZprimeMdd = mdd_and(Zmdd, bMdd, 1, 1); globalIsExact = (globalIsExact && isExact); mdd_free(bMdd); tmpMdd1 = mdd_and( Zmdd, globalCareStates, 1, 1 ); tmpMdd2 = mdd_and( ZprimeMdd, localCareStates, 1, 1 ); mdd_free(Zmdd); mdd_free(ZprimeMdd); if ((mdd_equal(tmpMdd1, tmpMdd2)) || (mdd_is_tautology(tmpMdd2, 0))){ break; }else if (( imcInfo->verbosity == Imc_VerbosityMax_c ) || (imcInfo->verbosity == Imc_VerbosityMin_c)) { size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1, imcInfo->systemInfo->psMddIdArray); size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2, imcInfo->systemInfo->psMddIdArray); if (isUpper){ fprintf(vis_stdout, "IMC : |SAT(EG)+| = %.0f (%10g)-> %.0f (%10g)\n", size1, size1, size2, size2); }else{ fprintf(vis_stdout, "IMC : |SAT(EG)-| = %.0f (%10g)-> %.0f (%10g)\n", size1, size1, size2, size2); } } mdd_free(tmpMdd1); Zmdd = bdd_minimize(tmpMdd2, globalCareStates); mdd_free(tmpMdd2); } if (( imcInfo->verbosity == Imc_VerbosityMax_c ) || (imcInfo->verbosity == Imc_VerbosityMin_c)) { size1 = mdd_count_onset(imcInfo->mddMgr, tmpMdd1, imcInfo->systemInfo->psMddIdArray); size2 = mdd_count_onset(imcInfo->mddMgr, tmpMdd2, imcInfo->systemInfo->psMddIdArray); if (isUpper){ fprintf(vis_stdout, "IMC : |SAT(EG)+| = %.0f (%10g)-> %.0f (%10g)\n", size1, size1, size2, size2); }else{ fprintf(vis_stdout, "IMC : |SAT(EG)-| = %.0f (%10g)-> %.0f (%10g)\n", size1, size1, size2, size2); } } mdd_free(tmpMdd1); mdd_free(localCareStates); result = bdd_minimize(tmpMdd2, globalCareStates); mdd_free(tmpMdd2); if (isRecomputation){ tmpMdd1 = mdd_and(nodeInfo->goalSet, result, 1, 1); mdd_free(result); nodeInfo->propagatedGoalSetTrue = mdd_or(nodeInfo->goalSetTrue,tmpMdd1,1,1); mdd_free(tmpMdd1); return 1; } mdd_free(invariantStates); if (isUpper){ if (nodeInfo->upperSat != NIL(mdd_t)){ mdd_free(nodeInfo->upperSat); } nodeInfo->upperSat = result; nodeInfo->upperDone = TRUE; }else{ if (nodeInfo->lowerSat != NIL(mdd_t)){ tmpMdd1 = mdd_or(nodeInfo->lowerSat, result, 1, 1); mdd_free(nodeInfo->lowerSat); mdd_free(result); result = bdd_minimize(tmpMdd1, globalCareStates); mdd_free(tmpMdd1); } nodeInfo->lowerSat = result; nodeInfo->lowerDone = TRUE; } if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EG)+ computation end.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EG)- computation end.\n"); } } if (lNodeInfo->isExact && globalIsExact){ nodeInfo->isExact = TRUE; if ( imcInfo->verbosity == Imc_VerbosityMax_c ){ if (isUpper){ fprintf(vis_stdout, "IMC : SAT(EG)+ computation is exact.\n"); }else{ fprintf(vis_stdout, "IMC : SAT(EG)- computation is exact.\n"); } } if (isUpper){ if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat); nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat); nodeInfo->lowerDone = TRUE; }else{ if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat); nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat); nodeInfo->upperDone = TRUE; } }else{ nodeInfo->isExact = FALSE; } return 1; } /**Function******************************************************************* Synopsis [Compte a supperset of exact pre image.] Description [Compte a supperset of exact pre image. If result is exact pre image, isExact is set.] SideEffects [] ******************************************************************************/ mdd_t * Imc_ComputeUpperPreimage( Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact) { if (imcInfo->upperMethod == Imc_UpperExistentialQuantification_c){ return Imc_ComputeApproxPreimageByQuantification(imcInfo, rangeCareStates, targetStates, isExact, FALSE); } return NIL(mdd_t); } /**Function******************************************************************* Synopsis [Compte a superset or a subset of exact pre image.] Description [Compte a superset or a subset of exact pre image accrding to computeLower parameter. If result is exact pre image, isExact is set.] SideEffects [] ******************************************************************************/ mdd_t * Imc_ComputeApproxPreimageByQuantification( Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact, boolean computeLower) { int i; int psMddId; double orgSize, newSize; mdd_t *result; mdd_t *nextTarget; mdd_t *reducedTarget; mdd_t *tempMdd; mdd_t *reducedTargetInCare; mdd_t *targetInCare; array_t *supportArray; *isExact = TRUE; if (mdd_is_tautology(targetStates, 0)){ return mdd_zero(imcInfo->mddMgr); } supportArray = mdd_get_support(imcInfo->mddMgr, targetStates); for(i=0;isystemInfo->excludedPsMddIdTable, (char *)(long)psMddId)){ *isExact = FALSE; break; } } array_free(supportArray); if (array_n(imcInfo->systemInfo->excludedPsMddId) >0){ if (!computeLower){ reducedTarget = mdd_smooth(imcInfo->mddMgr, targetStates, imcInfo->systemInfo->excludedPsMddId); }else{ reducedTarget = mdd_consensus(imcInfo->mddMgr, targetStates, imcInfo->systemInfo->excludedPsMddId); } if ((mdd_is_tautology(reducedTarget,1)) || (mdd_is_tautology(reducedTarget,0))){ return reducedTarget; } }else{ reducedTarget = mdd_dup(targetStates); } if (imcInfo->verbosity == Imc_VerbosityMax_c){ targetInCare = mdd_and(targetStates, imcInfo->modelCareStates, 1, 1); reducedTargetInCare = mdd_and(reducedTarget, imcInfo->modelCareStates, 1, 1); orgSize = mdd_count_onset(imcInfo->mddMgr, targetInCare, imcInfo->systemInfo->psMddIdArray); newSize = mdd_count_onset(imcInfo->mddMgr, reducedTargetInCare, imcInfo->systemInfo->psMddIdArray); if (!computeLower){ fprintf(vis_stdout, "IMC : Upper Approximation |S| = %.0f (%10g)-> %.0f (%10g)\n", orgSize, orgSize, newSize, newSize); }else{ fprintf(vis_stdout, "IMC : Lower Approximation |S| = %.0f (%10g)-> %.0f (%10g)\n", orgSize, orgSize, newSize, newSize); } mdd_free(targetInCare); mdd_free(reducedTargetInCare); } nextTarget = mdd_substitute(imcInfo->mddMgr, reducedTarget, imcInfo->systemInfo->psMddIdArray, imcInfo->systemInfo->nsMddIdArray); mdd_free(reducedTarget); if (!computeLower){ if (imcInfo->upperSystemInfo->bwdMinimizedRealationArray == NIL(array_t)){ result = Imc_ProductAbstract(imcInfo->mddMgr, imcInfo->upperSystemInfo->bwdRealationArray, imcInfo->upperSystemInfo->bwdSmoothVarsArray, nextTarget); }else{ result = Imc_ProductAbstract(imcInfo->mddMgr, imcInfo->upperSystemInfo->bwdMinimizedRealationArray, imcInfo->upperSystemInfo->bwdSmoothVarsArray, nextTarget); } }else{ if (imcInfo->lowerSystemInfo->bwdMinimizedRealationArray == NIL(array_t)){ result = Imc_ProductAbstract(imcInfo->mddMgr, imcInfo->lowerSystemInfo->bwdRealationArray, imcInfo->lowerSystemInfo->bwdSmoothVarsArray, nextTarget); }else{ result = Imc_ProductAbstract(imcInfo->mddMgr, imcInfo->lowerSystemInfo->bwdMinimizedRealationArray, imcInfo->lowerSystemInfo->bwdSmoothVarsArray, nextTarget); } } mdd_free(nextTarget); if (imcInfo->verbosity == Imc_VerbosityMax_c){ double exactSize, approxSize; tempMdd = mdd_and(result, rangeCareStates, 1, 1); approxSize = mdd_count_onset(imcInfo->mddMgr, result, imcInfo->systemInfo->psMddIdArray); exactSize = mdd_count_onset(imcInfo->mddMgr, tempMdd, imcInfo->systemInfo->psMddIdArray); mdd_free(tempMdd); if (!computeLower){ fprintf(vis_stdout, "IMC : Upper Preimage |S+DC| = %.0f (%10g)\n", approxSize, approxSize); fprintf(vis_stdout, "IMC : Upper Preimage |S| = %.0f (%10g)\n", exactSize, exactSize); }else{ fprintf(vis_stdout, "IMC : Lower Preimage |S+DC| = %.0f (%10g)\n", approxSize, approxSize); fprintf(vis_stdout, "IMC : Lower Preimage |S| = %.0f (%10g)\n", exactSize, exactSize); } } /* * If preimage is zero, don't need compute again */ if (mdd_is_tautology(result,0)){ *isExact = TRUE; } return result; } /**Function******************************************************************* Synopsis [Compte a subset of exact pre image.] Description [Compte a subset of exact pre image. If result is exact pre image, isExact is set.] SideEffects [] ******************************************************************************/ mdd_t * Imc_ComputeLowerPreimage( Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact) { if (imcInfo->lowerMethod == Imc_LowerSubsetTR_c){ return Imc_ComputeLowerPreimageBySubsetTR(imcInfo, rangeCareStates, targetStates, isExact); }else if (imcInfo->lowerMethod == Imc_LowerUniversalQuantification_c){ return Imc_ComputeApproxPreimageByQuantification(imcInfo, rangeCareStates, targetStates, isExact, TRUE); } return NIL(mdd_t); } /**Function******************************************************************* Synopsis [Compte a subset of exact pre image by subsetting some transition sub-relations.] Description [Compte a subset of exact pre image by subsetting some transition sub-relations. If result is exact pre image, isExact is set.] SideEffects [] ******************************************************************************/ mdd_t * Imc_ComputeLowerPreimageBySubsetTR( Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact) { mdd_t *tempMdd, *result; mdd_t *toStates; *isExact = TRUE; if (mdd_is_tautology(targetStates,0)){ return mdd_zero(imcInfo->mddMgr); } if (mdd_is_tautology(targetStates, 1)){ return mdd_one(imcInfo->mddMgr); } /* * T_i is T_i for all included latches. */ /*arrayOfMdd = array_alloc(mdd_t *, 0); never used, I guess. Chao Wang*/ toStates = mdd_substitute(imcInfo->mddMgr, targetStates, imcInfo->systemInfo->psMddIdArray, imcInfo->systemInfo->nsMddIdArray); /* Not works with partitioned transition relation supportArray = mdd_get_support(imcInfo->mddMgr, targetStates); for(i=0;isystemInfo->excludedPsMddIdTable, (char *)(long)psMddId)){ *isExact = FALSE; } } array_free(supportArray); */ if (st_count(imcInfo->systemInfo->excludedPsMddIdTable)>0){ *isExact = FALSE; } if (imcInfo->lowerSystemInfo->bwdMinimizedRealationArray == NIL(array_t)){ result = Imc_ProductAbstract(imcInfo->mddMgr, imcInfo->lowerSystemInfo->bwdRealationArray, imcInfo->lowerSystemInfo->bwdSmoothVarsArray, toStates); }else{ result = Imc_ProductAbstract(imcInfo->mddMgr, imcInfo->lowerSystemInfo->bwdMinimizedRealationArray, imcInfo->lowerSystemInfo->bwdSmoothVarsArray, toStates); } mdd_free(toStates); if (imcInfo->verbosity == Imc_VerbosityMax_c){ double exactSize, approxSize; tempMdd = mdd_and(result, rangeCareStates, 1, 1); approxSize = mdd_count_onset(imcInfo->mddMgr, result, imcInfo->systemInfo->psMddIdArray); exactSize = mdd_count_onset(imcInfo->mddMgr, tempMdd, imcInfo->systemInfo->psMddIdArray); mdd_free(tempMdd); fprintf(vis_stdout, "IMC : Lower Preimage |S+DC| = %.0f (%10g)\n", approxSize, approxSize); fprintf(vis_stdout, "IMC : Lower Preimage |S| = %.0f (%10g)\n", exactSize, exactSize); } return result; } /**Function******************************************************************** Synopsis [Compute a product of relation array. All variables in smoothVarsMddIdArray are quntified during product.] Description [Compute a product of relation array. All variables in smoothVarsMddIdArray are quntified during product.] SideEffects [] SeeAlso [] ******************************************************************************/ mdd_t * Imc_ProductAbstract( mdd_manager *mddMgr, array_t *relationArray, array_t *smoothVarsMddIdArray, mdd_t *toStates) { int i; mdd_t *product, *tempProd; mdd_t *singleTR; array_t *smoothVars; product = mdd_dup(toStates); for(i=0;iglobalFsm; Ntk_Network_t *network = Fsm_FsmReadNetwork( modelFsm ); char *nodeNameString = Ctlp_FormulaReadVariableName( formula ); char *nodeValueString = Ctlp_FormulaReadValueName( formula ); Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString ); Var_Variable_t *nodeVar; int nodeValue; graph_t *modelPartition; vertex_t *partitionVertex; Mvf_Function_t *MVF; Imc_NodeInfo_t *nodeInfo; if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){ fprintf(vis_stdout, "** imc error : Atomic nodeinfo is not initilize.\n"); return 0; } nodeVar = Ntk_NodeReadVariable( node ); if ( Var_VariableTestIsSymbolic( nodeVar ) ){ nodeValue = Var_VariableReadIndexFromSymbolicValue( nodeVar, nodeValueString ); } else { nodeValue = atoi( nodeValueString ); } modelPartition = Part_NetworkReadPartition( network ); if ( !( partitionVertex = Part_PartitionFindVertexByName( modelPartition, nodeNameString ) )) { lsGen tmpGen; Ntk_Node_t *tmpNode; array_t *mvfArray; array_t *tmpRoots = array_alloc( Ntk_Node_t *, 0 ); st_table *tmpLeaves = st_init_table( st_ptrcmp, st_ptrhash ); array_insert_last( Ntk_Node_t *, tmpRoots, node ); Ntk_NetworkForEachCombInput( network, tmpGen, tmpNode ) { st_insert( tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED ); } mvfArray = Ntm_NetworkBuildMvfs( network, tmpRoots, tmpLeaves, NIL(mdd_t) ); MVF = array_fetch( Mvf_Function_t *, mvfArray, 0 ); array_free( tmpRoots ); st_free_table( tmpLeaves ); array_free( mvfArray ); tmpMdd = Mvf_FunctionReadComponent( MVF, nodeValue ); resultMdd = mdd_dup( tmpMdd ); Mvf_FunctionFree( MVF ); } else { MVF = Part_VertexReadFunction( partitionVertex ); tmpMdd = Mvf_FunctionReadComponent( MVF, nodeValue ); resultMdd = mdd_dup( tmpMdd ); } tmpMdd = bdd_minimize(resultMdd, imcInfo->modelCareStates); mdd_free(resultMdd); resultMdd = tmpMdd; nodeInfo->upperSat = resultMdd; nodeInfo->lowerSat = mdd_dup(resultMdd); nodeInfo->upperDone = TRUE; nodeInfo->lowerDone = TRUE; nodeInfo->isExact = TRUE; return 1; } /**Function******************************************************************** Synopsis [Compute TRUE or FALSE expression.] Description [Compute TRUE or FALSE expression.] SideEffects [] ******************************************************************************/ int ImcModelCheckTrueFalseFormula( Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isTrue) { mdd_t *resultMdd; Imc_NodeInfo_t *nodeInfo; if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){ fprintf(vis_stdout, "** imc error : TRUE or FALSE nodeinfo is not initilize.\n"); return 0; } /* * Already computed, then return. */ if (nodeInfo->isExact) return 1; if (isTrue) resultMdd = mdd_one(imcInfo->mddMgr); else resultMdd = mdd_zero(imcInfo->mddMgr); nodeInfo->upperSat = resultMdd; nodeInfo->lowerSat = mdd_dup(resultMdd); nodeInfo->upperDone = TRUE; nodeInfo->lowerDone = TRUE; nodeInfo->isExact = TRUE; return 1; } /**Function******************************************************************** Synopsis [Compute NOT expression.] Description [Compute NOT expression.] SideEffects [] ******************************************************************************/ int ImcModelCheckNotFormula( Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper ) { mdd_t *upperSAT, *lowerSAT; Ctlp_Formula_t *leftChild; Imc_NodeInfo_t *nodeInfo, *leftNodeInfo; if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){ return 0; } leftChild = Ctlp_FormulaReadLeftChild(formula); if (!st_lookup(imcInfo->nodeInfoTable, leftChild, &leftNodeInfo)){ fprintf(vis_stdout, "** imc error : NOT nodeinfo is not initilize.\n"); return 0; } if (isUpper){ if (leftNodeInfo->lowerSat == NIL(mdd_t)){ return 0; }else{ if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat); upperSAT = mdd_not(leftNodeInfo->lowerSat); nodeInfo->upperSat = upperSAT; nodeInfo->upperDone = TRUE; } }else{ if (leftNodeInfo->upperSat == NIL(mdd_t)){ return 0; }else{ if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat); lowerSAT = mdd_not(leftNodeInfo->upperSat); nodeInfo->lowerSat = lowerSAT; nodeInfo->lowerDone = TRUE; } } if (leftNodeInfo->isExact){ nodeInfo->isExact = TRUE; if (isUpper){ if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat); nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat); nodeInfo->lowerDone = TRUE; }else{ if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat); nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat); nodeInfo->upperDone = TRUE; } } return 1; } /**Function******************************************************************** Synopsis [Compute AND expression.] Description [Compute AND expression.] SideEffects [] ******************************************************************************/ int ImcModelCheckAndFormula( Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper) { mdd_t *tmpMdd; mdd_t *upperSat, *lowerSat; Ctlp_Formula_t *leftChild, *rightChild; Imc_NodeInfo_t *nodeInfo, *leftNodeInfo, *rightNodeInfo; if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){ return 0; } /* * Already computed, then return. */ if (nodeInfo->isExact) return 1; leftChild = Ctlp_FormulaReadLeftChild(formula); rightChild = Ctlp_FormulaReadRightChild(formula); if (!st_lookup(imcInfo->nodeInfoTable, leftChild, &leftNodeInfo)){ fprintf(vis_stdout, "** imc error : AND left nodeinfo is not initilize.\n"); return 0; } if (!st_lookup(imcInfo->nodeInfoTable, rightChild, &rightNodeInfo)){ fprintf(vis_stdout, "** imc error : AND right nodeinfo is not initilize.\n"); return 0; } /* * Already computed, then return. */ if (isUpper){ if ((leftNodeInfo->upperSat == NIL(mdd_t))|| (rightNodeInfo->upperSat == NIL(mdd_t))){ fprintf(vis_stdout, "** imc error : AND child nodeinfo->upperSat is not computed.\n"); return 0; }else{ tmpMdd = mdd_and(leftNodeInfo->upperSat,rightNodeInfo->upperSat, 1, 1); upperSat = bdd_minimize(tmpMdd, imcInfo->modelCareStates); mdd_free(tmpMdd); if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat); nodeInfo->upperSat = upperSat; nodeInfo->upperDone = TRUE; } }else{ if ((leftNodeInfo->lowerSat == NIL(mdd_t))|| (rightNodeInfo->lowerSat == NIL(mdd_t))){ fprintf(vis_stdout, "** imc error : AND child nodeinfo->lowerSat is not computed.\n"); return 0; }else{ tmpMdd = mdd_and(leftNodeInfo->lowerSat,rightNodeInfo->lowerSat, 1, 1); lowerSat = bdd_minimize(tmpMdd, imcInfo->modelCareStates); mdd_free(tmpMdd); if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat); nodeInfo->lowerSat = lowerSat; nodeInfo->lowerDone = TRUE; } } if ((leftNodeInfo->isExact) && (rightNodeInfo->isExact)){ nodeInfo->isExact = TRUE; if (isUpper){ if (nodeInfo->lowerSat != NIL(mdd_t)) mdd_free(nodeInfo->lowerSat); nodeInfo->lowerSat = mdd_dup(nodeInfo->upperSat); nodeInfo->lowerDone = TRUE; }else{ if (nodeInfo->upperSat != NIL(mdd_t)) mdd_free(nodeInfo->upperSat); nodeInfo->upperSat = mdd_dup(nodeInfo->lowerSat); nodeInfo->upperDone = TRUE; } } return 1; } /**Function******************************************************************** Synopsis [Print latch names in an upper approximate system.] Description [Print latch names in an upper approximate system.] SideEffects [] ******************************************************************************/ void ImcPrintLatchInApproxSystem( Imc_Info_t *imcInfo) { int i, index; char *name; array_t *includedLatchIndex = imcInfo->systemInfo->includedLatchIndex; fprintf(vis_stdout, "Latches in approximate system\n"); fprintf(vis_stdout, "-----------------------------\n"); for(i=0;isystemInfo->latchNameArray, index); fprintf(vis_stdout, "%s\n", name); } } /**Function******************************************************************** Synopsis [Free node info table.] Description [Free node info table.] SideEffects [] ******************************************************************************/ void ImcNodeInfoTableFree( st_table *nodeInfoTable) { Ctlp_Formula_t *formula; Imc_NodeInfo_t *nodeInfo; st_generator *stGen; st_foreach_item(nodeInfoTable, stGen, &formula, &nodeInfo){ Imc_NodeInfoFree(nodeInfo); } st_free_table(nodeInfoTable); } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Compare two strings] SideEffects [] ******************************************************************************/ static int stringCompare( const void * s1, const void * s2) { return(strcmp(*(char **)s1, *(char **)s2)); }