diff options
Diffstat (limited to 'src/aig/fra')
| -rw-r--r-- | src/aig/fra/fra.h | 2 | ||||
| -rw-r--r-- | src/aig/fra/fraCec.c | 58 |
2 files changed, 57 insertions, 3 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index ee4e9115..dbe61522 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -258,7 +258,7 @@ static inline int Fra_ImpCreate( int Left, int Right ) /*=== fraCec.c ========================================================*/ extern int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ); extern int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose ); -extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int fVerbose ); +extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fVerbose ); /*=== fraClass.c ========================================================*/ extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj ); extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); 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 /// |