src/restr/restrUtil.c

Go to the documentation of this file.

#include "restrInt.h"

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


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


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


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


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

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


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


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

array_t *
RestrGetOutputArray(Ntk_Network_t *network)
{
    lsGen                gen;
    Ntk_Node_t  *node;
    array_t     *outputArray;

    outputArray = array_alloc(char *, 0);
    Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
        array_insert_last(char *, outputArray, Ntk_NodeReadName(node));
    }

    return outputArray;
}

bdd_node *
RestrCreateProductOutput(
  bdd_manager   *ddManager,
  array_t       *funArray,
  bdd_node      **xVars,
  bdd_node      **yVars,
  int           nVars)
{
  bdd_node      *ddtemp, *ddtemp1;
  bdd_node      *fn, *result;
  int           i, num = array_n(funArray);

  bdd_ref(result = bdd_read_one(ddManager));

  for(i = 0; i < num; i++) {

    ddtemp = array_fetch(bdd_node *, funArray, i);;

    ddtemp1 = bdd_bdd_swap_variables(ddManager,ddtemp,xVars,yVars,nVars);
    bdd_ref(ddtemp1);
    fn = bdd_bdd_xnor(ddManager,ddtemp1,ddtemp);
    bdd_ref(fn);
    bdd_recursive_deref(ddManager,ddtemp1);
    ddtemp1 = bdd_bdd_and(ddManager,result,fn);
    bdd_ref(ddtemp1);
    bdd_recursive_deref(ddManager,fn);
    bdd_recursive_deref(ddManager,result);
    result = ddtemp1;
  }

  return result;
}

array_t *
RestrComputeTRWithIds(
  bdd_manager   *ddManager,
  array_t       *nextBdds,
  bdd_node      **xVars,
  bdd_node      **yVars,
  bdd_node      **uVars,
  bdd_node      **vVars,
  int           nVars)
{
  bdd_node      *ddtemp1, *ddtemp2;
  bdd_node      *oldTR, *fn;
  array_t       *composite;
  int            i;


  /* First compute oldTR(x,y) = \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) */
  bdd_ref(oldTR = bdd_read_one(ddManager));

  for(i = 0; i < nVars; i++) {
    ddtemp2  = array_fetch(bdd_node *, nextBdds, i);

    fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
    bdd_ref(fn);
    ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
    bdd_ref(ddtemp1);
    bdd_recursive_deref(ddManager,fn);
    bdd_recursive_deref(ddManager,oldTR);
    oldTR = ddtemp1;
  }
  
  /* fn(u,v) = oldTR(x-->u,y-->v) */
  ddtemp2 = bdd_bdd_swap_variables(ddManager,oldTR,xVars,uVars,nVars);
  bdd_ref(ddtemp2);
  fn = bdd_bdd_swap_variables(ddManager,ddtemp2,yVars,vVars,nVars);
  bdd_ref(fn);
  bdd_recursive_deref(ddManager,ddtemp2);
  ddtemp1 = bdd_bdd_and(ddManager,fn,oldTR);
  bdd_ref(ddtemp1);
  bdd_recursive_deref(ddManager,fn);

  /* Return both the relations */
  composite = array_alloc(bdd_node *,0);
  array_insert_last(bdd_node *,composite,oldTR);
  array_insert_last(bdd_node *,composite,ddtemp1);

  return composite;
}

bdd_node *
RestrGetEquivRelation(
  bdd_manager           *mgr,
  bdd_node        *Lambda,
  bdd_node        *tranRelation,
  bdd_node      **xVars,
  bdd_node      **yVars,
  bdd_node      **uVars,
  bdd_node      **vVars,
  bdd_node      **piVars,
  int             nVars,
  int             nPi,
  boolean restrVerbose)

