diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index efc85813b..6e77e26c0 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -189,6 +189,7 @@ struct Gia_Man_t_ Vec_Int_t * vCoNumsOrig; // original CO names Vec_Int_t * vIdsOrig; // original object IDs Vec_Int_t * vIdsEquiv; // original object IDs proved equivalent + Vec_Int_t * vEquLitIds; // original object IDs proved equivalent Vec_Int_t * vCofVars; // cofactoring variables Vec_Vec_t * vClockDoms; // clock domains Vec_Flt_t * vTiming; // arrival/required/slack @@ -1729,7 +1730,7 @@ extern void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBox extern Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres ); extern Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxesLeft ); extern Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres, int fSeq ); -extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec ); +extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fNameMap, int fDumpFiles, int fVerbose, char * pFileSpec ); extern Vec_Int_t * Gia_ManDeriveBoxMapping( Gia_Man_t * pGia ); /*=== giaTruth.c ===========================================================*/ extern word Gia_LutComputeTruth6( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTruths ); diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index cd35586ea..85b48b118 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -907,6 +907,25 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi printf( "Cannot read extension \"w\" because AIG is rehashed. Use \"&r -s \".\n" ); Vec_IntFree( vPairs ); } + // read object ID mapping + else if ( *pCur == 'y' ) + { + pCur++; + int nInts = Gia_AigerReadInt(pCur)/4; pCur += 4; + if ( fSkipStrash ) { + pNew->vEquLitIds = Vec_IntStart( nInts ); + memcpy( Vec_IntArray(pNew->vEquLitIds), pCur, (size_t)4*nInts ); + if ( Vec_IntSize(pNew->vEquLitIds) != Gia_ManObjNum(pNew) ) { + printf( "Cannot read extension \"y\" because object count changed. Use \"&r -s \".\n" ); + Vec_IntFreeP( &pNew->vEquLitIds ); + } + else if ( fVerbose ) printf( "Finished reading extension \"y\".\n" ); + } + else { + if ( fVerbose ) printf( "Cannot read extension \"y\" because AIG is rehashed. Use \"&r -s \".\n" ); + } + pCur += 4*nInts; + } else break; } } @@ -1529,6 +1548,7 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in Gia_FileWriteBufferSize( pFile, Vec_IntSize(p->vRegClasses) ); for ( i = 0; i < Vec_IntSize(p->vRegClasses); i++ ) Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegClasses, i) ); + if ( fVerbose ) printf( "Finished writing extension \"r\".\n" ); } // write register inits if ( p->vRegInits ) @@ -1677,6 +1697,15 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in assert( Vec_IntSize(p->vObjClasses) == Gia_ManObjNum(p) ); fwrite( Vec_IntArray(p->vObjClasses), 1, 4*Gia_ManObjNum(p), pFile ); } + // write object classes + if ( p->vEquLitIds ) + { + fprintf( pFile, "y" ); + Gia_FileWriteBufferSize( pFile, 4*Gia_ManObjNum(p) ); + assert( Vec_IntSize(p->vEquLitIds) == Gia_ManObjNum(p) ); + fwrite( Vec_IntArray(p->vEquLitIds), 1, 4*Gia_ManObjNum(p), pFile ); + if ( fVerbose ) printf( "Finished writing extension \"y\".\n" ); + } // write name if ( p->pName ) { @@ -1916,4 +1945,3 @@ int main( int argc, char ** argv ) ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 72ec211ef..84a41d1dd 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -106,6 +106,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vCofVars ); Vec_IntFreeP( &p->vIdsOrig ); Vec_IntFreeP( &p->vIdsEquiv ); + Vec_IntFreeP( &p->vEquLitIds ); Vec_IntFreeP( &p->vLutConfigs ); Vec_IntFreeP( &p->vEdgeDelay ); Vec_IntFreeP( &p->vEdgeDelayR ); @@ -641,7 +642,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars ) } if ( pPars && pPars->fSlacks ) Gia_ManDfsSlacksPrint( p ); - if ( Gia_ManHasMapping(p) && pPars->fMapOutStats ) + if ( Gia_ManHasMapping(p) && pPars && pPars->fMapOutStats ) Gia_ManPrintOutputLutStats( p ); } diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 17f03aa4a..271c6d4ee 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -952,7 +952,114 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v SeeAlso [] ***********************************************************************/ -int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec ) + +/* +› Please have a look at how name mapping is done in procedure Abc_FrameReadMiniLutNameMapping() in file "src/aig/gia/ + giaMini.c". The main idea is to map the object IDs in the design after synthesis (pAbc->pGiaMiniLut) into the object IDs in + the design before synthesis (pAbc->pGiaMiniAig). The computation is divided into three steps: (1) computing object + equivalences using Gia_ManComputeGiaEquivs(), which annotates the input AIG (pGia) containing both designs before and after + synthesis with equivalence class information; this information contains equivalence classes of objects from both designs; (2) + creating a map (pRes) of the resulting object IDs (in pAbc->pGiaMiniLut) into the original object IDs (in pAbc->pGiaMiniAig) + using procedure Gia_ManMapMiniLut2MiniAig(); this map is enabled by having two arrays (one of them is pAbc->vCopyMiniAig + mapping objects of pAbc->pGiaMiniAig in the original object IDs; the other one is pAbc->vCopyMiniLut mapping objects of + pAbc->pGiaMiniLut into the IDs of pAbc->pGiaMiniLut); (3) verification procedure (commented out by default) + Gia_ManNameMapVerify() which checks that the resulting mapping computed by Gia_ManMapMiniLut2MiniAig() is correct. Please + let me know if this computation is clear. +*/ + +Vec_Int_t * Gia_ManVerifyFindNameMapping( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2 ) +{ + Vec_Int_t * vRes = Vec_IntStartFull(Vec_IntSize(vMap2)); + Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); + int i, Entry, iRepr, fCompl, iLit; + Gia_Obj_t * pObj; + Gia_ManSetPhase( p1 ); + Gia_ManSetPhase( p2 ); + Vec_IntForEachEntry( vMap1, Entry, i ) + { + if ( Entry == -1 ) + continue; + pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) ); + if ( ~pObj->Value == 0 ) + continue; + fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase; + iRepr = Gia_ObjReprSelf( p, Abc_Lit2Var(pObj->Value) ); + Vec_IntWriteEntry( vMap, iRepr, Abc_Var2Lit( i, fCompl ) ); + } + Vec_IntForEachEntry( vMap2, Entry, i ) + { + if ( Entry == -1 ) + continue; + pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) ); + if ( ~pObj->Value == 0 ) + continue; + fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase; + iRepr = Gia_ObjReprSelf( p, Abc_Lit2Var(pObj->Value) ); + if ( (iLit = Vec_IntEntry(vMap, iRepr)) == -1 ) + continue; + Vec_IntWriteEntry( vRes, i, Abc_LitNotCond( iLit, fCompl ) ); + } + Vec_IntFill( vMap, Gia_ManCoNum(p1), -1 ); + Vec_IntForEachEntry( vMap1, Entry, i ) + { + if ( Entry == -1 ) + continue; + pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) ); + if ( !Gia_ObjIsCo(pObj) ) + continue; + Vec_IntWriteEntry( vMap, Gia_ObjCioId(pObj), i ); + } + Vec_IntForEachEntry( vMap2, Entry, i ) + { + if ( Entry == -1 ) + continue; + pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) ); + if ( !Gia_ObjIsCo(pObj) ) + continue; + + assert( Vec_IntEntry(vRes, i) == -1 ); + Vec_IntWriteEntry( vRes, i, Abc_Var2Lit( Vec_IntEntry(vMap, Gia_ObjCioId(pObj)), 0 ) ); + assert( Vec_IntEntry(vRes, i) != -1 ); + } + Vec_IntFree( vMap ); + return vRes; +} + +void Gia_ManVerifyVerifyNameMapping( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2, Vec_Int_t * vMapRes ) +{ + int iImpl, iReprSpec, iReprImpl, nSize = Vec_IntSize(vMap2); + Gia_Obj_t * pObjSpec, * pObjImpl; + if ( vMapRes == NULL || p == NULL || p->pReprs == NULL ) + return; + assert( Vec_IntSize(vMapRes) == nSize ); + Gia_ManSetPhase( p1 ); + Gia_ManSetPhase( p2 ); + for ( iImpl = 0; iImpl < nSize; iImpl++ ) + if ( Vec_IntEntry(vMapRes, iImpl) >= 0 ) + { + int Entry = Vec_IntEntry( vMapRes, iImpl ); + int iSpec = Abc_Lit2Var( Entry ); + int fCompl = Abc_LitIsCompl( Entry ); + int iLitSpec = Vec_IntEntry( vMap1, iSpec ); + int iLitImpl = Vec_IntEntry( vMap2, iImpl ); + pObjSpec = Gia_ManObj( p1, Abc_Lit2Var(iLitSpec) ); + if ( Gia_ObjIsCo(pObjSpec) ) + continue; + if ( ~pObjSpec->Value == 0 ) + continue; + pObjImpl = Gia_ManObj( p2, Abc_Lit2Var(iLitImpl) ); + if ( ~pObjImpl->Value == 0 ) + continue; + iReprSpec = Gia_ObjReprSelf( p, Abc_Lit2Var(pObjSpec->Value) ); + iReprImpl = Gia_ObjReprSelf( p, Abc_Lit2Var(pObjImpl->Value) ); + if ( iReprSpec != iReprImpl ) + printf( "Found functional mismatch for ImplId %d and SpecId %d.\n", iImpl, iSpec ); + if ( (pObjImpl->fPhase ^ Abc_LitIsCompl(iLitImpl)) != (pObjSpec->fPhase ^ Abc_LitIsCompl(iLitSpec) ^ fCompl) ) + printf( "Found phase mismatch for ImplId %d and SpecId %d.\n", iImpl, iSpec ); + } +} + +int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fObjIdMap, int fDumpFiles, int fVerbose, char * pFileSpec ) { int Status = -1; Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter; @@ -1052,12 +1159,30 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS { Cec_ParCec_t ParsCec, * pPars = &ParsCec; Cec_ManCecSetDefaultParams( pPars ); - pPars->nBTLimit = nBTLimit; - pPars->TimeLimit = nTimeLim; - pPars->fVerbose = fVerbose; + pPars->nBTLimit = nBTLimit; + pPars->TimeLimit = nTimeLim; + pPars->fUseOrigIds = fObjIdMap; + pPars->fVerbose = fVerbose; Status = Cec_ManVerify( pMiter, pPars ); if ( pPars->iOutFail >= 0 ) Abc_Print( 1, "Verification failed for at least one output (%d).\n", pPars->iOutFail ); + if ( fObjIdMap ) { + Gia_Man_t * pReduced = Gia_ManOrigIdsReduce( pMiter, pMiter->vIdsEquiv ); + Gia_ManStop( pReduced ); + Gia_Obj_t * pObj; int i; + Vec_Int_t * vCopy0 = Vec_IntAlloc(Gia_ManObjNum(pSpec)); + Gia_ManForEachObj( pSpec, pObj, i ) + Vec_IntPush( vCopy0, pObj->Value ); + Vec_Int_t * vCopy1 = Vec_IntAlloc(Gia_ManObjNum(pGia)); + Gia_ManForEachObj( pGia, pObj, i ) + Vec_IntPush( vCopy1, pObj->Value ); + Vec_IntFreeP( &pGia->vEquLitIds ); + pGia->vEquLitIds = Gia_ManVerifyFindNameMapping( pMiter, pGia0, pGia1, vCopy0, vCopy1 ); + assert( Vec_IntSize(pGia->vEquLitIds) == Gia_ManObjNum(pGia) ); + Gia_ManVerifyVerifyNameMapping( pMiter, pGia0, pGia1, vCopy0, vCopy1, pGia->vEquLitIds ); + Vec_IntFree( vCopy0 ); + Vec_IntFree( vCopy1 ); + } Gia_ManStop( pMiter ); } } @@ -1094,4 +1219,3 @@ Vec_Int_t * Gia_ManDeriveBoxMapping( Gia_Man_t * pGia ) ABC_NAMESPACE_IMPL_END - diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9ce0dc107..fd1c2c8b2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -42227,9 +42227,9 @@ usage: int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv ) { char * pFileSpec = NULL; - int c, nBTLimit = 1000, nTimeLim = 0, fSeq = 0, fDumpFiles = 0, fVerbose = 0; + int c, nBTLimit = 1000, nTimeLim = 0, fSeq = 0, fObjIdMap = 0, fDumpFiles = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CTsdvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CTsmdvh" ) ) != EOF ) { switch ( c ) { @@ -42258,6 +42258,9 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': fSeq ^= 1; break; + case 'm': + fObjIdMap ^= 1; + break; case 'd': fDumpFiles ^= 1; break; @@ -42276,15 +42279,16 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv ) Extra_FileNameCorrectPath( pFileSpec ); printf( "Taking spec from file \"%s\".\n", pFileSpec ); } - Gia_ManVerifyWithBoxes( pAbc->pGia, nBTLimit, nTimeLim, fSeq, fDumpFiles, fVerbose, pFileSpec ); + Gia_ManVerifyWithBoxes( pAbc->pGia, nBTLimit, nTimeLim, fSeq, fObjIdMap, fDumpFiles, fVerbose, pFileSpec ); return 0; usage: - Abc_Print( -2, "usage: &verify [-CT num] [-sdvh] \n" ); + Abc_Print( -2, "usage: &verify [-CT num] [-smdvh] \n" ); Abc_Print( -2, "\t performs verification of combinational design\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nTimeLim ); Abc_Print( -2, "\t-s : toggle using sequential verification [default = %s]\n", fSeq? "yes":"no"); + Abc_Print( -2, "\t-m : toggle producing object ID mapping (CEC only) [default = %s]\n", fObjIdMap? "yes":"no"); Abc_Print( -2, "\t-d : toggle dumping AIGs to be compared [default = %s]\n", fDumpFiles? "yes":"no"); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes":"no"); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index ca7eed5a7..a3fb06376 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -135,6 +135,7 @@ struct Cec_ParCec_t_ int fUseSmartCnf; // use smart CNF computation int fRewriting; // enables AIG rewriting int fNaive; // performs naive SAT-based checking + int fUseOrigIds; // enable recording of original IDs int fSilent; // print no messages int fVeryVerbose; // verbose stats int fVerbose; // verbose stats diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index f6a1ab527..e52258b9d 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -359,11 +359,13 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) pParsFra->nItersMax = 1000; pParsFra->nBTLimit = pPars->nBTLimit; pParsFra->TimeLimit = pPars->TimeLimit; + pParsFra->fUseOrigIds = pPars->fUseOrigIds; pParsFra->fVerbose = pPars->fVerbose; pParsFra->fVeryVerbose = pPars->fVeryVerbose; pParsFra->fCheckMiter = 1; pParsFra->fDualOut = 1; pNew = Cec_ManSatSweeping( p, pParsFra, pPars->fSilent ); + ABC_SWAP( Vec_Int_t *, pInit->vIdsEquiv, p->vIdsEquiv ); pPars->iOutFail = pParsFra->iOutFail; // update pInit->pCexComb = p->pCexComb; p->pCexComb = NULL; @@ -383,6 +385,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) } return 0; } + Vec_IntFreeP( &pInit->vIdsEquiv ); p = Gia_ManDup( pInit ); Gia_ManEquivFixOutputPairs( p ); p = Gia_ManCleanup( pNew = p );