summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c140
-rw-r--r--src/base/abci/abcClpBdd.c7
-rw-r--r--src/base/abci/abcIvy.c69
-rw-r--r--src/base/abci/abcMiter.c1
-rw-r--r--src/base/abci/abcNtbdd.c154
-rw-r--r--src/base/abci/abcOrder.c131
-rw-r--r--src/base/abci/module.make1
7 files changed, 430 insertions, 73 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f3dbe357..c1327f43 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -74,6 +74,7 @@ static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandOneOutput ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -192,6 +193,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "sop", Abc_CommandSop, 0 );
Cmd_CommandAdd( pAbc, "Various", "bdd", Abc_CommandBdd, 0 );
Cmd_CommandAdd( pAbc, "Various", "reorder", Abc_CommandReorder, 0 );
+ Cmd_CommandAdd( pAbc, "Various", "order", Abc_CommandOrder, 0 );
Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 );
Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 );
Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandOneOutput, 1 );
@@ -1627,6 +1629,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
+ int fVerbose;
int fBddSizeMax;
int fDualRail;
int fReorder;
@@ -1637,11 +1640,12 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
+ fVerbose = 1;
fReorder = 1;
fDualRail = 0;
- fBddSizeMax = 1000000;
+ fBddSizeMax = 50000000;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Brdh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Brdvh" ) ) != EOF )
{
switch ( c )
{
@@ -1659,6 +1663,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDualRail ^= 1;
break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
case 'r':
fReorder ^= 1;
break;
@@ -1683,11 +1690,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
if ( Abc_NtkIsStrash(pNtk) )
- pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 );
+ pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
else
{
pNtk = Abc_NtkStrash( pNtk, 0, 0 );
- pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 );
+ pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
Abc_NtkDelete( pNtk );
}
if ( pNtkRes == NULL )
@@ -1700,11 +1707,12 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: collapse [-B num] [-rdh]\n" );
+ fprintf( pErr, "usage: collapse [-B num] [-rdvh]\n" );
fprintf( pErr, "\t collapses the network by constructing global BDDs\n" );
fprintf( pErr, "\t-B num : limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax );
fprintf( pErr, "\t-r : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
fprintf( pErr, "\t-d : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" );
+ fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -3462,6 +3470,93 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandOrder( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr, * pFile;
+ Abc_Ntk_t * pNtk;
+ char * pFileName;
+ int c;
+ int fReverse;
+ int fVerbose;
+ extern void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, int fVerbose );
+ extern void Abc_NtkFindCiOrder( Abc_Ntk_t * pNtk, int fReverse, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fReverse = 0;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'r':
+ fReverse ^= 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 )
+// {
+// printf( "Currently this procedure does not work for sequential networks.\n" );
+// return 1;
+// }
+
+ // if the var order file is given, implement this order
+ pFileName = NULL;
+ if ( argc == globalUtilOptind + 1 )
+ {
+ pFileName = argv[globalUtilOptind];
+ pFile = fopen( pFileName, "r" );
+ if ( pFile == NULL )
+ {
+ fprintf( pErr, "Cannot open file \"%s\" with the BDD variable order.\n", pFileName );
+ return 1;
+ }
+ fclose( pFile );
+ }
+ if ( pFileName )
+ Abc_NtkImplementCiOrder( pNtk, pFileName, fReverse, fVerbose );
+ else
+ Abc_NtkFindCiOrder( pNtk, fReverse, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: order [-rvh] <file>\n" );
+ fprintf( pErr, "\t computes a good static CI variable order\n" );
+ fprintf( pErr, "\t-r : toggle reverse ordering [default = %s]\n", fReverse? "yes": "no" );
+ fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ fprintf( pErr, "\t<file> : (optional) file with the given variable order\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -4583,7 +4678,8 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
// run the command
// pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
- pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+// pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+ pNtkRes = NULL;
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -5105,21 +5201,36 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
- int c, fUpdateLevel, fVerbose;
- extern Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int fVerbose );
+ int c, fUseZeroCost, fVerbose, nIters;
+ extern Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- fUpdateLevel = 1;
+ nIters = 3;
+ fUseZeroCost = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "zvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Izvh" ) ) != EOF )
{
switch ( c )
{
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nIters < 0 )
+ goto usage;
+ break;
+ case 'z':
+ fUseZeroCost ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -5140,7 +5251,7 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- pNtkRes = Abc_NtkIvyHaig( pNtk, fVerbose );
+ pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -5151,9 +5262,10 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: haig [-vh]\n" );
- fprintf( pErr, "\t prints HAIG stats after one round of sequential rewriting\n" );
-// fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+ fprintf( pErr, "usage: haig [-Izvh]\n" );
+ fprintf( pErr, "\t prints HAIG stats after sequential rewriting\n" );
+ fprintf( pErr, "\t-I num : the number of rewriting iterations [default = %d]\n", nIters );
+ fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", fUseZeroCost? "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;
diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c
index eed18e1b..1de087e8 100644
--- a/src/base/abci/abcClpBdd.c
+++ b/src/base/abci/abcClpBdd.c
@@ -46,14 +46,17 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
{
Abc_Ntk_t * pNtkNew;
+ int clk = clock();
assert( Abc_NtkIsStrash(pNtk) );
-
// compute the global BDDs
if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0, fReorder, fVerbose) == NULL )
return NULL;
if ( fVerbose )
- printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
+ {
+ printf( "The shared BDD size is %d nodes. ", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
+ PRT( "BDD construction time", clock() - clk );
+ }
// create the new network
if ( fDualRail )
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 7d5ed6ec..42d5173a 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -27,7 +27,7 @@
////////////////////////////////////////////////////////////////////////
static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
-static Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
+static Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig );
static Ivy_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld );
static void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
@@ -120,17 +120,17 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq )
+Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq, int fHaig )
{
Abc_Ntk_t * pNtkAig;
int nNodes, fCleanup = 1;
// convert from the AIG manager
if ( fSeq )
- pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan );
+ pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan, fHaig );
else
pNtkAig = Abc_NtkFromAig( pNtk, pMan );
// report the cleanup results
- if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
+ if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
// duplicate EXDC
if ( pNtk->pExdc )
@@ -163,11 +163,11 @@ Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
if ( pMan == NULL )
return NULL;
- pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+ pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
-
+
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
@@ -179,21 +179,28 @@ Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int fVerbose )
+Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan;
+ int i;
+
pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
if ( pMan == NULL )
return NULL;
- Ivy_ManHaigStart( pMan );
- Ivy_ManRewriteSeq( pMan, 0, fVerbose );
- Ivy_ManHaigPrintStats( pMan );
- Ivy_ManHaigStop( pMan );
+ Ivy_ManHaigStart( pMan, fVerbose );
+ Ivy_ManRewriteSeq( pMan, 0, 0 );
+ for ( i = 1; i < nIters; i++ )
+ Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
+ Ivy_ManHaigPostprocess( pMan, fVerbose );
+
+ // write working AIG into the current network
+// pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
+ // write HAIG into the current network
+ pNtkAig = Abc_NtkIvyAfter( pNtk, pMan->pHaig, 1, 1 );
-// pNtkAig = Abc_NtkIvyAfterHaig( pNtk, pMan, 1 );
- pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+ Ivy_ManHaigStop( pMan );
Ivy_ManStop( pMan );
return pNtkAig;
}
@@ -239,7 +246,7 @@ Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroC
if ( pMan == NULL )
return NULL;
Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose );
- pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0 );
+ pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
@@ -263,7 +270,9 @@ Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbo
if ( pMan == NULL )
return NULL;
Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose );
- pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+// Ivy_ManRewriteSeq( pMan, 1, 0 );
+// Ivy_ManRewriteSeq( pMan, 1, 0 );
+ pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
@@ -288,7 +297,7 @@ Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
return NULL;
pMan = Ivy_ManResyn( pTemp = pMan, fUpdateLevel, fVerbose );
Ivy_ManStop( pTemp );
- pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0 );
+ pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
@@ -474,14 +483,14 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig )
{
Vec_Int_t * vNodes, * vLatches;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
- Ivy_Obj_t * pNode;
+ Ivy_Obj_t * pNode, * pTemp;
int i;
- assert( Ivy_ManLatchNum(pMan) > 0 );
+// assert( Ivy_ManLatchNum(pMan) > 0 );
// perform strashing
pNtk = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
// transfer the pointers to the basic nodes
@@ -493,7 +502,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i )
{
pObjNew = Abc_NtkCreateLatch( pNtk );
- if ( Ivy_ObjInit(pNode) == IVY_INIT_DC )
+ if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC )
Abc_LatchSetInitDc( pObjNew );
else if ( Ivy_ObjInit(pNode) == IVY_INIT_1 )
Abc_LatchSetInit1( pObjNew );
@@ -505,14 +514,14 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
// rebuild the AIG
Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
{
- // add the first fanins
+ // add the first fanin
pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
if ( Ivy_ObjIsBuf(pNode) )
{
pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
continue;
}
- // add the first second
+ // add the second fanin
pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
// create the new node
if ( Ivy_ObjIsExor(pNode) )
@@ -520,6 +529,22 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
else
pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
pNode->TravId = Abc_EdgeFromNode( pObjNew );
+ // process the choice nodes
+ if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 )
+ {
+ pFaninNew = Abc_EdgeToNode( pNtk, pNode->TravId );
+ pFaninNew->fPhase = 0;
+ assert( !Ivy_IsComplement(pNode->pEquiv) );
+ for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) )
+ {
+ pFaninNew1 = Abc_EdgeToNode( pNtk, pTemp->TravId );
+ pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv );
+ pFaninNew->pData = pFaninNew1;
+ pFaninNew = pFaninNew1;
+ }
+ pFaninNew->pData = NULL;
+// printf( "Writing choice node %d.\n", pNode->Id );
+ }
}
// connect the PO nodes
Abc_NtkForEachPo( pNtkOld, pObj, i )
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index ecd44017..ea1beb8c 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -27,7 +27,6 @@
static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
static void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
static void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
-static void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
static void Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame );
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 6cbab1a6..0976b652 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -246,35 +246,47 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
{
ProgressBar * pProgress;
Vec_Ptr_t * vFuncsGlob;
- Abc_Obj_t * pNode;
+ Abc_Obj_t * pNode, * pFanin;
DdNode * bFunc;
DdManager * dd;
- int i, Counter;
+ int i, k, Counter;
+
+ // remove dangling nodes
+ Abc_AigCleanup( pNtk->pManFunc );
// start the manager
assert( pNtk->pManGlob == NULL );
dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+ // set reordering
if ( fReorder )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
- // set the elementary variables
+ // clean storage for local BDDs
Abc_NtkCleanCopy( pNtk );
+ // set the elementary variables
Abc_NtkForEachCi( pNtk, pNode, i )
- pNode->pCopy = (Abc_Obj_t *)dd->vars[i];
+ if ( Abc_ObjFanoutNum(pNode) > 0 )
+ {
+ pNode->pCopy = (Abc_Obj_t *)dd->vars[i];
+ Cudd_Ref( dd->vars[i] );
+ }
// assign the constant node BDD
pNode = Abc_NtkConst1( pNtk );
- pNode->pCopy = (Abc_Obj_t *)dd->one; Cudd_Ref( dd->one );
+ if ( Abc_ObjFanoutNum(pNode) > 0 )
+ {
+ pNode->pCopy = (Abc_Obj_t *)dd->one;
+ Cudd_Ref( dd->one );
+ }
// collect the global functions of the COs
- vFuncsGlob = Vec_PtrAlloc( 100 );
Counter = 0;
+ vFuncsGlob = Vec_PtrAlloc( 100 );
if ( fLatchOnly )
{
// construct the BDDs
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pNode, i )
{
-// Extra_ProgressBarUpdate( pProgress, i, NULL );
bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
if ( bFunc == NULL )
{
@@ -295,7 +307,6 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
{
-// Extra_ProgressBarUpdate( pProgress, i, NULL );
bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
if ( bFunc == NULL )
{
@@ -305,12 +316,12 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
Cudd_Quit( dd );
return NULL;
}
- bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc );
+ bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc );
Vec_PtrPush( vFuncsGlob, bFunc );
}
Extra_ProgressBarStop( pProgress );
}
-
+/*
// derefence the intermediate BDDs
Abc_NtkForEachNode( pNtk, pNode, i )
if ( pNode->pCopy )
@@ -318,6 +329,22 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
pNode->pCopy = NULL;
}
+*/
+/*
+ // make sure all nodes are derefed
+ Abc_NtkForEachObj( pNtk, pNode, i )
+ {
+ if ( pNode->pCopy != NULL )
+ printf( "Abc_NtkGlobalBdds() error: Node %d has BDD assigned\n", pNode->Id );
+ if ( pNode->vFanouts.nSize > 0 )
+ printf( "Abc_NtkGlobalBdds() error: Node %d has refs assigned\n", pNode->Id );
+ }
+*/
+ // reset references
+ Abc_NtkForEachObj( pNtk, pNode, i )
+ Abc_ObjForEachFanin( pNode, pFanin, k )
+ pFanin->vFanouts.nSize++;
+
// reorder one more time
if ( fReorder )
{
@@ -326,6 +353,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
}
pNtk->pManGlob = dd;
pNtk->vFuncsGlob = vFuncsGlob;
+// Cudd_PrintInfo( dd, stdout );
return dd;
}
@@ -342,7 +370,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
***********************************************************************/
DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose )
{
- DdNode * bFunc, * bFunc0, * bFunc1;
+ DdNode * bFunc, * bFunc0, * bFunc1, * bFuncC;
assert( !Abc_ObjIsComplement(pNode) );
if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
{
@@ -353,29 +381,87 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
return NULL;
}
// if the result is available return
- if ( pNode->pCopy )
- return (DdNode *)pNode->pCopy;
- // compute the result for both branches
- bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose );
- if ( bFunc0 == NULL )
- return NULL;
- Cudd_Ref( bFunc0 );
- bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose );
- if ( bFunc1 == NULL )
- return NULL;
- Cudd_Ref( bFunc1 );
- bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
- bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
- // get the final result
- bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
- Cudd_RecursiveDeref( dd, bFunc0 );
- Cudd_RecursiveDeref( dd, bFunc1 );
- // set the result
- assert( pNode->pCopy == NULL );
- pNode->pCopy = (Abc_Obj_t *)bFunc;
- // increment the progress bar
- if ( pProgress )
- Extra_ProgressBarUpdate( pProgress, (*pCounter)++, NULL );
+ if ( pNode->pCopy == NULL )
+ {
+ Abc_Obj_t * pNodeC, * pNode0, * pNode1;
+ pNode0 = Abc_ObjFanin0(pNode);
+ pNode1 = Abc_ObjFanin1(pNode);
+ // check for the special case when it is MUX/EXOR
+// if ( 0 )
+ if ( pNode0->pCopy == NULL && pNode1->pCopy == NULL &&
+ Abc_ObjIsNode(pNode0) && Abc_ObjFanoutNum(pNode0) == 1 &&
+ Abc_ObjIsNode(pNode1) && Abc_ObjFanoutNum(pNode1) == 1 &&
+ Abc_NodeIsMuxType(pNode) )
+ {
+ // deref the fanins
+ pNode0->vFanouts.nSize--;
+ pNode1->vFanouts.nSize--;
+ // recognize the MUX
+ pNodeC = Abc_NodeRecognizeMux( pNode, &pNode1, &pNode0 );
+ assert( Abc_ObjFanoutNum(pNodeC) > 1 );
+ // dereference the control once (the second time it will be derefed when BDDs are computed)
+ pNodeC->vFanouts.nSize--;
+
+ // compute the result for all branches
+ bFuncC = Abc_NodeGlobalBdds_rec( dd, pNodeC, nBddSizeMax, pProgress, pCounter, fVerbose );
+ if ( bFuncC == NULL )
+ return NULL;
+ Cudd_Ref( bFuncC );
+ bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode0), nBddSizeMax, pProgress, pCounter, fVerbose );
+ if ( bFunc0 == NULL )
+ return NULL;
+ Cudd_Ref( bFunc0 );
+ bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode1), nBddSizeMax, pProgress, pCounter, fVerbose );
+ if ( bFunc1 == NULL )
+ return NULL;
+ Cudd_Ref( bFunc1 );
+
+ // complement the branch BDDs
+ bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjIsComplement(pNode0) );
+ bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjIsComplement(pNode1) );
+ // get the final result
+ bFunc = Cudd_bddIte( dd, bFuncC, bFunc1, bFunc0 ); Cudd_Ref( bFunc );
+ Cudd_RecursiveDeref( dd, bFunc0 );
+ Cudd_RecursiveDeref( dd, bFunc1 );
+ Cudd_RecursiveDeref( dd, bFuncC );
+ // add the number of used nodes
+ (*pCounter) += 3;
+ }
+ else
+ {
+ // compute the result for both branches
+ bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose );
+ if ( bFunc0 == NULL )
+ return NULL;
+ Cudd_Ref( bFunc0 );
+ bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose );
+ if ( bFunc1 == NULL )
+ return NULL;
+ Cudd_Ref( bFunc1 );
+ bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
+ bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
+ // get the final result
+ bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
+ Cudd_RecursiveDeref( dd, bFunc0 );
+ Cudd_RecursiveDeref( dd, bFunc1 );
+ // add the number of used nodes
+ (*pCounter)++;
+ }
+ // set the result
+ assert( pNode->pCopy == NULL );
+ pNode->pCopy = (Abc_Obj_t *)bFunc;
+ // increment the progress bar
+ if ( pProgress )
+ Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
+ }
+ // prepare the return value
+ bFunc = (DdNode *)pNode->pCopy;
+ // dereference BDD at the node
+ if ( --pNode->vFanouts.nSize == 0 )
+ {
+ Cudd_Deref( bFunc );
+ pNode->pCopy = NULL;
+ }
return bFunc;
}
diff --git a/src/base/abci/abcOrder.c b/src/base/abci/abcOrder.c
new file mode 100644
index 00000000..c9ebdc12
--- /dev/null
+++ b/src/base/abci/abcOrder.c
@@ -0,0 +1,131 @@
+/**CFile****************************************************************
+
+ FileName [abcOrder.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Exploring static BDD variable orders.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcOrder.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkChangeCiOrder( Abc_Ntk_t * pNtk, Vec_Ptr_t * vSupp, int fReverse );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Changes the order of primary inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkFindCiOrder( Abc_Ntk_t * pNtk, int fReverse, int fVerbose )
+{
+ Vec_Ptr_t * vSupp;
+ vSupp = Abc_NtkSupport( pNtk );
+ Abc_NtkChangeCiOrder( pNtk, vSupp, fReverse );
+ Vec_PtrFree( vSupp );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements the given variable order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, int fVerbose )
+{
+ char Buffer[1000];
+ FILE * pFile;
+ Vec_Ptr_t * vSupp;
+ Abc_Obj_t * pObj;
+ pFile = fopen( pFileName, "r" );
+ vSupp = Vec_PtrAlloc( Abc_NtkCiNum(pNtk) );
+ while ( fscanf( pFile, "%s", Buffer ) == 1 )
+ {
+ pObj = Abc_NtkFindTerm( pNtk, Buffer );
+ if ( pObj == NULL || !Abc_ObjIsCi(pObj) )
+ {
+ printf( "Name \"%s\" is not a PI name. Cannot use this order.\n", Buffer );
+ Vec_PtrFree( vSupp );
+ fclose( pFile );
+ return;
+ }
+ Vec_PtrPush( vSupp, pObj );
+ }
+ fclose( pFile );
+ if ( Vec_PtrSize(vSupp) != Abc_NtkCiNum(pNtk) )
+ {
+ printf( "The number of names in the order (%d) is not the same as the number of PIs (%d).\n", Vec_PtrSize(vSupp), Abc_NtkCiNum(pNtk) );
+ Vec_PtrFree( vSupp );
+ return;
+ }
+ Abc_NtkChangeCiOrder( pNtk, vSupp, fReverse );
+ Vec_PtrFree( vSupp );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Changes the order of primary inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkChangeCiOrder( Abc_Ntk_t * pNtk, Vec_Ptr_t * vSupp, int fReverse )
+{
+ Abc_Obj_t * pObj;
+ int i;
+ assert( Vec_PtrSize(vSupp) == Abc_NtkCiNum(pNtk) );
+ // order CIs using the array
+ if ( fReverse )
+ Vec_PtrForEachEntry( vSupp, pObj, i )
+ Vec_PtrWriteEntry( pNtk->vCis, Vec_PtrSize(vSupp)-1-i, pObj );
+ else
+ Vec_PtrForEachEntry( vSupp, pObj, i )
+ Vec_PtrWriteEntry( pNtk->vCis, i, pObj );
+ // order PIs accordingly
+ Vec_PtrClear( pNtk->vPis );
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ if ( Abc_ObjIsPi(pObj) )
+ Vec_PtrPush( pNtk->vPis, pObj );
+// Abc_NtkForEachCi( pNtk, pObj, i )
+// printf( "%s ", Abc_ObjName(pObj) );
+// printf( "\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 5d35678d..2e338e48 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -15,6 +15,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcMap.c \
src/base/abci/abcMiter.c \
src/base/abci/abcNtbdd.c \
+ src/base/abci/abcOrder.c \
src/base/abci/abcPga.c \
src/base/abci/abcPrint.c \
src/base/abci/abcProve.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-19 20:27:41 +0000