src/res/res.c

Go to the documentation of this file.

#include "resInt.h"

static char rcsid[] UNUSED = "$Id: res.c,v 1.55 2009/04/11 21:31:29 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
#define RES_VERIFY_NOTHING 0
#define RES_VERIFY_DONE 1
#define RES_VERIFY_IGNORE_PREV_RESULTS 2
#define LOG2_FIRST_PRIME 8

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


static int PrimePool [] = { 5,   7,  9, 11, 13, 17,  19,  23,  29,
                            31,  37,  41,  43,  47,  53,  59,  61,  67,  71,
                            73,  79,  83,  89,  97, 101, 103, 107, 109, 113,
                            127, 131, 137, 139, 149, 151, 157, 163, 167, 173,
                            179, 181, 191, 193, 197, 199, 211, 223, 227, 229,
                            233, 239, 241, 251, 257, 263, 269, 271, 277, 281,
                            283, 293, 307, 311, 313, 317, 331, 337, 347, 349,
                            353, 359, 367, 373, 379, 383, 389, 397, 401, 409,
                            419, 421, 431, 433, 439, 443, 449, 457, 461, 463,
                            467, 479, 487, 491, 499, 503, 509, 521, 523, 541,
                            547};
static int PrimePoolSize = 100;    /* Number of elements of the array above */

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

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

static int ChoosePrimes(int numOutputs, int **pool, int numDirectVerify);
static int ComputeMaxNumberOfOutputs(void);
static void RestoreOldMddIds(Ntk_Network_t *network, st_table *table);
static st_table * GeneratePointerMatchTableFromNameMatch(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *nameMatchTable);
static st_table * GenerateDirectVerifyPointerTable(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *outputMatch, array_t *outputOrderArray, int numDirectVerify);
static st_table * GenerateIdentityMatchTable(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int inputOrOutput);
static bdd_manager * Initializebdd_manager(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int *initManagerHere);
static int SetBasicResultInfo(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int numDirectVerify);
static void Cleanup(int error, Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, int initManagerHere, int done, st_table *outputMatch, st_table *inputMatch, st_table *directVerifyMatch, st_table *oldSpecMddIdTable, st_table *oldImplMddIdTable, array_t *specLayerArray, array_t *implLayerArray);
static st_table * SaveOldMddIds(Ntk_Network_t *network);
static int DirectVerification(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *directVerifyMatch, st_table *inputMatch, st_table *outputMatch, array_t *outputOrderArray);
static bdd_reorder_type_t DecodeDynMethod(char *dynMethodString);
static int ResidueVerification(Ntk_Network_t *specNetwork, Ntk_Network_t *implNetwork, st_table *outputMatch, st_table *inputMatch, int numDirectVerify, array_t *specLayerArray, array_t *implLayerArray, array_t *outputArray);
static void ExtractACubeOfDifference(bdd_manager *mgr, Ntk_Network_t *specNetwork, bdd_node *fn1, bdd_node *fn2);

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

