diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-04-03 20:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-04-03 20:01:00 -0700 |
| commit | 69b5bcad56f9352eea80d3e9b5e1322782522059 (patch) | |
| tree | 9381d7ce208e93fc82efc5606bcd59ec1dbed765 /src/aig/fra/fraCec.c | |
| parent | 087951655efdc20b5b4beb64b15edf86a27850a8 (diff) | |
| download | abc-69b5bcad56f9352eea80d3e9b5e1322782522059.tar.gz abc-69b5bcad56f9352eea80d3e9b5e1322782522059.tar.bz2 abc-69b5bcad56f9352eea80d3e9b5e1322782522059.zip | |
Version abc80403_2
Diffstat (limited to 'src/aig/fra/fraCec.c')
| -rw-r--r-- | src/aig/fra/fraCec.c | 30 |
1 files changed, 21 insertions, 9 deletions
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index 779337bf..05f2493a 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -166,8 +166,7 @@ PRT( "Time", clock() - clk ); // duplicate the AIG clk = clock(); -// pAig = Aig_ManDupDfs( pTemp = pAig ); - pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 ); + pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 ); Aig_ManStop( pTemp ); if ( fVerbose ) { @@ -247,22 +246,25 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fVerbose ) +int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose ) { Aig_Man_t * pAig; Vec_Ptr_t * vParts; int i, RetValue = 1, nOutputs; // create partitions - vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize ); + vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize, fSmart ); // solve the partitions nOutputs = -1; Vec_PtrForEachEntry( vParts, pAig, i ) { nOutputs++; if ( fVerbose ) + { printf( "Verifying part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAig), Aig_ManPoNum(pAig), Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); + fflush( stdout ); + } RetValue = Fra_FraigMiterStatus( pAig ); if ( RetValue == 1 ) continue; @@ -306,8 +308,9 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize SeeAlso [] ***********************************************************************/ -int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int fPartition, int fVerbose ) +int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose ) { + Aig_Man_t * pTemp; //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose ); int RetValue, clkTotal = clock(); @@ -324,10 +327,19 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int f assert( Aig_ManPiNum(pMan1) == Aig_ManPiNum(pMan1) ); assert( Aig_ManPoNum(pMan1) == Aig_ManPoNum(pMan1) ); - if ( fPartition ) - RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, 100, fVerbose ); - else - RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), fVerbose ); + // make sure that the first miter has more nodes + if ( Aig_ManNodeNum(pMan1) < Aig_ManNodeNum(pMan2) ) + { + pTemp = pMan1; + pMan1 = pMan2; + pMan2 = pTemp; + } + assert( Aig_ManNodeNum(pMan1) >= Aig_ManNodeNum(pMan2) ); + + if ( nPartSize ) + RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nPartSize, fSmart, fVerbose ); + else // no partitioning + RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), 0, fVerbose ); // report the miter if ( RetValue == 1 ) |