diff options
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abcMiter.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abcPrint.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abcVerify.c | 34 | ||||
| -rw-r--r-- | src/base/io/ioReadBlifMv.c | 7 |
4 files changed, 40 insertions, 5 deletions
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index feeaa617..8c5a4a83 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int n assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) ); assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) ); // check that the networks have the same PIs/POs/latches - if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 0, fComb ) ) + if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fImplic, fComb ) ) return NULL; // make sure the circuits are strashed fRemove1 = (!Abc_NtkIsStrash(pNtk1) || Abc_NtkGetChoiceNum(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0)); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 38b21a13..d6883105 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -380,6 +380,8 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum // printf( "The total number of cube pairs = %d.\n", Abc_NtkGetCubePairNum(pNtk) ); fflush( stdout ); + if ( pNtk->pExdc ) + Abc_NtkPrintStats( pNtk->pExdc, fFactored, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes, fPower, fGlitch ); } /**Function************************************************************* diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 8367d23c..7d9973b1 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -125,9 +125,32 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV Prove_Params_t Params, * pParams = &Params; // Fraig_Params_t Params; // Fraig_Man_t * pMan; - Abc_Ntk_t * pMiter; + Abc_Ntk_t * pMiter, * pTemp; + Abc_Ntk_t * pExdc = NULL; int RetValue; + if ( pNtk1->pExdc != NULL || pNtk2->pExdc != NULL ) + { + if ( pNtk1->pExdc != NULL && pNtk2->pExdc != NULL ) + { + printf( "Comparing EXDC of the two networks:\n" ); + Abc_NtkCecFraig( pNtk1->pExdc, pNtk2->pExdc, nSeconds, fVerbose ); + printf( "Comparing networks under EXDC of the first network.\n" ); + pExdc = pNtk1->pExdc; + } + else if ( pNtk1->pExdc != NULL ) + { + printf( "Second network has no EXDC. Comparing main networks under EXDC of the first network.\n" ); + pExdc = pNtk1->pExdc; + } + else if ( pNtk2->pExdc != NULL ) + { + printf( "First network has no EXDC. Comparing main networks under EXDC of the second network.\n" ); + pExdc = pNtk2->pExdc; + } + else assert( 0 ); + } + // get the miter of the two networks pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0, 0 ); if ( pMiter == NULL ) @@ -135,6 +158,15 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV printf( "Miter computation has failed.\n" ); return; } + // add EXDC to the miter + if ( pExdc ) + { + assert( Abc_NtkPoNum(pMiter) == 1 ); + assert( Abc_NtkPoNum(pExdc) == 1 ); + pMiter = Abc_NtkMiter( pTemp = pMiter, pExdc, 1, 0, 1, 0 ); + Abc_NtkDelete( pTemp ); + } + // handle trivial case RetValue = Abc_NtkMiterIsConstant( pMiter ); if ( RetValue == 0 ) { diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 5b2a760a..e14c22c2 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -210,7 +210,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) { pNtk = (Abc_Ntk_t *)Vec_PtrEntry(pDesign->vModules, 0); Vec_PtrForEachEntryStart( Abc_Ntk_t *, pDesign->vModules, pExdc, i, 1 ) - if ( !strcmp(pExdc->pName, "exdc") ) + if ( !strcmp(pExdc->pName, "EXDC") ) { assert( pNtk->pExdc == NULL ); pNtk->pExdc = pExdc; @@ -678,7 +678,8 @@ static void Io_MvReadPreparse( Io_MvMan_t * p ) } else if ( !strncmp(pCur, "exdc", 4) ) { - fprintf( stdout, "Line %d: The design contains EXDC network (warning only).\n", Io_MvGetLine(p, pCur) ); +// fprintf( stdout, "Line %d: The design contains EXDC network (warning only).\n", Io_MvGetLine(p, pCur) ); + fprintf( stdout, "Warning: The design contains EXDC network.\n" ); if ( p->pLatest ) Vec_PtrPush( p->vModels, p->pLatest ); p->pLatest = Io_MvModAlloc(); @@ -928,7 +929,7 @@ static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine ) if ( pLine == NULL ) { p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 ); - p->pNtk->pName = Extra_UtilStrsav( "exdc" ); + p->pNtk->pName = Extra_UtilStrsav( "EXDC" ); return 1; } Io_MvSplitIntoTokens( vTokens, pLine, '\0' ); |