Deriving cell mapping with &if -kz.

9 files changed, 217 insertions, 38 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 1dda7dc0..28d65b35 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -135,7 +135,7 @@ struct Gia_Man_t_
     Abc_Cex_t *    pCexComb;      // combinational counter-example
     Abc_Cex_t *    pCexSeq;       // sequential counter-example
     Vec_Ptr_t *    vSeqModelVec;  // sequential counter-examples
-    int *          pCopies;       // intermediate copies
+    Vec_Int_t      vCopies;       // intermediate copies
     Vec_Int_t *    vTruths;       // used for truth table computation
     Vec_Int_t *    vFlopClasses;  // classes of flops for retiming/merging/etc
     Vec_Int_t *    vGateClasses;  // classes of gates for abstraction
@@ -465,11 +465,15 @@ static inline int          Gia_ObjFanin0Copy( Gia_Obj_t * pObj )               {
 static inline int          Gia_ObjFanin1Copy( Gia_Obj_t * pObj )               { return Abc_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );     }
 static inline int          Gia_ObjFanin2Copy( Gia_Man_t * p, Gia_Obj_t * pObj ){ return Abc_LitNotCond(Gia_ObjFanin2(p, pObj)->Value, Gia_ObjFaninC2(p, pObj)); }
 
-static inline int          Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )               { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)];  }
-static inline void         Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit )  { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit;  }
+static inline int          Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )               { return Vec_IntEntry(&p->vCopies, Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj));      }
+static inline void         Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit )  { Vec_IntWriteEntry(&p->vCopies, Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj), iLit);  }
+static inline int          Gia_ObjCopyArray( Gia_Man_t * p, int iObj )                          { return Vec_IntEntry(&p->vCopies, iObj);                                          }
+static inline void         Gia_ObjSetCopyArray( Gia_Man_t * p, int iObj, int iLit )             { Vec_IntWriteEntry(&p->vCopies, iObj, iLit);                                      }
 
-static inline int          Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj));  }
-static inline int          Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj));  }
+static inline int          Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj));   }
+static inline int          Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj));   }
+static inline int          Gia_ObjFanin0CopyArray( Gia_Man_t * p, Gia_Obj_t * pObj )            { return Abc_LitNotCond(Gia_ObjCopyArray(p, Gia_ObjFaninId0p(p,pObj)), Gia_ObjFaninC0(pObj));  }
+static inline int          Gia_ObjFanin1CopyArray( Gia_Man_t * p, Gia_Obj_t * pObj )            { return Abc_LitNotCond(Gia_ObjCopyArray(p, Gia_ObjFaninId1p(p,pObj)), Gia_ObjFaninC1(pObj));  }
 
 static inline Gia_Obj_t *  Gia_ObjFromLit( Gia_Man_t * p, int iLit )           { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) );  }
 static inline int          Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); }
diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c
index 9cb0dce5..03d1a390 100644
--- a/src/aig/gia/giaEnable.c
+++ b/src/aig/gia/giaEnable.c
@@ -362,8 +362,7 @@ Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames )
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj, * pObjRi, * pObjRo;
     int f, i;
-    ABC_FREE( p->pCopies );
-    p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
+    Vec_IntFill( &p->vCopies, -1, nFrames * Gia_ManObjNum(p) );
     pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
@@ -413,7 +412,7 @@ Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, i
     vCofSigs = Gia_ManTransferFrames( p, pFrames, nFrames, pAig, vTemp = vCofSigs );
     Vec_IntFree( vTemp );
     Gia_ManStop( pFrames );
-    ABC_FREE( p->pCopies );
+    ABC_FREE( p->vCopies.pArray );
     // cofactor all these variables
     pNew = Gia_ManDupCofAllInt( pAig, vCofSigs, fVerbose );
     Vec_IntFree( vCofSigs );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index c5dba25b..61290da2 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1017,7 +1017,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames
     }
 */
     assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 );
-    p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
+    Vec_IntFill( &p->vCopies, -1, nFrames * Gia_ManObjNum(p) );
     vXorLits = Vec_IntAlloc( 1000 );
     Gia_ManSetPhase( p );
     if ( fDualOut )
@@ -1052,7 +1052,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames
 //        Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" );
         Gia_ManAppendCo( pNew, 0 );
     }