int
Res_NetworkResidueVerify(
         Ntk_Network_t *specNetwork,
         Ntk_Network_t *implNetwork,
         int numDirectVerify,
         array_t *outputOrderArray,
         st_table *outputNameMatch,
         st_table *inputNameMatch)
{
  Ntk_Node_t *nodePtr;           /* To iterate over nodes */
  Ntk_Node_t *implNodePtr;       /* To iterate over nodes */
  Res_ResidueInfo_t *resultSpec; /* Structure holding all the info */
  Res_ResidueInfo_t *resultImpl; /* Structure holding all the info */
  array_t *specLayerArray;       /* array containing the reverse
                                  * topological layers of the spec.
                                  */
  array_t *implLayerArray;       /* array containing the reverse
                                  * topological layers of the impl.
                                  */
  st_table *oldSpecMddIdTable;   /* Tables to store MDD IDs of the spec
                                  * if already assigned
                                  */
  st_table *oldImplMddIdTable;   /* Tables to store MDD IDs of the impl.
                                  * if already assigned
                                  */

  st_table *outputMatch;         /* Output match table with node
                                  * pointers, spec node pointer is
                                  * the key
                                  */
  st_table *inputMatch;          /* Input match table with node
                                  * pointers, spec node pointer is
                                  * the key
                                  */

  bdd_manager *ddManager;          /* Manager read from the network */
  int initManagerHere;           /* Flag to indicate the network Mdd
                                  * managers initialized here
                                  */

  lsGen listGen;                 /* To iterate over outputList */
  long overallLap;               /* To measure overall execution time */
  int maxNumberOfOutputs;        /* max number of outputs that can be
                                  * verified here
                                  * = product(100 primes)
                                  */
  int numOutputs;                /* Store the number of outputs in spec.,
                                  * impl
                                  */
  int done;                      /* flag to determine the status of
                                  * previous verification
                                  */
  int error;                     /* error flag, set for cleanup, 1 failed,
                                  * 0 if successful
                                  */
  int status;                    /* error status of residue verification */
  int directVerifyStatus;        /* direct verification status, 1 if failed,
                                  * 0 if successful
                                  */
  st_table *directVerifyMatch;   /* match table with pointers for the
                                  * directly verified outputs, spec pointer
                                  * is key
                                  */
  char *name;                    /* variable to store name of node */
  array_t *outputArray;          /* array to store output nodes */
  array_t *ignoreOutputArray;    /* array to store outputs nodes to be
                                  * ignored
                                  */
  int verbose;                   /* variable to read residue_verbosity value */
  char *flagValue;               /* string to read flag values */
  int i;                         /* Loop iterators */
  int unassignedValue;           /* NTK_UNASSIGNED_MDD_ID value holder */

  /* Initialize some variables to default values */

  overallLap = 0;
  initManagerHere = 0;
  ddManager = NIL(bdd_manager);
  done = RES_VERIFY_NOTHING;
  error = 0;
  status = 1;
  verbose = 0;

  unassignedValue =  NTK_UNASSIGNED_MDD_ID;
  directVerifyStatus = 1;
  directVerifyMatch = NIL(st_table);
  specLayerArray = NIL(array_t);
  implLayerArray = NIL(array_t);
  outputArray = NIL(array_t);
  ignoreOutputArray = NIL(array_t);
  outputMatch = NIL(st_table);
  inputMatch = NIL(st_table);
  oldSpecMddIdTable = NIL(st_table);
  oldImplMddIdTable = NIL(st_table);
  resultSpec = NIL(Res_ResidueInfo_t);
  resultImpl = NIL(Res_ResidueInfo_t);


  /* Initialize global time values*/
  Res_composeTime = 0;
  Res_smartVarTime = 0;
  Res_shuffleTime = 0;
  Res_orderTime = 0;


  /* Read verbosity value */
  flagValue = Cmd_FlagReadByName("residue_verbosity");
  if (flagValue != NIL(char)) {
    verbose = atoi(flagValue);
  }

  /* Read the mdd Manager (or create it if necessary) */
  ddManager = Initializebdd_manager(specNetwork, implNetwork, &initManagerHere);
  if (ddManager == NIL(bdd_manager)) {
    /* error, but nothing allocated, so no cleanup */
    return 1;
  }

  /* Set up the correct maximum number of outputs */
  maxNumberOfOutputs  = ComputeMaxNumberOfOutputs();
  if (verbose >= 2) {
    fprintf(vis_stdout, "The Maximum Number of outputs that can be");
    fprintf(vis_stdout, " verified are %d.\n", maxNumberOfOutputs);
  }

  /* check number of outputs */
  numOutputs = Ntk_NetworkReadNumCombOutputs(specNetwork);
  /* Check if the circuit has too many outputs */
  if (numOutputs >= maxNumberOfOutputs) {
    error_append("Circuit with too many outputs.\n");
    /* Clean up before you leave */
    error = 1;
    Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
            outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
            oldImplMddIdTable, specLayerArray, implLayerArray);
    return 1;
  } /* End of if */

  /* Create result data structure for both the spec and the implementation */
  done = SetBasicResultInfo(specNetwork, implNetwork, numDirectVerify);
  if (done ==  RES_VERIFY_DONE) {/* same verification as previous time */
    /* Clean up before you leave */
    fprintf(vis_stdout, "Verification has been previously performed\n");
    error = 0;
    Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
            outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
            oldImplMddIdTable, specLayerArray, implLayerArray);
    return 0; /* success */
  } /* end of case RES_VERIFY_DONE */

  /* if output match table does not exist, create one with matching names
   * in the two networks. Insert with spec network node pointer as key
   * in the outputMatch table. If match table does exist, convert name table
   * to pointer table.
   */
  if(outputNameMatch == NIL(st_table)) {
    outputMatch = GenerateIdentityMatchTable(specNetwork, implNetwork, PRIMARY_OUTPUTS);
  } else {
    outputMatch = GeneratePointerMatchTableFromNameMatch(specNetwork,
                                                         implNetwork,outputNameMatch);
    if (outputMatch == NIL(st_table)) {
      error_append("Output pointer table is NULL\n");
      /* Clean up before you leave */
      error = 1;
      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
              outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
              oldImplMddIdTable, specLayerArray, implLayerArray);
      return 1; /* error return */
    }
  }

  /* if input match table does not exist, create one with matching names
   * in the two networks. Insert with spec network node pointer as key
   * in the inputMatch table. If match table does exist, convert name table
   * to pointer table.
   */
  if(inputNameMatch == NIL(st_table)) {
    inputMatch = GenerateIdentityMatchTable(specNetwork, implNetwork, PRIMARY_INPUTS);
  } else {
    inputMatch = GeneratePointerMatchTableFromNameMatch(specNetwork,
                                                        implNetwork,inputNameMatch);
    if (inputMatch == NIL(st_table)) {
      error_append("Input pointer table is NULL\n");
      /* Clean up before you leave */
      error = 1;
      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
              outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
              oldImplMddIdTable, specLayerArray, implLayerArray);
      return 1; /* error return */
    }
  }

  /* Save the old MDD IDs in a st_table */
  oldSpecMddIdTable = SaveOldMddIds(specNetwork);
  if (oldSpecMddIdTable == NIL(st_table)) {
    error_append("Unable to save old Mdd Ids for spec\n");
    /* Clean up before you leave */
    error = 1;
    Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
            outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
            oldImplMddIdTable, specLayerArray, implLayerArray);
    return 1;
  }

  /* Save the old MDD IDs in a st_table */
  oldImplMddIdTable = SaveOldMddIds(implNetwork);
  if (oldImplMddIdTable == NIL(st_table)) {
    error_append("Unable to save old Mdd Ids for impl\n");
    /* Clean up before you leave */
    error = 1;
    Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
            outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
            oldImplMddIdTable, specLayerArray, implLayerArray);
    return 1;
  }

  /* Initialize time to measure overall lap time */
  overallLap = util_cpu_time();

  /* Perform direct verification of the given outputs. */
  if (numDirectVerify) {
    /* generate output match table for outputs to be directly verified */
    directVerifyMatch = GenerateDirectVerifyPointerTable(specNetwork,
         implNetwork, outputMatch, outputOrderArray, numDirectVerify);
    if (directVerifyMatch == NIL(st_table)) {
      error_append("Directly verify  pointer table is NULL\n");
      /* Clean up before you leave */
      error = 1;
      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
              outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
              oldImplMddIdTable, specLayerArray, implLayerArray);
      return 1; /* error return */
    }

    /* perform direct verification of the outputs in the match table */
    directVerifyStatus = DirectVerification(specNetwork, implNetwork,
                    directVerifyMatch, inputMatch, outputMatch, outputOrderArray);
    /* Direct verification error */
    if (directVerifyStatus == 1) {
      error_append("Direct Verification error\n");
      /* Clean up before you leave */
      error = 1;
      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
      outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
              oldImplMddIdTable, specLayerArray, implLayerArray);
      return 1; /* error return */
    }

    resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
                                            RES_NETWORK_APPL_KEY);
    resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
                                            RES_NETWORK_APPL_KEY);
    /* Direct verification failed */
    if ((ResResidueInfoReadDirectVerificationSuccess(resultSpec) == RES_FAIL) &&
        (ResResidueInfoReadDirectVerificationSuccess(resultImpl) == RES_FAIL)) {
      ResResidueInfoSetSuccess(resultSpec, RES_FAIL);
      ResResidueInfoSetSuccess(resultImpl, RES_FAIL);
      /*  Clean up before you leave */
      error = 0;
      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
      outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
              oldImplMddIdTable, specLayerArray, implLayerArray);
      return 0;
    } else if (numDirectVerify == numOutputs) {
      if ((ResResidueInfoReadDirectVerificationSuccess(resultSpec) == RES_PASS) &&
          (ResResidueInfoReadDirectVerificationSuccess(resultImpl) == RES_PASS)) {
        /* if all outputs are directly verified */
        ResResidueInfoSetSuccess(resultSpec, RES_PASS);
        ResResidueInfoSetSuccess(resultImpl, RES_PASS);
      }
    } /* end of else */


  } /* Direct Verification, done and successful */

  (void) fprintf(vis_stdout, "Total Direct Verification Time = %.3f (secs).\n",
                 (util_cpu_time() - overallLap)/1000.0);

  if (verbose >= 1) {
    util_print_cpu_stats(vis_stdout);
  }


  /* RESIDUE VERIFICATION starts here */

  if (numOutputs - numDirectVerify) { /* if residue verification required */
    /* reset all Ids after direct verification as residue verification
     * assigns new Ids.
     */
    Ntk_NetworkForEachNode(specNetwork, listGen, nodePtr) {
      Ntk_NodeSetMddId(nodePtr, unassignedValue);
    }
    Ntk_NetworkForEachNode(implNetwork, listGen, nodePtr) {
      Ntk_NodeSetMddId(nodePtr, unassignedValue);
    }

    /* check if directly verified outputs are to be involved in residue
     * verification
     */
    flagValue = Cmd_FlagReadByName("residue_ignore_direct_verified_outputs");
    if (flagValue != NIL(char)) {
      if ((strcmp(flagValue, "1") == 0) && (numDirectVerify)) {
        ignoreOutputArray = array_alloc(Ntk_Node_t *, numDirectVerify);
      }
    }
    if (ignoreOutputArray == NIL(array_t)) {
      /* fill the output array with all output nodes */
      outputArray = array_alloc(Ntk_Node_t *, array_n(outputOrderArray));
      arrayForEachItem(char *, outputOrderArray, i, name) {
        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
        st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
        array_insert(Ntk_Node_t *, outputArray, i, implNodePtr);
      }
    } else {
      outputArray = array_alloc(Ntk_Node_t *, array_n(outputOrderArray)-numDirectVerify);
      /* fill the output array with nodes not directly verified */
      for (i = 0; i < (array_n(outputOrderArray) - numDirectVerify); i++) {
        name = array_fetch(char *, outputOrderArray, i);
        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
        st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
        array_insert(Ntk_Node_t *, outputArray, i, implNodePtr);
      }
      /* fill ignore array with outputs directly verified. */
      for (i = (array_n(outputOrderArray) - numDirectVerify); i < array_n(outputOrderArray); i++) {
        name = array_fetch(char *, outputOrderArray, i);
        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
        st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
        array_insert(Ntk_Node_t *, ignoreOutputArray, (i-array_n(outputOrderArray)+numDirectVerify) , implNodePtr);
      }
    }


    /* Compute the layers to be used for function composition */
    implLayerArray = ResComputeCompositionLayers(implNetwork, outputArray, ignoreOutputArray);

    /* create the output array for the spec. */
    if (ignoreOutputArray == NIL(array_t)) {
      /* fill the output array with all output nodes */
      arrayForEachItem(char *, outputOrderArray, i, name) {
        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
        array_insert(Ntk_Node_t *, outputArray, i, nodePtr);
      }
    } else {
      /* fill the output array with nodes not directly verified */
      for (i = 0; i < (array_n(outputOrderArray) - numDirectVerify); i++) {
        name = array_fetch(char *, outputOrderArray, i);
        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
        array_insert(Ntk_Node_t *, outputArray, i, nodePtr);
      }
      /* fill ignore array with outputs directly verified. */
      for (i = (array_n(outputOrderArray) - numDirectVerify); i < array_n(outputOrderArray); i++) {
        name = array_fetch(char *, outputOrderArray, i);
        nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
        array_insert(Ntk_Node_t *, ignoreOutputArray, (i-array_n(outputOrderArray)+numDirectVerify), nodePtr);
      }
    }

    /* Compute the layers to be used for function composition */
    specLayerArray = ResComputeCompositionLayers(specNetwork, outputArray, ignoreOutputArray);

    /* print the array */
    if (verbose >=3) {
      ResLayerPrintInfo(specNetwork, specLayerArray);
      ResLayerPrintInfo(implNetwork, implLayerArray);
    }

    /* free the ignore array */
    if (ignoreOutputArray != NIL(array_t)) {
      array_free(ignoreOutputArray);
    }

    /* Perform residue verification on the spec. and impl. */
    status = ResidueVerification(specNetwork, implNetwork, outputMatch, inputMatch, numDirectVerify, specLayerArray, implLayerArray, outputArray);

    /* free output array */
    array_free(outputArray);

    if (status) {
      error_append("Residue Verification error\n");
      /* Clean up before you leave */
      error = 1;
      Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
              outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
              oldImplMddIdTable, specLayerArray, implLayerArray);
      return 1; /* error return */
    }


    resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
                                              RES_NETWORK_APPL_KEY);
    resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
                                            RES_NETWORK_APPL_KEY);
    /* Print success message and info */
    if ((ResResidueInfoReadSuccess(resultSpec) == RES_FAIL) &&
        (ResResidueInfoReadSuccess(resultImpl) == RES_FAIL)) {
      /* Clean up before you leave */
      error = 0;
            Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
              outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
              oldImplMddIdTable, specLayerArray, implLayerArray);
      return 0;
    }

    if(verbose >= 2) {
      (void) fprintf(vis_stdout, "Total Compose Time = %3f(secs).\n",
                     Res_composeTime/1000.0);
      (void) fprintf(vis_stdout, "Total Order Time = %3f(secs).\n",
                     Res_orderTime/1000.0);
      (void) fprintf(vis_stdout, "Total Shuffle Time = %3f(secs).\n",
                     Res_shuffleTime/1000.0);

      (void) fprintf(vis_stdout, "Total Smart Var Time = %3f(secs).\n",
                     Res_smartVarTime/1000.0);
    }


  } /* end of residue verification */

  /* Print success message and info */
  if ((ResResidueInfoReadSuccess(resultSpec) == RES_PASS) &&
      (ResResidueInfoReadSuccess(resultImpl) == RES_PASS))
    (void) fprintf(vis_stdout, "Verification of %s and %s successful.\n",
                   Res_ResidueInfoReadName(resultSpec),
                   Res_ResidueInfoReadName(resultImpl));


  if (verbose >= 1) {
    fprintf(vis_stdout, "Specification:\n");
    (void) Res_ResidueInfoPrint(resultSpec);
    fprintf(vis_stdout, "Implementation:\n");
    (void) Res_ResidueInfoPrint(resultImpl);
  }
  if (verbose >= 1) {
    util_print_cpu_stats(vis_stdout);
  }

  (void) fprintf(vis_stdout, "Total Time = %.3f (secs).\n",
                 (util_cpu_time() - overallLap)/1000.0);

  /* no error */
  error = 0;
  Cleanup(error, specNetwork, implNetwork, initManagerHere, done,
          outputMatch, inputMatch, directVerifyMatch, oldSpecMddIdTable,
          oldImplMddIdTable, specLayerArray, implLayerArray);

  /* End of clean up */

  return 0;
} /* End of Res_NetworkResidueVerify */

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



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

static int
ChoosePrimes(int numOutputs,
             int **pool,
             int numDirectVerify)
{
  double accumulator = 0.0;
  int i,max, index = 0;
  double factor = log10((double)2.0);

  assert(*pool == NIL(int));

  if (numDirectVerify) {
    accumulator = (double)numDirectVerify;
  } else {
    /* make first prime 2^LOG2_FIRST_PRIME */
    if (numOutputs >= LOG2_FIRST_PRIME) {
      accumulator = (double)LOG2_FIRST_PRIME;
    } else {
      accumulator = (double)numOutputs;
    }
  }

  /* step through primes till their product exceeds the max value of outputs */
  max = 0;
  while (accumulator < ((double)numOutputs)) {
    accumulator += log10((double)PrimePool[max])/factor;
    max++;
  }

  index = 0;
  /* if no direct verification, then set the first prime to be 2^LOG2_FIRST_PRIME */
  if (!numDirectVerify) {
    *pool = ALLOC(int, max+1);
    if (numOutputs >= LOG2_FIRST_PRIME) {
      (*pool)[index++] = (int)pow((double)2.0, (double)LOG2_FIRST_PRIME);
    } else {
      (*pool)[index++] = (int)pow((double)2.0, (double)numOutputs);
    }
  } else {
    *pool = ALLOC(int, max);
  }

  /* fill the array with other primes */
  for(i=0; i < max; i++) {
   (*pool)[index++] = PrimePool[i];
  }

  return index;
} /* End of ChoosePrimes */


static int
ComputeMaxNumberOfOutputs(void)
{
  int i;
  double result = 0;
  int maxNumberOfOutputs;

  result = LOG2_FIRST_PRIME;
  for(i = 0; i < PrimePoolSize; i++) {
    result += log10((double)PrimePool[i]);
  } /* End of for */

  maxNumberOfOutputs = (int) (result/log10((double) 2.0)) - 1;

  return (maxNumberOfOutputs);
} /* End of ComputeMaxNumberOfOutputs */


static void
RestoreOldMddIds(Ntk_Network_t *network,
                 st_table *table)
{
  lsGen listGen;
  Ntk_Node_t *nodePtr;
  int value;
  if (table != NULL) {
    Ntk_NetworkForEachNode(network, listGen, nodePtr) {
      if(st_lookup_int(table, (char *)nodePtr, &value)) {
        Ntk_NodeSetMddId(nodePtr, value);
      } else {
        error_append("Node");
        error_append(Ntk_NetworkReadName(network));
        error_append("should have been in the table.\n");
        (void) lsFinish(listGen);
      }
    }
  }
} /* End of RestoreOldMddIds */


static st_table *
GeneratePointerMatchTableFromNameMatch(
                       Ntk_Network_t *specNetwork,
                       Ntk_Network_t *implNetwork,
                       st_table *nameMatchTable)
{
  st_table *pointerMatch;
  Ntk_Node_t *nodePtr, *implNodePtr;
  st_generator *stGen;
  char *key, *value;

  pointerMatch = st_init_table( st_ptrcmp, st_ptrhash);
  st_foreach_item(nameMatchTable, stGen, &key, &value) {
    /* find node in spec */
    nodePtr = Ntk_NetworkFindNodeByName(specNetwork, key);
    if (nodePtr == NIL(Ntk_Node_t)) {
      /* if node not in spec, find in impl */
      implNodePtr = Ntk_NetworkFindNodeByName(implNetwork, key);
      nodePtr = Ntk_NetworkFindNodeByName(specNetwork, value);
    } else {
      implNodePtr = Ntk_NetworkFindNodeByName(implNetwork,value);
    }
    if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))) {
      /* error */
      error_append("Nodes not found by the keys in match table.\n");
      st_free_gen(stGen);
      return NIL(st_table);
    }
    st_insert(pointerMatch, (char *)nodePtr, (char *)implNodePtr);
  } /* end of st_foreach_item */

  return(pointerMatch);
} /* End of GeneratePointerMatchTableFromNameMatch */


static st_table *
GenerateDirectVerifyPointerTable(Ntk_Network_t *specNetwork,
                                 Ntk_Network_t *implNetwork,
                                 st_table *outputMatch,
                                 array_t *outputOrderArray,
                                 int numDirectVerify)

{
  char *specName;
  int i;
  Ntk_Node_t *nodePtr, *implNodePtr;
  st_table *directVerifyMatch;

  directVerifyMatch = st_init_table(st_ptrcmp, st_ptrhash);
  for (i = 0; i < numDirectVerify; i++) {
    specName = array_fetch(char *, outputOrderArray, array_n(outputOrderArray) - 1 - i);
    nodePtr = Ntk_NetworkFindNodeByName(specNetwork, specName);
    st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
    if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))) {
      error_append("Couldn't find nodes to directly verify\n");
      st_free_table(directVerifyMatch);
      return NIL(st_table);
    }
    st_insert(directVerifyMatch, (char *)nodePtr, (char *)implNodePtr);
  }
  return (directVerifyMatch);
} /* End of GenerateDirectVerifyPointerTable */


static st_table *
GenerateIdentityMatchTable(Ntk_Network_t *specNetwork,
                           Ntk_Network_t *implNetwork,
                           int inputOrOutput)
{
  Ntk_Node_t *nodePtr, *implNodePtr;
  st_table *matchTable;
  lsGen listGen;
  char *name;

  matchTable = st_init_table(st_ptrcmp, st_ptrhash);
  if (matchTable == NULL) return(NIL(st_table));

  if (inputOrOutput == PRIMARY_INPUTS) {
    Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
      name = Ntk_NodeReadName(nodePtr);
      implNodePtr = Ntk_NetworkFindNodeByName(implNetwork, name);
      if (implNodePtr == NIL(Ntk_Node_t)) {
        error_append(name);
        error_append(" node does not have corresponding node in impl.");
        st_free_table(matchTable);
        return (NIL(st_table));
      }
      st_insert(matchTable, (char *)nodePtr, (char *)implNodePtr);
    }
  } else if (inputOrOutput == PRIMARY_OUTPUTS) {
    Ntk_NetworkForEachCombOutput(specNetwork, listGen, nodePtr) {
      name = Ntk_NodeReadName(nodePtr);
      implNodePtr = Ntk_NetworkFindNodeByName(implNetwork,name);
      if (implNodePtr == NIL(Ntk_Node_t)) {
        error_append(name);
        error_append(" node does not have corresponding node in impl.");
        st_free_table(matchTable);
        return (NIL(st_table));
      }
      st_insert(matchTable, (char *)nodePtr, (char *)implNodePtr);
    }
  }
  return (matchTable);
} /* End of GenerateIdentityMatchTable */

