/**CFile***********************************************************************

  FileName    [ioCheck.c]

  PackageName [io]

  Synopsis    [Routines to test if a blif-mv file is consistent.]

  Description [Routines to test if a blif-mv file is consistent. They are
  also responsible for setting several internal data structures. Here are
  the list of checks we can do on an hsis network. For each model, we first
  check if there is no node labeled both as PI and PS or both as PI and PO.
  Then, for each subcircuit in the model, the compatibllity of the interface
  is verified namewise and rangewise. This is detailed below. Then,
  we verify that there is no combinational cycle in any model.  Furthermore,
  for each latch in the model, we make sure that the input and the output
  of the latch are of the same type and that every latch has a reset table.  
  Finally, we check to see if each variable is an output of at
  most one table. As for the check to be done for a subcircuit, we first check
  if the model to be instantiated is present in the hmanager. Then, we 
  test if all the formal variables in the subcircuit definition exist
  in the model and at the same time they are of the same type of the
  corresponding actual variables. More thoroughly, we have to check
  if a flattened network has no cycle, but it is not currently implemented.]

  SeeAlso     []

  Author      [Yuji Kukimoto, Rajeev Ranjan, Huey-Yih Wang]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.

  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

******************************************************************************/

#include "ioInt.h"

static char rcsid[] UNUSED = "$Id: ioCheck.c,v 1.11 2005/04/16 06:17:45 fabio Exp $";

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


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


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


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


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


/**AutomaticStart*************************************************************/

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

static boolean _IoModelTestMasterNodeConsistency(Hrc_Model_t *model, Hrc_Node_t *hnode);
static boolean _IoModelTestConnectionConsistency(Hrc_Manager_t *hmgr, Hrc_Model_t *model, Hrc_Node_t *hnode, array_t *subcktArray);
static boolean _IoModelTestLatchConsistency(Hrc_Node_t *hnode);
static boolean _IoModelTestResetConsistency(Hrc_Manager_t *hmgr, Hrc_Model_t *model, Hrc_Node_t *hnode, array_t *resetArray);
static boolean _IoModelTestInternalConnectionConsistency(Hrc_Model_t *model, Hrc_Node_t *hnode, boolean isVerbose);
static boolean _IoModelTestIsAcyclic(Hrc_Model_t *model, Hrc_Node_t *hnode, st_table *varToTable, st_table *outputVarToSubckt, st_table *visitTable);
static void _IoModelTestIsAcyclicError(Hrc_Model_t *model, Var_Variable_t *var);
static int _IoModelTestIsAcyclicRecursive(Hrc_Model_t *model, Hrc_Node_t *hnode, Var_Variable_t *var, st_table *varToTable, st_table *outputVarToSubckt, st_table *visitTable, boolean isResetLogic);

/**AutomaticEnd***************************************************************/


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


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

/**Function********************************************************************

  Synopsis    [Checks to see if a given blif-mv network is consistent.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
boolean
IoNetworkTestConsistency(
  Hrc_Manager_t *hmgr, 
  array_t *modelArray,
  st_table *parserSubcktInfo,
  st_table *parserResetInfo,
  boolean isVerbose)
{
  char *subcktArray, *resetArray;
  Hrc_Model_t *model;
  Hrc_Node_t *hnode;
  int i;

  for (i=0; i < array_n(modelArray); i++){
    model = array_fetch(Hrc_Model_t *,modelArray,i);

    hnode = Hrc_ModelReadMasterNode(model);

    if (_IoModelTestMasterNodeConsistency(model,hnode) == 0){
      return 0;
    }
    /* the following st_lookup should return 1 */
    (void)st_lookup(parserSubcktInfo,(char *)model,&subcktArray);
    if ((array_t *)subcktArray != NIL(array_t)){
      if (_IoModelTestConnectionConsistency(hmgr,model,hnode,(array_t *)subcktArray) == 0){
        return 0;
      }
    }
    /* the following st_lookup should return 1 */
    (void)st_lookup(parserResetInfo,(char *)model,&resetArray);
    if ((array_t *)resetArray != NIL(array_t)){
      if (_IoModelTestResetConsistency(hmgr,model,hnode,(array_t *)resetArray) == 0){
        return 0;
      }
    }
    if (_IoModelTestLatchConsistency(hnode) == 0){
      return 0;
    }
    if (_IoModelTestInternalConnectionConsistency(model,hnode,isVerbose) == 0){
      return 0;
    }
  }
  return 1;
}

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

