src/res/resCmd.c

Go to the documentation of this file.

#include "resInt.h" 

static char rcsid[] UNUSED = "$Id: resCmd.c,v 1.58 2010/04/10 00:38:26 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


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


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


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

static jmp_buf timeOutEnv;

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


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

static int CommandResVerify(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static void TimeOutHandle(void);
static st_table * ReadMatchingPairs(char *fileName, Ntk_Network_t *ntk1, Ntk_Network_t *ntk2);
static array_t * ReadOutputOrder(char *fileName, Ntk_Network_t *ntk1);
static array_t * GenerateDefaultOutputOrder(Ntk_Network_t *specNetwork);
static int CheckForMultiValueNode(Ntk_Network_t *network);

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

void
Res_Init(void)
{
  Cmd_CommandAdd("res_verify", CommandResVerify, /* doesn't changes_network */ 0);
}


void
Res_End(void)
{
  /*
   * For example, free any global memory (if any) which the test package is
   * responsible for.
   */
}

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


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

static int
CommandResVerify(Hrc_Manager_t ** hmgr,
                 int  argc,
                 char ** argv)
{
  static int           timeOutPeriod; /* CPU seconds allowed */
  static array_t       *outputOrderArray;   /* required to specify the outputs
                                       * starting with MSB first */
  static Hrc_Manager_t *implHmgr;     /* Auxiliary hierarchy manager */
  static Hrc_Manager_t *specHmgr;     /* Auxiliary hierarchy manager */
  static Hrc_Node_t    *currentNode;  /* node in the hierarchy */
  static Ntk_Network_t *specNetwork;  /* spec network */
  static Ntk_Network_t *implNetwork;  /* implementation network */
  static st_table      *inputMatch;   /* List of pairs of input name match */
  static st_table      *outputMatch;  /* List of pairs of output name match */
  int                  outputsToVerifyDirectly; /* number of outputs to
                                                 * directly verify
                                                 */
  int                  c;             /* To process the command line options */
  /* Flush previous verification if any */
  int                  success;       /* Outcome of the verification */
  int                  status;        /* Status of the call to the function */
  char                 *specFileName;  /* File to read the specification from */
  char                 *impFileName;  /* File to read the implementation from */
  char                 *fileMatchOut; /* File specifying the output matching */
  char                 *fileMatchIn;  /* File specifying the input matching */
  char                 *fileOutputOrder; /*file name that contains the order of
                                           outputs starting with MSB */
  boolean              isInBlifMv;    /* Format to be read in */
  st_generator         *stGen;        /* generator to step through the table */
  char                 *key, *value;  /* variables for the st_table */
  int i;
  int defaultOutputOrder;             /* flag to indicate default order to
                                       * be taken, if no output order file
                                       * is specified
                                       */
  char                 *strptr;       /* variable to hold return value
                                       * of strtol
                                       */
  int                  allFlag;
  
  if (bdd_get_package_name() != CUDD) {
    fprintf(vis_stdout, "** res error: Residue Verification is available with the CUDD package only.\n");
    return 0;
  }
  /* Default values for some variables */
  timeOutPeriod = 0;
  allFlag = 1;
  outputsToVerifyDirectly = 0;
  outputOrderArray = NIL(array_t);
  implHmgr = NIL(Hrc_Manager_t);
  specHmgr = NIL(Hrc_Manager_t);
  currentNode = NIL(Hrc_Node_t);
  specNetwork = NIL(Ntk_Network_t);
  implNetwork = NIL(Ntk_Network_t);
  inputMatch = NIL(st_table);
  outputMatch = NIL(st_table);
  impFileName = NIL(char);
  specFileName = NIL(char);
  isInBlifMv = FALSE;
  fileMatchOut = NIL(char);
  fileMatchIn = NIL(char);
  status = 1;
  fileOutputOrder = NIL(char);
  defaultOutputOrder = 0;
  
  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "bd:hi:m:n:o:Os:t:")) != EOF) {
    switch(c) {
    case 'b':
      isInBlifMv = TRUE;
      break;
    case 'd':
      /* number of outputs to verify directly */
      /*      outputsToVerifyDirectly = atoi(util_optarg); */
      outputsToVerifyDirectly = (int)strtol(util_optarg, &strptr, 0);
      allFlag = strcmp(util_optarg, "all");
      break;
    case 'h':
      goto usage;
    case 'i':
      impFileName = util_optarg;
      break;
    case 'm':
      fileMatchOut = util_optarg;
      break;
    case 'n':
      fileMatchIn = util_optarg;
      break;
    case 'o':
      fileOutputOrder = util_optarg;
      break;
    case 'O':
      defaultOutputOrder = 1;
      break;
    case 's':
      specFileName = util_optarg;
      break;
    case 't':
      timeOutPeriod = atoi(util_optarg);
      break;
    default:
      goto usage;
    }
  }

  /* Obtain the Specification network either from file or hierarchy manager */
  if (specFileName != NIL(char)) {

    /* Read blif or blif-mv depending on the flag */
    error_init();
    if (isInBlifMv) {
      FILE *fp; /* Used to read from files */

      /* Open the file */
      fp = Cmd_FileOpen(specFileName, "r", NIL(char *), TRUE);
      if (fp != NULL) {
        specHmgr = Io_BlifMvRead(fp, NIL(Hrc_Manager_t),
                                 0, /* No Cannonical */
                                 0, /* No incremental */
                                 0  /* No verbosity */);
        fclose(fp);
      } else {
        fprintf(vis_stderr, "** res error: Specification file required(may not exist in path)\n");
        goto usage;
      }

    } /* End of then */ 
    else {
      specHmgr = Io_BlifRead(specFileName, 0 /* No verbosity */);
    } /* End of if-then-else */

    /* Check if the read has been performed correctly */
    if (specHmgr == NIL(Hrc_Manager_t)) {
      (void) fprintf(vis_stderr, "%s", error_string());
      (void) fprintf(vis_stderr, "Cannot read blif file %s.\n", impFileName);
      goto cleanup;
    }
    
    /* Hierarchy manager successfully created */
    error_init();
    currentNode = Hrc_ManagerReadCurrentNode(specHmgr);
    specNetwork = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, (lsList)0);
    if (specNetwork == NIL(Ntk_Network_t)) {
      (void) fprintf(vis_stderr, "%s", error_string());
      (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
      goto cleanup;
    }
  } else {
    /* Check if any circuit has been read in */
    currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
    if (currentNode == NIL(Hrc_Node_t)) {
      (void) fprintf(vis_stderr, "The hierarchy manager is empty. ");
      (void) fprintf(vis_stderr, "Read in design.\n");
      goto cleanup;
    }

    /* Check if the network has been created with flatten_hierarchy */
    specNetwork = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
    if (specNetwork == NIL(Ntk_Network_t)) {
      goto cleanup;
    } /* End of if */
  }

  /* Obtain the implementation network from file */
  if (impFileName != NIL(char)) {

    /* Read blif or blif-mv depending on the flag */
    error_init();
    if (isInBlifMv) {
      FILE *fp; /* Used to read from files */

      /* Open the file */
      fp = Cmd_FileOpen(impFileName, "r", NIL(char *), TRUE);

      if (fp != NULL) {
        implHmgr = Io_BlifMvRead(fp, NIL(Hrc_Manager_t),
                                 0, /* No Cannonical */
                                 0, /* No incremental */
                                 0  /* No verbosity */);
        fclose(fp);
      } else {
        fprintf(vis_stderr, "** res error: Implementation file required(may not exist in path)\n");
        goto usage;
      }

    }  else { /* End of then */
      implHmgr = Io_BlifRead(impFileName, 0 /* No verbosity */);
    } /* End of if-then-else */

    /* Check if the read has been performed correctly */
    if (implHmgr == NIL(Hrc_Manager_t)) {
      (void) fprintf(vis_stderr, "%s", error_string());
      (void) fprintf(vis_stderr, "Cannot read blif file %s.\n", impFileName);
      goto cleanup;
    }
    
    /* Hierarchy manager successfully created */
    error_init();
    currentNode = Hrc_ManagerReadCurrentNode(implHmgr);
    implNetwork = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, NULL);
    if (implNetwork == NIL(Ntk_Network_t)) {
      (void) fprintf(vis_stderr, "%s", error_string());
      (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
      goto cleanup;
    }
  }
  else {
    /* The option -1 has not been provided in the command line */
    goto usage;
  }
  /* At this point both networks have been built */

  /* Check that no node in the two network is multi-valued */
  if (CheckForMultiValueNode(specNetwork)) {
    fprintf(vis_stderr, "** res error: Specification has multivalued network\n");
    fprintf(vis_stderr, "** res error: Residue verification does not support multi-valued variables, variables have to be binary.\n");
    goto cleanup;
  }
  if (CheckForMultiValueNode(implNetwork)) {
    fprintf(vis_stderr, "** res error: Implementation has multivalued network\n");
    fprintf(vis_stderr, "** res error: Residue verification does not support multi-valued variables, variables have to be binary.\n");
    goto cleanup;
  }
  
  /* Check that both networks have the same number of inputs and outputs */
  if ((Ntk_NetworkReadNumCombInputs(implNetwork) != 
       Ntk_NetworkReadNumCombInputs(specNetwork)) ||
      (Ntk_NetworkReadNumCombOutputs(implNetwork) != 
       Ntk_NetworkReadNumCombOutputs(specNetwork))) {

    (void) fprintf(vis_stderr, "** res error: Networks do not have equal number of inputs ");
    (void) fprintf(vis_stderr, "or outputs\n");
    goto cleanup;
  } /* End of if */  

  /* Check if there has been some name matching file provided for outputs. */
  if (fileMatchOut != NIL(char)) {
    outputMatch = ReadMatchingPairs(fileMatchOut, implNetwork, specNetwork);
    if (outputMatch == NIL(st_table)) {
      (void) fprintf(vis_stderr, "** res error: Error reading Output match file ");
      (void) fprintf(vis_stderr, "%s\n", fileMatchOut);
      goto cleanup;
    } /* End of if */
  } /* End of if */

  /* Check if there has been some name matching file provided for inputs. */
  if (fileMatchIn != NIL(char)) {
    inputMatch = ReadMatchingPairs(fileMatchIn, implNetwork, specNetwork);
    if (inputMatch == NIL(st_table)) {
      (void) fprintf(vis_stderr, "** res error: Error reading Input match file ");
      (void) fprintf(vis_stderr, "%s\n", fileMatchIn);
      /* Clean up */
      goto cleanup;
    } /* End of if */
  } /* End of if */

  /* Transfer names of outputs starting with MSB from the file to an
   * array_t
   */
  if (fileOutputOrder != NIL(char)) {
    outputOrderArray = ReadOutputOrder(fileOutputOrder, specNetwork);
  } else if (defaultOutputOrder) {
    outputOrderArray = GenerateDefaultOutputOrder(specNetwork);
  }
    
  if (outputOrderArray == NIL(array_t)) {
    /* Clean up */
    fprintf(vis_stderr, "** res error: Output order(msb first) required for residue method.\n");
    goto usage;
  } else if  (array_n(outputOrderArray) != Ntk_NetworkReadNumCombOutputs(specNetwork)) {
    fprintf(vis_stderr, "** res error: Number of Outputs seem to be %d\n", Ntk_NetworkReadNumCombOutputs(specNetwork));
    fprintf(vis_stderr, "** res error: The output order seems to contain %d outputs\n", array_n(outputOrderArray));
    fprintf(vis_stderr, "** res error: Partial Orders or mismatch in the above two numbers is not allowed in the -o option\n");
    goto usage;
  }
  /* Start the timer before calling the verifyer */
  if (timeOutPeriod > 0) {
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);

    /* The second time setjmp is called, it returns here !!*/
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout, "Residue Verification timeout occurred after%d seconds.\n", 
                     timeOutPeriod);
      alarm(0);

      /* Note that there is a huge memory leak here. */
      goto cleanup;
    } /* End of if */
  }

  /* number of outputs to directly verify should be less than the
   * number of outputs for the circuit. If all flag set, number of
   * directly verified circuit, set it to number of combinational
   * outputs.
   */
  if (allFlag == 0) {
    outputsToVerifyDirectly = Ntk_NetworkReadNumCombOutputs(specNetwork);
  }
  if (outputsToVerifyDirectly > Ntk_NetworkReadNumCombOutputs(specNetwork)) {
    fprintf(vis_stderr, "** res error: More outputs to directly verify than that exist in the circuit\n");
    goto usage;
  }
    
  error_init();


  /* main procedure for residue verification */
  status = Res_NetworkResidueVerify(specNetwork,
                                    implNetwork,
                                    outputsToVerifyDirectly,
                                    outputOrderArray,
                                    outputMatch,
                                    inputMatch);
    
  /* Deactivate the alarm */
  alarm(0);
  
  /* If the computation succeded store the result in specNetwork */
  if (status == 0) {
    Res_ResidueInfo_t *residueInfo;

    residueInfo = (Res_ResidueInfo_t *) Ntk_NetworkReadApplInfo(specNetwork, 
                                                                RES_NETWORK_APPL_KEY);

    /* Print out the error string in case success is false */
    success = Res_ResidueInfoReadSuccess(residueInfo);
    switch (success) {
    case FALSE:
      (void) fprintf(vis_stdout, "Residue Verification failed !\n");
      break;
    case TRUE:
      (void) fprintf(vis_stdout, "Residue Verification successful\n");
      break;
    default:
      (void) fprintf(vis_stderr, "** res error: Residue Verification unable to produce ");
      (void) fprintf(vis_stderr, "result\n");
      break;
    }
  } else {
    (void) fprintf(vis_stderr, "%s", error_string());
  }

  /* Clean up */
  error_cleanup();
  goto cleanup;
  
    /* update with all functions */
