From 97c826a6e63eb0020920819595f4da8f2cc674ba Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 18 May 2020 16:02:57 -0700 Subject: Dumping BDD variable order after 'clp'. --- src/base/abc/abc.h | 2 +- src/base/abci/abc.c | 14 ++++++++++---- src/base/abci/abcCollapse.c | 15 +++++++++++++-- src/base/abci/abcIvy.c | 2 +- src/base/abci/abcLutmin.c | 2 +- src/base/abci/abcProve.c | 2 +- 6 files changed, 27 insertions(+), 10 deletions(-) diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 312354da..c36bde70 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -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 ==========================================================*/ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b7f0517e..411f66ed 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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 ] [-L file] [-rodvh]\n" ); + Abc_Print( -2, "usage: collapse [-B ] [-L file] [-rodxvh]\n" ); Abc_Print( -2, "\t collapses the network by constructing global BDDs\n" ); Abc_Print( -2, "\t-B : 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; diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index ca54d542..136712cb 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -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; } diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 5dc125d0..3f268ea2 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -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 ); diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c index 2ac44060..be01beb6 100644 --- a/src/base/abci/abcLutmin.c +++ b/src/base/abci/abcLutmin.c @@ -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; diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c index 03722926..b14c0827 100644 --- a/src/base/abci/abcProve.c +++ b/src/base/abci/abcProve.c @@ -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 ); -- cgit v1.2.3