/**Function********************************************************************

  Synopsis    [Checks to see if there is no inconsistency in a model.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static boolean
_IoModelTestMasterNodeConsistency(
  Hrc_Model_t *model,
  Hrc_Node_t *hnode)
{
  char *varName;
  Var_Variable_t *var;
  st_generator *gen;

  Hrc_NodeForEachVariable(hnode,gen,varName,var){
    if (Var_VariableTestTypeConsistency(var) == 0){
      st_free_gen(gen);
      return 0;
    }
  }
  return 1;
}

/**Function********************************************************************

  Synopsis    [Checks to see if there is no inconsistency in subcircuit connections.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static boolean
_IoModelTestConnectionConsistency(
  Hrc_Manager_t *hmgr, 
  Hrc_Model_t *model, 
  Hrc_Node_t *hnode, 
  array_t *subcktArray)
{
  int i, j;
  IoSubckt_t *subckt;
  char *nameOfSubcktModel, *instanceName, *formalName, *actualName, *actualPort;
  Hrc_Model_t *subcktModel;
  Hrc_Node_t *subcktHnode;
  st_table *tmpTable;
  st_table *outputCheckTable;
  array_t *formalNameArray, *actualNameArray, *actualInputArray, *actualOutputArray;
  Var_Variable_t *port, *var;

  for (i=0; i < array_n(subcktArray); i++){
    subckt = array_fetch(IoSubckt_t *,subcktArray,i);
    nameOfSubcktModel = subckt->modelName;
    if ((subcktModel = Hrc_ManagerFindModelByName(hmgr,nameOfSubcktModel)) == NIL(Hrc_Model_t)){
      error_append("Error: Model ");
      error_append(Hrc_ModelReadName(model));
      error_append(" has a subcircuit whose model ");
      error_append(nameOfSubcktModel);
      error_append(" is not defined.\n");
      return 0;
    }

    subcktHnode = Hrc_ModelReadMasterNode(subcktModel);
    instanceName = subckt->instanceName;
    formalNameArray = subckt->formalNameArray;
    actualNameArray = subckt->actualNameArray;
    assert(array_n(formalNameArray) == array_n(actualNameArray));

    if (array_n(formalNameArray) != 
        Hrc_NodeReadNumFormalInputs(subcktHnode) + Hrc_NodeReadNumFormalOutputs(subcktHnode)){
      error_append("Error: Subcircuit ");
      error_append(instanceName);
      error_append(" in model ");
      error_append(Hrc_ModelReadName(model));
      error_append(" and the corresponding model ");
      error_append(nameOfSubcktModel);
      error_append(" have different number of i/o ports.\n");
      return 0;
    }

    /* creating a temporary hash table from formal names to actual names */
    tmpTable = st_init_table(strcmp,st_strhash);
    for (j=0; j < array_n(formalNameArray); j++){
      formalName = array_fetch(char *,formalNameArray,j);
      actualName = array_fetch(char *,actualNameArray,j);
      if (st_insert(tmpTable,(char *)formalName,(char *)actualName)){
        error_append("Error: In subcircuit ");
        error_append(instanceName);
        error_append(" in model ");
        error_append(Hrc_ModelReadName(model));
        error_append(", formal variable ");
        error_append(formalName);
        error_append(" is used more than once.\n");
        st_free_table(tmpTable);
        return 0;
      }
    }

    /* create actualInputArray */
    actualInputArray = array_alloc(Var_Variable_t *,0);
    actualOutputArray = array_alloc(Var_Variable_t *,0);
    Hrc_NodeForEachFormalInput(subcktHnode,j,port){
      if (st_lookup(tmpTable,(char *)Var_VariableReadName(port),&actualPort) == 0){
        error_append("Error: Subcircuit ");
        error_append(instanceName);
        error_append(" in model ");
        error_append(Hrc_ModelReadName(model));
        error_append(" has no actual variable defined for variable ");
        error_append(Var_VariableReadName(port));
        error_append(".\n");
        return 0;
      }
      /* var should get a non-nil pointer */
      var = Hrc_NodeFindVariableByName(hnode,actualPort);
      if (Var_VariablesTestHaveSameDomain(var,port) == 0){
        error_append("Error: Formal variable ");
        error_append(Var_VariableReadName(port));
        error_append(" and actual variable ");
        error_append(actualPort);
        error_append(" have different types in subcircuit ");
        error_append(instanceName);
        error_append(" in model ");
        error_append(Hrc_ModelReadName(model));
        error_append(".\n");
        return 0;
      }
      if (Var_VariableSetSI(var) == -1){
        return 0;
      };
      array_insert_last(Var_Variable_t *,actualInputArray,var); 
    }

    /* create actualOutputArray */
    outputCheckTable = st_init_table(strcmp,st_strhash);
    Hrc_NodeForEachFormalOutput(subcktHnode,j,port){

      if (st_lookup(tmpTable,(char *)Var_VariableReadName(port),&actualPort) == 0){
        error_append("Error: Subcircuit ");
        error_append(instanceName);
        error_append(" in model ");
        error_append(Hrc_ModelReadName(model));
        error_append(" has no actual variable defined for variable ");
        error_append(Var_VariableReadName(port));
        error_append(".\n");
        return 0;
      }
      if (st_is_member(outputCheckTable,actualPort) == 1){
        error_append("Error: Subcircuit ");
        error_append(instanceName);
        error_append(" in model ");
        error_append(Hrc_ModelReadName(model));
        error_append(" has more than one output connected to the same variable ");
        error_append(actualPort);
        error_append(".\n");
        return 0;
      }
      (void)st_insert(outputCheckTable,actualPort,(char *)0);
      /* var should get a non-nil pointer */
      var = Hrc_NodeFindVariableByName(hnode,actualPort);
      if (Var_VariablesTestHaveSameDomain(var,port) == 0){
        error_append("Error: Formal variable ");
        error_append(Var_VariableReadName(port));
        error_append(" and actual variable ");
        error_append(actualPort);
        error_append(" have different types in subcircuit ");
        error_append(instanceName);
        error_append(" in model ");
        error_append(Hrc_ModelReadName(model));
        error_append(".\n");
        return 0;
      }
      if (Var_VariableSetSO(var) == -1){
        return 0;
      };
      array_insert_last(Var_Variable_t *,actualOutputArray,var); 
    }
    st_free_table(outputCheckTable);
    st_free_table(tmpTable);
    if (Hrc_ModelAddSubckt(model,subcktModel,instanceName,actualInputArray,actualOutputArray) == 0){
      error_append("Error: Model ");
      error_append(Hrc_ModelReadName(model));
      error_append(" has two subcircuits with the same instance name ");
      error_append(instanceName);
      error_append("\n");
      return 0;
    }
  }
  return 1;
}