-    ABC_FREE( p->pCopies );
+    ABC_FREE( p->vCopies.pArray );
     Vec_IntFree( vXorLits );
     Gia_ManHashStop( pNew );
     pNew = Gia_ManCleanup( pTemp = pNew );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 1c4ae9c0..a5eafb5f 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -1425,9 +1425,51 @@ int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * p
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * pCutBest, sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, void * pNtkCell, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking )
+int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t * pTemp, If_Cut_t * pCutBest, sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, Ifn_Ntk_t * pNtkCell, int nLutMax, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking )
 {
-    return 0;
+    int iLit;
+    if ( Vec_IntSize(vLeaves) <= nLutMax )
+        iLit = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 );
+    else
+    {
+        Gia_Obj_t * pObj;
+        int i, Id;
+        // extract variable permutation
+        word Perm = If_DsdManGetFuncPerm( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest) );
+        assert( Perm > 0 );
+        // perform boolean matching
+        if ( !If_ManSatFindCofigBits( pSat, vPiVars, vPoVars, If_CutTruthW(pIfMan, pCutBest), Vec_IntSize(vLeaves), Perm, Ifn_NtkInputNum(pNtkCell), vLits ) )
+        {
+            printf( "Boolean matching does not exist.\n" );
+            return -1;
+        }
+        // use config bits to generate the network
+        iLit = If_ManSatDeriveGiaFromBits( pTemp, pNtkCell, vLits, vCover );
+        // copy GIA back into the manager
+        Vec_IntFillExtra( &pTemp->vCopies, Gia_ManObjNum(pTemp), -1 );
+        Gia_ObjSetCopyArray( pTemp, 0, 0 );
+        Gia_ManForEachCiId( pTemp, Id, i )
+            Gia_ObjSetCopyArray( pTemp, Id, Vec_IntEntry(vLeaves, i) );
+        // collect nodes
+        Gia_ManIncrementTravId( pTemp );
+        Id = Abc_Lit2Var( iLit );
+        Gia_ManCollectAnds( pTemp, &Id, 1, vCover );
+        // copy GIA
+        Gia_ManForEachObjVec( vCover, pTemp, pObj, i )
+        {
+            iLit = Gia_ManAppendAnd( pNew, Gia_ObjFanin0CopyArray(pTemp, pObj), Gia_ObjFanin1CopyArray(pTemp, pObj) );
+            Gia_ObjSetCopyArray( pTemp, Gia_ObjId(pTemp, pObj), iLit );
+        }
+        iLit = Abc_LitNotCond( Gia_ObjCopyArray(pTemp, Id), Abc_LitIsCompl(iLit) );
+    }
+    // write packing
+    if ( !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(iLit))) && iLit > 1 )
+    {
+        Vec_IntPush( vPacking, 1 );
+        Vec_IntPush( vPacking, Abc_Lit2Var(iLit) );
+        Vec_IntAddToEntry( vPacking, 0, 1 );
+    }
+    return iLit;
 }
 
 /**Function*************************************************************
@@ -1443,15 +1485,15 @@ int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t *
 ***********************************************************************/
 Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
 {
-    Gia_Man_t * pNew;
+    Gia_Man_t * pNew, * pHashed = NULL;
     If_Cut_t * pCutBest;
     If_Obj_t * pIfObj, * pIfLeaf;
     Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL;
     Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits;
     Vec_Int_t * vPiVars = NULL, * vPoVars = NULL;
     sat_solver * pSat = NULL;
-    void * pNtkCell = NULL;
-    int i, k, Entry;
+    Ifn_Ntk_t * pNtkCell = NULL;
+    int i, k, nLutMax, Entry;
     assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth );
 //    if ( pIfMan->pPars->fEnableCheck07 )
 //        pIfMan->pPars->fDeriveLuts = 0;
