src/maig/maigUtil.c

Go to the documentation of this file.

#include "maigInt.h"
#include "mvfaig.h"
#include "mvfaigInt.h"
#include "ctlspInt.h"
#include "ctlsp.h"
#include "ntk.h"

static char rcsid[] UNUSED = "$Id: maigUtil.c,v 1.20 2005/05/18 18:11:59 jinh Exp $";

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

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


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


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


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


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

static int NoOfBitEncode(int n);
static bAigEdge_t Case(mAig_Manager_t * mgr, array_t * encodeList, int index);
static int mCommandmAigTest(void);

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

void
mAig_Init(void)
{
  Cmd_CommandAdd("_mAig_test",
                 (int(*)(Hrc_Manager_t **, int, char **))  mCommandmAigTest,
                 0);
}


void
mAig_End(void)
{
}

array_t *
mAig_ArrayDuplicate(
  array_t *mAigArray)
{
  int      i;
  int      length = array_n(mAigArray);
  array_t *result = array_alloc(mAigEdge_t *, length);
  for (i = 0; i < length; i++) {
    mAigEdge_t *tempMAig = array_fetch(mAigEdge_t *, mAigArray, i);
    array_insert(mAigEdge_t *, result, i, tempMAig);
  }

  return (result);
}

mAig_Manager_t *
mAig_initAig(void)
{
  return bAig_initAig(5000); /* Initial number of nodes in the bAIG greaph*/
}

void
mAig_quit(
  mAig_Manager_t *manager)
{
 bAig_quit(manager);
}

mAigEdge_t
mAig_EquC(
  mAig_Manager_t * mgr,
  mAigEdge_t     mVarId,
  int            constant)
{
  array_t *mVarList    = mAigReadMulVarList(mgr);
  mAigMvar_t mVar      = array_fetch(mAigMvar_t, mVarList, mVarId);
  array_t  *encodeList = array_alloc(bAigEdge_t, 0);
  int i;
  bAigEdge_t bVarId;
  for(i=0; i< mVar.values; i++){
    if( i == constant){
      array_insert_last(bAigEdge_t, encodeList, mAig_One);      
    }
    else{
      array_insert_last(bAigEdge_t, encodeList, mAig_Zero);
    } /* if */
  } /* for */
  bVarId = Case(mgr, encodeList, mVar.bVars + mVar.encodeLength-1); /* Build the bAig grpah */
  array_free(encodeList);
  return bVarId;  
}

mAigEdge_t
mAig_CreateVar(
  mAig_Manager_t * mgr,
  char           * name,
  int            value)
{
  array_t *mVarList    = mAigReadMulVarList(mgr);
  array_t *bVarList    = mAigReadBinVarList(mgr);

  int         noBits      = NoOfBitEncode(value);
  int         i, startBvar, startMvar;
  /*
  char        bName[100];
  */
  char        *bName = ALLOC(char, strlen(name) + 10);
  mAigMvar_t  mVar;   
  mAigBvar_t  bVar; 

  assert(mVarList != NIL(array_t));
  assert(bVarList != NIL(array_t));

  startBvar = array_n(bVarList);
  startMvar = array_n(mVarList);

  /* Create Multi-valued variable */
  mVar.mVarId       = startMvar;
  mVar.bVars        = startBvar;
  mVar.values       = value;
  mVar.name         = name;
  mVar.encodeLength = noBits;
 
  array_insert_last(mAigMvar_t, mVarList, mVar);

  /* Create binary Variables of the Multi-valued variable */
  for (i=0; i<noBits; i++){
    sprintf(bName, "%s_%d", name, i);
    bVar.node = bAig_CreateVarNode(mgr,  util_strsav(bName));

    bVar.mVarId = mVar.mVarId; 
    array_insert_last(mAigBvar_t, bVarList, bVar);
  } /* for */
  return (mVar.mVarId);
}

mAigEdge_t
mAig_CreateVarFromAig(
  mAig_Manager_t * mgr,
  char           * name,
  array_t        *mvfAig)
{
  array_t *mVarList    = mAigReadMulVarList(mgr);
  array_t *bVarList    = mAigReadBinVarList(mgr);

  int noBits, value, index1;
  int startBvar, startMvar;
  int i, j, divider, orFlag;
  bAigEdge_t v, resultOn, resultOff;
  mAigMvar_t  mVar;   
  mAigBvar_t  bVar; 

  assert(mVarList != NIL(array_t));
  assert(bVarList != NIL(array_t));

  value = array_n(mvfAig);
  noBits = NoOfBitEncode(value);
  startBvar = array_n(bVarList);
  startMvar = array_n(mVarList);

  /* Create Multi-valued variable */
  mVar.mVarId       = startMvar;
  mVar.bVars        = startBvar;
  mVar.values       = value;
  mVar.name         = name;
  mVar.encodeLength = noBits;
 
  array_insert_last(mAigMvar_t, mVarList, mVar);

  for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {

    resultOn = bAig_Zero;
    resultOff = bAig_Zero;
/*    divider = (int)pow(2.0, (double)(i)); */
    divider = (int)pow(2.0, (double)(mVar.encodeLength-i-1));
    orFlag = 1;
    for(j=0; j<value; j++) {
      if(j%divider == 0)orFlag = !orFlag;
      v = array_fetch(bAigEdge_t, mvfAig, j);
      if(orFlag){
        resultOn = bAig_Or(mgr, resultOn, v);
      }
      else {
        resultOff = bAig_Or(mgr, resultOff, v);
      }
    }
    bVar.node = resultOn;
    bVar.mVarId = mVar.mVarId; 
    array_insert_last(mAigBvar_t, bVarList, bVar);
    index1++;
  }
  return (mVar.mVarId);
}

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

array_t * 
mAigReadBinVarList(
    mAig_Manager_t * manager)
{
  return (manager->bVarList);
}

array_t *
mAigReadMulVarList(
    mAig_Manager_t * manager)
{
  return (manager->mVarList);
}

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


static int
NoOfBitEncode(
   int n)
{
    int i = 0;
    int j = 1;

    if (n < 2) return 1; /* Takes care of mv.values <= 1 */

    while (j < n) {
        j = j * 2;
        i++;
    }
    return i;
}


static bAigEdge_t
Case(
  mAig_Manager_t * mgr,
  array_t *       encodeList,
  int             index)
{
  array_t       *bVarList    = mAigReadBinVarList(mgr);
  mAigBvar_t    bVar; 
  array_t       *newEncodeList;
  int           encodeLen = array_n(encodeList);  
  bAigEdge_t    andResult1, andResult2, orResult, result;
  bAigEdge_t    node1, node2;
  int i; 
  int count=0;

  if (encodeLen == 1){
    return array_fetch(bAigEdge_t, encodeList, 0);
  }
  bVar   = array_fetch(mAigBvar_t, bVarList, index); 
  newEncodeList =  array_alloc(bAigEdge_t, 0);

  for (i=0; i< (encodeLen/2); i++){
     node1 = array_fetch(bAigEdge_t, encodeList, count++);
     node2 = array_fetch(bAigEdge_t, encodeList, count++);
  
     /*  performs ITE operator */
     andResult1 = bAig_And(mgr, bVar.node,           node2);
     andResult2 = bAig_And(mgr, bAig_Not(bVar.node), node1);
     orResult   = bAig_Or (mgr, andResult1,          andResult2);
    
     array_insert_last(bAigEdge_t, newEncodeList, orResult);
    
  }
  if (encodeLen %2){ /* Odd */
     node1 = array_fetch(bAigEdge_t, encodeList, count);
     array_insert_last(bAigEdge_t, newEncodeList, node1);
  }
  result = Case(mgr, newEncodeList, index-1);
  array_free(newEncodeList);
  return result;
}


static int
mCommandmAigTest(void)
{
  array_t *mVarList;
  array_t *bVarList;

  MvfAig_Function_t * aa;
  MvfAig_Function_t * bb;
  MvfAig_Function_t * cc;

  mAigMvar_t mVar;   
  mAigBvar_t bVar; 

  int i;

  mAig_Manager_t *manager = mAig_initAig();
  mAigEdge_t      node1, node2, node3, node4, node5, node6;

  node1 = mAig_CreateVar(manager,"a",5); /* var a of 5 values */
  node2 = mAig_CreateVar(manager,"b",6); /* var b of 6 values */
  node3 = mAig_CreateVar(manager,"c",2); /* var c of 2 values */

  aa = MvfAig_FunctionCreateFromVariable(manager, node1);
  bb = MvfAig_FunctionCreateFromVariable(manager, node2);
  cc = MvfAig_FunctionCreateFromVariable(manager, node3);

  mVarList    = mAigReadMulVarList(manager);
  bVarList    = mAigReadBinVarList(manager);  
  fprintf(vis_stdout,"mValist: \n");
  for (i=0; i< array_n(mVarList); i++){
    mVar   = array_fetch(mAigMvar_t, mVarList, i);
    fprintf(vis_stdout,"mVarId=%d name=%s bVarId=%d values:%d\n",  mVar.mVarId, mVar.name, mVar.bVars, mVar.values);
  }

  fprintf(vis_stdout,"bValist: \n");
  for (i=0; i< array_n(bVarList); i++){
    bVar   = array_fetch(mAigBvar_t, bVarList, i);
    fprintf(vis_stdout,"mVar ID=%d bVar ID=%ld \n",  bVar.mVarId, bVar.node);
  }

  node4 = array_fetch(bAigEdge_t, aa, 3);
  node5 = array_fetch(bAigEdge_t, bb, 2);
  node6 = mAig_Or(manager, node4, node5);

  node4 = array_fetch(bAigEdge_t, cc, 0);
  node5 = bAig_Eq(manager, node6, node4);

  fprintf(vis_stdout,"%ld %ld %ld %ld %ld %ld\n",node1, node2, node3, node4, node5, node6);
  fprintf(vis_stdout,"Nodes Array:\n\n");
  for (i=0; i< manager->nodesArraySize ; i++)
    fprintf(vis_stdout,"Node #%d  value=%ld \n",i,manager->NodesArray[i]);

  fprintf(vis_stdout,"\n\nName List:\n");
  for (i=0; i< 20; i++)
    fprintf(vis_stdout,"index %d  Name %s \n",i, manager->nameList[i]);

  bAig_PrintDot(vis_stdout, manager);

  return 0;

}