Adding extension "y" for obj ID mapping.

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 );

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 <file.aig>\".\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 <file.aig>\".\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 <file.aig>\".\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
-

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 );
 }
 

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->nBTLimit    = nBTLimit;
-            pPars->TimeLimit = nTimeLim;
+            pPars->TimeLimit   = nTimeLim;
-            pPars->fVerbose  = fVerbose;
+            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
-

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] <file>\n" );
+    Abc_Print( -2, "usage: &verify [-CT num] [-smdvh] <file>\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");

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

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 );