/**Function********************************************************************

  Synopsis    [Checks to see if there is no inconsistency in a latch definition.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static boolean
_IoModelTestLatchConsistency(Hrc_Node_t *hnode)
{
  Hrc_Latch_t *latch;
  Var_Variable_t *varIn, *varOut;
  st_generator *gen;
  char *latchName;

  Hrc_NodeForEachLatch(hnode,gen,latchName,latch){
    varIn = Hrc_LatchReadInput(latch);
    varOut = Hrc_LatchReadOutput(latch);
    if (Var_VariablesTestHaveSameDomain(varIn,varOut) == 0){
      error_append("Error: The input and the output of latch ");
      error_append(latchName);
      error_append(" have different domains.\n"); 
      return 0; 
    }
    if (Hrc_LatchReadResetTable(latch) == NIL(Tbl_Table_t)){
      error_append("Error: Latch ");
      error_append(Var_VariableReadName(varOut));
      error_append(" has no reset table.\n");
      return 0;
    }
  }
  return 1;
}

/**Function********************************************************************

  Synopsis    [Checks to see if there is no inconsistency in reset declarations.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

static boolean
_IoModelTestResetConsistency(
  Hrc_Manager_t *hmgr,
  Hrc_Model_t *model,
  Hrc_Node_t *hnode,
  array_t *resetArray)
{
  int i;
  Var_Variable_t *output;
  Tbl_Table_t *resetTable;
  Hrc_Latch_t *latch;

  for (i=0; i < array_n(resetArray); i++){
    resetTable = array_fetch(Tbl_Table_t *,resetArray,i);
    if (Tbl_TableReadNumOutputs(resetTable) != 1){
      error_append("Error: Reset table with output ");
      error_append(Var_VariableReadName(Tbl_TableReadIndexVar(resetTable,0,1)));
      error_append(" has to be a single output table.\n");
      return 0;
    }
    output = Tbl_TableReadIndexVar(resetTable,0,1);
    if (Var_VariableTestIsPS(output) == 0){
      error_append("Error: Reset table with output ");
      error_append(Var_VariableReadName(output));
      error_append(" is not attached to a latch.\n");
      return 0;
    }
    latch = Hrc_NodeFindLatchByName(hnode,Var_VariableReadName(output));
    if (Hrc_LatchSetResetTable(latch,resetTable) == 0){
      error_append("Error: You try to overwrite the reset table of ");
      error_append(Var_VariableReadName(output));
      error_append(".\n");
      return 0;
    }
    /* once a reset table is associated with a latch,
    we remove the table from resetArray */
    array_insert(Tbl_Table_t *,resetArray,i,NIL(Tbl_Table_t));
  }
  return 1;
}


