diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 140 | ||||
-rw-r--r-- | src/base/abci/abcClpBdd.c | 7 | ||||
-rw-r--r-- | src/base/abci/abcIvy.c | 69 | ||||
-rw-r--r-- | src/base/abci/abcMiter.c | 1 | ||||
-rw-r--r-- | src/base/abci/abcNtbdd.c | 154 | ||||
-rw-r--r-- | src/base/abci/abcOrder.c | 131 | ||||
-rw-r--r-- | src/base/abci/module.make | 1 |
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 \ |