static bdd_manager *
Initializebdd_manager(Ntk_Network_t *specNetwork,
                    Ntk_Network_t *implNetwork,
                    int *initManagerHere)
{
  bdd_manager *ddManager;

  /* Read the mdd Manager (or create it if necessary) */
  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);

  /* To set the spec manager the same as the impl. manager, either
   * both are nil, or the impl manager is freed and set to the
   * spec manager
   */
  if(ddManager != (bdd_manager *)Ntk_NetworkReadMddManager(implNetwork)) {
    if ((bdd_manager *)Ntk_NetworkReadMddManager(implNetwork) != NIL(bdd_manager)) {
      /* unacceptable if the impl. manager is different from NIl or
       * from the spec manager
       */
      mdd_quit(Ntk_NetworkReadMddManager(implNetwork));
    }
    Ntk_NetworkSetMddManager(implNetwork, (mdd_manager *)ddManager);
  }

  /* if the spec. manager is NIL, then network initialize manager */
  if (ddManager ==  NIL(bdd_manager)) {
    /* flag to say that manager is verified here */
    *initManagerHere = 1;
    ddManager = (bdd_manager *)Ntk_NetworkInitializeMddManager(specNetwork);
    Ntk_NetworkSetMddManager(implNetwork, (mdd_manager *)ddManager);
  }
  return (ddManager);
} /* End of Initializebdd_manager */

static int
SetBasicResultInfo (Ntk_Network_t *specNetwork,
                    Ntk_Network_t *implNetwork,
                    int numDirectVerify)
{
  int numInputs;
  int numOutputs;
  char *specName;
  char *implName;
  Res_ResidueInfo_t *resultSpec;
  Res_ResidueInfo_t *resultImpl;

  /* if previous verification to be considered, make sure the
   *  verification was with the same spec network and the number
   *  of directly verified outputs are the same.
   */
  resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
                                                    RES_NETWORK_APPL_KEY);

  if (resultSpec != NIL(Res_ResidueInfo_t)) {
    if ((strcmp(ResResidueInfoReadNameVerifiedAgainst(resultSpec),
              Ntk_NetworkReadName(implNetwork)) == 0) &&
        (ResResidueInfoReadNumDirectVerifiedOutputs(resultSpec) ==
                                                 numDirectVerify) &&
        (ResResidueInfoReadSuccess(resultSpec) == RES_PASS)) {
      /* if already verified then done, return success (0) */
      return RES_VERIFY_DONE;
    }
    /* if the above conditions are not satisfied, attempt
     * verification again
     */
    Ntk_NetworkFreeApplInfo(specNetwork, RES_NETWORK_APPL_KEY );
  }


  /* create result structure */
  resultSpec = (Res_ResidueInfo_t *)
    ResNetworkResidueInfoReadOrCreate(specNetwork);
  /* add hook to network */
  Ntk_NetworkAddApplInfo(specNetwork, RES_NETWORK_APPL_KEY,
                 (Ntk_ApplInfoFreeFn) Res_ResidueInfoFreeCallback,
                 (void *)resultSpec);

  /* number of outputs */
  numOutputs = Ntk_NetworkReadNumCombOutputs(specNetwork);
  ResResidueInfoSetNumOutputs(resultSpec, numOutputs);
  /* number of Inputs */
  numInputs = Ntk_NetworkReadNumCombInputs(specNetwork);
  ResResidueInfoSetNumInputs(resultSpec, numInputs);
  /* impl name */
  implName = util_strsav(Ntk_NetworkReadName(implNetwork));
  ResResidueInfoSetNameVerifiedAgainst(resultSpec, implName);
  /* number of directly verified outputs */
  ResResidueInfoSetNumDirectVerifiedOutputs(resultSpec, numDirectVerify);

  /*
   * Assumption: The implementation residue information is invalid even
   * if it does exist and will be overwritten
   */
  resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
                                        RES_NETWORK_APPL_KEY);
  /* free existing structure */
  if (resultImpl != NIL(Res_ResidueInfo_t)) {
    Ntk_NetworkFreeApplInfo(implNetwork,RES_NETWORK_APPL_KEY);
  }

  /* create a new structure for the implementation network */
  resultImpl = (Res_ResidueInfo_t *)
    ResNetworkResidueInfoReadOrCreate(implNetwork);
  Ntk_NetworkAddApplInfo(implNetwork, RES_NETWORK_APPL_KEY,
                (Ntk_ApplInfoFreeFn) Res_ResidueInfoFreeCallback,
                (void *)resultImpl);


  /*
   * Get some information about the network  and initialize the residue
   * information for the implementation network.
   */

  /* number of outputs */
  assert (numOutputs == Ntk_NetworkReadNumCombOutputs(implNetwork));
  ResResidueInfoSetNumOutputs(resultImpl, numOutputs);
  /* number of Inputs */
  assert (numInputs == Ntk_NetworkReadNumCombInputs(implNetwork));
  ResResidueInfoSetNumInputs(resultImpl, numInputs);
  /* spec name */
  specName = util_strsav(Ntk_NetworkReadName(specNetwork));
  ResResidueInfoSetNameVerifiedAgainst(resultImpl, specName);
  /* number of directly verified outputs */
  ResResidueInfoSetNumDirectVerifiedOutputs(resultImpl, numDirectVerify);

  return RES_VERIFY_IGNORE_PREV_RESULTS;
} /* End of SetBasicResultInfo */

static void
Cleanup(int error,
        Ntk_Network_t *specNetwork,
        Ntk_Network_t *implNetwork,
        int initManagerHere,
        int done,
        st_table *outputMatch,
        st_table *inputMatch,
        st_table *directVerifyMatch,
        st_table *oldSpecMddIdTable,
        st_table *oldImplMddIdTable,
        array_t *specLayerArray,
        array_t *implLayerArray)
{
  bdd_manager *ddManager;

  if (initManagerHere) {
    ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
    if (ddManager != NIL(bdd_manager)) {
      mdd_quit(ddManager);
      Ntk_NetworkSetMddManager(specNetwork, NIL(mdd_manager));
      Ntk_NetworkSetMddManager(implNetwork, NIL(mdd_manager));
    }
  }

  if (done != RES_VERIFY_NOTHING) {  /* if result structure allocated */
    if (error) { /* on error free results */
      if (done == RES_VERIFY_IGNORE_PREV_RESULTS) {
        /* if spec result was created here */
        Ntk_NetworkFreeApplInfo(specNetwork,RES_NETWORK_APPL_KEY);
      }
      Ntk_NetworkFreeApplInfo(implNetwork,RES_NETWORK_APPL_KEY);
    }
  }
  if (outputMatch != NIL(st_table)) {
    st_free_table(outputMatch);
  }
  if (inputMatch != NIL(st_table)) {
    st_free_table(inputMatch);
  }
  if (directVerifyMatch != NIL(st_table)) {
    st_free_table(directVerifyMatch);
  }

  if (oldSpecMddIdTable != NIL(st_table)) {
    RestoreOldMddIds(specNetwork, oldSpecMddIdTable);
    st_free_table(oldSpecMddIdTable);
  }
  if (oldImplMddIdTable != NIL(st_table)) {
    RestoreOldMddIds(implNetwork, oldImplMddIdTable);
    st_free_table(oldImplMddIdTable);
  }
  if (specLayerArray != NULL) {
    ResLayerArrayFree(specLayerArray);
  }
  if (implLayerArray != NULL) {
    ResLayerArrayFree(implLayerArray);
  }
  return;
} /* End of Cleanup */


static st_table *
SaveOldMddIds(Ntk_Network_t *network)
{
  st_table *oldMddIdTable;
  Ntk_Node_t *nodePtr;
  lsGen listGen;             /* To iterate over outputList */

  oldMddIdTable = st_init_table(st_ptrcmp, st_ptrhash);
  if (oldMddIdTable == NULL) return NIL(st_table);

  Ntk_NetworkForEachNode(network, listGen, nodePtr) {
    st_insert(oldMddIdTable, (char *)nodePtr,
              (char *)(long)Ntk_NodeReadMddId(nodePtr));
  }
  return(oldMddIdTable);
}

static int
DirectVerification(Ntk_Network_t *specNetwork,
                   Ntk_Network_t *implNetwork,
                   st_table *directVerifyMatch,
                   st_table *inputMatch,
                   st_table *outputMatch,
                   array_t *outputOrderArray)
{

    Ntk_Node_t *nodePtr, *implNodePtr;         /* node variables */
    long startTime, endTime, directVerifyTime; /* to measure elapsed time */
    long lapTimeSpec, lapTimeImpl;             /* to measure elapsed time */
    bdd_node *specBDD, *implBDD, *permutedBDD;   /* bdds of direct verified outputs */
    lsGen listGen;                             /* To iterate over outputList */
    int *permut;                              /* permutation array to store
                                               * correspondence of inputs
                                               */
    int specMddId, implMddId;
    Ntk_Node_t **specArray, **implArray;      /* arrays to store the
                                               * corresponding nodes of the
                                               * spec. and the impl.
                                               */
    st_generator *stGen;
    lsList dummy;                               /* dummy list fed to the ord
                                                 * package.
                                                 */
    char *key, *value;                          /* variables to read values
                                                 * from the st_table
                                                 */
    int index, i;                               /* iterators */
    char *name;                                 /* variable to read node name */
    int numOutputs;                             /* total number of outputs of
                                                 * the spec.(impl).
                                                 */
    bdd_manager *ddManager;                     /* the bdd manager */
    bdd_reorder_type_t oldDynMethod, dynMethod = BDD_REORDER_SAME;
                                                /* dynamic reordering methods */
    int dynStatus = 0;                          /* original status of the manager
                                                 * w. r. t. dynamic reordering
                                                 */
    boolean dyn;                                /* current dynamic reordering
                                                 * status
                                                 */
    int verbose;                                /* verbosity level */
    char  *flagValue;                           /* string to hold "Set" variable
                                                 * value
                                                 */
    Res_ResidueInfo_t *resultSpec;              /* result structure for the
                                                 * spec.
                                                 */
    Res_ResidueInfo_t *resultImpl;              /* result structure for the
                                                 * impl.
                                                 */
    int specSize, implSize;                     /* sizes of bdds */
    mdd_t *fnMddT;                              /* mdd_t structure to calculate sizes */


    /* Initializations */
    dummy = (lsList)0;
    lapTimeSpec = 0;
    lapTimeImpl = 0;
    dyn = FALSE;
    verbose = 0;

    /* read verbosity value */
    flagValue = Cmd_FlagReadByName("residue_verbosity");
    if (flagValue != NIL(char)) {
      verbose = atoi(flagValue);
    }

    /* read if dynamic ordering is required */
    flagValue = Cmd_FlagReadByName("residue_autodyn_direct_verif");
    if (flagValue != NIL(char)) {
      dyn = (strcmp(flagValue, "1") == 0) ? TRUE : FALSE;
    }
    /* read method for dynamic reordering */
    if (dyn == TRUE) {
      flagValue = Cmd_FlagReadByName("residue_direct_dyn_method");
      if (flagValue != NULL) {
        dynMethod = DecodeDynMethod(flagValue);
      } else {
        dynMethod = BDD_REORDER_SAME;
      }
    }

    /* read manager from network */
    ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
    /* save old values for dynamic reordering */
    if (dyn == TRUE) {
      dynStatus = bdd_reordering_status(ddManager, &oldDynMethod);
      bdd_dynamic_reordering(ddManager, dynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
    }

    /* find total time elapsed */
    directVerifyTime = util_cpu_time();

    /* find number of outputs to be directly verified */
    numOutputs = st_count(directVerifyMatch);

    /*
     * Order primary input variables in the network to build the BDDs for
     * outputs to be directly verified.
     */
    if (Ord_NetworkTestAreVariablesOrdered(specNetwork,
                                           Ord_InputAndLatch_c) == FALSE) {
      /* order the variables in the network since not done */
      startTime = util_cpu_time();
      Ord_NetworkOrderVariables(specNetwork, Ord_RootsByDefault_c,
                      Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c,
                      Ord_Unassigned_c, dummy, 0);

      endTime = util_cpu_time();
      lapTimeSpec += endTime - startTime;

      startTime = endTime;
      Ord_NetworkOrderVariables(implNetwork, Ord_RootsByDefault_c,
                      Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c,
                      Ord_Unassigned_c, dummy, 0);
      lapTimeImpl += endTime - startTime;

    } else {
      /* if order is not specified, assume the same order for spec.
       * and implementation
       */
      Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
        assert(Ntk_NodeReadMddId(nodePtr) != NTK_UNASSIGNED_MDD_ID);
        st_lookup(inputMatch, (char *)nodePtr, &implNodePtr);
        Ntk_NodeSetMddId(implNodePtr, Ntk_NodeReadMddId(nodePtr));
      }
    }

    if (verbose >= 5) {
      Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
        specMddId = Ntk_NodeReadMddId(nodePtr);
        if (specMddId != NTK_UNASSIGNED_MDD_ID) {
          fprintf(vis_stdout, "%s ", Ntk_NodeReadName(nodePtr));
        }
      }
      fprintf(vis_stdout, "\n");
      Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
        specMddId = Ntk_NodeReadMddId(nodePtr);
        if (specMddId != NTK_UNASSIGNED_MDD_ID) {
          fprintf(vis_stdout, "%d ", specMddId);
        }
      }
      fprintf(vis_stdout, "\n");
    }

    /* build arrays of corresponding nodes to be directly verified */
    specArray = ALLOC(Ntk_Node_t *, numOutputs);
    implArray = ALLOC(Ntk_Node_t *, numOutputs);
    index = 0;
    /* Order array starting from the LSB, so direct verification is performed
     * starting from the inputs.
     */
    for (i = 0; i < array_n(outputOrderArray); i++) {
      name = array_fetch(char *, outputOrderArray, array_n(outputOrderArray)-1-i);
      nodePtr = Ntk_NetworkFindNodeByName(specNetwork, name);
      /* find node in direct verify match table */
      if (st_lookup(directVerifyMatch, (char *)nodePtr, (char **)&value)) {
        specArray[index] = (Ntk_Node_t *)nodePtr;
        implArray[index] = (Ntk_Node_t *)value;
        index++;
      }
    }
    /* number of outputs in the arrays should be as many entries as the match
     * table.
     */
    assert(numOutputs == index);

    /* Create a permutation array for the specMddId and implMddId input nodes */
    permut = ALLOC(int, bdd_num_vars(ddManager));
    for (i= 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
      permut[i] = i;
    }
    st_foreach_item(inputMatch, stGen, &key, &value) {
      nodePtr = (Ntk_Node_t *)key;
      implNodePtr = (Ntk_Node_t *)value;
      if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))){
        error_append("Input match values do not return");
        error_append("valid node pointers.\n");
        /* Clean up */
        FREE(permut);
        FREE(specArray);
        FREE(implArray);
        st_free_gen(stGen);
        return 1;
      }
      /* create the array with the impl. vars to be composed with spec. vars. */
      specMddId = Ntk_NodeReadMddId(nodePtr);
      implMddId = Ntk_NodeReadMddId(implNodePtr);
      /* there should be no node with NTK_UNASSIGNED_MDD_ID due to the
       * ordering above
       */
      assert(specMddId != NTK_UNASSIGNED_MDD_ID);
      assert(implMddId != NTK_UNASSIGNED_MDD_ID);
      permut[implMddId] = specMddId;

    } /* end of input match */

    /*
     * Build BDDs for each output to be directly verified and check
     * for identical BDDs in spec. and impl.
     */
    for (i = 0; i < numOutputs; i++) {
      /* build the spec BDD */
      startTime = util_cpu_time();
      specBDD = BuildBDDforNode(specNetwork, specArray[i], PRIMARY_INPUTS);
      if (specBDD == NIL(bdd_node)) {
        error_append("Unable to build spec. BDD for the direct verification output");
        error_append(Ntk_NodeReadName(specArray[i]));
        error_append(".\n");
        /* Clean up */
        FREE(permut);
        FREE(specArray);
        FREE(implArray);
        return 1; /* error status */
      } /* end of if spec BDD is NIL */
      endTime = util_cpu_time();
      lapTimeSpec += endTime - startTime;

      /* build the impl BDD */
      startTime = endTime;
      implBDD = BuildBDDforNode(implNetwork, implArray[i], PRIMARY_INPUTS);
      if (implBDD == NIL(bdd_node)) {
        error_append("Unable to build spec. BDD for the direct verification output");
        error_append(Ntk_NodeReadName(implArray[i]));
        error_append(".\n");
        /* Clean up */
        bdd_recursive_deref(ddManager, specBDD);
        FREE(permut);
        FREE(specArray);
        FREE(implArray);
        return 1; /* error status */
      } /* end of if spec BDD is NIL */
      endTime = util_cpu_time();
      lapTimeImpl += endTime - startTime;

      /* call bdd permute to compose the impl variables with the spec
       * variables.
       */
      startTime = endTime;
      bdd_ref(permutedBDD = bdd_bdd_permute(ddManager, implBDD, permut));
      bdd_recursive_deref(ddManager, implBDD);
      endTime = util_cpu_time();
      lapTimeSpec += (endTime - startTime)/2;
      lapTimeImpl += (endTime - startTime)/2;
      implBDD = permutedBDD;
      if (implBDD == NIL(bdd_node)) {
        error_append("Permuting the impl bdd in terms of spec bdd vars failed\n");
        /* Clean up */
        bdd_recursive_deref(ddManager, specBDD);
        FREE(permut);
        FREE(specArray);
        FREE(implArray);
        return 1; /* error status */
      }

      /* compare the bdds */
      if(specBDD != implBDD)  {
        /* error since spec and impl are not the same */
        /* update result structure */
        if (verbose >= 2) {
          (void)fprintf(vis_stdout, "Vector where the two networks differ :\n");
          (void)fprintf(vis_stdout, "Specification Input Names :\n");
          ExtractACubeOfDifference(ddManager, specNetwork, specBDD, implBDD);
        }
        resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
                                          RES_NETWORK_APPL_KEY);
        resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
                                          RES_NETWORK_APPL_KEY);
        ResResidueInfoSetDirectVerificationSuccess(resultSpec, RES_FAIL);
        ResResidueInfoSetDirectVerificationSuccess(resultImpl, RES_FAIL);
        (void) fprintf(vis_stdout, "%.2f (secs) spent in failed direct verification.\n",
                       (util_cpu_time() - directVerifyTime)/1000.0);
        fprintf(vis_stdout, "Residue Direct Verification failed at output node ");
        fprintf(vis_stdout, "%s", Ntk_NodeReadName(specArray[i]));
        fprintf(vis_stdout, " of the spec.\n");
        fprintf(vis_stdout, "Spec. did not match Impl.\n");
        /* Clean up */
        /* free the bdds just created */
        bdd_recursive_deref(ddManager, specBDD);
        bdd_recursive_deref(ddManager, implBDD);
        FREE(permut);
        FREE(specArray);
        FREE(implArray);
        return 0;
      } /* end if spec BDD != impl BDD */

      /* if the bdds are equal, print some information */
      if (verbose >= 2) {
        fprintf(vis_stdout, "%d out of %d ", i + 1 ,numOutputs);
        fprintf(vis_stdout, "direct verification outputs done.\n");
      }
      if (verbose >= 3) {
        fprintf(vis_stdout, "%s(spec)/%s(impl) output verified. \n",
                Ntk_NodeReadName(specArray[i]), Ntk_NodeReadName(implArray[i]));
        bdd_ref(specBDD);
        fnMddT = bdd_construct_bdd_t(ddManager, specBDD);
        specSize = bdd_size(fnMddT);
        bdd_free(fnMddT);
        bdd_ref(implBDD);
        fnMddT = bdd_construct_bdd_t(ddManager, implBDD);
        implSize = bdd_size(fnMddT);
        bdd_free(fnMddT);
        fprintf(vis_stdout, "Size of %s(spec) = %d, Size of %s(impl) = %d\n",
         Ntk_NodeReadName(specArray[i]) ,specSize, Ntk_NodeReadName(implArray[i]), implSize);
        fprintf(vis_stdout, "%.3f spec time elapsed, %.3f impl. time elapsed.\n", lapTimeSpec/1000.0,
                lapTimeImpl/1000.0);
      }
      /* free the bdds just created */
      bdd_recursive_deref(ddManager, specBDD);
      bdd_recursive_deref(ddManager, implBDD);

    } /* end of for-loop that iterates through the nodes to be directly
       * verified.
       */

    FREE(permut);
    FREE(specArray);
    FREE(implArray);

    /* set direct verification success info */
    /* update result structure */
    resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
                                                        RES_NETWORK_APPL_KEY);
    resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
                                                        RES_NETWORK_APPL_KEY);
    ResResidueInfoSetDirectVerificationSuccess(resultSpec, RES_PASS);
    ResResidueInfoSetCpuDirectVerif(resultSpec, (float) lapTimeSpec);
    ResResidueInfoSetDirectVerificationSuccess(resultImpl, RES_PASS);
    ResResidueInfoSetCpuDirectVerif(resultImpl, (float) lapTimeImpl);

    /* Print success message */
    fprintf(vis_stdout, "Residue Direct Verification successful.\n");

    /* Print Time taken for direct verification */
    if (verbose >= 1) {
      (void) fprintf(vis_stdout, "%.2f (secs) spent in Direct verification.\n",
                       (util_cpu_time() - directVerifyTime)/1000.0);
    }

    /* Print which outputs were directly verified and time spent for
     * the spec and the impl
     */
    if (verbose >= 2) {
      fprintf(vis_stdout, "Time taken to build spec. BDD = %.3f\n",
              ResResidueInfoReadCpuDirectVerif(resultSpec)/1000.0);
      fprintf(vis_stdout, "Time taken to build impl. BDD = %.3f\n",
              ResResidueInfoReadCpuDirectVerif(resultImpl)/1000.0);
      st_foreach_item(directVerifyMatch, stGen, &key, &value) {
        fprintf(vis_stdout, "%s ", Ntk_NodeReadName((Ntk_Node_t *)key));
      }
      fprintf(vis_stdout, "verified successfully.\n");
    }

    /* Print order of variables of this verification */
    if (verbose >= 3) {
      Ord_NetworkPrintVariableOrder(vis_stdout, specNetwork,
      Ord_InputAndLatch_c);
      Ord_NetworkPrintVariableOrder(vis_stdout, implNetwork,
      Ord_InputAndLatch_c);
    }

    /* restore the old values for dynamic reordering */
    if(dyn == TRUE) {
      bdd_dynamic_reordering(ddManager, oldDynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
      if (!dynStatus) {
        bdd_dynamic_reordering_disable(ddManager);
      }
    }

    return 0; /* direct verification success */
} /* End of Direct Verification */


static bdd_reorder_type_t
DecodeDynMethod(char *dynMethodString)
{
  bdd_reorder_type_t dynMethod;

  /* Translate reordering string to specifying method */
  if (dynMethodString == NIL(char)) {
    dynMethod = BDD_REORDER_SIFT;
  } else if (strcmp(dynMethodString, "same") == 0) {
    dynMethod = BDD_REORDER_SAME;
  } else if (strcmp(dynMethodString, "none") == 0) {
    dynMethod = BDD_REORDER_NONE;
  } else if (strcmp(dynMethodString, "random") == 0) {
    dynMethod = BDD_REORDER_RANDOM;
  } else if (strcmp(dynMethodString, "randompivot") == 0) {
    dynMethod = BDD_REORDER_RANDOM_PIVOT;
  } else if (strcmp(dynMethodString, "sift") == 0) {
    dynMethod = BDD_REORDER_SIFT;
  } else if (strcmp(dynMethodString, "siftconverge") == 0) {
    dynMethod = BDD_REORDER_SIFT_CONVERGE;
  } else if (strcmp(dynMethodString, "symmsift") == 0) {
    dynMethod = BDD_REORDER_SYMM_SIFT;
  } else if (strcmp(dynMethodString, "symmsiftconverge") == 0) {
    dynMethod = BDD_REORDER_SYMM_SIFT_CONV;
  } else if (strcmp(dynMethodString, "window2") == 0) {
    dynMethod = BDD_REORDER_WINDOW2;
  } else if (strcmp(dynMethodString, "window3") == 0) {
    dynMethod = BDD_REORDER_WINDOW3;
  } else if (strcmp(dynMethodString, "window4") == 0) {
    dynMethod = BDD_REORDER_WINDOW4;
  } else if (strcmp(dynMethodString, "window2converge") == 0) {
    dynMethod = BDD_REORDER_WINDOW2_CONV;
  } else if (strcmp(dynMethodString, "window3converge") == 0) {
    dynMethod = BDD_REORDER_WINDOW3_CONV;
  } else if (strcmp(dynMethodString, "window4converge") == 0) {
    dynMethod = BDD_REORDER_WINDOW4_CONV;
  } else if (strcmp(dynMethodString, "groupsift") == 0) {
    dynMethod = BDD_REORDER_GROUP_SIFT;
  } else if (strcmp(dynMethodString, "groupsiftconverge") == 0) {
    dynMethod = BDD_REORDER_GROUP_SIFT_CONV;
  } else if (strcmp(dynMethodString, "anneal") == 0) {
    dynMethod = BDD_REORDER_ANNEALING;
  } else if (strcmp(dynMethodString, "genetic") == 0) {
    dynMethod = BDD_REORDER_GENETIC;
  } else if (strcmp(dynMethodString, "linear") == 0) {
    dynMethod = BDD_REORDER_LINEAR;
  } else if (strcmp(dynMethodString, "linearconverge") == 0) {
    dynMethod = BDD_REORDER_LINEAR_CONVERGE;
  } else if (strcmp(dynMethodString, "exact") == 0) {
    dynMethod = BDD_REORDER_EXACT;
  } else {
    dynMethod = BDD_REORDER_SIFT;
  }
  return dynMethod;
} /* End of DecodeDynMethod */



static int
ResidueVerification(Ntk_Network_t *specNetwork,
                    Ntk_Network_t *implNetwork,
                    st_table *outputMatch,
                    st_table *inputMatch,
                    int numDirectVerify,
                    array_t *specLayerArray,
                    array_t *implLayerArray,
                    array_t *outputArray)
{
  int numOutputs;                 /* number of outputs in the networks */
  int actualOutputs;                 /* number of outputs in the networks */
  int msbId;                      /* stores the top Id available */
  int msbLsb;                     /* 1 means Msb on top */

  Ntk_Node_t *nodePtr, *implNodePtr; /* variables to store nodes in networks */

  Res_ResidueInfo_t *resultSpec;   /* spec. result structure */
  Res_ResidueInfo_t *resultImpl;   /* impl. result structure */

  int verbose;                     /* verbosity value */
  char *flagValue;                 /* string to store flag values */
  int i;                           /* iterating index */

  lsGen listGen;                   /* list generator for looping over nodes
                                    * in a network.
                                    */
  st_generator *stGen;     /* generator to step through st_table */
  char *key, *value;               /* variables to read in st-table values */
  long overallLap;      /* to measure elapsed time */
  long lap;     /* to measure elapsed time */
  int primeIndex;       /* index to iterate over prime array */
  bdd_manager *ddManager;      /* Manager read from the network */
  bdd_node *implADD, *specADD, *tmpDd; /* final ADDs after composition */
  int specSize, implSize;               /* sizes of bdds */
  int specMddId, implMddId;  /* id variables for nodes */
  bdd_node *residueDd;  /* residue ADD (n x m) */
  int *permut;  /* array to permute impl ADD variables to spec.
                                 * ADD variables.
                                 */
  int numOfPrimes;      /* Number of primes needed for verification */
  int *primeTable;      /* array to store primes needed for current
                                 * verification
                                 */
  bdd_reorder_type_t oldDynMethod, dynMethod; /* dynamic reordering
                                               * methods
                                               */
  int dynStatus;                /* Status of manager w.r.t. original
                                 * reordering
                                 */
  boolean dyn;          /* flag to indicate dynamic reordering
                                 * is turned on.
                                 */
  mdd_t *fnMddT;                /* mdd_t structure to calculate sizes */
  int unassignedValue;          /* NTK_UNASSIGNED_MDD_ID value holder */
  array_t *implOutputArray;     /* array of output nodes of the impl.in consideration
                                 * for composition
                                 */

  /* Initialization */
  verbose = 0;
  unassignedValue =  NTK_UNASSIGNED_MDD_ID;
  numOfPrimes = 0;
  msbLsb = 1; /* default value msb is on top */
  primeTable = NULL;
  overallLap = util_cpu_time();
  dyn = FALSE; /* default dynamic reordering disabled */
  permut = NULL;

  /* specify if the top var of the residue ADD is the MSB/LSB */
  flagValue = Cmd_FlagReadByName("residue_top_var");
  if (flagValue != NIL(char) && strcmp(flagValue,"lsb") == 0) {
    msbLsb = 0;
  } else {
    msbLsb = 1;
  }

  /* initialize number of outputs */
  actualOutputs = Ntk_NetworkReadNumCombOutputs(specNetwork);

  /* Read the mdd Manager (or create it if necessary) */
  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
    /* save old dynamic reordering values */
  dynStatus = bdd_reordering_status(ddManager, &oldDynMethod);

  /* read verbosity value */
  flagValue = Cmd_FlagReadByName("residue_verbosity");
  if (flagValue != NIL(char)) {
    verbose = atoi(flagValue);
  }

  /* read if dynamic ordering is required */
  flagValue = Cmd_FlagReadByName("residue_autodyn_residue_verif");
  if (flagValue != NIL(char)) {
    dyn = (strcmp(flagValue,"1")==0) ? TRUE : FALSE;
  }
  /* read method of dynamic reordering */
  if (dyn == TRUE) {
    flagValue = Cmd_FlagReadByName("residue_residue_dyn_method");
    if ( flagValue != NULL) {
      dynMethod = DecodeDynMethod(flagValue);
    } else {
      dynMethod = BDD_REORDER_SAME;
    }
    /* update manager with dynamic reordering and the method */
    bdd_dynamic_reordering(ddManager, dynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
  } else {
    /* unless specified, TURN REORDERING OFF for residue verification */
    bdd_dynamic_reordering_disable(ddManager);
  }

  /*
   * Choose the set of primes that will be used, primeTable is allocated
   * here.
   */
  numOfPrimes = ChoosePrimes(actualOutputs,  &primeTable, numDirectVerify);

  /* get result structures */
  resultSpec = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(specNetwork,
                                                    RES_NETWORK_APPL_KEY);
  resultImpl = (Res_ResidueInfo_t *)Ntk_NetworkReadApplInfo(implNetwork,
                                                    RES_NETWORK_APPL_KEY);

  /* update result with primes info */
  if ((resultSpec  != NIL(Res_ResidueInfo_t)) && (resultImpl != NIL(Res_ResidueInfo_t))) {
    ResResidueInfoAllocatePrimeInfoArray(resultSpec, numOfPrimes, primeTable);
    ResResidueInfoAllocatePrimeInfoArray(resultImpl, numOfPrimes, primeTable);
    ResResidueInfoSetNumOfPrimes(resultSpec, numOfPrimes);
    ResResidueInfoSetNumOfPrimes(resultImpl, numOfPrimes);
  } else {
    /* error - the result structure should be there */
    error_append("Result structures are missing\n");
    FREE(primeTable);
    return 1;
  }

  /* Print the list of primes depending on the verbosity level*/
  if (verbose >= 0) {
    (void) fprintf(vis_stdout, "List of Primes used: ");
    for(i=0; i<numOfPrimes; i++) {
      (void) fprintf(vis_stdout, "%d ", primeTable[i]);
    }
    (void) fprintf(vis_stdout, "\n");
  } /* End of if */

  /* form impl Output Array */
  implOutputArray = array_alloc(Ntk_Node_t *, array_n(outputArray));
  arrayForEachItem(Ntk_Node_t *, outputArray, i, nodePtr) {
    st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
    array_insert(Ntk_Node_t *, implOutputArray, i, implNodePtr);
  }

  /* number of outputs in consideration */
  numOutputs = array_n(outputArray);


  /* Main Loop in which the verification is done for each prime. */
  for(primeIndex = 0; primeIndex < numOfPrimes; primeIndex++) {
    int currentPrime;

    /* Read current prime from table */
    currentPrime = primeTable[primeIndex];
    if (verbose >=2)
      (void) fprintf(vis_stdout, "Processing prime %d:\n", currentPrime);

    /* update the mdd manager with the first set of output variables */
    MddCreateVariables((mdd_manager *)ddManager, numOutputs-bdd_num_vars(ddManager));


    /* Obtain the residue bdd for the given prime, assume top id is
     * always 0i.e. msbId = 0;
     */
    msbId = 0;
    bdd_ref(residueDd = bdd_add_residue(ddManager, numOutputs, currentPrime,
                                         msbLsb, msbId));

    /*  Set the output Id. Needs to be set each time because it gets
     * cleared each time.
     */
    arrayForEachItem(Ntk_Node_t *, outputArray, i , nodePtr) {
      st_lookup(outputMatch, (char *)nodePtr, &implNodePtr);
      if (msbLsb == 1) {
        Ntk_NodeSetMddId(nodePtr, i);
        Ntk_NodeSetMddId(implNodePtr, i);
      } else {
        Ntk_NodeSetMddId(nodePtr, numOutputs - i);
        Ntk_NodeSetMddId(implNodePtr, numOutputs - i);
      }
    }


    /* Set the cpu usage lap */
    lap = util_cpu_time();

    if (verbose >= 1) {
      fprintf(vis_stdout, "Specification being built\n");
    }
    /* the actual composition of the spec. network into the residue ADD
     * is done here. The composed ADD return is referenced
     */
    specADD = ComposeLayersIntoResidue(specNetwork, specLayerArray, residueDd, outputArray);
    if (specADD == NIL(bdd_node)) {
      error_append("Composition of spec. failed.\n");
      /* Clean up before you leave */
      array_free(implOutputArray);
      FREE(primeTable);
      bdd_recursive_deref(ddManager, residueDd);
      return 1; /* error return */
    }

    /* Store the information in the result structure of the spec.*/
    bdd_ref(specADD);
    fnMddT = bdd_construct_bdd_t(ddManager, specADD);
    specSize = bdd_size(fnMddT);
    bdd_free(fnMddT);
    ResResidueInfoSetPerPrimeInfo(resultSpec, primeIndex, currentPrime,
                                  (util_cpu_time() - lap)/1000.0, specSize, specADD);
    /* Print info regarding this prime if pertinent */
    if (verbose >=3) {
      (void) fprintf(vis_stdout, "%.2f (secs) spent in composing prime\n",
                     ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->cpuTime);
      (void) fprintf(vis_stdout, "Composed Dd with %d nodes\n", specSize);
    }

    /* Set the cpu usage lap */
    lap = util_cpu_time();

    /*
     * the actual composition of the impl. network into the residue ADD
     * is done here. The composed ADD return is referenced
     */
    if (verbose >= 1) {
      fprintf(vis_stdout, "Implementation being built\n");
    }
    implADD = ComposeLayersIntoResidue(implNetwork, implLayerArray, residueDd, implOutputArray);

    bdd_recursive_deref(ddManager, residueDd);
    if (implADD == NIL(bdd_node)) {
      error_append("Composition of spec. failed.\n");
      /* Clean up before you leave */
      bdd_recursive_deref(ddManager, specADD);
      array_free(implOutputArray);
      FREE(primeTable);
      return 1; /* error return */
    }

    /* Create a permutation array for the specMddId and implMddId input nodes */
    permut = ALLOC(int, bdd_num_vars(ddManager));
    for (i= 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
      permut[i] = i;
    }
    st_foreach_item(inputMatch, stGen, &key, &value) {
      nodePtr = (Ntk_Node_t *)key;
      implNodePtr = (Ntk_Node_t *)value;
      if ((nodePtr == NIL(Ntk_Node_t)) || (implNodePtr == NIL(Ntk_Node_t))){
        error_append("Input match values do not return");
        error_append("valid node pointers.\n");
        /* Clean up */
        FREE(permut);
        FREE(primeTable);
        array_free(implOutputArray);
        bdd_recursive_deref(ddManager, specADD);
        bdd_recursive_deref(ddManager, implADD);
        st_free_gen(stGen);
        return 1;
      }
      /* create the array with the impl. vars to be composed with spec. vars. */
      specMddId = Ntk_NodeReadMddId(nodePtr);
      implMddId = Ntk_NodeReadMddId(implNodePtr);

      /* there should be no node with NTK_UNASSIGNED_MDD_ID due to the
       * ordering above
       */

#if 0
      if (Ntk_NodeReadNumFanouts(nodePtr) != 0) {
        assert(specMddId != NTK_UNASSIGNED_MDD_ID);
      }
      if (Ntk_NodeReadNumFanouts(implNodePtr) != 0) {
        assert(implMddId != NTK_UNASSIGNED_MDD_ID);
      }
#endif

      if ((specMddId != NTK_UNASSIGNED_MDD_ID) &&
          (implMddId != NTK_UNASSIGNED_MDD_ID)) {
        permut[implMddId] = specMddId;
      } else {
        assert(specMddId == implMddId);
      }

    } /* end of st_foreach_item */

    /* permute the variables so that the impl variables are replaced by
     * spec. variables
     */
    bdd_ref(tmpDd = bdd_add_permute(ddManager, implADD, permut));
    bdd_recursive_deref(ddManager, implADD);
    FREE(permut);
    implADD = tmpDd;
    if(implADD == NIL(bdd_node)) { /* error */
      error_append("Last composition failed,");
      error_append("Cannot compose spec. ADD PI vars into Impl. ADD.\n");
      FREE(primeTable);
      array_free(implOutputArray);
      return 1; /* error return */
    }

    if (verbose > 0) {
      (void) fprintf(vis_stdout, "%.2f (secs) spent in residue verification.\n",
                     (util_cpu_time() - overallLap)/1000.0);
    }

    /* Store the information in the result structure of the impl.*/
    bdd_ref(implADD);
    fnMddT = bdd_construct_bdd_t(ddManager, implADD);
    implSize = bdd_size(fnMddT);
    bdd_free(fnMddT);
    ResResidueInfoSetPerPrimeInfo(resultImpl, primeIndex, currentPrime,
         (util_cpu_time() - lap)/1000.0, implSize, implADD);
    /* Print info regarding this prime if pertinent */
    if (verbose >=3) {
      (void) fprintf(vis_stdout, "%.2f (secs) spent in composing prime\n",
                     ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->cpuTime);
      (void) fprintf(vis_stdout, "Composed Dd with %d nodes\n", implSize);
    }


    /* Compare the Spec and the Impl composed Dds */
    if (ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->residueDd !=
        ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->residueDd) {
      ResResidueInfoSetSuccess(resultSpec, RES_FAIL);
      ResResidueInfoSetSuccess(resultImpl, RES_FAIL);
      (void) fprintf(vis_stdout, "Verification of %s and %s failed.\n",
                     Res_ResidueInfoReadName(resultSpec),
                     Res_ResidueInfoReadName(resultImpl));
      (void)fprintf(vis_stdout,"The composed ADDs with residue are not the same.\n");
      (void)fprintf(vis_stdout,"Verification failed at prime %d.\n", currentPrime);
      if (verbose >= 2) {
        (void)fprintf(vis_stdout, "Vector where the two networks differ :\n");
        (void)fprintf(vis_stdout, "Specification Input Names :\n");
        ExtractACubeOfDifference(ddManager, specNetwork, specADD, implADD);
      }

      /* Clean up before you leave */
      bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->residueDd);
      ResResidueInfoSetPerPrimeDd(resultSpec, primeIndex, NIL(bdd_node));

      bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->residueDd);
      ResResidueInfoSetPerPrimeDd(resultImpl, primeIndex, NIL(bdd_node));
      array_free(implOutputArray);
      FREE(primeTable);
      return 0;
    } else {

      /* free the result Dd*/
      bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultSpec, primeIndex)->residueDd);
      ResResidueInfoSetPerPrimeDd(resultSpec, primeIndex, NIL(bdd_node));

      bdd_recursive_deref(ddManager, ResResidueInfoReadPerPrimeInfo(resultImpl, primeIndex)->residueDd);
      ResResidueInfoSetPerPrimeDd(resultImpl, primeIndex, NIL(bdd_node));
    }


    /* reset node Ids of primary inputs */
    Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
      Ntk_NodeSetMddId(nodePtr, unassignedValue);
    }
    Ntk_NetworkForEachCombInput(implNetwork, listGen, nodePtr) {
      Ntk_NodeSetMddId(nodePtr, unassignedValue);
    }


  } /* End of the main for-loop */
  FREE(primeTable);
  array_free(implOutputArray);

  /* restore old dynamic reordering values */
  bdd_dynamic_reordering(ddManager, oldDynMethod, BDD_REORDER_VERBOSITY_DEFAULT);
  if (!dynStatus) {
    bdd_dynamic_reordering_disable(ddManager);
  }

  /* set pass flag if residue verification success and direct verification
   * success.
   */
  if (((numDirectVerify) &&
       (ResResidueInfoReadDirectVerificationSuccess(resultSpec) == RES_PASS)) ||
       (ResResidueInfoReadDirectVerificationSuccess(resultSpec) != RES_FAIL)) {
    ResResidueInfoSetSuccess(resultSpec, RES_PASS);
  }
  if (((numDirectVerify) &&
       (ResResidueInfoReadDirectVerificationSuccess(resultImpl) == RES_PASS)) ||
      (ResResidueInfoReadDirectVerificationSuccess(resultImpl) != RES_FAIL)) {
    ResResidueInfoSetSuccess(resultImpl, RES_PASS);
  }
  return 0;
} /* End of ResidueVerification */

static void
ExtractACubeOfDifference(bdd_manager *mgr,
                         Ntk_Network_t *specNetwork,
                         bdd_node *fn1,
                         bdd_node *fn2)
{
  bdd_t *fnMddT, *fnMddT1;      /* mdd_t structure to calculate sizes */
  bdd_t *fnMddT2, *fnMddT3;     /* mdd_t structure to calculate sizes */
  bdd_gen *gen;
  array_t *cube, *namesArray;
  lsGen listGen;
  int i, literal;
  Ntk_Node_t *nodePtr;

  /* make bdd_ts of the two functions */
  bdd_ref(fn2);
  fnMddT = bdd_construct_bdd_t(mgr, fn2);
  bdd_ref(fn1);
  fnMddT1 = bdd_construct_bdd_t(mgr, fn1);
  fnMddT2 = bdd_not(fnMddT1);
  /* extracts some cubes in the intersection of fn1' and fn2 */
  fnMddT3 = bdd_intersects(fnMddT, fnMddT2);
  /* check not zero */
  if (bdd_is_tautology(fnMddT3, 0)) {
    bdd_free(fnMddT3);
    bdd_free(fnMddT2);
    /* extracts some cubes in the intersection of fn2' and fn1 */
    fnMddT2 = bdd_not(fnMddT);
    fnMddT3 = bdd_intersects(fnMddT1, fnMddT2);
  }
  assert(!bdd_is_tautology(fnMddT3, 0));
  bdd_free(fnMddT);
  bdd_free(fnMddT1);
  bdd_free(fnMddT2);

  /* pick a cube from the xor of fn1 and fn2 */
  gen = bdd_first_cube(fnMddT3, &cube);
  bdd_free(fnMddT3);

  /* store the names to be printed out later */
  namesArray = array_alloc(char *, array_n(cube));
  Ntk_NetworkForEachCombInput(specNetwork, listGen, nodePtr) {
    array_insert(char *, namesArray , Ntk_NodeReadMddId(nodePtr),  Ntk_NodeReadName(nodePtr));
  }

  /* print out the cube */
  arrayForEachItem(int, cube, i, literal) {
    if (literal != 2) {
      (void) fprintf(vis_stdout, "%s ", array_fetch(char *, namesArray, i));
    }
  }
  fprintf(vis_stdout, "\n");
  arrayForEachItem(int, cube, i, literal) {
    if (literal != 2) {
      (void) fprintf(vis_stdout, "%1d", literal);
    }
  }
  fprintf(vis_stdout, "\n");
  array_free(namesArray);
  bdd_gen_free(gen);
  return;
}