src/spfd/spfdSpfd.c

Go to the documentation of this file.

#include "spfdInt.h"

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


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


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


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


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


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

static bdd_node * ComputeAuxRel(SpfdApplData_t *applData, bdd_node *faninRel, Ntk_Node_t *from, int piSwap);

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


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

bdd_node *
SpfdNodeComputeSpfdFromOnAndOffSet(
  SpfdApplData_t *applData,
  Ntk_Node_t *regNode,
  bdd_node *bdd1,
  bdd_node *bdd0)
{
  bdd_manager *ddManager = applData->ddManager;
  int numFanin = Ntk_NodeReadNumFanins(regNode);
  bdd_node **yVars,**yAuxVars;
  bdd_node *ddTemp,*rel,*spfd;
  Ntk_Node_t *fanin;
  int j,clean;

  /* If bdd1 and bdd0 are not specified, replace bdd1 and bdd0 by the
     node's local ON-set and OFF-set respectively */
  clean = 0;
  if (bdd1 == NIL(bdd_node) ||
      bdd0 == NIL(bdd_node)) {
    Ntk_Network_t *network;
    network = Ntk_NodeReadNetwork(regNode);
    bdd_ref(bdd1 = SpfdNodeReadLocalBdd(network,regNode));
    bdd_ref(bdd0 = bdd_not_bdd_node(bdd1));
    /* Delete bdd1 and bdd0 at the end.*/
    clean = 1;
  }
  
  /* Array of variables for swapping */
  numFanin = Ntk_NodeReadNumFanins(regNode);
  yVars = ALLOC(bdd_node *,numFanin);
  yAuxVars = ALLOC(bdd_node *,numFanin);
  Ntk_NodeForEachFanin(regNode,j,fanin) {
    yVars[j] = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
    yAuxVars[j] = bdd_bdd_ith_var(ddManager,
                                  SpfdNodeReadAuxId(applData,fanin));
  }

  /* spfd is bdd1(y) * bdd0(y') + bdd1(y') * bdd0(y) */
  bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,bdd0,
                                          yVars,yAuxVars,numFanin));
  bdd_ref(rel = bdd_bdd_and(ddManager,bdd1,ddTemp));
  bdd_recursive_deref(ddManager,ddTemp);
      
  bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,rel,
                                          yVars,yAuxVars,numFanin));
  bdd_ref(spfd = bdd_bdd_or(ddManager,rel,ddTemp));
  bdd_recursive_deref(ddManager,rel);
  bdd_recursive_deref(ddManager,ddTemp);
  FREE(yVars);
  FREE(yAuxVars);

  if (clean) {
    bdd_recursive_deref(ddManager,bdd1);
    bdd_recursive_deref(ddManager,bdd0);
  }
  return spfd;
} /* End of SpfdNodeComputeSpfdFromOnAndOffSet */


