src/imc/imcImc.c File Reference

#include "imcInt.h"
#include "part.h"
#include "img.h"
#include "ntm.h"

Include dependency graph for imcImc.c:

Go to the source code of this file.

Functions
static int	stringCompare (const void *s1, const void *s2)
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_VerificationResult	Imc_ImcVerifyFormula (Imc_Info_t *imcInfo, Ctlp_Formula_t *formula)
Imc_VerificationResult	Imc_SatCheck (Imc_Info_t *imcInfo, Ctlp_Formula_t *formula)
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)
void	Imc_ImcInfoFree (Imc_Info_t *imcInfo)
void	Imc_SystemInfoInitialize (Imc_Info_t *imcInfo, st_table *globalLatchNameTable, st_table *initialLatchNameTable)
void	Imc_SystemInfoFree (Imc_SystemInfo_t *systemInfo)
void	Imc_ImcSystemInfoUpdate (Imc_Info_t *imcInfo, st_table *newLatchNameTable)
void	Imc_UpperSystemInfoInitialize (Imc_Info_t *imcInfo, st_table *latchNameTable)
void	Imc_UpperSystemMinimize (Imc_Info_t *imcInfo, mdd_t *careStates)
void	Imc_UpperSystemInfoFree (Imc_UpperSystemInfo_t *upperSystem)
void	Imc_LowerSystemInfoInitialize (Imc_Info_t *imcInfo, st_table *latchNameTable)
void	Imc_LowerSystemMinimize (Imc_Info_t *imcInfo, mdd_t *careStates)
void	Imc_LowerSystemInfoFree (Imc_LowerSystemInfo_t *lowerSystem)
Imc_NodeInfo_t *	Imc_NodeInfoInitialize (Imc_Polarity polarity)
void	Imc_NodeInfoReset (Imc_Info_t *imcInfo)
void	Imc_NodeInfoFree (Imc_NodeInfo_t *nodeInfo)
void	Imc_ImcPrintSystemSize (Imc_Info_t *imcInfo)
void	Imc_ImcPrintApproxSystemSize (Imc_Info_t *imcInfo)
mdd_t *	Imc_GetUpperSat (Imc_Info_t *imcInfo, Ctlp_Formula_t *formula)
mdd_t *	Imc_GetLowerSat (Imc_Info_t *imcInfo, Ctlp_Formula_t *formula)
int	Imc_ImcEvaluateCTLFormula (Imc_Info_t *imcInfo, Ctlp_Formula_t *ctlFormula, Imc_Polarity polarity)
int	Imc_ImcEvaluateEXApprox (Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation)
int	Imc_ImcEvaluateEUApprox (Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation)
int	Imc_ImcEvaluateEGApprox (Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper, boolean isRecomputation)
mdd_t *	Imc_ComputeUpperPreimage (Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact)
mdd_t *	Imc_ComputeApproxPreimageByQuantification (Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact, boolean computeLower)
mdd_t *	Imc_ComputeLowerPreimage (Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact)
mdd_t *	Imc_ComputeLowerPreimageBySubsetTR (Imc_Info_t *imcInfo, mdd_t *rangeCareStates, mdd_t *targetStates, boolean *isExact)
mdd_t *	Imc_ProductAbstract (mdd_manager *mddMgr, array_t *relationArray, array_t *smoothVarsMddIdArray, mdd_t *toStates)
array_t *	ImcCreateScheduleArray (Ntk_Network_t *network, Ctlp_Formula_t *formula, boolean dynamicIncrease, Imc_RefineMethod refine, int verbosity, int incrementalSize, Part_CMethod correlationMethod)
int	ImcModelCheckAtomicFormula (Imc_Info_t *imcInfo, Ctlp_Formula_t *formula)
int	ImcModelCheckTrueFalseFormula (Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isTrue)
int	ImcModelCheckNotFormula (Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper)
int	ImcModelCheckAndFormula (Imc_Info_t *imcInfo, Ctlp_Formula_t *formula, boolean isUpper)
void	ImcPrintLatchInApproxSystem (Imc_Info_t *imcInfo)
void	ImcNodeInfoTableFree (st_table *nodeInfoTable)
Variables
static char rcsid[]	UNUSED = "$Id: imcImc.c,v 1.21 2005/04/27 00:13:01 fabio Exp $"

---

Function Documentation

mdd_t* Imc_ComputeApproxPreimageByQuantification	(	Imc_Info_t *	imcInfo,
		mdd_t *	rangeCareStates,
		mdd_t *	targetStates,
		boolean *	isExact,
		boolean	computeLower
	)

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 []

Definition at line 2487 of file imcImc.c.

{
  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;i<array_n(supportArray);i++){
    psMddId = array_fetch(int, supportArray, i);
    if (st_is_member(imcInfo->systemInfo->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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

mdd_t* Imc_ComputeLowerPreimage	(	Imc_Info_t *	imcInfo,
		mdd_t *	rangeCareStates,
		mdd_t *	targetStates,
		boolean *	isExact
	)

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 []

Definition at line 2631 of file imcImc.c.

{
  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

mdd_t* Imc_ComputeLowerPreimageBySubsetTR	(	Imc_Info_t *	imcInfo,
		mdd_t *	rangeCareStates,
		mdd_t *	targetStates,
		boolean *	isExact
	)

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 []

Definition at line 2661 of file imcImc.c.

{
  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;i<array_n(supportArray);i++){
    psMddId = array_fetch(int, supportArray,i);

    if (st_is_member(imcInfo->systemInfo->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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

mdd_t* Imc_ComputeUpperPreimage	(	Imc_Info_t *	imcInfo,
		mdd_t *	rangeCareStates,
		mdd_t *	targetStates,
		boolean *	isExact
	)

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 []

Definition at line 2461 of file imcImc.c.

{
  if (imcInfo->upperMethod == Imc_UpperExistentialQuantification_c){
    return Imc_ComputeApproxPreimageByQuantification(imcInfo, rangeCareStates,
             targetStates, isExact, FALSE);
  }

  return NIL(mdd_t);
}

Here is the call graph for this function:

Here is the caller graph for this function:

mdd_t* Imc_GetLowerSat	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	formula
	)

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 []

Definition at line 1614 of file imcImc.c.

{
  Imc_NodeInfo_t *nodeInfo;

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    return NIL(mdd_t); 
  }

  return nodeInfo->lowerSat;
}

mdd_t* Imc_GetUpperSat	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	formula
	)

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 []

Definition at line 1588 of file imcImc.c.

{
  Imc_NodeInfo_t *nodeInfo;

  if (!st_lookup(imcInfo->nodeInfoTable, formula, &nodeInfo)){
    return NIL(mdd_t); 
  }

  return nodeInfo->upperSat;
}

int Imc_ImcEvaluateCTLFormula	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	ctlFormula,
		Imc_Polarity	polarity
	)

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 []

Definition at line 1641 of file imcImc.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int Imc_ImcEvaluateEGApprox	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	formula,
		boolean	isUpper,
		boolean	isRecomputation
	)

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 []

Definition at line 2220 of file imcImc.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int Imc_ImcEvaluateEUApprox	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	formula,
		boolean	isUpper,
		boolean	isRecomputation
	)

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 []

Definition at line 1979 of file imcImc.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int Imc_ImcEvaluateEXApprox	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	formula,
		boolean	isUpper,
		boolean	isRecomputation
	)

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 []

Definition at line 1783 of file imcImc.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

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
	)

AutomaticEnd Function********************************************************************

Synopsis [Verify a formula with incremental refinement.]

Description [Verify a formula with incremental refinement.]

SideEffects []

SeeAlso []

Definition at line 76 of file imcImc.c.

{
  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 */
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Imc_ImcInfoFree

(

Imc_Info_t *

imcInfo

)

Function********************************************************************

Synopsis [Free an imcInfo structure for the given method.]

Description [Free an imcInfo structure for the given method.]

SideEffects []

SeeAlso []

Definition at line 537 of file imcImc.c.

{
  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

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
	)

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 []

Definition at line 301 of file imcImc.c.

{
  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Imc_ImcPrintApproxSystemSize

(

Imc_Info_t *

imcInfo

)

Function********************************************************************

Synopsis [Print upper-system size.]

Description [Print upper-system size by multi-value and boolean value latch.]

SideEffects []

SeeAlso []

Definition at line 1547 of file imcImc.c.

{
  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;i<array_n(includedLatchIndex);i++){
    index = array_fetch(int,includedLatchIndex, i); 
    psMddId = array_fetch(int, psMddIdArray, index); 
    array_insert(int, includedPsMddIdArray, i, psMddId);
  }
 
  includedBooleanVars = mdd_id_array_to_bdd_id_array(imcInfo->mddMgr,
                        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);  
}

Here is the caller graph for this function:

void Imc_ImcPrintSystemSize

(

Imc_Info_t *

imcInfo

)

Function********************************************************************

Synopsis [Print global system size.]

Description [Print global system size by multi-value and boolean value latch.]

SideEffects []

SeeAlso []

Definition at line 1518 of file imcImc.c.

{
  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);  
}

