summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c330
-rw-r--r--src/base/abci/abcAuto.c229
-rw-r--r--src/base/abci/abcBalance.c71
-rw-r--r--src/base/abci/abcDsd.c1
-rw-r--r--src/base/abci/abcMap.c2
-rw-r--r--src/base/abci/abcRenode.c2
-rw-r--r--src/base/abci/abcSat.c31
-rw-r--r--src/base/abci/abcUnate.c150
-rw-r--r--src/base/abci/abcVerify.c12
-rw-r--r--src/base/abci/module.make2
10 files changed, 720 insertions, 110 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5f5c4b49..119f8cdf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -40,6 +40,8 @@ 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_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 );
static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintGates ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -137,6 +139,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Printing", "print_level", Abc_CommandPrintLevel, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_supp", Abc_CommandPrintSupport, 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 );
Cmd_CommandAdd( pAbc, "Printing", "print_kmap", Abc_CommandPrintKMap, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_gates", Abc_CommandPrintGates, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_sharing", Abc_CommandPrintSharing, 0 );
@@ -247,7 +251,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fFactor;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -310,7 +314,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
extern double Abc_NtkSpacePercentage( Abc_Obj_t * pNode );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -398,7 +402,7 @@ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Obj_t * pNode;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -467,7 +471,7 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -517,7 +521,7 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -570,7 +574,7 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fUseRealNames;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -653,7 +657,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
int fListNodes;
int fProfile;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -742,7 +746,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
extern void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -817,7 +821,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerbose;
extern void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -884,6 +888,160 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandPrintUnate( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int fUseBdds;
+ int fUseNaive;
+ int fVerbose;
+ extern void Abc_NtkPrintUnate( Abc_Ntk_t * pNtk, int fUseBdds, int fUseNaive, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fUseBdds = 1;
+ fUseNaive = 0;
+ fVerbose = 0;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "bnvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'b':
+ fUseBdds ^= 1;
+ break;
+ case 'n':
+ fUseNaive ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" );
+ return 1;
+ }
+ Abc_NtkPrintUnate( pNtk, fUseBdds, fUseNaive, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: print_unate [-bnvh]\n" );
+ fprintf( pErr, "\t computes unate variables of the PO functions\n" );
+ fprintf( pErr, "\t-b : toggle BDD-based or SAT-based computations [default = %s].\n", fUseBdds? "BDD": "SAT" );
+ fprintf( pErr, "\t-n : toggle naive BDD-based computation [default = %s].\n", fUseNaive? "yes": "no" );
+ fprintf( pErr, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandPrintAuto( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int Output;
+ int fNaive;
+ int fVerbose;
+ extern void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ Output = -1;
+ fNaive = 0;
+ fVerbose = 0;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "Onvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'O':
+ if ( util_optind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-O\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ Output = atoi(argv[util_optind]);
+ util_optind++;
+ if ( Output < 0 )
+ goto usage;
+ break;
+ case 'n':
+ fNaive ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" );
+ return 1;
+ }
+
+
+ Abc_NtkAutoPrint( pNtk, Output, fNaive, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: print_auto [-O num] [-nvh]\n" );
+ fprintf( pErr, "\t computes autosymmetries of the PO functions\n" );
+ fprintf( pErr, "\t-O num : (optional) the 0-based number of the output [default = all]\n");
+ fprintf( pErr, "\t-n : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" );
+ fprintf( pErr, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -894,7 +1052,7 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -981,7 +1139,7 @@ int Abc_CommandPrintGates( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -1044,7 +1202,7 @@ int Abc_CommandPrintSharing( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NtkPrintSharing( Abc_Ntk_t * pNtk );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -1106,7 +1264,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
extern void Abc_NodeShowBdd( Abc_Obj_t * pNode );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -1194,7 +1352,7 @@ int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv )
int nConeSizeMax;
extern void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -1295,7 +1453,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk );
extern void Abc_NtkShowMulti( Abc_Ntk_t * pNtk );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -1369,7 +1527,7 @@ int Abc_CommandShowNtk( Abc_Frame_t * pAbc, int argc, char ** argv )
int fGateNames;
extern void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -1432,7 +1590,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -1506,7 +1664,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
int fAllNodes;
int fCleanup;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -1573,22 +1731,27 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes, * pNtkTemp;
int c;
- int fDuplicate;
+ bool fDuplicate;
+ bool fSelective;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fDuplicate = 0;
+ fSelective = 0;
util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF )
+ while ( ( c = util_getopt( argc, argv, "dsh" ) ) != EOF )
{
switch ( c )
{
case 'd':
fDuplicate ^= 1;
break;
+ case 's':
+ fSelective ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -1610,7 +1773,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
if ( Abc_NtkIsStrash(pNtk) )
{
- pNtkRes = Abc_NtkBalance( pNtk, fDuplicate );
+ pNtkRes = Abc_NtkBalance( pNtk, fDuplicate, fSelective );
}
else
{
@@ -1620,7 +1783,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Strashing before balancing has failed.\n" );
return 1;
}
- pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate );
+ pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate, fSelective );
Abc_NtkDelete( pNtkTemp );
}
@@ -1635,9 +1798,10 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: balance [-dh]\n" );
+ fprintf( pErr, "usage: balance [-dsh]\n" );
fprintf( pErr, "\t transforms the current network into a well-balanced AIG\n" );
fprintf( pErr, "\t-d : toggle duplication of logic [default = %s]\n", fDuplicate? "yes": "no" );
+ fprintf( pErr, "\t-s : toggle duplication on the critical paths [default = %s]\n", fSelective? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -1662,7 +1826,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
int fMulti;
int fSimple;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -1769,7 +1933,7 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -1824,7 +1988,7 @@ int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -1883,7 +2047,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
extern bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
extern void Abc_NtkFxuFreeInfo( Fxu_Data_t * p );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2010,7 +2174,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
extern int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2136,7 +2300,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Rwr_Precompute();
extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2233,7 +2397,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
bool fVerbose;
extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2351,7 +2515,7 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2420,7 +2584,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCheck;
int fComb;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2491,7 +2655,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
int nFrames;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2575,7 +2739,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2635,7 +2799,7 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2696,7 +2860,7 @@ int Abc_CommandReorder( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerbose;
extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2757,7 +2921,7 @@ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2825,7 +2989,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerbose;
int nSeconds;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2887,7 +3051,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
*/
if ( Abc_NtkIsStrash(pNtk) )
{
- RetValue = Abc_NtkMiterSat2( pNtk, nSeconds, fVerbose );
+ RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose );
if ( RetValue == -1 )
printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
else if ( RetValue == 0 )
@@ -2899,7 +3063,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pTemp;
pTemp = Abc_NtkStrash( pNtk, 0, 0 );
- RetValue = Abc_NtkMiterSat2( pTemp, nSeconds, fVerbose );
+ RetValue = Abc_NtkMiterSat( pTemp, nSeconds, fVerbose );
if ( RetValue == -1 )
printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
else if ( RetValue == 0 )
@@ -2939,7 +3103,7 @@ int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerbose;
extern int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNet, bool fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -3010,7 +3174,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
int fUseAllCis;
int Output;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -3122,7 +3286,7 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Obj_t * pNode;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -3202,7 +3366,7 @@ int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -3251,7 +3415,7 @@ int Abc_CommandExdcFree( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -3311,7 +3475,7 @@ int Abc_CommandExdcGet( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -3369,7 +3533,7 @@ int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv )
char * FileName;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -3461,7 +3625,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
extern void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * pCutOracle );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -3591,7 +3755,7 @@ int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -3696,7 +3860,7 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
int nFaninMax;
extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -3784,9 +3948,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
- extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
+// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -3819,7 +3983,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// printf( "This command is currently not used.\n" );
// run the command
// pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
- pNtkRes = Abc_NtkNewAig( pNtk );
+
+// pNtkRes = Abc_NtkNewAig( pNtk );
+ pNtkRes = NULL;
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -3859,7 +4025,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
int fExdc;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4017,7 +4183,7 @@ int Abc_CommandFraigTrust( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fDuplicate;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4081,7 +4247,7 @@ int Abc_CommandFraigStore( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fDuplicate;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4142,7 +4308,7 @@ int Abc_CommandFraigRestore( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fDuplicate;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4206,7 +4372,7 @@ int Abc_CommandFraigClean( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fDuplicate;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4258,7 +4424,7 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerbose;
extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4345,7 +4511,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose );
extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4410,7 +4576,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Strashing before mapping has failed.\n" );
return 1;
}
- pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0 );
+ pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 );
Abc_NtkDelete( pNtkRes );
if ( pNtk == NULL )
{
@@ -4481,7 +4647,7 @@ int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
extern int Abc_NtkUnmap( Abc_Ntk_t * pNtk );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4542,7 +4708,7 @@ int Abc_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
extern int Abc_NtkUnmap( Abc_Ntk_t * pNtk );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4605,7 +4771,7 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4678,7 +4844,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int fSwitching, int fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4740,7 +4906,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
return 1;
}
- pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0 );
+ pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 );
Abc_NtkDelete( pNtkRes );
if ( pNtk == NULL )
{
@@ -4806,7 +4972,7 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
extern Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -4863,7 +5029,7 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
return 1;
}
- pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0 );
+ pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 );
Abc_NtkDelete( pNtkRes );
if ( pNtk == NULL )
{
@@ -4931,7 +5097,7 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
int fRandom;
int fDontCare;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -5039,7 +5205,7 @@ int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv )
int nLatches;
extern void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -5115,7 +5281,7 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -5192,7 +5358,7 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fShare;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -5269,7 +5435,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
int fInitial;
int fVerbose;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -5395,7 +5561,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nMaxIters;
int fVerbose;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -5459,7 +5625,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0 );
+ pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0 );
Abc_NtkDelete( pNtkRes );
if ( pNtkNew == NULL )
{
@@ -5519,7 +5685,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nMaxIters;
int fVerbose;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -5583,7 +5749,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0 );
+ pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0 );
Abc_NtkDelete( pNtkRes );
if ( pNtkNew == NULL )
{
@@ -5649,7 +5815,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
extern Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -5756,7 +5922,7 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -5822,7 +5988,7 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -5914,7 +6080,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
- pNtk = Abc_FrameReadNet(pAbc);
+ pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
new file mode 100644
index 00000000..752943c3
--- /dev/null
+++ b/src/base/abci/abcAuto.c
@@ -0,0 +1,229 @@
+/**CFile****************************************************************
+
+ FileName [abcAuto.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Computation of autosymmetries.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcAuto.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int nOutputs, char * pInputNames[], char * pOutputNames[], int fNaive );
+static void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int Output, char * pInputNames[], char * pOutputNames[], int fNaive );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
+{
+ DdManager * dd; // the BDD manager used to hold shared BDDs
+ DdNode ** pbGlobal; // temporary storage for global BDDs
+ char ** pInputNames; // pointers to the CI names
+ char ** pOutputNames; // pointers to the CO names
+ int nOutputs, nInputs, i;
+
+ // compute the global BDDs
+ if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+ return;
+
+ // get information about the network
+ nInputs = Abc_NtkCiNum(pNtk);
+ nOutputs = Abc_NtkCoNum(pNtk);
+ dd = pNtk->pManGlob;
+ pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob );
+
+ // get the network names
+ pInputNames = Abc_NtkCollectCioNames( pNtk, 0 );
+ pOutputNames = Abc_NtkCollectCioNames( pNtk, 1 );
+
+ // print the size of the BDDs
+ if ( fVerbose )
+ printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+ // allocate additional variables
+ for ( i = 0; i < nInputs; i++ )
+ Cudd_bddNewVar( dd );
+ assert( Cudd_ReadSize(dd) == 2 * nInputs );
+
+ // create ZDD variables in the manager
+ Cudd_zddVarsFromBddVars( dd, 2 );
+
+ // perform the analysis of the primary output functions for auto-symmetry
+ if ( Output == -1 )
+ Abc_NtkAutoPrintAll( dd, nInputs, pbGlobal, nOutputs, pInputNames, pOutputNames, fNaive );
+ else
+ Abc_NtkAutoPrintOne( dd, nInputs, pbGlobal, Output, pInputNames, pOutputNames, fNaive );
+
+ // deref the PO functions
+ Abc_NtkFreeGlobalBdds( pNtk );
+ // stop the global BDD manager
+ Extra_StopManager( pNtk->pManGlob );
+ pNtk->pManGlob = NULL;
+ free( pInputNames );
+ free( pOutputNames );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int nOutputs, char * pInputNames[], char * pOutputNames[], int fNaive )
+{
+ DdNode * bSpace1, * bSpace2, * bCanVars, * bReduced, * zEquations;
+ double nMints;
+ int nSupp, SigCounter, o;
+
+ int nAutos;
+ int nAutoSyms;
+ int nAutoSymsMax;
+ int nAutoSymsMaxSupp;
+ int nAutoSymOuts;
+ int nSuppSizeMax;
+ int clk;
+
+ nAutoSymOuts = 0;
+ nAutoSyms = 0;
+ nAutoSymsMax = 0;
+ nAutoSymsMaxSupp = 0;
+ nSuppSizeMax = 0;
+ clk = clock();
+
+ SigCounter = 0;
+ for ( o = 0; o < nOutputs; o++ )
+ {
+ bSpace1 = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[o] ); Cudd_Ref( bSpace1 );
+// bSpace1 = Extra_bddSpaceFromFunction( dd, pbOutputs[o], pbOutputs[o] ); Cudd_Ref( bSpace1 );
+ bCanVars = Extra_bddSpaceCanonVars( dd, bSpace1 ); Cudd_Ref( bCanVars );
+ bReduced = Extra_bddSpaceReduce( dd, pbOutputs[o], bCanVars ); Cudd_Ref( bReduced );
+ zEquations = Extra_bddSpaceEquations( dd, bSpace1 ); Cudd_Ref( zEquations );
+
+ nSupp = Cudd_SupportSize( dd, bSpace1 );
+ nMints = Cudd_CountMinterm( dd, bSpace1, nSupp );
+ nAutos = Extra_Base2LogDouble(nMints);
+ printf( "Output #%3d: Inputs = %2d. AutoK = %2d.\n", o, nSupp, nAutos );
+
+ if ( nAutos > 0 )
+ {
+ nAutoSymOuts++;
+ nAutoSyms += nAutos;
+ if ( nAutoSymsMax < nAutos )
+ {
+ nAutoSymsMax = nAutos;
+ nAutoSymsMaxSupp = nSupp;
+ }
+ }
+ if ( nSuppSizeMax < nSupp )
+ nSuppSizeMax = nSupp;
+
+
+//PRB( dd, bCanVars );
+//PRB( dd, bReduced );
+//Cudd_PrintMinterm( dd, bReduced );
+//printf( "The equations are:\n" );
+//Cudd_zddPrintCover( dd, zEquations );
+//printf( "\n" );
+//fflush( stdout );
+
+ bSpace2 = Extra_bddSpaceFromMatrixPos( dd, zEquations ); Cudd_Ref( bSpace2 );
+//PRB( dd, bSpace1 );
+//PRB( dd, bSpace2 );
+ if ( bSpace1 != bSpace2 )
+ printf( "Spaces are NOT EQUAL!\n" );
+// else
+// printf( "Spaces are equal.\n" );
+
+ Cudd_RecursiveDeref( dd, bSpace1 );
+ Cudd_RecursiveDeref( dd, bSpace2 );
+ Cudd_RecursiveDeref( dd, bCanVars );
+ Cudd_RecursiveDeref( dd, bReduced );
+ Cudd_RecursiveDerefZdd( dd, zEquations );
+ }
+
+ printf( "The cumulative statistics for all outputs:\n" );
+ printf( "Ins=%3d ", nInputs );
+ printf( "InMax=%3d ", nSuppSizeMax );
+ printf( "Outs=%3d ", nOutputs );
+ printf( "Auto=%3d ", nAutoSymOuts );
+ printf( "SumK=%3d ", nAutoSyms );
+ printf( "KMax=%2d ", nAutoSymsMax );
+ printf( "Supp=%3d ", nAutoSymsMaxSupp );
+ printf( "Time=%4.2f ", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int Output, char * pInputNames[], char * pOutputNames[], int fNaive )
+{
+ DdNode * bSpace1, * bCanVars, * bReduced, * zEquations;
+ double nMints;
+ int nSupp, SigCounter;
+ int nAutos;
+
+ SigCounter = 0;
+ bSpace1 = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[Output] ); Cudd_Ref( bSpace1 );
+// bSpace1 = Extra_bddSpaceFromFunction( dd, pbOutputs[Output], pbOutputs[Output] ); Cudd_Ref( bSpace1 );
+ bCanVars = Extra_bddSpaceCanonVars( dd, bSpace1 ); Cudd_Ref( bCanVars );
+ bReduced = Extra_bddSpaceReduce( dd, pbOutputs[Output], bCanVars ); Cudd_Ref( bReduced );
+ zEquations = Extra_bddSpaceEquations( dd, bSpace1 ); Cudd_Ref( zEquations );
+
+ nSupp = Cudd_SupportSize( dd, bSpace1 );
+ nMints = Cudd_CountMinterm( dd, bSpace1, nSupp );
+ nAutos = Extra_Base2LogDouble(nMints);
+ printf( "Output #%3d: Inputs = %2d. AutoK = %2d.\n", Output, nSupp, nAutos );
+
+ Cudd_RecursiveDeref( dd, bSpace1 );
+ Cudd_RecursiveDeref( dd, bCanVars );
+ Cudd_RecursiveDeref( dd, bReduced );
+ Cudd_RecursiveDerefZdd( dd, zEquations );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index fed89dbb..effae853 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -24,10 +24,11 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate );
-static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, bool fDuplicate );
-static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate );
-static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate );
+static void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective );
+static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, bool fDuplicate, bool fSelective );
+static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate, bool fSelective );
+static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate, bool fSelective );
+static void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -44,14 +45,26 @@ static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSupe
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
+Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective )
{
Abc_Ntk_t * pNtkAig;
assert( Abc_NtkIsStrash(pNtk) );
+ // compute the required times
+ if ( fSelective )
+ {
+ Abc_NtkStartReverseLevels( pNtk );
+ Abc_NtkMarkCriticalNodes( pNtk );
+ }
// perform balancing
pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
- Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate );
+ Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective );
Abc_NtkFinalize( pNtk, pNtkAig );
+ // undo the required times
+ if ( fSelective )
+ {
+ Abc_NtkStopReverseLevels( pNtk );
+ Abc_NtkCleanMarkA( pNtk );
+ }
if ( pNtk->pExdc )
pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
// make sure everything is okay
@@ -75,7 +88,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
SeeAlso []
***********************************************************************/
-void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate )
+void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective )
{
int fCheck = 1;
ProgressBar * pProgress;
@@ -94,7 +107,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
Extra_ProgressBarUpdate( pProgress, i, NULL );
// strash the driver node
pDriver = Abc_ObjFanin0(pNode);
- Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate );
+ Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate, fSelective );
}
Extra_ProgressBarStop( pProgress );
Vec_VecFree( vStorage );
@@ -147,7 +160,7 @@ void Abc_NodeBalanceRandomize( Vec_Ptr_t * vSuper )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate )
+Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate, bool fSelective )
{
Abc_Aig_t * pMan = pNtkNew->pManFunc;
Abc_Obj_t * pNodeNew, * pNode1, * pNode2;
@@ -159,7 +172,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
return pNodeOld->pCopy;
assert( Abc_ObjIsNode(pNodeOld) );
// get the implication supergate
- vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate );
+ vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate, fSelective );
if ( vSuper->nSize == 0 )
{ // it means that the supergate contains two nodes in the opposite polarity
pNodeOld->pCopy = Abc_ObjNot(Abc_NtkConst1(pNtkNew));
@@ -168,7 +181,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
// for each old node, derive the new well-balanced node
for ( i = 0; i < vSuper->nSize; i++ )
{
- pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate );
+ pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate, fSelective );
vSuper->pArray[i] = Abc_ObjNotCond( pNodeNew, Abc_ObjIsComplement(vSuper->pArray[i]) );
}
if ( vSuper->nSize < 2 )
@@ -207,7 +220,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
SeeAlso []
***********************************************************************/
-Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, int fDuplicate )
+Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, int fDuplicate, bool fSelective )
{
Vec_Ptr_t * vNodes;
int RetValue, i;
@@ -219,7 +232,7 @@ Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Le
vNodes = Vec_VecEntry( vStorage, Level );
Vec_PtrClear( vNodes );
// collect the nodes in the implication supergate
- RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, fDuplicate );
+ RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, fDuplicate, fSelective );
assert( vNodes->nSize > 1 );
// unmark the visited nodes
for ( i = 0; i < vNodes->nSize; i++ )
@@ -245,7 +258,7 @@ Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Le
SeeAlso []
***********************************************************************/
-int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate )
+int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate, bool fSelective )
{
int RetValue1, RetValue2, i;
// check if the node is visited
@@ -263,7 +276,7 @@ int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst,
return 0;
}
// if the new node is complemented or a PI, another gate begins
- if ( !fFirst && (Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || !fDuplicate && (Abc_ObjFanoutNum(pNode) > 1)) )
+ if ( !fFirst && (Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || !fDuplicate && !fSelective && (Abc_ObjFanoutNum(pNode) > 1)) )
{
Vec_PtrPush( vSuper, pNode );
Abc_ObjRegular(pNode)->fMarkB = 1;
@@ -272,8 +285,8 @@ int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst,
assert( !Abc_ObjIsComplement(pNode) );
assert( Abc_ObjIsNode(pNode) );
// go through the branches
- RetValue1 = Abc_NodeBalanceCone_rec( Abc_ObjChild0(pNode), vSuper, 0, fDuplicate );
- RetValue2 = Abc_NodeBalanceCone_rec( Abc_ObjChild1(pNode), vSuper, 0, fDuplicate );
+ RetValue1 = Abc_NodeBalanceCone_rec( Abc_ObjChild0(pNode), vSuper, 0, fDuplicate, fSelective );
+ RetValue2 = Abc_NodeBalanceCone_rec( Abc_ObjChild1(pNode), vSuper, 0, fDuplicate, fSelective );
if ( RetValue1 == -1 || RetValue2 == -1 )
return -1;
// return 1 if at least one branch has a duplicate
@@ -315,7 +328,7 @@ Vec_Ptr_t * Abc_NodeFindCone_rec( Abc_Obj_t * pNode )
else
{
// collect the nodes in the implication supergate
- RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, 1 );
+ RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, 1, 0 );
assert( vNodes->nSize > 1 );
// unmark the visited nodes
Vec_PtrForEachEntry( vNodes, pNode, i )
@@ -442,6 +455,28 @@ void Abc_NtkBalanceLevel( Abc_Ntk_t * pNtk )
}
+/**Function*************************************************************
+
+ Synopsis [Marks the nodes on the critical and near critical paths.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNode;
+ int i, Counter = 0;
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ if ( Abc_NodeReadRequiredLevel(pNode) - pNode->Level <= 1 )
+ pNode->fMarkA = 1, Counter++;
+ printf( "The number of nodes on the critical paths = %6d (%5.2f %%)\n", Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk) );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 5c7f0d48..a73ab2b5 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -172,6 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
int i, nNodesDsd;
// save the CI nodes in the DSD nodes
+ Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkConst1(pNtk)->pCopy );
Abc_NtkForEachCi( pNtk, pNode, i )
{
pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 39bf15aa..128e054a 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -105,7 +105,7 @@ clk = clock();
Map_ManFree( pMan );
return NULL;
}
-// Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk );
+ Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk );
// reconstruct the network after mapping
pNtkNew = Abc_NtkFromMap( pMan, pNtk );
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index c1f83e1f..ea2f808c 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -173,6 +173,8 @@ Abc_Obj_t * Abc_NtkRenode_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
assert( !Abc_NodeIsConst(pNodeOld) );
assert( pNodeOld->fMarkA );
+//printf( "%d ", Abc_NodeMffcSizeSupp(pNodeOld) );
+
// collect the renoding cone
vCone = Vec_PtrAlloc( 10 );
Abc_NtkRenodeCone( pNodeOld, vCone );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index f7b9892e..9c650aa9 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -29,6 +29,8 @@ static int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t *
static solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk );
+static Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
+
static nMuxes;
////////////////////////////////////////////////////////////////////////
@@ -46,7 +48,7 @@ static nMuxes;
SeeAlso []
***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
+int Abc_NtkMiterSat_OldAndRusty( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
{
solver * pSat;
lbool status;
@@ -317,7 +319,7 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
SeeAlso []
***********************************************************************/
-int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
{
solver * pSat;
lbool status;
@@ -376,7 +378,8 @@ int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
// if the problem is SAT, get the counterexample
if ( status == l_True )
{
- Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
+// Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
+ Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
Vec_IntFree( vCiIds );
}
@@ -385,6 +388,28 @@ int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
return RetValue;
}
+/**Function*************************************************************
+
+ Synopsis [Returns the array of CI IDs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk )
+{
+ Vec_Int_t * vCiIds;
+ Abc_Obj_t * pObj;
+ int i;
+ vCiIds = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ Vec_IntPush( vCiIds, (int)pObj->pCopy );
+ return vCiIds;
+}
+
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
new file mode 100644
index 00000000..08a42623
--- /dev/null
+++ b/src/base/abci/abcUnate.c
@@ -0,0 +1,150 @@
+/**CFile****************************************************************
+
+ FileName [abcUnate.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcUnate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose );
+static void Abc_NtkPrintUnateSat( Abc_Ntk_t * pNtk, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Detects unate variables of the multi-output function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintUnate( Abc_Ntk_t * pNtk, int fUseBdds, int fUseNaive, int fVerbose )
+{
+ if ( fUseBdds || fUseNaive )
+ Abc_NtkPrintUnateBdd( pNtk, fUseNaive, fVerbose );
+ else
+ Abc_NtkPrintUnateSat( pNtk, fVerbose );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Detects unate variables using BDDs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose )
+{
+ Abc_Obj_t * pNode;
+ Extra_UnateInfo_t * p;
+ DdManager * dd; // the BDD manager used to hold shared BDDs
+ DdNode ** pbGlobal; // temporary storage for global BDDs
+ int TotalSupps = 0;
+ int TotalUnate = 0;
+ int i, clk = clock();
+ int clkBdd, clkUnate;
+
+ // compute the global BDDs
+ if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+ return;
+clkBdd = clock() - clk;
+
+ // get information about the network
+ dd = pNtk->pManGlob;
+ pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob );
+
+ // print the size of the BDDs
+ printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+ // perform naive BDD-based computation
+ if ( fUseNaive )
+ {
+ Abc_NtkForEachCo( pNtk, pNode, i )
+ {
+ p = Extra_UnateComputeSlow( dd, pbGlobal[i] );
+ if ( fVerbose )
+ Extra_UnateInfoPrint( p );
+ TotalSupps += p->nVars;
+ TotalUnate += p->nUnate;
+ Extra_UnateInfoDissolve( p );
+ }
+ }
+ // perform smart BDD-based computation
+ else
+ {
+ // create ZDD variables in the manager
+ Cudd_zddVarsFromBddVars( dd, 2 );
+ Abc_NtkForEachCo( pNtk, pNode, i )
+ {
+ p = Extra_UnateComputeFast( dd, pbGlobal[i] );
+ if ( fVerbose )
+ Extra_UnateInfoPrint( p );
+ TotalSupps += p->nVars;
+ TotalUnate += p->nUnate;
+ Extra_UnateInfoDissolve( p );
+ }
+ }
+clkUnate = clock() - clk - clkBdd;
+
+ // print stats
+ printf( "Ins/Outs = %4d/%4d. Total supp = %5d. Total unate = %5d.\n",
+ Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), TotalSupps, TotalUnate );
+ PRT( "Glob BDDs", clkBdd );
+ PRT( "Unateness", clkUnate );
+ PRT( "Total ", clock() - clk );
+
+ // deref the PO functions
+ Abc_NtkFreeGlobalBdds( pNtk );
+ // stop the global BDD manager
+ Extra_StopManager( pNtk->pManGlob );
+ pNtk->pManGlob = NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Detects unate variables using SAT.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintUnateSat( Abc_Ntk_t * pNtk, int fVerbose )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index b30a6452..99392e48 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -148,9 +148,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
Fraig_ParamsSetDefault( &Params );
Params.fVerbose = fVerbose;
Params.nSeconds = nSeconds;
- Params.fFuncRed = 0;
- Params.nPatsRand = 0;
- Params.nPatsDyna = 0;
+// Params.fFuncRed = 0;
+// Params.nPatsRand = 0;
+// Params.nPatsDyna = 0;
pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 );
Fraig_ManProveMiter( pMan );
@@ -328,9 +328,9 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
Fraig_ParamsSetDefault( &Params );
Params.fVerbose = fVerbose;
Params.nSeconds = nSeconds;
- Params.fFuncRed = 0;
- Params.nPatsRand = 0;
- Params.nPatsDyna = 0;
+// Params.fFuncRed = 0;
+// Params.nPatsRand = 0;
+// Params.nPatsDyna = 0;
pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 );
Fraig_ManProveMiter( pMan );
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 660aee63..5b15641b 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -1,5 +1,6 @@
SRC += src/base/abci/abc.c \
src/base/abci/abcAttach.c \
+ src/base/abci/abcAuto.c \
src/base/abci/abcBalance.c \
src/base/abci/abcCollapse.c \
src/base/abci/abcCut.c \
@@ -21,6 +22,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcSweep.c \
src/base/abci/abcSymm.c \
src/base/abci/abcTiming.c \
+ src/base/abci/abcUnate.c \
src/base/abci/abcUnreach.c \
src/base/abci/abcVanEijk.c \
src/base/abci/abcVanImp.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 12:03:21 +0000