summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c561
-rw-r--r--src/base/abci/abcAuto.c2
-rw-r--r--src/base/abci/abcCas.c2
-rw-r--r--src/base/abci/abcCascade.c2
-rw-r--r--src/base/abci/abcCollapse.c18
-rw-r--r--src/base/abci/abcDsd.c2
-rw-r--r--src/base/abci/abcExact.c4
-rw-r--r--src/base/abci/abcGen.c49
-rw-r--r--src/base/abci/abcIvy.c2
-rw-r--r--src/base/abci/abcLutmin.c2
-rw-r--r--src/base/abci/abcNpn.c6
-rw-r--r--src/base/abci/abcNtbdd.c5
-rw-r--r--src/base/abci/abcProve.c2
-rw-r--r--src/base/abci/abcReach.c2
-rw-r--r--src/base/abci/abcSymm.c2
-rw-r--r--src/base/abci/abcUnate.c2
-rw-r--r--src/base/abci/abcUnreach.c2
17 files changed, 601 insertions, 64 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0e527058..181ca54a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -86,6 +86,7 @@ static int Abc_CommandPrintMffc ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintMint ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSymms ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintUnate ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintAuto ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -154,6 +155,7 @@ static int Abc_CommandTwoExact ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandLutExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAllExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTestExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMajGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -184,6 +186,7 @@ static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandReach ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCof ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTopAnd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTrim ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -314,6 +317,8 @@ static int Abc_CommandInsWin ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandPermute ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnpermute ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCubeEnum ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPathEnum ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFunEnum ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -775,6 +780,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Printing", "print_factor", Abc_CommandPrintFactor, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_level", Abc_CommandPrintLevel, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_supp", Abc_CommandPrintSupport, 0 );
+ Cmd_CommandAdd( pAbc, "Printing", "print_mint", Abc_CommandPrintMint, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_symm", Abc_CommandPrintSymms, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_unate", Abc_CommandPrintUnate, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_auto", Abc_CommandPrintAuto, 0 );
@@ -844,6 +850,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Exact synthesis", "lutexact", Abc_CommandLutExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "allexact", Abc_CommandAllExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "testexact", Abc_CommandTestExact, 0 );
+ Cmd_CommandAdd( pAbc, "Exact synthesis", "majgen", Abc_CommandMajGen, 0 );
Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 );
Cmd_CommandAdd( pAbc, "Various", "comb", Abc_CommandComb, 1 );
@@ -874,8 +881,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "reach", Abc_CommandReach, 0 );
Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 );
Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 );
+ Cmd_CommandAdd( pAbc, "Various", "cof", Abc_CommandCof, 1 );
Cmd_CommandAdd( pAbc, "Various", "topmost", Abc_CommandTopmost, 1 );
- Cmd_CommandAdd( pAbc, "Various", "topand", Abc_CommandTopAnd, 1 );
+ Cmd_CommandAdd( pAbc, "Various", "topand", Abc_CommandTopAnd, 1 );
Cmd_CommandAdd( pAbc, "Various", "trim", Abc_CommandTrim, 1 );
Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 );
Cmd_CommandAdd( pAbc, "Various", "move_names", Abc_CommandMoveNames, 0 );
@@ -999,6 +1007,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "permute", Abc_CommandPermute, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "unpermute", Abc_CommandUnpermute, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "cubeenum", Abc_CommandCubeEnum, 0 );
+ Cmd_CommandAdd( pAbc, "Sequential", "pathenum", Abc_CommandPathEnum, 0 );
+ Cmd_CommandAdd( pAbc, "Sequential", "funenum", Abc_CommandFunEnum, 0 );
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 );
@@ -2013,6 +2023,68 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandPrintMint( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+ Abc_Obj_t * pObj;
+ int c;
+ int fVerbose;
+
+ // set defaults
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "svwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( -1, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsStrash(pNtk) )
+ {
+ Abc_Print( -1, "This command works only for logic networks (run \"clp\").\n" );
+ return 1;
+ }
+ if ( !Abc_NtkHasBdd(pNtk) )
+ {
+ Abc_Print( -1, "This command works only for logic networks with local functions represented by BDDs.\n" );
+ return 1;
+ }
+ Abc_NtkForEachNode( pNtk, pObj, c )
+ printf( "ObjId %3d : SuppSize = %5d MintCount = %32.0f\n", c, Abc_ObjFaninNum(pObj),
+ Cudd_CountMinterm((DdManager *)pNtk->pManFunc, (DdNode *)pObj->pData, Abc_ObjFaninNum(pObj)) );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: print_mint [-svwh]\n" );
+ Abc_Print( -2, "\t prints the number of on-set minterms in the PO functions\n" );
+ Abc_Print( -2, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
@@ -2991,15 +3063,22 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
Abc_Obj_t * pNode;
- int c;
- extern void Abc_NodeShowBdd( Abc_Obj_t * pNode );
+ int c, fCompl = 0, fGlobal = 0;
+ extern void Abc_NodeShowBdd( Abc_Obj_t * pNode, int fCompl );
+ extern void Abc_NtkShowBdd( Abc_Ntk_t * pNtk, int fCompl );
// set defaults
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "cgh" ) ) != EOF )
{
switch ( c )
{
+ case 'c':
+ fCompl ^= 1;
+ break;
+ case 'g':
+ fGlobal ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -3013,12 +3092,20 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
+ if ( fGlobal )
+ {
+ Abc_Ntk_t * pTemp = Abc_NtkIsStrash(pNtk) ? pNtk : Abc_NtkStrash(pNtk, 0, 0, 0);
+ Abc_NtkShowBdd( pTemp, fCompl );
+ if ( pTemp != pNtk )
+ Abc_NtkDelete( pTemp );
+ return 0;
+ }
+
if ( !Abc_NtkIsBddLogic(pNtk) )
{
Abc_Print( -1, "Visualizing BDDs can only be done for logic BDD networks (run \"bdd\").\n" );
return 1;
}
-
if ( argc > globalUtilOptind + 1 )
{
Abc_Print( -1, "Wrong number of auguments.\n" );
@@ -3042,17 +3129,20 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
}
- Abc_NodeShowBdd( pNode );
+ Abc_NodeShowBdd( pNode, fCompl );
return 0;
usage:
- Abc_Print( -2, "usage: show_bdd [-h] <node>\n" );
- Abc_Print( -2, " visualizes the BDD of a node using DOT and GSVIEW\n" );
+ Abc_Print( -2, "usage: show_bdd [-cgh] <node>\n" );
+ Abc_Print( -2, " uses DOT and GSVIEW to visualize the global BDDs of primary outputs\n" );
+ Abc_Print( -2, " in terms of primary inputs or the local BDD of a node in terms of its fanins\n" );
#ifdef WIN32
Abc_Print( -2, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
Abc_Print( -2, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
#endif
- Abc_Print( -2, "\t<node>: the node to consider [default = the driver of the first PO]\n");
+ Abc_Print( -2, "\t<node>: (optional) the node to consider [default = the driver of the first PO]\n");
+ Abc_Print( -2, "\t-c : toggle visualizing BDD with complemented edges [default = %s].\n", fCompl? "yes": "no" );
+ Abc_Print( -2, "\t-g : toggle visualizing the global BDDs of primary outputs [default = %s].\n", fGlobal? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -3173,16 +3263,18 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
int fBddSizeMax;
int fDualRail;
int fReorder;
+ int fReverse;
int c;
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
fVerbose = 0;
fReorder = 1;
+ fReverse = 0;
fDualRail = 0;
fBddSizeMax = ABC_INFINITY;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Brdvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Brodvh" ) ) != EOF )
{
switch ( c )
{
@@ -3197,15 +3289,18 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fBddSizeMax < 0 )
goto usage;
break;
+ case 'r':
+ fReorder ^= 1;
+ break;
+ case 'o':
+ fReverse ^= 1;
+ break;
case 'd':
fDualRail ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
- case 'r':
- fReorder ^= 1;
- break;
case 'h':
goto usage;
default:
@@ -3227,11 +3322,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
if ( Abc_NtkIsStrash(pNtk) )
- pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
+ pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fVerbose );
else
{
pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
- pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
+ pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fVerbose );
Abc_NtkDelete( pNtk );
}
if ( pNtkRes == NULL )
@@ -3244,10 +3339,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: collapse [-B <num>] [-rdvh]\n" );
+ Abc_Print( -2, "usage: collapse [-B <num>] [-rodvh]\n" );
Abc_Print( -2, "\t collapses the network by constructing global BDDs\n" );
Abc_Print( -2, "\t-B <num>: limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax );
Abc_Print( -2, "\t-r : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
+ Abc_Print( -2, "\t-o : toggles reverse variable ordering [default = %s]\n", fReverse? "yes": "no" );
Abc_Print( -2, "\t-d : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" );
Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -8217,7 +8313,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "INaogvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "INTaogvh" ) ) != EOF )
{
switch ( c )
{
@@ -8243,6 +8339,17 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nNodes < 0 )
goto usage;
break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->RuntimeLim = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->RuntimeLim < 0 )
+ goto usage;
+ break;
case 'a':
pPars->fOnlyAnd ^= 1;
break;
@@ -8290,10 +8397,11 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: twoexact [-IN <num>] [-aogvh] <hex>\n" );
+ Abc_Print( -2, "usage: twoexact [-INT <num>] [-aogvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" );
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
- Abc_Print( -2, "\t-N <num> : the number of MAJ3 nodes [default = %d]\n", pPars->nNodes );
+ Abc_Print( -2, "\t-N <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes );
+ Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" );
Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" );
@@ -8329,7 +8437,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "INKiaogvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "INKTiaogvh" ) ) != EOF )
{
switch ( c )
{
@@ -8366,6 +8474,17 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nLutSize < 0 )
goto usage;
break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->RuntimeLim = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->RuntimeLim < 0 )
+ goto usage;
+ break;
case 'i':
pPars->fUseIncr ^= 1;
break;
@@ -8421,11 +8540,12 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: lutexact [-INK <num>] [-iaogvh] <hex>\n" );
+ Abc_Print( -2, "usage: lutexact [-INKT <num>] [-iaogvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" );
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
Abc_Print( -2, "\t-N <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes );
Abc_Print( -2, "\t-K <num> : the number of node fanins [default = %d]\n", pPars->nLutSize );
+ Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" );
Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" );
@@ -8681,6 +8801,62 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandMajGen( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern int Gem_Enumerate( int nVars, int fDump, int fVerbose );
+ int c, nVars = 8, fDump = 0, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Ndvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nVars = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nVars < 0 )
+ goto usage;
+ break;
+ case 'd':
+ fDump ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ Gem_Enumerate( nVars, fDump, fVerbose );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: majgen [-N <num>] [-dvh]>\n" );
+ Abc_Print( -2, "\t generates networks for majority gates\n" );
+ Abc_Print( -2, "\t-N <num> : the maximum number of variables [default = %d]\n", nVars );
+ Abc_Print( -2, "\t-d : toggle dumping functions into a file [default = %s]\n", fVerbose ? "yes" : "no" );
+ Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
@@ -11067,6 +11243,81 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandCof( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pNode;
+ int c, Const;
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ // set defaults
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ Abc_Print( -1, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ Abc_Print( -1, "Currently can only be applied to a logic network.\n" );
+ return 1;
+ }
+
+ if ( argc != globalUtilOptind + 2 )
+ {
+ Abc_Print( -1, "Wrong number of auguments.\n" );
+ goto usage;
+ }
+ pNode = Abc_NtkFindCi( pNtk, argv[globalUtilOptind] );
+ if ( pNode == NULL )
+ pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
+ if ( pNode == NULL )
+ {
+ Abc_Print( -1, "Cannot find node \"%s\".\n", argv[globalUtilOptind] );
+ return 1;
+ }
+ Const = atoi( argv[globalUtilOptind+1] );
+ if ( Const != 0 && Const != 1 )
+ {
+ Abc_Print( -1, "Constant should be 0 or 1.\n", argv[globalUtilOptind+1] );
+ return 1;
+ }
+ Abc_ObjReplaceByConstant( pNode, Const );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: cof [-h] <node> <const>\n" );
+ Abc_Print( -2, "\t replaces one node in a logic network by constant 0 or 1\n" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ Abc_Print( -2, "\t<node> : the node to replace\n");
+ Abc_Print( -2, "\t<const> : the constant to replace the node with\n");
+ Abc_Print( -2, "\tname : the node name\n");
+ return 1;
+}
+
/**Function*************************************************************
@@ -12057,9 +12308,11 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c;
int nVars; // the number of variables
+ int nArgs; // the number of arguments
int nLutSize = -1; // the size of LUTs
int nLuts = -1; // the number of LUTs
int fAdder;
+ int fAdderTree;
int fSorter;
int fMesh;
int fMulti;
@@ -12076,10 +12329,13 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars );
extern void Abc_GenOneHot( char * pFileName, int nVars );
extern void Abc_GenRandom( char * pFileName, int nPis );
+ extern void Abc_GenAdderTree( char * pFileName, int nArgs, int nBits );
// set defaults
nVars = 8;
+ nArgs = 8;
fAdder = 0;
+ fAdderTree = 0;
fSorter = 0;
fMesh = 0;
fMulti = 0;
@@ -12088,7 +12344,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
fRandom = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "NKLasemftrvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NAKLabsemftrvh" ) ) != EOF )
{
switch ( c )
{
@@ -12103,6 +12359,17 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nVars < 0 )
goto usage;
break;
+ case 'A':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nArgs = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nArgs < 0 )
+ goto usage;
+ break;
case 'K':
if ( globalUtilOptind >= argc )
{
@@ -12128,6 +12395,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'a':
fAdder ^= 1;
break;
+ case 'b':
+ fAdderTree ^= 1;
+ break;
case 's':
fSorter ^= 1;
break;
@@ -12183,6 +12453,14 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_GenOneHot( FileName, nVars );
else if ( fRandom )
Abc_GenRandom( FileName, nVars );
+ else if ( fAdderTree )
+ {
+ printf( "Generating adder tree with %d arguments and %d bits.\n", nArgs, nVars );
+ Abc_GenAdderTree( FileName, nArgs, nVars );
+ sprintf( Command, "%%read %s; %%blast; &put", FileName );
+ Cmd_CommandExecute( pAbc, Command );
+ return 0;
+ }
else
{
Abc_Print( -1, "Type of circuit is not specified.\n" );
@@ -12194,12 +12472,14 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: gen [-NKL num] [-asemftrvh] <file>\n" );
+ Abc_Print( -2, "usage: gen [-NAKL num] [-asemftrvh] <file>\n" );
Abc_Print( -2, "\t generates simple circuits\n" );
Abc_Print( -2, "\t-N num : the number of variables [default = %d]\n", nVars );
+ Abc_Print( -2, "\t-A num : the number of agruments (for adder tree) [default = %d]\n", nArgs );
Abc_Print( -2, "\t-K num : the LUT size (to be used with switch -f) [default = %d]\n", nLutSize );
Abc_Print( -2, "\t-L num : the LUT count (to be used with switch -f) [default = %d]\n", nLuts );
Abc_Print( -2, "\t-a : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" );
+ Abc_Print( -2, "\t-b : generate an adder tree [default = %s]\n", fAdderTree? "yes": "no" );
Abc_Print( -2, "\t-s : generate a sorter [default = %s]\n", fSorter? "yes": "no" );
Abc_Print( -2, "\t-e : generate a mesh [default = %s]\n", fMesh? "yes": "no" );
Abc_Print( -2, "\t-m : generate a multiplier [default = %s]\n", fMulti? "yes": "no" );
@@ -12871,11 +13151,12 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv )
***********************************************************************/
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ extern void Dau_NetworkEnumTest();
//Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int nCutMax = 1;
int nLeafMax = 4;
int nDivMax = 2;
- int nDecMax = 70;
+ int nDecMax = 3;
int nNumOnes = 4;
int fNewAlgo = 0;
int fNewOrder = 0;
@@ -13029,7 +13310,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
*/
{
// extern void Abc_EnumerateFuncs( int nDecMax, int nDivMax, int fVerbose );
-// Abc_EnumerateFuncs( nDecMax, nDivMax, fVerbose );
+// Abc_EnumerateFuncs( 4, 7, 0 );
}
/*
if ( fNewAlgo )
@@ -13080,7 +13361,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Cba_PrsReadBlifTest();
}
// Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
-// Psl_FileTest();
+ //Dau_NetworkEnumTest();
+ //Ext_TruthDiagnoseTest();
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@@ -22756,6 +23038,183 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandPathEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Abc_EnumerateFrontierTest( int nSize );
+ int c, nSize = 4, fZddAlgo = 0, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Nzvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nSize < 0 )
+ goto usage;
+ break;
+ case 'z':
+ fZddAlgo ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ Abc_Print( -2, "Unknown switch.\n");
+ goto usage;
+ }
+ }
+ Abc_EnumerateFrontierTest( nSize );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: pathenum [-N num] [-vh]\n" );
+ Abc_Print( -2, "\t enumerates self-avoiding paths on the NxN grid\n" );
+ Abc_Print( -2, "\t-N num : the size of the grid to consider [default = %d]\n", nSize );
+// Abc_Print( -2, "\t-z : toggle using ZDD-based algorithm [default = %s]\n", fZddAlgo? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandFunEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerbose );
+ extern void Dau_FunctionEnum( int nInputs, int nVars, int nNodeMax, int fUseTwo, int fReduce, int fVerbose );
+ int c, nInputs = 4, nVars = 4, nNodeMax = 32, fUseTwo = 0, fReduce = 0, fSimple = 0, fDelay = 0, fMulti = 0, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "SIMtrldmvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nInputs = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nInputs < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nVars = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nVars < 0 )
+ goto usage;
+ break;
+ case 'M':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nNodeMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nNodeMax < 0 )
+ goto usage;
+ break;
+ case 't':
+ fUseTwo ^= 1;
+ break;
+ case 'r':
+ fReduce ^= 1;
+ break;
+ case 'l':
+ fSimple ^= 1;
+ break;
+ case 'd':
+ fDelay ^= 1;
+ break;
+ case 'm':
+ fMulti ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ Abc_Print( -2, "Unknown switch.\n");
+ goto usage;
+ }
+ }
+ if ( fSimple || fDelay )
+ {
+ if ( nVars < 3 || nVars > 5 )
+ {
+ Abc_Print( -1, "The number of inputs should be 3 <= I <= 5.\n" );
+ goto usage;
+ }
+ Dtt_EnumerateLf( nVars, nNodeMax, fDelay, fMulti, fVerbose );
+ }
+ else
+ {
+ if ( nVars < 2 || nVars > 6 )
+ {
+ Abc_Print( -1, "The number of inputs should be 2 <= I <= 6.\n" );
+ goto usage;
+ }
+ if ( nInputs < nVars || nInputs > 6 )
+ {
+ Abc_Print( -1, "The intermediate support size should be I <= S <= 6.\n" );
+ goto usage;
+ }
+ Dau_FunctionEnum( nInputs, nVars, nNodeMax, fUseTwo, fReduce, fVerbose );
+ }
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: funenum [-SIM num] [-trldmvh]\n" );
+ Abc_Print( -2, "\t enumerates minimum 2-input-gate implementations\n" );
+ Abc_Print( -2, "\t-S num : the maximum intermediate support size [default = %d]\n", nInputs );
+ Abc_Print( -2, "\t-I num : the number of inputs of Boolean functions [default = %d]\n", nVars );
+ Abc_Print( -2, "\t-M num : the maximum number of 2-input gates [default = %d]\n", nNodeMax );
+ Abc_Print( -2, "\t-t : toggle adding combination of two gates [default = %s]\n", fUseTwo? "yes": "no" );
+ Abc_Print( -2, "\t-r : toggle reducing the last level [default = %s]\n", fReduce? "yes": "no" );
+ Abc_Print( -2, "\t-l : toggle generating L(f) rather than C(f) [default = %s]\n", fSimple? "yes": "no" );
+ Abc_Print( -2, "\t-d : toggle generating D(f) rather than C(f) [default = %s]\n", fDelay? "yes": "no" );
+ Abc_Print( -2, "\t-m : toggle generating multiplicity statistics [default = %s]\n", fMulti? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
@@ -42647,11 +43106,11 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern void Gia_PolynBuild2Test( Gia_Man_t * pGia, int nExtra, int fSigned, int fVerbose, int fVeryVerbose );
- Vec_Int_t * vOrder = NULL;
- int c, nExtra = -1, fOld = 0, fSimple = 1, fSigned = 0, fVerbose = 0, fVeryVerbose = 0;
+ extern void Gia_PolynBuild2Test( Gia_Man_t * pGia, char * pSign, int nExtra, int fSigned, int fVerbose, int fVeryVerbose );
+ Vec_Int_t * vOrder = NULL; char * pSign = NULL;
+ int c, nExtra = 0, fOld = 0, fSimple = 1, fSigned = 0, fVerbose = 0, fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Noasvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NSoasvwh" ) ) != EOF )
{
switch ( c )
{
@@ -42666,6 +43125,15 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nExtra < 0 )
goto usage;
break;
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-S\" should be followed by a char string without spaces.\n" );
+ goto usage;
+ }
+ pSign = argv[globalUtilOptind];
+ globalUtilOptind++;
+ break;
case 'o':
fOld ^= 1;
break;
@@ -42692,6 +43160,11 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" );
return 0;
}
+ if ( argc >= globalUtilOptind + 1 )
+ {
+ printf( "Trailing symbols on the command line (\"%s\").\n", argv[globalUtilOptind] );
+ return 0;
+ }
if ( fOld )
{
vOrder = fSimple ? NULL : Gia_PolynReorder( pAbc->pGia, fVerbose, fVeryVerbose );
@@ -42699,11 +43172,11 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
Vec_IntFreeP( &vOrder );
}
else
- Gia_PolynBuild2Test( pAbc->pGia, nExtra, fSigned, fVerbose, fVeryVerbose );
+ Gia_PolynBuild2Test( pAbc->pGia, pSign, nExtra, fSigned, fVerbose, fVeryVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: &polyn [-N num] [-oasvwh]\n" );
+ Abc_Print( -2, "usage: &polyn [-N num] [-oasvwh] [-S str]\n" );
Abc_Print( -2, "\t derives algebraic polynomial from AIG\n" );
Abc_Print( -2, "\t-N num : the number of additional primary outputs (-1 = unused) [default = %d]\n", nExtra );
Abc_Print( -2, "\t-o : toggles old computation [default = %s]\n", fOld? "yes": "no" );
@@ -42712,6 +43185,18 @@ usage:
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggles printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
+ Abc_Print( -2, "\t\n");
+ Abc_Print( -2, "\t-S str : (optional) the output signature as a character string\n" );
+ Abc_Print( -2, "\t The format used to represent the output signature is very restrictive.\n" );
+ Abc_Print( -2, "\t It should be a string without spaces containing monomials in terms of\n" );
+ Abc_Print( -2, "\t inputs (i<num>) and outputs (o<num>) where <num> is 0-based. Coefficients\n" );
+ Abc_Print( -2, "\t are degrees of two, represented by log2 of their value: for example, \n" );
+ Abc_Print( -2, "\t \"2\" is 2^2 = 4, \"-4\" is -2^4=-16, \"-0\" is -2^0=-1, etc\n" );
+ Abc_Print( -2, "\t Two types of signature are accepted:\n" );
+ Abc_Print( -2, "\t (1) a sequence of monomials without parentheses (for example, \"-2*o0+1*o1+0*o2\")\n" );
+ Abc_Print( -2, "\t (2) a product of two sequences followed by a sum with a sequence\n" );
+ Abc_Print( -2, "\t (for example, \"(4*o0+2*o1+1*o2)*(4*i3+2*i4+1*i5)+(4*o3+2*o4+1*o5)\")\n" );
+ Abc_Print( -2, "\t Here is the signature of a signed 2-bit multiplier: \"(0*o0+1*o1+2*o2-3*o3)\"\n" );
return 1;
}
@@ -43362,6 +43847,16 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has no mapping.\n" );
return 0;
}
+ if ( Gia_ManLutSizeMax(pAbc->pGia) > 6 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current mapping has nodes with more than 6 inputs. Cannot use \"mfs\".\n" );
+ return 0;
+ }
+ if ( pAbc->pGia->pAigExtra && Gia_ManPiNum(pAbc->pGia->pAigExtra) > 6 )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current white-boxes have more than 6 inputs. Cannot use \"mfs\".\n" );
+ return 0;
+ }
pTemp = Gia_ManPerformMfs( pAbc->pGia, pPars );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
@@ -43379,7 +43874,7 @@ usage:
Abc_Print( -2, "\t-d : toggle performing redundancy removal [default = %s]\n", pPars->fRrOnly? "yes": "no" );
Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
Abc_Print( -2, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
- Abc_Print( -2, "\t-b : toggle preserving all while boxes [default = %s]\n", pPars->fAllBoxes? "yes": "no" );
+ Abc_Print( -2, "\t-b : toggle preserving all white boxes [default = %s]\n", pPars->fAllBoxes? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
index 18c92657..8f7eead0 100644
--- a/src/base/abci/abcAuto.c
+++ b/src/base/abci/abcAuto.c
@@ -62,7 +62,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
Abc_Obj_t * pObj;
// compute the global BDDs
- if ( Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, fVerbose) == NULL )
+ if ( Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, 0, fVerbose) == NULL )
return;
// get information about the network
diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c
index 9abdd792..6615bff0 100644
--- a/src/base/abci/abcCas.c
+++ b/src/base/abci/abcCas.c
@@ -70,7 +70,7 @@ Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVer
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
- if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL )
+ if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, 0, fVerbose) == NULL )
return NULL;
if ( fVerbose )
diff --git a/src/base/abci/abcCascade.c b/src/base/abci/abcCascade.c
index 70f2e891..50e66675 100644
--- a/src/base/abci/abcCascade.c
+++ b/src/base/abci/abcCascade.c
@@ -1010,7 +1010,7 @@ Abc_Ntk_t * Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose )
int i;
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkCoNum(pNtk) <= BDD_FUNC_MAX );
- dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddSizeMax, fDropInternal, fReorder, fVerbose );
+ dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddSizeMax, fDropInternal, fReorder, 0, fVerbose );
if ( dd == NULL )
{
Abc_Print( -1, "Construction of global BDDs has failed.\n" );
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index 1542c25a..caeea3a1 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -118,7 +118,7 @@ int Abc_NtkMinimumBase2( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc )
+Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc, int fReverse )
{
Abc_Obj_t * pNodeNew, * pTemp;
int i;
@@ -126,12 +126,12 @@ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode
pNodeNew = Abc_NtkCreateNode( pNtkNew );
// add the fanins in the order, in which they appear in the reordered manager
Abc_NtkForEachCi( pNtkNew, pTemp, i )
- Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, dd->invperm[i]) );
+ Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, fReverse ? Abc_NtkCiNum(pNtkNew)-1-dd->invperm[i] : dd->invperm[i]) );
// transfer the function
pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( (DdNode *)pNodeNew->pData );
return pNodeNew;
}
-Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk, int fReverse )
{
ProgressBar * pProgress;
Abc_Ntk_t * pNtkNew;
@@ -147,7 +147,7 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
assert( Abc_NtkIsStrash(pNtk->pExdc) );
assert( Abc_NtkCoNum(pNtk->pExdc) == 1 );
// compute the global BDDs
- if ( Abc_NtkBuildGlobalBdds(pNtk->pExdc, 10000000, 1, 1, 0) == NULL )
+ if ( Abc_NtkBuildGlobalBdds(pNtk->pExdc, 10000000, 1, 1, 0, 0) == NULL )
return NULL;
// transfer tot the same manager
ddExdc = (DdManager *)Abc_NtkGlobalBddMan( pNtk->pExdc );
@@ -188,21 +188,21 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy );
continue;
}
- pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)Abc_ObjGlobalBdd(pNode) );
+ pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)Abc_ObjGlobalBdd(pNode), fReverse );
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
}
Extra_ProgressBarStop( pProgress );
return pNtkNew;
}
-Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fVerbose )
{
Abc_Ntk_t * pNtkNew;
abctime clk = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
- if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL )
+ if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fReverse, fVerbose) == NULL )
return NULL;
if ( fVerbose )
{
@@ -212,7 +212,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
}
// create the new network
- pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
+ pNtkNew = Abc_NtkFromGlobalBdds( pNtk, fReverse );
Abc_NtkFreeGlobalBdds( pNtk, 1 );
if ( pNtkNew == NULL )
return NULL;
@@ -236,7 +236,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
#else
-Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fVerbose )
{
return NULL;
}
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 4d8f5217..5121a4fc 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -67,7 +67,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, int fVerbose, int fPrint, int fS
DdManager * dd;
Abc_Ntk_t * pNtkNew;
assert( Abc_NtkIsStrash(pNtk) );
- dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
+ dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, 0, fVerbose );
if ( dd == NULL )
return NULL;
if ( fVerbose )
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index 2fbf63dd..b717f5b4 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -2983,8 +2983,8 @@ void Abc_ExactStoreTest( int fVerbose )
Abc_Ntk_t * pNtk;
Abc_Obj_t * pFanins[4];
Vec_Ptr_t * vNames;
- char pPerm[4];
- int Cost;
+ char pPerm[4] = {0};
+ int Cost = 0;
pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
pNtk->pName = Extra_UtilStrsav( "exact" );
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index 26ee3f86..e90040ab 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -821,6 +821,55 @@ void Abc_GenFsm( char * pFileName, int nPis, int nPos, int nStates, int nLines,
Vec_StrFree( vCond );
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_AdderTree( FILE * pFile, int nArgs, int nBits )
+{
+ int i, k, nDigits = Abc_Base10Log( nBits ), Log2 = Abc_Base2Log( nArgs );
+ assert( nArgs > 1 && nBits > 1 );
+ fprintf( pFile, "module adder_tree_%d_%d (\n ", nArgs, nBits );
+ for ( i = 0; i < nBits; i++, fprintf(pFile, "\n ") )
+ for ( k = 0; k < nArgs; k++ )
+ fprintf( pFile, " i%0*d_%0*d,", nDigits, k, nDigits, nBits-1-i );
+ fprintf( pFile, " z\n" );
+ fprintf( pFile, " );\n" );
+ for ( i = 0; i < nBits; i++ )
+ {
+ fprintf( pFile, " input" );
+ for ( k = 0; k < nArgs; k++ )
+ fprintf( pFile, " i%0*d_%0*d%s", nDigits, k, nDigits, nBits-1-i, k==nArgs-1 ? "":"," );
+ fprintf( pFile, ";\n" );
+ }
+ fprintf( pFile, " output [%d:0] z;\n", nBits+Log2-1 );
+ for ( i = 0; i < nArgs; i++ )
+ {
+ fprintf( pFile, " wire [%d:0] t%d = {", nBits-1, i );
+ for ( k = 0; k < nBits; k++ )
+ fprintf( pFile, " i%0*d_%0*d%s", nDigits, i, nDigits, nBits-1-k, k==nBits-1 ? "":"," );
+ fprintf( pFile, " };\n" );
+ }
+ for ( i = 0; i < nArgs-1; i++ )
+ fprintf( pFile, " wire [%d:0] s%d = t%d + %s%d;\n", nBits+Log2-1, i+1, i+1, i ? "s":"t", i );
+ fprintf( pFile, " assign z = s%d;\n", nArgs-1 );
+ fprintf( pFile, "endmodule\n\n" );
+}
+void Abc_GenAdderTree( char * pFileName, int nArgs, int nBits )
+{
+ FILE * pFile = fopen( pFileName, "w" );
+ fprintf( pFile, "// %d-argument %d-bit adder-tree generated by ABC on %s\n", nArgs, nBits, Extra_TimeStamp() );
+ Abc_AdderTree( pFile, nArgs, nBits );
+ fclose( pFile );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 59481d3e..e4a5d3b4 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -600,7 +600,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
fflush( stdout );
}
- pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
+ pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0 );
if ( pNtk )
{
Abc_NtkDelete( pNtkTemp );
diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c
index ad686299..2ac44060 100644
--- a/src/base/abci/abcLutmin.c
+++ b/src/base/abci/abcLutmin.c
@@ -739,7 +739,7 @@ Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fVerbose )
else
pNtkNew = Abc_NtkStrash( pNtkInit, 0, 1, 0 );
// collapse the network
- pNtkNew = Abc_NtkCollapse( pTemp = pNtkNew, 10000, 0, 1, 0 );
+ pNtkNew = Abc_NtkCollapse( pTemp = pNtkNew, 10000, 0, 1, 0, 0 );
Abc_NtkDelete( pTemp );
if ( pNtkNew == NULL )
return NULL;
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
index d2d06924..744b6443 100644
--- a/src/base/abci/abcNpn.c
+++ b/src/base/abci/abcNpn.c
@@ -295,10 +295,6 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
}
else if ( NpnType == 7 )
{
- extern unsigned Abc_TtCanonicizeHie(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int fExact );
- extern Abc_TtHieMan_t * Abc_TtHieManStart( int nVars, int nLevels );
- extern void Abc_TtHieManStop(Abc_TtHieMan_t * p );
-
int fExact = 0;
Abc_TtHieMan_t * pMan = Abc_TtHieManStart( p->nVars, 5 );
for ( i = 0; i < p->nFuncs; i++ )
@@ -318,8 +314,6 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
typedef unsigned(*TtCanonicizeFunc)(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag);
unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag);
unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres);
- Abc_TtHieMan_t * Abc_TtHieManStart(int nVars, int nLevels);
- void Abc_TtHieManStop(Abc_TtHieMan_t * p);
int fHigh = 1, iEnumThres = 25;
Abc_TtHieMan_t * pMan = Abc_TtHieManStart(p->nVars, 5);
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 0225d800..a55ea227 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -254,7 +254,7 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
SeeAlso []
***********************************************************************/
-void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
+void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fReverse, int fVerbose )
{
ProgressBar * pProgress;
Abc_Obj_t * pObj, * pFanin;
@@ -287,8 +287,7 @@ void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInter
Abc_NtkForEachCi( pNtk, pObj, i )
if ( Abc_ObjFanoutNum(pObj) > 0 )
{
- bFunc = dd->vars[i];
-// bFunc = dd->vars[Abc_NtkCiNum(pNtk) - 1 - i];
+ bFunc = fReverse ? dd->vars[Abc_NtkCiNum(pNtk) - 1 - i] : dd->vars[i];
Abc_ObjSetGlobalBdd( pObj, bFunc ); Cudd_Ref( bFunc );
}
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index c31e9d94..03722926 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -201,7 +201,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
fflush( stdout );
}
clk = Abc_Clock();
- pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
+ pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0 );
if ( pNtk )
{
Abc_NtkDelete( pNtkTemp );
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
index 908b16be..bf705dc9 100644
--- a/src/base/abci/abcReach.c
+++ b/src/base/abci/abcReach.c
@@ -271,7 +271,7 @@ void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fP
assert( Abc_ObjFanoutNum(Abc_NtkPo(pNtk,0)) == 0 ); // PO should go first
// compute the global BDDs of the latches
- dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, fVerbose );
+ dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, 0, fVerbose );
if ( dd == NULL )
{
printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c
index 096c3ae4..36a5ee3e 100644
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -99,7 +99,7 @@ void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fReorder, int
// compute the global functions
clk = Abc_Clock();
- dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, fReorder, fVerbose );
+ dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, fReorder, 0, fVerbose );
printf( "Shared BDD size = %d nodes.\n", Abc_NtkSizeOfGlobalBdds(pNtk) );
Cudd_AutodynDisable( dd );
if ( !fGarbCollect )
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
index 63003237..211f1ca3 100644
--- a/src/base/abci/abcUnate.c
+++ b/src/base/abci/abcUnate.c
@@ -82,7 +82,7 @@ void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose )
abctime clkBdd, clkUnate;
// compute the global BDDs
- dd = (DdManager *)Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, fVerbose);
+ dd = (DdManager *)Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, 0, fVerbose);
if ( dd == NULL )
return;
clkBdd = Abc_Clock() - clk;
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 679d9eed..ae4bc84b 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -67,7 +67,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, int fVerbose )
}
// compute the global BDDs of the latches
- dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
+ dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, 0, fVerbose );
if ( dd == NULL )
return 0;
if ( fVerbose )
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-15 10:55:48 +0000