Adding switch 'clp -o' to reverse initial variable ordering.

This commit is contained in:
Alan Mishchenko 2018-06-07 15:53:12 -07:00
parent aae37ffd4c
commit b729c737b5
17 changed files with 41 additions and 36 deletions

View File

@ -600,7 +600,7 @@ extern ABC_DLL int Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk );
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_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, 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 fCnfShared, int fVerbose );
extern ABC_DLL Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk );
/*=== abcCut.c ==========================================================*/
@ -761,7 +761,7 @@ extern ABC_DLL Abc_Ntk_t * Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk );
/*=== abcNtbdd.c ==========================================================*/
extern ABC_DLL Abc_Ntk_t * Abc_NtkDeriveFromBdd( void * dd, void * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
extern ABC_DLL Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
extern ABC_DLL void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
extern ABC_DLL void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fReverse, int fVerbose );
extern ABC_DLL void * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan );
extern ABC_DLL int Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk );
/*=== abcNtk.c ==========================================================*/

View File

@ -3237,16 +3237,18 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
int fBddSizeMax;
int fDualRail;
int fReorder;
int fReverse;
int c;
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
fVerbose = 0;
fReorder = 1;
fReverse = 0;
fDualRail = 0;
fBddSizeMax = ABC_INFINITY;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Brdvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Brodvh" ) ) != EOF )
{
switch ( c )
{
@ -3261,15 +3263,18 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fBddSizeMax < 0 )
goto usage;
break;
case 'r':
fReorder ^= 1;
break;
case 'o':
fReverse ^= 1;
break;
case 'd':
fDualRail ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'r':
fReorder ^= 1;
break;
case 'h':
goto usage;
default:
@ -3291,11 +3296,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, fVerbose );
pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fVerbose );
else
{
pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fVerbose );
Abc_NtkDelete( pNtk );
}
if ( pNtkRes == NULL )
@ -3308,10 +3313,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: collapse [-B <num>] [-rdvh]\n" );
Abc_Print( -2, "usage: collapse [-B <num>] [-rodvh]\n" );
Abc_Print( -2, "\t collapses the network by constructing global BDDs\n" );
Abc_Print( -2, "\t-B <num>: limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax );
Abc_Print( -2, "\t-r : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
Abc_Print( -2, "\t-o : toggles reverse variable ordering [default = %s]\n", fReverse? "yes": "no" );
Abc_Print( -2, "\t-d : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" );
Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -13144,7 +13150,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Cba_PrsReadBlifTest();
}
// Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
Abc_EnumeratePathsTest();
// Abc_EnumeratePathsTest();
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );

View File

@ -62,7 +62,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
Abc_Obj_t * pObj;
// compute the global BDDs
if ( Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, fVerbose) == NULL )
if ( Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, 0, fVerbose) == NULL )
return;
// get information about the network

View File

@ -70,7 +70,7 @@ Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVer
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL )
if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, 0, fVerbose) == NULL )
return NULL;
if ( fVerbose )

View File

@ -1010,7 +1010,7 @@ Abc_Ntk_t * Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose )
int i;
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkCoNum(pNtk) <= BDD_FUNC_MAX );
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddSizeMax, fDropInternal, fReorder, fVerbose );
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddSizeMax, fDropInternal, fReorder, 0, fVerbose );
if ( dd == NULL )
{
Abc_Print( -1, "Construction of global BDDs has failed.\n" );

View File

@ -118,7 +118,7 @@ int Abc_NtkMinimumBase2( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc )
Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc, int fReverse )
{
Abc_Obj_t * pNodeNew, * pTemp;
int i;
@ -126,12 +126,12 @@ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode
pNodeNew = Abc_NtkCreateNode( pNtkNew );
// add the fanins in the order, in which they appear in the reordered manager
Abc_NtkForEachCi( pNtkNew, pTemp, i )
Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, dd->invperm[i]) );
Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, fReverse ? Abc_NtkCiNum(pNtkNew)-1-dd->invperm[i] : dd->invperm[i]) );
// transfer the function
pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( (DdNode *)pNodeNew->pData );
return pNodeNew;
}
Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk, int fReverse )
{
ProgressBar * pProgress;
Abc_Ntk_t * pNtkNew;
@ -147,7 +147,7 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
assert( Abc_NtkIsStrash(pNtk->pExdc) );
assert( Abc_NtkCoNum(pNtk->pExdc) == 1 );
// compute the global BDDs
if ( Abc_NtkBuildGlobalBdds(pNtk->pExdc, 10000000, 1, 1, 0) == NULL )
if ( Abc_NtkBuildGlobalBdds(pNtk->pExdc, 10000000, 1, 1, 0, 0) == NULL )
return NULL;
// transfer tot the same manager
ddExdc = (DdManager *)Abc_NtkGlobalBddMan( pNtk->pExdc );
@ -188,21 +188,21 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy );
continue;
}
pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)Abc_ObjGlobalBdd(pNode) );
pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)Abc_ObjGlobalBdd(pNode), fReverse );
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
}
Extra_ProgressBarStop( pProgress );
return pNtkNew;
}
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fVerbose )
{
Abc_Ntk_t * pNtkNew;
abctime clk = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL )
if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fReverse, fVerbose) == NULL )
return NULL;
if ( fVerbose )
{
@ -212,7 +212,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
}
// create the new network
pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
pNtkNew = Abc_NtkFromGlobalBdds( pNtk, fReverse );
Abc_NtkFreeGlobalBdds( pNtk, 1 );
if ( pNtkNew == NULL )
return NULL;
@ -236,7 +236,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
#else
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fVerbose )
{
return NULL;
}

View File

@ -67,7 +67,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, int fVerbose, int fPrint, int fS
DdManager * dd;
Abc_Ntk_t * pNtkNew;
assert( Abc_NtkIsStrash(pNtk) );
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, 0, fVerbose );
if ( dd == NULL )
return NULL;
if ( fVerbose )

View File

@ -2983,8 +2983,8 @@ void Abc_ExactStoreTest( int fVerbose )
Abc_Ntk_t * pNtk;
Abc_Obj_t * pFanins[4];
Vec_Ptr_t * vNames;
char pPerm[4];
int Cost;
char pPerm[4] = {0};
int Cost = 0;
pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
pNtk->pName = Extra_UtilStrsav( "exact" );

View File

@ -600,7 +600,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
fflush( stdout );
}
pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0 );
if ( pNtk )
{
Abc_NtkDelete( pNtkTemp );

View File

@ -739,7 +739,7 @@ Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fVerbose )
else
pNtkNew = Abc_NtkStrash( pNtkInit, 0, 1, 0 );
// collapse the network
pNtkNew = Abc_NtkCollapse( pTemp = pNtkNew, 10000, 0, 1, 0 );
pNtkNew = Abc_NtkCollapse( pTemp = pNtkNew, 10000, 0, 1, 0, 0 );
Abc_NtkDelete( pTemp );
if ( pNtkNew == NULL )
return NULL;

View File

@ -254,7 +254,7 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
SeeAlso []
***********************************************************************/
void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fReverse, int fVerbose )
{
ProgressBar * pProgress;
Abc_Obj_t * pObj, * pFanin;
@ -287,8 +287,7 @@ void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInter
Abc_NtkForEachCi( pNtk, pObj, i )
if ( Abc_ObjFanoutNum(pObj) > 0 )
{
bFunc = dd->vars[i];
// bFunc = dd->vars[Abc_NtkCiNum(pNtk) - 1 - i];
bFunc = fReverse ? dd->vars[Abc_NtkCiNum(pNtk) - 1 - i] : dd->vars[i];
Abc_ObjSetGlobalBdd( pObj, bFunc ); Cudd_Ref( bFunc );
}

View File

@ -201,7 +201,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
fflush( stdout );
}
clk = Abc_Clock();
pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0 );
if ( pNtk )
{
Abc_NtkDelete( pNtkTemp );

View File

@ -271,7 +271,7 @@ void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fP
assert( Abc_ObjFanoutNum(Abc_NtkPo(pNtk,0)) == 0 ); // PO should go first
// compute the global BDDs of the latches
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, fVerbose );
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, 0, fVerbose );
if ( dd == NULL )
{
printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );

View File

@ -99,7 +99,7 @@ void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fReorder, int
// compute the global functions
clk = Abc_Clock();
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, fReorder, fVerbose );
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, fReorder, 0, fVerbose );
printf( "Shared BDD size = %d nodes.\n", Abc_NtkSizeOfGlobalBdds(pNtk) );
Cudd_AutodynDisable( dd );
if ( !fGarbCollect )

View File

@ -82,7 +82,7 @@ void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose )
abctime clkBdd, clkUnate;
// compute the global BDDs
dd = (DdManager *)Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, fVerbose);
dd = (DdManager *)Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, 0, fVerbose);
if ( dd == NULL )
return;
clkBdd = Abc_Clock() - clk;

View File

@ -67,7 +67,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, int fVerbose )
}
// compute the global BDDs of the latches
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, 0, fVerbose );
if ( dd == NULL )
return 0;
if ( fVerbose )

View File

@ -390,7 +390,7 @@ int Io_WriteMoPlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
Abc_Obj_t * pObj;
int i;
assert( Abc_NtkIsStrash(pNtk) );
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, 0, fVerbose );
if ( dd == NULL )
return 0;
if ( fVerbose )