usage:
  (void) fprintf(vis_stderr, "usage: res_verify [-b]  ");
  (void) fprintf(vis_stderr, "[-d n] [-h] -i impl file\n       ");
  (void) fprintf(vis_stderr, "[-m file] [-n file] -o file [-s spec file] ");
  (void) fprintf(vis_stderr, "[-t secs]\n");
  (void) fprintf(vis_stderr, "   -b        The file format to be read is ");
  (void) fprintf(vis_stderr, "blif-mv (default is blif)\n");
  (void) fprintf(vis_stderr, "   -d n      Number of outputs to verify ");
  (void) fprintf(vis_stderr, "directly\n");
  (void) fprintf(vis_stderr, "   -h        Print the usage of the command\n");
  (void) fprintf(vis_stderr, "   -i impl   Implementation file (required)\n");
  (void) fprintf(vis_stderr, "   -m file   File specifying the matching pair ");
  (void) fprintf(vis_stderr, "of names for the outputs\n");
  (void) fprintf(vis_stderr, "   -n file   File specifying the matching pair");
  (void) fprintf(vis_stderr, " of names for the inputs\n");
  (void) fprintf(vis_stderr, "   -o        Output order starting with MSB (required or -O required)\n");
  (void) fprintf(vis_stderr, "   -O        Default output order (required or -o required)\n");
  (void) fprintf(vis_stderr, "   -s file   Specification File\n");
  (void) fprintf(vis_stderr, "   -t secs   Seconds allowed for computation\n");

  
  /* Clean up */
