summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2006-02-20 08:01:00 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2006-02-20 08:01:00 -0800
commit8eef7f8326e715ea4e9e84f46487cf4657601c25 (patch)
tree03a394e5a245bd3c0ed0b6397275c5b029adfb41 /src/base/abci
parent77d7377442c28fd5c65144d7ea23938600967b2b (diff)
downloadabc-8eef7f8326e715ea4e9e84f46487cf4657601c25.tar.gz
abc-8eef7f8326e715ea4e9e84f46487cf4657601c25.tar.bz2
abc-8eef7f8326e715ea4e9e84f46487cf4657601c25.zip
Version abc60220
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c1045
-rw-r--r--src/base/abci/abcBalance.c117
-rw-r--r--src/base/abci/abcClpBdd.c (renamed from src/base/abci/abcCollapse.c)0
-rw-r--r--src/base/abci/abcClpSop.c53
-rw-r--r--src/base/abci/abcCut.c55
-rw-r--r--src/base/abci/abcDsd.c2
-rw-r--r--src/base/abci/abcEspresso.c244
-rw-r--r--src/base/abci/abcFraig.c2
-rw-r--r--src/base/abci/abcMap.c2
-rw-r--r--src/base/abci/abcMiter.c18
-rw-r--r--src/base/abci/abcNewAig.c13
-rw-r--r--src/base/abci/abcNtbdd.c2
-rw-r--r--src/base/abci/abcProve.c232
-rw-r--r--src/base/abci/abcRenode.c2
-rw-r--r--src/base/abci/abcRestruct.c1026
-rw-r--r--src/base/abci/abcRewrite.c8
-rw-r--r--src/base/abci/abcSat.c294
-rw-r--r--src/base/abci/abcUnreach.c2
-rw-r--r--src/base/abci/abcVanEijk.c8
-rw-r--r--src/base/abci/abcVanImp.c2
-rw-r--r--src/base/abci/abcVerify.c8
-rw-r--r--src/base/abci/module.make5
22 files changed, 2460 insertions, 680 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 119f8cdf..d2422b64 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -62,6 +62,7 @@ static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv
static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRestructure ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -80,6 +81,7 @@ static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv
static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -110,6 +112,7 @@ static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -161,6 +164,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "restructure", Abc_CommandRestructure, 1 );
// Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 );
Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 );
@@ -171,14 +175,15 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 );
Cmd_CommandAdd( pAbc, "Various", "sat", Abc_CommandSat, 0 );
Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 );
- Cmd_CommandAdd( pAbc, "Various", "one_output", Abc_CommandOneOutput, 1 );
- Cmd_CommandAdd( pAbc, "Various", "one_node", Abc_CommandOneNode, 1 );
+ Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandOneOutput, 1 );
+ Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandOneNode, 1 );
Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 );
Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 );
Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 );
Cmd_CommandAdd( pAbc, "Various", "exdc_set", Abc_CommandExdcSet, 1 );
Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 );
Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 );
+ Cmd_CommandAdd( pAbc, "Various", "espresso", Abc_CommandEspresso, 1 );
Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 );
@@ -209,6 +214,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
// Rwt_Man4ExploreStart();
// Map_Var3Print();
@@ -258,8 +264,8 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
// set the defaults
fShort = 1;
fFactor = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "sfh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "sfh" ) ) != EOF )
{
switch ( c )
{
@@ -321,8 +327,8 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
// set the defaults
fShort = 1;
fPrintDc = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "sdh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "sdh" ) ) != EOF )
{
switch ( c )
{
@@ -407,8 +413,8 @@ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -425,18 +431,18 @@ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( argc > util_optind + 1 )
+ if ( argc > globalUtilOptind + 1 )
{
fprintf( pErr, "Wrong number of auguments.\n" );
goto usage;
}
- if ( argc == util_optind + 1 )
+ if ( argc == globalUtilOptind + 1 )
{
- pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+ pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
if ( pNode == NULL )
{
- fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+ fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] );
return 1;
}
Abc_NodePrintFanio( pOut, pNode );
@@ -476,8 +482,8 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -526,8 +532,8 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -580,8 +586,8 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fUseRealNames = 1;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "nh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF )
{
switch ( c )
{
@@ -607,18 +613,18 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( argc > util_optind + 1 )
+ if ( argc > globalUtilOptind + 1 )
{
fprintf( pErr, "Wrong number of auguments.\n" );
goto usage;
}
- if ( argc == util_optind + 1 )
+ if ( argc == globalUtilOptind + 1 )
{
- pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+ pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
if ( pNode == NULL )
{
- fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+ fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] );
return 1;
}
Abc_NodePrintFactor( pOut, pNode, fUseRealNames );
@@ -664,8 +670,8 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fListNodes = 0;
fProfile = 1;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "nph" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "nph" ) ) != EOF )
{
switch ( c )
{
@@ -694,18 +700,18 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( argc > util_optind + 1 )
+ if ( argc > globalUtilOptind + 1 )
{
fprintf( pErr, "Wrong number of auguments.\n" );
goto usage;
}
- if ( argc == util_optind + 1 )
+ if ( argc == globalUtilOptind + 1 )
{
- pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+ pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
if ( pNode == NULL )
{
- fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+ fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] );
return 1;
}
Abc_NodePrintLevel( pOut, pNode );
@@ -752,8 +758,8 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
@@ -829,8 +835,8 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
fUseBdds = 0;
fNaive = 0;
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "bnvh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "bnvh" ) ) != EOF )
{
switch ( c )
{
@@ -906,8 +912,8 @@ int Abc_CommandPrintUnate( Abc_Frame_t * pAbc, int argc, char ** argv )
fUseBdds = 1;
fUseNaive = 0;
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "bnvh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "bnvh" ) ) != EOF )
{
switch ( c )
{
@@ -978,19 +984,19 @@ int Abc_CommandPrintAuto( Abc_Frame_t * pAbc, int argc, char ** argv )
Output = -1;
fNaive = 0;
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Onvh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Onvh" ) ) != EOF )
{
switch ( c )
{
case 'O':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-O\" should be followed by an integer.\n" );
goto usage;
}
- Output = atoi(argv[util_optind]);
- util_optind++;
+ Output = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( Output < 0 )
goto usage;
break;
@@ -1058,8 +1064,8 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fUseRealNames = 1;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "nh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF )
{
switch ( c )
{
@@ -1084,12 +1090,12 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Visualizing Karnaugh map works for BDD logic networks (run \"bdd\").\n" );
return 1;
}
- if ( argc > util_optind + 1 )
+ if ( argc > globalUtilOptind + 1 )
{
fprintf( pErr, "Wrong number of auguments.\n" );
goto usage;
}
- if ( argc == util_optind )
+ if ( argc == globalUtilOptind )
{
pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
if ( !Abc_ObjIsNode(pNode) )
@@ -1100,10 +1106,10 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
{
- pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+ pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
if ( pNode == NULL )
{
- fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+ fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] );
return 1;
}
}
@@ -1145,8 +1151,8 @@ int Abc_CommandPrintGates( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fUseLibrary = 1;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
{
switch ( c )
{
@@ -1208,8 +1214,8 @@ int Abc_CommandPrintSharing( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fUseLibrary = 1;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
{
switch ( c )
{
@@ -1269,8 +1275,8 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -1293,12 +1299,12 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( argc > util_optind + 1 )
+ if ( argc > globalUtilOptind + 1 )
{
fprintf( pErr, "Wrong number of auguments.\n" );
goto usage;
}
- if ( argc == util_optind )
+ if ( argc == globalUtilOptind )
{
pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
if ( !Abc_ObjIsNode(pNode) )
@@ -1309,10 +1315,10 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
{
- pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+ pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
if ( pNode == NULL )
{
- fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+ fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] );
return 1;
}
}
@@ -1359,30 +1365,30 @@ int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nNodeSizeMax = 10;
nConeSizeMax = ABC_INFINITY;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "NCh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NCh" ) ) != EOF )
{
switch ( c )
{
case 'N':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
- nNodeSizeMax = atoi(argv[util_optind]);
- util_optind++;
+ nNodeSizeMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nNodeSizeMax < 0 )
goto usage;
break;
case 'C':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
- nConeSizeMax = atoi(argv[util_optind]);
- util_optind++;
+ nConeSizeMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nConeSizeMax < 0 )
goto usage;
break;
@@ -1404,16 +1410,16 @@ int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Visualizing cuts only works for AIGs (run \"strash\").\n" );
return 1;
}
- if ( argc != util_optind + 1 )
+ if ( argc != globalUtilOptind + 1 )
{
fprintf( pErr, "Wrong number of auguments.\n" );
goto usage;
}
- pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+ pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
if ( pNode == NULL )
{
- fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+ fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] );
return 1;
}
Abc_NodeShowCut( pNode, nNodeSizeMax, nConeSizeMax );
@@ -1459,8 +1465,8 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fMulti = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "mh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
{
switch ( c )
{
@@ -1533,8 +1539,8 @@ int Abc_CommandShowNtk( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fGateNames = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "gh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "gh" ) ) != EOF )
{
switch ( c )
{
@@ -1595,8 +1601,8 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -1671,8 +1677,8 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fAllNodes = 0;
fCleanup = 1;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "ach" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ach" ) ) != EOF )
{
switch ( c )
{
@@ -1733,19 +1739,24 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
bool fDuplicate;
bool fSelective;
+ bool fUpdateLevel;
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, "dsh" ) ) != EOF )
+ fDuplicate = 0;
+ fSelective = 0;
+ fUpdateLevel = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ldsh" ) ) != EOF )
{
switch ( c )
{
+ case 'l':
+ fUpdateLevel ^= 1;
+ break;
case 'd':
fDuplicate ^= 1;
break;
@@ -1773,7 +1784,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, fSelective );
+ pNtkRes = Abc_NtkBalance( pNtk, fDuplicate, fSelective, fUpdateLevel );
}
else
{
@@ -1783,7 +1794,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, fSelective );
+ pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate, fSelective, fUpdateLevel );
Abc_NtkDelete( pNtkTemp );
}
@@ -1798,8 +1809,9 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: balance [-dsh]\n" );
+ fprintf( pErr, "usage: balance [-ldsh]\n" );
fprintf( pErr, "\t transforms the current network into a well-balanced AIG\n" );
+ fprintf( pErr, "\t-l : toggle minimizing the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
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");
@@ -1836,30 +1848,30 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
fCnf = 0;
fMulti = 0;
fSimple = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "TFmcsh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "TFmcsh" ) ) != EOF )
{
switch ( c )
{
case 'T':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
- nThresh = atoi(argv[util_optind]);
- util_optind++;
+ nThresh = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nThresh < 0 )
goto usage;
break;
case 'F':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
- nFaninMax = atoi(argv[util_optind]);
- util_optind++;
+ nFaninMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nFaninMax < 0 )
goto usage;
break;
@@ -1938,8 +1950,8 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -1993,8 +2005,8 @@ int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -2062,30 +2074,30 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
p->fUse0 = 0;
p->fUseCompl = 1;
p->fVerbose = 0;
- util_getopt_reset();
- while ( (c = util_getopt(argc, argv, "LNsdzcvh")) != EOF )
+ Extra_UtilGetoptReset();
+ while ( (c = Extra_UtilGetopt(argc, argv, "LNsdzcvh")) != EOF )
{
switch (c)
{
case 'L':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
- p->nPairsMax = atoi(argv[util_optind]);
- util_optind++;
+ p->nPairsMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( p->nPairsMax < 0 )
goto usage;
break;
case 'N':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
- p->nNodesExt = atoi(argv[util_optind]);
- util_optind++;
+ p->nNodesExt = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( p->nNodesExt < 0 )
goto usage;
break;
@@ -2184,8 +2196,8 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
fVerbose = 0;
fPrint = 0;
fShort = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "grvpsh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "grvpsh" ) ) != EOF )
{
switch ( c )
{
@@ -2309,8 +2321,8 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
fPrecompute = 0;
fUseZeros = 0;
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "lxzvh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvh" ) ) != EOF )
{
switch ( c )
{
@@ -2371,7 +2383,7 @@ usage:
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
-}
+}
/**Function*************************************************************
@@ -2404,34 +2416,34 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nNodeSizeMax = 10;
nConeSizeMax = 16;
- fUpdateLevel = 0;
+ fUpdateLevel = 1;
fUseZeros = 0;
fUseDcs = 0;
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "NClzdvh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NClzdvh" ) ) != EOF )
{
switch ( c )
{
case 'N':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
- nNodeSizeMax = atoi(argv[util_optind]);
- util_optind++;
+ nNodeSizeMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nNodeSizeMax < 0 )
goto usage;
break;
case 'C':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
- nConeSizeMax = atoi(argv[util_optind]);
- util_optind++;
+ nConeSizeMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nConeSizeMax < 0 )
goto usage;
break;
@@ -2497,6 +2509,109 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int nCutMax;
+ bool fUpdateLevel;
+ bool fUseZeros;
+ bool fVerbose;
+ extern int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nCutMax = 5;
+ fUpdateLevel = 0;
+ fUseZeros = 0;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Klzvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nCutMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nCutMax < 0 )
+ goto usage;
+ break;
+ case 'l':
+ fUpdateLevel ^= 1;
+ break;
+ case 'z':
+ fUseZeros ^= 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 ( nCutMax < 4 || nCutMax > CUT_SIZE_MAX )
+ {
+ fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", 4, CUT_SIZE_MAX );
+ return 1;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" );
+ return 1;
+ }
+ if ( Abc_NtkGetChoiceNum(pNtk) )
+ {
+ fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" );
+ return 1;
+ }
+
+ // modify the current network
+ if ( !Abc_NtkRestructure( pNtk, nCutMax, fUpdateLevel, fUseZeros, fVerbose ) )
+ {
+ fprintf( pErr, "Refactoring has failed.\n" );
+ return 1;
+ }
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: restructure [-K num] [-lzvh]\n" );
+ fprintf( pErr, "\t performs technology-independent restructuring of the AIG\n" );
+ fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", CUT_SIZE_MIN, CUT_SIZE_MAX, nCutMax );
+ fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+ fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
@@ -2520,8 +2635,8 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -2591,8 +2706,8 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fComb = 1;
fCheck = 1;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
{
switch ( c )
{
@@ -2604,8 +2719,8 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
- pArgvNew = argv + util_optind;
- nArgcNew = argc - util_optind;
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
return 1;
@@ -2662,19 +2777,19 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fInitial = 0;
nFrames = 5;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Fih" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Fih" ) ) != EOF )
{
switch ( c )
{
case 'F':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
- nFrames = atoi(argv[util_optind]);
- util_optind++;
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nFrames <= 0 )
goto usage;
break;
@@ -2744,8 +2859,8 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -2804,8 +2919,8 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -2866,8 +2981,8 @@ int Abc_CommandReorder( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
@@ -2926,8 +3041,8 @@ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -2987,29 +3102,43 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int RetValue;
int fVerbose;
- int nSeconds;
+ int nConfLimit;
+ int nImpLimit;
+ int clk;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- fVerbose = 0;
- nSeconds = 20;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Tvh" ) ) != EOF )
+ fVerbose = 0;
+ nConfLimit = 100000;
+ nImpLimit = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF )
{
switch ( c )
{
- case 'T':
- if ( util_optind >= argc )
+ case 'C':
+ if ( globalUtilOptind >= argc )
{
- fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
- nSeconds = atoi(argv[util_optind]);
- util_optind++;
- if ( nSeconds < 0 )
+ nConfLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfLimit < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nImpLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nImpLimit < 0 )
goto usage;
break;
case 'v':
@@ -3038,46 +3167,42 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
-/*
- if ( !Abc_NtkIsLogic(pNtk) )
- {
- fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" );
- return 0;
- }
- if ( Abc_NtkIsMappedLogic(pNtk) )
- Abc_NtkUnmap(pNtk);
- if ( Abc_NtkIsSopLogic(pNtk) )
- Abc_NtkSopToBdd(pNtk);
-*/
if ( Abc_NtkIsStrash(pNtk) )
{
- RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose );
+ clk = clock();
+ RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, fVerbose );
if ( RetValue == -1 )
- printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
+ printf( "UNDECIDED " );
else if ( RetValue == 0 )
- printf( "The miter is SATISFIABLE.\n" );
+ printf( "SATISFIABLE " );
else
- printf( "The miter is UNSATISFIABLE.\n" );
+ printf( "UNSATISFIABLE " );
+ //printf( "\n" );
+ PRT( "Time", clock() - clk );
}
else
{
Abc_Ntk_t * pTemp;
pTemp = Abc_NtkStrash( pNtk, 0, 0 );
- RetValue = Abc_NtkMiterSat( pTemp, nSeconds, fVerbose );
+ clk = clock();
+ RetValue = Abc_NtkMiterSat( pTemp, nConfLimit, nImpLimit, fVerbose );
if ( RetValue == -1 )
- printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
+ printf( "UNDECIDED " );
else if ( RetValue == 0 )
- printf( "The miter is SATISFIABLE.\n" );
+ printf( "SATISFIABLE " );
else
- printf( "The miter is UNSATISFIABLE.\n" );
+ printf( "UNSATISFIABLE " );
+ //printf( "\n" );
+ PRT( "Time", clock() - clk );
Abc_NtkDelete( pTemp );
}
return 0;
usage:
- fprintf( pErr, "usage: sat [-T num] [-vh]\n" );
+ fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" );
fprintf( pErr, "\t solves the combinational miter\n" );
- fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
+ fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+ fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -3109,8 +3234,8 @@ int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
@@ -3169,9 +3294,10 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
- Abc_Obj_t * pNode;
+ Abc_Obj_t * pNode, * pNodeCo;
int c;
int fUseAllCis;
+ int fUseMffc;
int Output;
pNtk = Abc_FrameReadNtk(pAbc);
@@ -3180,23 +3306,26 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fUseAllCis = 0;
+ fUseMffc = 0;
Output = -1;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Oah" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Omah" ) ) != EOF )
{
switch ( c )
{
case 'O':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-O\" should be followed by an integer.\n" );
goto usage;
}
- Output = atoi(argv[util_optind]);
- util_optind++;
+ Output = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( Output < 0 )
goto usage;
break;
+ case 'm':
+ fUseMffc ^= 1;
case 'a':
fUseAllCis ^= 1;
break;
@@ -3219,27 +3348,31 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( argc > util_optind + 1 )
+ if ( argc > globalUtilOptind + 1 )
{
fprintf( pErr, "Wrong number of auguments.\n" );
goto usage;
}
- if ( argc == util_optind + 1 )
+ if ( argc == globalUtilOptind + 1 )
{
- pNode = Abc_NtkFindCo( pNtk, argv[util_optind] );
+ pNodeCo = Abc_NtkFindCo( pNtk, argv[globalUtilOptind] );
+ pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
if ( pNode == NULL )
{
- fprintf( pErr, "Cannot find CO node \"%s\".\n", argv[util_optind] );
+ fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] );
return 1;
}
- pNtkRes = Abc_NtkCreateOutput( pNtk, pNode, fUseAllCis );
+ if ( fUseMffc )
+ pNtkRes = Abc_NtkCreateMffc( pNtk, pNode, argv[globalUtilOptind] );
+ else
+ pNtkRes = Abc_NtkCreateCone( pNtk, pNode, argv[globalUtilOptind], fUseAllCis );
}
else
{
if ( Output == -1 )
{
- fprintf( pErr, "The output is not specified.\n" );
+ fprintf( pErr, "The node is not specified.\n" );
return 1;
}
if ( Output >= Abc_NtkCoNum(pNtk) )
@@ -3247,11 +3380,17 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "The 0-based output number (%d) is larger than the number of outputs (%d).\n", Output, Abc_NtkCoNum(pNtk) );
return 1;
}
- pNtkRes = Abc_NtkCreateOutput( pNtk, Abc_NtkCo(pNtk,Output), fUseAllCis );
+ pNodeCo = Abc_NtkCo( pNtk, Output );
+ if ( fUseMffc )
+ pNtkRes = Abc_NtkCreateMffc( pNtk, Abc_ObjFanin0(pNodeCo), Abc_ObjName(pNodeCo) );
+ else
+ pNtkRes = Abc_NtkCreateCone( pNtk, Abc_ObjFanin0(pNodeCo), Abc_ObjName(pNodeCo), fUseAllCis );
}
+ if ( pNodeCo && Abc_ObjFaninC0(pNodeCo) )
+ printf( "The extracted cone represents the complement function of the CO.\n" );
if ( pNtkRes == NULL )
{
- fprintf( pErr, "Splitting one output has failed.\n" );
+ fprintf( pErr, "Writing the logic cone of one node has failed.\n" );
return 1;
}
// replace the current network
@@ -3259,12 +3398,13 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: one_output [-O num] [-ah] <name>\n" );
- fprintf( pErr, "\t replaces the current network by the logic cone of one output\n" );
+ fprintf( pErr, "usage: cone [-O num] [-amh] <name>\n" );
+ fprintf( pErr, "\t replaces the current network by one logic cone\n" );
fprintf( pErr, "\t-a : toggle writing all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" );
+ fprintf( pErr, "\t-m : toggle writing only MFFC or complete TFI cone [default = %s]\n", fUseMffc? "MFFC": "TFI cone" );
fprintf( pErr, "\t-h : print the command usage\n");
- fprintf( pErr, "\t-O num : (optional) the 0-based number of the output\n");
- fprintf( pErr, "\tname : (optional) the name of the output\n");
+ fprintf( pErr, "\t-O num : (optional) the 0-based number of the CO to extract\n");
+ fprintf( pErr, "\tname : (optional) the name of the node to extract\n");
return 1;
}
@@ -3291,8 +3431,8 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -3315,16 +3455,16 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( argc != util_optind + 1 )
+ if ( argc != globalUtilOptind + 1 )
{
fprintf( pErr, "Wrong number of auguments.\n" );
goto usage;
}
- pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+ pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
if ( pNode == NULL )
{
- fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+ fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] );
return 1;
}
@@ -3340,7 +3480,7 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: one_node [-h] <name>\n" );
+ fprintf( pErr, "usage: node [-h] <name>\n" );
fprintf( pErr, "\t replaces the current network by the network composed of one node\n" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tname : the node name\n");
@@ -3371,8 +3511,8 @@ int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -3420,8 +3560,8 @@ int Abc_CommandExdcFree( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -3480,8 +3620,8 @@ int Abc_CommandExdcGet( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -3538,8 +3678,8 @@ int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -3556,13 +3696,13 @@ int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( argc != util_optind + 1 )
+ if ( argc != globalUtilOptind + 1 )
{
goto usage;
}
// get the input file name
- FileName = argv[util_optind];
+ FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
@@ -3639,30 +3779,30 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
pParams->fDrop = 0; // drop cuts on the fly
pParams->fMulti = 0; // use multi-input AND-gates
pParams->fVerbose = 0; // the verbosiness flag
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "KMtfdmvoh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdmvoh" ) ) != EOF )
{
switch ( c )
{
case 'K':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
- pParams->nVarsMax = atoi(argv[util_optind]);
- util_optind++;
+ pParams->nVarsMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( pParams->nVarsMax < 0 )
goto usage;
break;
case 'M':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
- pParams->nKeepMax = atoi(argv[util_optind]);
- util_optind++;
+ pParams->nKeepMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( pParams->nKeepMax < 0 )
goto usage;
break;
@@ -3729,7 +3869,7 @@ usage:
fprintf( pErr, "\t-t : toggle truth table computation [default = %s]\n", pParams->fTruth? "yes": "no" );
fprintf( pErr, "\t-f : toggle filtering of duplicated/dominated [default = %s]\n", pParams->fFilter? "yes": "no" );
fprintf( pErr, "\t-d : toggle dropping when fanouts are done [default = %s]\n", pParams->fDrop? "yes": "no" );
- fprintf( pErr, "\t-m : toggle using multi-input AND-gates [default = %s]\n", pParams->fMulti? "yes": "no" );
+ fprintf( pErr, "\t-m : toggle computing only factor-cuts [default = %s]\n", pParams->fMulti? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", pParams->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -3767,30 +3907,30 @@ int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv )
pParams->fFilter = 1; // filter dominated cuts
pParams->fSeq = 1; // compute sequential cuts
pParams->fVerbose = 0; // the verbosiness flag
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "KMtvh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KMtvh" ) ) != EOF )
{
switch ( c )
{
case 'K':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
- pParams->nVarsMax = atoi(argv[util_optind]);
- util_optind++;
+ pParams->nVarsMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( pParams->nVarsMax < 0 )
goto usage;
break;
case 'M':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
- pParams->nKeepMax = atoi(argv[util_optind]);
- util_optind++;
+ pParams->nKeepMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( pParams->nKeepMax < 0 )
goto usage;
break;
@@ -3868,19 +4008,19 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
fVerbose = 0;
fUseInvs = 1;
nFaninMax = 128;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Nivh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Nivh" ) ) != EOF )
{
switch ( c )
{
case 'N':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
- nFaninMax = atoi(argv[util_optind]);
- util_optind++;
+ nFaninMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nFaninMax < 0 )
goto usage;
break;
@@ -3931,6 +4071,66 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandEspresso( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int fVerbose;
+ extern void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ fprintf( pErr, "SOP minimization is possible for logic networks (run \"renode\").\n" );
+ return 1;
+ }
+ Abc_NtkEspresso( pNtk, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: espresso [-vh]\n" );
+ fprintf( pErr, "\t minimizes SOPs of the local functions using Espresso\n" );
+ fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
@@ -3948,15 +4148,15 @@ 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_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -3984,8 +4184,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// run the command
// pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
-// pNtkRes = Abc_NtkNewAig( pNtk );
- pNtkRes = NULL;
+ pNtkRes = Abc_NtkNewAig( pNtk );
+// pNtkRes = NULL;
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -4044,41 +4244,41 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pParams->fTryProve = 0; // tries to solve the final miter
pParams->fVerbose = 0; // the verbosiness flag
pParams->fVerboseP = 0; // the verbosiness flag
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "RDBrscpvaeh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "RDBrscpvaeh" ) ) != EOF )
{
switch ( c )
{
case 'R':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
- pParams->nPatsRand = atoi(argv[util_optind]);
- util_optind++;
+ pParams->nPatsRand = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( pParams->nPatsRand < 0 )
goto usage;
break;
case 'D':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
- pParams->nPatsDyna = atoi(argv[util_optind]);
- util_optind++;
+ pParams->nPatsDyna = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( pParams->nPatsDyna < 0 )
goto usage;
break;
case 'B':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" );
goto usage;
}
- pParams->nBTLimit = atoi(argv[util_optind]);
- util_optind++;
+ pParams->nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( pParams->nBTLimit < 0 )
goto usage;
break;
@@ -4189,8 +4389,8 @@ int Abc_CommandFraigTrust( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fDuplicate = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
{
switch ( c )
{
@@ -4253,8 +4453,8 @@ int Abc_CommandFraigStore( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fDuplicate = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
{
switch ( c )
{
@@ -4314,8 +4514,8 @@ int Abc_CommandFraigRestore( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fDuplicate = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
{
switch ( c )
{
@@ -4378,8 +4578,8 @@ int Abc_CommandFraigClean( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fDuplicate = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
{
switch ( c )
{
@@ -4432,8 +4632,8 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
fUseInv = 1;
fExdc = 0;
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "ievh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ievh" ) ) != EOF )
{
switch ( c )
{
@@ -4521,19 +4721,19 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
fSweep = 1;
fSwitching = 0;
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Daspvh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Daspvh" ) ) != EOF )
{
switch ( c )
{
case 'D':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-D\" should be followed by a floating point number.\n" );
goto usage;
}
- DelayTarget = (float)atof(argv[util_optind]);
- util_optind++;
+ DelayTarget = (float)atof(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( DelayTarget <= 0.0 )
goto usage;
break;
@@ -4576,7 +4776,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, 0 );
+ pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 );
Abc_NtkDelete( pNtkRes );
if ( pNtk == NULL )
{
@@ -4652,8 +4852,8 @@ int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -4713,8 +4913,8 @@ int Abc_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -4776,8 +4976,8 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -4853,8 +5053,8 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
fSwitching = 0;
fVerbose = 0;
DelayTarget =-1;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "apvhD" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "apvhD" ) ) != EOF )
{
switch ( c )
{
@@ -4870,13 +5070,13 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'h':
goto usage;
case 'D':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-D\" should be followed by a floating point number.\n" );
goto usage;
}
- DelayTarget = (float)atof(argv[util_optind]);
- util_optind++;
+ DelayTarget = (float)atof(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( DelayTarget <= 0.0 )
goto usage;
break;
@@ -4906,7 +5106,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, 0 );
+ pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 );
Abc_NtkDelete( pNtkRes );
if ( pNtk == NULL )
{
@@ -4985,8 +5185,8 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
pParams->fSwitching = 0;
pParams->fDropCuts = 0;
pParams->fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "fapdvh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "fapdvh" ) ) != EOF )
{
switch ( c )
{
@@ -5029,7 +5229,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, 0 );
+ pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 );
Abc_NtkDelete( pNtkRes );
if ( pNtk == NULL )
{
@@ -5106,8 +5306,8 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
fOnes = 0;
fRandom = 0;
fDontCare = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "zordh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "zordh" ) ) != EOF )
{
switch ( c )
{
@@ -5211,19 +5411,19 @@ int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nLatches = 5;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Lh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Lh" ) ) != EOF )
{
switch ( c )
{
case 'L':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-L\" should be followed by a positive integer.\n" );
goto usage;
}
- nLatches = atoi(argv[util_optind]);
- util_optind++;
+ nLatches = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nLatches < 0 )
goto usage;
break;
@@ -5286,8 +5486,8 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -5364,8 +5564,8 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fShare = 1;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "sh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
{
switch ( c )
{
@@ -5445,19 +5645,19 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
fInitial = 1;
fVerbose = 0;
nMaxIters = 15;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Ifbivh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Ifbivh" ) ) != EOF )
{
switch ( c )
{
case 'I':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
goto usage;
}
- nMaxIters = atoi(argv[util_optind]);
- util_optind++;
+ nMaxIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nMaxIters < 0 )
goto usage;
break;
@@ -5568,19 +5768,19 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nMaxIters = 15;
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Ivh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
{
switch ( c )
{
case 'I':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
goto usage;
}
- nMaxIters = atoi(argv[util_optind]);
- util_optind++;
+ nMaxIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nMaxIters < 0 )
goto usage;
break;
@@ -5625,7 +5825,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0 );
+ pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0, 1 );
Abc_NtkDelete( pNtkRes );
if ( pNtkNew == NULL )
{
@@ -5692,19 +5892,19 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nMaxIters = 15;
fVerbose = 0;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Ivh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
{
switch ( c )
{
case 'I':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
goto usage;
}
- nMaxIters = atoi(argv[util_optind]);
- util_optind++;
+ nMaxIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nMaxIters < 0 )
goto usage;
break;
@@ -5749,7 +5949,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0 );
+ pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0, 1 );
Abc_NtkDelete( pNtkRes );
if ( pNtkNew == NULL )
{
@@ -5824,19 +6024,19 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
fExdc = 1;
fImp = 0;
fVerbose = 1;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Feivh" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Feivh" ) ) != EOF )
{
switch ( c )
{
case 'F':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
- nFrames = atoi(argv[util_optind]);
- util_optind++;
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nFrames <= 0 )
goto usage;
break;
@@ -5927,8 +6127,8 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
@@ -5983,8 +6183,10 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
int fSat;
int fVerbose;
int nSeconds;
+ int nConfLimit;
+ int nImpLimit;
- extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds );
+ extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit );
extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
@@ -5996,22 +6198,46 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
fSat = 0;
fVerbose = 0;
nSeconds = 20;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "Tsvh" ) ) != EOF )
+ nConfLimit = 10000;
+ nImpLimit = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "TCIsvh" ) ) != EOF )
{
switch ( c )
{
case 'T':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
- nSeconds = atoi(argv[util_optind]);
- util_optind++;
+ nSeconds = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nSeconds < 0 )
goto usage;
break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfLimit < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nImpLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nImpLimit < 0 )
+ goto usage;
+ break;
case 's':
fSat ^= 1;
break;
@@ -6023,14 +6249,14 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
- pArgvNew = argv + util_optind;
- nArgcNew = argc - util_optind;
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
return 1;
// perform equivalence checking
if ( fSat )
- Abc_NtkCecSat( pNtk1, pNtk2, nSeconds );
+ Abc_NtkCecSat( pNtk1, pNtk2, nConfLimit, nImpLimit );
else
Abc_NtkCecFraig( pNtk1, pNtk2, nSeconds, fVerbose );
@@ -6039,9 +6265,11 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: cec [-T num] [-svh] <file1> <file2>\n" );
+ fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-svh] <file1> <file2>\n" );
fprintf( pErr, "\t performs combinational equivalence checking\n" );
fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
+ fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+ fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@@ -6075,8 +6303,10 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerbose;
int nFrames;
int nSeconds;
+ int nConfLimit;
+ int nImpLimit;
- extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames );
+ extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit, int nFrames );
extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
@@ -6089,33 +6319,57 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
fVerbose = 0;
nFrames = 3;
nSeconds = 20;
- util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "FTsvh" ) ) != EOF )
+ nConfLimit = 10000;
+ nImpLimit = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
- nFrames = atoi(argv[util_optind]);
- util_optind++;
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nFrames <= 0 )
goto usage;
break;
case 'T':
- if ( util_optind >= argc )
+ if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
- nSeconds = atoi(argv[util_optind]);
- util_optind++;
+ nSeconds = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
if ( nSeconds < 0 )
goto usage;
break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfLimit < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nImpLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nImpLimit < 0 )
+ goto usage;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -6127,14 +6381,14 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
- pArgvNew = argv + util_optind;
- nArgcNew = argc - util_optind;
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
return 1;
// perform equivalence checking
if ( fSat )
- Abc_NtkSecSat( pNtk1, pNtk2, nSeconds, nFrames );
+ Abc_NtkSecSat( pNtk1, pNtk2, nConfLimit, nImpLimit, nFrames );
else
Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose );
@@ -6143,13 +6397,15 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: sec [-F num] [-T num] [-svh] <file1> <file2>\n" );
+ fprintf( pErr, "usage: sec [-F num] [-T num] [-C num] [-I num] [-svh] <file1> <file2>\n" );
fprintf( pErr, "\t performs bounded sequential equivalence checking\n" );
fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
+ fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+ fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
fprintf( pErr, "\t if no files are given, uses the current network and its spec\n");
@@ -6157,6 +6413,137 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkTemp;
+ int c;
+ int RetValue;
+ int fVerbose;
+ int fRewrite;
+ int fFraig;
+ int nConfLimit;
+ int nImpLimit;
+ int clk;
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fVerbose = 0;
+ fRewrite = 1;
+ fFraig = 1;
+ nConfLimit = 300000;
+ nImpLimit = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CIrfvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfLimit < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nImpLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nImpLimit < 0 )
+ goto usage;
+ break;
+ case 'r':
+ fRewrite ^= 1;
+ break;
+ case 'f':
+ fFraig ^= 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_NtkLatchNum(pNtk) > 0 )
+ {
+ fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
+ return 0;
+ }
+ if ( Abc_NtkCoNum(pNtk) != 1 )
+ {
+ fprintf( stdout, "Currently can only solve the miter with one output.\n" );
+ return 0;
+ }
+ if ( Abc_NtkIsSeq(pNtk) )
+ {
+ fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" );
+ return 0;
+ }
+
+ clk = clock();
+
+ if ( Abc_NtkIsStrash(pNtk) )
+ pNtkTemp = Abc_NtkDup( pNtk );
+ else
+ pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
+
+ RetValue = Abc_NtkMiterProve( &pNtkTemp, nConfLimit, nImpLimit, fRewrite, fFraig, fVerbose );
+ if ( RetValue == -1 )
+ printf( "UNDECIDED " );
+ else if ( RetValue == 0 )
+ printf( "SATISFIABLE " );
+ else
+ printf( "UNSATISFIABLE " );
+ //printf( "\n" );
+
+ PRT( "Time", clock() - clk );
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkTemp );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: prove [-C num] [-I num] [-rfvh]\n" );
+ fprintf( pErr, "\t solves combinational miter by rewriting, FRAIGing, and SAT\n" );
+ fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+ fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
+ fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
+ fprintf( pErr, "\t-f : toggle the use of FRAIGing [default = %s]\n", fFraig? "yes": "no" );
+ fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index effae853..919ea3b2 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -24,8 +24,8 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-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 void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective, bool fUpdateLevel );
+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, bool fUpdateLevel );
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 );
@@ -45,7 +45,7 @@ static void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk );
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective )
+Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, bool fUpdateLevel )
{
Abc_Ntk_t * pNtkAig;
assert( Abc_NtkIsStrash(pNtk) );
@@ -57,7 +57,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective )
}
// perform balancing
pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
- Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective );
+ Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective, fUpdateLevel );
Abc_NtkFinalize( pNtk, pNtkAig );
// undo the required times
if ( fSelective )
@@ -88,7 +88,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective )
SeeAlso []
***********************************************************************/
-void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective )
+void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective, bool fUpdateLevel )
{
int fCheck = 1;
ProgressBar * pProgress;
@@ -107,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, fSelective );
+ Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate, fSelective, fUpdateLevel );
}
Extra_ProgressBarStop( pProgress );
Vec_VecFree( vStorage );
@@ -115,38 +115,93 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
/**Function*************************************************************
- Synopsis [Randomizes the node positions.]
+ Synopsis [Finds the left bound on the next candidate to be paired.]
- Description []
+ Description [The nodes in the array are in the decreasing order of levels.
+ The last node in the array has the smallest level. By default it would be paired
+ with the next node on the left. However, it may be possible to pair it with some
+ other node on the left, in such a way that the new node is shared. This procedure
+ finds the index of the left-most node, which can be paired with the last node.]
SideEffects []
SeeAlso []
***********************************************************************/
-void Abc_NodeBalanceRandomize( Vec_Ptr_t * vSuper )
+int Abc_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
{
- Abc_Obj_t * pNode1, * pNode2;
- int i, Signature;
+ Abc_Obj_t * pNodeRight, * pNodeLeft;
+ int Current;
+ // if two or less nodes, pair with the first
if ( Vec_PtrSize(vSuper) < 3 )
+ return 0;
+ // set the pointer to the one before the last
+ Current = Vec_PtrSize(vSuper) - 2;
+ pNodeRight = Vec_PtrEntry( vSuper, Current );
+ // go through the nodes to the left of this one
+ for ( Current--; Current >= 0; Current-- )
+ {
+ // get the next node on the left
+ pNodeLeft = Vec_PtrEntry( vSuper, Current );
+ // if the level of this node is different, quit the loop
+ if ( Abc_ObjRegular(pNodeLeft)->Level != Abc_ObjRegular(pNodeRight)->Level )
+ break;
+ }
+ Current++;
+ // get the node, for which the equality holds
+ pNodeLeft = Vec_PtrEntry( vSuper, Current );
+ assert( Abc_ObjRegular(pNodeLeft)->Level == Abc_ObjRegular(pNodeRight)->Level );
+ return Current;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Moves closer to the end the node that is best for sharing.]
+
+ Description [If there is no node with sharing, randomly chooses one of
+ the legal nodes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeBalancePermute( Abc_Ntk_t * pNtkNew, Vec_Ptr_t * vSuper, int LeftBound )
+{
+ Abc_Obj_t * pNode1, * pNode2, * pNode3;
+ int RightBound, i;
+ // get the right bound
+ RightBound = Vec_PtrSize(vSuper) - 2;
+ assert( LeftBound <= RightBound );
+ if ( LeftBound == RightBound )
return;
- pNode1 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-2 );
- pNode2 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-3 );
- if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level )
- return;
- // some reordering will be performed
- Signature = rand();
- for ( i = Vec_PtrSize(vSuper)-2; i > 0; i-- )
+ // get the two last nodes
+ pNode1 = Vec_PtrEntry( vSuper, RightBound + 1 );
+ pNode2 = Vec_PtrEntry( vSuper, RightBound );
+ // find the first node that can be shared
+ for ( i = RightBound; i >= LeftBound; i-- )
+ {
+ pNode3 = Vec_PtrEntry( vSuper, i );
+ if ( Abc_AigAndLookup( pNtkNew->pManFunc, pNode1, pNode3 ) )
+ {
+ if ( pNode3 == pNode2 )
+ return;
+ Vec_PtrWriteEntry( vSuper, i, pNode2 );
+ Vec_PtrWriteEntry( vSuper, RightBound, pNode3 );
+ return;
+ }
+ }
+/*
+ // we did not find the node to share, randomize choice
{
- pNode1 = Vec_PtrEntry( vSuper, i );
- pNode2 = Vec_PtrEntry( vSuper, i-1 );
- if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level )
+ int Choice = rand() % (RightBound - LeftBound + 1);
+ pNode3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
+ if ( pNode3 == pNode2 )
return;
- if ( Signature & (1 << (i % 10)) )
- continue;
- Vec_PtrWriteEntry( vSuper, i, pNode2 );
- Vec_PtrWriteEntry( vSuper, i-1, pNode1 );
+ Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pNode2 );
+ Vec_PtrWriteEntry( vSuper, RightBound, pNode3 );
}
+*/
}
/**Function*************************************************************
@@ -160,12 +215,12 @@ 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, bool fSelective )
+Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate, bool fSelective, bool fUpdateLevel )
{
Abc_Aig_t * pMan = pNtkNew->pManFunc;
Abc_Obj_t * pNodeNew, * pNode1, * pNode2;
Vec_Ptr_t * vSuper;
- int i;
+ int i, LeftBound;
assert( !Abc_ObjIsComplement(pNodeOld) );
// return if the result if known
if ( pNodeOld->pCopy )
@@ -181,7 +236,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, fSelective );
+ pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate, fSelective, fUpdateLevel );
vSuper->pArray[i] = Abc_ObjNotCond( pNodeNew, Abc_ObjIsComplement(vSuper->pArray[i]) );
}
if ( vSuper->nSize < 2 )
@@ -192,8 +247,10 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
assert( vSuper->nSize > 1 );
while ( vSuper->nSize > 1 )
{
- // randomize the node positions
-// Abc_NodeBalanceRandomize( vSuper );
+ // find the left bound on the node to be paired
+ LeftBound = (!fUpdateLevel)? 0 : Abc_NodeBalanceFindLeft( vSuper );
+ // find the node that can be shared (if no such node, randomize choice)
+ Abc_NodeBalancePermute( pNtkNew, vSuper, LeftBound );
// pull out the last two nodes
pNode1 = Vec_PtrPop(vSuper);
pNode2 = Vec_PtrPop(vSuper);
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcClpBdd.c
index 59c76e09..59c76e09 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcClpBdd.c
diff --git a/src/base/abci/abcClpSop.c b/src/base/abci/abcClpSop.c
new file mode 100644
index 00000000..de92243f
--- /dev/null
+++ b/src/base/abci/abcClpSop.c
@@ -0,0 +1,53 @@
+/**CFile****************************************************************
+
+ FileName [abcCollapse.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Collapsing the network into two-levels.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcCollapse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Collapses the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCollapseSop( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ Abc_Ntk_t * pNtkNew;
+ pNtkNew = NULL;
+ return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 3e34602d..1ee9a712 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -57,10 +57,41 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
assert( Abc_NtkIsStrash(pNtk) );
-
+/*
if ( pParams->fMulti )
- Abc_NtkBalanceAttach(pNtk);
-
+ {
+ Abc_Obj_t * pNode, * pNodeA, * pNodeB, * pNodeC;
+ int nFactors;
+ // lebel the nodes, which will be the roots of factor-cuts
+ // mark the multiple-fanout nodes
+ Abc_AigForEachAnd( pNtk, pNode, i )
+ if ( pNode->vFanouts.nSize > 1 )
+ pNode->fMarkB = 1;
+ // unmark the control inputs of MUXes and inputs of EXOR gates
+ Abc_AigForEachAnd( pNtk, pNode, i )
+ {
+ if ( !Abc_NodeIsMuxType(pNode) )
+ continue;
+
+ pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeA, &pNodeB );
+ // if real children are used, skip
+ if ( Abc_ObjFanin0(pNode)->vFanouts.nSize > 1 || Abc_ObjFanin1(pNode)->vFanouts.nSize > 1 )
+ continue;
+
+ if ( pNodeC->vFanouts.nSize == 2 )
+ pNodeC->fMarkB = 0;
+ if ( Abc_ObjRegular(pNodeA) == Abc_ObjRegular(pNodeB) && Abc_ObjRegular(pNodeA)->vFanouts.nSize == 2 )
+ Abc_ObjRegular(pNodeA)->fMarkB = 0;
+ }
+ // mark the PO drivers
+// Abc_NtkForEachCo( pNtk, pNode, i )
+// Abc_ObjFanin0(pNode)->fMarkB = 1;
+ nFactors = 0;
+ Abc_AigForEachAnd( pNtk, pNode, i )
+ nFactors += pNode->fMarkB;
+ printf( "Total nodes = %6d. Total factors = %6d.\n", Abc_NtkNodeNum(pNtk), nFactors );
+ }
+*/
// start the manager
pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
p = Cut_ManStart( pParams );
@@ -104,8 +135,13 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
}
Vec_PtrFree( vNodes );
Vec_IntFree( vChoices );
+/*
if ( pParams->fMulti )
- Abc_NtkBalanceDetach(pNtk);
+ {
+ Abc_NtkForEachObj( pNtk, pNode, i )
+ pNode->fMarkB = 0;
+ }
+*/
PRT( "Total", clock() - clk );
//Abc_NtkPrintCuts_( p, pNtk, 0 );
// Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
@@ -282,14 +318,14 @@ printf( "Converged after %d iterations.\n", nIters );
SeeAlso []
***********************************************************************/
-void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj )
+void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti )
{
void * pList;
if ( pList = Abc_NodeReadCuts( p, pObj ) )
return pList;
- Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj) );
- Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj) );
- return Abc_NodeGetCuts( p, pObj, 0 );
+ Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fMulti );
+ Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fMulti );
+ return Abc_NodeGetCuts( p, pObj, fMulti );
}
/**Function*************************************************************
@@ -305,7 +341,8 @@ void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj )
***********************************************************************/
void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti )
{
- int fTriv = (!fMulti) || (pObj->pCopy != NULL);
+// int fTriv = (!fMulti) || pObj->fMarkB;
+ int fTriv = (!fMulti) || (pObj->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pObj));
assert( Abc_NtkIsStrash(pObj->pNtk) );
assert( Abc_ObjFaninNum(pObj) == 2 );
return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index a73ab2b5..9dd5ea3a 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -446,7 +446,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
/**Function*************************************************************
- Synopsis [Performs decomposition of one node.]
+ Synopsis [Checks if the node should be decomposed by DSD.]
Description []
diff --git a/src/base/abci/abcEspresso.c b/src/base/abci/abcEspresso.c
new file mode 100644
index 00000000..ee6598c9
--- /dev/null
+++ b/src/base/abci/abcEspresso.c
@@ -0,0 +1,244 @@
+/**CFile****************************************************************
+
+ FileName [abcEspresso.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Procedures to minimize SOPs using Espresso.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcEspresso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "espresso.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NodeEspresso( Abc_Obj_t * pNode );
+static pset_family Abc_SopToEspresso( char * pSop );
+static char * Abc_SopFromEspresso( Extra_MmFlex_t * pMan, pset_family Cover );
+static pset_family Abc_EspressoMinimize( pset_family pOnset, pset_family pDcset );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Minimizes SOP representations using Espresso.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ Abc_Obj_t * pNode;
+ int i;
+ assert( Abc_NtkIsLogic(pNtk) );
+ // convert the network to have SOPs
+ if ( Abc_NtkHasMapping(pNtk) )
+ Abc_NtkUnmap(pNtk);
+ else if ( Abc_NtkHasBdd(pNtk) )
+ Abc_NtkBddToSop(pNtk);
+ // minimize SOPs of all nodes
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ if ( i ) Abc_NodeEspresso( pNode );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Minimizes SOP representation of one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeEspresso( Abc_Obj_t * pNode )
+{
+ extern void define_cube_size( int n );
+ pset_family Cover;
+ int fCompl;
+
+ assert( Abc_ObjIsNode(pNode) );
+ // define the cube for this node
+ define_cube_size( Abc_ObjFaninNum(pNode) );
+ // create the Espresso cover
+ fCompl = Abc_SopIsComplement( pNode->pData );
+ Cover = Abc_SopToEspresso( pNode->pData );
+ // perform minimization
+ Cover = Abc_EspressoMinimize( Cover, NULL ); // deletes also cover
+ // convert back onto the node's SOP representation
+ pNode->pData = Abc_SopFromEspresso( pNode->pNtk->pManFunc, Cover );
+ if ( fCompl ) Abc_SopComplement( pNode->pData );
+ sf_free(Cover);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts SOP in ABC into SOP representation in Espresso.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+pset_family Abc_SopToEspresso( char * pSop )
+{
+ char * pCube;
+ pset_family Cover;
+ pset set;
+ int nCubes, nVars, Value, v;
+
+ if ( pSop == NULL )
+ return NULL;
+
+ nVars = Abc_SopGetVarNum(pSop);
+ nCubes = Abc_SopGetCubeNum(pSop);
+ assert( cube.size == 2 * nVars );
+
+ if ( Abc_SopIsConst0(pSop) )
+ {
+ Cover = sf_new(0, cube.size);
+ return Cover;
+ }
+ if ( Abc_SopIsConst1(pSop) )
+ {
+ Cover = sf_new(1, cube.size);
+ set = GETSET(Cover, Cover->count++);
+ set_copy( set, cube.fullset );
+ return Cover;
+ }
+
+ // create the cover
+ Cover = sf_new(nCubes, cube.size);
+ // fill in the cubes
+ Abc_SopForEachCube( pSop, nVars, pCube )
+ {
+ set = GETSET(Cover, Cover->count++);
+ set_copy( set, cube.fullset );
+ Abc_CubeForEachVar( pCube, Value, v )
+ {
+ if ( Value == '0' )
+ set_remove(set, 2*v+1);
+ else if ( Value == '1' )
+ set_remove(set, 2*v);
+ }
+ }
+ return Cover;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts SOP representation in Espresso into SOP in ABC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Abc_SopFromEspresso( Extra_MmFlex_t * pMan, pset_family Cover )
+{
+ pset set;
+ char * pSop, * pCube;
+ int Lit, nVars, nCubes, i, k;
+
+ nVars = Cover->sf_size/2;
+ nCubes = Cover->count;
+
+ pSop = Abc_SopStart( pMan, nCubes, nVars );
+
+ // go through the cubes
+ i = 0;
+ Abc_SopForEachCube( pSop, nVars, pCube )
+ {
+ set = GETSET(Cover, i++);
+ for ( k = 0; k < nVars; k++ )
+ {
+ Lit = GETINPUT(set, k);
+ if ( Lit == ZERO )
+ pCube[k] = '0';
+ else if ( Lit == ONE )
+ pCube[k] = '1';
+ }
+ }
+ return pSop;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Minimizes the cover using Espresso.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+pset_family Abc_EspressoMinimize( pset_family pOnset, pset_family pDcset )
+{
+ pset_family pOffset;
+ int fNewDcset, i;
+ int fSimple = 0;
+ int fSparse = 0;
+
+ if ( fSimple )
+ {
+ for ( i = 0; i < cube.num_vars; i++ )
+ pOnset = d1merge( pOnset, i );
+ pOnset = sf_contain( pOnset );
+ return pOnset;
+ }
+
+ // create the dcset
+ fNewDcset = (pDcset == NULL);
+ if ( pDcset == NULL )
+ pDcset = sf_new( 1, cube.size );
+ pDcset->wsize = pOnset->wsize;
+ pDcset->sf_size = pOnset->sf_size;
+
+ // derive the offset
+ if ( pDcset->sf_size == 0 || pDcset->count == 0 )
+ pOffset = complement(cube1list(pOnset));
+ else
+ pOffset = complement(cube2list(pOnset, pDcset));
+
+ // perform minimization
+ skip_make_sparse = !fSparse;
+ pOnset = espresso( pOnset, pDcset, pOffset );
+
+ // free covers
+ sf_free( pOffset );
+ if ( fNewDcset )
+ sf_free( pDcset );
+ return pOnset;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index d59f21a0..4aae6ba5 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -26,7 +26,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
static Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
static Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
static void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs );
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 128e054a..39bf15aa 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/abcMiter.c b/src/base/abci/abcMiter.c
index 44130a20..30fc3a79 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -90,7 +90,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
// start the new network
pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
- pNtkMiter->pName = util_strsav(Buffer);
+ pNtkMiter->pName = Extra_UtilStrsav(Buffer);
// perform strashing
Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb );
@@ -308,7 +308,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
// start the new network
pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
sprintf( Buffer, "%s_miter", Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
- pNtkMiter->pName = util_strsav(Buffer);
+ pNtkMiter->pName = Extra_UtilStrsav(Buffer);
// get the root output
pRoot = Abc_NtkCo( pNtk, Out );
@@ -372,7 +372,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
// start the new network
pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
- pNtkMiter->pName = util_strsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) );
+ pNtkMiter->pName = Extra_UtilStrsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) );
// get the root output
pRoot = Abc_NtkCo( pNtk, 0 );
@@ -384,14 +384,16 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
// add the first cofactor
Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
// save the output
- pOutput1 = Abc_ObjFanin0(pRoot)->pCopy;
+// pOutput1 = Abc_ObjFanin0(pRoot)->pCopy;
+ pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) );
// set the second cofactor
Abc_NtkCi(pNtk, In)->pCopy = Abc_NtkConst1( pNtkMiter );
// add the second cofactor
Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
// save the output
- pOutput2 = Abc_ObjFanin0(pRoot)->pCopy;
+// pOutput2 = Abc_ObjFanin0(pRoot)->pCopy;
+ pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) );
// create the miter of the two outputs
if ( fExist )
@@ -461,7 +463,7 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter )
assert( Abc_NtkIsStrash(pMiter) );
Abc_NtkForEachPo( pMiter, pNodePo, i )
{
- pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,i) );
+ pChild = Abc_ObjChild0( pNodePo );
if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_NodeIsConst(pChild) )
{
assert( Abc_ObjRegular(pChild) == Abc_NtkConst1(pMiter) );
@@ -552,7 +554,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
// start the new network
pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
- pNtkFrames->pName = util_strsav(Buffer);
+ pNtkFrames->pName = Extra_UtilStrsav(Buffer);
// create new latches (or their initial values) and remember them in the new latches
if ( !fInitial )
{
@@ -682,7 +684,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram
// start the new network
pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
- pNtkFrames->pName = util_strsav(Buffer);
+ pNtkFrames->pName = Extra_UtilStrsav(Buffer);
// create new latches (or their initial values) and remember them in the new latches
if ( !fInitial )
{
diff --git a/src/base/abci/abcNewAig.c b/src/base/abci/abcNewAig.c
index 33f58135..ce76195a 100644
--- a/src/base/abci/abcNewAig.c
+++ b/src/base/abci/abcNewAig.c
@@ -56,9 +56,11 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk )
{
Aig_Man_t * pMan;
Abc_Ntk_t * pNtkAig;
- Aig_ProofType_t RetValue;
+// Aig_ProofType_t RetValue;
int fCleanup = 1;
int nNodes;
+ extern void Aig_MffcTest( Aig_Man_t * pMan );
+
assert( !Abc_NtkIsNetlist(pNtk) );
assert( !Abc_NtkIsSeq(pNtk) );
@@ -70,6 +72,10 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk )
// convert to the AIG manager
pMan = Abc_NtkToAig( pNtk );
+
+ Aig_MffcTest( pMan );
+
+/*
// execute a command in the AIG manager
RetValue = Aig_FraigProve( pMan );
if ( RetValue == AIG_PROOF_SAT )
@@ -80,6 +86,7 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk )
printf( "Undecided.\n" );
else
assert( 0 );
+*/
// convert from the AIG manager
pNtkAig = Abc_NtkFromAig( pNtk, pMan );
@@ -173,6 +180,8 @@ Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld )
Abc_NtkConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
Abc_NtkForEachCi( pNtkOld, pObj, i )
pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePi(pMan);
+ Abc_NtkForEachCo( pNtkOld, pObj, i )
+ pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePo(pMan);
// perform the conversion of the internal nodes
Abc_NtkStrashPerformAig( pNtkOld, pMan );
// create the POs
@@ -180,7 +189,7 @@ Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld )
{
pFanin = (Aig_Node_t *)Abc_ObjFanin0(pObj)->pCopy;
pFanin = Aig_NotCond( pFanin, Abc_ObjFaninC0(pObj) );
- pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePo( pMan, pFanin );
+ Aig_NodeConnectPo( pMan, (Aig_Node_t *)pObj->pCopy, pFanin );
}
return pMan;
}
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 6257bd08..b961ec15 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -79,7 +79,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo
// start the network
pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
- pNtk->pName = util_strsav(pNamePo);
+ pNtk->pName = Extra_UtilStrsav(pNamePo);
// make sure the new manager has enough inputs
Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) );
// add the PIs corresponding to the names
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
new file mode 100644
index 00000000..18ee9a3f
--- /dev/null
+++ b/src/base/abci/abcProve.c
@@ -0,0 +1,232 @@
+/**CFile****************************************************************
+
+ FileName [abcProve.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Proves the miter using AIG rewriting, FRAIGing, and SAT solving.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose );
+extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
+extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+
+static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue );
+static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Attempts to solve the miter using a number of tricks.]
+
+ Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT. Returns
+ a simplified version of the original network (or a constant 0 network).
+ In case the network is not a constant zero and a SAT assignment is found,
+ pNtk->pModel contains a satisfying assignment.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose )
+{
+ Abc_Ntk_t * pNtk, * pNtkTemp;
+ int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2;
+ int nConfs, nImps, nBTLimit, RetValue;
+ int nIter = 0, clk, timeStart = clock();
+
+ // get the starting network
+ pNtk = *ppNtk;
+ assert( Abc_NtkIsStrash(pNtk) );
+ assert( Abc_NtkPoNum(pNtk) == 1 );
+
+ // set the initial limits
+ nConfs = !nConfLimit? nConfsStart : ABC_MIN( nConfsStart, nConfLimit );
+ nImps = !nImpLimit ? nImpsStart : ABC_MIN( nImpsStart , nImpLimit );
+ nBTLimit = nBTLimitStart;
+
+ if ( fVerbose )
+ printf( "Global resource limits: ConfsLim = %6d. ImpsLim = %d.\n", nConfLimit, nImpLimit );
+
+ // if SAT only, solve without iteration
+ if ( !fUseRewrite && !fUseFraig )
+ {
+ clk = clock();
+ RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 );
+ Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+ *ppNtk = pNtk;
+ return RetValue;
+ }
+
+ // check the current resource limits
+ do {
+ nIter++;
+
+ if ( fVerbose )
+ printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter, nConfs, nBTLimit );
+
+ // try brute-force SAT
+ clk = clock();
+ RetValue = Abc_NtkMiterSat( pNtk, nConfs, nImps, 0 );
+ Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+ if ( RetValue >= 0 )
+ break;
+
+ if ( fUseRewrite )
+ {
+ clk = clock();
+
+ // try rewriting
+ Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+ break;
+ Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+ if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+ break;
+ pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp );
+ if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+ break;
+
+ Abc_NtkMiterPrint( pNtk, "Rewriting ", clk, fVerbose );
+ }
+
+ if ( fUseFraig )
+ {
+ // try FRAIGing
+ clk = clock();
+ pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue ); Abc_NtkDelete( pNtkTemp );
+ Abc_NtkMiterPrint( pNtk, "FRAIGing ", clk, fVerbose );
+ if ( RetValue >= 0 )
+ break;
+ }
+
+ // increase resource limits
+ nConfs = ABC_MIN( nConfs * 3 / 2, 1000000000 );
+ nImps = ABC_MIN( nImps * 3 / 2, 1000000000 );
+ nBTLimit = ABC_MIN( nBTLimit * 8, 1000000000 );
+
+ // timeout at 5 minutes
+ if ( clock() - timeStart >= 300 * CLOCKS_PER_SEC )
+ break;
+ if ( nIter == 4 )
+ break;
+ }
+ while ( (nConfLimit == 0 || nConfs <= nConfLimit) &&
+ (nImpLimit == 0 || nImps <= nImpLimit ) );
+
+ // try to prove it using brute force SAT
+ if ( RetValue < 0 )
+ {
+ clk = clock();
+ RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 );
+ Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+ }
+
+ *ppNtk = pNtk;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Attempts to solve the miter using a number of tricks.]
+
+ Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue )
+{
+ Abc_Ntk_t * pNtkNew;
+ Fraig_Params_t Params, * pParams = &Params;
+ Fraig_Man_t * pMan;
+ int nWords1, nWords2, nWordsMin, RetValue;
+ int * pModel;
+
+ // to determine the number of simulation patterns
+ // use the following strategy
+ // at least 64 words (32 words random and 32 words dynamic)
+ // no more than 256M for one circuit (128M + 128M)
+ nWords1 = 32;
+ nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
+ nWordsMin = ABC_MIN( nWords1, nWords2 );
+
+ // set the FRAIGing parameters
+ Fraig_ParamsSetDefault( pParams );
+ pParams->nPatsRand = nWordsMin * 32; // the number of words of random simulation info
+ pParams->nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info
+ pParams->nBTLimit = nBTLimit; // the max number of backtracks
+ pParams->nSeconds = -1; // the runtime limit
+ pParams->fTryProve = 0; // do not try to prove the final miter
+ pParams->fDoSparse = 1; // try proving sparse functions
+ pParams->fVerbose = 0;
+
+ // transform the target into a fraig
+ pMan = Abc_NtkToFraig( pNtk, pParams, 0, 0 );
+ Fraig_ManProveMiter( pMan );
+ RetValue = Fraig_ManCheckMiter( pMan );
+
+ // save model
+ if ( RetValue == 0 )
+ {
+ pModel = Fraig_ManReadModel( pMan );
+ FREE( pNtk->pModel );
+ pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
+ memcpy( pNtk->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtk) );
+ }
+ // create the network
+ pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
+ // delete the fraig manager
+ Fraig_ManFree( pMan );
+ *pRetValue = RetValue;
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Attempts to solve the miter using a number of tricks.]
+
+ Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose )
+{
+ if ( !fVerbose )
+ return;
+ printf( "Nodes = %7d. Levels = %4d. ", Abc_NtkNodeNum(pNtk), Abc_AigGetLevelNum(pNtk) );
+ PRT( pString, clock() - clk );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index ea2f808c..cfb05aee 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -407,7 +407,7 @@ void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax )
continue;
if ( pNode->fMarkA == 0 )
continue;
- // continue cutting branches ntil it meets the fanin limit
+ // continue cutting branches until it meets the fanin limit
while ( Abc_NtkRenodeLimit(pNode, vCone, nFaninMax) );
assert( vCone->nSize <= nFaninMax );
}
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
new file mode 100644
index 00000000..0b4c80c8
--- /dev/null
+++ b/src/base/abci/abcRestruct.c
@@ -0,0 +1,1026 @@
+/**CFile****************************************************************
+
+ FileName [abcRestruct.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: abcRestruct.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dec.h"
+#include "dsd.h"
+#include "cut.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_ManRst_t_ Abc_ManRst_t;
+struct Abc_ManRst_t_
+{
+ // the network
+ Abc_Ntk_t * pNtk; // the network for restructuring
+ // user specified parameters
+ int nCutMax; // the limit on the size of the supernode
+ int fUpdateLevel; // turns on watching the number of levels
+ int fUseZeros; // turns on zero-cost replacements
+ int fVerbose; // the verbosity flag
+ // internal data structures
+ DdManager * dd; // the BDD manager
+ Dsd_Manager_t * pManDsd; // the DSD manager
+ Vec_Ptr_t * vVisited; // temporary
+ Vec_Ptr_t * vLeaves; // temporary
+ Vec_Ptr_t * vDecs; // temporary
+ // node statistics
+ int nLastGain;
+ int nCutsConsidered;
+ int nCutsExplored;
+ int nNodesConsidered;
+ int nNodesRestructured;
+ int nNodesGained;
+ // runtime statistics
+ int timeCut;
+ int timeBdd;
+ int timeDsd;
+ int timeEval;
+ int timeRes;
+ int timeNtk;
+ int timeTotal;
+};
+
+static Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCutList );
+static Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCut );
+static Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, Abc_Obj_t * pRoot, int Required, int nNodesSaved, int * pnNodesAdded );
+
+static Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fMulti );
+static Abc_ManRst_t * Abc_NtkManRstStart( int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose );
+static void Abc_NtkManRstStop( Abc_ManRst_t * p );
+static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Implements AIG restructuring.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose )
+{
+ ProgressBar * pProgress;
+ Abc_ManRst_t * pManRst;
+ Cut_Man_t * pManCut;
+ Cut_Cut_t * pCutList;
+ Dec_Graph_t * pGraph;
+ Abc_Obj_t * pNode;
+ int clk, clkStart = clock();
+ int fMulti = 1;
+ int i, nNodes;
+
+ assert( Abc_NtkIsStrash(pNtk) );
+ // cleanup the AIG
+ Abc_AigCleanup(pNtk->pManFunc);
+ Abc_NtkCleanCopy(pNtk);
+
+ // compute the reverse levels if level update is requested
+ if ( fUpdateLevel )
+ Abc_NtkStartReverseLevels( pNtk );
+
+ // start the restructuring manager
+ pManRst = Abc_NtkManRstStart( nCutMax, fUpdateLevel, fUseZeros, fVerbose );
+ pManRst->pNtk = pNtk;
+ // start the cut manager
+clk = clock();
+ pManCut = Abc_NtkStartCutManForRestruct( pNtk, nCutMax, fMulti );
+pManRst->timeCut += clock() - clk;
+// pNtk->pManCut = pManCut;
+
+ // resynthesize each node once
+ nNodes = Abc_NtkObjNumMax(pNtk);
+ pProgress = Extra_ProgressBarStart( stdout, nNodes );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ // skip the constant node
+ if ( Abc_NodeIsConst(pNode) )
+ continue;
+ // skip the node if it is inside the tree
+// if ( Abc_ObjFanoutNum(pNode) < 2 )
+// continue;
+ // skip the nodes with too many fanouts
+ if ( Abc_ObjFanoutNum(pNode) > 1000 )
+ continue;
+ // stop if all nodes have been tried once
+ if ( i >= nNodes )
+ break;
+ // get the cuts for the given node
+clk = clock();
+ pCutList = Abc_NodeGetCutsRecursive( pManCut, pNode, fMulti );
+pManRst->timeCut += clock() - clk;
+ // evaluate these cuts
+clk = clock();
+ pGraph = Abc_NodeRestructure( pManRst, pNode, pCutList );
+pManRst->timeRes += clock() - clk;
+ if ( pGraph == NULL )
+ continue;
+ // acceptable replacement found, update the graph
+clk = clock();
+ Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, pManRst->nLastGain );
+pManRst->timeNtk += clock() - clk;
+ Dec_GraphFree( pGraph );
+ }
+ Extra_ProgressBarStop( pProgress );
+pManRst->timeTotal = clock() - clkStart;
+
+ // print statistics of the manager
+// if ( fVerbose )
+ Abc_NtkManRstPrintStats( pManRst );
+ // delete the managers
+ Cut_ManStop( pManCut );
+ Abc_NtkManRstStop( pManRst );
+ // put the nodes into the DFS order and reassign their IDs
+ Abc_NtkReassignIds( pNtk );
+// Abc_AigCheckFaninOrder( pNtk->pManFunc );
+ // fix the levels
+ if ( fUpdateLevel )
+ Abc_NtkStopReverseLevels( pNtk );
+ else
+ Abc_NtkGetLevelNum( pNtk );
+ // check
+ if ( !Abc_NtkCheck( pNtk ) )
+ {
+ printf( "Abc_NtkRefactor: The network check has failed.\n" );
+ return 0;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_RestructNodeDivisors( Abc_ManRst_t * p, Abc_Obj_t * pRoot )
+{
+ Abc_Obj_t * pNode, * pFanin, * pFanout;
+ int i, k;
+ // start with the leaves
+ Vec_PtrClear( p->vDecs );
+ Vec_PtrForEachEntry( p->vLeaves, pNode, i )
+ {
+ Vec_PtrPush( p->vDecs, pNode );
+ assert( pNode->fMarkC == 0 );
+ pNode->fMarkC = 1;
+ }
+ // explore the fanouts
+ Vec_PtrForEachEntry( p->vDecs, pNode, i )
+ {
+ // if the fanout has both fanins in the set, add it
+ Abc_ObjForEachFanout( pNode, pFanout, k )
+ {
+ if ( pFanout->fMarkC || Abc_ObjIsPo(pFanout) )
+ continue;
+ if ( Abc_ObjFanin0(pFanout)->fMarkC && Abc_ObjFanin1(pFanout)->fMarkC )
+ {
+ Vec_PtrPush( p->vDecs, pFanout );
+ pFanout->fMarkC = 1;
+ }
+ }
+ }
+ // unmark the nodes
+ Vec_PtrForEachEntry( p->vDecs, pNode, i )
+ pNode->fMarkC = 0;
+ // print the nodes
+ Vec_PtrForEachEntryStart( p->vDecs, pNode, i, Vec_PtrSize(p->vLeaves) )
+ {
+ printf( "%2d %s = ", i, Abc_NodeIsTravIdCurrent(pNode)? "*" : " " );
+ // find the first fanin
+ Vec_PtrForEachEntry( p->vDecs, pFanin, k )
+ if ( Abc_ObjFanin0(pNode) == pFanin )
+ break;
+ if ( k < Vec_PtrSize(p->vLeaves) )
+ printf( "%c", 'a' + k );
+ else
+ printf( "%d", k );
+ printf( "%s ", Abc_ObjFaninC0(pNode)? "\'" : "" );
+ // find the second fanin
+ Vec_PtrForEachEntry( p->vDecs, pFanin, k )
+ if ( Abc_ObjFanin1(pNode) == pFanin )
+ break;
+ if ( k < Vec_PtrSize(p->vLeaves) )
+ printf( "%c", 'a' + k );
+ else
+ printf( "%d", k );
+ printf( "%s ", Abc_ObjFaninC1(pNode)? "\'" : "" );
+ printf( "\n" );
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Starts the cut manager for rewriting.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCutList )
+{
+ Dec_Graph_t * pGraph;
+ Cut_Cut_t * pCut;
+ int nCuts;
+ p->nNodesConsidered++;
+
+ // count the number of cuts with four inputs or more
+ nCuts = 0;
+ for ( pCut = pCutList; pCut; pCut = pCut->pNext )
+ nCuts += (int)(pCut->nLeaves > 3);
+ printf( "-----------------------------------\n" );
+ printf( "Node %6d : Factor-cuts = %5d.\n", pNode->Id, nCuts );
+
+ // go through the interesting cuts
+ for ( pCut = pCutList; pCut; pCut = pCut->pNext )
+ {
+ if ( pCut->nLeaves < 4 )
+ continue;
+ if ( pGraph = Abc_NodeRestructureCut( p, pNode, pCut ) )
+ return pGraph;
+ }
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the cut manager for rewriting.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut )
+{
+ Dec_Graph_t * pGraph;
+ Dsd_Node_t * pNodeDsd;
+ Abc_Obj_t * pLeaf;
+ DdNode * bFunc;
+ int nNodesSaved, nNodesAdded;
+ int Required, nMaxSize, clk, i;
+ int fVeryVerbose = 0;
+
+ p->nCutsConsidered++;
+
+ // get the required time for the node
+ Required = p->fUpdateLevel? Abc_NodeReadRequiredLevel(pRoot) : ABC_INFINITY;
+
+ // collect the leaves of the cut
+ Vec_PtrClear( p->vLeaves );
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ {
+ pLeaf = Abc_NtkObj(pRoot->pNtk, pCut->pLeaves[i]);
+ if ( pLeaf == NULL ) // the so-called "bad cut phenomenon" is due to removed nodes
+ return NULL;
+ Vec_PtrPush( p->vLeaves, pLeaf );
+ }
+clk = clock();
+ // collect the internal nodes of the cut
+ Abc_NodeConeCollect( &pRoot, 1, p->vLeaves, p->vVisited, 0 );
+ // derive the BDD of the cut
+ bFunc = Abc_NodeConeBdd( p->dd, p->dd->vars, pRoot, p->vLeaves, p->vVisited ); Cudd_Ref( bFunc );
+p->timeBdd += clock() - clk;
+
+ // consider the special case, when the function is a constant
+ if ( Cudd_IsConstant(bFunc) )
+ {
+ p->nLastGain = Abc_NodeMffcSize( pRoot );
+ p->nNodesGained += p->nLastGain;
+ p->nNodesRestructured++;
+ Cudd_RecursiveDeref( p->dd, bFunc );
+ if ( Cudd_IsComplement(bFunc) )
+ return Dec_GraphCreateConst0();
+ return Dec_GraphCreateConst1();
+ }
+
+clk = clock();
+ // try disjoint support decomposition
+ pNodeDsd = Dsd_DecomposeOne( p->pManDsd, bFunc );
+p->timeDsd += clock() - clk;
+
+
+ // skip nodes with non-decomposable blocks
+ Dsd_TreeNodeGetInfoOne( pNodeDsd, NULL, &nMaxSize );
+ if ( nMaxSize > 3 )
+ {
+ Cudd_RecursiveDeref( p->dd, bFunc );
+ return NULL;
+ }
+/*
+ // skip nodes that cannot be improved
+ if ( Vec_PtrSize(p->vVisited) <= Dsd_TreeGetAigCost(pNodeDsd) )
+ {
+ Cudd_RecursiveDeref( p->dd, bFunc );
+ return NULL;
+ }
+*/
+
+ p->nCutsExplored++;
+
+ // mark the fanin boundary
+ // (can mark only essential fanins, belonging to bNodeFunc!)
+ Vec_PtrForEachEntry( p->vLeaves, pLeaf, i )
+ pLeaf->vFanouts.nSize++;
+ // label MFFC with current traversal ID
+ Abc_NtkIncrementTravId( pRoot->pNtk );
+ nNodesSaved = Abc_NodeMffcLabel( pRoot );
+ // unmark the fanin boundary and set the fanins as leaves in the form
+ Vec_PtrForEachEntry( p->vLeaves, pLeaf, i )
+ pLeaf->vFanouts.nSize--;
+
+
+ printf( "%5d : Cut-size = %d. Old AIG = %2d. New AIG = %2d. Old MFFC = %2d.\n",
+ pRoot->Id, pCut->nLeaves, Vec_PtrSize(p->vVisited), Dsd_TreeGetAigCost(pNodeDsd),
+ nNodesSaved );
+ Dsd_NodePrint( stdout, pNodeDsd );
+
+ Abc_RestructNodeDivisors( p, pRoot );
+
+ if ( pRoot->Id == 433 )
+ {
+ int x = 0;
+ }
+
+ // detect how many new nodes will be added (while taking into account reused nodes)
+clk = clock();
+ pGraph = Abc_NodeEvaluateDsd( p, pNodeDsd, pRoot, Required, nNodesSaved, &nNodesAdded );
+// pGraph = NULL;
+p->timeEval += clock() - clk;
+
+ // quit if there is no improvement
+ if ( nNodesAdded == -1 || nNodesAdded == nNodesSaved && !p->fUseZeros )
+ {
+ Cudd_RecursiveDeref( p->dd, bFunc );
+ if ( pGraph ) Dec_GraphFree( pGraph );
+ return NULL;
+ }
+
+
+ // print stats
+ printf( "%5d : Cut-size = %d. Old AIG = %2d. New AIG = %2d. Old MFFC = %2d. New MFFC = %2d. Gain = %d.\n",
+ pRoot->Id, pCut->nLeaves, Vec_PtrSize(p->vVisited), Dsd_TreeGetAigCost(pNodeDsd),
+ nNodesSaved, nNodesAdded, (nNodesAdded == -1)? 0 : nNodesSaved-nNodesAdded );
+// Dsd_NodePrint( stdout, pNodeDsd );
+// Dec_GraphPrint( stdout, pGraph, NULL, NULL );
+
+
+ // compute the total gain in the number of nodes
+ p->nLastGain = nNodesSaved - nNodesAdded;
+ p->nNodesGained += p->nLastGain;
+ p->nNodesRestructured++;
+
+ // report the progress
+ if ( fVeryVerbose )
+ {
+ printf( "Node %6s : ", Abc_ObjName(pRoot) );
+ printf( "Cone = %2d. ", p->vLeaves->nSize );
+ printf( "BDD = %2d. ", Cudd_DagSize(bFunc) );
+ printf( "FF = %2d. ", 1 + Dec_GraphNodeNum(pGraph) );
+ printf( "MFFC = %2d. ", nNodesSaved );
+ printf( "Add = %2d. ", nNodesAdded );
+ printf( "GAIN = %2d. ", p->nLastGain );
+ printf( "\n" );
+ }
+ Cudd_RecursiveDeref( p->dd, bFunc );
+ return pGraph;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Moves closer to the end the node that is best for sharing.]
+
+ Description [If the flag is set, tries to find an EXOR, otherwise, tries
+ to find an OR.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeEdgeDsdPermute( Dec_Graph_t * pGraph, Abc_ManRst_t * pManRst, Vec_Int_t * vEdges, int fExor )
+{
+ Dec_Edge_t eNode1, eNode2, eNode3;
+ Abc_Obj_t * pNode1, * pNode2, * pNode3, * pTemp;
+ int LeftBound = 0, RightBound, i;
+ // get the right bound
+ RightBound = Vec_IntSize(vEdges) - 2;
+ assert( LeftBound <= RightBound );
+ if ( LeftBound == RightBound )
+ return;
+ // get the two last nodes
+ eNode1 = Dec_IntToEdge( Vec_IntEntry(vEdges, RightBound + 1) );
+ eNode2 = Dec_IntToEdge( Vec_IntEntry(vEdges, RightBound ) );
+ pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc;
+ pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc;
+ pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl );
+ pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl );
+ // quit if the last node does not exist
+ if ( pNode1 == NULL )
+ return;
+ // find the first node that can be shared
+ for ( i = RightBound; i >= LeftBound; i-- )
+ {
+ // get the third node
+ eNode3 = Dec_IntToEdge( Vec_IntEntry(vEdges, i) );
+ pNode3 = Dec_GraphNode( pGraph, eNode3.Node )->pFunc;
+ pNode3 = !pNode3? NULL : Abc_ObjNotCond( pNode3, eNode3.fCompl );
+ if ( pNode3 == NULL )
+ continue;
+ // check if the node exists
+ if ( fExor )
+ {
+ if ( pNode1 && pNode3 )
+ {
+ pTemp = Abc_AigXorLookup( pManRst->pNtk->pManFunc, pNode1, pNode3, NULL );
+ if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
+ continue;
+
+ if ( pNode3 == pNode2 )
+ return;
+ Vec_IntWriteEntry( vEdges, i, Dec_EdgeToInt(eNode2) );
+ Vec_IntWriteEntry( vEdges, RightBound, Dec_EdgeToInt(eNode3) );
+ return;
+ }
+ }
+ else
+ {
+ if ( pNode1 && pNode3 )
+ {
+ pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode3) );
+ if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
+ continue;
+
+ if ( eNode3.Node == eNode2.Node )
+ return;
+ Vec_IntWriteEntry( vEdges, i, Dec_EdgeToInt(eNode2) );
+ Vec_IntWriteEntry( vEdges, RightBound, Dec_EdgeToInt(eNode3) );
+ return;
+ }
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds the new edge in the given order.]
+
+ Description [Similar to Vec_IntPushOrder, except in decreasing order.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeEdgeDsdPushOrdered( Dec_Graph_t * pGraph, Vec_Int_t * vEdges, int Edge )
+{
+ int i, NodeOld, NodeNew;
+ vEdges->nSize++;
+ for ( i = vEdges->nSize-2; i >= 0; i-- )
+ {
+ NodeOld = Dec_IntToEdge(vEdges->pArray[i]).Node;
+ NodeNew = Dec_IntToEdge(Edge).Node;
+ // use <= because we are trying to push the new (non-existent) nodes as far as possible
+ if ( Dec_GraphNode(pGraph, NodeOld)->Level <= Dec_GraphNode(pGraph, NodeNew)->Level )
+ vEdges->pArray[i+1] = vEdges->pArray[i];
+ else
+ break;
+ }
+ vEdges->pArray[i+1] = Edge;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Evaluation one DSD.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Edge_t Abc_NodeEvaluateDsd_rec( Dec_Graph_t * pGraph, Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, int Required, int nNodesSaved, int * pnNodesAdded )
+{
+ Dec_Edge_t eNode1, eNode2, eNode3, eResult, eQuit = { 0, 2006 };
+ Abc_Obj_t * pNode1, * pNode2, * pNode3, * pNode4, * pTemp;
+ Dsd_Node_t * pChildDsd;
+ Dsd_Type_t DecType;
+ Vec_Int_t * vEdges;
+ int Level1, Level2, Level3, Level4;
+ int i, Index, fCompl, Type;
+
+ // remove the complemented attribute
+ fCompl = Dsd_IsComplement( pNodeDsd );
+ pNodeDsd = Dsd_Regular( pNodeDsd );
+
+ // consider the trivial case
+ DecType = Dsd_NodeReadType( pNodeDsd );
+ if ( DecType == DSD_NODE_BUF )
+ {
+ Index = Dsd_NodeReadFunc(pNodeDsd)->index;
+ assert( Index < Dec_GraphLeaveNum(pGraph) );
+ eResult = Dec_EdgeCreate( Index, fCompl );
+ return eResult;
+ }
+ assert( DecType == DSD_NODE_OR || DecType == DSD_NODE_EXOR || DecType == DSD_NODE_PRIME );
+
+ // solve the problem for the children
+ vEdges = Vec_IntAlloc( Dsd_NodeReadDecsNum(pNodeDsd) );
+ Dsd_NodeForEachChild( pNodeDsd, i, pChildDsd )
+ {
+ eResult = Abc_NodeEvaluateDsd_rec( pGraph, pManRst, pChildDsd, Required, nNodesSaved, pnNodesAdded );
+ if ( eResult.Node == eQuit.Node ) // infeasible
+ {
+ Vec_IntFree( vEdges );
+ return eQuit;
+ }
+ // order the inputs only if this is OR or EXOR
+ if ( DecType == DSD_NODE_PRIME )
+ Vec_IntPush( vEdges, Dec_EdgeToInt(eResult) );
+ else
+ Abc_NodeEdgeDsdPushOrdered( pGraph, vEdges, Dec_EdgeToInt(eResult) );
+ }
+ // the edges are sorted by the level of their nodes in decreasing order
+
+
+ // consider special cases
+ if ( DecType == DSD_NODE_OR )
+ {
+ // try to balance the nodes by delay
+ assert( Vec_IntSize(vEdges) > 1 );
+ while ( Vec_IntSize(vEdges) > 1 )
+ {
+ // permute the last two entries
+ if ( Vec_IntSize(vEdges) > 2 )
+ Abc_NodeEdgeDsdPermute( pGraph, pManRst, vEdges, 0 );
+ // get the two last nodes
+ eNode1 = Dec_IntToEdge( Vec_IntPop(vEdges) );
+ eNode2 = Dec_IntToEdge( Vec_IntPop(vEdges) );
+ pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc;
+ pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc;
+ pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl );
+ pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl );
+ // check if the new node exists
+ pNode3 = NULL;
+ if ( pNode1 && pNode2 )
+ {
+ pNode3 = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) );
+ pNode3 = !pNode3? NULL : Abc_ObjNot(pNode3);
+ }
+ // create the new node
+ eNode3 = Dec_GraphAddNodeOr( pGraph, eNode1, eNode2 );
+ // set level
+ Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level;
+ Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level;
+ Dec_GraphNode( pGraph, eNode3.Node )->Level = 1 + ABC_MAX(Level1, Level2);
+ // get the new node if possible
+ if ( pNode3 )
+ {
+ Dec_GraphNode( pGraph, eNode3.Node )->pFunc = Abc_ObjNotCond(pNode3, eNode3.fCompl);
+ Level3 = Dec_GraphNode( pGraph, eNode3.Node )->Level;
+ assert( Required == ABC_INFINITY || Level3 == (int)Abc_ObjRegular(pNode3)->Level );
+ }
+ if ( !pNode3 || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pNode3)) )
+ {
+ (*pnNodesAdded)++;
+ if ( *pnNodesAdded > nNodesSaved )
+ {
+ Vec_IntFree( vEdges );
+ return eQuit;
+ }
+ }
+ // add the resulting node to the form
+ Abc_NodeEdgeDsdPushOrdered( pGraph, vEdges, Dec_EdgeToInt(eNode3) );
+ }
+ // get the last node
+ eResult = Dec_IntToEdge( Vec_IntPop(vEdges) );
+ Vec_IntFree( vEdges );
+ // complement the graph if the node was complemented
+ eResult.fCompl ^= fCompl;
+ return eResult;
+ }
+ if ( DecType == DSD_NODE_EXOR )
+ {
+ // try to balance the nodes by delay
+ assert( Vec_IntSize(vEdges) > 1 );
+ while ( Vec_IntSize(vEdges) > 1 )
+ {
+ // permute the last two entries
+ if ( Vec_IntSize(vEdges) > 2 )
+ Abc_NodeEdgeDsdPermute( pGraph, pManRst, vEdges, 1 );
+ // get the two last nodes
+ eNode1 = Dec_IntToEdge( Vec_IntPop(vEdges) );
+ eNode2 = Dec_IntToEdge( Vec_IntPop(vEdges) );
+ pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc;
+ pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc;
+ pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl );
+ pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl );
+ // check if the new node exists
+ Type = 0;
+ pNode3 = NULL;
+ if ( pNode1 && pNode2 )
+ pNode3 = Abc_AigXorLookup( pManRst->pNtk->pManFunc, pNode1, pNode2, &Type );
+ // create the new node
+ eNode3 = Dec_GraphAddNodeXor( pGraph, eNode1, eNode2, Type ); // should have the same structure as in AIG
+ // set level
+ Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level;
+ Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level;
+ Dec_GraphNode( pGraph, eNode3.Node )->Level = 2 + ABC_MAX(Level1, Level2);
+ // get the new node if possible
+ if ( pNode3 )
+ {
+ Dec_GraphNode( pGraph, eNode3.Node )->pFunc = Abc_ObjNotCond(pNode3, eNode3.fCompl);
+ Level3 = Dec_GraphNode( pGraph, eNode3.Node )->Level;
+ assert( Required == ABC_INFINITY || Level3 == (int)Abc_ObjRegular(pNode3)->Level );
+ }
+ if ( !pNode3 || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pNode3)) )
+ {
+ (*pnNodesAdded)++;
+ if ( !pNode1 || !pNode2 )
+ (*pnNodesAdded) += 2;
+ else if ( Type == 0 )
+ {
+ pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, Abc_ObjNot(pNode2) );
+ if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
+ (*pnNodesAdded)++;
+ pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), pNode2 );
+ if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
+ (*pnNodesAdded)++;
+ }
+ else
+ {
+ pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) );
+ if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
+ (*pnNodesAdded)++;
+ pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, pNode2 );
+ if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
+ (*pnNodesAdded)++;
+ }
+ if ( *pnNodesAdded > nNodesSaved )
+ {
+ Vec_IntFree( vEdges );
+ return eQuit;
+ }
+ }
+ // add the resulting node to the form
+ Abc_NodeEdgeDsdPushOrdered( pGraph, vEdges, Dec_EdgeToInt(eNode3) );
+ }
+ // get the last node
+ eResult = Dec_IntToEdge( Vec_IntPop(vEdges) );
+ Vec_IntFree( vEdges );
+ // complement the graph if the node is complemented
+ eResult.fCompl ^= fCompl;
+ return eResult;
+ }
+ if ( DecType == DSD_NODE_PRIME )
+ {
+ DdNode * bLocal, * bVar, * bCofT, * bCofE;
+ bLocal = Dsd_TreeGetPrimeFunction( pManRst->dd, pNodeDsd ); Cudd_Ref( bLocal );
+//Extra_bddPrint( pManRst->dd, bLocal );
+
+ bVar = pManRst->dd->vars[0];
+ bCofE = Cudd_Cofactor( pManRst->dd, bLocal, Cudd_Not(bVar) ); Cudd_Ref( bCofE );
+ bCofT = Cudd_Cofactor( pManRst->dd, bLocal, bVar ); Cudd_Ref( bCofT );
+ if ( !Extra_bddIsVar(bCofE) || !Extra_bddIsVar(bCofT) )
+ {
+ Cudd_RecursiveDeref( pManRst->dd, bCofE );
+ Cudd_RecursiveDeref( pManRst->dd, bCofT );
+ bVar = pManRst->dd->vars[1];
+ bCofE = Cudd_Cofactor( pManRst->dd, bLocal, Cudd_Not(bVar) ); Cudd_Ref( bCofE );
+ bCofT = Cudd_Cofactor( pManRst->dd, bLocal, bVar ); Cudd_Ref( bCofT );
+ if ( !Extra_bddIsVar(bCofE) || !Extra_bddIsVar(bCofT) )
+ {
+ Cudd_RecursiveDeref( pManRst->dd, bCofE );
+ Cudd_RecursiveDeref( pManRst->dd, bCofT );
+ bVar = pManRst->dd->vars[2];
+ bCofE = Cudd_Cofactor( pManRst->dd, bLocal, Cudd_Not(bVar) ); Cudd_Ref( bCofE );
+ bCofT = Cudd_Cofactor( pManRst->dd, bLocal, bVar ); Cudd_Ref( bCofT );
+ if ( !Extra_bddIsVar(bCofE) || !Extra_bddIsVar(bCofT) )
+ {
+ Cudd_RecursiveDeref( pManRst->dd, bCofE );
+ Cudd_RecursiveDeref( pManRst->dd, bCofT );
+ Cudd_RecursiveDeref( pManRst->dd, bLocal );
+ Vec_IntFree( vEdges );
+ return eQuit;
+ }
+ }
+ }
+ Cudd_RecursiveDeref( pManRst->dd, bLocal );
+ // we found the control variable (bVar) and the var-cofactors (bCofT, bCofE)
+
+ // find the graph nodes
+ eNode1 = Dec_IntToEdge( Vec_IntEntry(vEdges, bVar->index) );
+ eNode2 = Dec_IntToEdge( Vec_IntEntry(vEdges, Cudd_Regular(bCofT)->index) );
+ eNode3 = Dec_IntToEdge( Vec_IntEntry(vEdges, Cudd_Regular(bCofE)->index) );
+ // add the complements to the graph nodes
+ eNode2.fCompl ^= Cudd_IsComplement(bCofT);
+ eNode3.fCompl ^= Cudd_IsComplement(bCofE);
+
+ // because the cofactors are vars, we can just as well deref them here
+ Cudd_RecursiveDeref( pManRst->dd, bCofE );
+ Cudd_RecursiveDeref( pManRst->dd, bCofT );
+
+ // find the ABC nodes
+ pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc;
+ pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc;
+ pNode3 = Dec_GraphNode( pGraph, eNode3.Node )->pFunc;
+ pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl );
+ pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl );
+ pNode3 = !pNode3? NULL : Abc_ObjNotCond( pNode3, eNode3.fCompl );
+
+ // check if the new node exists
+ Type = 0;
+ pNode4 = NULL;
+ if ( pNode1 && pNode2 && pNode3 )
+ pNode4 = Abc_AigMuxLookup( pManRst->pNtk->pManFunc, pNode1, pNode2, pNode3, &Type );
+
+ // create the new node
+ eResult = Dec_GraphAddNodeMux( pGraph, eNode1, eNode2, eNode3, Type ); // should have the same structure as AIG
+
+ // set level
+ Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level;
+ Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level;
+ Level3 = Dec_GraphNode( pGraph, eNode3.Node )->Level;
+ Dec_GraphNode( pGraph, eResult.Node )->Level = 2 + ABC_MAX( ABC_MAX(Level1, Level2), Level3 );
+ // get the new node if possible
+ if ( pNode4 )
+ {
+ Dec_GraphNode( pGraph, eResult.Node )->pFunc = Abc_ObjNotCond(pNode4, eResult.fCompl);
+ Level4 = Dec_GraphNode( pGraph, eResult.Node )->Level;
+ assert( Required == ABC_INFINITY || Level4 == (int)Abc_ObjRegular(pNode4)->Level );
+ }
+ if ( !pNode4 || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pNode4)) )
+ {
+ (*pnNodesAdded)++;
+ if ( Type == 0 )
+ {
+ if ( !pNode1 || !pNode2 )
+ (*pnNodesAdded)++;
+ else
+ {
+ pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, pNode2 );
+ if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
+ (*pnNodesAdded)++;
+ }
+ if ( !pNode1 || !pNode3 )
+ (*pnNodesAdded)++;
+ else
+ {
+ pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), pNode3 );
+ if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
+ (*pnNodesAdded)++;
+ }
+ }
+ else
+ {
+ if ( !pNode1 || !pNode2 )
+ (*pnNodesAdded)++;
+ else
+ {
+ pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, Abc_ObjNot(pNode2) );
+ if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
+ (*pnNodesAdded)++;
+ }
+ if ( !pNode1 || !pNode3 )
+ (*pnNodesAdded)++;
+ else
+ {
+ pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode3) );
+ if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) )
+ (*pnNodesAdded)++;
+ }
+ }
+ if ( *pnNodesAdded > nNodesSaved )
+ {
+ Vec_IntFree( vEdges );
+ return eQuit;
+ }
+ }
+
+ Vec_IntFree( vEdges );
+ // complement the graph if the node was complemented
+ eResult.fCompl ^= fCompl;
+ return eResult;
+ }
+ Vec_IntFree( vEdges );
+ return eQuit;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Evaluation one DSD.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, Abc_Obj_t * pRoot, int Required, int nNodesSaved, int * pnNodesAdded )
+{
+ Dec_Graph_t * pGraph;
+ Dec_Edge_t gEdge;
+ Abc_Obj_t * pLeaf;
+ Dec_Node_t * pNode;
+ int i;
+
+ // create the graph and set the leaves
+ pGraph = Dec_GraphCreate( Vec_PtrSize(pManRst->vLeaves) );
+ Dec_GraphForEachLeaf( pGraph, pNode, i )
+ {
+ pLeaf = Vec_PtrEntry( pManRst->vLeaves, i );
+ pNode->pFunc = pLeaf;
+ pNode->Level = pLeaf->Level;
+ }
+
+ // create the decomposition structure from the DSD
+ *pnNodesAdded = 0;
+ gEdge = Abc_NodeEvaluateDsd_rec( pGraph, pManRst, pNodeDsd, Required, nNodesSaved, pnNodesAdded );
+ if ( gEdge.Node > 1000 ) // infeasible
+ {
+ *pnNodesAdded = -1;
+ Dec_GraphFree( pGraph );
+ return NULL;
+ }
+
+ // quit if the root node is the same
+ pLeaf = Dec_GraphNode( pGraph, gEdge.Node )->pFunc;
+ if ( Abc_ObjRegular(pLeaf) == pRoot )
+ {
+ *pnNodesAdded = -1;
+ Dec_GraphFree( pGraph );
+ return NULL;
+ }
+
+ Dec_GraphSetRoot( pGraph, gEdge );
+ return pGraph;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Starts the cut manager for rewriting.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fMulti )
+{
+ static Cut_Params_t Params, * pParams = &Params;
+ Cut_Man_t * pManCut;
+ Abc_Obj_t * pObj;
+ int i;
+ // start the cut manager
+ memset( pParams, 0, sizeof(Cut_Params_t) );
+ pParams->nVarsMax = nCutMax; // the max cut size ("k" of the k-feasible cuts)
+ pParams->nKeepMax = 250; // the max number of cuts kept at a node
+ pParams->fTruth = 0; // compute truth tables
+ pParams->fFilter = 1; // filter dominated cuts
+ pParams->fSeq = 0; // compute sequential cuts
+ pParams->fDrop = 0; // drop cuts on the fly
+ pParams->fMulti = fMulti; // compute factor-cuts
+ pParams->fVerbose = 0; // the verbosiness flag
+ pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
+ pManCut = Cut_ManStart( pParams );
+ if ( pParams->fDrop )
+ Cut_ManSetFanoutCounts( pManCut, Abc_NtkFanoutCounts(pNtk) );
+ // set cuts for PIs
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ if ( Abc_ObjFanoutNum(pObj) > 0 )
+ Cut_NodeSetTriv( pManCut, pObj->Id );
+ return pManCut;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_ManRst_t * Abc_NtkManRstStart( int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose )
+{
+ Abc_ManRst_t * p;
+ p = ALLOC( Abc_ManRst_t, 1 );
+ memset( p, 0, sizeof(Abc_ManRst_t) );
+ // set the parameters
+ p->nCutMax = nCutMax;
+ p->fUpdateLevel = fUpdateLevel;
+ p->fUseZeros = fUseZeros;
+ p->fVerbose = fVerbose;
+ // start the BDD manager
+ p->dd = Cudd_Init( p->nCutMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+ Cudd_zddVarsFromBddVars( p->dd, 2 );
+ // start the DSD manager
+ p->pManDsd = Dsd_ManagerStart( p->dd, p->dd->size, 0 );
+ // other temp datastructures
+ p->vVisited = Vec_PtrAlloc( 100 );
+ p->vLeaves = Vec_PtrAlloc( 100 );
+ p->vDecs = Vec_PtrAlloc( 100 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkManRstStop( Abc_ManRst_t * p )
+{
+ Dsd_ManagerStop( p->pManDsd );
+ Extra_StopManager( p->dd );
+ Vec_PtrFree( p->vDecs );
+ Vec_PtrFree( p->vLeaves );
+ Vec_PtrFree( p->vVisited );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkManRstPrintStats( Abc_ManRst_t * p )
+{
+ printf( "Refactoring statistics:\n" );
+ printf( "Nodes considered = %8d.\n", p->nNodesConsidered );
+ printf( "Cuts considered = %8d.\n", p->nCutsConsidered );
+ printf( "Cuts explored = %8d.\n", p->nCutsExplored );
+ printf( "Nodes restructured = %8d.\n", p->nNodesRestructured );
+ printf( "Calculated gain = %8d.\n", p->nNodesGained );
+ PRT( "Cuts ", p->timeCut );
+ PRT( "Resynthesis", p->timeRes );
+ PRT( " BDD ", p->timeBdd );
+ PRT( " DSD ", p->timeDsd );
+ PRT( " Eval ", p->timeEval );
+ PRT( "AIG update ", p->timeNtk );
+ PRT( "TOTAL ", p->timeTotal );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index b3b30d9a..f3360421 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -96,6 +96,14 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
{
Dec_Graph_t * pGraph = Rwr_ManReadDecs(pManRwr);
int fCompl = Rwr_ManReadCompl(pManRwr);
+/*
+ if ( nGain > 0 )
+ { // print stats on the MFFC
+ extern void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode );
+ printf( "Node %6d : Gain = %4d ", pNode->Id, nGain );
+ Abc_NodeMffsConeSuppPrint( pNode );
+ }
+*/
// complement the FF if needed
if ( fCompl ) Dec_GraphComplement( pGraph );
clk = clock();
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 9c650aa9..5376444b 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -24,13 +24,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
-static int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
-
-static solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk );
-
static Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
-
static nMuxes;
////////////////////////////////////////////////////////////////////////
@@ -48,13 +42,13 @@ static nMuxes;
SeeAlso []
***********************************************************************/
-int Abc_NtkMiterSat_OldAndRusty( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose )
{
solver * pSat;
lbool status;
int RetValue, clk;
- assert( Abc_NtkIsBddLogic(pNtk) );
+ assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkLatchNum(pNtk) == 0 );
if ( Abc_NtkPoNum(pNtk) > 1 )
@@ -84,7 +78,7 @@ int Abc_NtkMiterSat_OldAndRusty( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
clk = clock();
if ( fVerbose )
pSat->verbosity = 1;
- status = solver_solve( pSat, NULL, NULL, nSeconds );
+ status = solver_solve( pSat, NULL, NULL, nConfLimit, nImpLimit );
if ( status == l_Undef )
{
// printf( "The problem timed out.\n" );
@@ -107,277 +101,6 @@ int Abc_NtkMiterSat_OldAndRusty( 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 );
- pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
- Vec_IntFree( vCiIds );
- }
- // free the solver
- solver_delete( pSat );
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis [Sets up the SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
-{
- solver * pSat;
- Extra_MmFlex_t * pMmFlex;
- Abc_Obj_t * pNode;
- Vec_Str_t * vCube;
- Vec_Int_t * vVars;
- char * pSop0, * pSop1;
- int i, clk = clock();
-
- assert( Abc_NtkIsBddLogic(pNtk) );
-
- // start the data structures
- pSat = solver_new();
- pMmFlex = Extra_MmFlexStart();
- vCube = Vec_StrAlloc( 100 );
- vVars = Vec_IntAlloc( 100 );
-
- // add clauses for each internal nodes
- Abc_NtkForEachNode( pNtk, pNode, i )
- {
- // derive SOPs for both phases of the node
- Abc_NodeBddToCnf( pNode, pMmFlex, vCube, &pSop0, &pSop1 );
- // add the clauses to the solver
- if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) )
- {
- solver_delete( pSat );
- return NULL;
- }
- }
- // add clauses for the POs
- if ( !Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars ) )
- {
- solver_delete( pSat );
- return NULL;
- }
-// Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 );
-
- PRT( "Creating solver", clock() - clk );
-
- // delete
- Vec_StrFree( vCube );
- Vec_IntFree( vVars );
- Extra_MmFlexStop( pMmFlex, 0 );
- return pSat;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds clauses for the internal node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
-{
- Abc_Obj_t * pFanin;
- int i, c, nFanins;
- char * pCube;
-
- nFanins = Abc_ObjFaninNum( pNode );
- assert( nFanins == Abc_SopGetVarNum( pSop0 ) );
-
- if ( nFanins == 0 )
- {
- vVars->nSize = 0;
- if ( Abc_SopIsConst1(pSop1) )
- Vec_IntPush( vVars, toLit(pNode->Id) );
- else
- Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
- return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
- }
-
- // add clauses for the negative phase
- for ( c = 0; ; c++ )
- {
- // get the cube
- pCube = pSop0 + c * (nFanins + 3);
- if ( *pCube == 0 )
- break;
- // add the clause
- vVars->nSize = 0;
- Abc_ObjForEachFanin( pNode, pFanin, i )
- {
- if ( pCube[i] == '0' )
- Vec_IntPush( vVars, toLit(pFanin->Id) );
- else if ( pCube[i] == '1' )
- Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
- }
- Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
- }
-
- // add clauses for the positive phase
- for ( c = 0; ; c++ )
- {
- // get the cube
- pCube = pSop1 + c * (nFanins + 3);
- if ( *pCube == 0 )
- break;
- // add the clause
- vVars->nSize = 0;
- Abc_ObjForEachFanin( pNode, pFanin, i )
- {
- if ( pCube[i] == '0' )
- Vec_IntPush( vVars, toLit(pFanin->Id) );
- else if ( pCube[i] == '1' )
- Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
- }
- Vec_IntPush( vVars, toLit(pNode->Id) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds clauses for the PO node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
-{
- Abc_Obj_t * pFanin;
-
- pFanin = Abc_ObjFanin0(pNode);
- if ( Abc_ObjFaninC0(pNode) )
- {
- vVars->nSize = 0;
- Vec_IntPush( vVars, toLit(pFanin->Id) );
- Vec_IntPush( vVars, toLit(pNode->Id) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
-
- vVars->nSize = 0;
- Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
- Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
- }
- else
- {
- vVars->nSize = 0;
- Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
- Vec_IntPush( vVars, toLit(pNode->Id) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
-
- vVars->nSize = 0;
- Vec_IntPush( vVars, toLit(pFanin->Id) );
- Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
- }
-
- vVars->nSize = 0;
- Vec_IntPush( vVars, toLit(pNode->Id) );
- return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-}
-
-
-
-
-
-
-
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Attempts to solve the miter using an internal SAT solver.]
-
- Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
-{
- solver * pSat;
- lbool status;
- int RetValue, clk;
-
- assert( Abc_NtkIsStrash(pNtk) );
- assert( Abc_NtkLatchNum(pNtk) == 0 );
-
- if ( Abc_NtkPoNum(pNtk) > 1 )
- fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
-
- // load clauses into the solver
- clk = clock();
- pSat = Abc_NtkMiterSatCreate2( pNtk );
- if ( pSat == NULL )
- return 1;
-// printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
-// PRT( "Time", clock() - clk );
-
- // simplify the problem
- clk = clock();
- status = solver_simplify(pSat);
-// printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
-// PRT( "Time", clock() - clk );
- if ( status == 0 )
- {
- solver_delete( pSat );
-// printf( "The problem is UNSATISFIABLE after simplification.\n" );
- return 1;
- }
-
- // solve the miter
- clk = clock();
- if ( fVerbose )
- pSat->verbosity = 1;
- status = solver_solve( pSat, NULL, NULL, nSeconds );
- if ( status == l_Undef )
- {
-// printf( "The problem timed out.\n" );
- RetValue = -1;
- }
- else if ( status == l_True )
- {
-// printf( "The problem is SATISFIABLE.\n" );
- RetValue = 0;
- }
- else if ( status == l_False )
- {
-// printf( "The problem is UNSATISFIABLE.\n" );
- RetValue = 1;
- }
- else
- assert( 0 );
- PRT( "SAT solver time", clock() - clk );
-
- // if the problem is SAT, get the counterexample
- if ( status == l_True )
- {
// Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
@@ -411,7 +134,6 @@ Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk )
}
-
/**Function*************************************************************
@@ -669,7 +391,7 @@ void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNo
SeeAlso []
***********************************************************************/
-int Abc_NtkMiterSatCreate2Int( solver * pSat, Abc_Ntk_t * pNtk )
+int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
Vec_Ptr_t * vNodes, * vSuper;
@@ -787,7 +509,7 @@ int Abc_NtkMiterSatCreate2Int( solver * pSat, Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
+solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
{
solver * pSat;
Abc_Obj_t * pNode;
@@ -796,7 +518,7 @@ solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
nMuxes = 0;
pSat = solver_new();
- RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk );
+ RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk );
Abc_NtkForEachObj( pNtk, pNode, i )
pNode->fMarkA = 0;
// Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
@@ -805,8 +527,8 @@ solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
solver_delete(pSat);
return NULL;
}
- printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
- PRT( "Creating solver", clock() - clk );
+// printf( "Ands = %6d. Muxes = %6d (%5.2f %%). ", Abc_NtkNodeNum(pNtk), nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
+// PRT( "Creating solver", clock() - clk );
return pSat;
}
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 00370002..34757145 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -285,7 +285,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
// start the new network
pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
- pNtkNew->pName = util_strsav( "exdc" );
+ pNtkNew->pName = Extra_UtilStrsav( "exdc" );
pNtkNew->pSpec = NULL;
// create PIs corresponding to LOs
diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c
index f8d659a0..d719df4f 100644
--- a/src/base/abci/abcVanEijk.c
+++ b/src/base/abci/abcVanEijk.c
@@ -517,13 +517,13 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF
pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
if ( fShortNames )
{
- pNtkFrames->pName = util_strsav(pNtk->pName);
- pNtkFrames->pSpec = util_strsav(pNtk->pSpec);
+ pNtkFrames->pName = Extra_UtilStrsav(pNtk->pName);
+ pNtkFrames->pSpec = Extra_UtilStrsav(pNtk->pSpec);
}
else
{
sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames + fAddLast );
- pNtkFrames->pName = util_strsav(Buffer);
+ pNtkFrames->pName = Extra_UtilStrsav(Buffer);
}
// map the constant nodes
Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkFrames);
@@ -722,7 +722,7 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
// start the network
pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
- pNtkNew->pName = util_strsav("exdc");
+ pNtkNew->pName = Extra_UtilStrsav("exdc");
pNtkNew->pSpec = NULL;
// map the constant nodes
diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c
index 693d0af7..1805378c 100644
--- a/src/base/abci/abcVanImp.c
+++ b/src/base/abci/abcVanImp.c
@@ -878,7 +878,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I
// start the network
pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
- pNtkNew->pName = util_strsav( "exdc" );
+ pNtkNew->pName = Extra_UtilStrsav( "exdc" );
pNtkNew->pSpec = NULL;
// map the constant nodes
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 99392e48..5c7b525e 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -46,7 +46,7 @@ static void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2,
SeeAlso []
***********************************************************************/
-void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds )
+void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit )
{
Abc_Ntk_t * pMiter;
Abc_Ntk_t * pCnf;
@@ -87,7 +87,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds )
}
// solve the CNF using the SAT solver
- RetValue = Abc_NtkMiterSat( pCnf, nSeconds, 0 );
+ RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 );
if ( RetValue == -1 )
printf( "Networks are undecided (SAT solver timed out).\n" );
else if ( RetValue == 0 )
@@ -184,7 +184,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
SeeAlso []
***********************************************************************/
-void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames )
+void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit, int nFrames )
{
Abc_Ntk_t * pMiter;
Abc_Ntk_t * pFrames;
@@ -244,7 +244,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFra
}
// solve the CNF using the SAT solver
- RetValue = Abc_NtkMiterSat( pCnf, nSeconds, 0 );
+ RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 );
if ( RetValue == -1 )
printf( "Networks are undecided (SAT solver timed out).\n" );
else if ( RetValue == 0 )
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 5b15641b..3ca188b7 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -2,9 +2,11 @@ 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/abcClpBdd.c \
+ src/base/abci/abcClpSop.c \
src/base/abci/abcCut.c \
src/base/abci/abcDsd.c \
+ src/base/abci/abcEspresso.c \
src/base/abci/abcFpga.c \
src/base/abci/abcFraig.c \
src/base/abci/abcFxu.c \
@@ -13,6 +15,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcNtbdd.c \
src/base/abci/abcPga.c \
src/base/abci/abcPrint.c \
+ src/base/abci/abcProve.c \
src/base/abci/abcReconv.c \
src/base/abci/abcRefactor.c \
src/base/abci/abcRenode.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-08 18:00:25 +0000