VIS
|
#include "synthInt.h"
Go to the source code of this file.
Functions | |
static int | CommandSynthesizeNetwork (Hrc_Manager_t **hmgr, int argc, char **argv) |
static void | TimeOutHandle (void) |
static int | TestIsNetworkMultipleValued (Ntk_Network_t *network) |
void | Synth_Init (void) |
void | Synth_End (void) |
Variables | |
static char rcsid[] | UNUSED = "$Id: synth.c,v 1.60 2005/05/16 06:22:00 fabio Exp $" |
int | VerifyTreeMode |
static jmp_buf | timeOutEnv |
static int CommandSynthesizeNetwork | ( | Hrc_Manager_t ** | hmgr, |
int | argc, | ||
char ** | argv | ||
) | [static] |
AutomaticStart
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 <divisor>\] \[-e\] \[-f <factoringMethod>\] \[-h\] \[-i <prefix>\] \[-o <fileHead>\] \[-r <reachMethod>\] \[-t <timeOut>\] \[-v\] \[-A\] \[-O <outputOrdering>\] \[-R <reorder>\] \[-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.
Command options:
Choose a divisor.
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.
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.
2 : Most occuring literal divisor. If a variable occurs the most frequently in cubes, it returns the variable as a divisor.
3 : Level-0 divisor. It finds a divisor that is a level-0 cokernel.
Dump the synthesized circuit in equation format also. Default is not to.
Choose a factoring method.
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.
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.
Print the command usage.
Specify the prefix of internal node names. By default, the prefix is "_n".
Specify the output file name (without extension). By default, the model name in a blif file is used.
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:
0 : Do not use dont cares (default).
1 : Use normal breadth first search method for reachability analysis.
2 : Use high density traversal method for reachablity analysis.
3 : Use approximate unreachable states(a subset of actual unreachable states) as dont cares.
Time in seconds allowed to perform synthesize_network. The default is no limit.
Print debug information.
Allow realignment to ZDD/BDD after BDD/ZDD reordering, respectively. This option is effective when only one reordering in BDD or ZDD is enabled.
Choose an output ordering method.
0 : No ordering.
1 : (default) Use support variable set of output functions.
2 : Use BDD size of output functions.
Allow reordering in BDD and/or ZDD.
0 or n : (default) No reordering neither in BDD nor in ZDD.
1 or b : Allows reordering only in BDD, not in ZDD.
2 or z : Allows reordering only in ZDD, not in BDD.
3 or a : Allows reordering both in BDD and in ZDD.
Try to share more nodes during symbolic factorization. Existing divisors are checked for potential reuse before extracting divisors from the current boolean function.
<> ]
Definition at line 275 of file synth.c.
{ 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 */ }
void Synth_End | ( | void | ) |
Function********************************************************************
Synopsis [This function ends the synth package.]
Description [This function ends the synth package.]
SideEffects [none]
SeeAlso [Synth_Init()]
Definition at line 107 of file synth.c.
{ }
void Synth_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [This function initializes the synth package.]
Description [This function initializes the synth package.]
SideEffects [Installs the synthesize_network command.]
SeeAlso [Synth_End()]
Definition at line 90 of file synth.c.
{ Cmd_CommandAdd("synthesize_network", CommandSynthesizeNetwork, 0); }
static int TestIsNetworkMultipleValued | ( | Ntk_Network_t * | network | ) | [static] |
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 []
Definition at line 666 of file synth.c.
{ 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; }
static void TimeOutHandle | ( | void | ) | [static] |
Function********************************************************************
Synopsis [Handler for timeout.]
Description [This function is called when a time out occurs.]
SideEffects []
SeeAlso []
Definition at line 647 of file synth.c.
{ longjmp(timeOutEnv, 1); }
jmp_buf timeOutEnv [static] |
char rcsid [] UNUSED = "$Id: synth.c,v 1.60 2005/05/16 06:22:00 fabio Exp $" [static] |
CFile***********************************************************************
FileName [synth.c]
PackageName [synth]
Synopsis [Commands for synthesize_network.]
Description [External procedures included in this module:
Static procedures included in this module:
]
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.]
int VerifyTreeMode |
Definition at line 73 of file synthFactor.c.