source: vis_dev/vis-2.3/src/restr/restrRestructure.c @ 45

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

  FileName    [restrRestructure.c]

  PackageName [restr]

  Synopsis [This file contains a main procedure that restructures an STG and
  transforms it into a new multilevel circuit.]

  Description [This file contains a main procedure that restructures an STG and
  transforms it into a new multilevel circuit. 

  Please refer to "A symbolic algorithm for low power sequential synthesis,"
  ISLPED 97, for more details.]

  SeeAlso     [restrHammingD.c restrFaninout.c restrCProj.c]

  Author      [Balakrishna Kumthekar <kumtheka@colorado.edu>]

  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 "restrInt.h"

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


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


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

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
extern int restrCreatedPart;
extern int restrCreatedFsm;
extern boolean restrVerbose;

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


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

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

static array_t * BuildFunctions(graph_t *partition, array_t *rootNames);
static bdd_node ** AddPowerSolve(bdd_manager *mgr, bdd_node *bddTr, bdd_node *init, bdd_node **x, bdd_node **y, bdd_node **pi, st_table *inputProb, int nVars, int nPi);
static bdd_node * PerformRestructure(bdd_manager *ddManager, bdd_node *prunedTR, bdd_node *equivRel, bdd_node *reachable, bdd_node *initBdd, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, bdd_node **uVars, bdd_node **vVars, st_table *inputProb, int nVars, int nPi, RestructureHeuristic heuristic, boolean equivClasses, array_t **outBdds, bdd_node **newInit, bdd_node **stateProbs);
static st_table * CreateNameToMvfTable(bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray);
static st_table * CreateCareTable(Ntk_Network_t *network, mdd_t *reachMdd);
static enum st_retval StMvfFree(char *key, char *value, char *arg);
static void CountEquivalentClasses(bdd_manager *ddManager, bdd_node *equivRel, bdd_node *initBdd, bdd_node **xVars, bdd_node **uVars, int nVars);
static array_t * GetBddArrayFromMvfArray(array_t *mvfArray);
static bdd_node * DoMarkovPowerAnalysis(bdd_manager *ddManager, bdd_node *prunedTR, bdd_node *initBdd, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, st_table *inputProb, int nVars, int nPi);
static array_t * ExtractTransitionFuns(bdd_manager *ddManager, bdd_node *finalTR, bdd_node **yVars, int nVars);
static array_t * GetBddArrayFromNameArray(Fsm_Fsm_t *fsm, array_t *nameArray);
static void ExpandReachableSet(bdd_manager *ddManager, bdd_node **reachable, bdd_node *equivRel, bdd_node **xVars, bdd_node **uVars, int nVars);
static graph_t * CreateNewPartition(Ntk_Network_t *network, bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray);
static Fsm_Fsm_t * CreateNewFsm(Ntk_Network_t *network, graph_t *partition, bdd_manager *ddManager, bdd_node *finalTR, bdd_node *initBdd, bdd_node *reachable, bdd_node *stateProbs, bdd_node **xVars, bdd_node **yVars, bdd_node **piVars, st_table *inputProb, int nVars, int nPi);

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


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

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

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

  Synopsis [This function performs the complete task of STG restructuring and
  logic implementation.]

  Description [The STG restructuring process proceeds as follows: First a state
  equivalence relation E(x,y) is derived from the current STG of the finite
  state machine. If the parameter <tt>nonReachEquiv</tt> is set E(x,y) is used
  to extend the set of reachable states R(x) to include those states equivalent
  to R(x) but unreachable. This sometimes provides extra flexibility when
  choosing an edge. To perform the restructuring transformation, edges are
  first added (clearly driven by E(x,y)) to the original STG and then
  undesirable edges are removed, in such a way that the functional behavior of
  the machine is not affected. We say that the original STG is transformed into
  an <tt>augmented</tt> STG.

  The steady state probabilities of the STG are computed using Markovian
  analysis. The edges of the augmented STG are then labeled by a cost function
  which depends on the absolute transition probability and hamming distance
  between the ends of the edge. After the appropriate <tt>heuristic</tt> is
  applied, the new (restructured) STG is then translated in to a multi-level
  boolean network.

  <tt>heuristic</tt> takes on four options: ham: Hamming distance based
  heuristic is used, fanin: Fanin oriented heuristic, faninout: Fanin-Fanout
  oriented heuristic, cproj: C-Projection. For more information please refer to
  "A symbolic algorithm for low power sequential synthesis," ISLPED 97.

  <tt>equivClasses</tt> prints the number of equivalent classes in the STG.

  <tt>inputProb</tt> is optional. If not specified, equiprobabale primary
  inputs are assumed. Else, the table contains the pair, (PI_name,prob), where
  <tt>prob</tt> is the probability of the PI signal being 1.

  <tt>synthInfo</tt> specifies synthesis specific options. For more information
  look at synth.h]

  The BDD variable order at the end of the algorithm is dumped into
  <tt>orderFileName</tt>.

  SideEffects [Network partition and FSM data structure are hooked to the
  network if necessary. They are however, cleared at the end of this
  procedure.]

  SeeAlso     [Synth_InitializeInfo]