cleanup:
  if ((specFileName == NIL(char)) && (specHmgr != NIL(Hrc_Manager_t))) {
    int zerorefcountbdds;
    bdd_manager *ddManager;
    Hrc_ManagerFree(specHmgr);
    if (specNetwork != NIL(Ntk_Network_t)) {
      ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
      if (ddManager != NIL(bdd_manager)) {
        zerorefcountbdds = bdd_check_zero_ref((bdd_manager *)Ntk_NetworkReadMddManager(specNetwork));
        if (zerorefcountbdds) {
          fprintf(vis_stdout, "Number of Nodes with non zero ref count are %d\n", zerorefcountbdds);
          fprintf(vis_stdout, "Size of DD manager = %d\n", bdd_num_vars(ddManager));
        }
      }
    }
    Ntk_NetworkFree(specNetwork);
  }
  if (implHmgr != NIL(Hrc_Manager_t)) {
    Hrc_ManagerFree(implHmgr);
    /* dont free manager if not set here */
    if ((specNetwork != NIL(Ntk_Network_t)) &&
        ((bdd_manager *)Ntk_NetworkReadMddManager(specNetwork) != NIL(bdd_manager))) {
      Ntk_NetworkSetMddManager(implNetwork, NIL(bdd_manager));
    }
    Ntk_NetworkFree(implNetwork);
  }
  if (outputMatch != NIL(st_table)) {
    st_foreach_item(outputMatch, stGen, &key, &value) {
      /* free only the key, cos the value appears as a key also */
      FREE(key);
    }
    st_free_table(outputMatch);
  } /* End of if */
  if (inputMatch != NIL(st_table)) {
    st_foreach_item(inputMatch, stGen, &key, &value) {
      /* free only the key, cos the value appears as a key also */
      FREE(key);
    }
    st_free_table(inputMatch);
  }
  if (outputOrderArray != NIL(array_t)) {
    char * name;
    arrayForEachItem(char *, outputOrderArray, i, name) {
      FREE(name);
    }
    array_free(outputOrderArray);
  }    
  return status;
}  /* End of CommandResVerify */


