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

  FileName    [synth.c]

  PackageName [synth]

  Synopsis    [Commands for synthesize_network.]

  Description [External procedures included in this module:
		<ul>
		<li> Synth_Init()
		<li> Synth_End()
		</ul>
	Static procedures included in this module:
		<ul>
		<li> CommandSynthesizeNetwork()
		<li> TimeOutHandle()
		</ul> ]

  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: synth.c,v 1.60 2005/05/16 06:22:00 fabio Exp $";

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


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


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


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

extern	int		VerifyTreeMode;

static	jmp_buf		timeOutEnv;

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


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

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

static int CommandSynthesizeNetwork(Hrc_Manager_t **hmgr, int argc, char **argv);
static void TimeOutHandle(void);
static int TestIsNetworkMultipleValued(Ntk_Network_t *network);

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


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

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

  Synopsis    [This function initializes the synth package.]

  Description [This function initializes the synth package.]

  SideEffects [Installs the synthesize_network command.]

  SeeAlso     [Synth_End()]

******************************************************************************/
void
Synth_Init(void)
{
  Cmd_CommandAdd("synthesize_network", CommandSynthesizeNetwork, 0);
}

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

  Synopsis    [This function ends the synth package.]

  Description [This function ends the synth package.]

  SideEffects [none]

  SeeAlso     [Synth_Init()]

******************************************************************************/
void
Synth_End(void)
{
}

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

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

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

  Synopsis [Implements the synthesize_network command.]

  Description [This function synthesizes a network to have as few
  literals as possible and outputs a blif file and an equation file.
  Those files are the results of the synthesis. By default, the names
  of the files are model_name.ml.blif and model_name.eq unless users
  specify the model_name explicitly using -o option. But, when the
  output blif file is read in sis, it may have slightly different
  number of literals. This problem will be fixed in the later version.
  Currently, this command can be used only with CUDD package.

  Designs described in BLIF or BLIF-MV format can be synthesized by
  this command. However, multiple valued variables are not
  supported. Hence, signals in the designs described in BLIF-MV need
  to be restricted to binary values.]

  SideEffects [None]

  SeeAlso []

  CommandName [synthesize_network]

  CommandSynopsis [Synthesizes a network using ZDD factorization method.]

  CommandArguments [\[-d &lt;divisor&gt;\] \[-e\] \[-f &lt;factoringMethod&gt;\]
  \[-h\] \[-i &lt;prefix&gt;\] \[-o &lt;fileHead&gt;\]
  \[-r &lt;reachMethod&gt;\]
  \[-t &lt;timeOut&gt;\] \[-v\] \[-A\] \[-O &lt;outputOrdering&gt;\]
  \[-R &lt;reorder&gt;\] \[-T\]]

  CommandDescription [This command synthesizes a network to have as few
  literals as possible and outputs a blif file and an equation file.  Those
  files are the results of the synthesis. By default, the names of the files
  are model_name.ml.blif and model_name.eq unless users specify the model_name
  explicitly using -o option. But, when the output blif file is read in sis, it
  may have slightly different number of literals. This problem will be fixed in
  the later version.  Currently, this command can be used only with CUDD
  package.

  Designs described in BLIF or BLIF-MV format can be synthesized by this
  command. However, multiple valued variables are not supported. Hence, signals
  in the designs described in BLIF-MV need to be restricted to binary values.

  There are 4 divisor functions to find a good divisor of a function. Neither
  of them consistently generates the best result. And, there are 2 factoring
  methods: simple factoring and generic factoring. Also, neither of two always
  does better than the other.  <p>

  Command options:<p>

  <dl>

  <dt> -d &lt;divisor&gt;
  <dd> Choose a divisor.<p>
  <dd>
  0 : Fast divisor. We find a divisor on a ZDD graph. As soon as any
  shared node(variable) is found, the variable is returned as a divisor.
  <p>

  1 : (default) Least occuring literal divisor. If a variable occurs the least
  frequently(but, should be more than one) in cubes, it returns the
  variable as a divisor. <p>

  2 : Most occuring literal divisor. If a variable occurs the most frequently
  in cubes, it returns the variable as a divisor. <p>

  3 : Level-0 divisor. It finds a divisor that is a level-0 cokernel.
  <p>

  <dt> -e
  <dd> Dump the synthesized circuit in equation format also. Default is 
  not to.  <p>

  <dt> -f &lt;factoringMethod&gt;
  <dd> Choose a factoring method.<p>
  <dd>
  0 : (default) Simple factoring. This method uses a simple recursion. First,
  it finds a proper divisor of a function, then divide the function by the
  divisor, then it gets a quotient and a remainder. And, it does the
  same thing recursively for each divisor, quotient, and
  remainder. <p>

  1 : Generic factoring. This method is quite similar to the simple
  factoring, but it does more in terms of considering cube-free and
  common divisor and literal factoring. But, it does not always generate
  better results than the simple factoring does. <p>

  <dt> -h
  <dd> Print the command usage. <p>

  <dt> -i &lt;prefix&gt;
  <dd> Specify the prefix of internal node names. By default, the prefix
  is "_n". <p>

  <dt> -o &lt;fileHead&gt;
  <dd> Specify the output file name (without extension). By default, the model
  name in a blif file is used. <p>

  <dt> -r &lt;reachMethod&gt;
  <dd> If the network is sequential, then use unreachable states as dont cares
  in the optimization. By default no reachability analysis is performed. See
  -A option of command compute_reach for more details. The various options
  are:<p>
  <dd>
  0 : Do not use dont cares (default). <p>

  1 : Use normal breadth first search method for reachability analysis. <p>

  2 : Use high density traversal method for reachablity analysis. <p>

  3 : Use approximate unreachable states(a subset of actual unreachable states)
  as dont cares. <p>

  <dt> -t &lt;timeOut&gt;
  <dd> Time in seconds allowed to perform synthesize_network.  The default is
  no limit.<p>

  <dt> -v
  <dd> Print debug information. <p>

  <dt> -A
  <dd> Allow realignment to ZDD/BDD after BDD/ZDD reordering, respectively.
  This option is effective when only one reordering in BDD or ZDD is enabled.

  <dt> -O &lt;outputOrdering&gt;
  <dd> Choose an output ordering method. <p>
  <dd>
  0 : No ordering. <p>

  1 : (default) Use support variable set of output functions. <p>

  2 : Use BDD size of output functions. <p>

  <dt> -R &lt;reorder&gt;
  <dd> Allow reordering in BDD and/or ZDD. <p>
  <dd>
  0 or n : (default) No reordering neither in BDD nor in ZDD. <p>

  1 or b : Allows reordering only in BDD, not in ZDD. <p>

  2 or z : Allows reordering only in ZDD, not in BDD. <p>

  3 or a : Allows reordering both in BDD and in ZDD. <p>

  <dt> -T
  <dd> Try to share more nodes during symbolic factorization. Existing
  divisors are checked for potential reuse before extracting divisors from the
  current boolean function.<p>

  <\dl>
  ]

******************************************************************************/
static int
CommandSynthesizeNetwork(Hrc_Manager_t **hmgr,
			 int argc,
			 char **argv)
{
  Ntk_Network_t *network1;
  Ntk_Node_t *node;
  bdd_manager *ddManager;
  int timeOutPeriod;
  int createdMgr;
  int factoring, divisor;
  int unreachDC, verbosity;
  int result, varOrdered;
  long initialTime, finalTime;
  char *filehead,*filename;
  char *prefix;
  FILE *fp;
  int c;
  lsList dummy = (lsList) 0;
  lsGen gen;
  Synth_InfoData_t *synthInfo;
  char *reorder = NIL(char);
  int reordering;
  int trySharing;
  int realign;
  int outputOrdering;
  boolean eqn;

  if (bdd_get_package_name() != CUDD) {
    (void) fprintf(vis_stderr,
 "** synth error: synthesize_network can be used only with the CUDD package\n");
    (void) fprintf(vis_stderr,
		   "** synth error: Please link with CUDD package\n");
    return 1;
  }

  /* To keep the Alpha compilers happy. */
  network1 = NIL(Ntk_Network_t);
  node = NIL(Ntk_Node_t);
  ddManager = NIL(bdd_manager);
  synthInfo = NIL(Synth_InfoData_t);

  /* These are the default values. */
  timeOutPeriod   = 0;
  createdMgr      = 0;
  factoring       = 0; /* Simple factoring algorithm. */
  divisor         = 1; /* Quick divisor */
  unreachDC       = 0; /* Do not use unreachable states as DCs */
  filehead        = NIL(char);
  filename        = NIL(char);
  prefix          = NIL(char);
  fp              = NIL(FILE);
  reordering      = 0;
  trySharing      = 0;
  realign         = 0;
  verbosity       = 0;
  varOrdered      = 0;
  outputOrdering  = 0;
  eqn             = 0;
  util_getopt_reset();

  while((c = util_getopt(argc, argv, "d:ef:hi:o:r:t:vAO:R:TV:")) != EOF) {
    switch(c) {
    case 'd':
      divisor = atoi(util_optarg);
      if (divisor < 0 || divisor > 3)
	goto usage;
      break;
    case 'e':
      eqn = 1;
      break;
    case 'f':
      factoring = atoi(util_optarg);
      if (factoring < 0 || factoring > 1)
	goto usage;
      break;
    case 'h':
      goto usage;
    case 'i':
      prefix = util_strsav(util_optarg);
      break;
    case 'o':
      filehead = util_strsav(util_optarg);
      break;
    case 'r':
      unreachDC = atoi(util_optarg);
      break;
    case 't':
      timeOutPeriod = atoi(util_optarg);
      break;
    case 'v':
      verbosity = 1;
      break;
    case 'A':
      realign = 1;
      break;
    case 'O':
      outputOrdering = atoi(util_optarg);
      if (outputOrdering < 0 || outputOrdering > 2)
	goto usage;
      SynthSetOutputOrdering(outputOrdering);
      break;
    case 'R':
      reorder = util_strsav(util_optarg);
      if (reorder[0] == '0' || reorder[0] == 'n')
	reordering = 0;
      else if (reorder[0] == '1' || reorder[0] == 'b')
	reordering = 1;
      else if (reorder[0] == '2' || reorder[0] == 'z')
	reordering = 2;
      else if (reorder[0] == '3' || reorder[0] == 'a')
	reordering = 3;
      else
	goto usage;
      break;
    case 'T':
      trySharing = 1;
      break;
    case 'V':
      VerifyTreeMode = atoi(util_optarg);
      break;
    default:
      if (util_optarg)
	(void) fprintf(vis_stderr,
			"** synth error: Unknown option %s\n",util_optarg);
      else
	(void) fprintf(vis_stderr,"** synth error: Unknown option ?\n");
      goto usage;
    }
  }

  if(Hrc_ManagerReadCurrentNode(*hmgr) == NIL(Hrc_Node_t)) {
    (void)fprintf(vis_stderr,"** synth error: The hierarchy manager is empty.");
    (void)fprintf(vis_stderr,"** synth error: Read in design.\n");
    goto endgame;
  }

  network1 = (Ntk_Network_t *) 
    Hrc_NodeReadApplInfo(Hrc_ManagerReadCurrentNode(*hmgr), 
			 NTK_HRC_NODE_APPL_KEY);

  if(network1 == NIL(Ntk_Network_t)) {
    (void) fprintf(vis_stderr, "** synth error: There is no network. ");
    (void) fprintf(vis_stderr,"** synth error:Use flatten_hierarchy.\n");
    goto endgame;
  }

  /* Check if the current network has signals with multiple values. */
  if (TestIsNetworkMultipleValued(network1)) {
    (void) fprintf(vis_stderr,
		   "** synth error: Circuit has multiple valued variables.\n");
    (void) fprintf(vis_stderr,
	"** synth error: This command works with boolean signals only.\n");
    goto endgame;
  }

  if (!filehead)
    filehead = util_strsav(Ntk_NetworkReadName(network1));

  /* Check if the output equation file already exists */
  if (eqn) {
    filename = util_strcat3(filehead,".eq","");
    fp = Cmd_FileOpen(filename,"r",NIL(char *),1);
    if (fp) {
      (void) fprintf(vis_stderr,
		"** synth error: Output equation file %s already exists.\n",
		filename);
      (void) fprintf(vis_stderr,
		"** synth error: Please specify another name.\n");
      fclose(fp);
      FREE(filename);
      goto endgame;
    }
    FREE(filename);
  }
  /* Check if the output blif file already exists */
  filename = util_strcat3(filehead,".ml.blif","");
  fp = Cmd_FileOpen(filename,"r",NIL(char *),1);
  if (fp) {
    (void) fprintf(vis_stderr,
		   "** synth error: Output blif file %s already exists.\n",
		   filename);
    (void) fprintf(vis_stderr,"** synth error: Please specify another name.\n");
    fclose(fp);
    FREE(filename);
    goto endgame;
  }
  FREE(filename);

  if(Ntk_NetworkReadNumPrimaryInputs(network1) !=
     Ntk_NetworkReadNumInputs(network1)) {
    (void) fprintf(vis_stderr,
		   "** synth error: Pseudo inputs present in the network.\n");
    (void) fprintf(vis_stderr,
		   "** synth error: Cannot synthesize the network\n");
    goto endgame;
  }

  ddManager = (bdd_manager *) Ntk_NetworkReadMddManager(network1);
  if (ddManager == NIL(bdd_manager)) {
    ddManager = (bdd_manager *)Ntk_NetworkInitializeMddManager(network1);
    if (ddManager == NIL(bdd_manager)) {
      (void) fprintf(vis_stderr,
		     "** synth error: Could not create Mdd Manager\n");
      goto endgame;
    }
    createdMgr = 1;
  }

  /* Check if the network has the variables ordered.
   * For combinational synthesis we are only interested in the primary 
   * input variables. But for sequential synthesis we need primary inputs,
   * present state variables and next state variables (to use in 
   * reachability analysis and use the unreachable states as dont cares).
   */

  if (Ord_NetworkTestAreVariablesOrdered(network1, Ord_InputAndLatch_c) == 
      FALSE) {
    Ord_NetworkOrderVariables(network1,Ord_RootsByDefault_c,
			      Ord_NodesByDefault_c, FALSE,
			      Ord_InputAndLatch_c,Ord_Unassigned_c,
			      dummy,0);
    varOrdered = 1;
  }
    
  /* Start the timer. */
  if (timeOutPeriod > 0){
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stderr, "** synth warning: Timeout occurred after ");
      (void) fprintf(vis_stderr, "%d seconds.\n", timeOutPeriod);
      alarm(0);
      goto endgame;
    }
  }

  synthInfo = Synth_InitializeInfo(factoring,divisor,unreachDC,
				   reordering,trySharing,realign,
				   filehead,prefix,eqn);
  if (!synthInfo)
    goto endgame;

  /* Synthesize.*/
  initialTime = util_cpu_time();

  result = Synth_SynthesizeNetwork(network1,NIL(graph_t), 
				   NIL(st_table),synthInfo,
				   verbosity);

  finalTime = util_cpu_time();

  if (result) {
    (void) fprintf(vis_stdout, "%-20s%10ld\n", "analysis time =",
		   (finalTime-initialTime)/1000);
  } else {
    (void) fprintf(vis_stdout, "** synth error: Could not synthesize.\n");
  }

  /* Set the mdd id's for all the nodes to unassigned if it
   * was specifically set in this routine.
   */
  if (varOrdered) {
    Ntk_NetworkForEachPrimaryInput(network1,gen,node) {
      Ntk_NodeSetMddId(node,NTK_UNASSIGNED_MDD_ID);
    }
    Ntk_NetworkForEachLatch(network1,gen,node) {
      Ntk_Node_t *shadow;
      shadow = Ntk_NodeReadShadow(node);
      Ntk_NodeSetMddId(node,NTK_UNASSIGNED_MDD_ID);    
      Ntk_NodeSetMddId(shadow,NTK_UNASSIGNED_MDD_ID);    
    }
  }

  if (createdMgr) {
    mdd_quit((mdd_manager *)ddManager);
    Ntk_NetworkSetMddManager(network1,NIL(mdd_manager));
  }

  if (reorder)
    FREE(reorder);
  if (filehead)
    FREE(filehead);
  if (prefix)
    FREE(prefix);

  if (synthInfo)
    Synth_FreeInfo(synthInfo);

  alarm(0);
  return 0;  /* normal exit */

 endgame:
  if (varOrdered) {
    Ntk_NetworkForEachNode(network1,gen,node) {
      Ntk_NodeSetMddId(node,NTK_UNASSIGNED_MDD_ID);
    }
  }

  if (createdMgr) {
    mdd_quit((mdd_manager *)ddManager);
    Ntk_NetworkSetMddManager(network1,NIL(mdd_manager));
  }

  if (reorder)
    FREE(reorder);
  if(filehead)
    FREE(filehead);
  if(prefix)
    FREE(prefix);

  if (synthInfo)
    Synth_FreeInfo(synthInfo);

  return 1;

 usage:
  (void) fprintf(vis_stderr, "usage: synthesize_network [-d divisor] [-e] [-f factoringMethod] [-h] [-i prefix] [-o fileHead] [-r reachMethod] [-t timeOut] [-v] [-A] [-O outputOrdering] [-R reorder] [-T]\n");
  (void) fprintf(vis_stderr, "   -d n\t\tChoose a divisor function (0-4)\n");
  (void) fprintf(vis_stderr, "   \t\t\t0: Fast divisor\n");
  (void) fprintf(vis_stderr,
		 "   \t\t\t1: Least occuring literal divisor (default)\n");
  (void) fprintf(vis_stderr, "   \t\t\t2: Most occuring literal divisor\n");
  (void) fprintf(vis_stderr, "   \t\t\t3: Level-0 kernel divisor\n");
  (void) fprintf(vis_stderr, "   -e n\t\tOutput equation format file\n");
  (void) fprintf(vis_stderr, "   -f n\t\tChoose a factoring method(0-1)\n");
  (void) fprintf(vis_stderr, "   \t\t\t0: Simple factoring (default)\n");
  (void) fprintf(vis_stderr, "   \t\t\t1: Generic factoring\n");
  (void) fprintf(vis_stderr, "   -h\t\tPrint the command usage\n");
  (void) fprintf(vis_stderr, "   -i prefix\tPrefix of internal node names.\n");
  (void) fprintf(vis_stderr,
		 "   -o name\tName of output file (without extension)\n");
  (void) fprintf(vis_stderr,
		 "   -r n\t\tUse unreachable states for sequential circuits\n");
  (void) fprintf(vis_stderr, "   \t\tas dont cares(0-3)\n");
  (void) fprintf(vis_stderr,
	 "   \t\t\t0: Do not use unreachable states (default).\n");
  (void) fprintf(vis_stderr,
	 "   \t\t\t1: Use normal BFS method for reachability analysis.\n");
  (void) fprintf(vis_stderr,
	 "   \t\t\t2: Use high density method for reachability analysis.\n");
  (void) fprintf(vis_stderr,
	 "   \t\t\t3: Use approximate unreachable states as dont cares.\n");
  (void) fprintf(vis_stderr, "   -t time\tTime out period (in seconds)\n");
  (void) fprintf(vis_stderr, "   -v \t\tVerbosity On.\n");
  (void) fprintf(vis_stderr,
		 "   -A \t\tAllow realignment after BDD/ZDD reordering.\n");
  (void) fprintf(vis_stderr,
		 "   -O n\t\tChoose an output ordering method(0-2)\n");
  (void) fprintf(vis_stderr, "   \t\t\t0: no ordering\n");
  (void) fprintf(vis_stderr, "   \t\t\t1: support variable set (default)\n");
  (void) fprintf(vis_stderr, "   \t\t\t2: BDD size\n");
  (void) fprintf(vis_stderr, "   -R n\t\tSet reordering (0-3)\n");
  (void) fprintf(vis_stderr, "   \t\t\t0 or n: no reordering (default)\n");
  (void) fprintf(vis_stderr, "   \t\t\t1 or b: reordering in only BDD\n");
  (void) fprintf(vis_stderr, "   \t\t\t2 or z: reordering on only ZDD\n");
  (void) fprintf(vis_stderr, "   \t\t\t3 or a: reordering on both\n");
  (void) fprintf(vis_stderr, "   -T \t\tTry to share mode nodes.\n");
  return 1;    /* error exit */
}

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

  Synopsis    [Handler for timeout.]

  Description [This function is called when a time out occurs.]

  SideEffects []

  SeeAlso []

******************************************************************************/
static void
TimeOutHandle(void)
{
  longjmp(timeOutEnv, 1);
}


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

  Synopsis    [Checks whether the network has multiple valued signals.]

  Description [Checks whether the network has multiple valued
  signals. Returns 1 if true, else 0.]

  SideEffects [None]

  SeeAlso []

******************************************************************************/
static int
TestIsNetworkMultipleValued(Ntk_Network_t *network)
{
  Ntk_Node_t *node;
  lsGen gen;
  Var_Variable_t *var;
  int numValues;

  Ntk_NetworkForEachNode(network,gen,node) {
    var = Ntk_NodeReadVariable(node);
    numValues = Var_VariableReadNumValues(var);
    if (numValues > 2) {
      lsFinish(gen);
      return 1;
    }
  }
  return 0;
}