/**Function********************************************************************

  Synopsis    [Checks the consistency of the internal connection of a model.]

  Description [Checks the consistency of the internal connection of a model.
  Returns 1 if success. Otherwise returns 0.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static boolean
_IoModelTestInternalConnectionConsistency(
  Hrc_Model_t *model,
  Hrc_Node_t *hnode,
  boolean isVerbose)
{
  st_table *varToTable, *outputVarToSubckt, *inputVarToSubckt, *visitTable;
  st_generator *gen;
  int i, j, status, warningStatus;
  Var_Variable_t *var, *actualOutput;
  Tbl_Table_t *table;
  char *varName, *subcktName, *latchName;
  Hrc_Subckt_t *subckt, *anotherSubckt;
  Hrc_Latch_t *latch;
  
  /* creates a hash table from variables to tables */ 
  varToTable = st_init_table(st_ptrcmp,st_ptrhash);
  Hrc_NodeForEachNameTable(hnode,i,table){
    Tbl_TableForEachOutputVar(table,j,var){
      if (Var_VariableTestIsPI(var) == 1){
        error_append("Error: Primary input ");
        error_append(Var_VariableReadName(var));
        error_append(" is an output of a table in model ");
        error_append(Hrc_ModelReadName(model));
        error_append(".\n");
        st_free_table(varToTable);
        return 0; 
      }
      if (st_insert(varToTable,(char *)var,(char *)table) == 1){
        error_append("Error: Variable ");
        error_append(Var_VariableReadName(var));
        error_append(" is an output of more than one table in model ");
        error_append(Hrc_ModelReadName(model));
        error_append(".\n");
        st_free_table(varToTable);
        return 0;
      }
    }
  }
  Hrc_NodeForEachLatch(hnode,gen,latchName,latch){
    if (st_insert(varToTable,(char *)Hrc_LatchReadOutput(latch),(char *)Hrc_LatchReadResetTable(latch)) == 1){
      error_append("Error: Latch output ");
      error_append(Var_VariableReadName(Hrc_LatchReadOutput(latch)));
      error_append(" is an output of a table in model ");
      error_append(Hrc_ModelReadName(model));
      error_append(".\n");
      st_free_table(varToTable);
      return 0;
    }
  }

  /* creates two hash tables
     one from output variables of subckts to subckts
     the other one from input variables of subckts to subckts */
  outputVarToSubckt = st_init_table(st_ptrcmp,st_ptrhash);
  inputVarToSubckt = st_init_table(st_ptrcmp,st_ptrhash);

  Hrc_ModelForEachSubckt(model,gen,subcktName,subckt){
    array_t *actualOutputs = Hrc_SubcktReadActualOutputVars(subckt);
    array_t *actualInputs = Hrc_SubcktReadActualInputVars(subckt);

    for (i=0; i < array_n(actualOutputs); i++){
      actualOutput = array_fetch(Var_Variable_t *,actualOutputs,i);
      if (st_lookup(varToTable,(char *)actualOutput,&table) == 1){
        error_append("Error: Subckt output ");
        error_append(Var_VariableReadName(actualOutput));
        error_append(" in ");
        error_append(subcktName);
        error_append(" is an output of a table in model ");
        error_append(Hrc_ModelReadName(model));
        error_append(".\n");
        st_free_table(varToTable);
        st_free_table(outputVarToSubckt);
        st_free_gen(gen);
        return 0;
      }
      if (st_lookup(outputVarToSubckt,(char *)actualOutput,&anotherSubckt) == 1){
        error_append("Error: Subckt output ");
        error_append(Var_VariableReadName(actualOutput));
        error_append(" in ");
        error_append(subcktName);
        error_append(" is also a subckt output of ");
        error_append(Hrc_SubcktReadInstanceName(anotherSubckt));
        error_append(" in model ");
        error_append(Hrc_ModelReadName(model));
        error_append(".\n");
        st_free_table(varToTable);
        st_free_table(outputVarToSubckt);
        st_free_gen(gen);
        return 0;
      }
      (void)st_insert(outputVarToSubckt,(char *)actualOutput,(char *)subckt);
    }
    
    for (i=0; i < array_n(actualInputs); i++){
      Var_Variable_t *actualInput = array_fetch(Var_Variable_t *,actualInputs,i);
      (void)st_insert(inputVarToSubckt,(char *)actualInput,(char *)subckt);
    }

  }

  /* start checking the consistency of a hnode */
  Hrc_NodeForEachVariable(hnode,gen,varName,var) {
    if (st_lookup(varToTable,(char *)var,&table) == 0){
      if (Var_VariableTestIsPS(var) == 1 || Var_VariableTestIsPI(var) == 1){
        continue;
      }
      else {
       if (st_lookup(outputVarToSubckt,(char *)var,&subckt) == 0) { 
         error_append("Error: Variable "); 
         error_append(varName); 
         error_append(" is not defined as an output of a table in model "); 
         error_append(Hrc_ModelReadName(model)); 
         error_append(".\n"); 
         st_free_table(varToTable); 
         st_free_gen(gen); 
         return 0; 
       }
    }
    }
  }

  
  /* compute numFanoutTables */
  Hrc_NodeForEachNameTable(hnode,i,table){
    Tbl_TableForEachInputVar(table,j,var){
      Var_VariableIncrementNumFanoutTables(var);
    }
  }

  /* acyclic check */
  visitTable = st_init_table(st_ptrcmp,st_ptrhash);
  status = _IoModelTestIsAcyclic(model,hnode,varToTable,outputVarToSubckt,visitTable);
  warningStatus = 0;
  if (status == 1){
  /* as a by-product of the acyclic check, visitTable now contains
  all the variables reachable from either PO, NS, or reset tables.
  We use this to detect all the variables not used in the hnode */
    Hrc_NodeForEachVariable(hnode,gen,varName,var){
      if (st_is_member(visitTable,(char *)var) == 0 && 
          st_is_member(inputVarToSubckt,(char *)var) == 0 &&
          Var_VariableTestIsPO(var) == 0 &&
          Var_VariableTestIsNS(var) == 0 &&
          Var_VariableTestIsPS(var) == 0 ){
        warningStatus = 1;
        if (isVerbose){
          /* the following is just a warning. We do not return a failure status */
          error_append("Warning: Variable ");
          error_append(Var_VariableReadName(var));
          error_append(" is not used in ");
          error_append(Hrc_ModelReadName(model));
          error_append(".\n");
        }
      }
    }
  }
  if (isVerbose == 0 && warningStatus == 1){
    error_append("Warning: Some variables are unused in model ");
    error_append(Hrc_ModelReadName(model));
    error_append(".\n");
  }
  st_free_table(varToTable);
  st_free_table(outputVarToSubckt);
  st_free_table(inputVarToSubckt);
  st_free_table(visitTable);

  return 1;
}


/**Function********************************************************************

  Synopsis    [A DFS-based procedure for checking acyclicity.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static boolean
_IoModelTestIsAcyclic(
  Hrc_Model_t *model,
  Hrc_Node_t *hnode,
  st_table *varToTable,
  st_table *outputVarToSubckt,
  st_table *visitTable)
{
  int i;
  Var_Variable_t *var;
  st_generator *gen;
  char *latchName;
  Hrc_Latch_t *latch;

  Hrc_NodeForEachFormalOutput(hnode,i,var){
    if (_IoModelTestIsAcyclicRecursive(model,hnode,var,varToTable,outputVarToSubckt,visitTable,0) == 0){
      _IoModelTestIsAcyclicError(model,var);
      return 0;
    }
  }
  Hrc_NodeForEachLatch(hnode,gen,latchName,latch){
    Tbl_Table_t *resetTable;

    resetTable = Hrc_LatchReadResetTable(latch);
    Tbl_TableForEachInputVar(resetTable,i,var){
      int status;
      if ((status = _IoModelTestIsAcyclicRecursive(model,hnode,
          var,varToTable,outputVarToSubckt,visitTable,1)) == 0){
        _IoModelTestIsAcyclicError(model,var);
        st_free_gen(gen);
        return 0;
      }
      /* found a path from a PS to a reset table */
      if (status == -1){
        error_append(latchName);
        error_append(" in model ");
        error_append(Hrc_ModelReadName(model));
        error_append(".\n");
        st_free_gen(gen);
        return 0;
      }
    } 
  }
  Hrc_NodeForEachLatch(hnode,gen,latchName,latch){
    if (_IoModelTestIsAcyclicRecursive(model,hnode,
        (var = Hrc_LatchReadInput(latch)),varToTable,outputVarToSubckt,visitTable,0) == 0){
      _IoModelTestIsAcyclicError(model,var);
      st_free_gen(gen);
      return 0;
    } 
  }
  return 1;
}

