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

  FileName    [spfdCommon.c]

  PackageName [spfd]

  Synopsis [Essential routines required during SPFD computation.]

  Description [Essential routines required during SPFD computation.]

  SeeAlso     [spfdSpfd.c]

  Author      [Balakrishna Kumthekar]

  Copyright [This file was created at the University of Colorado at Boulder.
  The University of Colorado at Boulder makes no warranty about the suitability
  of this software for any purpose.  It is presented on an AS IS basis.]

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

#include "spfdInt.h"

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


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


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


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


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


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

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

static bdd_node * NodeComputeGeneralProbability(Ntk_Network_t *network, bdd_manager *ddManager, Ntk_Node_t *regNode, bdd_node *result);

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


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


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

  Synopsis [Compute SPFDs for the nodes in regionArray, i.e., the
  cluster. regionArray is sorted in the increasing order of
  topological depth.]

  SideEffects [None]

******************************************************************************/
void
SpfdRegionComputeSinglePairSpfd(
  Ntk_Network_t *network,
  SpfdApplData_t *applData,
  array_t *regionArray)
{
  Ntk_Node_t *node,*fanin,*fanout;
  int i,j,bound,maxFanin;
  long id;
  int numNodes,numFanin;
  boolean isPi,boundOrPO;
  st_table *nodeCountTable = NIL(st_table);
  st_table *regionNodes = applData->currRegionNodes;
  st_table *inUseVars = applData->currInUseVars;
  bdd_manager *ddManager = applData->ddManager;
  bdd_node **tempVars,*spfd,*localAlt;
  
  numFanin = -1; /* To keep compiler happy. */
  /* Delete node spfds when not needed */
  nodeCountTable = st_init_table(st_ptrcmp,st_ptrhash);
  arrayForEachItem(Ntk_Node_t *,regionArray,j,node) {
    int num = 0;
    Ntk_NodeForEachFanin(node,i,fanin) {
      /* spfds for boundary nodes, PI, PO are not derived from their
	 fanouts. */
      if (st_lookup(regionNodes,(char *)fanin,&bound) &&
	  !bound &&
	  !Ntk_NodeTestIsPrimaryInput(fanin) &&
	  !Ntk_NodeTestIsPrimaryOutput(fanin)) {
	num++;
      }
    }
    if (num) {
      int *count;
      count = ALLOC(int,1);
      *count = num;
      st_insert(nodeCountTable,(char *)node,(char *)count);
    }
  }

  /* Allocate temporary variables that MIGHT BE required during the
     computation of SCCs. We will allocate maxFanin temporary
     variables. */
  maxFanin = -1;
  arrayForEachItem(Ntk_Node_t *,regionArray,i,node) {
    numFanin = Ntk_NodeReadNumFanins(node);
    if (numFanin > maxFanin)
      maxFanin = numFanin;
  }
  tempVars = SpfdAllocateTemporaryVariables(ddManager,inUseVars,maxFanin);
  
  /* Compute spfd and localAlt for all the nodes in the region. */
  numNodes = array_n(regionArray);
  for (i = numNodes-1; i >= 0; i--) {
    node = array_fetch(Ntk_Node_t *,regionArray,i);
    st_lookup(regionNodes,(char *)node,&bound);

    /* Is it a boundary node or is it primary output? For such nodes,
       we dont not derive SPFDs from their fanouts. Their SPFDs are
       derived from their current function impelementation */
    boundOrPO = (bound || Ntk_NodeTestIsPrimaryOutput(node));
    isPi = Ntk_NodeTestIsPrimaryInput(node);
    
    if (isPi) {
      spfd = NIL(bdd_node);
    } else if (boundOrPO) {
      spfd = SpfdNodeComputeSpfdFromOnAndOffSet(applData,node,
						  NIL(bdd_node),
						  NIL(bdd_node));
    } else { /* Internal node */
      spfd = SpfdNodeComputeSpfdFromFanouts(applData,node);
    }
    /* Set node's spfd */
    SpfdNodeSetSpfd(applData,node,spfd);
    /* Set node's localAlt */
    if (isPi) {
      SpfdNodeSetLocalAlt(applData,node,NIL(bdd_node));
    } else if (boundOrPO) {
      bdd_ref(localAlt = SpfdNodeReadLocalBdd(network,node));
      SpfdNodeSetLocalAlt(applData,node,localAlt);
    } else { /* Internal node */
      int numSCC;
      st_table *SCC;
      SCC = SpfdNodeComputeSCCs(applData,node,tempVars);
      numSCC = st_count(SCC);
      if (numSCC == 0) {
	bdd_node *logicZero;
	if (spfdVerbose > 1)
	  (void) fprintf(vis_stdout,
			 "** spfd info: node %s is redundant.\n",
			 Ntk_NodeReadName(node));
	/* Set the localAlt to empty. */
	bdd_ref(logicZero = bdd_read_logic_zero(ddManager));
	SpfdNodeSetLocalAlt(applData,node,logicZero);
      } else {
	/* Reduce the spfd to a single pair. SCC components are dereferenced in
           the function. The localAlt is also set to one of the components of
           the single pair */
	SpfdNodeReduceSCCToSinglePair(applData,node,SCC);
      }
      st_free_table(SCC);
    }
    /* Clean nodeCountTable if the present node is an internal node. */
    if (!bound &&
	!Ntk_NodeTestIsPrimaryInput(node) &&
	!Ntk_NodeTestIsPrimaryOutput(node)) {
      Ntk_NodeForEachFanout(node,j,fanout) {
	int *count;
	if (st_lookup(nodeCountTable,(char *)fanout,&count)) {
	  (*count)--;
	  if (*count == 0) {
	    st_delete(nodeCountTable,&fanout,&count);
	    SpfdNodeDeleteSpfd(applData,fanout);
	    FREE(count);
	  }
	}
      }
    }
  }

  /* Some of the internal nodes' spfd might not be deleted via
     nodeCountTable. Delete them explicitly. SPFD of the first node is
     needed. It will be deleted later in the calling function. */
  for (i = 1; i < numNodes; i++) {
    node = array_fetch(Ntk_Node_t *,regionArray,i);
    SpfdNodeDeleteSpfd(applData,node);
  }
  /* Delete the fanin order arrays for region nodes */
  arrayForEachItem(Ntk_Node_t *,regionArray,i,node) {
    SpfdNodeDeleteFaninOrder(applData,node);
  }
  for (i = 0; i < numFanin; i++) {
    id = (long) bdd_node_read_index(tempVars[i]);
    st_delete(inUseVars,&id,NIL(char *));
  }
  FREE(tempVars);

  /* Assert that nodeCountTable is empty */
  assert(st_count(nodeCountTable) == 0);
  st_free_table(nodeCountTable);

  return;

} /* End of SpfdRegionComputeSinglePairSpfd */


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

  Synopsis [Collapse the SCCs in a node's SPFD into a binary SPFD by
  appropriately choosing a binary value associated with each of the
  SCCs. This function is used only when signal probabilites are known,
  i.e, only when vector simulation is performed. 'result' is the
  characteristic function of the set of SCCs combined with the
  parameters. For example, if {(E1_i,E0_i)} is the set of bipartite SCCs,

  result(Y,P) = \sum (p_i*E1_i + \bar{p}_i*E0_i). This function computes
  assignments to p_i such that the 'result' has lower switching
  activity than the previous implementation at regNode.]

  SideEffects [None]

******************************************************************************/
bdd_node *
SpfdNodeComputeOptParams(
  SpfdApplData_t *applData,
  Ntk_Node_t *regNode,
  bdd_node *result,
  bdd_node **parameters,
  int numIsfs)
{
  bdd_manager *ddManager = applData->ddManager;
  Ntk_Network_t *network = Ntk_NodeReadNetwork(regNode);
  bdd_node *genProb,*offGenProb;
  bdd_node *diff,*maxDiff,*optComb;
  bdd_node *ddTemp,*prevSwitching,*newSwitching;
  float prob,switching;
  
  /* Compute the new node probability in terms of parameters introduced */
  genProb = NodeComputeGeneralProbability(network,ddManager,regNode,result);
  bdd_ref(offGenProb = bdd_add_apply(ddManager,bdd_add_minus,
				     bdd_read_one(ddManager),genProb));
  bdd_ref(newSwitching = bdd_add_apply(ddManager,bdd_add_times,
				       genProb,offGenProb));
  bdd_recursive_deref(ddManager,genProb);
  bdd_recursive_deref(ddManager,offGenProb);
  
  /* Compute the previous power dissipated */
  ddTemp = SpfdNodeReadLocalBdd(network,regNode);
  prob = Truesim_BddNodeComputeProbability(network,ddTemp);
  switching = prob*(1.0-prob);
  bdd_ref(prevSwitching = bdd_add_const(ddManager,switching));

  /* Find the combination of parameters that give max power savings,
     i.e. max(prevPowerAdd - newPowerAdd) */
  bdd_ref(diff = bdd_add_apply(ddManager,bdd_add_minus,prevSwitching,
			       newSwitching));
  bdd_recursive_deref(ddManager,prevSwitching);
  bdd_recursive_deref(ddManager,newSwitching);

  /* Find the max. difference */
  bdd_ref(maxDiff = bdd_add_find_max(ddManager,diff));

  if (bdd_add_value(maxDiff) <= 0.0) {
    bdd_recursive_deref(ddManager,diff);
    bdd_recursive_deref(ddManager,maxDiff);

    optComb = NIL(bdd_node);
  } else {
    /* Find minterms with max. difference */
    bdd_ref(optComb = bdd_add_apply(ddManager,SpfdAddEqual,maxDiff,diff));
    bdd_recursive_deref(ddManager,maxDiff);
    bdd_recursive_deref(ddManager,diff);

    /* optComb (an ADD) can be a cube, i.e., more than one
       minterm. Pick a minterm. Convert optComb to a BDD */
    bdd_ref(maxDiff = bdd_add_bdd_threshold(ddManager,optComb,(double) 1.0));
    bdd_recursive_deref(ddManager,optComb);
    optComb = maxDiff;

    /* Pick one cube */
    bdd_ref(maxDiff = bdd_bdd_pick_one_minterm(ddManager,optComb,parameters,
					       numIsfs));
    bdd_recursive_deref(ddManager,optComb);
    optComb = maxDiff;
  }

  return optComb;
  
} /* End of SpfdNodeComputeOptParams */


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

  Synopsis [Reduce the set of SCCs in a SPFD to a single SCC, i.e, to
  reduce to a binary SPFD. ]

  SideEffects [None]

******************************************************************************/
void
SpfdNodeReduceSCCToSinglePair(
  SpfdApplData_t *applData,
  Ntk_Node_t *regNode,
  st_table *SCC)
{
  Ntk_Network_t *network = Ntk_NodeReadNetwork(regNode);
  st_table *inUseVars = applData->currInUseVars;
  bdd_manager *ddManager = applData->ddManager;
  bdd_node **parameters;
  bdd_node *bdd1,*bdd0,*result,*spfd;
  bdd_node *optComb;
  st_generator *stGen;
  int numIsfs;
  int i;
  long lid;

  numIsfs = st_count(SCC);
  /* Allocate numIsfs binary valued parameters, one for each SCC. */
  parameters = SpfdComputeParameters(applData,SCC);

  /* Compute the general form representation for the local alternate
     function */
  bdd_ref(result = bdd_read_logic_zero(ddManager));
  i = 0;
  st_foreach_item(SCC,stGen,&bdd1,&bdd0) {
    bdd_node *ddTemp,*ddTemp2;
    bdd_ref(ddTemp = bdd_bdd_ite(ddManager,parameters[i],bdd1,bdd0));
    bdd_recursive_deref(ddManager,bdd1);
    bdd_recursive_deref(ddManager,bdd0);
    bdd_ref(ddTemp2 = bdd_bdd_or(ddManager,ddTemp,result));
    bdd_recursive_deref(ddManager,ddTemp);
    bdd_recursive_deref(ddManager,result);
    result = ddTemp2;
    i++;
  }

  if (!spfdPerfSim) { /* No switching activity info. available */
    /* Choose one combination of parameters */
    bdd_ref(optComb = bdd_bdd_compute_cube(ddManager,parameters,
					   NIL(int),numIsfs));
  } else {
    /* Compute the combination of parameters that reduce switching */
    optComb = SpfdNodeComputeOptParams(applData,regNode,result,
				       parameters,numIsfs);
  }

  if (optComb) { /* If such a combination exists */
    bdd_node *E1y,*E0y; /* BDDs for the care ON-set and care OFF-set,
			   respectively,  of the optimal ISF found in the
			   previous step. */
    bdd_node *imgOptComb;
    bdd_node **notParams;
    int size,i,id;

    /* Compute the lhs (care ON-set) of the ISF */
    bdd_ref(E1y = bdd_bdd_cofactor(ddManager,result,optComb));
    /* Compute the rhs (care OFF-set) of the ISF */
    size = bdd_num_vars(ddManager);
    notParams = ALLOC(bdd_node *,size);
    for (i = 0; i < size; i++) {
      bdd_ref(notParams[i] = bdd_bdd_ith_var(ddManager,i));
    }
    for (i = 0; i < numIsfs; i++) {
      id = bdd_node_read_index(parameters[i]);
      bdd_recursive_deref(ddManager,notParams[id]);
      bdd_ref(notParams[id] = bdd_not_bdd_node(parameters[i]));
    }
    bdd_ref(imgOptComb = bdd_bdd_vector_compose(ddManager,optComb,notParams));
    bdd_recursive_deref(ddManager,optComb);
    bdd_ref(E0y = bdd_bdd_cofactor(ddManager,result,imgOptComb));
    bdd_recursive_deref(ddManager,result);
    bdd_recursive_deref(ddManager,imgOptComb);

    /* Compute the spfd of E1y and E0y */
    spfd = SpfdNodeComputeSpfdFromOnAndOffSet(applData,regNode,E1y,E0y);
    SpfdNodeDeleteSpfd(applData,regNode);
    SpfdNodeSetSpfd(applData,regNode,spfd);

    /* Set E1y as the localAlt */
    SpfdNodeSetLocalAlt(applData,regNode,E1y);
    bdd_recursive_deref(ddManager,E0y);
    
    /* Free notParams */
    for (i = 0; i < size; i++) {
      bdd_recursive_deref(ddManager,notParams[i]);
    }
    FREE(notParams);
  } else { /* Compute alternate spfd from local function */
    bdd_node *bdd1,*bdd0;
    bdd_recursive_deref(ddManager,result);

    /* Set localAlt Bdd */
    bdd_ref(bdd1 = SpfdNodeReadLocalBdd(network,regNode));
    bdd_ref(bdd0 = bdd_not_bdd_node(bdd1));

    /* Set the new spfd */
    spfd = SpfdNodeComputeSpfdFromOnAndOffSet(applData,regNode,bdd1,bdd0);
    SpfdNodeDeleteSpfd(applData,regNode);
    SpfdNodeSetSpfd(applData,regNode,spfd);

    /* Set bdd1 as the localAlt */
    SpfdNodeSetLocalAlt(applData,regNode,bdd1);
    bdd_recursive_deref(ddManager,bdd0);
  }

  /* Free the parameters */
  for (i = 0; i < numIsfs; i++) {
    lid = (long) bdd_node_read_index(parameters[i]);
    st_delete(inUseVars,&lid,NIL(char *));
  }
  FREE(parameters);
  
  return;
  
} /* End of SpfdNodeReduceSCCToSinglePair */


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

  Synopsis [Global BDDs are required during the computation of SPFDs
  for cluster members. We compute them once and use it when
  needed. Also, these BDDs are removed when they are no longer
  required. Gloabl BDDs are required for all nodes in the cluster and
  their respective fanin nodes.]

  SideEffects [None]

******************************************************************************/
void
SpfdComputeRequiredGlobalBdds(
  Ntk_Network_t *network,
  SpfdApplData_t *applData)
{
  st_table *regionNodes,*rootTable,*leavesTable;
  st_table *currBddReq;
  array_t *rootArray,*nodeMvfs;
  st_generator *stGen;
  Ntk_Node_t *node,*fanin;
  char *dummy;
  int i;
  lsGen gen;
  bdd_t *mddOne;
  bdd_node *bdd1;
  bdd_manager *ddManager = applData->ddManager;
  mddOne = bdd_one(ddManager);

  /* Collect cluster nodes and also their fanin nodes */
  regionNodes = applData->currRegionNodes;
  rootTable = st_init_table(st_ptrcmp,st_ptrhash);
  st_foreach_item(regionNodes,stGen,&node,&dummy) {
    Ntk_NodeForEachFanin(node,i,fanin) {
      st_insert(rootTable,(char *)fanin,(char *)-1);
    }
  }

  /* Convert rootTable to rootArray for use by Ntm_NetworkBuildMvfs */
  rootArray = array_alloc(Ntk_Node_t *,0);
  st_foreach_item(rootTable,stGen,&node,&dummy) {
    array_insert_last(Ntk_Node_t *,rootArray,node);
  }
  st_free_table(rootTable);
  
  /* Collect the leaf nodes in the network. */
  leavesTable = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachCombInput(network,gen,node) {
    st_insert(leavesTable,(char *)node,(char *) -1);
  }

  /* Compute the Mvfs for the nodes in rootArray */
  nodeMvfs = Ntm_NetworkBuildMvfs(network,rootArray,leavesTable,mddOne);
  bdd_free(mddOne);
  st_free_table(leavesTable);
  
  /* Extract the BDDs and put them in currBddReq */
  currBddReq = applData->currBddReq = st_init_table(st_ptrcmp,st_ptrhash);
  arrayForEachItem(Ntk_Node_t *,rootArray,i,node) {
    Mvf_Function_t *mvf;
    mvf = array_fetch(Mvf_Function_t *,nodeMvfs,i);
    bdd1 = bdd_extract_node_as_is(array_fetch(bdd_t *,mvf,1));
    bdd_ref(bdd1);
    st_insert(currBddReq,(char *)node,(char *)bdd1);
  }
  array_free(rootArray);
  Mvf_FunctionArrayFree(nodeMvfs);

  return;

} /* End of SpfdComputeRequiredGlobalBdds */

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

  Synopsis [Returns the ADD representing the signal probability of
  regNode. 'result' is the BDD which has in support the variables in
  the fanin of regNode.]

  SideEffects [None]

******************************************************************************/
static bdd_node *
NodeComputeGeneralProbability(
  Ntk_Network_t *network,
  bdd_manager *ddManager,
  Ntk_Node_t *regNode,
  bdd_node *result)
{
  int size,k,id;
  bdd_node **onArray,**offArray;
  bdd_node *resultAdd,*genProb;
  Ntk_Node_t *fanin;
  float prob;
  
  size = bdd_num_vars(ddManager);
  onArray = ALLOC(bdd_node *,size);
  offArray = ALLOC(bdd_node *,size);
  for (k = 0; k < size; k++) {
    bdd_ref(onArray[k] = bdd_add_ith_var(ddManager,k));
    bdd_ref(offArray[k] = bdd_add_ite(ddManager,onArray[k],
				      bdd_read_zero(ddManager),
				      bdd_read_one(ddManager)));
  }
  
  Ntk_NodeForEachFanin(regNode,k,fanin) {
    id = Ntk_NodeReadMddId(fanin);
    bdd_recursive_deref(ddManager,onArray[id]);
    bdd_recursive_deref(ddManager,offArray[id]);
    prob = Truesim_NetworkReadNodeProbability(network,fanin);
    bdd_ref(onArray[id] = bdd_add_const(ddManager,prob));
    bdd_ref(offArray[id] = bdd_add_const(ddManager,1.0-prob));
  }

  bdd_ref(resultAdd = bdd_bdd_to_add(ddManager,result));
  genProb = (bdd_node *)bdd_add_general_vector_compose(ddManager,resultAdd,
						      onArray,offArray);
  bdd_ref(genProb);
  bdd_recursive_deref(ddManager,resultAdd);

  return genProb;
  
} /* End of NodeComputeGeneralProbability */