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

  FileName    [synthSynth.c]

  PackageName [synth]

  Synopsis    [Synthesis Algorithms]

  Description [This file contains main routines that implement symbolic
  factorization algorithms.]

  SeeAlso     [synthDiv.c synthFactor.c synthGen.c synthOpt.c synthSimple.c]

  Author      [Balakrishna Kumthekar, In-Ho Moon]

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

static char rcsid[] UNUSED = "$Id: synthSynth.c,v 1.47 2005/04/23 14:37:51 jinh Exp $";


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


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


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


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


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


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

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

static int synthesizeNetwork(Ntk_Network_t *network, graph_t *partition, Fsm_Fsm_t *fsm, st_table *careBddTable, Synth_InfoData_t *synthInfo, int verbosity);
static int IsPartitionValid(Ntk_Network_t *network, graph_t *partition);
static array_t * GetCombOutputNameArray(Ntk_Network_t *network);
static array_t * GetCombInputIdArray(Ntk_Network_t *network);
static bdd_node ** GetBddArray(Mvf_Function_t *combMvfs);

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


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

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

  Synopsis    [Initialize the info data structure.]

  Description [Initialize the info data structure. See the documentation for
  CommandSynthesizeNetwork for the meaning of the various fields.]

  SideEffects [None]

  SeeAlso [Synth_FreeInfo]

******************************************************************************/
Synth_InfoData_t *
Synth_InitializeInfo(int factoring,
		     int divisor,
		     int unreachDC,
		     int reordering,
		     int trySharing,
		     int realign,
		     char *filehead,
		     char *prefix,
		     boolean eqn)
{

  Synth_InfoData_t *synthInfo;

  synthInfo = ALLOC(Synth_InfoData_t, 1);
  if (!synthInfo) {
    (void) fprintf(vis_stderr,
		   "** synth error: Could not initialize info structure.\n");
    return NIL(Synth_InfoData_t);
  }
  synthInfo->factoring = factoring;
  synthInfo->divisor = divisor;
  synthInfo->unreachDC = unreachDC;
  synthInfo->reordering = reordering;
  synthInfo->trySharing = trySharing;
  synthInfo->realign = realign;
  synthInfo->filehead = filehead;
  synthInfo->prefix = prefix;
  synthInfo->eqn = eqn;
  return synthInfo;
}

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

  Synopsis    [Free info data.]

  Description [Free Info data.]

  SideEffects [None]

  SeeAlso [Synth_InitializeInfo]

******************************************************************************/
void
Synth_FreeInfo(Synth_InfoData_t *synthInfo)
{
  FREE(synthInfo);
}

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

  Synopsis    [Synthesize a network.]

  Description [Synthesize a network. Here a major assumption is that, if the
  network is sequential, and an FSM is already hooked to the network, then the
  partition field of the FSM and that of the network are isomorphic.]

  SideEffects [If an FSM (in case of a sequential design) or the circuit
  partition does not already exist in the network, they are created and hooked
  to the network. However, they are freed at the end of this procedure. ]

  SeeAlso [Synth_SynthesizeFsm]

******************************************************************************/
int
Synth_SynthesizeNetwork(Ntk_Network_t *network,
			graph_t *partition,
			st_table *careTable,
			Synth_InfoData_t *synthInfo,
			int verbosity)
{
  graph_t *newPartition = NIL(graph_t);
  Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t);
  st_table *careBddTable;
  int status;
  int createdPart = 0;
  int createdFsm = 0;
  int ntkIsSeq = 1;

  if (bdd_get_package_name() != CUDD) {
    (void) fprintf(vis_stderr,
  "** synth error: The synthesis package can be used only with CUDD package\n");
    (void) fprintf(vis_stderr,
		   "** synth error: Please link with the CUDD package\n");
    return 0;
  }
  if (partition == NIL(graph_t)) {
    newPartition = (graph_t *) Ntk_NetworkReadApplInfo(network, 
						       PART_NETWORK_APPL_KEY);
    createdPart = 0; /* Using partition of the network. */
    if (newPartition == NIL(graph_t) || 
	(!IsPartitionValid(network,newPartition))) {
      newPartition = Part_NetworkCreatePartition(network, 
						 NIL(Hrc_Node_t),
						 "dummy", (lsList) 0, 
						 (lsList) 0, NIL(mdd_t),
						 Part_InOut_c,
						 (lsList) 0, 
						 FALSE, FALSE, TRUE);
      if (newPartition == NIL(graph_t)) {
	(void) fprintf(vis_stderr,"** synth error: Could not create an InOut");
	(void) fprintf(vis_stderr,"partition.\n");
	return 0;
      }
      createdPart = 1; /* Using new partition */
    }
  } else {
    if (IsPartitionValid(network,partition)) {
      newPartition = partition;
      createdPart = 2; /* Using the partition provided. */
    } else {
      newPartition = Part_NetworkCreatePartition(network, 
						 NIL(Hrc_Node_t),
						 "dummy", (lsList) 0, 
						 (lsList) 0, NIL(mdd_t),
						 Part_InOut_c,
						 (lsList) 0, 
						 FALSE, FALSE, TRUE);
      if (newPartition == NIL(graph_t)) {
	(void) fprintf(vis_stderr,"** synth error: Could not create an InOut");
	(void) fprintf(vis_stderr,"partition.\n");
	return 0;
      }
      createdPart = 1;    
    }
  }


  if(!Ntk_NetworkReadNumLatches(network)) {
    (void) fprintf(vis_stdout, "** synth info: No latches present in the ");
    (void) fprintf(vis_stdout, "current network.\n");
    (void) fprintf(vis_stdout,
		   "** synth info: Proceeding with combinational synthesis.\n");
    ntkIsSeq = 0;
  }

  if (ntkIsSeq) {
    switch (createdPart) {
    case 0:
      /* Check if there is already an Fsm attached to 
       * the network.
       */
      fsm = (Fsm_Fsm_t *) Ntk_NetworkReadApplInfo(network, 
						  FSM_NETWORK_APPL_KEY);
      if (fsm == NIL(Fsm_Fsm_t)) {
	fsm = Fsm_FsmCreateFromNetworkWithPartition(network, 
						    NIL(graph_t));
	if (fsm == NIL(Fsm_Fsm_t)) {
	  (void) fprintf(vis_stderr,"** synth error: Could not create ");
	  (void) fprintf(vis_stderr,"an Fsm\n");
	  goto endgame;
	}
	createdFsm = 1;
      } else {
	createdFsm = 0;
      }
      break;
    case 1:
    case 2:
      fsm = Fsm_FsmCreateFromNetworkWithPartition(network,
				  Part_PartitionDuplicate(newPartition));

      if (fsm == NIL(Fsm_Fsm_t)) {
	(void) fprintf(vis_stderr,"** synth error: Could not create ");
	(void) fprintf(vis_stderr,"an Fsm\n");
	goto endgame;
      }
      createdFsm = 1;
      break;
    }
  }

  careBddTable = NIL(st_table);
  if (careTable != NIL(st_table)) {
    mdd_t *mddTemp;
    bdd_node *ddNode;
    char *name;
    st_generator *stGen;

    careBddTable = st_init_table(strcmp, st_strhash);
    st_foreach_item(careTable,stGen,&name,&mddTemp) {
      ddNode = bdd_extract_node_as_is(mddTemp);
      st_insert(careBddTable,name,(char *)ddNode);
    }
  }
  if (fsm)
    status = synthesizeNetwork(network, newPartition,
			       fsm, careBddTable, synthInfo,
			       verbosity);
  else
    status = synthesizeNetwork(network,newPartition,
			       NIL(Fsm_Fsm_t), careBddTable,
			       synthInfo, verbosity);

  if (careBddTable)
    st_free_table(careBddTable);
  if (createdPart == 1)
    Part_PartitionFree(newPartition);
  if (createdFsm == 1)
    Fsm_FsmFree(fsm);

  return status;

 endgame:
  if (createdPart == 1)
    Part_PartitionFree(newPartition);
  if (createdFsm == 1)
    Fsm_FsmFree(fsm);

  return 0;

}

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

  Synopsis    [Synthesize an FSM.]

  Description [Synthesize an FSM. This procedure can be used if the default FSM
  attached to the network is different from the one that needs to be
  synthesized.]

  SideEffects [None]

  SeeAlso [Synth_SynthesizeNetwork]

