diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-03-30 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-03-30 08:01:00 -0700 |
commit | 2c7f6e39b84d29db096388459db7583c01b79b01 (patch) | |
tree | 7fd628f0ac0391c45d2f8c95483887a984b8789c /src/aig/fra/fraCec.c | |
parent | 93c3f16066b69c840dc636f827f5f3ca18749906 (diff) | |
download | abc-2c7f6e39b84d29db096388459db7583c01b79b01.tar.gz abc-2c7f6e39b84d29db096388459db7583c01b79b01.tar.bz2 abc-2c7f6e39b84d29db096388459db7583c01b79b01.zip |
Version abc80330
Diffstat (limited to 'src/aig/fra/fraCec.c')
-rw-r--r-- | src/aig/fra/fraCec.c | 58 |
1 files changed, 56 insertions, 2 deletions
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index bdab25dd..aead8c9e 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -247,13 +247,13 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int fVerbose ) +int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fVerbose ) { Aig_Man_t * pAig; Vec_Ptr_t * vParts; int i, RetValue = 1, nOutputs; // create partitions - vParts = Aig_ManMiterPartitioned( pMan1, pMan2, 100 ); + vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize ); // solve the partitions nOutputs = -1; Vec_PtrForEachEntry( vParts, pAig, i ) @@ -295,6 +295,60 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int fVerbose return RetValue; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int fPartition, int fVerbose ) +{ + //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose ); + int RetValue, clkTotal = clock(); + + if ( Aig_ManPiNum(pMan1) != Aig_ManPiNum(pMan1) ) + { + printf( "Abc_CommandAbc8Cec(): Miters have different number of PIs.\n" ); + return 0; + } + if ( Aig_ManPoNum(pMan1) != Aig_ManPoNum(pMan1) ) + { + printf( "Abc_CommandAbc8Cec(): Miters have different number of POs.\n" ); + return 0; + } + 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 ); + + // report the miter + if ( RetValue == 1 ) + { + printf( "Networks are equivalent. " ); +PRT( "Time", clock() - clkTotal ); + } + else if ( RetValue == 0 ) + { + printf( "Networks are NOT EQUIVALENT. " ); +PRT( "Time", clock() - clkTotal ); + } + else + { + printf( "Networks are UNDECIDED. " ); +PRT( "Time", clock() - clkTotal ); + } + fflush( stdout ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |