luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Dumping BDD variable order after 'clp'.

This commit is contained in:
Alan Mishchenko 2020-05-18 16:02:57 -07:00
parent 0ae0744e73
commit 97c826a6e6
6 changed files with 27 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/base/abc/abc.h
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 fReverse, int fVerbose );
extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, 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 ==========================================================*/

14
src/base/abci/abc.c
View File

@ -3355,6 +3355,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
int fDualRail;
int fReorder;
int fReverse;
int fDumpOrder;
int c;
char * pLogFileName = NULL;
pNtk = Abc_FrameReadNtk(pAbc);
@ -3364,9 +3365,10 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
fReorder = 1;
fReverse = 0;
fDualRail = 0;
fDumpOrder = 0;
fBddSizeMax = ABC_INFINITY;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "BLrodvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "BLrodxvh" ) ) != EOF )
{
switch ( c )
{
@ -3399,6 +3401,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDualRail ^= 1;
break;
case 'x':
fDumpOrder ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -3423,11 +3428,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, fReverse, fVerbose );
pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fDumpOrder, fVerbose );
else
{
pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fVerbose );
pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fReverse, fDumpOrder, fVerbose );
Abc_NtkDelete( pNtk );
}
if ( pNtkRes == NULL )
@ -3450,13 +3455,14 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: collapse [-B <num>] [-L file] [-rodvh]\n" );
Abc_Print( -2, "usage: collapse [-B <num>] [-L file] [-rodxvh]\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-L file : the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
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-x : toggles dumping file \"order.txt\" with variable order [default = %s]\n", fDumpOrder? "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");
return 1;

15
src/base/abci/abcCollapse.c
View File

@ -195,7 +195,16 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk, int fReverse )
Extra_ProgressBarStop( pProgress );
return pNtkNew;
}
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fVerbose )
void Abc_NtkDumpVariableOrder( Abc_Ntk_t * pNtk )
{
DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
FILE * pFile = fopen( "order.txt", "wb" ); int i;
for ( i = 0; i < dd->size; i++ )
fprintf( pFile, "%d ", dd->invperm[i] );
fprintf( pFile, "\n" );
fclose( pFile );
}
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, int fVerbose )
{
Abc_Ntk_t * pNtkNew;
abctime clk = Abc_Clock();
@ -210,6 +219,8 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
ABC_PRT( "BDD construction time", Abc_Clock() - clk );
}
if ( fDumpOrder )
Abc_NtkDumpVariableOrder( pNtk );
// create the new network
pNtkNew = Abc_NtkFromGlobalBdds( pNtk, fReverse );
@ -236,7 +247,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 fReverse, int fVerbose )
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, int fVerbose )
{
return NULL;
}

2
src/base/abci/abcIvy.c
View File

@ -601,7 +601,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, 0 );
pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0, 0 );
if ( pNtk )
{
Abc_NtkDelete( pNtkTemp );

2
src/base/abci/abcLutmin.c
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, 0 );
pNtkNew = Abc_NtkCollapse( pTemp = pNtkNew, 10000, 0, 1, 0, 0, 0 );
Abc_NtkDelete( pTemp );
if ( pNtkNew == NULL )
return NULL;

2
src/base/abci/abcProve.c
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, 0 );
pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0, 0, 0 );
if ( pNtk )
{
Abc_NtkDelete( pNtkTemp );