******************************************************************************/
int
Synth_SynthesizeFsm(Fsm_Fsm_t *fsm,
		    st_table *careTable,
		    Synth_InfoData_t *synthInfo,
		    int verbosity)
{
  Ntk_Network_t *network;
  graph_t *partition;
  st_table *careBddTable;
  int status;

  network = Fsm_FsmReadNetwork(fsm);
  partition = Fsm_FsmReadPartition(fsm);

  careBddTable = NIL(st_table);
  if (careTable != NIL(st_table)) {
    mdd_t *mddTemp;
    bdd_node *ddNode;
    char *name;
    st_generator *stGen;

    careBddTable = st_init_table(strcmp, st_strhash);
    st_foreach_item(careTable,stGen,&name,&mddTemp) {
      ddNode = bdd_extract_node_as_is(mddTemp);
      st_insert(careBddTable,name,(char *)ddNode);
    }
  }
    
  status = synthesizeNetwork(network,partition,fsm,careBddTable,synthInfo,
			     verbosity);
  if (careBddTable)
    st_free_table(careBddTable);

  return status;
}

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


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

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

  Synopsis    [Core function of Synth_SynthesizeNetwork.]

  Description [Core function of Synth_SynthesizeNetwork and
  Synth_SynthesizeFsm.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static int
synthesizeNetwork(Ntk_Network_t *network,
		  graph_t *partition,
		  Fsm_Fsm_t *fsm,
		  st_table *careBddTable,
		  Synth_InfoData_t *synthInfo,
		  int verbosity)
{
  bdd_manager *ddManager = (bdd_manager *) Ntk_NetworkReadMddManager(network);
  int i, numOut;
  int *initStates = NIL(int);
  Mvf_Function_t *combMvfs;
  array_t *inputIds, *combOutNamesArray;
  bdd_node **combOutBdds, *ddTemp;
  bdd_node *unReachable = NIL(bdd_node), *reachable = NIL(bdd_node);
  bdd_node **combUpperBdds;
  bdd_node *initBdd = NIL(bdd_node), *temp;
  char **combOutNames;
  char *str;
  int realign_bdd, realign_zdd;
  Fsm_RchType_t reachMethod;

  /* Save current values of realignment flags. */
  realign_zdd = bdd_zdd_realignment_enabled(ddManager);
  realign_bdd = bdd_realignment_enabled(ddManager);

  if (synthInfo->reordering == 1) {
    if (synthInfo->realign)
      bdd_zdd_realign_enable(ddManager);
    else
      bdd_zdd_realign_disable(ddManager);
    bdd_realign_disable(ddManager);
  } else if (synthInfo->reordering == 2) {
    bdd_zdd_realign_disable(ddManager);
    if (synthInfo->realign)
      bdd_realign_enable(ddManager);
    else
      bdd_realign_disable(ddManager);
  } else {
    bdd_zdd_realign_disable(ddManager);
    bdd_realign_disable(ddManager);
  }

  /* Get the names of the combinational outputs, i.e, next state functions
   * as well as primary outputs. In VIS even latch initial inputs are
   * considered combinational outputs. Since, we support only blif files,
   * latch initial inputs are not present in combOutNamesArray.
   */
  combOutNamesArray = GetCombOutputNameArray(network);
  if (combOutNamesArray == NIL(array_t)) {
    if (realign_zdd == 1)
      bdd_zdd_realign_enable(ddManager);
    else
      bdd_zdd_realign_disable(ddManager);
    if (realign_bdd == 1)
      bdd_realign_enable(ddManager);
    else
      bdd_realign_disable(ddManager);
    return 0;
  }
  /* Get the array of combinational inputs, i.e., primary inputs, 
   * present state variables.
   */
  inputIds = GetCombInputIdArray(network);
  if (inputIds == NIL(array_t)) {
    array_free(combOutNamesArray);
    /* Restore values of realignment flags. */
    if (realign_zdd == 1)
      bdd_zdd_realign_enable(ddManager);
    else
      bdd_zdd_realign_disable(ddManager);
    if (realign_bdd == 1)
      bdd_realign_enable(ddManager);
    else
      bdd_realign_disable(ddManager);
    return 0;
  }
  /* Compute the Bdds */
  combMvfs = Part_PartitionBuildFunctions(partition,combOutNamesArray,
					  inputIds,NIL(mdd_t));
  combOutBdds = (bdd_node **) GetBddArray(combMvfs);
  if (combOutBdds == NIL(bdd_node *)) {
    array_free(combOutNamesArray);
    array_free(inputIds);
    Mvf_FunctionArrayFree(combMvfs);
    if (realign_zdd == 1)
      bdd_zdd_realign_enable(ddManager);
    else
      bdd_zdd_realign_disable(ddManager);
    if (realign_bdd == 1)
      bdd_realign_enable(ddManager);
    else
      bdd_realign_disable(ddManager);
    return 0;
  }
  Mvf_FunctionArrayFree(combMvfs);

  numOut = array_n(combOutNamesArray); 
  combOutNames = ALLOC(char *, numOut);
  if (combOutNames == NIL(char *)) {
    (void) fprintf(vis_stderr,"** synth error: Could not allocate memory\n");
    array_free(combOutNamesArray);
    array_free(inputIds);

    for (i = 0; i < numOut; i++) {
      bdd_recursive_deref(ddManager,combOutBdds[i]);
    }
    FREE(combOutBdds);
    if (realign_zdd == 1)
      bdd_zdd_realign_enable(ddManager);
    else
      bdd_zdd_realign_disable(ddManager);
    if (realign_bdd == 1)
      bdd_realign_enable(ddManager);
    else
      bdd_realign_disable(ddManager);
    return 0;
  }
  arrayForEachItem(char *, combOutNamesArray, i, str) {
    combOutNames[i] = str;
  }
  array_free(combOutNamesArray);


  combUpperBdds = ALLOC(bdd_node *,numOut);
  /* Initialize the upper bound to be the lower bound */
  for (i = 0; i < numOut; i++) {
    bdd_ref(combUpperBdds[i] = combOutBdds[i]);
  }

  if (fsm) {
    mdd_t *initMdd;
    /* Duplicate copy of initial States is returned */
    initMdd = Fsm_FsmComputeInitialStates(fsm);
    initBdd = (bdd_node *)bdd_extract_node_as_is(initMdd);
    bdd_ref(initBdd);
    mdd_free(initMdd);

    if (synthInfo->unreachDC) {
      mdd_t *reachStates;

      (void) fprintf(vis_stdout,
		     "** synth info: Using unreachable states as dont cares\n");
      if (synthInfo->unreachDC == 1) {
	reachMethod = Fsm_Rch_Bfs_c;
      } else if (synthInfo->unreachDC == 2) {
	reachMethod = Fsm_Rch_Hd_c;
      } else if (synthInfo->unreachDC == 3) {
	reachMethod = Fsm_Rch_Oa_c;
      } else {
	reachMethod = Fsm_Rch_Default_c;
      }
      reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,
						  0,0,1000,reachMethod,
						  0,0,NIL(array_t), FALSE,
						  NIL(array_t));
      reachable = (bdd_node *)bdd_extract_node_as_is(reachStates);
      bdd_ref(reachable);
      unReachable = bdd_not_bdd_node(reachable);
      bdd_ref(unReachable);
      mdd_free(reachStates);
    }
  }

  if (careBddTable == NIL(st_table)) {
    if (fsm && synthInfo->unreachDC) {
      /* Upper bound = LowerBould + DC */
      for (i = 0; i < numOut; i++) {
	bdd_recursive_deref(ddManager,combUpperBdds[i]);
	combUpperBdds[i] = bdd_bdd_or(ddManager,combOutBdds[i],
				      unReachable);
	bdd_ref(combUpperBdds[i]);
      }
      
      /* LowerBound = OutputFuns . Care */
      bdd_recursive_deref(ddManager,unReachable);
      for (i = 0; i < numOut; i++) {
	bdd_node *temp;
	temp = bdd_bdd_and(ddManager,combOutBdds[i],reachable);
	bdd_ref(temp);
	bdd_recursive_deref(ddManager,combOutBdds[i]);
	combOutBdds[i] = temp;
      }
      bdd_recursive_deref(ddManager,reachable);
    }
  } else { /* Use the cares supplied. */
    if (fsm && synthInfo->unreachDC) {
      bdd_recursive_deref(ddManager,unReachable);
    }
    for (i = 0; i < numOut; i++) {
      bdd_node *dontCare,*care;

      if (st_lookup(careBddTable,combOutNames[i],&ddTemp) == 1) {
	if (fsm && synthInfo->unreachDC) {
	  bdd_ref(care = bdd_bdd_or(ddManager,ddTemp,reachable));
	} else {
	  bdd_ref(care = ddTemp);
	}
	bdd_ref(dontCare = bdd_not_bdd_node(care));
	
	/* Update the upper bound for each combinational output */
	bdd_recursive_deref(ddManager,combUpperBdds[i]);
	combUpperBdds[i] = bdd_bdd_or(ddManager,combOutBdds[i],dontCare);
	bdd_ref(combUpperBdds[i]);
	bdd_recursive_deref(ddManager,dontCare);
	
	/* Update the lower bound */
	bdd_ref(temp = bdd_bdd_and(ddManager,combOutBdds[i],care));
	bdd_recursive_deref(ddManager,combOutBdds[i]);
	bdd_recursive_deref(ddManager,care);
	combOutBdds[i]=temp;
      }
    }
  }

  if (fsm) {
    bdd_t *bddVar, *bddTInit, *bddTtemp;
    int id, i = 0;
    lsGen gen;
    Ntk_Node_t *node;
    bdd_node *logicZero = bdd_read_logic_zero(ddManager);

    bddTInit = bdd_construct_bdd_t(ddManager,initBdd);
    initStates = ALLOC(int, Ntk_NetworkReadNumLatches(network));
    Ntk_NetworkForEachLatch(network,gen,node) {
      id = Ntk_NodeReadMddId(node);
      bddVar = bdd_get_variable(ddManager,id);
      bddTtemp = bdd_cofactor(bddTInit, bddVar);
      if (bdd_extract_node_as_is(bddTtemp) == logicZero) 
	initStates[i] = 0;
      else
	initStates[i] = 1;
      i++;
      bdd_free(bddVar);
      bdd_free(bddTtemp);
    }
    /* This will free initBdd too. So, no need to deref it again.  */
    bdd_free(bddTInit);
  }

  SynthMultiLevelOptimize(network,combOutBdds,combUpperBdds,
			  combOutNames, initStates,synthInfo,
			  verbosity);

  /* Clean up. */
  if (fsm) {
    FREE(initStates);
  }
  for (i = 0; i < numOut; i++) {
    bdd_recursive_deref(ddManager,combUpperBdds[i]);
    bdd_recursive_deref(ddManager,combOutBdds[i]);
  }
  FREE(combOutNames);
  FREE(combOutBdds);
  FREE(combUpperBdds);
  array_free(inputIds);
  if (realign_zdd == 1)
    bdd_zdd_realign_enable(ddManager);
  else
    bdd_zdd_realign_disable(ddManager);
  if (realign_bdd == 1)
    bdd_realign_enable(ddManager);
  else
    bdd_realign_disable(ddManager);
  return(1);
}

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

  Synopsis    [Checks whether partition is valid.]

  Description [Checks whether partition is valid. The condition is that the
  given partition should have a vertex for each combinational output (PO and
  NS) and combinational input (PI and PS) of the network. This is necessary to
  completely synthesize the network.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static int
IsPartitionValid(Ntk_Network_t *network,
		 graph_t *partition)
{
  Ntk_Node_t *node;
  lsGen gen;
  char *name;

  Ntk_NetworkForEachCombOutput(network, gen, node) {
    name = Ntk_NodeReadName(node);
    if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) {
      return(0);
    }
  }
  Ntk_NetworkForEachCombInput(network, gen, node) {
    name = Ntk_NodeReadName(node);
    if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) {
      return(0);
    }
  }

  return 1;
}


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

  Synopsis    [Returns an array containing all combinational output names.]

  Description [Returns an array containing all combinational output names.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static array_t *
GetCombOutputNameArray(Ntk_Network_t *network)
{
  array_t *outputFunNames;
  lsGen gen;
  Ntk_Node_t *node;
    
  outputFunNames = array_alloc(char *, 0);
  if (outputFunNames == NIL(array_t)) {
    (void) fprintf(vis_stderr,"** synth error: Could not allocate space ");
    (void) fprintf(vis_stderr,"for the names of combinational outputs\n");
    return NIL(array_t);
  }
  Ntk_NetworkForEachCombOutput(network, gen, node){
    if (Ntk_NodeTestIsLatchInitialInput(node))
      continue;
    array_insert_last(char *, outputFunNames, 
		      Ntk_NodeReadName(node));
  }
  return outputFunNames;
}

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

  Synopsis    [Returns an array containing mdd-ids of all combinational inputs.]

  Description [Returns an array containing mdd-ids of all combinational inputs.]

  SideEffects []

  SeeAlso []

******************************************************************************/
static array_t *
GetCombInputIdArray(Ntk_Network_t *network)
{
  array_t *inputIds;
  lsGen gen;
  Ntk_Node_t *node;
    
  inputIds = array_alloc(int, 0);
  if (inputIds == NIL(array_t)) {
    (void) fprintf(vis_stderr,"** synth error: Could not allocate space ");
    (void) fprintf(vis_stderr,"for an array of ids of comb. inputs\n");
    return NIL(array_t);
  }
  Ntk_NetworkForEachCombInput(network, gen, node){
    array_insert_last(int, inputIds, Ntk_NodeReadMddId(node));
  }
  return inputIds;
}


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

  Synopsis    [Returns array of bdds of combinational outputs.]

  Description [Returns array of bdds of combinational outputs.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static bdd_node **
GetBddArray(Mvf_Function_t *combMvfs)
{
  bdd_node **bddArray;
  Mvf_Function_t *mvf;
  int i;

  bddArray = ALLOC(bdd_node *,array_n(combMvfs));
  if (bddArray == NIL(bdd_node *)) {
    (void) fprintf(vis_stderr,"** synth error: Could not allocate space ");
    (void) fprintf(vis_stderr,"for an array of Bdd nodes.\n");
    return NIL(bdd_node *);
  }
  arrayForEachItem(Mvf_Function_t *, combMvfs, i, mvf) {
    mdd_t *mddTemp;

    mddTemp = array_fetch(mdd_t *, mvf, 1);
    bddArray[i] = (bdd_node *) bdd_extract_node_as_is(mddTemp);
    bdd_ref(bddArray[i]);
  }
  return bddArray;
}