diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-23 15:34:49 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-23 15:34:49 -0700 |
commit | 637da8baeaabf6f12aa8d9ec287aa675d9ea5fab (patch) | |
tree | 628e631e30dff964ead2df3ceb74000a2b7f9b3f | |
parent | 3712dd30d0e6152e627b487f7f4f5e4e6f6c5afd (diff) | |
download | abc-637da8baeaabf6f12aa8d9ec287aa675d9ea5fab.tar.gz abc-637da8baeaabf6f12aa8d9ec287aa675d9ea5fab.tar.bz2 abc-637da8baeaabf6f12aa8d9ec287aa675d9ea5fab.zip |
Added switch 'satclp -Z' to control the max size of the cone to work with.
-rw-r--r-- | src/base/abc/abc.h | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 21 | ||||
-rw-r--r-- | src/base/abci/abcCollapse.c | 26 |
3 files changed, 37 insertions, 12 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 450aaafe..54fa12bd 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -600,7 +600,7 @@ extern ABC_DLL int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk ); extern ABC_DLL int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk ); /*=== abcCollapse.c ==========================================================*/ extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ); -extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); +extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose ); /*=== abcCut.c ==========================================================*/ extern ABC_DLL void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree ); extern ABC_DLL void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2a71fd7a..9b62c622 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3104,6 +3104,7 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; int nCubeLim = 1000; int nBTLimit = 1000000; + int nCostMax = 20000000; int fCanon = 0; int fReverse = 0; int fVerbose = 0; @@ -3111,7 +3112,7 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CLcrvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CLZcrvh" ) ) != EOF ) { switch ( c ) { @@ -3137,6 +3138,17 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nBTLimit < 0 ) goto usage; break; + case 'Z': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Z\" should be followed by an integer.\n" ); + goto usage; + } + nCostMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCostMax < 0 ) + goto usage; + break; case 'c': fCanon ^= 1; break; @@ -3167,11 +3179,11 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network if ( Abc_NtkIsStrash(pNtk) ) - pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose ); else { pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 ); - pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose ); Abc_NtkDelete( pNtk ); } if ( pNtkRes == NULL ) @@ -3184,10 +3196,11 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: satclp [-CL num] [-crvh]\n" ); + Abc_Print( -2, "usage: satclp [-CLZ num] [-crvh]\n" ); Abc_Print( -2, "\t performs SAT based collapsing\n" ); Abc_Print( -2, "\t-C num : the limit on the SOP size of one output [default = %d]\n", nCubeLim ); Abc_Print( -2, "\t-L num : the limit on the number of conflicts in one SAT call [default = %d]\n", nBTLimit ); + Abc_Print( -2, "\t-Z num : the limit on the cost of the largest output [default = %d]\n", nCostMax ); Abc_Print( -2, "\t-c : toggles using canonical ISOP computation [default = %s]\n", fCanon? "yes": "no" ); Abc_Print( -2, "\t-r : toggles using reverse veriable ordering [default = %s]\n", fReverse? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index e4bfa885..e6618e15 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -368,7 +368,7 @@ Vec_Ptr_t * Abc_NtkCreateCoOrder( Abc_Ntk_t * pNtk, Vec_Wec_t * vSupps ) Vec_Ptr_t * vNodes = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) { - pNode->iTemp = Vec_IntSize( Vec_WecEntry(vSupps, Abc_ObjFanin0(pNode)->Id) ); + pNode->iTemp = Vec_IntSize( Vec_WecEntry(vSupps, Abc_ObjFaninId0(pNode)) ); Vec_PtrPush( vNodes, pNode ); } // order objects alphabetically @@ -412,15 +412,15 @@ Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, Vec_StrFree( vSop ); return pNodeNew; } -Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose ) { ProgressBar * pProgress; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pNode, * pDriver, * pNodeNew; - Vec_Ptr_t * vDriverCopy, * vCoNodes; - Vec_Int_t * vNodeCoIds; + Vec_Ptr_t * vDriverCopy, * vCoNodes, * vDfsNodes; + Vec_Int_t * vNodeCoIds, * vLevel; Vec_Wec_t * vSupps; - int i; + int i, Cost; // Abc_NtkForEachCi( pNtk, pNode, i ) // printf( "%d ", Abc_ObjFanoutNum(pNode) ); @@ -430,6 +430,18 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f vSupps = Abc_NtkCreateCoSupps( pNtk, fVerbose ); // order CO nodes by support size vCoNodes = Abc_NtkCreateCoOrder( pNtk, vSupps ); + // compute cost of the largest node + pNode = (Abc_Obj_t *)Vec_PtrEntry( vCoNodes, 0 ); + vDfsNodes = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); + vLevel = Vec_WecEntry( vSupps, Abc_ObjFaninId0(pNode) ); + Cost = Vec_PtrSize(vDfsNodes) * Vec_IntSize(vLevel) * nCubeLim; + Vec_PtrFree( vDfsNodes ); + if ( Cost > nCostMax ) + { + Vec_PtrFree( vCoNodes ); + Vec_WecFree( vSupps ); + return NULL; + } // collect CO IDs in this order vNodeCoIds = Vec_IntAlloc( Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) @@ -487,12 +499,12 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f Extra_ProgressBarStop( pProgress ); return pNtkNew; } -Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose ) { Abc_Ntk_t * pNtkNew; assert( Abc_NtkIsStrash(pNtk) ); // create the new network - pNtkNew = Abc_NtkFromSops( pNtk, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + pNtkNew = Abc_NtkFromSops( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose ); if ( pNtkNew == NULL ) return NULL; if ( pNtk->pExdc ) |