bdd_node *
SpfdNodeComputeSpfdFromFanouts(
  SpfdApplData_t *applData,
  Ntk_Node_t *from)
{
  bdd_manager *ddManager = applData->ddManager;
  st_table *currBddReq;
  st_table *wireTable,*wiresRemoved;
  array_t *ordArray;
  bdd_node *result,*var,*varAux,*ddTemp,*ddTemp2;
  bdd_node *wireSpfd,*toSpfd,*fromSpfd,*xCube;
  bdd_node *step1,*faninRel,*faninRelAux,*inter,*final;
  bdd_node **firstCompose,**secondCompose;
  bdd_node *logicZero;
  Ntk_Node_t *fanin,*to;
  int index,i,j;
  int size,piSwap;


  if (Ntk_NodeReadNumFanouts(from) < 1) {
    (void) fprintf(vis_stdout,
                   "** spfd error: Node %s has no fanouts.\n",
                   Ntk_NodeReadName(from));
    return NIL(bdd_node);
  }
  currBddReq = applData->currBddReq;
  xCube = applData->currXCube;
  logicZero = bdd_read_logic_zero(ddManager);

  /* Compute the characteristic function of the fanin relation:
   faninRel = \prod y_i == f_i(X) */
  faninRel = SpfdComputeNodeArrayRelation(applData,currBddReq,NIL(array_t),
                                          Ntk_NodeReadFanins(from),
                                          TRUE,&piSwap);
  
  /* Convert faninRel(y,pi) to faninRel(\hat{y},pi) */
  faninRelAux = ComputeAuxRel(applData,faninRel,from,piSwap);
    
  /* Compute SPFD wire by wire according to the order specified for
     each fanout node. */
  wireTable = applData->currWireTable;
  wiresRemoved = applData->wiresRemoved;
  bdd_ref(fromSpfd = logicZero);
  Ntk_NodeForEachFanout(from,j,to) {

    bdd_ref(result = bdd_read_one(ddManager));
    ordArray = SpfdNodeReadFaninOrder(applData,to);
    arrayForEachItem(Ntk_Node_t *,ordArray,i,fanin) {
      var = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
      index = SpfdNodeReadAuxId(applData,fanin);
      varAux = bdd_bdd_ith_var(ddManager,index);
        
      if (fanin != from) {
        /* XNOR */
        bdd_ref(ddTemp = bdd_bdd_xnor(ddManager,var,varAux));
      } else {
        /* XOR */
        bdd_ref(ddTemp = bdd_bdd_xor(ddManager,var,varAux));
      }
      bdd_ref(ddTemp2 = bdd_bdd_and(ddManager,result,ddTemp));
      bdd_recursive_deref(ddManager,result);
      bdd_recursive_deref(ddManager,ddTemp);
      result = ddTemp2;
        
      if (fanin == from)
        break;
    }
      
    /* Compute AND of result and the SPFD of 'to'. */
    toSpfd = SpfdNodeReadSpfd(applData,to);
    if (toSpfd == NIL(bdd_node)) {
      (void) fprintf(vis_stderr,
                     "** spfd error: Spfd expected but not found.\n");
      (void) fprintf(vis_stderr, "To node:\n");
      Ntk_NodePrint(vis_stderr, to, TRUE, TRUE);
      (void) fprintf(vis_stderr, "From node:\n");
      Ntk_NodePrint(vis_stderr, from, TRUE, TRUE);
      fflush(vis_stderr);
      assert(0);
    }
    bdd_ref(wireSpfd = bdd_bdd_and(ddManager,toSpfd,result));
    bdd_recursive_deref(ddManager,result);

    /* Convert wireSpfd from fanout space to fanin space */
    /* Prepare the vectors for composition */
    size = bdd_num_vars(ddManager);
    firstCompose = ALLOC(bdd_node *,size);
    secondCompose = ALLOC(bdd_node *,size);
    for (i = 0; i < size; i++) {
      firstCompose[i] = bdd_bdd_ith_var(ddManager,i);
      secondCompose[i] = bdd_bdd_ith_var(ddManager,i);
    }
      
    arrayForEachItem(Ntk_Node_t *,ordArray,i,fanin) {
      int id,auxId;
        
      id = Ntk_NodeReadMddId(fanin);
      auxId = SpfdNodeReadAuxId(applData,fanin);
      st_lookup(currBddReq,(char *)fanin,(char **)&firstCompose[id]);
      secondCompose[auxId] = firstCompose[id];
    }
      
    /* Perform the steps of compose --> existential abstraction twice */
    bdd_ref(step1 = bdd_bdd_vector_compose(ddManager,wireSpfd,firstCompose));
    bdd_recursive_deref(ddManager,wireSpfd);
    FREE(firstCompose);
    bdd_ref(inter = bdd_bdd_and_abstract(ddManager,faninRel,step1,xCube));
    bdd_recursive_deref(ddManager,step1);
    
    /* The second of compose --> existential abstraction steps */
    bdd_ref(ddTemp = bdd_bdd_vector_compose(ddManager,inter,secondCompose));
    bdd_recursive_deref(ddManager,inter);
    FREE(secondCompose);
    bdd_ref(final = bdd_bdd_and_abstract(ddManager,faninRelAux,
                                         ddTemp,xCube));
    bdd_recursive_deref(ddManager,ddTemp);

    /* Now 'final' is in the fanin space */
    if (final == logicZero) {
      st_table *sinkTable;
      Ntk_Node_t *tempNode;
      boolean add;

      /* Check if this wire has already been removed. If yes, skip */
      add = TRUE;
      if (st_lookup(wiresRemoved,(char *)from,&sinkTable) &&
          st_lookup(sinkTable,(char *)to,&tempNode)) {
        add = FALSE;
      }

      if (add) {
        if (spfdVerbose > 2)
          (void) fprintf(vis_stdout,
                         "** spfd info: wire %s --> %s has empty spfd.\n",
                         Ntk_NodeReadName(from),Ntk_NodeReadName(to));
        
        /* Add to the wireTable */
        if (st_lookup(wireTable,(char *)from,&sinkTable)) {
          st_insert(sinkTable,(char *)to,(char *)to);
        } else {
          sinkTable = st_init_table(st_ptrcmp,st_ptrhash);
          st_insert(sinkTable,(char *)to,(char *)to);
          st_insert(wireTable,(char *)from,(char *)sinkTable);
        }
      }
    }
    
    bdd_ref(ddTemp = bdd_bdd_or(ddManager,fromSpfd,final));
    bdd_recursive_deref(ddManager,fromSpfd);
    bdd_recursive_deref(ddManager,final);
    
    fromSpfd = ddTemp;
  }
  bdd_recursive_deref(ddManager,faninRel);
  bdd_recursive_deref(ddManager,faninRelAux);
    
  /* Swap variables for fromSpfd if necessary */
  if (piSwap) { /* If we have used alternate PI ids */
    ddTemp = SpfdSwapPiAndAltPi(applData,fromSpfd);
    bdd_recursive_deref(ddManager,fromSpfd);
    fromSpfd = ddTemp;
  }
  
  return fromSpfd;
  
} /* End of SpfdNodeComputeSpfdFromFanouts */


st_table *
SpfdNodeComputeSCCs(
  SpfdApplData_t *applData,
  Ntk_Node_t *regNode,
  bdd_node **tempVars)
{
  bdd_manager *ddManager = applData->ddManager;
  st_table *inUseVars = applData->currInUseVars;
  Ntk_Node_t *fanin;
  st_table *SCC;
  bdd_node *spfd,*spfd2,*auxCube;
  bdd_node *ddTemp1,*ddTemp2,*logicZero,*faninCube;
  bdd_node *Ny,*E1y,*E0y;
  bdd_node *from,*To,*new_,*reached;
  bdd_node **faninVars,**auxVars;
  int i,numFanin,varsAllocated;

  numFanin = Ntk_NodeReadNumFanins(regNode);
  SCC = st_init_table(st_ptrcmp,st_ptrhash);
  spfd = SpfdNodeReadSpfd(applData,regNode);
  logicZero = bdd_read_logic_zero(ddManager);

  if (spfd == logicZero)
    return SCC;
  
  varsAllocated = 0;
  /* Allocate variables if necessary */
  if (tempVars == NIL(bdd_node *)) {
    tempVars = SpfdAllocateTemporaryVariables(ddManager,inUseVars,numFanin);
    varsAllocated = 1;
  }
  
  faninVars = ALLOC(bdd_node *,numFanin);
  auxVars = ALLOC(bdd_node *,numFanin);
  Ntk_NodeForEachFanin(regNode,i,fanin) {
    faninVars[i] = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
    auxVars[i] = bdd_bdd_ith_var(ddManager,
                                 SpfdNodeReadAuxId(applData,fanin));
  }

  bdd_ref(auxCube = bdd_bdd_compute_cube(ddManager,auxVars,
                                         NIL(int),numFanin));
  /* Compute spfd2 = \exists_{\hat{y}} spfd(y,\hat{y}) *
     spfd(\hat{y},\tilde{y}) */
  bdd_ref(ddTemp1 = bdd_bdd_swap_variables(ddManager,spfd,faninVars,
                                           auxVars,numFanin));
  bdd_ref(ddTemp2 = bdd_bdd_swap_variables(ddManager,ddTemp1,faninVars,
                                           tempVars,numFanin));
  bdd_recursive_deref(ddManager,ddTemp1);
  bdd_ref(spfd2 = bdd_bdd_and_abstract(ddManager,spfd,ddTemp2,auxCube));
  bdd_recursive_deref(ddManager,ddTemp2);

  /* SCC computation */
  bdd_ref(faninCube = bdd_bdd_compute_cube(ddManager,faninVars,
                                           NIL(int),numFanin));
  /* Compute N(y) = \exists_{\hat{y}} spfd(y,\hat{y}) */
  bdd_ref(Ny = bdd_bdd_exist_abstract(ddManager,spfd,auxCube));
  bdd_recursive_deref(ddManager,auxCube);

  while (Ny != logicZero) {
    /* To compute E1(y) perform the fixpoint image computation */
    bdd_ref(from = bdd_bdd_pick_one_minterm(ddManager,Ny,faninVars,numFanin));
    bdd_ref(reached = from);
    do {
      bdd_ref(ddTemp1 = bdd_bdd_and_abstract(ddManager,spfd2,from,faninCube));
      bdd_recursive_deref(ddManager,from);
      bdd_ref(To = bdd_bdd_swap_variables(ddManager,ddTemp1,tempVars,
                                          faninVars,numFanin));
      bdd_recursive_deref(ddManager,ddTemp1);
      bdd_ref(new_ = bdd_bdd_and(ddManager,To,bdd_not_bdd_node(reached)));
      bdd_recursive_deref(ddManager,To);
      bdd_ref(ddTemp1 = bdd_bdd_or(ddManager,reached,new_));
      bdd_recursive_deref(ddManager,reached);
      reached = ddTemp1;
      from = new_;
    } while (new_ != logicZero);

    E1y = reached;
    
    /* E_0(y) = \exists_{\hat{y}} spfd(y,\hat{y}) * E_1(y) */
    bdd_ref(ddTemp1 = bdd_bdd_and_abstract(ddManager,spfd,E1y,faninCube));
    bdd_ref(E0y = bdd_bdd_swap_variables(ddManager,ddTemp1,auxVars,
                                         faninVars,numFanin));
    bdd_recursive_deref(ddManager,ddTemp1);
    
    /* Update Ny: Ny = Ny * (E1y + E0y)' */
    bdd_ref(ddTemp1 = bdd_bdd_or(ddManager,E1y,E0y));
    bdd_ref(ddTemp2 = bdd_bdd_and(ddManager,Ny,bdd_not_bdd_node(ddTemp1)));
    bdd_recursive_deref(ddManager,ddTemp1);
    bdd_recursive_deref(ddManager,Ny);
    Ny = ddTemp2;

    /* Store E1y and E0y in an st_table */
    st_insert(SCC,(char *)E1y,(char *)E0y);
  }
  bdd_recursive_deref(ddManager,faninCube);
  bdd_recursive_deref(ddManager,Ny);
  
  FREE(auxVars);
  FREE(faninVars);

  if (varsAllocated) {
    long id;
    for (i = 0; i < numFanin; i++) {
      id = (long) bdd_node_read_index(tempVars[i]);
      st_delete(inUseVars,&id,NIL(char *));
    }
    FREE(tempVars);
  }
  
  return SCC;

} /* End of SpfdNodeComputeSCCs */

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

static bdd_node *
ComputeAuxRel(
  SpfdApplData_t *applData,
  bdd_node *faninRel,
  Ntk_Node_t *from,
  int piSwap)
{
  bdd_node **fromVars,**toVars;
  int numFi = Ntk_NodeReadNumFanins(from);
  int k,altId;
  Ntk_Node_t *fanin;
  bdd_node *faninRelAux;
  st_table *piAltVars;
  bdd_manager *ddManager = applData->ddManager;
  
  piAltVars = applData->currPiAltVars;
  
  /* Collect variables for swapping. */
  fromVars = ALLOC(bdd_node *,numFi);
  toVars = ALLOC(bdd_node *,numFi);
  Ntk_NodeForEachFanin(from,k,fanin) {
    int id = Ntk_NodeReadMddId(fanin);
    if (piSwap && st_lookup(piAltVars,(char *)(long)id,&altId)) {
      fromVars[k] = bdd_bdd_ith_var(ddManager,altId);
    } else {
      fromVars[k] = bdd_bdd_ith_var(ddManager,id);
    }
    toVars[k] = bdd_bdd_ith_var(ddManager,SpfdNodeReadAuxId(applData,fanin));
  }
  bdd_ref(faninRelAux = bdd_bdd_swap_variables(ddManager,faninRel,fromVars,
                                               toVars,numFi));
  FREE(fromVars);
  FREE(toVars);

  return faninRelAux;
  
} /* End of ComputeAuxRel */