{
    bdd_node *initialEsp, *espK;
    bdd_node *espKPlusOne;
    bdd_node *inputCube, *nextCube;
    bdd_node **allPreVars, **allNexVars;
    bdd_node *temp;
    int i,depth;

    allPreVars = ALLOC(bdd_node *, 2*nVars);
    allNexVars = ALLOC(bdd_node *, 2*nVars);
    for(i = 0; i < nVars;i++) {
        allPreVars[i] = xVars[i];
        allNexVars[i] = yVars[i];
    } 
    for(i = 0; i < nVars;i++) {
        allPreVars[i+nVars] = uVars[i];
        allNexVars[i+nVars] = vVars[i];
    } 

    nextCube = bdd_bdd_compute_cube(mgr,allNexVars,NIL(int),2*nVars);
    bdd_ref(nextCube);

    inputCube = bdd_bdd_compute_cube(mgr,piVars,NIL(int),nPi);
    bdd_ref(inputCube);

    initialEsp = bdd_bdd_univ_abstract(mgr,Lambda,inputCube);
    bdd_ref(initialEsp);

    espK = bdd_bdd_swap_variables(mgr,initialEsp,allPreVars,
                                 allNexVars,2*nVars);
    bdd_ref(espK);
    
    depth = 0;
    do {
        bdd_node *image, *temp1;
        image = bdd_bdd_and_abstract(mgr,tranRelation, espK, nextCube);
        bdd_ref(image);

        temp1 = bdd_bdd_univ_abstract(mgr,image,inputCube);
        bdd_ref(temp1);
        bdd_recursive_deref(mgr,image);

        espKPlusOne = bdd_bdd_and(mgr,temp1,initialEsp);
        bdd_ref(espKPlusOne);
        bdd_recursive_deref(mgr,temp1);
        temp1 = bdd_bdd_swap_variables(mgr,espKPlusOne,allPreVars,
                                     allNexVars,2*nVars);
        bdd_ref(temp1);
        bdd_recursive_deref(mgr,espKPlusOne);
        espKPlusOne = temp1;
        
        if (espKPlusOne == espK) {
          break;
        }
        bdd_recursive_deref(mgr,espK);
        espK = espKPlusOne;
        depth++;
    } while (1);

    if (restrVerbose)
      (void) fprintf(vis_stdout,"** restr info: EQ. relation computation depth = %d\n",
                     depth);

    bdd_recursive_deref(mgr,espKPlusOne);
    bdd_recursive_deref(mgr,initialEsp);
    bdd_recursive_deref(mgr,inputCube);
    bdd_recursive_deref(mgr,nextCube);

    bdd_ref(temp = bdd_bdd_swap_variables(mgr,espK,allNexVars,
                                          allPreVars,2*nVars));
    bdd_recursive_deref(mgr,espK);
    espK = temp;

    FREE(allPreVars);
    FREE(allNexVars);

    return espK;
}

bdd_node *
RestrComputeEquivRelationUsingCofactors(
  bdd_manager   *mgr,
  bdd_node      *Lambda,
  bdd_node      *TR,
  bdd_node      **xVars,
  bdd_node      **yVars,
  bdd_node      **uVars,
  bdd_node      **vVars,
  bdd_node      **piVars,
  int             nVars,
  int             nPi,
  boolean         restrVerbose)

{
  bdd_node *espKxu, *espKyv, *espKPlusOne, *espKMinusOne;
  bdd_node *espKCofKMinusOne;
  bdd_node *inputCube, *nextCube;
  bdd_node *tranRelation;
  bdd_node *newTran;
  bdd_node **allPreVars, **allNexVars;
  int i,depth;

  bdd_ref(tranRelation = TR);

  allPreVars = ALLOC(bdd_node *, 2*nVars);
  allNexVars = ALLOC(bdd_node *, 2*nVars);
  for(i = 0; i < nVars;i++) {
    allPreVars[i] = xVars[i];
    allNexVars[i] = yVars[i];
  } 
  for(i = 0; i < nVars;i++) {
    allPreVars[i+nVars] = uVars[i];
    allNexVars[i+nVars] = vVars[i];
  } 

  /* nextCube is a cube of yVars and vVars */
  nextCube = bdd_bdd_compute_cube(mgr,allNexVars,NIL(int),2*nVars);
  bdd_ref(nextCube);

  /* inputCube is a cube of piVars */
  inputCube = bdd_bdd_compute_cube(mgr,piVars,NIL(int),nPi);
  bdd_ref(inputCube);

  /* espKxu = \forall_{piVars} Lambda */
  espKxu = bdd_bdd_univ_abstract(mgr,Lambda,inputCube);
  bdd_ref(espKxu);

  espKyv = bdd_bdd_swap_variables(mgr,espKxu,allPreVars,
                                  allNexVars,2*nVars);
  bdd_ref(espKyv);
  bdd_ref(espKMinusOne = bdd_read_one(mgr));
  bdd_ref(espKPlusOne = bdd_read_one(mgr));

  /* The following loop is essentially the following:
   * E_{k+1} = E_k \wedge (\forall_x(func)) where
   * func = \exists_{yv} ((TR \downarrow E_k) \wedge (E_k \downarrow E_{k-1}))
   */
  depth = 0;
  while (1) {
    bdd_node *image, *temp1;
        
    bdd_recursive_deref(mgr, espKPlusOne);
    bdd_ref(espKCofKMinusOne = bdd_bdd_constrain(mgr, espKyv, 
                                                 espKMinusOne));
    bdd_recursive_deref(mgr, espKMinusOne);
    bdd_ref(espKMinusOne = espKyv);

    bdd_ref(newTran = bdd_bdd_constrain(mgr, tranRelation, espKxu));

    image = bdd_bdd_and_abstract(mgr,newTran, espKCofKMinusOne, nextCube);
    bdd_ref(image);
    bdd_recursive_deref(mgr, newTran);
    bdd_recursive_deref(mgr, espKCofKMinusOne);

    temp1 = bdd_bdd_univ_abstract(mgr,image,inputCube);
    bdd_ref(temp1);
    bdd_recursive_deref(mgr,image);
    espKPlusOne = bdd_bdd_and(mgr,temp1,espKxu);
    bdd_ref(espKPlusOne);
    bdd_recursive_deref(mgr,temp1);

    if (espKPlusOne == espKxu) {
      bdd_recursive_deref(mgr,espKMinusOne);
      bdd_recursive_deref(mgr,espKxu);
      bdd_recursive_deref(mgr,espKyv);
      bdd_recursive_deref(mgr,tranRelation);
      bdd_recursive_deref(mgr,inputCube);
      bdd_recursive_deref(mgr,nextCube);
      FREE(allPreVars);
      FREE(allNexVars);
      if (restrVerbose) {
        (void) fprintf(vis_stdout,"** restr info: EQ. relation computation depth = %d\n",
                       depth);
      }
      return espKPlusOne;
    }

    bdd_recursive_deref(mgr, espKxu);
    bdd_ref(espKxu = espKPlusOne);
    bdd_recursive_deref(mgr, espKyv);
    espKyv = bdd_bdd_swap_variables(mgr,espKxu,allPreVars,
                                    allNexVars,2*nVars);
    bdd_ref(espKyv);
        
    depth++;
  }

}

bdd_node *
RestrComputeTrWithGhostEdges(
  bdd_manager *mgr,
  bdd_node **yVars,
  bdd_node **vVars,
  bdd_node *tr,
  bdd_node *equivRelation,
  int nVars)
{
  bdd_node *abstractCube;
  bdd_node *temp;
  bdd_node *ghostTR;

  abstractCube = bdd_bdd_compute_cube(mgr,yVars,NIL(int),nVars);
  bdd_ref(abstractCube);

  temp = bdd_bdd_and_abstract(mgr,tr,equivRelation,abstractCube);
  bdd_ref(temp);
  bdd_recursive_deref(mgr,abstractCube);

  ghostTR = bdd_bdd_swap_variables(mgr,temp,vVars,yVars,nVars);
  bdd_ref(ghostTR);
  bdd_recursive_deref(mgr,temp);

  return ghostTR;
}

bdd_node *
RestrAddMaximum(
  bdd_manager *ddManager,
  bdd_node **f,
  bdd_node **g)
{
  bdd_node *plusInf;
  bdd_node *zero, *one;

  zero = bdd_read_zero(ddManager);
  one = bdd_read_one(ddManager);
  plusInf = bdd_read_plus_infinity(ddManager);

  if(*g == plusInf) {
    return zero;
  }

  if(bdd_is_constant(*f) && bdd_is_constant(*g)) {
    if(bdd_add_value(*f) > bdd_add_value(*g)) {
      return one;
    } else {
      return zero;
    }
  }
  return NULL;
}


bdd_node *
RestrAddEqual(
  bdd_manager *ddManager,
  bdd_node **f,
  bdd_node **g)
{
  bdd_node *zero, *one;

  zero = bdd_read_zero(ddManager);
  one = bdd_read_one(ddManager);

  if(*f == *g) {
    return one;
  }

  if(bdd_is_constant(*f) && bdd_is_constant(*g)) {
      return zero;
  }
  return NULL;
}

bdd_node **
RestrBddNodeArrayFromIdArray(
  bdd_manager   *ddManager,
  array_t       *idArray)
{
  bdd_node **xvars;
  int i,id;
  int nvars = array_n(idArray);

  xvars = ALLOC(bdd_node *, nvars);
  if (xvars == NULL)
    return NULL;

  for(i = 0; i < nvars; i++) {
    id = array_fetch(int,idArray,i);
    xvars[i] = bdd_bdd_ith_var(ddManager,id);
    bdd_ref(xvars[i]);
  }
  return xvars;
}

double 
RestrAverageBitChange(
  bdd_manager *manager,
  bdd_node *probTR,
  bdd_node **xVars,
  bdd_node **yVars,
  int nVars)
{
  bdd_node *diff, *cube, *PA, *QA;
  bdd_node **vars;
  double Mean;
  int i;

  vars = ALLOC(bdd_node *,2*nVars);
  for (i = 0; i < nVars; i++) {
    vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(xVars[i]));
    bdd_ref(vars[i]);
  }
  for (i = nVars; i < 2*nVars; i++) {
    vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(yVars[i-nVars]));
    bdd_ref(vars[i]);
  }

  cube = bdd_add_compute_cube(manager,vars,NIL(int),2*nVars);
  bdd_ref(cube);

  /* Calculate the Hamming distance ADD. This ADD represents the hamming
   * distance between two vectors represented by xVars and yVars.
   */
  bdd_ref(diff = bdd_add_hamming(manager,xVars,yVars,nVars));
  bdd_ref(PA = bdd_add_apply(manager,bdd_add_times,probTR,diff));
  bdd_recursive_deref(manager,diff);
  
  /* And now add and abstract all the variables.*/
  bdd_ref(QA = bdd_add_exist_abstract(manager,PA,cube));
  bdd_recursive_deref(manager,PA);
  bdd_recursive_deref(manager,cube);
  Mean = (double)bdd_add_value(QA);
  bdd_recursive_deref(manager,QA); 

  for (i = 0; i < 2*nVars; i++) {
    bdd_recursive_deref(manager,vars[i]);
  }
  FREE(vars);
  return Mean;
}

array_t *
RestrCreateNewStateVars(
  Ntk_Network_t *network,
  bdd_manager *ddManager,
  bdd_node **xVars,
  bdd_node **yVars)

{
  Ntk_Node_t *node1;
  char *name, *name1;
  array_t *varValues;
  array_t *nameArray;
  int i,id,index;
  int nVars = Ntk_NetworkReadNumLatches(network);

  array_t *uVarIds, *vVarIds;
  array_t *result;

  varValues = array_alloc(int, 0);
  nameArray = array_alloc(char *,0);    
  uVarIds = array_alloc(int, 0);
  vVarIds = array_alloc(int, 0);
  result = array_alloc(array_t *, 0);

  id = bdd_num_vars(ddManager);

  for (i = 0; i < nVars; i++) {
    index = bdd_node_read_index(yVars[i]);
    node1 = Ntk_NetworkFindNodeByMddId(network,index);
    name = Ntk_NodeReadName(node1);
    name1 = util_strcat3(name,"$NTK2","");
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name1);
    array_insert_last(int, vVarIds, id);
    id++;

    index = bdd_node_read_index(xVars[i]);
    node1 = Ntk_NetworkFindNodeByMddId(network,index);
    name = Ntk_NodeReadName(node1);
    name1 = util_strcat3(name,"$NTK2","");
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name1);
    array_insert_last(int, uVarIds, id);
    id++;

  }
  mdd_create_variables(ddManager,varValues,nameArray,NIL(array_t));

  arrayForEachItem(char *,nameArray,i,name) {
    FREE(name);
  }
  array_free(nameArray);
  array_free(varValues);

  array_insert_last(array_t *, result, uVarIds);
  array_insert_last(array_t *, result, vVarIds);

  return result;
}


void
RestrSetInitialOrder(
  Ntk_Network_t *network,
  bdd_manager   *ddManager)

{
  Ntk_Node_t *node, *node1;
  lsGen gen;
  char *name;
  array_t       *varValues;
  array_t       *nameArray;
  int           id;

  varValues = array_alloc(int,0);
  nameArray = array_alloc(char *,0);

  id = 0;
  Ntk_NetworkForEachLatch(network,gen,node) {
    node1 = Ntk_NodeReadShadow(node);
    name = util_strsav(Ntk_NodeReadName(node1));
    Ntk_NodeSetMddId(node1,id);
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name);
    id++;

    name = util_strsav(Ntk_NodeReadName(node));
    Ntk_NodeSetMddId(node,id);
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name);
    id++;
  }

  Ntk_NetworkForEachPrimaryInput(network,gen,node) {
    name = util_strsav(Ntk_NodeReadName(node));
    Ntk_NodeSetMddId(node,id);
    array_insert_last(int,varValues,2);
    array_insert_last(char *,nameArray,name);
    id++;
  }

  mdd_create_variables(ddManager,varValues,nameArray,NIL(array_t));

  id = 0;
  arrayForEachItem(char *, nameArray, id, name) {
    FREE(name);
  }
  array_free(nameArray);
  array_free(varValues);

}