@@ -1499,8 +1541,16 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
             else if ( pIfMan->pPars->fUseDsd && pIfMan->pPars->fUseDsdTune && pIfMan->pPars->fDeriveLuts )
             {
                 if ( pSat == NULL )
-                    pSat = (sat_solver *)If_ManSatBuildFromCell( NULL, &vPiVars, &vPoVars, (void **)&pNtkCell );
-                pIfObj->iCopy = Gia_ManFromIfLogicFindCell( pIfMan, pNew, pCutBest, pSat, vPiVars, vPoVars, pNtkCell, vLeaves, vLits, vCover, vMapping, vMapping2, vPacking );
+                {
+                    pSat = (sat_solver *)If_ManSatBuildFromCell( If_DsdManGetCellStr(pIfMan->pIfDsdMan), &vPiVars, &vPoVars, &pNtkCell );
+                    nLutMax = Ifn_NtkLutSizeMax( pNtkCell );
+                    pHashed = Gia_ManStart( 10000 );
+                    Vec_IntFillExtra( &pHashed->vCopies, 10000, -1 );
+                    for ( k = 0; k < pIfMan->pPars->nLutSize; k++ )
+                        Gia_ManAppendCi( pHashed );
+                    Gia_ManHashAlloc( pHashed );
+                }
+                pIfObj->iCopy = Gia_ManFromIfLogicFindCell( pIfMan, pNew, pHashed, pCutBest, pSat, vPiVars, vPoVars, pNtkCell, nLutMax, vLeaves, vLits, vCover, vMapping, vMapping2, vPacking );
                 pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
             }
             else if ( (pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth) || pIfMan->pPars->fUseDsd || pIfMan->pPars->fUseTtPerm )
@@ -1549,8 +1599,10 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
     Vec_IntFreeP( &vPoVars );
     if ( pNtkCell )
         ABC_FREE( pNtkCell );
-    if ( pSat != NULL )
+    if ( pSat )
         sat_solver_delete(pSat);
+    if ( pHashed )
+        Gia_ManStop( pHashed );
 //    printf( "Mapping array size:  IfMan = %d. Gia = %d. Increase = %.2f\n", 
 //        If_ManObjNum(pIfMan), Gia_ManObjNum(pNew), 1.0 * Gia_ManObjNum(pNew) / If_ManObjNum(pIfMan) );
     // finish mapping 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c1865128..57263ed4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -16139,7 +16139,15 @@ int Abc_CommandDsdMatch( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     if ( pStruct )
+    {
+        char * pStructCur = If_DsdManGetCellStr( pDsdMan );
+        if ( pStructCur && strcmp(pStructCur, pStruct) )
+        {
+            Abc_Print( -1, "DSD manager matched with cell %s needs to be cleaned before matching with cell %s.\n", pStructCur, pStruct );
+            return 0;
+        }
         Id_DsdManTuneStr( pDsdMan, pStruct, nConfls, nProcs, fVerbose );
+    }
     else
         If_DsdManTune( pDsdMan, LutSize, fFast, fAdd, fSpec, fVerbose );
     return 0;
@@ -31414,6 +31422,11 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( -1, "LUT size (%d) is more than the number of variables in the DSD manager (%d).\n", pPars->nLutSize, If_DsdManVarNum(pDsdMan) );
             return 1;
         }
+        if ( pPars->fDeriveLuts && If_DsdManGetCellStr(pDsdMan) == NULL )
+        {
+            Abc_Print( -1, "DSD manager is not matched with any particular cell.\n" );
+            return 1;
+        }
         pPars->fCutMin = 1;
         pPars->fUseDsd = 1;
         If_DsdManSetNewAsUseless( pDsdMan );
@@ -31454,7 +31467,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         pPars->fTruth = 1;
         pPars->fExpRed = 0;
-        if ( pPars->pLutStruct == NULL )
+        if ( pPars->pLutStruct == NULL && !pPars->fUseDsdTune )
             pPars->fDeriveLuts = 1;
     }
     // modify the subgraph recording
diff --git a/src/map/if/if.h b/src/map/if/if.h
index a94a5fe8..909a54ce 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -81,6 +81,7 @@ typedef struct If_Set_t_     If_Set_t;
 typedef struct If_LibLut_t_  If_LibLut_t;
 typedef struct If_LibBox_t_  If_LibBox_t;
 typedef struct If_DsdMan_t_  If_DsdMan_t;
+typedef struct Ifn_Ntk_t_    Ifn_Ntk_t;
 
 typedef struct Ifif_Par_t_   Ifif_Par_t;
 struct Ifif_Par_t_
@@ -560,6 +561,8 @@ extern int             If_DsdManSuppSize( If_DsdMan_t * p, int iDsd );
 extern int             If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
 extern int             If_DsdManReadMark( If_DsdMan_t * p, int iDsd );
 extern void            If_DsdManSetNewAsUseless( If_DsdMan_t * p );
+extern word            If_DsdManGetFuncPerm( If_DsdMan_t * p, int iDsd );
+extern char *          If_DsdManGetCellStr( If_DsdMan_t * p );
 extern unsigned        If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose );
 extern int             If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig );
 extern int             If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm );
@@ -624,7 +627,14 @@ extern void            If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
 extern int             If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
 extern int             If_CutComputeTruthPerm( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
 /*=== ifTune.c ===========================================================*/
-extern void *          If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, void ** ppNtk );
+extern Ifn_Ntk_t *     Ifn_NtkParse( char * pStr );
+extern int             Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pPerm );
+extern void            Ifn_NtkPrint( Ifn_Ntk_t * p );
+extern int             Ifn_NtkLutSizeMax( Ifn_Ntk_t * p );
+extern int             Ifn_NtkInputNum( Ifn_Ntk_t * p );
+extern void *          If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, Ifn_Ntk_t ** ppNtk );
+extern int             If_ManSatFindCofigBits( void * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues );
+extern int             If_ManSatDeriveGiaFromBits( void * pNew, Ifn_Ntk_t * p, Vec_Int_t * vLeaves, Vec_Int_t * vValues );
 /*=== ifUtil.c ============================================================*/
 extern void            If_ManCleanNodeCopy( If_Man_t * p );
 extern void            If_ManCleanCutData( If_Man_t * p );
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index c4cd2a3c..c71df9e7 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -90,6 +90,7 @@ struct If_DsdMan_t_
     Gia_Man_t *    pTtGia;         // GIA to represent truth tables
     Vec_Int_t *    vCover;         // temporary memory
     void *         pSat;           // SAT solver
+    char *         pCellStr;       // symbolic cell description
     int            nObjsPrev;      // previous number of objects
     int            fNewAsUseless;  // set new as useless
     int            nUniqueHits;    // statistics
@@ -195,6 +196,14 @@ void If_DsdManSetNewAsUseless( If_DsdMan_t * p )
         p->nObjsPrev = If_DsdManObjNum(p);
     p->fNewAsUseless = 1;
 }
