src/hrc/hrcInOut.c

Go to the documentation of this file.

#include "hrcInt.h"
#include "io.h"

static char rcsid[] UNUSED = "$Id: hrcInOut.c,v 1.6 2005/04/28 14:16:09 fabio Exp $";

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


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


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


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


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


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


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/
boolean
Hrc_NodeAddApplInfo(
  Hrc_Node_t *node,
  char * key,
  Hrc_ApplInfoFreeFn  freeFn,
  Hrc_ApplInfoChangeFn changeFn,
  void * data)
{
  ApplInfo_t *applInfo;
  boolean status;
  
  if (st_lookup(node->applInfoTable, key, &applInfo)) {
    (*applInfo->freeFn)(applInfo->data);
    status = TRUE;
  }
  else {
    char       *keyCopy  = util_strsav(key);

    applInfo = ALLOC(ApplInfo_t, 1);
    st_insert(node->applInfoTable, keyCopy, applInfo);
    status = FALSE;
  }
  applInfo->freeFn = freeFn;
  applInfo->changeFn = changeFn;
  applInfo->data   = data;
  return status;
}


void *
Hrc_NodeReadApplInfo(
  Hrc_Node_t *node,
  char * key)
{
  int         status;
  ApplInfo_t *applInfo;
  
  status = st_lookup(node->applInfoTable, key, &applInfo);
  if (status == 1) {
    return (applInfo->data);
  }
  else {
    return (NIL(void));
  }
}


boolean
Hrc_NodeFreeApplInfo(
  Hrc_Node_t *node,
  char * key)
{
  int         status;
  ApplInfo_t *applInfo;
  
  status = st_lookup(node->applInfoTable, key, &applInfo);

  if (status == 1) {
    st_delete(node->applInfoTable, &key, &applInfo);
    (*applInfo->freeFn)(applInfo->data);
    FREE(key);  /* frees the string contained in the table */
    FREE(applInfo);
  }

  return ((status) ? TRUE : FALSE);
}

void
Hrc_ModelWriteBlifMv(
  FILE *fp,
  Hrc_Model_t *model,
  boolean isRootModel,
  char *rootInstanceName)
{
  Hrc_Node_t *hnode, *subcktHnode;
  Hrc_Model_t *subcktModel;
  int i, is_enum, range;
  Var_Variable_t *var, *actualVar;
  Hrc_Latch_t *latch;
  Hrc_Subckt_t *subckt;
  Tbl_Table_t *table;
  char *varName, *latchName, *instanceName;
  st_generator *gen;
  array_t *subcktActualInputVars, *subcktActualOutputVars;

  (void)fprintf(fp,".model %s\n",Hrc_ModelReadName(model));
  if (isRootModel){
    (void)fprintf(fp,".root %s\n",rootInstanceName);
  }
  hnode = Hrc_ModelReadMasterNode(model);

  /* .inputs */
  if (Hrc_NodeReadNumFormalInputs(hnode) != 0){
    (void)fprintf(fp,".inputs ");
    Hrc_NodeForEachFormalInput(hnode,i,var){
      (void)fprintf(fp,"%s ",Var_VariableReadName(var));
    }
    (void)fprintf(fp,"\n");
  }

  /* .outputs */
  if (Hrc_NodeReadNumFormalOutputs(hnode) != 0){
    (void)fprintf(fp,".outputs ");
    Hrc_NodeForEachFormalOutput(hnode,i,var){
      (void)fprintf(fp,"%s ",Var_VariableReadName(var));
    }
    (void)fprintf(fp,"\n");
  }

  /* .mv */
  Hrc_NodeForEachVariable(hnode,gen,varName,var){
    is_enum = Var_VariableTestIsEnumerative(var);
    range = Var_VariableReadNumValues(var);
    
    if (is_enum == 1){
      if (range == 2){
        /* Boolean enumerative variables need no .mv declaration. */
        continue;
      }
      else {
        (void)fprintf(fp,".mv %s %d\n",Var_VariableReadName(var),range);
      }
    }
    else {
      /* variable var is symbolic */
      (void)fprintf(fp,".mv %s %d ",Var_VariableReadName(var),range);
      for (i=0; i < range; i++){
        (void)fprintf(fp,"%s ",Var_VariableReadSymbolicValueFromIndex(var,i));
      }
      (void)fprintf(fp,"\n");
    }
  }

  /* .latches */
  Hrc_NodeForEachLatch(hnode,gen,latchName,latch){
    (void)fprintf(fp,".latch %s %s\n",
       Var_VariableReadName(Hrc_LatchReadInput(latch)),
       Var_VariableReadName(Hrc_LatchReadOutput(latch)));
    Tbl_TableWriteBlifMvToFile(Hrc_LatchReadResetTable(latch),1,fp);
  }

  /* .subckt */
  Hrc_ModelForEachSubckt(model,gen,instanceName,subckt){
    subcktModel = Hrc_SubcktReadModel(subckt);
    subcktHnode = Hrc_ModelReadMasterNode(subcktModel);
    subcktActualInputVars = Hrc_SubcktReadActualInputVars(subckt);
    subcktActualOutputVars = Hrc_SubcktReadActualOutputVars(subckt);

    (void)fprintf(fp,".subckt %s %s ",
       Hrc_ModelReadName(subcktModel), Hrc_SubcktReadInstanceName(subckt));
    Hrc_NodeForEachFormalInput(subcktHnode,i,var){
      actualVar = array_fetch(Var_Variable_t *,subcktActualInputVars,i);
      (void)fprintf(fp,"%s = %s ",Var_VariableReadName(var),Var_VariableReadName(actualVar)); 
    }   
    Hrc_NodeForEachFormalOutput(subcktHnode,i,var){
      actualVar = array_fetch(Var_Variable_t *,subcktActualOutputVars,i);
      (void)fprintf(fp,"%s = %s ",Var_VariableReadName(var),Var_VariableReadName(actualVar)); 
    }   
    (void)fprintf(fp,"\n");
  }

  /* .names */
  Hrc_NodeForEachNameTable(hnode,i,table){
    Tbl_TableWriteBlifMvToFile(table,0,fp);
  }

  (void)fprintf(fp,".end\n");
}


void
Hrc_ModelWriteSmv(
  FILE *fp,
  Hrc_Model_t *model,
  boolean isRootModel,
  char *rootInstanceName)
{
  Hrc_Node_t *hnode, *subcktHnode;
  Hrc_Model_t *subcktModel;
  int i, is_enum, range;
  Var_Variable_t *var, *actualVar;
  Hrc_Latch_t *latch;
  Hrc_Subckt_t *subckt;
  Tbl_Table_t *table;
  char *varName, *latchName, *instanceName;
  st_generator *gen;
  array_t *subcktActualInputVars, *subcktActualOutputVars;

  hnode = Hrc_ModelReadMasterNode(model);
  
  if (isRootModel){
    (void)fprintf(fp,"\n\nMODULE main --(");
    if (Hrc_NodeReadNumFormalInputs(hnode) != 0){
      fprintf(stderr, 
              "Warning: ignored %d input parameter(s) in the main module (root model)\n", 
              Hrc_NodeReadNumFormalInputs(hnode));
    }
    if (Hrc_NodeReadNumFormalOutputs(hnode) != 0){
      fprintf(stderr, 
              "Warning: ignored %d output parameter(s) in the main module (root model)\n", 
              Hrc_NodeReadNumFormalOutputs(hnode));
    }
  } else {
    (void)fprintf(fp,"\n\nMODULE %s (",Hrc_ModelReadName(model));
  }

  /* Input parameters */
  if (Hrc_NodeReadNumFormalInputs(hnode) != 0){
    Hrc_NodeForEachFormalInput(hnode,i,var){
      Io_SmvPrintVar(fp, var);
      if(i < Hrc_NodeReadNumFormalInputs(hnode)-1 ||
         Hrc_NodeReadNumFormalOutputs(hnode) > 0) {
        (void)fprintf(fp,", ");
      }
    }
  }
  /* Output parameters */
  if (Hrc_NodeReadNumFormalOutputs(hnode) != 0){
    Hrc_NodeForEachFormalOutput(hnode,i,var){
      Io_SmvPrintVar(fp, var);
      if(i < Hrc_NodeReadNumFormalOutputs(hnode)-1) {
        (void)fprintf(fp,", ");
      }
    }
  }
  (void)fprintf(fp,")\n");

  /* Variables */
  Hrc_NodeForEachVariable(hnode,gen,varName,var){
    if (!isRootModel && (Var_VariableTestIsPI(var) || Var_VariableTestIsPO(var))) {
      fprintf(fp,"-- PI or PO: ");
    }

    is_enum = Var_VariableTestIsEnumerative(var);
    range = Var_VariableReadNumValues(var);
    
    (void)fprintf(fp,"VAR ");
    Io_SmvPrintVar(fp, var);
    if (is_enum == 1){
      if (range == 2){
        (void)fprintf(fp," : boolean;\n");
      }
      else {
        (void)fprintf(fp," : 0..%d;\n",range-1);
      }
    }
    else {
      /* variable var is symbolic */
      (void)fprintf(fp," : {");
      for (i=0; i < range; i++){
        (void)fprintf(fp,"%s",Var_VariableReadSymbolicValueFromIndex(var,i));
        if(i < range-1)
          (void)fprintf(fp, ", ");
      }
      (void)fprintf(fp,"};\n");
    }
  }

  /* Subcircuits */
  Hrc_ModelForEachSubckt(model,gen,instanceName,subckt){
    subcktModel = Hrc_SubcktReadModel(subckt);
    subcktHnode = Hrc_ModelReadMasterNode(subcktModel);
    subcktActualInputVars = Hrc_SubcktReadActualInputVars(subckt);
    subcktActualOutputVars = Hrc_SubcktReadActualOutputVars(subckt);

    /* Note: mv uses named parameters; we do not check that there are
       enough parameters or that they occur in the correct order. This
       doesn't seem to matter at the moment. */
    (void)fprintf(fp,"VAR %s : %s(",
       Hrc_SubcktReadInstanceName(subckt), Hrc_ModelReadName(subcktModel));
    Hrc_NodeForEachFormalInput(subcktHnode,i,var){
      actualVar = array_fetch(Var_Variable_t *,subcktActualInputVars,i);
      Io_SmvPrintVar(fp, actualVar);
      if(i < Hrc_NodeReadNumFormalInputs(subcktHnode)-1 ||
         Hrc_NodeReadNumFormalOutputs(subcktHnode) > 0) {
        (void)fprintf(fp,", ");
      }
    }   
    Hrc_NodeForEachFormalOutput(subcktHnode,i,var){
      actualVar = array_fetch(Var_Variable_t *,subcktActualOutputVars,i);
      Io_SmvPrintVar(fp, actualVar);
      if(i < Hrc_NodeReadNumFormalOutputs(subcktHnode)-1) {
        (void)fprintf(fp,", ");
      }
    }   
    (void)fprintf(fp,");\n");
  }

  /* .latches */
  (void)fprintf(fp,"\nASSIGN\n");
  Hrc_NodeForEachLatch(hnode,gen,latchName,latch){
    (void)fprintf(fp,"next(");
    Io_SmvPrintVar(fp, Hrc_LatchReadOutput(latch));
    (void)fprintf(fp,") := ");
    Io_SmvPrintVar(fp, Hrc_LatchReadInput(latch));
    (void)fprintf(fp,";\ninit(");
    Io_SmvPrintVar(fp, Hrc_LatchReadOutput(latch));
    (void)fprintf(fp,") := ");
    Tbl_TableWriteSmvToFile(Hrc_LatchReadResetTable(latch),1,fp);
    (void)fprintf(fp,"\n");
  }

  /* .names */
  Hrc_NodeForEachNameTable(hnode,i,table){
    Tbl_TableWriteSmvToFile(table,0,fp);
  }

}

Hrc_Node_t *
Hrc_ManagerReadRootNode(
  Hrc_Manager_t *manager)
{
  return manager->rootNode;
}

Hrc_Node_t *
Hrc_ManagerReadCurrentNode(
  Hrc_Manager_t *manager)
{
  return manager->currentNode;
}

st_table *
Hrc_ManagerReadModelTable(
  Hrc_Manager_t *manager)
{
  return manager->modelTable;
}

Hrc_Model_t *
Hrc_ManagerFindModelByName(
  Hrc_Manager_t *manager,
  char *modelName)
{
  Hrc_Model_t *model;
    
  if(st_lookup(manager->modelTable, modelName, &model)) {
    return model;
  }
  else {
    return NIL(Hrc_Model_t);
  }
}

Hrc_Node_t *
Hrc_ModelReadMasterNode(
  Hrc_Model_t *model)
{
  return model->masterNode;
}

char *
Hrc_ModelReadName(
  Hrc_Model_t *model)
{
  return model->modelName;
}

st_table *
Hrc_ModelReadSubcktTable(
  Hrc_Model_t *model)
{
  return model->subcktTable;
}

Hrc_Model_t *
Hrc_SubcktReadModel(
  Hrc_Subckt_t *subckt)
{
  return subckt->model;
}
    
char *
Hrc_SubcktReadInstanceName(
  Hrc_Subckt_t *subckt)
{
  return subckt->instanceName;
}

array_t *
Hrc_SubcktReadActualInputVars(
  Hrc_Subckt_t *subckt)
{
  return subckt->actualInputVars;
}

array_t *
Hrc_SubcktReadActualOutputVars(
  Hrc_Subckt_t *subckt)
{    
  return subckt->actualOutputVars;
}

Hrc_Manager_t *
Hrc_NodeReadManager(
  Hrc_Node_t *node)
{
  return node->manager;
}

char *
Hrc_NodeReadModelName(
  Hrc_Node_t *node)
{
  return node->modelName;
}

char *
Hrc_NodeReadInstanceName(
  Hrc_Node_t *node)
{
  return node->instanceName;
}

Hrc_Node_t *
Hrc_NodeReadParentNode(
  Hrc_Node_t *node)
{
  return node->parentNode;
}

int
Hrc_NodeReadNumFormalInputs(
  Hrc_Node_t *node)
{
  return array_n(node->formalInputs);
}

int
Hrc_NodeReadNumFormalOutputs(
  Hrc_Node_t *node)
{
  return array_n(node->formalOutputs);
}

int
Hrc_NodeReadNumVariables(
  Hrc_Node_t *node)
{
  return st_count(node->varTable);
}

int
Hrc_NodeReadNumTables(
  Hrc_Node_t *node)
{
  return array_n(node->nameTables);
}

int
Hrc_NodeReadNumLatches(
  Hrc_Node_t *node)
{
  return st_count(node->latchTable);
}

int
Hrc_NodeReadNumChildren(
  Hrc_Node_t *node)
{
  return st_count(node->childTable);
}

array_t *
Hrc_NodeReadFormalInputs(
  Hrc_Node_t *node)
{
  return node->formalInputs;
}

array_t *
Hrc_NodeReadFormalOutputs(
  Hrc_Node_t *node)
{
  return node->formalOutputs;
}

array_t *
Hrc_NodeReadActualInputs(
  Hrc_Node_t *node)
{
  return node->actualInputs;
}

array_t *
Hrc_NodeReadActualOutputs(
  Hrc_Node_t *node)
{
  return node->actualOutputs;
}

array_t *
Hrc_NodeReadNameTables(
  Hrc_Node_t *node)
{
  return node->nameTables;
}
    
st_table *
Hrc_NodeReadChildTable(
  Hrc_Node_t *node)
{
  return node->childTable;
}

st_table *
Hrc_NodeReadLatchTable(
  Hrc_Node_t *node)
{
  return node->latchTable;
}

st_table *
Hrc_NodeReadVariableTable(
  Hrc_Node_t *node)
{
  return node->varTable;
}

void *
Hrc_NodeReadUndef(
  Hrc_Node_t *node)
{
  return node->undef;
}
Hrc_Latch_t *
Hrc_NodeFindLatchByName(
  Hrc_Node_t *node,
  char *latchName)
{
  Hrc_Latch_t *latch;
    
  if(st_lookup(node->latchTable, latchName, &latch)) {
    return latch;
  }
  else {
    return NIL(Hrc_Latch_t);
  }
}

Var_Variable_t *
Hrc_NodeFindVariableByName(
  Hrc_Node_t *node,
  char *varName)
{
  Var_Variable_t *var;
  
  if(st_lookup(node->varTable, varName, &var)) {
    return var;
  }
  else {
    return NIL(Var_Variable_t);
  }    
}

Hrc_Node_t *
Hrc_NodeFindChildByName(
    Hrc_Node_t *node,
    char *instanceName)
{
  Hrc_Node_t *childNode;

  if(st_lookup(node->childTable, instanceName, &childNode)) {
    return childNode;
  }
  else {
    return NIL(Hrc_Node_t);
  }    
}

Var_Variable_t *
Hrc_LatchReadInput(
  Hrc_Latch_t *latch)
{
  return latch->latchInput;
}
    
Var_Variable_t *
Hrc_LatchReadOutput(
  Hrc_Latch_t *latch)
{
  return latch->latchOutput;
}

Tbl_Table_t *
Hrc_LatchReadResetTable(
    Hrc_Latch_t *latch)
{
  return latch->resetTable;
}

void *
Hrc_LatchReadUndef(
  Hrc_Latch_t *latch)
{
  return latch->undef;
}

void
Hrc_ManagerSetRootNode(
  Hrc_Manager_t *manager,
  Hrc_Node_t *node)
{
  manager->rootNode = node;
}

void
Hrc_ManagerSetCurrentNode(
  Hrc_Manager_t *manager,
  Hrc_Node_t *currentNode)
{
  manager->currentNode = currentNode;
}

boolean
Hrc_NodeAddFormalInput(
  Hrc_Node_t *node,
  Var_Variable_t *var)
{
  char *name = Var_VariableReadName(var);

  if(!Var_VariableTestIsPI(var)) {
    array_insert_last(Var_Variable_t *, node->formalInputs, var);
    st_insert(node->varTable, name, (char *) var);
    (void)Var_VariableSetPI(var);
    return TRUE;
  }
  else {
    return FALSE;
  }
}

boolean
Hrc_NodeAddFormalOutput(
  Hrc_Node_t *node,
  Var_Variable_t *var)
{
  char *name = Var_VariableReadName(var);

  if(!Var_VariableTestIsPO(var)) {
    array_insert_last(Var_Variable_t *, node->formalOutputs, var);
    st_insert(node->varTable, name, (char *) var);
    (void)Var_VariableSetPO(var);
    return TRUE;
  }
  else {
    return FALSE;
  }
}

void
Hrc_NodeAddNameTable(
  Hrc_Node_t *node,
  Tbl_Table_t *nameTable)
{
  array_insert_last(Tbl_Table_t *, node->nameTables, nameTable);
}

void
Hrc_NodeSetUndef(
  Hrc_Node_t *node,
  void *value)
{
  node->undef = value;
}

boolean
Hrc_LatchSetResetTable(
  Hrc_Latch_t *latch,
  Tbl_Table_t *table)
{
  if (latch->resetTable != NIL(Tbl_Table_t)){
    return FALSE;
  }
  latch->resetTable = table;
  return TRUE;
}

void
Hrc_LatchSetUndef(
  Hrc_Latch_t *latch,
  void *value)
{
  latch->undef = value;
}
    

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


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