static void
TimeOutHandle(void)
{
  longjmp(timeOutEnv, 1);
} /* End of TimeOutHandle */

static st_table *
ReadMatchingPairs(char *fileName,
                  Ntk_Network_t *ntk1,
                  Ntk_Network_t *ntk2)
{
  st_table *result = NIL(st_table);
  int check;
  char name1[80], name2[80]; /* Note the size of buffer is used in fscanf */
  char *ptr1, *ptr2;
  FILE *fp;
#if HAVE_MKSTEMP && HAVE_CLOSE
  int  fd;
#else
  char buffer[512];
#endif
  char *realFileName, *blifMvFileName, *visDirectoryName;
  char command[512];
  int cmdStatus;
  
  fp = Cmd_FileOpen(fileName, "r", &realFileName, 1 /* silent */);
  
  if (fp == NIL(FILE)) {
    FREE(realFileName);
    (void) fprintf(vis_stderr, "** res error: Cannot open %s to read.\n", fileName);
    return result;
  } /* End of if */
  
  if (fp != stdin){
    (void)fclose(fp);
  }  

#if HAVE_MKSTEMP && HAVE_CLOSE
  blifMvFileName = util_strsav("/tmp/vis.XXXXXX");
  fd = mkstemp(blifMvFileName);
  if (fd == -1){
#else
  blifMvFileName = util_strsav(tmpnam(buffer));
  if (blifMvFileName == NIL(char)){
#endif
    FREE(realFileName);
    (void)fprintf(vis_stderr,"** res error: Could not create temporary file. ");
    (void)fprintf(vis_stderr,"** res error: Clean up /tmp an try again.\n");
    return NIL(st_table);
  }
#if HAVE_MKSTEMP && HAVE_CLOSE
  close(fd);
#endif
   /* Invoking an awk script */
  visDirectoryName = Vm_VisObtainLibrary();
  (void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| sed 's/(/<</g' | sed 's/)/>>/g' > %s", realFileName, blifMvFileName);
  /* the following is missing two new sed processings 
  (void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| %s -f %s/ioBlifToMv.nawk > %s", realFileName, NAWK, visDirectoryName, blifMvFileName);
  */
  cmdStatus = system(command);
  FREE(visDirectoryName);
  FREE(realFileName);
  if (cmdStatus != 0) {
    return NIL(st_table);
  }

  fp = Cmd_FileOpen(blifMvFileName, "r", NIL(char *), 1);
  assert(fp != NIL(FILE));


  result = st_init_table(st_ptrcmp, st_ptrhash);
  while (!feof(fp)) {
    check = fscanf(fp, "%80s %80s", name1, name2);
    if (check != 2 && check != EOF) {
      st_free_table(result);
      result = NIL(st_table);
      return result;
    } /* End of if */
    
    if (Ntk_NetworkFindNodeByName(ntk1, name1) == NIL(Ntk_Node_t) &&
        Ntk_NetworkFindNodeByName(ntk2, name1) == NIL(Ntk_Node_t)) {
      (void) fprintf(vis_stderr, "** res error: While reading matching file. ");
      (void) fprintf(vis_stderr, "** res error: Node %s not found in any of the networks.\n", 
                     name1);
      st_free_table(result);
      result = NIL(st_table);
      return result;
    }
    
    if (Ntk_NetworkFindNodeByName(ntk1, name2) == NIL(Ntk_Node_t) &&
        Ntk_NetworkFindNodeByName(ntk2, name2) == NIL(Ntk_Node_t)) {
      (void) fprintf(vis_stderr, "** res error: While reading matching file. ");
      (void) fprintf(vis_stderr, "** res error: Node %s not found in any of the networks.\n", 
                     name2);
      st_free_table(result);
      result = NIL(st_table);
      return result;
    }

    ptr1 = util_strsav(name1);
    ptr2 = util_strsav(name2);
    st_insert(result, ptr1, ptr2);
    st_insert(result, ptr2, ptr1);
  } /* End of while */
  
  fclose(fp);
#if HAVE_UNLINK
  unlink(blifMvFileName);
#endif
  FREE(blifMvFileName);

  return result;
} /* End of ReadMatchingPairs */

static array_t *
ReadOutputOrder(char *fileName,
                Ntk_Network_t *ntk1)
{
  FILE *fp;
#if HAVE_MKSTEMP && HAVE_CLOSE
  int  fd;
#else
  char buffer[512];
#endif
  array_t *result = NIL(array_t);
  int check;
  char name1[80]; /* Note the size of buffer is used in fscanf */
  char *ptr1;
  char *realFileName, *blifMvFileName, *visDirectoryName;
  char command[512];
  int cmdStatus;
  
  fp = Cmd_FileOpen(fileName, "r", &realFileName, 1 /* silent */);
  
  if (fp == NIL(FILE)) {
    FREE(realFileName);
    (void) fprintf(vis_stderr, "** res error: Cannot open %s to read.\n", fileName);
    return result;
  } /* End of if */

  if (fp != stdin){
    (void)fclose(fp);
  }  

#if HAVE_MKSTEMP && HAVE_CLOSE
  blifMvFileName = util_strsav("/tmp/vis.XXXXXX");
  fd = mkstemp(blifMvFileName);
  if (fd == -1){
#else
  blifMvFileName = util_strsav(tmpnam(buffer));
  if (blifMvFileName == NIL(char)){
#endif
    FREE(realFileName);
    (void)fprintf(vis_stderr,"** res error: Could not create temporary file. ");
    (void)fprintf(vis_stderr,"** res error: Clean up /tmp an try again.\n");
    return NIL(array_t);
  }
#if HAVE_MKSTEMP && HAVE_CLOSE
  close(fd);
#endif
  /* Invoking an awk script */
  visDirectoryName = Vm_VisObtainLibrary();
  (void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| sed 's/(/<</g' | sed 's/)/>>/g' > %s", realFileName, blifMvFileName);
  /* the following is missing two new sed processings 
  (void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| %s -f %s/ioBlifToMv.nawk > %s", realFileName, NAWK, visDirectoryName, blifMvFileName);
  */
  cmdStatus = system(command);
  FREE(visDirectoryName);
  FREE(realFileName);
  if (cmdStatus != 0) {
    return NIL(array_t);
  }

  fp = Cmd_FileOpen(blifMvFileName, "r", NIL(char *), 1);
  assert(fp != NIL(FILE));
  
  result = array_alloc(char *, 0);
  while (!feof(fp)) {
    check = fscanf(fp, "%80s", name1);
    if (check != EOF) {
      if (check != 1) {
        array_free(result);
        result = NIL(array_t);
        return result;
      } /* End of if */
      
      if (Ntk_NetworkFindNodeByName(ntk1, name1) == NIL(Ntk_Node_t)) {
        (void) fprintf(vis_stderr, "** res error: While reading output order file. ");
        (void) fprintf(vis_stderr, "** res error: Node %s not found in the network.\n", 
                       name1);
        array_free(result);
        result = NIL(array_t);
        return result;
      }
      ptr1 = util_strsav(name1);
      array_insert_last(char *, result, ptr1);
    }
  } /* End of while */
#ifdef DEBUG
  arrayForEachItem(char *,result, i, ptr1) {
    fprintf(vis_stdout, "%s\n", ptr1);
  }
#endif  

  fclose(fp);
#if HAVE_UNLINK
  unlink(blifMvFileName);
#endif
  FREE(blifMvFileName);

  return result;
} /* End of ReadMatchingPairs */


static array_t *
GenerateDefaultOutputOrder(Ntk_Network_t *specNetwork)
{
  array_t *outputOrderArray;
  lsGen listGen;
  Ntk_Node_t *nodePtr;
  char *name, *ptr1;
  int i;

  i = 0;
  outputOrderArray = array_alloc(char *,
                                 Ntk_NetworkReadNumCombOutputs(specNetwork));
  Ntk_NetworkForEachCombOutput(specNetwork, listGen, nodePtr) {
    name = Ntk_NodeReadName(nodePtr);
    ptr1 = util_strsav(name);
    array_insert(char *, outputOrderArray, i, ptr1);
    i++;
  }
  return outputOrderArray;
}

static int
CheckForMultiValueNode(Ntk_Network_t *network)
{
  lsGen listGen;
  Ntk_Node_t *nodePtr;
  Var_Variable_t * var;
  
  Ntk_NetworkForEachNode(network, listGen, nodePtr) {
    var = Ntk_NodeReadVariable(nodePtr);
    if ((Var_VariableReadNumValues(var) > 2) ||
        (!Var_VariableTestIsEnumerative(var))) {
      return 1;
    }
  }
  return 0;
}