/**Function********************************************************************

  Synopsis    [Prints out error messages during an acyclic check.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
_IoModelTestIsAcyclicError(
  Hrc_Model_t *model,
  Var_Variable_t *var)
{
  error_append("Warning: Model ");
  error_append(Hrc_ModelReadName(model));
  error_append(" may have a cyclic connection which involves variable ");
  error_append(Var_VariableReadName(var));
  error_append("\n");
}

/**Function********************************************************************

  Synopsis    [Recursive DFS routine for acyclic check.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
_IoModelTestIsAcyclicRecursive(
  Hrc_Model_t *model,
  Hrc_Node_t *hnode,
  Var_Variable_t *var,
  st_table *varToTable,
  st_table *outputVarToSubckt,
  st_table *visitTable,
  boolean isResetLogic)
{
  int val, i;
  Var_Variable_t *input;
  Tbl_Table_t *table;
  Hrc_Subckt_t *subckt;

  if (st_lookup_int(visitTable,(char *)var, &val) == 1){
    return (!val);
  }
  else{
    (void)st_insert(visitTable,(char *)var,(char *)1);
    
    if (Var_VariableTestIsPI(var) == 0 &&
           (isResetLogic || Var_VariableTestIsPS(var) == 0)){
      if (isResetLogic && (Var_VariableTestIsPS(var) == 1)){
        error_append("Warning: There is a path from latch output ");
        error_append(Var_VariableReadName(var));
        error_append(" to reset table ");

        /* the error message is to be continued in _IoModelTestIsAcyclic() */
        return -1;  
      }
      if (st_lookup(varToTable,(char *)var,&table) == 1){
        Tbl_TableForEachInputVar(table,i,input){
          int status;
          if ((status = _IoModelTestIsAcyclicRecursive(model,hnode,input,
                           varToTable,outputVarToSubckt,visitTable,isResetLogic)) == 0){
            return 0;
          }
          if (status == -1){
            return -1;
          }
        }
      }
      else {
        array_t *actualInputs;
        /* the return value of the following st_lookup should be 1 */
        (void)st_lookup(outputVarToSubckt,(char *)var,&subckt);
        actualInputs = Hrc_SubcktReadActualInputVars(subckt);
        assert (actualInputs != NIL(array_t));
        for (i=0; i < array_n(actualInputs); i++){
          int status;
          input = array_fetch(Var_Variable_t *,actualInputs,i);
          if ((status = _IoModelTestIsAcyclicRecursive(model,hnode,input,
                         varToTable,outputVarToSubckt,visitTable,0)) == 0){
            return 0;
          }
          if (status == -1){
            return -1;
          }
        }
      }
    }
    (void)st_insert(visitTable,(char *)var,(char *)0);
    return 1;
  }
}