Here is the caller graph for this function:

void Imc_ImcSystemInfoUpdate	(	Imc_Info_t *	imcInfo,
		st_table *	newLatchNameTable
	)

Function********************************************************************

Synopsis [Update a system info.]

Description [Update a system info. All variables in newLatchNameTable are now computed exactly.]

SideEffects []

SeeAlso []

Definition at line 876 of file imcImc.c.

{
  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;i<array_n(imcInfo->systemInfo->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));
    }        
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Imc_VerificationResult Imc_ImcVerifyFormula	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	formula
	)

Function********************************************************************

Synopsis [Verify a formula.]

Description [Verify a formula.]

SideEffects []

SeeAlso []

Definition at line 228 of file imcImc.c.

{
  Imc_VerificationResult result;

  if (!Imc_ImcEvaluateCTLFormula(imcInfo, formula, Imc_PolarityPos_c)){
    return Imc_VerificationError_c;
  }

  result = Imc_SatCheck(imcInfo, formula);

  return result;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Imc_LowerSystemInfoFree

(

Imc_LowerSystemInfo_t *

lowerSystem

)

Function********************************************************************

Synopsis [Free a lower-bound approximate system info.]

Description [Free a lower-bound approximate system info.]

SideEffects []

SeeAlso []

Definition at line 1349 of file imcImc.c.

{
  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; i<array_n(lowerSystem->bwdSmoothVarsArray);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;
}

Here is the caller graph for this function:

void Imc_LowerSystemInfoInitialize	(	Imc_Info_t *	imcInfo,
		st_table *	latchNameTable
	)

Function********************************************************************

Synopsis [Initilalize a lower-bound approximate system info.]

Description [Initilalize a lower-bound approximate system info.]

SideEffects []

SeeAlso []

Definition at line 1194 of file imcImc.c.

{
  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;i<array_n(imcInfo->upperSystemInfo->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;i<array_n(latchNameArray);i++){
    name = array_fetch(char *, latchNameArray, i);
    st_lookup_int(globalLatchNameTable, name, (int *)&index);
    if (st_lookup(latchNameTable, name, NIL(char *))){
      singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Imc_LowerSystemMinimize	(	Imc_Info_t *	imcInfo,
		mdd_t *	careStates
	)

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 []

Definition at line 1293 of file imcImc.c.

{
  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;i<array_n(lowerSystem->bwdRealationArray);i++){
      array_insert(mdd_t *, lowerSystem->bwdMinimizedRealationArray, i, NIL(mdd_t));
    }
  } 

  for (i=0;i<array_n(lowerSystem->bwdRealationArray);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));
  }
}

Here is the caller graph for this function:

void Imc_NodeInfoFree

(

Imc_NodeInfo_t *

nodeInfo

)

Function********************************************************************

Synopsis [Free node info.]

Description [Free node info.]

SideEffects []

SeeAlso []

Definition at line 1478 of file imcImc.c.

{
  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);
}

Here is the caller graph for this function:

Imc_NodeInfo_t* Imc_NodeInfoInitialize

(

Imc_Polarity

polarity

)

Function********************************************************************

Synopsis [Initilalize node info.]

Description [Initilalize node info.]

SideEffects []

SeeAlso []

Definition at line 1394 of file imcImc.c.

{
  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;
}

Here is the caller graph for this function:

void Imc_NodeInfoReset

(

Imc_Info_t *

imcInfo

)

Function********************************************************************

Synopsis [Reset node info.]

Description [Reset node info.]

SideEffects []

SeeAlso []

Definition at line 1429 of file imcImc.c.

{
  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);
    }   
  }
}

Here is the caller graph for this function:

mdd_t* Imc_ProductAbstract	(	mdd_manager *	mddMgr,
		array_t *	relationArray,
		array_t *	smoothVarsMddIdArray,
		mdd_t *	toStates
	)

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 []

Definition at line 2752 of file imcImc.c.

{
  int i;
  mdd_t *product, *tempProd;
  mdd_t *singleTR;
  array_t *smoothVars;

  product = mdd_dup(toStates);

  for(i=0;i<array_n(relationArray);i++){
    singleTR = array_fetch(mdd_t *, relationArray, i);
    smoothVars = array_fetch(array_t*, smoothVarsMddIdArray, i);
    if (array_n(smoothVars) == 0){
      tempProd = mdd_and(product, singleTR, 1, 1);
    }else{
      tempProd = bdd_and_smooth(product, singleTR, smoothVars);
    }
    mdd_free(product);
    product = tempProd;
  }
  if (i < array_n(smoothVarsMddIdArray)) {
    smoothVars = array_fetch(array_t*, smoothVarsMddIdArray, i);
    tempProd = bdd_smooth(product, smoothVars);
    mdd_free(product);
    product = tempProd;
  }

  return product;  
}

Here is the caller graph for this function:

Imc_VerificationResult Imc_SatCheck	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	formula
	)

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 []

Definition at line 258 of file imcImc.c.

{
  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;
}

Here is the caller graph for this function:

void Imc_SystemInfoFree

(

Imc_SystemInfo_t *

systemInfo

)

Function********************************************************************

Synopsis [Free a system info.]

Description [Free a system info.]

SideEffects []

SeeAlso []

Definition at line 799 of file imcImc.c.

{
  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;i<array_n(systemInfo->TRArray);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;i<array_n(systemInfo->lowerTRArray);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);
}

Here is the caller graph for this function:

void Imc_SystemInfoInitialize	(	Imc_Info_t *	imcInfo,
		st_table *	globalLatchNameTable,
		st_table *	initialLatchNameTable
	)

Function********************************************************************

Synopsis [Initilalize a system info.]

Description [Initilalize a system info.]

SideEffects []

SeeAlso []

Definition at line 584 of file imcImc.c.

{
  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;i<array_n(latchNameArray);i++){
    name = array_fetch(char *, latchNameArray, i);
    node = Ntk_NetworkFindNodeByName(network, name);
    psMddId = Ntk_NodeReadMddId(node);
    nsMddId = Ntk_NodeReadMddId(Ntk_NodeReadShadow(node));

    dataInputName = Ntk_NodeReadName(Ntk_LatchReadDataInput(node));

    if (st_is_member(initialLatchNameTable, name)) { 
      vertex = Part_PartitionFindVertexByName(partition, dataInputName);
      mvf = Part_VertexReadFunction(vertex);      
      singleTR = Mvf_FunctionBuildRelationWithVariable(mvf, nsMddId);
      array_insert(mdd_t *, TRArray, i, 
                   bdd_minimize(singleTR, imcInfo->modelCareStates));
      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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Imc_UpperSystemInfoFree

(

Imc_UpperSystemInfo_t *

upperSystem

)

Function********************************************************************

Synopsis [Free a upper-bound approximate system info.]

Description [Free a upper-bound approximate system info.]

SideEffects []

SeeAlso []

Definition at line 1140 of file imcImc.c.

{
  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; i<array_n(upperSystem->bwdSmoothVarsArray);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;
}

Here is the caller graph for this function:

void Imc_UpperSystemInfoInitialize	(	Imc_Info_t *	imcInfo,
		st_table *	latchNameTable
	)

Function********************************************************************

Synopsis [Initilalize an upper-bound approximate system info.]

Description [Initilalize an upper-bound approximate system info.]

SideEffects []

SeeAlso []

Definition at line 1012 of file imcImc.c.

{
  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;i<array_n(globalLatchNameArray);i++){
    name = array_fetch(char *, globalLatchNameArray, i);  
    if (st_is_member(latchNameTable, name)){
      st_lookup_int(globalLatchNameTable, name, (int *)&index);
      singleTR = array_fetch(mdd_t *, imcInfo->systemInfo->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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Imc_UpperSystemMinimize	(	Imc_Info_t *	imcInfo,
		mdd_t *	careStates
	)

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 []

Definition at line 1084 of file imcImc.c.

{
  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;i<array_n(upperSystem->bwdRealationArray);i++){
      array_insert(mdd_t *, upperSystem->bwdMinimizedRealationArray, i, NIL(mdd_t));
    }
  }

  for (i=0;i<array_n(upperSystem->bwdRealationArray);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;
}

Here is the caller graph for this function:

array_t* ImcCreateScheduleArray	(	Ntk_Network_t *	network,
		Ctlp_Formula_t *	formula,
		boolean	dynamicIncrease,
		Imc_RefineMethod	refine,
		int	verbosity,
		int	incrementalSize,
		Part_CMethod	correlationMethod
	)

Function********************************************************************

Synopsis [Create an refinement schedule array.]

Description [If dynamicIncrease is true, the first element of return array includes varibales appered in formula. The size of the first element should be less than or equal to incrementalSize. The second element includes all variables in formula's cone of influence. When dynamicIncrease is false, all vaiables in formula's cone of influence (let's say n variables) are partitioned into ceil(n/incrementalSize) elements. Then one more element which includes all n variables are added to return array.]

SideEffects []

SeeAlso [Part_SubsystemInfo_t]

Definition at line 2809 of file imcImc.c.

{
  array_t               *partitionArray;
  Part_Subsystem_t      *partitionSubsystem;
  Part_SubsystemInfo_t  *subsystemInfo; 
  st_table              *latchNameTable;
  st_table              *latchNameTableSum, *latchNameTableSumCopy;
  int                   i;
  char                  *flagValue;
  st_generator          *stGen;
  char                  *name;
  array_t               *ctlArray;
  double                affinityFactor;
  array_t               *scheduleArray;
  boolean               dynamicAndDependency;
  array_t               *tempArray, *tempArray2;
  int                   count;

  /* affinity factor to decompose state space */
  flagValue = Cmd_FlagReadByName("part_group_affinity_factor");
  if(flagValue != NIL(char)){
    affinityFactor = atof(flagValue); 
  }
  else{
    /* default value */
    affinityFactor = 0.5; 
  }

  if (refine == Imc_RefineSort_c) dynamicAndDependency = TRUE;
  else dynamicAndDependency = FALSE;

  /* 
   * Obtain submachines as array. 
   * The first sub-system includes variables in CTL formulas and other
   * latches are groupted in the same way as Part_PartCreateSubsystems()
   */
  ctlArray = array_alloc(Ctlp_Formula_t *, 1);
  subsystemInfo = Part_PartitionSubsystemInfoInit(network);
  Part_PartitionSubsystemInfoSetBound(subsystemInfo, incrementalSize);
  Part_PartitionSubsystemInfoSetVerbosity(subsystemInfo, verbosity);
  Part_PartitionSubsystemInfoSetCorrelationMethod(subsystemInfo,
    correlationMethod); 
  Part_PartitionSubsystemInfoSetAffinityFactor(subsystemInfo, affinityFactor);
  array_insert(Ctlp_Formula_t *, ctlArray, 0, formula);

  partitionArray = Part_PartCreateSubsystemsWithCTL(subsystemInfo,
                   ctlArray, NIL(array_t), dynamicIncrease,dynamicAndDependency);
  Part_PartitionSubsystemInfoFree(subsystemInfo);
  array_free(ctlArray);
  scheduleArray = array_alloc(st_table *, 0);


  /* 
   * For each partitioned submachines build an FSM. 
   */
  latchNameTableSum = st_init_table(strcmp, st_strhash);
  if (!dynamicAndDependency){
    for (i=0;i<array_n(partitionArray);i++){
      partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, i);
      if (partitionSubsystem != NIL(Part_Subsystem_t)) {
        latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
        st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
          if (!st_lookup(latchNameTableSum, name, NIL(char *))){ 
            st_insert(latchNameTableSum, name, NIL(char));
          }
        }
        Part_PartitionSubsystemFree(partitionSubsystem);
      } 
      latchNameTableSumCopy = st_copy(latchNameTableSum);
      array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
    }
  }else{
    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 0);
    latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
    st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
      st_insert(latchNameTableSum, name, NIL(char));
    }
    latchNameTableSumCopy = st_copy(latchNameTableSum);
    array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
    Part_PartitionSubsystemFree(partitionSubsystem);

    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 1);
    tempArray = array_alloc(char *, 0);    
    if (partitionSubsystem != NIL(Part_Subsystem_t)){
      latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
      st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
        array_insert_last(char *, tempArray, name);
      }
      array_sort(tempArray, stringCompare);
      Part_PartitionSubsystemFree(partitionSubsystem);
    }
    
    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 2);
    tempArray2 = array_alloc(char *, 0);
    if (partitionSubsystem != NIL(Part_Subsystem_t)) {
      latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
      st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
        array_insert_last(char *, tempArray2, name);
      }
      array_sort(tempArray2, stringCompare);
      Part_PartitionSubsystemFree(partitionSubsystem);
    }

    array_append(tempArray, tempArray2);
    array_free(tempArray2);

    count = 0;
    arrayForEachItem(char *, tempArray, i, name){   
      if (!st_lookup(latchNameTableSum, name, NIL(char *))){ 
        st_insert(latchNameTableSum, (char *)name, (char *)0);
        count++;
      }
      if ((count == incrementalSize) && (i < array_n(tempArray)-1)){
        latchNameTableSumCopy = st_copy(latchNameTableSum);
        array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
        count = 0;
      }
    }
    array_free(tempArray);
    latchNameTableSumCopy = st_copy(latchNameTableSum);
    array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
  }

  array_free(partitionArray);
  st_free_table(latchNameTableSum);

  return scheduleArray;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ImcModelCheckAndFormula	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	formula,
		boolean	isUpper
	)

Function********************************************************************

Synopsis [Compute AND expression.]

Description [Compute AND expression.]

SideEffects []

Definition at line 3150 of file imcImc.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ImcModelCheckAtomicFormula	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	formula
	)

Function********************************************************************

Synopsis [Find Mdd for states satisfying Atomic Formula.]

Description [This is a duplicate copy of static function, ModelCheckAtomicFormula(). ]

SideEffects []

Definition at line 2957 of file imcImc.c.

{
  mdd_t * resultMdd;
  mdd_t *tmpMdd;
  Fsm_Fsm_t *modelFsm = imcInfo->globalFsm;
  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;  
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ImcModelCheckNotFormula	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	formula,
		boolean	isUpper
	)

Function********************************************************************

Synopsis [Compute NOT expression.]

Description [Compute NOT expression.]

SideEffects []

Definition at line 3082 of file imcImc.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ImcModelCheckTrueFalseFormula	(	Imc_Info_t *	imcInfo,
		Ctlp_Formula_t *	formula,
		boolean	isTrue
	)

Function********************************************************************

Synopsis [Compute TRUE or FALSE expression.]

Description [Compute TRUE or FALSE expression.]

SideEffects []

Definition at line 3041 of file imcImc.c.

{
  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;
}

Here is the caller graph for this function:

void ImcNodeInfoTableFree

(

st_table *

nodeInfoTable

)

Function********************************************************************

Synopsis [Free node info table.]

Description [Free node info table.]

SideEffects []

Definition at line 3265 of file imcImc.c.

{
  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ImcPrintLatchInApproxSystem

(

Imc_Info_t *

imcInfo

)

Function********************************************************************

Synopsis [Print latch names in an upper approximate system.]

Description [Print latch names in an upper approximate system.]

SideEffects []

Definition at line 3238 of file imcImc.c.

{
  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;i<array_n(includedLatchIndex);i++){
    index = array_fetch(int,includedLatchIndex,i);
    name = array_fetch(char *, imcInfo->systemInfo->latchNameArray, index);
    fprintf(vis_stdout, "%s\n", name);
  }
}

static int stringCompare	(	const void *	s1,
		const void *	s2
	)		[static]

AutomaticStart

Function********************************************************************

Synopsis [Compare two strings]

SideEffects []

Definition at line 3291 of file imcImc.c.

{
  return(strcmp(*(char **)s1, *(char **)s2));
}

Here is the caller graph for this function:

---

Variable Documentation

char rcsid [] UNUSED = "$Id: imcImc.c,v 1.21 2005/04/27 00:13:01 fabio Exp $" [static]

CFile***********************************************************************

FileName [imcImc.c]

PackageName [imc]

Synopsis [Incremental Model Checker.]

Author [Jae-Young Jang <jjang@vlsi.colorado.edu>]

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.]

Definition at line 22 of file imcImc.c.