+word If_DsdManGetFuncPerm( If_DsdMan_t * p, int iDsd )
+{
+    return p->vPerms ? Vec_WrdEntry(p->vPerms, Abc_Lit2Var(iDsd)) : 0;
+}
+char * If_DsdManGetCellStr( If_DsdMan_t * p )
+{
+    return p->pCellStr;
+}
 
 /**Function*************************************************************
 
@@ -339,6 +348,7 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
     Gia_ManStopP( &p->pTtGia );
     Vec_IntFreeP( &p->vCover );
     If_ManSatUnbuild( p->pSat );
+    ABC_FREE( p->pCellStr );
     ABC_FREE( p->pStore );
     ABC_FREE( p->pBins );
     ABC_FREE( p );
@@ -720,6 +730,8 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support,
     If_DsdManPrintDistrib( p );
     printf( "Number of inputs = %d.  LUT size = %d.  Marks = %s.  NewAsUseless = %s.  Bookmark = %d.\n", 
         p->nVars, p->LutSize, If_DsdManHasMarks(p)? "yes" : "no", p->fNewAsUseless? "yes" : "no", p->nObjsPrev );
+    if ( p->pCellStr )
+        printf( "Symbolic cell description: %s\n", p->pCellStr );
     if ( p->pTtGia )
     fprintf( pFile, "Non-DSD AIG nodes          = %8d\n", Gia_ManAndNum(p->pTtGia) );
     fprintf( pFile, "Unique table misses        = %8d\n", p->nUniqueMisses );
@@ -1061,6 +1073,14 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
             fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
         }
     }
+    Num = p->vPerms ? Vec_WrdSize(p->vPerms) : 0;
+    fwrite( &Num, 4, 1, pFile );
+    if ( Num )
+        fwrite( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile );
+    Num = p->pCellStr ? strlen(p->pCellStr) : 0;
+    fwrite( &Num, 4, 1, pFile );
+    if ( Num )
+        fwrite( p->pCellStr, sizeof(char)*Num, 1, pFile );
     fclose( pFile );
 }
 If_DsdMan_t * If_DsdManLoad( char * pFileName )
@@ -1139,6 +1159,18 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
         assert( Num2 == Vec_PtrSize(p->vTtDecs[v]) ); 
     }
     ABC_FREE( pTruth );
+    RetValue = fread( &Num, 4, 1, pFile );
+    if ( Num )
+    {
+        p->vPerms = Vec_WrdStart( Num );
+        RetValue = fread( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile );
+    }
+    RetValue = fread( &Num, 4, 1, pFile );
+    if ( Num )
+    {
+        p->pCellStr = ABC_CALLOC( char, Num + 1 );
+        RetValue = fread( p->pCellStr, sizeof(char)*Num, 1, pFile );
+    }
     fclose( pFile );
     return p;
 }
@@ -1187,6 +1219,7 @@ void If_DsdManCleanMarks( If_DsdMan_t * p, int fVerbose )
 {
     If_DsdObj_t * pObj; 
     int i;
+    ABC_FREE( p->pCellStr );
     If_DsdVecForEachObj( &p->vObjs, pObj, i )
         pObj->fMark = 0;
 }
@@ -2371,13 +2404,6 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec
 }
 
 
-typedef struct Ifn_Ntk_t_  Ifn_Ntk_t;
-
-extern Ifn_Ntk_t * Ifn_NtkParse( char * pStr );
-extern int         Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pPerm );
-extern void        Ifn_NtkPrint( Ifn_Ntk_t * p );
-extern int         Ifn_NtkLutSizeMax( Ifn_Ntk_t * p );
-extern int         Ifn_NtkInputNum( Ifn_Ntk_t * p );
 
 /**Function*************************************************************
 
@@ -2408,6 +2434,8 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
         ABC_FREE( pNtk );
         return;
     }
+    ABC_FREE( p->pCellStr );
+    p->pCellStr = Abc_UtilStrsav( pStruct );
     if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) )
         printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
     LutSize = Ifn_NtkLutSizeMax(pNtk);
@@ -2544,6 +2572,8 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
         ABC_FREE( pNtk );
         return;
     }
+    ABC_FREE( p->pCellStr );
+    p->pCellStr = Abc_UtilStrsav( pStruct );
     if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) )
         printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
     // check the largest LUT
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index 6e48448b..defafcb4 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -58,8 +58,6 @@ static char * Ifn_Symbs[16] = {
 };
 
 typedef struct Ifn_Obj_t_  Ifn_Obj_t;
-typedef struct Ifn_Ntk_t_  Ifn_Ntk_t;
-
 struct Ifn_Obj_t_
 {
     unsigned               Type    :  3;      // node type
@@ -621,9 +619,10 @@ sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t **
     Gia_ManStop( p2 );
     return pSat;
 }
-void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, void ** ppNtk )
+void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, Ifn_Ntk_t ** ppNtk )
 {
     Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
+    Ifn_Prepare( p, NULL, p->nInps );
     *ppNtk = p;
     if ( p == NULL )
         return NULL;
@@ -651,7 +650,7 @@ void Ifn_ManSatPrintPerm( char * pPerms, int nVars )
 }
 int Ifn_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nInps, Vec_Int_t * vLits )
 {
-    int v, Value, m, mNew, nMints = (1 << nVars);
+    int v, Value, m, mNew, nMints = (1 << nVars); // (1 << nInps);
     assert( (1 << nInps) == Vec_IntSize(vPoVars) );
     assert( nVars <= nInps );
     // remap minterms
@@ -685,7 +684,7 @@ void Ifn_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vV
     Vec_IntForEachEntry( vPiVars, iVar, i )
         Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
 }
-int Ifn_ManSatFindCofigBits( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues )
+int If_ManSatFindCofigBits( void * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues )
 {
     // extract permutation
     int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE];
@@ -696,7 +695,7 @@ int Ifn_ManSatFindCofigBits( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t *
         assert( pPerm[i] < nVars );
     }
     // perform SAT check 
-    RetValue = Ifn_ManSatCheckOne( pSat, vPoVars, pTruth, nVars, pPerm, nInps, vValues );
+    RetValue = Ifn_ManSatCheckOne( (sat_solver *)pSat, vPoVars, pTruth, nVars, pPerm, nInps, vValues );
     Vec_IntClear( vValues );
     if ( RetValue == 0 )
         return 0;
@@ -708,7 +707,7 @@ int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word P
     Vec_Int_t * vValues = Vec_IntAlloc( 100 );
     Vec_Int_t * vPiVars, * vPoVars;
     sat_solver * pSat = Ifn_ManSatBuild( p, &vPiVars, &vPoVars );
-    int RetValue = Ifn_ManSatFindCofigBits( pSat, vPiVars, vPoVars, pTruth, nVars, Perm, p->nInps, vValues );
+    int RetValue = If_ManSatFindCofigBits( pSat, vPiVars, vPoVars, pTruth, nVars, Perm, p->nInps, vValues );
     Vec_IntPrint( vValues );
     // cleanup
     sat_solver_delete( pSat );
@@ -718,6 +717,78 @@ int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word P
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derive GIA using programmable bits.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues, Vec_Int_t * vCover )
+{
+    Gia_Man_t * pNew = (Gia_Man_t *)pGia;
+    int i, Id, k, iLit, iVar = 0, nVarsNew, pVarMap[1000];
+    assert( Gia_ManCiNum(pNew) == p->nInps && p->nParsVIni < 1000 );
+    Gia_ManForEachCiId( pNew, Id, i )
+        pVarMap[i] = Abc_Var2Lit( Id, 0 );
+    for ( i = p->nInps; i < p->nObjs; i++ )
+    {
+        int Type = p->Nodes[i].Type;
+        int nFans = p->Nodes[i].nFanins;
+        int * pFans = p->Nodes[i].Fanins;
+        int iFanin = p->Nodes[i].iFirst;
+        assert( nFans <= 6 );
+        if ( Type == IFN_DSD_AND )
+        {
+            iLit = 1;
+            for ( k = 0; k < nFans; k++ )
+                iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] );
+            pVarMap[i] = iLit;
+        }
+        else if ( Type == IFN_DSD_XOR )
+        {
+            iLit = 0;
+            for ( k = 0; k < nFans; k++ )
+                iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] );
+            pVarMap[i] = iLit;
+        }
+        else if ( Type == IFN_DSD_MUX )
+        {
+            assert( nFans == 3 );
+            pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] );
+        }
+        else if ( Type == IFN_DSD_PRIME )
+        {
+            int pFaninLits[16];
+            // collect truth table
+            word uTruth = 0;
+            int nMints = (1 << nFans);
+            for ( k = 0; k < nMints; k++ )
+                if ( Vec_IntEntry( vValues, iVar++ ) )
+                    uTruth |= ((word)1 << k);
+            // collect function
+            for ( k = 0; k < nFans; k++ )
+                pFaninLits[k] = pVarMap[pFans[k]];
+            // implement the function
+            nVarsNew = Abc_TtMinBase( &uTruth, pFaninLits, nFans, 6 );
+            if ( nVarsNew == 0 )
+                pVarMap[i] = (int)(uTruth & 1);
+            else
+            {
+                extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
+                Vec_Int_t Leaves = { nVarsNew, nVarsNew, pFaninLits };
+                pVarMap[i] = Kit_TruthToGia( pNew, (unsigned *)uTruth, nVarsNew, vCover, &Leaves, 1 ); // hashing enabled!!!
+            }
+        }
+        else assert( 0 );
+    }
+    assert( iVar == Vec_IntSize(vValues) );
+    return pVarMap[p->nObjs - 1];
+}
 
 /**Function*************************************************************
 
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index 83345ae5..fd6c6006 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
     assert( nFrames > 0 );
     assert( Gia_ManRegNum(p) > 0 );
     assert( p->pReprs != NULL );
-    p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
+    Vec_IntFill( &p->vCopies, -1, (nFrames+fScorr)*Gia_ManObjNum(p) );
     Gia_ManSetPhase( p );
     pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
@@ -200,7 +200,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
         Gia_ManAppendCo( pNew, iObjNew );
     Vec_IntFree( vXorLits );
     Gia_ManHashStop( pNew );
-    ABC_FREE( p->pCopies );
+    ABC_FREE( p->vCopies.pArray );
 //Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
     pNew = Gia_ManCleanup( pTemp = pNew );
 //Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
@@ -229,7 +229,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix,
     assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
     assert( Gia_ManRegNum(p) > 0 );
     assert( p->pReprs != NULL );
-    p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) );
+    Vec_IntFill( &p->vCopies, -1, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) );
     Gia_ManSetPhase( p );
     pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
@@ -270,7 +270,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix,
         Gia_ManAppendCo( pNew, iObjNew );
     Vec_IntFree( vXorLits );
     Gia_ManHashStop( pNew );
-    ABC_FREE( p->pCopies );
+    ABC_FREE( p->vCopies.pArray );
 //Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
     pNew = Gia_ManCleanup( pTemp = pNew );
 //Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );