src/abs/absInternal.c

Go to the documentation of this file.

#include "absInt.h"

static char rcsid[] UNUSED = "$Id: absInternal.c,v 1.30 2005/04/16 04:22:21 fabio Exp $";


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
static int vertexCounter = 0;

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static mdd_t * ComputeEGtrue(Abs_VerificationInfo_t *absInfo, mdd_t *careStates);
static void SelectIdentifierVertices(AbsVertexInfo_t *vertexPtr, array_t *result, st_table *visited);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

Abs_VerificationInfo_t *
Abs_VerificationComputeInfo(
  Ntk_Network_t *network)
{
  Abs_VerificationInfo_t *absInfo;
  Ntk_Node_t            *nodePtr;
  graph_t               *partition;
  mdd_manager           *mddManager;
  st_table              *table;
  lsGen                 lsgen;


  /* Create the data structure to store all the needed info */
  absInfo = AbsVerificationInfoInitialize();

  /* Fill the data structure in */
  AbsVerificationInfoSetNetwork(absInfo, network);
  partition = Part_NetworkReadPartition(network);
  AbsVerificationInfoSetPartition(absInfo, partition);
  mddManager = Part_PartitionReadMddManager(partition);
  AbsVerificationInfoSetMddManager(absInfo, mddManager);
  
  /* Compute the state variable pairs */
  table = st_init_table(st_numcmp, st_numhash);
  Ntk_NetworkForEachLatch(network, lsgen, nodePtr) {
    Ntk_Node_t *latchInputPtr;
    int        mddId, mddId2;
    
    mddId = Ntk_NodeReadMddId(nodePtr);
    latchInputPtr = Ntk_NodeReadShadow(nodePtr);
    mddId2 = Ntk_NodeReadMddId(latchInputPtr);
    st_insert(table, (char *)(long)mddId, (char *)(long)mddId2);
  }
  AbsVerificationInfoSetStateVars(absInfo, table);
  
  /* Compute the quantify variables */
  table = st_init_table(st_numcmp, st_numhash);
  Ntk_NetworkForEachInput(network, lsgen, nodePtr) {
    int mddId;
    
    mddId = Ntk_NodeReadMddId(nodePtr);
    st_insert(table, (char *)(long)mddId, NIL(char));
  }
  AbsVerificationInfoSetQuantifyVars(absInfo, table);
  
  /* Initalize the catalog to detect common expressions */
  AbsVerificationInfoSetCatalog(absInfo, AbsVertexCatalogInitialize());
  
  return absInfo;
} /* End of Abs_VerificationComputeInfo */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

AbsVertexInfo_t *
AbsVertexInitialize(void)
{
  AbsVertexInfo_t *result;

  result = ALLOC(AbsVertexInfo_t, 1);

  AbsVertexSetType(result, false_c);
  AbsVertexSetId(result, vertexCounter++);
  AbsVertexSetSat(result, NIL(mdd_t));
  AbsVertexSetRefs(result, 1);
  AbsVertexSetServed(result, 0);
  AbsVertexSetPolarity(result, FALSE);
  AbsVertexSetDepth(result, -1);
  AbsVertexSetLocalApprox(result, FALSE);
  AbsVertexSetGlobalApprox(result, FALSE);
  AbsVertexSetConstant(result, FALSE);
  AbsVertexSetTrueRefine(result, FALSE);
  AbsVertexSetLeftKid(result, NIL(AbsVertexInfo_t));
  AbsVertexSetRightKid(result, NIL(AbsVertexInfo_t));
  result->parent = lsCreate();
 
  /* Not all of these need to be initialized, but to be sure... */
  AbsVertexSetSolutions(result, NIL(st_table));
  AbsVertexSetVarId(result, 0);
  AbsVertexSetFpVar(result, NIL(AbsVertexInfo_t));
  AbsVertexSetVarId(result, 0);
  AbsVertexSetGoalSet(result, NIL(mdd_t));
  AbsVertexSetRings(result, NIL(array_t));
  AbsVertexSetRingApprox(result, NIL(array_t));
  AbsVertexSetSubApprox(result, NIL(array_t));
  AbsVertexSetUseExtraCareSet(result, FALSE);
  AbsVertexSetName(result, NIL(char));
  AbsVertexSetValue(result, NIL(char));

  return result;
} /* End of AbsVertexInitialize */

void
AbsVertexFree(
  AbsVertexCatalog_t *catalog,
  AbsVertexInfo_t *v,
  AbsVertexInfo_t *fromVertex)
{
  /* Decrement the number of references */
  AbsVertexReadRefs(v)--;

  /* Remove the pointer from its parent to itself */
  if (fromVertex != NIL(AbsVertexInfo_t)) {
    AbsVertexInfo_t *result;
    lsGen listGen;
    lsHandle item, toDelete;
    lsGeneric userData;

    listGen = lsStart(AbsVertexReadParent(v));
    toDelete = (lsHandle) 0;
    while(toDelete == (lsHandle) 0 &&
          lsNext(listGen, &result, &item) == LS_OK) {
      if (result == fromVertex) {
        toDelete = item;
      }
    }
    lsFinish(listGen);

    if (toDelete != (lsHandle)0) {
      lsRemoveItem(toDelete, &userData);
    }
  }

  /* If it is not the last reference we are done */
  if (AbsVertexReadRefs(v) != 0) {
    return;
  }

  /* Vertices that need recursion over the leftKid */
  if (AbsVertexReadType(v) == fixedPoint_c ||
      AbsVertexReadType(v) == and_c ||
      AbsVertexReadType(v) == xor_c ||
      AbsVertexReadType(v) == xnor_c ||
      AbsVertexReadType(v) == not_c ||
      AbsVertexReadType(v) == preImage_c) {
    AbsVertexFree(catalog, AbsVertexReadLeftKid(v), v);
  }
  
  /* Vertices that need recursion over the rightKid */
  if (AbsVertexReadType(v) == and_c ||
      AbsVertexReadType(v) == xor_c ||
      AbsVertexReadType(v) == xnor_c) {
    AbsVertexFree(catalog, AbsVertexReadRightKid(v), v);
  }

  /* Remove the vertex from the catalog */
  AbsCatalogDelete(catalog, v);

  /* The variable vertex does not reference the sat set */
  if (AbsVertexReadType(v) != variable_c && 
      AbsVertexReadSat(v) != NIL(mdd_t)) {
    mdd_free(AbsVertexReadSat(v));
  }

  if (AbsVertexReadType(v) == variable_c && 
      AbsVertexReadGoalSet(v) != NIL(mdd_t)) {
    mdd_free(AbsVertexReadGoalSet(v));
  }
  
  lsDestroy(AbsVertexReadParent(v), (void (*)(lsGeneric))0);

  /* Free the union fields depending on the type of vertex */
  if (AbsVertexReadType(v) == preImage_c) {
    if (AbsVertexReadSolutions(v) != NIL(st_table)) {
      AbsEvalCacheEntry_t *value;
      bdd_node            *key;
      st_generator        *stgen;

      st_foreach_item(AbsVertexReadSolutions(v), stgen, &key, &value) {
        AbsCacheEntryFree(value);
      }
      st_free_table(AbsVertexReadSolutions(v));
    }
  }
  else if (AbsVertexReadType(v) == fixedPoint_c) {
    if (AbsVertexReadRings(v) != NIL(array_t)) {
      mdd_t *unit;
      int i;

      arrayForEachItem(mdd_t *, AbsVertexReadRings(v), i, unit) {
        mdd_free(unit);
      }
      array_free(AbsVertexReadRings(v));
    }
    if (AbsVertexReadRingApprox(v) != NIL(array_t)) {
      array_free(AbsVertexReadRingApprox(v));
    }
    if (AbsVertexReadSubApprox(v) != NIL(array_t)) {
      array_free(AbsVertexReadSubApprox(v));
    }
  }
  else if (AbsVertexReadType(v) == identifier_c) {
    FREE(AbsVertexReadName(v));
    FREE(AbsVertexReadValue(v));
  }

  /* Deallocate the memory for the structure itself */
  FREE(v);
} /* End of AbsVertexFree */

Abs_VerificationInfo_t *
AbsVerificationInfoInitialize(void)
{
  Abs_VerificationInfo_t *result;

  result = ALLOC(Abs_VerificationInfo_t, 1);

  AbsVerificationInfoSetNetwork(result, NIL(Ntk_Network_t));
  AbsVerificationInfoSetPartition(result, NIL(graph_t));
  AbsVerificationInfoSetFsm(result, NIL(Fsm_Fsm_t));
  AbsVerificationInfoSetNumStateVars(result, 0);
  AbsVerificationInfoSetApproxFsm(result, NIL(Fsm_Fsm_t));
  AbsVerificationInfoSetStateVars(result, NIL(st_table));
  AbsVerificationInfoSetQuantifyVars(result, NIL(st_table));
  AbsVerificationInfoSetCareSet(result, NIL(mdd_t));
  AbsVerificationInfoSetTmpCareSet(result, NIL(mdd_t));
  AbsVerificationInfoSetImageCache(result, NIL(st_table));
  AbsVerificationInfoSetMddManager(result, NIL(mdd_manager));
  AbsVerificationInfoSetCatalog(result, NIL(AbsVertexCatalog_t));
  AbsVerificationInfoSetStats(result, AbsStatsInitialize());
  AbsVerificationInfoSetOptions(result, NIL(AbsOptions_t));
  
  return result;
} /* End of AbsVerificationInfoInitialize */

void
AbsVerificationInfoFree(
  Abs_VerificationInfo_t *v)
{
  if (AbsVerificationInfoReadStateVars(v) != NIL(st_table)) {
    st_free_table(AbsVerificationInfoReadStateVars(v));
  }

  if (AbsVerificationInfoReadQuantifyVars(v) != NIL(st_table)) {
    st_free_table(AbsVerificationInfoReadQuantifyVars(v));
  }

  if (AbsVerificationInfoReadImageCache(v) != NIL(st_table)) {
    AbsEvalCacheEntry_t *value;
    bdd_node            *key;
    st_generator        *stgen;

    st_foreach_item(AbsVerificationInfoReadImageCache(v), stgen,
                    &key, &value) {
      AbsCacheEntryFree(value);
    }
    st_free_table(AbsVerificationInfoReadImageCache(v));
  }

  if (AbsVerificationInfoReadCareSet(v) != NIL(mdd_t)) {
    mdd_free(AbsVerificationInfoReadCareSet(v));
  }

  if (AbsVerificationInfoReadTmpCareSet(v) != NIL(mdd_t)) {
    mdd_free(AbsVerificationInfoReadTmpCareSet(v));
  }

  if (AbsVerificationInfoReadCatalog(v) != NIL(AbsVertexCatalog_t)) {
    AbsVertexCatalogFree(AbsVerificationInfoReadCatalog(v));
  }

  AbsStatsFree(AbsVerificationInfoReadStats(v));

  FREE(v);

  /* 
   * The options field is not freed since it is assumed that it has been
   * allocated outside the AbsVerificationInitialize procedure
   */

  return;
} /* End of AbsVerificationInfoFree */

AbsOptions_t *
AbsOptionsInitialize(void)
{
  AbsOptions_t *result;

  result = ALLOC(AbsOptions_t, 1);

  AbsOptionsSetVerbosity(result, 0);
  AbsOptionsSetTimeOut(result, 0);
  AbsOptionsSetFileName(result, NIL(char));
  AbsOptionsSetReachability(result, FALSE);
  AbsOptionsSetFairFileName(result, NIL(char));
  AbsOptionsSetExact(result, FALSE);
  AbsOptionsSetPrintStats(result, FALSE);
  AbsOptionsSetMinimizeIterate(result, FALSE);
  AbsOptionsSetNegateFormula(result, FALSE);
  AbsOptionsSetPartApprox(result, FALSE);

  return result;
} /* End of AbsOptionsInitialize */

void
AbsOptionsFree(AbsOptions_t *unit)
{
  if (AbsOptionsReadFileName(unit) != NIL(char)) {
    FREE(AbsOptionsReadFileName(unit));
  }
  
  if (AbsOptionsReadFairFileName(unit) != NIL(char)) {
    FREE(AbsOptionsReadFairFileName(unit));
  }

  FREE(unit);
  
  return;
} /* End of AbsOptionsInitialize */


AbsStats_t *
AbsStatsInitialize(void)
{
  AbsStats_t *result;

  result = ALLOC(AbsStats_t, 1);
  
  AbsStatsSetNumReorderings(result, 0);
  AbsStatsSetEvalFixedPoint(result, 0);
  AbsStatsSetEvalAnd(result, 0);
  AbsStatsSetEvalNot(result, 0);
  AbsStatsSetEvalPreImage(result, 0);
  AbsStatsSetEvalIdentifier(result, 0);
  AbsStatsSetEvalVariable(result, 0);
  AbsStatsSetRefineFixedPoint(result, 0);
  AbsStatsSetRefineAnd(result, 0);
  AbsStatsSetRefineNot(result, 0);
  AbsStatsSetRefinePreImage(result, 0);
  AbsStatsSetRefineIdentifier(result, 0);
  AbsStatsSetRefineVariable(result, 0);
  AbsStatsSetExactPreImage(result, 0);
  AbsStatsSetApproxPreImage(result, 0);
  AbsStatsSetExactImage(result, 0);
  AbsStatsSetPreImageCacheEntries(result, 0);
  AbsStatsSetImageCacheEntries(result, 0);
  AbsStatsSetImageCpuTime(result, 0);
  AbsStatsSetPreImageCpuTime(result, 0);
  AbsStatsSetAppPreCpuTime(result, 0);

  return result;

} /* End of AbsStatsInitialize */

void
AbsStatsFree(
  AbsStats_t *unit)
{
  FREE(unit);
} /* End of AbsStatsFree */

AbsEvalCacheEntry_t *
AbsCacheEntryInitialize(void)
{
  AbsEvalCacheEntry_t *result;

  result = ALLOC(AbsEvalCacheEntry_t, 1);

  AbsEvalCacheEntrySetKey(result, NIL(mdd_t));
  AbsEvalCacheEntrySetApprox(result, FALSE);
  AbsEvalCacheEntrySetComplement(result, 0);
  AbsEvalCacheEntrySetResult(result, NIL(mdd_t));
  AbsEvalCacheEntrySetCareSet(result, NIL(mdd_t));

  return result;
} /* End of AbsCacheEntryInitialize */

void
AbsCacheEntryFree(
  AbsEvalCacheEntry_t *unit)
{
  mdd_free(AbsEvalCacheEntryReadKey(unit));
  mdd_free(AbsEvalCacheEntryReadResult(unit));
  mdd_free(AbsEvalCacheEntryReadCareSet(unit));

  FREE(unit);
} /* End of AbsCacheEntryFree */

void
AbsEvalCacheInsert(
  st_table *solutions,
  mdd_t *key,
  mdd_t *result,
  mdd_t *careSet,
  boolean approx,
  boolean replace)
{
  AbsEvalCacheEntry_t *entry;
  int                 complement;
  bdd_node            *f;

  entry = NIL(AbsEvalCacheEntry_t);
  f = bdd_get_node(key, &complement);

  /* If the replacement is required, delete the element from the table */
  if (replace) {
    st_delete(solutions, &f, &entry);

    mdd_free(AbsEvalCacheEntryReadKey(entry));
    mdd_free(AbsEvalCacheEntryReadResult(entry));
    mdd_free(AbsEvalCacheEntryReadCareSet(entry));
  }

  assert(!st_is_member(solutions, (char *)f));

  if (entry == NIL(AbsEvalCacheEntry_t)) {
    entry = AbsCacheEntryInitialize();
  }

  AbsEvalCacheEntrySetKey(entry, mdd_dup(key));
  AbsEvalCacheEntrySetApprox(entry, approx);
  AbsEvalCacheEntrySetComplement(entry, complement);
  AbsEvalCacheEntrySetResult(entry, mdd_dup(result));
  AbsEvalCacheEntrySetCareSet(entry, mdd_dup(careSet));
  
  /* Insert the new entry in the cache */
  st_insert(solutions, (char *)f, (char *)entry);

  return;
} /* End of AbsEvalCacheInsert */

boolean
AbsEvalCacheLookup(
  st_table *solutions,
  mdd_t *key,
  mdd_t *careSet,
  boolean approx,
  mdd_t **result,
  boolean *storedApprox)
{
  AbsEvalCacheEntry_t *entry;
  bdd_node            *f;
  int                 complement;
  
  f = bdd_get_node(key, &complement);

  if (st_lookup(solutions, f, &entry)) {
    if (complement == AbsEvalCacheEntryReadComplement(entry) &&
        (approx || !AbsEvalCacheEntryReadApprox(entry)) &&
        mdd_lequal(careSet, AbsEvalCacheEntryReadCareSet(entry), 1, 1)) {
      *result = AbsEvalCacheEntryReadResult(entry);
      if (storedApprox != 0) {
        *storedApprox = AbsEvalCacheEntryReadApprox(entry);
      }
      return TRUE;
    }
    else {
      st_delete(solutions, &f, &entry);
      AbsCacheEntryFree(entry);
    }
  }

  return FALSE;
} /* End of AbsEvalCacheLookup */

void
AbsVerificationFlushCache(
  Abs_VerificationInfo_t *absInfo)
{
  AbsEvalCacheEntry_t *value;
  st_table            *table;
  bdd_node            *key;
  st_generator        *stgen;

  table = AbsVerificationInfoReadImageCache(absInfo);

  if (table == NIL(st_table)) {
    return;
  }

  st_foreach_item(table, stgen, &key, &value) {
    AbsCacheEntryFree(value);
  }

  st_free_table(table);
  AbsVerificationInfoSetImageCache(absInfo, NIL(st_table));

  return;
} /* End of AbsVerificationFlushCache */

void
AbsVertexFlushCache(
  AbsVertexInfo_t *vertexPtr)
{
  if (AbsVertexReadType(vertexPtr) == preImage_c) {
    if (AbsVertexReadSolutions(vertexPtr) != NIL(st_table)) {
      AbsEvalCacheEntry_t *value;
      bdd_node            *key;
      st_generator        *stgen;
      
      st_foreach_item(AbsVertexReadSolutions(vertexPtr), stgen, &key,
                      &value) {
        AbsCacheEntryFree(value);
      }
      st_free_table(AbsVertexReadSolutions(vertexPtr));
      AbsVertexSetSolutions(vertexPtr, NIL(st_table));
    }
  }

  if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
    AbsVertexFlushCache(AbsVertexReadLeftKid(vertexPtr));
  }

  if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) {
    AbsVertexFlushCache(AbsVertexReadRightKid(vertexPtr));
  }

  return;
} /* End of AbsVertexFlushCache */

mdd_t *
AbsImageReadOrCompute(
  Abs_VerificationInfo_t *absInfo,
  Img_ImageInfo_t *imageInfo,
  mdd_t *set,
  mdd_t *careSet
)
{
  AbsEvalCacheEntry_t *entry;
  st_table            *table;
  bdd_node            *f;
  mdd_t               *result;
  long                cpuTime;
  int                 complement;

  entry = NIL(AbsEvalCacheEntry_t);
  table = AbsVerificationInfoReadImageCache(absInfo);
  f = bdd_get_node(set, &complement);

  /* See if the table has been created */
  if (table == NIL(st_table)) {
    table = st_init_table(st_ptrcmp, st_ptrhash);
    AbsVerificationInfoSetImageCache(absInfo, table);
  }
  else {
    /* Look up for the operation */
    if (st_lookup(table, f, &entry)) {
      if (complement == AbsEvalCacheEntryReadComplement(entry) &&
          mdd_lequal(careSet, AbsEvalCacheEntryReadCareSet(entry), 1, 1)) {
        result = mdd_dup(AbsEvalCacheEntryReadResult(entry));
        return result;
      }
      else {
        st_delete(table, &f, &entry);

        mdd_free(AbsEvalCacheEntryReadKey(entry));
        mdd_free(AbsEvalCacheEntryReadResult(entry));
        mdd_free(AbsEvalCacheEntryReadCareSet(entry));
      }
    }
  }

  /* The result has not been found. Compute it and insert it in the cache */
  cpuTime = util_cpu_time();
  result = Img_ImageInfoComputeFwdWithDomainVars(imageInfo, set, set, careSet);
  AbsStatsReadImageCpuTime(AbsVerificationInfoReadStats(absInfo))+= 
    util_cpu_time() - cpuTime;
  AbsStatsReadExactImage(AbsVerificationInfoReadStats(absInfo))++;

  if (entry == NIL(AbsEvalCacheEntry_t)) {
    entry = AbsCacheEntryInitialize();
  }

  AbsEvalCacheEntrySetKey(entry, mdd_dup(set));
  AbsEvalCacheEntrySetComplement(entry, complement);
  AbsEvalCacheEntrySetResult(entry, mdd_dup(result));
  AbsEvalCacheEntrySetCareSet(entry, mdd_dup(careSet));
  
  /* Insert the new entry in the cache */
  st_insert(table, (char *)f, (char *)entry);

  AbsStatsReadImageCacheEntries(AbsVerificationInfoReadStats(absInfo))++;

  return result;
} /* End of AbsImageReadOrCompute */

array_t *
AbsFormulaArrayVerify(
  Abs_VerificationInfo_t *absInfo,
  array_t *formulaArray)
{
  AbsOptions_t    *options;
  AbsVertexInfo_t *formulaPtr;
  Fsm_Fsm_t       *fsm;
  array_t         *result;
  mdd_manager     *mddManager;
  int             fIndex;
  int             numReorderings;

  /* Initialize some variables */
  options = AbsVerificationInfoReadOptions(absInfo);
  mddManager = AbsVerificationInfoReadMddManager(absInfo);
  numReorderings = bdd_read_reorderings(mddManager);
  
  /* Print the configuration of the system */
  if (AbsOptionsReadVerbosity(options) & ABS_VB_PIFF) {
    (void) fprintf(vis_stdout, "ABS: System with (PI,FF) = (%d,%d)\n", 
                   st_count(AbsVerificationInfoReadQuantifyVars(absInfo)), 
                   st_count(AbsVerificationInfoReadStateVars(absInfo)));
  }

  /* Create the array of results */
  result = array_alloc(AbsVerificationResult_t, array_n(formulaArray));

  /* Obtain the fsm representing the complete circuit */
  fsm = Fsm_FsmCreateFromNetworkWithPartition(
          AbsVerificationInfoReadNetwork(absInfo), NIL(graph_t));

  /* Traverse the array of formulas and verify all of them */
  arrayForEachItem(AbsVertexInfo_t *, formulaArray, fIndex, formulaPtr) {
    Fsm_Fsm_t *localSystem;
    Fsm_Fsm_t *approxSystem;
    array_t   *stateVarIds;
    mdd_t     *initialStates;
    mdd_t     *careStates;
    long      cpuTime;
    int       numBddVars;
    int       mddId;
    int       i;

    /* Variable Initialization */
    approxSystem = NIL(Fsm_Fsm_t);

    /* Set the cpu-time lap */
    cpuTime = util_cpu_time();

    /* Print the labeled operational graph */
    if (AbsOptionsReadVerbosity(options) & ABS_VB_GRAPH) {
      (void) fprintf(vis_stdout, "ABS: === Labeled Operational Graph ===\n");
      AbsVertexPrint(formulaPtr, NIL(st_table), TRUE,
                     AbsOptionsReadVerbosity(options));
      (void) fprintf(vis_stdout, "ABS: === End of Graph ===\n");
    }
    
    /* Simplify the system with respect to the given formula */
    localSystem = AbsCreateReducedFsm(absInfo, formulaPtr, &approxSystem);
    if (localSystem == NIL(Fsm_Fsm_t)) {
      localSystem = fsm;
    }
    if (approxSystem == NIL(Fsm_Fsm_t)) {
      approxSystem = fsm;
    }

    AbsVerificationInfoSetFsm(absInfo, localSystem);

    /* Compute the number of bdd variables needed to encode the state space */
    stateVarIds = Fsm_FsmReadPresentStateVars(localSystem);
    numBddVars = 0;
    arrayForEachItem(int, stateVarIds, i, mddId) {
      array_t *mvarList = mdd_ret_mvar_list(mddManager);
      mvar_type mddVar  = array_fetch(mvar_type, mvarList, mddId);
      numBddVars += mddVar.encode_length;
    }
    AbsVerificationInfoSetNumStateVars(absInfo, numBddVars);

    AbsVerificationInfoSetApproxFsm(absInfo, approxSystem);

    if (AbsOptionsReadVerbosity(options) & ABS_VB_SIMPLE) {
      (void) fprintf(vis_stdout, 
                     "ABS: System Simplified from %d to %d latches\n",
                     array_n(Fsm_FsmReadPresentStateVars(fsm)),
                     array_n(Fsm_FsmReadPresentStateVars(localSystem)));
      (void) fprintf(vis_stdout, 
                     "ABS: System Approximated by %d of %d latches\n",
                     array_n(Fsm_FsmReadPresentStateVars(approxSystem)),
                     array_n(Fsm_FsmReadPresentStateVars(localSystem)));
    }
                   
    /* Compute reachability if requested */
    if (AbsOptionsReadReachability(options)) {
      mdd_t *reachableStates;
      long  cpuTime;
      
      cpuTime = util_cpu_time();
      
      reachableStates = Fsm_FsmComputeReachableStates(localSystem, 0, 1, 0, 0, 
                        0, 0, 0,Fsm_Rch_Default_c, 0, 0, NIL(array_t), FALSE,
                        NIL(array_t));
      if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) {
        (void) fprintf(vis_stdout, "ABS: %7.1f secs spent in reachability \n",
                       (util_cpu_time() - cpuTime)/1000.0);
      }

      /* Print the number of reachable states */
      if (AbsOptionsReadVerbosity(options) & ABS_VB_PRCH) {
        array_t *sVars;
        
        sVars = Fsm_FsmReadPresentStateVars(localSystem);
        (void) fprintf(vis_stdout, "ABS: System with %.0f reachable states.\n",
                       mdd_count_onset(mddManager, reachableStates, sVars));
      }
      
      careStates = reachableStates;
    } /* End of reachability analysis */
    else {
      careStates = mdd_one(mddManager);
    }

    /* Compute the initial states */
    initialStates = Fsm_FsmComputeInitialStates(localSystem);
    if (initialStates == NIL(mdd_t)) {
      (void) fprintf(vis_stdout, "** abs error: Unable to compute initial states.\n");
      (void) fprintf(vis_stdout, "ABS: %s\n", error_string());
      
      AbsVerificationInfoFree(absInfo);
      array_free(result);
      /* Deallocate the FSM if the system was reduced */
      if (localSystem != fsm) {
        Fsm_FsmFree(localSystem);
      }
      return NIL(array_t);
    }

    /* Set the don't care information */
    if (AbsVerificationInfoReadCareSet(absInfo) != NIL(mdd_t)) {
      mdd_free(AbsVerificationInfoReadCareSet(absInfo));
    }
    AbsVerificationInfoSetCareSet(absInfo, careStates);
    if (AbsVerificationInfoReadTmpCareSet(absInfo) != NIL(mdd_t)) {
      mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
    }
    AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager));

    /* Compute the formula EG(true) if required */
    if (AbsOptionsReadEnvelope(options)) {
      mdd_t *newCareStates;
      mdd_t *tmp1;

      newCareStates = ComputeEGtrue(absInfo, careStates);
      tmp1 = mdd_and(newCareStates, careStates, 1, 1);
      mdd_free(careStates);
      mdd_free(newCareStates);
      careStates = tmp1;
      AbsVerificationInfoSetCareSet(absInfo, careStates);
    }

    /* Print verbosity message */
    if (AbsOptionsReadVerbosity(options) & ABS_VB_VTXCNT) {
      (void) fprintf(vis_stdout, "ABS: === Initial Verification ===\n");
    }
    
    /* Create the initial evaluation of the formula */
    AbsSubFormulaVerify(absInfo, formulaPtr);
    
    assert(!AbsVertexReadTrueRefine(formulaPtr));

    /* Print verbosity message */
    if (AbsOptionsReadVerbosity(options) & ABS_VB_VTXCNT) {
      (void) fprintf(vis_stdout, "ABS: === End of Initial Verification ===\n");
    }
    
    /* Print cpu-time information */
    if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) {
      (void) fprintf(vis_stdout, "ABS: Initial verification: %7.1f secs.\n",
                     (util_cpu_time() - cpuTime)/1000.0);
    }

    /* Check if the initial states satisfy the formula */
    if (mdd_lequal(initialStates, AbsVertexReadSat(formulaPtr), 1, 1)) {
        array_insert(int, result, fIndex, trueVerification_c);
    }
    else {
      if (AbsVertexReadGlobalApprox(formulaPtr)) {
        mdd_t *goalSet;
        mdd_t *refinement;

        /* 
         * Compute the set of states remaining in the goal. We are assuming
         * that the parity of the top vertex is negative 
         */
        assert(!AbsVertexReadPolarity(formulaPtr));

        /* Compute the initial goal set */
        goalSet = mdd_and(initialStates, AbsVertexReadSat(formulaPtr), 1, 0);

        /* Notify that the refinement process is beginning */
        if (AbsOptionsReadVerbosity(options) &ABS_VB_PPROGR) {
          (void) fprintf(vis_stdout, 
                         "ABS: Verification has been approximated. ");
          (void) fprintf(vis_stdout, "Beginning approximation refinement\n");
        }

        /* Print the number of states to refine */
        if (AbsOptionsReadVerbosity(options) & ABS_VB_PRINIT) {
          array_t *sVars;

          sVars = Fsm_FsmReadPresentStateVars(fsm);
          (void) fprintf(vis_stdout, 
                         "ABS: %.0f states out of %.0f to be refined\n",
                         mdd_count_onset(mddManager, goalSet, sVars),
                         mdd_count_onset(mddManager, initialStates, sVars));
        }

        /* Effectively perform the refinement */
        refinement = AbsSubFormulaRefine(absInfo, formulaPtr, goalSet); 

        /* Insert the outcome of the refinement in the solution */
        if (mdd_is_tautology(refinement, 0)) {
          array_insert(int, result, fIndex, trueVerification_c);
        }
        else {
          if (!AbsVertexReadTrueRefine(formulaPtr)) {
            array_insert(int, result, fIndex, inconclusiveVerification_c);
          }
          else {
            array_insert(int, result, fIndex, falseVerification_c);
          }
        }
        mdd_free(goalSet);
        mdd_free(refinement);
      }
      else {
        array_insert(int, result, fIndex, falseVerification_c);
      }
    }
    mdd_free(initialStates);
    
    /* Print cpu-time information */
    if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) {
      (void) fprintf(vis_stdout, "ABS: Formula #%d verified in %7.1f secs.\n",
                     fIndex + 1, (util_cpu_time() - cpuTime)/1000.0);
    }

    /* Print the number of states in the on set of Sat */
    if (AbsOptionsReadVerbosity(options) & ABS_VB_TSAT) {
      array_t *sVars;
      
      sVars = Fsm_FsmReadPresentStateVars(localSystem);
      (void) fprintf(vis_stdout, "ABS: %.0f States in sat of the formula.\n",
                     mdd_count_onset(mddManager, AbsVertexReadSat(formulaPtr), 
                                     sVars));
    }

    /* Clean up */
    AbsVertexFlushCache(formulaPtr);
    AbsVerificationFlushCache(absInfo);
    if (approxSystem != fsm) {
      Fsm_FsmFree(approxSystem);
    }
    if (localSystem != fsm) {
      Fsm_FsmFree(localSystem);
    }
  } /* End of the loop over the array of formulas to be verified */

  /* Set the number of reorderings in the stats */
  AbsStatsSetNumReorderings(AbsVerificationInfoReadStats(absInfo),
                            bdd_read_reorderings(mddManager) - numReorderings);

  /* Clean up */
  Fsm_FsmFree(fsm);

  return result;
}

Fsm_Fsm_t *
AbsCreateReducedFsm(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr,
  Fsm_Fsm_t **approxFsm)
{
  AbsVertexInfo_t *vPtr;
  Ntk_Network_t   *network;
  Ntk_Node_t      *nodePtr;
  Fsm_Fsm_t       *result;
  lsGen           gen;
  array_t         *vertexArray;
  array_t         *nodeArray;
  array_t         *supportArray;
  array_t         *inputs;
  array_t         *latches;
  st_table        *visited;
  int             i;

  if (vertexPtr == NIL(AbsVertexInfo_t)) {
    return NIL(Fsm_Fsm_t);
  }

  network = AbsVerificationInfoReadNetwork(absInfo);

  /* Select the vertices of type "identifier" */
  visited = st_init_table(st_ptrcmp, st_ptrhash);
  vertexArray = array_alloc(AbsVertexInfo_t *, 0);
  SelectIdentifierVertices(vertexPtr, vertexArray, visited);
  st_free_table(visited);

  if (array_n(vertexArray) == 0) {
    array_free(vertexArray);
    return NIL(Fsm_Fsm_t);
  }

  /* Create the array of network nodes corresponding to the identifiers */
  visited = st_init_table(st_ptrcmp, st_ptrhash);
  nodeArray = array_alloc(Ntk_Node_t *, 0);
  arrayForEachItem(AbsVertexInfo_t *, vertexArray, i, vPtr) {
    nodePtr = Ntk_NetworkFindNodeByName(network, AbsVertexReadName(vPtr));

    assert(nodePtr != NIL(Ntk_Node_t));

    if (!st_is_member(visited, (char *)nodePtr)) {
      array_insert_last(Ntk_Node_t *, nodeArray, nodePtr);
      st_insert(visited, (char *)nodePtr, NIL(char));
    }
  }
  array_free(vertexArray);

  /* Create the input and array latches to compute the approxFsm */
  inputs = array_alloc(Ntk_Node_t *, 0);
  Ntk_NetworkForEachInput(network, gen, nodePtr) {
    array_insert_last(Ntk_Node_t *, inputs, nodePtr);
  }
  latches = array_alloc(Ntk_Node_t *, 0);
  Ntk_NetworkForEachLatch(network, gen, nodePtr) {
    if (st_is_member(visited, (char *)nodePtr)) {
      array_insert_last(Ntk_Node_t *, latches, nodePtr);
    }
    else {
      array_insert_last(Ntk_Node_t *, inputs, nodePtr);
    }
  }
  st_free_table(visited);

  /* Obtain the approximated system */
  *approxFsm = Fsm_FsmCreateReducedFsm(network, NIL(graph_t), latches, inputs, 
                                       NIL(array_t));
  array_free(inputs);
  array_free(latches);

  /* Obtain the transitive fanin of the nodes */
  supportArray = Ntk_NodeComputeCombinationalSupport(network, nodeArray, FALSE);
  array_free(nodeArray);

  /* If the transitive fanin of the nodes is empty, return */
  if (array_n(supportArray) == 0) {
    array_free(supportArray);
    return NIL(Fsm_Fsm_t);
  }

  /* Divide the nodes between inputs and latches and create the final FSM */
  inputs = array_alloc(Ntk_Node_t *, 0);
  latches = array_alloc(Ntk_Node_t *, 0);
  arrayForEachItem(Ntk_Node_t *, supportArray, i, nodePtr) {
    if (Ntk_NodeTestIsInput(nodePtr)) {
      array_insert_last(Ntk_Node_t *, inputs, nodePtr);
    }
    else {
      assert(Ntk_NodeTestIsLatch(nodePtr));
      array_insert_last(Ntk_Node_t *, latches, nodePtr);
    }
  }
  array_free(supportArray);

  /* If the collection of inputs and latches is the whole FSM, return */
  if (array_n(inputs) == Ntk_NetworkReadNumInputs(network) &&
      array_n(latches) == Ntk_NetworkReadNumLatches(network)) {
    array_free(inputs);
    array_free(latches);
    return NIL(Fsm_Fsm_t);
  }

  result = Fsm_FsmCreateReducedFsm(network, NIL(graph_t), latches, inputs, 
                                   NIL(array_t));

  /* Clean up */
  array_free(inputs);
  array_free(latches);

  return result;
} /* End of AbsCreateReducedFsm */

boolean
AbsMddEqualModCareSet(
  mdd_t *f,
  mdd_t *g,
  mdd_t *careSet)
{
  boolean result = mdd_equal_mod_care_set(f, g, careSet);
  return result;
} /* End of AbsMddEqualModCareSet */

boolean
AbsMddLEqualModCareSet(
  mdd_t *f,
  mdd_t *g,
  mdd_t *careSet)
{
  boolean result = mdd_lequal_mod_care_set(f, g, 1, 1, careSet);
  return result;
} /* End of AbsMddLEqualModCareSet */

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

static mdd_t *
ComputeEGtrue(
  Abs_VerificationInfo_t *absInfo,
  mdd_t *careStates)
{
  AbsOptions_t    *options;
  AbsVertexInfo_t *vertex;
  Ctlp_Formula_t  *egFormula;
  Ctlp_Formula_t  *trueFormula;
  mdd_manager     *mddManager;
  array_t         *inputTranslation;
  array_t         *outputTranslation;
  mdd_t           *envelope;
  long            cpuTime;
  
  cpuTime = util_cpu_time();
  options = AbsVerificationInfoReadOptions(absInfo);
  mddManager = AbsVerificationInfoReadMddManager(absInfo);
  
  /* Compute the EG(true) fixed point */
  trueFormula = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(void), NIL(void));
  egFormula = Ctlp_FormulaCreate(Ctlp_EG_c, trueFormula, NIL(void));
  
  /* Translate into the graph representation */
  inputTranslation = array_alloc(Ctlp_Formula_t *, 1);
  array_insert(Ctlp_Formula_t *, inputTranslation, 0, egFormula);
  outputTranslation = AbsCtlFormulaArrayTranslate(absInfo, inputTranslation, 
                                                  NIL(array_t));
  vertex = array_fetch(AbsVertexInfo_t *, outputTranslation, 0);
  array_free(inputTranslation);
  array_free(outputTranslation);
  
  /* Evaluate the formula */
  AbsSubFormulaVerify(absInfo, vertex);
  
  envelope = mdd_dup(AbsVertexReadSat(vertex));
  
  /* Clean up */
  Ctlp_FormulaFree(egFormula);
  AbsVertexFree(AbsVerificationInfoReadCatalog(absInfo), vertex, 
                NIL(AbsVertexInfo_t));
  
  /* Print the number of envelope states */
  if (AbsOptionsReadVerbosity(options) & ABS_VB_PENV) {
    array_t *sVars;
    mdd_t *states;
  
    sVars = Fsm_FsmReadPresentStateVars(AbsVerificationInfoReadFsm(absInfo));
    states = mdd_and(envelope, careStates, 1, 1);
    (void) fprintf(vis_stdout, "ABS: Envelope with %.0f care states.\n",
                   mdd_count_onset(mddManager, states, sVars));
    mdd_free(states);
  }
  
  if (AbsOptionsReadVerbosity(options) & ABS_VB_PENV) {
    (void) fprintf(vis_stdout, "ABS: %7.1f secs computing EG(TRUE)\n",
                   (util_cpu_time() - cpuTime)/1000.0);
  }

  return envelope;
} /* End of ComputeEGtrue */

static void
SelectIdentifierVertices(
  AbsVertexInfo_t *vertexPtr,
  array_t *result,
  st_table *visited)
{
  assert(result != NIL(array_t));

  if (vertexPtr == NIL(AbsVertexInfo_t)) {
    return;
  }

  if (st_is_member(visited, (char *)vertexPtr)) {
    return;
  }

  if (AbsVertexReadType(vertexPtr) == identifier_c) {
    array_insert_last(AbsVertexInfo_t *, result, vertexPtr);
    st_insert(visited, (char *)vertexPtr, NIL(char));
    return;
  }
  else {
    SelectIdentifierVertices(AbsVertexReadLeftKid(vertexPtr), result, visited);
    SelectIdentifierVertices(AbsVertexReadRightKid(vertexPtr), result, visited);
  }

  st_insert(visited, (char *)vertexPtr, NIL(char));

  return;
} /* End of SelectIdentifierVertices */