******************************************************************************/
int
RestrCommandRestructureFsm(
  Fsm_Fsm_t *fsm,                          
  RestructureHeuristic heuristic,
  char *orderFileName,
  boolean equivClasses,
  boolean nonReachEquiv,
  boolean eqvMethod,
  st_table *inputProb,
  Synth_InfoData_t *synthInfo)
{

  graph_t *partition;
  Ntk_Network_t *network1;
  bdd_manager *ddManager;

  array_t *outputArray, *tranFunArray;
  array_t *outBdds, *nextBdds;
  array_t *tranRelationPair;
  array_t *newStateVars;

  st_table *careTable;

  int i;
  int nVars, nPi;
  int noRestruct = 0;
  boolean status;

  bdd_node *Lambda, *productTranRel, *prunedTR, *initialTR;
  bdd_node *equivRel;
  bdd_node *stateProbs;
  bdd_node *finalTR = NIL(bdd_node);
  bdd_node **xVars,**yVars,**uVars,**vVars;
  bdd_node **piVars;
  bdd_node *ddTemp, *reachable, *initBdd;
  bdd_node *newInit;

  mdd_t *reachStates, *mddTemp;
  mdd_t *careMdd;

  FILE *outFile;

  network1 = Fsm_FsmReadNetwork(fsm);
  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network1);

  /* Get the bdd_node for primary, present and next state variables.*/
  piVars = RestrBddNodeArrayFromIdArray(ddManager, 
                                        Fsm_FsmReadInputVars(fsm));
  xVars = RestrBddNodeArrayFromIdArray(ddManager, 
                                       Fsm_FsmReadPresentStateVars(fsm));
  yVars = RestrBddNodeArrayFromIdArray(ddManager,
                                       Fsm_FsmReadNextStateVars(fsm));
  /* Create new state variables for duplicate machine. */
  newStateVars = RestrCreateNewStateVars(network1, ddManager,xVars,yVars);
  uVars = RestrBddNodeArrayFromIdArray(ddManager,
                                       array_fetch(array_t *, 
                                                   newStateVars, 0));
  vVars = RestrBddNodeArrayFromIdArray(ddManager,
                                       array_fetch(array_t *, 
                                                   newStateVars, 1));

  /* Free memory: Delete the id array for new state variables.*/
  array_free(array_fetch(array_t *,newStateVars,0));
  array_free(array_fetch(array_t *,newStateVars,1));
  array_free(newStateVars);

  /* outputArray is the list of primary outputs. It is my responsibility to
  free it later. Both outputArray and tranFunArray are char * arrays.  Get the
  BDDs for output functions and transition functions.  Duplicate functions are
  returned.*/

  /* tranFunArray should not be freed */
  outputArray = RestrGetOutputArray(network1);
  tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm);
  outBdds = GetBddArrayFromNameArray(fsm,outputArray);
  nextBdds = GetBddArrayFromNameArray(fsm,tranFunArray);

  nVars = array_n(Fsm_FsmReadNextStateVars(fsm));
  nPi = array_n(Fsm_FsmReadInputVars(fsm));

  /* Compute Lambda = AND (out1 xnor out1$NTK2) and Transition relation.
   out1$NTK2 is the corresponding primary output (of output1) in the duplicate
   machine.*/
  if (restrVerbose) {
    fprintf(vis_stdout,"** restr info: Computing product output ... ");
  }
  Lambda = RestrCreateProductOutput(ddManager,outBdds,xVars, uVars, nVars);
  if (restrVerbose) {
    fprintf(vis_stdout,"Done.\n");
  }

  if (restrVerbose) {
    fprintf(vis_stdout,"** restr info: Computing TR of product machine ... ");
  }
  /* Compute the transition relation for both the single FSM and the product
     machine.  tranRelationPair[0] is the TR of single FSM and
     tranRelationPair[1] is the TR of product machine.  
     TR(x,w,y) = \prod_{i=0}^{i=n-1} (y_i \equiv f_i(w,x))
     productTR(x,u,w,y,v) = TR(x,w,y) * TR(u,w,v) */
  tranRelationPair = RestrComputeTRWithIds(ddManager,nextBdds,xVars, yVars,
                                           uVars,vVars,nVars);
  if (restrVerbose) {
    fprintf(vis_stdout,"Done.\n");
  }

  productTranRel = array_fetch(bdd_node *,tranRelationPair,1);

  /* Compute the state equivalence relation for the FSM */
  /* The support of equivRel is xVars and uVars. */
  if (restrVerbose) {
    fprintf(vis_stdout,"** restr info: Computing the equivalence relation ... ");
  }

  if (eqvMethod) {
    equivRel = RestrComputeEquivRelationUsingCofactors(ddManager,Lambda,
                                                       productTranRel,
                                                       xVars, yVars, uVars,
                                                       vVars, piVars,
                                                       nVars, nPi,
                                                       restrVerbose);
    bdd_recursive_deref(ddManager,Lambda);
  } else {
    equivRel = RestrGetEquivRelation(ddManager,Lambda,productTranRel,
                                     xVars,yVars,uVars,vVars,
                                     piVars,nVars,nPi,restrVerbose);
    bdd_recursive_deref(ddManager,Lambda);
  }
  if (restrVerbose) {
    fprintf(vis_stdout,"Done.\n");
  }
  /* Delete the product transition relation, as we no longer need it. */
  bdd_recursive_deref(ddManager,productTranRel);

  /* Compute the initial states */
  mddTemp = Fsm_FsmComputeInitialStates(fsm);
  initBdd = bdd_extract_node_as_is(mddTemp);
  bdd_ref(initBdd);
  mdd_free(mddTemp);

  /* Compute the reachable states. */
  reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
                                              Fsm_Rch_Default_c,0,0,
                                              NIL(array_t),FALSE, NIL(array_t));

  reachable = bdd_extract_node_as_is(reachStates);
  bdd_ref(reachable);
  mdd_free(reachStates);

  /* Check to see if there are any usable equivalence classes */
  if (bdd_count_minterm(ddManager,equivRel,2*nVars) == pow(2.0,nVars)) {
    fprintf(vis_stdout,"** restr info: Number of equivalence classes equals ");
    fprintf(vis_stdout,"number of possible states. \n");
    fprintf(vis_stdout,"** restr info: Restructuring will not help.\n");
    fprintf(vis_stdout,"** restr info: Proceeding with synthesis.\n");
    bdd_recursive_deref(ddManager,equivRel);
    /* Do not perform restructuring */
    noRestruct = 1;
  }

  /* Expand the reachable set R(x) to include those states which are equivalent
   to R(x) but unreachable. */
  if(nonReachEquiv && !noRestruct) {
    ExpandReachableSet(ddManager,&reachable,equivRel,xVars,uVars,nVars);
  }

  if (noRestruct) {
    /* Only synthesize the network */
    bdd_recursive_deref(ddManager,equivRel);
    bdd_recursive_deref(ddManager,
                        array_fetch(bdd_node *,tranRelationPair,0));
    array_free(tranRelationPair);
  } else {
    /* Constrain the original TR */
    initialTR = array_fetch(bdd_node *, tranRelationPair, 0);
    /* bdd_ref(prunedTR = bdd_bdd_and(ddManager,initialTR,reachable)); */
    bdd_ref(prunedTR = initialTR);
    bdd_recursive_deref(ddManager,initialTR);
    array_free(tranRelationPair);

    finalTR = PerformRestructure(ddManager,prunedTR,equivRel,reachable,
                                   initBdd,piVars,xVars,yVars,uVars,
                                   vVars,inputProb,nVars,nPi,heuristic,
                                   equivClasses,&outBdds,&newInit,
                                   &stateProbs);
    /* equivRel is dereferenced in the above procedure */
    if (prunedTR == finalTR) {
      fprintf(vis_stdout,"** restr info: Restructuring produces no changes. \n");
      fprintf(vis_stdout,"** restr info: Proceeding with synthesis. \n");
      bdd_recursive_deref(ddManager,stateProbs);
      noRestruct = 1;
    }

    bdd_recursive_deref(ddManager,prunedTR);
    bdd_recursive_deref(ddManager,initBdd);

    /* reachable can be deleted after computing the new reachable states.  Also
     need to perform markov analysis to find final bit change. */
    initBdd = newInit;
    if (!noRestruct) {
      arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
        bdd_recursive_deref(ddManager,ddTemp);
      }
      array_free(nextBdds);
      nextBdds = ExtractTransitionFuns(ddManager,finalTR,yVars,nVars);
    }
  }

  /* Create a partition for the new view of the fsm/network */
  if (!noRestruct) {
    partition = CreateNewPartition(network1,ddManager,outBdds,nextBdds,
                                   outputArray,tranFunArray);
    array_free(outBdds);
    array_free(nextBdds);
    /* Create the FSM and perform markov ananlysis */
    /* finalTR, stateProbs and reachabale are deleted in CreateNewFsm */
    fsm = CreateNewFsm(network1,partition,ddManager,finalTR,initBdd,
                       reachable,stateProbs,xVars,yVars,piVars,
                       inputProb,nVars,nPi);
  } else {
    /* Remove the outBdds, nextBdds */
    arrayForEachItem(bdd_node *, outBdds, i, ddTemp) {
      bdd_recursive_deref(ddManager,ddTemp);
    }
    arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
      bdd_recursive_deref(ddManager,ddTemp);
    }
    array_free(outBdds);
    array_free(nextBdds);
  }

  /* First create the care table for next state and primary output
   functions. */
  careMdd = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
                                          Fsm_Rch_Default_c,0,0,
                                          NIL(array_t),FALSE, NIL(array_t));

  careTable = CreateCareTable(network1,careMdd);

  /* Synthesize the restructured FSM */
  status = Synth_SynthesizeFsm(fsm,careTable,synthInfo,0);

  /* Clean up */
  if (!noRestruct) {
    Ntk_NetworkFreeApplInfo(network1,RESTR_PART_NETWORK_APPL_KEY);
    Ntk_NetworkFreeApplInfo(network1,RESTR_FSM_NETWORK_APPL_KEY);
  }
  mdd_free(careMdd);
  st_free_table(careTable);

  /* Dump the current BDD variable order, for future use. */
  if(orderFileName) {
    outFile = fopen(orderFileName,"w");
    if(outFile) {
      int size = array_n(mdd_ret_mvar_list(ddManager));
      int index;
      mvar_type var;
      for(i = 0; i < size;i++) {
        index = bdd_get_id_from_level(ddManager,i);
        var = mdd_get_var_by_id(ddManager,index);
        fprintf(outFile,"%s\n",var.name);
      }
      fclose(outFile);
    } else {
      fprintf(vis_stderr,"** restr error: Cannot open %s .\n",orderFileName);
    }
  }

  /* Clean up */
  for(i = 0; i < nVars; i++) {
    bdd_recursive_deref(ddManager,xVars[i]);
    bdd_recursive_deref(ddManager,yVars[i]);
    bdd_recursive_deref(ddManager,uVars[i]);
    bdd_recursive_deref(ddManager,vVars[i]);
  }
  for(i = 0 ; i < nPi; i++) {
    bdd_recursive_deref(ddManager,piVars[i]);
  }
  FREE(xVars);
  FREE(yVars);
  FREE(uVars);
  FREE(vVars);
  FREE(piVars);

  array_free(outputArray);

  return (status);
}


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

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

  Synopsis [Returns an array of Mvfs given node names.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static array_t *
BuildFunctions(
  graph_t *partition,
  array_t *rootNames)
{
  char *name;
  vertex_t *vertexPtr;
  Mvf_Function_t *mvf1;
  int i;
  array_t *result;

  result = array_alloc(Mvf_Function_t *,0);
  arrayForEachItem(char *,rootNames,i,name) {
    vertexPtr = Part_PartitionFindVertexByName(partition,name);
    mvf1 = Mvf_FunctionDuplicate(Part_VertexReadFunction(vertexPtr));
    array_insert(Mvf_Function_t *,result,i,mvf1);
  }

  return result;
}

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

  Synopsis [Performs markovian analysis.]

  Description [Returns a pair of ADDs. The ADD for steady state
  probabilities is at index 0 and the one-step transition probability
  is returned in index 1. bddTr is the BDD of the transition relation
  representing the STG. init is an ADD of initial probability vector.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static bdd_node **
AddPowerSolve(
  bdd_manager   *mgr,
  bdd_node      *bddTr,          
  bdd_node      *init,   
  bdd_node      **x,
  bdd_node      **y,
  bdd_node      **pi,
  st_table      *inputProb,
  int            nVars,
  int            nPi)
{
  bdd_node      *temp1, *temp, *q, *Correction;
  bdd_node        **result, *tr;
  bdd_node        **xAddVars, **yAddVars;
  bdd_node      *initG, *NewG;
  bdd_node      *inputCube,*xCube; 
  bdd_node      *newTr, *probMatrix;
  int           iter = 0;
  int           i;
  double        max,relTol = 0.0001;
  
  /* Initialize variables */
  result = ALLOC(bdd_node *, 2);
  xAddVars = ALLOC(bdd_node *, nVars);
  yAddVars = ALLOC(bdd_node *, nVars);
  for (i = 0; i < nVars; i++) {
    bdd_ref(xAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(x[i])));
    bdd_ref(yAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(y[i])));
  }
  bdd_ref(tr = bdd_bdd_to_add(mgr, bddTr));
  
  /* Create the input cube for abstraction */
  bdd_ref(temp1 = bdd_bdd_compute_cube(mgr, pi, NIL(int), nPi));
  bdd_ref(inputCube = bdd_bdd_to_add(mgr, temp1));
  bdd_recursive_deref(mgr, temp1);

  /* Compute the one-step transition probability matrix. */
  if (inputProb) {
    bdd_ref(probMatrix = Mark_addInProb(mgr,tr,inputCube,inputProb));
    bdd_recursive_deref(mgr,inputCube);
    bdd_recursive_deref(mgr,tr);
  }
  else {
    bdd_ref(Correction = bdd_add_const(mgr,(1.0/(double)(1 << nPi))));
    bdd_ref(q = bdd_add_exist_abstract(mgr,tr,inputCube));
    bdd_recursive_deref(mgr,inputCube);
    bdd_recursive_deref(mgr,tr);
    /* apply correction to the transition relation matrix and print it */
    bdd_ref(probMatrix = bdd_add_apply(mgr, bdd_add_times, q, Correction));
    bdd_recursive_deref(mgr,Correction);
    bdd_recursive_deref(mgr,q);
  }
  result[1] = probMatrix;

  /* Prepare the initial prob. vector. and the transition prob. matrix. */
  initG = bdd_add_swap_variables(mgr,init,xAddVars,yAddVars,nVars);
  bdd_ref(initG);
  /* Put transition prob. matrix in appropriate form (transpose). */
  newTr = bdd_add_swap_variables(mgr,probMatrix,xAddVars,yAddVars,nVars);
  bdd_ref(newTr);

  /* Calculate the x-cube for abstraction */
  bdd_ref(xCube = bdd_add_compute_cube(mgr,xAddVars,NIL(int),nVars));

  /* Loop until convergence */
  do {
    iter++;
    bdd_ref(temp = bdd_add_matrix_multiply(mgr,newTr,initG,yAddVars,nVars));
    bdd_ref(temp1 = bdd_add_exist_abstract(mgr,temp,xCube));
    bdd_ref(NewG = bdd_add_apply(mgr,bdd_add_divide,temp,temp1));
    bdd_recursive_deref(mgr,temp);
    bdd_recursive_deref(mgr,temp1);
    temp = NewG; 
    bdd_ref(q = bdd_add_swap_variables(mgr,temp,xAddVars,yAddVars,nVars));
    max = bdd_add_value(bdd_add_find_max(mgr,initG));

    if(bdd_equal_sup_norm(mgr,q,initG,relTol*max,0)) {
      bdd_recursive_deref(mgr,initG);
      bdd_recursive_deref(mgr,q);
      bdd_recursive_deref(mgr,xCube);
      bdd_recursive_deref(mgr,newTr);

      bdd_ref(temp1 = bdd_add_apply(mgr,bdd_add_times,probMatrix,temp));
      if (restrVerbose) {
        fprintf(vis_stdout,"** restr info: Average state bit change = %f\n",
                RestrAverageBitChange(mgr,temp1,x,y,nVars));
      }
      
      bdd_recursive_deref(mgr,temp1);
      for(i = 0;i < nVars; i++) {
        bdd_recursive_deref(mgr,xAddVars[i]);
        bdd_recursive_deref(mgr,yAddVars[i]);
      }
      FREE(xAddVars);
      FREE(yAddVars);
      result[0] = temp;
      return result;
    }
    bdd_recursive_deref(mgr,initG);
    bdd_recursive_deref(mgr,temp);
    initG = q;

  } while (1);

} /* end of AddPowerSolve */

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

  Synopsis [This routine performs the preprocessing steps of markovian analysis
  and the augmented STG computation. After the preprocessing steps the core
  restructuring steps are performed. Returns the BDD of the restructured STG.]

  SideEffects [<tt>outBdds</tt>, <tt>newInit</tt> are changed to
  reflect the restructured finite state machine. Steady state
  probabilities are returned in <tt>stateProbs</tt>]

  SeeAlso     []

******************************************************************************/
static bdd_node *
PerformRestructure(
  bdd_manager *ddManager,
  bdd_node *prunedTR,
  bdd_node *equivRel,
  bdd_node *reachable,
  bdd_node *initBdd,
  bdd_node **piVars,
  bdd_node **xVars,
  bdd_node **yVars,
  bdd_node **uVars,
  bdd_node **vVars,
  st_table *inputProb,
  int nVars,
  int nPi,
  RestructureHeuristic heuristic,
  boolean equivClasses,
  array_t **outBdds,
  bdd_node **newInit,
  bdd_node **stateProbs)
{
  /* equivRel is a function of uVars and xVars */
  /* prunedTR is a funciton of xVars, piVars and yVars */

  bdd_node *possessedProbMatrix;
  bdd_node *possessedTR = NIL(bdd_node);
  bdd_node *addPTR;
  bdd_node *finalTR;
  bdd_node *ddTemp;
  bdd_node *localStateProbs = NIL(bdd_node);

  if(equivClasses) {
    CountEquivalentClasses(ddManager,equivRel,initBdd,xVars,uVars,nVars);
  }

  /* Change the support of equivRel */
  bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,equivRel,xVars,yVars,
                                          nVars));
  bdd_recursive_deref(ddManager,equivRel);
  bdd_ref(equivRel = bdd_bdd_swap_variables(ddManager,ddTemp,uVars,vVars,
                                            nVars));
  bdd_recursive_deref(ddManager, ddTemp);

  /* The support of possessedTR is xVars and yVars and inputs.
   * If there exists an edge between x and y, and y == v, then
   * the following function adds an edge between x and v. These new
   * edges are referred to as ghost edges.
   */
  
  if (heuristic != RestrCProjection_c) {
    possessedTR = RestrComputeTrWithGhostEdges(ddManager, yVars, vVars, 
                                               prunedTR, equivRel, nVars);
  }

  /* stateProbs will not be used in the case of CProj and hammingD methods.  We
   can still compute the stateProbs to find the initial average bit change on
   the state lines. */
  *stateProbs = DoMarkovPowerAnalysis(ddManager,prunedTR,
                                      initBdd,piVars,xVars, 
                                      yVars,inputProb,nVars,nPi);
    
  if (!(heuristic == RestrCProjection_c || heuristic == RestrHammingD_c)) {
    bdd_node *temp, *cube;

    bdd_ref(cube = bdd_bdd_compute_cube(ddManager,piVars,NIL(int),nPi));
    bdd_ref(temp = bdd_bdd_exist_abstract(ddManager,possessedTR,cube));
    bdd_ref(addPTR = bdd_bdd_to_add(ddManager,temp));
    bdd_recursive_deref(ddManager,temp);

    bdd_ref(temp = bdd_bdd_to_add(ddManager, possessedTR));
    bdd_recursive_deref(ddManager, possessedTR);

    /* possessedProbMatrix is a weighted augmented STG where the weights are
       the transition probabilities */
    if (inputProb) {
      bdd_ref(possessedProbMatrix = Mark_addInProb(ddManager,temp,cube,
                                                   inputProb));
    } else {
      /* Assume equi probable primary inputs */
      bdd_node *q, *Correction;
      bdd_node *inputCube;

      bdd_ref(inputCube = bdd_bdd_to_add(ddManager,cube));
      bdd_ref(Correction = bdd_add_const(ddManager,
                                         (1.0/(double)(1 << nPi))));
      bdd_ref(q = bdd_add_exist_abstract(ddManager,temp,inputCube));
      bdd_ref(possessedProbMatrix = bdd_add_apply(ddManager,
                                                  bdd_add_times,
                                                  q, Correction));
      bdd_recursive_deref(ddManager,Correction);
      bdd_recursive_deref(ddManager,q);
      bdd_recursive_deref(ddManager,inputCube);
    }
    bdd_recursive_deref(ddManager,cube);
    bdd_recursive_deref(ddManager,temp);
    localStateProbs = *stateProbs;
  }

  switch(heuristic) {
  case RestrCProjection_c:
    finalTR = RestrMinimizeFsmByCProj(ddManager,equivRel,
                                      prunedTR,initBdd,
                                      xVars,yVars,uVars,vVars,piVars,
                                      nVars,nPi,outBdds,newInit);
    break;
  case RestrFanin_c:
  case RestrFaninFanout_c:
    ddTemp = bdd_read_background(ddManager);
    bdd_set_background(ddManager, 
                       bdd_read_plus_infinity(ddManager));

    /* addPTR and possessedProbMatrix are deleted in the following 
     * procedure. */
    finalTR = RestrMinimizeFsmByFaninFanout(ddManager,equivRel, prunedTR, 
                                            &addPTR,&possessedProbMatrix,initBdd,
                                            reachable,localStateProbs,piVars,xVars,
                                            yVars, uVars,vVars,
                                            nVars, nPi,heuristic,outBdds,newInit);

    /* Replace the original background value */
    bdd_set_background(ddManager,ddTemp);
    break; 
  case RestrHammingD_c: 
  default : 
    
    /* BALA, testing ... */
    /* Remove the edges out of the initial state. */
    {
/*       bdd_node *outEdges; */

/*       bdd_ref(outEdges = bdd_bdd_and(ddManager,prunedTR,initBdd)); */
/*       bdd_ref(adjustedTR = bdd_bdd_and(ddManager,prunedTR, */
/*                                     bdd_not_bdd_node(outEdges))); */
/*       finalTR = RestrSelectLeastHammingDStates(ddManager,adjustedTR, */
/*                                             possessedTR,xVars, */
/*                                             yVars,vVars,nVars,nPi); */
      
      finalTR = RestrSelectLeastHammingDStates(ddManager,prunedTR,
                                               possessedTR,xVars,
                                               yVars,vVars,nVars,nPi);
      bdd_recursive_deref(ddManager,possessedTR);
      bdd_ref(*newInit = initBdd);
      break;
    }
  }

  bdd_recursive_deref(ddManager,equivRel);
  return finalTR;
}

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

  Synopsis [Returns a table of (rootNames,rootMvfs). The parameters
  <tt>outBdds</tt> and <tt>nextBdds</tt> aare arrays of bdd_node *.
  <tt>outputArray</tt> and <tt>tranFunArray</tt> are arrays of strings and are
  in one-to-one correspondence with <tt>outBdds</tt> and <tt>nextBdds</tt>.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static st_table *
CreateNameToMvfTable(
  bdd_manager *ddManager,                  
  array_t *outBdds,
  array_t *nextBdds,
  array_t *outputArray,
  array_t *tranFunArray)
{
  st_table *nameToMvf;
  bdd_node *ddTemp;
  int i;

  /* Initialize variables */
  nameToMvf = st_init_table(strcmp, st_strhash);

  arrayForEachItem(bdd_node *, outBdds, i, ddTemp) {
    bdd_node *temp;
    mdd_t *regular, *complement;
    Mvf_Function_t *mvf;
    char *name;

    bdd_ref(temp = bdd_not_bdd_node(ddTemp));

    regular = bdd_construct_bdd_t(ddManager,ddTemp);
    complement = bdd_construct_bdd_t(ddManager,temp);

    mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0);
    array_insert(mdd_t *, mvf, 0, complement);
    array_insert(mdd_t *, mvf, 1, regular);

    name = array_fetch(char *, outputArray, i);
    st_insert(nameToMvf,name,(char *)mvf);
  }

  arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
    bdd_node *temp;
    mdd_t *regular, *complement;
    Mvf_Function_t *mvf;
    char *name;

    bdd_ref(temp = bdd_not_bdd_node(ddTemp));

    regular = bdd_construct_bdd_t(ddManager,ddTemp);
    complement = bdd_construct_bdd_t(ddManager,temp);

    mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0);
    array_insert(mdd_t *, mvf, 0, complement);
    array_insert(mdd_t *, mvf, 1, regular);

    name = array_fetch(char *, tranFunArray, i);
    st_insert(nameToMvf,name,(char *)mvf);
  }

  return nameToMvf;
}


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

  Synopsis [Create a (name,mdd_t*) table.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static st_table *
CreateCareTable(
  Ntk_Network_t *network,
  mdd_t *reachMdd)
{
  lsGen gen;
  Ntk_Node_t *node;
  st_table *careTable;

  careTable = st_init_table(strcmp, st_strhash);
  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
    char *name;
    name = Ntk_NodeReadName(node);
    st_insert(careTable,name,(char *)reachMdd);
  }
  Ntk_NetworkForEachLatch(network,gen,node){
    char *name;
    name = Ntk_NodeReadName(Ntk_LatchReadDataInput(node));
    st_insert(careTable,name,(char *)reachMdd);
  }

  return careTable;
}

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

  Synopsis    [Routine to free members of an st_table.]

  SideEffects [None]

  SeeAlso []
******************************************************************************/
static enum st_retval
StMvfFree(
  char *key,
  char *value,
  char *arg)
{
  /* This will free the memory associated with the array also */
  Mvf_FunctionFree((Mvf_Function_t *)value);
  
  return(ST_CONTINUE);
  
} /* end of StMvfFree */


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

  Synopsis [Routine to count number of equivalence classes in a relation.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static void
CountEquivalentClasses(
  bdd_manager *ddManager,
  bdd_node *equivRel,
  bdd_node *initBdd,
  bdd_node **xVars,
  bdd_node **uVars,
  int nVars)
{
  bdd_node *resultXU,*uCube;
  bdd_node *oneInitState,*classes;

  oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars);
  bdd_ref(oneInitState);

  bdd_ref(resultXU = bdd_bdd_cprojection(ddManager,equivRel,oneInitState));
  bdd_recursive_deref(ddManager,oneInitState);

#ifdef RESTR_DIAG
  {
    /* The following is valid only when equivRel is the equivalence relation on
       the complete set of states.*/
    bdd_node *xCube,*tautology;
    bdd_node *one;
    one = bdd_read_one(ddManager);
    bdd_ref(xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars));
    bdd_ref(tautology = bdd_bdd_exist_abstract(ddManager,resultXU,xCube));
    assert(tautology == one);
    bdd_recursive_deref(ddManager,tautology);
    bdd_recursive_deref(ddManager,xCube);
  }
#endif

#ifdef RESTR_DIAG
  {
    bdd_node *uCube,*zero,*classes;
    bdd_node *oneClass,*temp,*rep;
    int i;

    zero = bdd_not_bdd_node(bdd_read_one(ddManager));
    /* Extract the classes */
    bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars));
    bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube));
    bdd_recursive_deref(ddManager,uCube);
    
    i = 0;
    (void) fprintf(vis_stdout,"\n** restr diag: EQUIVALENT CLASSES:\n");
    while (classes != zero) {
      i++;
      bdd_ref(rep = bdd_bdd_pick_one_minterm(ddManager,classes,
                                             xVars,nVars));
      (void) fprintf(vis_stdout,"** restr diag: Class %d\n",i);
      (void) fprintf(vis_stdout,"** restr diag: Class representative:\n");
      RestrPrintBddNode(ddManager,rep);

      /* Extract the complete class now */
      bdd_ref(temp = bdd_bdd_cofactor(ddManager,resultXU,rep));
      bdd_ref(oneClass = bdd_bdd_swap_variables(ddManager,temp,uVars,
                                                xVars,nVars));
      bdd_recursive_deref(ddManager,temp);
      (void) fprintf(vis_stdout,"** restr diag: Class members:\n");
      RestrPrintBddNode(ddManager,oneClass);
      bdd_recursive_deref(ddManager,oneClass);

      /* Remove rep from classes */
      bdd_ref(temp = bdd_bdd_and(ddManager,classes,bdd_not_bdd_node(rep)));
      bdd_recursive_deref(ddManager,rep);
      bdd_recursive_deref(ddManager,classes);
      classes = temp;
    }
    (void) fprintf(vis_stdout,"** restr diag: Number of classes = %d\n",i);
  }
#endif

  /* Compute uCube and extract the u variables from resultXU */
  bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars));
  bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube));
  bdd_recursive_deref(ddManager,uCube);
  bdd_recursive_deref(ddManager,resultXU);

  fprintf(vis_stdout, "** restr info: Number of Equivalence Classes = %g\n",
          bdd_count_minterm(ddManager,classes,nVars));
  
  bdd_recursive_deref(ddManager,classes);
}


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

  Synopsis [Convert an array of Mvf_Function_t * to an array of bdd_node *]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static array_t *
GetBddArrayFromMvfArray(array_t *mvfArray)
{
  int     i;
  array_t *bddArray;
  Mvf_Function_t *mvf;

  bddArray = array_alloc(bdd_node *,0);

  arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) {
    mdd_t     *mddTemp;
    bdd_node    *ddNode;

    mddTemp = array_fetch(mdd_t *, mvf, 1);
    ddNode = bdd_extract_node_as_is(mddTemp);
    bdd_ref(ddNode);

    array_insert_last(bdd_node *, bddArray, ddNode);
  }
  return bddArray;
}

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

  Synopsis [Perform markovian analysis. The ADD for steady state probabilities
  of the STG is returned.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static bdd_node *
DoMarkovPowerAnalysis(
  bdd_manager *ddManager,
  bdd_node *prunedTR,
  bdd_node *initBdd,
  bdd_node **piVars,
  bdd_node **xVars,
  bdd_node **yVars,
  st_table *inputProb,
  int nVars,
  int nPi)
{
  bdd_node **result, *stateProbs;
  bdd_node *init;
  
  bdd_ref(init = bdd_bdd_to_add(ddManager,initBdd));
  if (restrVerbose) 
    (void) fprintf(vis_stdout,"** restr info: Initial average state bit change:\n");

  result = AddPowerSolve(ddManager,prunedTR,init,xVars,yVars,
                              piVars,inputProb,nVars,nPi);
  
  bdd_recursive_deref(ddManager,result[1]);
  stateProbs = result[0];
  bdd_recursive_deref(ddManager,init);
  FREE(result);
  
  return stateProbs;
}

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

  Synopsis [Given a relation R(X,Y) returns the array of functions y_i=f(X).]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static array_t *
ExtractTransitionFuns(
  bdd_manager   *ddManager,
  bdd_node      *finalTR,
  bdd_node      **yVars,
  int           nVars)
{
  bdd_node      *completeCube, *extractCube;
  bdd_node      *fun, *tranFun;
  array_t       *allTranFuns;
  int           i;

  allTranFuns = array_alloc(bdd_node *,0);

  completeCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars);
  bdd_ref(completeCube);

  for(i = 0;i < nVars; i++) {
    extractCube = bdd_bdd_cofactor(ddManager,completeCube,yVars[i]);
    bdd_ref(extractCube);
    fun = bdd_bdd_exist_abstract(ddManager,finalTR,extractCube);
    bdd_ref(fun);
    bdd_recursive_deref(ddManager,extractCube);
    tranFun = bdd_bdd_cofactor(ddManager,fun,yVars[i]);
    bdd_ref(tranFun);

#ifdef RESTR_DIAG
    {
      /* The following is to test if there are multiple edges out of a state
         with the same input label: in short to check if the relation is
         deterministic or not. */

      bdd_node *yBar,*yNot,*inter;
      bdd_ref(yNot = bdd_not_bdd_node(yVars[i]));
      bdd_ref(yBar = bdd_bdd_cofactor(ddManager,fun,yNot));
      bdd_recursive_deref(ddManager,yNot);
      bdd_ref(inter = bdd_bdd_and(ddManager,yBar,tranFun));
      yNot = bdd_not_bdd_node(bdd_read_one(ddManager));
      assert(inter == yNot);
      bdd_recursive_deref(ddManager,inter);
      bdd_recursive_deref(ddManager,yBar);
    }
#endif

    bdd_recursive_deref(ddManager,fun);
    array_insert_last(bdd_node *,allTranFuns,tranFun);
  }

  bdd_recursive_deref(ddManager,completeCube);
  return allTranFuns;
}

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

  Synopsis [Returns an array of BDDs given the node names of a network.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static array_t *
GetBddArrayFromNameArray(
  Fsm_Fsm_t *fsm,
  array_t *nameArray)
{
  graph_t *partition;
  array_t *bdds,*mvfs;
  
  partition = Fsm_FsmReadPartition(fsm);
  mvfs = BuildFunctions(partition,nameArray);
  bdds = GetBddArrayFromMvfArray(mvfs);
  Mvf_FunctionArrayFree(mvfs);

  return bdds;
}

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

  Synopsis [Expand the reachable set R(x) to include those states which are
  equivalent to R(x) but potentially not reachable.]

  SideEffects [<tt>reachable</tt> is updated.]

  SeeAlso     []

******************************************************************************/
static void
ExpandReachableSet(
  bdd_manager *ddManager,
  bdd_node **reachable,
  bdd_node *equivRel,
  bdd_node **xVars,
  bdd_node **uVars,
  int nVars)
{
  bdd_node *xcube,*potUnReach,*extReach;
  bdd_node *temp1;

  bdd_ref(xcube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars));
  /* potUnReach = \exists_x (E(x,u) * R(x)) */
  bdd_ref(potUnReach = bdd_bdd_and_abstract(ddManager,*reachable,
                                            equivRel,xcube));
  bdd_recursive_deref(ddManager,xcube);
  /* temp1(x) = potUnReach(u) */
  bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,potUnReach,uVars,
                                         xVars,nVars));
  bdd_recursive_deref(ddManager,potUnReach);
  /* extReach(x) = R(x) + potUnReach(x) */
  bdd_ref(extReach = bdd_bdd_or(ddManager,*reachable,temp1));
  bdd_recursive_deref(ddManager,temp1);
  bdd_recursive_deref(ddManager,*reachable);
  *reachable = extReach;
}

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

  Synopsis [Create a partition for the new view of the fsm/network]

  SideEffects [The new view is attached to the network.]

  SeeAlso     [CreateNewFsm]

******************************************************************************/
static graph_t *
CreateNewPartition(
  Ntk_Network_t *network,                  
  bdd_manager *ddManager,
  array_t *outBdds,
  array_t *nextBdds,
  array_t *outputArray,
  array_t *tranFunArray)
{
  st_table *nameToMvf;
  graph_t *partition;

  /* Create a table of next state and output Mvfs with their names as key to
     the table. This table is used to create a partition for the network. */
  nameToMvf = CreateNameToMvfTable(ddManager,outBdds,nextBdds,
                                   outputArray,tranFunArray);
  /* Delete the old partition and old fsm as we dont need it any more */
  if (restrCreatedPart) {
    Ntk_NetworkFreeApplInfo(network,RESTR_PART_NETWORK_APPL_KEY);
    restrCreatedPart = 0;
  }
  if (restrCreatedFsm) {
    Ntk_NetworkFreeApplInfo(network,RESTR_FSM_NETWORK_APPL_KEY);
    restrCreatedFsm = 0;
  }

  /* Create a new partition from the new root functions */
  partition = Part_NetworkCreatePartitionFromMvfs(network,nameToMvf);
  Ntk_NetworkAddApplInfo(network, RESTR_PART_NETWORK_APPL_KEY,
                         (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                         (void *) partition);
  st_foreach(nameToMvf,StMvfFree,NIL(char));
  st_free_table(nameToMvf);

  return partition;
}

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

  Synopsis [Create the FSM data structure for the restructured STG and perform
  markov analysis to estimate the final state average bit change.]

  SideEffects [<tt>reachable,initBdd,stateProbs,finalTR</tt> are dereferenced in this
  function.]

  SeeAlso     [CreateNewPatition]

******************************************************************************/
static Fsm_Fsm_t *
CreateNewFsm(
  Ntk_Network_t *network,
  graph_t *partition,
  bdd_manager *ddManager,
  bdd_node *finalTR,
  bdd_node *initBdd,
  bdd_node *reachable,
  bdd_node *stateProbs,
  bdd_node **xVars,
  bdd_node **yVars,
  bdd_node **piVars,
  st_table *inputProb,
  int nVars,
  int nPi)
{
  Fsm_Fsm_t *fsm;
  mdd_t *reachStates;
  mdd_t *mddTemp;
  bdd_node *ddTemp;
  bdd_node **markovResult;

  /* Create a new Fsm for the restructured network. */
  fsm = Fsm_FsmCreateFromNetworkWithPartition(network,
                                              Part_PartitionDuplicate(partition));
  assert(fsm != NIL(Fsm_Fsm_t));
  Ntk_NetworkAddApplInfo(network, RESTR_FSM_NETWORK_APPL_KEY,
                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
                         (void *) fsm); 
  /* We need to update the initial states as the
     Fsm_FsmCreateFromNetworkWithPartition will pick up old initial state from
     the network. Fsm_FsmSetInitialStates deletes old inital states. */
  mddTemp = bdd_construct_bdd_t(ddManager,initBdd);
  Fsm_FsmSetInitialStates(fsm,mddTemp);

  /* Compute the new reachable states */
  reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
                                              Fsm_Rch_Default_c,0,0,
                                              NIL(array_t),FALSE, NIL(array_t));

  bdd_recursive_deref(ddManager,reachable);
  reachable = bdd_extract_node_as_is(reachStates);
  bdd_ref(reachable);
  mdd_free(reachStates);
        
  /* Constrain the transition relation */
  bdd_ref(ddTemp = bdd_bdd_constrain(ddManager,finalTR,reachable));
  bdd_recursive_deref(ddManager,finalTR);
  finalTR = ddTemp;

  /* Use the state probs. of the original STG as the initial guess to compute
     the state probs. of the restructured STG. */
  if (restrVerbose)
    (void) fprintf(vis_stdout,"** restr info: Final average state bit change:\n");

  markovResult = AddPowerSolve(ddManager, finalTR, stateProbs, xVars,
                                    yVars,piVars,inputProb,nVars,nPi);
  bdd_recursive_deref(ddManager, markovResult[0]);
  bdd_recursive_deref(ddManager, markovResult[1]);
  FREE(markovResult);
        
  bdd_recursive_deref(ddManager,stateProbs);
  bdd_recursive_deref(ddManager,finalTR);
  bdd_recursive_deref(ddManager,reachable);

  return fsm;
}