Support for representing programmable cell configuration data.

9 files changed, 333 insertions, 100 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index bc7238d8..88e47ed0 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -131,6 +131,8 @@ struct Gia_Man_t_
     Vec_Int_t *    vMapping;      // mapping for each node
     Vec_Int_t *    vCellMapping;  // mapping for each node
     Vec_Int_t *    vPacking;      // packing information
+    Vec_Int_t *    vConfigs;      // cell configurations
+    char *         pCellStr;      // cell description
     Vec_Int_t *    vLutConfigs;   // LUT configurations
     Abc_Cex_t *    pCexComb;      // combinational counter-example
     Abc_Cex_t *    pCexSeq;       // sequential counter-example
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 2c76b7dc..90a97955 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -670,6 +670,21 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
                 assert( pCur == pCurTemp );
                 if ( fVerbose ) printf( "Finished reading extension \"r\".\n" );
             }
+            // read configuration data
+            else if ( *pCur == 'b' )
+            {
+                int nSize;
+                pCur++;
+                nSize = Gia_AigerReadInt(pCur);
+                pCurTemp = pCur + nSize + 4;                            pCur += 4;
+                pNew->pCellStr = Abc_UtilStrsav( pCur );                pCur += strlen(pCur) + 1;
+                nSize = nSize - strlen(pNew->pCellStr) - 1;
+                assert( nSize % 4 == 0 );
+                pNew->vConfigs = Vec_IntStart(nSize / 4);
+                memcpy(Vec_IntArray(pNew->vConfigs), pCur, nSize);      pCur += nSize;
+                assert( pCur == pCurTemp );
+                if ( fVerbose ) printf( "Finished reading extension \"b\".\n" );
+            }
             // read choices
             else if ( *pCur == 'q' )
             {
@@ -1267,6 +1282,15 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         for ( i = 0; i < Vec_IntSize(p->vRegClasses); i++ )
             Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vRegClasses, i) );
     }
+    // write configuration data
+    if ( p->vConfigs )
+    {
+        fprintf( pFile, "b" );
+        assert( p->pCellStr != NULL );
+        Gia_FileWriteBufferSize( pFile, 4*Vec_IntSize(p->vConfigs) + strlen(p->pCellStr) + 1 );
+        fwrite( p->pCellStr, 1, strlen(p->pCellStr) + 1, pFile );
+        fwrite( Vec_IntArray(p->vConfigs), 1, 4*Vec_IntSize(p->vConfigs), pFile );
+    }
     // write choices
     if ( Gia_ManHasChoices(p) )
     {
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 645c45b0..367df593 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -1467,9 +1467,54 @@ 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, 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 )
+void Gia_ManFromIfGetConfig( Vec_Int_t * vConfigs, If_Man_t * pIfMan, If_Cut_t * pCutBest, int fCompl )
+{
+    If_Obj_t * pIfObj;
+    word * pPerm = If_DsdManGetFuncConfig( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest) ); // cell input -> DSD input
+    char * pCutPerm = If_CutDsdPerm( pIfMan, pCutBest ); // DSD input -> cut input
+    word * pArray;  int v, i, Lit, Var;
+    int nVarNum = If_DsdManVarNum(pIfMan->pIfDsdMan);
+    int nTtBitNum = If_DsdManTtBitNum(pIfMan->pIfDsdMan);
+    int nPermBitNum = If_DsdManPermBitNum(pIfMan->pIfDsdMan);
+    int nPermBitOne = nPermBitNum / nVarNum;
+    // prepare storage
+    int nIntNum = Vec_IntEntry( vConfigs, 1 );
+    for ( i = 0; i < nIntNum; i++ )
+        Vec_IntPush( vConfigs, 0 );
+    pArray = (word *)Vec_IntEntryP( vConfigs, Vec_IntSize(vConfigs) - nIntNum );
+    assert( nPermBitNum % nVarNum == 0 );
+    // set truth table bits
+    for ( i = 0; i < nTtBitNum; i++ )
+        if ( Abc_TtGetBit(pPerm + 1, i) )
+            Abc_TtSetBit( pArray, i );
+    // set permutation bits
+    for ( v = 0; v < nVarNum; v++ )
+    {
+        // get DSD variable
+        Var = ((pPerm[0] >> (v * 4)) & 0xF);
+        assert( Var < (int)pCutBest->nLeaves );
+        // get AIG literal
+        Lit = (int)pCutPerm[Var];
+        assert( Abc_Lit2Var(Lit) < (int)pCutBest->nLeaves );
+        // complement if polarity has changed
+        pIfObj = If_ManObj( pIfMan, pCutBest->pLeaves[Abc_Lit2Var(Lit)] );
+        Lit = Abc_LitNotCond( Lit, Abc_LitIsCompl(pIfObj->iCopy) );
+        // create config literal
+        for ( i = 0; i < nPermBitOne; i++ )
+            if ( (Lit >> i) & 1 )
+                Abc_TtSetBit( pArray, nTtBitNum + v * nPermBitOne + i );
+    }
+    // remember complementation
+    assert( nTtBitNum + nPermBitNum < 32 * nIntNum );
+    if ( Abc_LitIsCompl(If_CutDsdLit(pIfMan, pCutBest)) ^ pCutBest->fCompl ^ fCompl )
+        Abc_TtSetBit( pArray, nTtBitNum + nPermBitNum );
+    // update count
+    Vec_IntAddToEntry( vConfigs, 0, 1 );
+}
+int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t * pTemp, If_Cut_t * pCutBest, 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 * vConfigs )
 {
     int iLit;
+    assert( 0 );
     if ( Vec_IntSize(vLeaves) <= nLutMax )
         iLit = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 );
     else
@@ -1478,19 +1523,10 @@ int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t *
         int i, Id, iLitTemp;
         // extract variable permutation
         char * pCutPerm = If_CutDsdPerm( pIfMan, pCutBest ); // DSD input -> cut input
-        word Perm = If_DsdManGetFuncPerm( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest) ); // cell input -> DSD input
-        assert( Perm > 0 );
-        // (extend storage for configuration bits)
-        // derive mapping from cell inputs into cut inputs
-        // retrieve config bits of the LUTs
-        // 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;
-        }
+        word * pPerm = If_DsdManGetFuncConfig( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest) ); // cell input -> DSD input
+        int nBits = If_DsdManTtBitNum( pIfMan->pIfDsdMan );
         // use config bits to generate the network
-        iLit = If_ManSatDeriveGiaFromBits( pTemp, pNtkCell, vLits, vCover );
+        iLit = If_ManSatDeriveGiaFromBits( pTemp, pNtkCell, pPerm + 1, vLeaves, vCover );
         // copy GIA back into the manager
         Vec_IntFillExtra( &pTemp->vCopies, Gia_ManObjNum(pTemp), -1 );
         Gia_ObjSetCopyArray( pTemp, 0, 0 );
@@ -1512,15 +1548,12 @@ int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t *
         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 );
-    }
+//    if ( vConfigs && !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(iLit))) && iLit > 1 )
+//        Gia_ManFromIfGetConfig( vConfigs, pIfMan, pCutBest );
     return iLit;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Converts IF into GIA manager.]
@@ -1669,23 +1702,31 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
     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 * vMapping, * vMapping2, * vPacking = NULL, * vConfigs = NULL;
     Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits;
-    Vec_Int_t * vPiVars = NULL, * vPoVars = NULL;
-    sat_solver * pSat = NULL;
     Ifn_Ntk_t * pNtkCell = NULL;
-    int i, k, nLutMax = -1, Entry;
+    sat_solver * pSat = NULL;
+    int i, k, Entry, nLutMax = -1; int Count = 0;
     assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth );
 //    if ( pIfMan->pPars->fEnableCheck07 )
 //        pIfMan->pPars->fDeriveLuts = 0;
     // start mapping and packing
     vMapping  = Vec_IntStart( If_ManObjNum(pIfMan) );
     vMapping2 = Vec_IntStart( 1 );
-    if ( pIfMan->pPars->fDeriveLuts && (pIfMan->pPars->pLutStruct || pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u || pIfMan->pPars->fEnableCheck07 || pIfMan->pPars->fUseDsdTune) )
+    if ( pIfMan->pPars->fDeriveLuts && (pIfMan->pPars->pLutStruct || pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u || pIfMan->pPars->fEnableCheck07) )
     {
         vPacking = Vec_IntAlloc( 1000 );
         Vec_IntPush( vPacking, 0 );
     }
+    if ( pIfMan->pPars->fUseDsdTune )
+    {
+        int nTtBitNum = If_DsdManTtBitNum(pIfMan->pIfDsdMan);
+        int nPermBitNum = If_DsdManPermBitNum(pIfMan->pIfDsdMan);
+        int nConfigInts = Abc_BitWordNum(nTtBitNum + nPermBitNum + 1);
+        vConfigs = Vec_IntAlloc( 1000 );
+        Vec_IntPush( vConfigs, 0 );
+        Vec_IntPush( vConfigs, nConfigInts );
+    }
     // create new manager
     pNew = Gia_ManStart( If_ManObjNum(pIfMan) );
     // iterate through nodes used in the mapping
@@ -1722,11 +1763,13 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
                     pIfObj->iCopy = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 );
                 pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
             }
+/*
             else if ( pIfMan->pPars->fUseDsd && pIfMan->pPars->fUseDsdTune && pIfMan->pPars->fDeriveLuts )
             {
-                if ( pSat == NULL )
+                if ( pNtkCell == NULL )
                 {
-                    pSat = (sat_solver *)If_ManSatBuildFromCell( If_DsdManGetCellStr(pIfMan->pIfDsdMan), &vPiVars, &vPoVars, &pNtkCell );
+                    assert( If_DsdManGetCellStr(pIfMan->pIfDsdMan) != NULL );
+                    pNtkCell = Ifn_NtkParse( If_DsdManGetCellStr(pIfMan->pIfDsdMan) );
                     nLutMax = Ifn_NtkLutSizeMax( pNtkCell );
                     pHashed = Gia_ManStart( 10000 );
                     Vec_IntFillExtra( &pHashed->vCopies, 10000, -1 );
@@ -1734,9 +1777,10 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
                         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 = Gia_ManFromIfLogicFindCell( pIfMan, pNew, pHashed, pCutBest, pNtkCell, nLutMax, vLeaves, vLits, vCover, vMapping, vMapping2, vConfigs );
                 pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
             }
+*/
             else if ( pIfMan->pPars->fUseAndVars && pIfMan->pPars->fUseCofVars && pIfMan->pPars->fDeriveLuts && (int)pCutBest->nLeaves > pIfMan->pPars->nLutSize/2 )
             {
                 int truthId = Abc_Lit2Var(pCutBest->iCutFunc);
@@ -1764,6 +1808,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
                 // perform decomposition of the cut
                 pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, pTruth, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u), pIfMan->pPars->fEnableCheck07 );
                 pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
+                if ( vConfigs && Vec_IntSize(vLeaves) > 1 && !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(pIfObj->iCopy))) && pIfObj->iCopy > 1 )
+                    Gia_ManFromIfGetConfig( vConfigs, pIfMan, pCutBest, Abc_LitIsCompl(pIfObj->iCopy) );
             }
             else
             {
@@ -1796,8 +1842,6 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
     Vec_IntFree( vCover );
     Vec_IntFree( vLeaves );
     Vec_IntFree( vLeaves2 );
-    Vec_IntFreeP( &vPiVars );
-    Vec_IntFreeP( &vPoVars );
     if ( pNtkCell )
         ABC_FREE( pNtkCell );
     if ( pSat )
@@ -1820,8 +1864,13 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
     // attach mapping and packing
     assert( pNew->vMapping == NULL );
     assert( pNew->vPacking == NULL );
+    assert( pNew->vConfigs == NULL );
+    assert( pNew->pCellStr == NULL );
     pNew->vMapping = vMapping;
     pNew->vPacking = vPacking;
+    pNew->vConfigs = vConfigs;
+    pNew->pCellStr = vConfigs ? Abc_UtilStrsav( If_DsdManGetCellStr(pIfMan->pIfDsdMan) ) : NULL;
+    assert( !vConfigs || Vec_IntSize(vConfigs) == 2 + Vec_IntEntry(vConfigs, 0) * Vec_IntEntry(vConfigs, 1) );
     // verify that COs have mapping
     {
         Gia_Obj_t * pObj;
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index bd364456..c4da925e 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -114,6 +114,8 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vMapping );
     Vec_IntFreeP( &p->vCellMapping );
     Vec_IntFreeP( &p->vPacking );
+    Vec_IntFreeP( &p->vConfigs );
+    ABC_FREE( p->pCellStr );
     Vec_FltFreeP( &p->vInArrs );
     Vec_FltFreeP( &p->vOutReqs );
     Gia_ManStopP( &p->pAigExtra );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f1c19bd8..e28e5e7d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26745,12 +26745,10 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Strash(): There is no AIG.\n" );
         return 1;
     }
-    if ( Gia_ManHasMapping(pAbc->pGia) )
-    {
-        pTemp = (Gia_Man_t *)Dsm_ManDeriveGia( pAbc->pGia, fAddMuxes );
-//        if ( !Abc_FrameReadFlag("silentmode") )
-//            printf( "Performed delay-oriented unmapping.\n" );
-    }
+    if ( Gia_ManHasMapping(pAbc->pGia) && pAbc->pGia->vConfigs )
+        pTemp = (Gia_Man_t *)If_ManDeriveGiaFromCells( pAbc->pGia );
+    else if ( Gia_ManHasMapping(pAbc->pGia) )
+        pTemp = (Gia_Man_t *)Dsm_ManDeriveGia( pAbc->pGia, fAddMuxes ); // delay-oriented unmapping
     else if ( fAddMuxes )
     {
         if ( pAbc->pGia->pMuxes )
diff --git a/src/base/wlc/wlcStdin.c b/src/base/wlc/wlcStdin.c
index 353cbb3e..d0249d1e 100644
--- a/src/base/wlc/wlcStdin.c
+++ b/src/base/wlc/wlcStdin.c
@@ -110,7 +110,7 @@ Vec_Str_t * Wlc_ConvertToRadix( unsigned * pBits, int Start, int nBits, int Radi
 void Wlc_NtkReport( Wlc_Ntk_t * p, Abc_Cex_t * pCex, char * pName, int Radix )
 {
     Vec_Str_t * vNum;
-    int i, NameId, Name, Start, nBits = -1;
+    int i, NameId, Name, Start = -1, nBits = -1;
     assert( pCex->nRegs == 0 );
     // get the name ID
     NameId = Abc_NamStrFind( p->pManName, pName );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 6a47a52b..067ce0ad 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -559,12 +559,14 @@ extern char *          If_DsdManFileName( If_DsdMan_t * p );
 extern int             If_DsdManVarNum( If_DsdMan_t * p );
 extern int             If_DsdManObjNum( If_DsdMan_t * p );
 extern int             If_DsdManLutSize( If_DsdMan_t * p );
+extern int             If_DsdManTtBitNum( If_DsdMan_t * p );
+extern int             If_DsdManPermBitNum( If_DsdMan_t * p );
 extern void            If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize );
 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 word *          If_DsdManGetFuncConfig( 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 );
@@ -631,13 +633,15 @@ extern int             If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut
 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 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 int             Ifn_NtkTtBits( char * pStr );
+extern int             Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pConfig );
 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 );
+extern int             If_ManSatDeriveGiaFromBits( void * pNew, Ifn_Ntk_t * p, word * pTtData, Vec_Int_t * vLeaves, Vec_Int_t * vValues );
+extern void *          If_ManDeriveGiaFromCells( void * p );
 /*=== 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 9b09ce95..cdc34b2a 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -44,6 +44,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define DSD_VERSION "dsd1"
+
 // network types
 typedef enum { 
     IF_DSD_NONE = 0,               // 0:  unknown
@@ -86,7 +88,9 @@ struct If_DsdMan_t_
     Vec_Ptr_t *    vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions
     Vec_Wec_t *    vIsops[IF_MAX_FUNC_LUTSIZE+1];  // ISOP for each function
     int *          pSched[IF_MAX_FUNC_LUTSIZE];    // grey code schedules
-    Vec_Wrd_t *    vPerms;         // permutations
+    int            nTtBits;        // the number of truth table bits
+    int            nConfigWords;   // the number of words for config data per node
+    Vec_Wrd_t *    vConfigs;       // permutations
     Gia_Man_t *    pTtGia;         // GIA to represent truth tables
     Vec_Int_t *    vCover;         // temporary memory
     void *         pSat;           // SAT solver
@@ -174,6 +178,14 @@ int If_DsdManLutSize( If_DsdMan_t * p )
 {
     return p->LutSize;
 }
+int If_DsdManTtBitNum( If_DsdMan_t * p )
+{
+    return p->nTtBits;
+}
+int If_DsdManPermBitNum( If_DsdMan_t * p )
+{
+    return (Abc_Base2Log(p->nVars + 1) + 1) * p->nVars;
+}
 void If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize )
 {
     p->LutSize = nLutSize;
@@ -196,9 +208,9 @@ void If_DsdManSetNewAsUseless( If_DsdMan_t * p )
         p->nObjsPrev = If_DsdManObjNum(p);
     p->fNewAsUseless = 1;
 }
-word If_DsdManGetFuncPerm( If_DsdMan_t * p, int iDsd )
+word * If_DsdManGetFuncConfig( If_DsdMan_t * p, int iDsd )
 {
-    return p->vPerms ? Vec_WrdEntry(p->vPerms, Abc_Lit2Var(iDsd)) : 0;
+    return p->vConfigs ? Vec_WrdEntryP(p->vConfigs, p->nConfigWords * Abc_Lit2Var(iDsd)) : NULL;
 }
 char * If_DsdManGetCellStr( If_DsdMan_t * p )
 {
@@ -259,6 +271,7 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
     p->nBins   = Abc_PrimeCudd( 100000 );
     p->pBins   = ABC_CALLOC( unsigned, p->nBins );
     p->pMem    = Mem_FlexStart();
+    p->nConfigWords = 1;
     Vec_PtrGrow( &p->vObjs, 10000 );
     Vec_IntGrow( &p->vNexts, 10000 );
     Vec_IntGrow( &p->vTruths, 10000 );
@@ -338,7 +351,7 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
         if ( p->vIsops[v] )
             Vec_WecFree( p->vIsops[v] );
     }
-    Vec_WrdFreeP( &p->vPerms );
+    Vec_WrdFreeP( &p->vConfigs );
     Vec_IntFreeP( &p->vTemp1 );
     Vec_IntFreeP( &p->vTemp2 );
     ABC_FREE( p->vObjs.pArray );
@@ -1033,7 +1046,6 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
 {
     If_DsdObj_t * pObj; 
     Vec_Int_t * vSets;
-    char * pBuffer = "dsd0";
     word * pTruth; 
     int i, v, Num;
     FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" );
@@ -1042,7 +1054,7 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
         printf( "Writing DSD manager file \"%s\" has failed.\n", pFileName ? pFileName : p->pStore );
         return;
     }
-    fwrite( pBuffer, 4, 1, pFile );
+    fwrite( DSD_VERSION, 4, 1, pFile );
     Num = p->nVars;
     fwrite( &Num, 4, 1, pFile );
     Num = p->LutSize;
@@ -1073,10 +1085,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;
+    Num = p->nConfigWords;
+    fwrite( &Num, 4, 1, pFile );
+    Num = p->nTtBits;
+    fwrite( &Num, 4, 1, pFile );
+    Num = p->vConfigs ? Vec_WrdSize(p->vConfigs) : 0;
     fwrite( &Num, 4, 1, pFile );
     if ( Num )
-        fwrite( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile );
+        fwrite( Vec_WrdArray(p->vConfigs), sizeof(word)*Num, 1, pFile );
     Num = p->pCellStr ? strlen(p->pCellStr) : 0;
     fwrite( &Num, 4, 1, pFile );
     if ( Num )
@@ -1099,7 +1115,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
         return NULL;
     }
     RetValue = fread( pBuffer, 4, 1, pFile );
-    if ( pBuffer[0] != 'd' && pBuffer[1] != 's' && pBuffer[2] != 'd' && pBuffer[3] != '0' )
+    if ( strncmp(pBuffer, DSD_VERSION, strlen(DSD_VERSION)) )
     {
         printf( "Unrecognized format of file \"%s\".\n", pFileName );
         return NULL;
@@ -1160,10 +1176,14 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
     }
     ABC_FREE( pTruth );
     RetValue = fread( &Num, 4, 1, pFile );
+    p->nConfigWords = Num;
+    RetValue = fread( &Num, 4, 1, pFile );
+    p->nTtBits = Num;
+    RetValue = fread( &Num, 4, 1, pFile );
     if ( RetValue && Num )
     {
-        p->vPerms = Vec_WrdStart( Num );
-        RetValue = fread( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile );
+        p->vConfigs = Vec_WrdStart( Num );
+        RetValue = fread( Vec_WrdArray(p->vConfigs), sizeof(word)*Num, 1, pFile );
     }
     RetValue = fread( &Num, 4, 1, pFile );
     if ( RetValue && Num )
@@ -1190,14 +1210,16 @@ void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew )
         printf( "LUT size should be the same.\n" );
         return;
     }
+    assert( p->nTtBits == pNew->nTtBits );
+    assert( p->nConfigWords == pNew->nConfigWords );
     if ( If_DsdManHasMarks(p) != If_DsdManHasMarks(pNew) )
         printf( "Warning! Old manager has %smarks while new manager has %smarks.\n", 
             If_DsdManHasMarks(p) ? "" : "no ", If_DsdManHasMarks(pNew) ? "" : "no " );
     vMap = Vec_IntAlloc( Vec_PtrSize(&pNew->vObjs) );
     Vec_IntPush( vMap, 0 );
     Vec_IntPush( vMap, 1 );
-    if ( p->vPerms && pNew->vPerms )
-        Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs) + Vec_PtrSize(&pNew->vObjs), 0 );
+    if ( p->vConfigs && pNew->vConfigs )
+        Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * (Vec_PtrSize(&p->vObjs) + Vec_PtrSize(&pNew->vObjs)), 0 );
     If_DsdVecForEachNode( &pNew->vObjs, pObj, i )
     {
         If_DsdObjForEachFaninLit( &pNew->vObjs, pObj, iFanin, k )
@@ -1205,14 +1227,19 @@ void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew )
         Id = If_DsdObjFindOrAdd( p, pObj->Type, pFanins, pObj->nFans, pObj->Type == IF_DSD_PRIME ? If_DsdObjTruth(pNew, pObj) : NULL );
         if ( pObj->fMark )
             If_DsdVecObjSetMark( &p->vObjs, Id );
-        if ( p->vPerms && pNew->vPerms && i < Vec_WrdSize(pNew->vPerms) )
-            Vec_WrdFillExtra( p->vPerms, Id, Vec_WrdEntry(pNew->vPerms, i) );
+        if ( p->vConfigs && pNew->vConfigs && p->nConfigWords * i < Vec_WrdSize(pNew->vConfigs) )
+        {
+            //Vec_WrdFillExtra( p->vConfigs, Id, Vec_WrdEntry(pNew->vConfigs, i) );
+            word * pConfigNew = Vec_WrdEntryP(pNew->vConfigs, p->nConfigWords * i);
+            word * pConfigOld = Vec_WrdEntryP(p->vConfigs, p->nConfigWords * Id);
+            memcpy( pConfigOld, pConfigNew, sizeof(word) * p->nConfigWords );
+        }
         Vec_IntPush( vMap, Id );
     }
     assert( Vec_IntSize(vMap) == Vec_PtrSize(&pNew->vObjs) );
     Vec_IntFree( vMap );
-    if ( p->vPerms && pNew->vPerms )
-        Vec_WrdShrink( p->vPerms, Vec_PtrSize(&p->vObjs) );
+    if ( p->vConfigs && pNew->vConfigs )
+        Vec_WrdShrink( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs) );
 }
 void If_DsdManCleanOccur( If_DsdMan_t * p, int fVerbose )
 {
@@ -1226,7 +1253,7 @@ void If_DsdManCleanMarks( If_DsdMan_t * p, int fVerbose )
     If_DsdObj_t * pObj; 
     int i;
     ABC_FREE( p->pCellStr );
-    Vec_WrdFreeP( &p->vPerms );
+    Vec_WrdFreeP( &p->vConfigs );
     If_DsdVecForEachObj( &p->vObjs, pObj, i )
         pObj->fMark = 0;
 }
@@ -1235,7 +1262,7 @@ void If_DsdManInvertMarks( If_DsdMan_t * p, int fVerbose )
     If_DsdObj_t * pObj; 
     int i;
     ABC_FREE( p->pCellStr );
-    Vec_WrdFreeP( &p->vPerms );
+    Vec_WrdFreeP( &p->vConfigs );
     If_DsdVecForEachObj( &p->vObjs, pObj, i )
         pObj->fMark = !pObj->fMark;
 }
@@ -2440,7 +2467,7 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
     int fVeryVerbose = 0;
     ProgressBar * pProgress = NULL;
     If_DsdObj_t * pObj;
-    word * pTruth, Perm;
+    word * pTruth, * pConfig;
     int i, nVars, Value, LutSize;
     abctime clk = Abc_Clock();
     // parse the structure
@@ -2458,6 +2485,8 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
     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);
+    p->nTtBits = Ifn_NtkTtBits( pStruct );
+    p->nConfigWords = 1 + Abc_Bit6WordNum( p->nTtBits );
     // print
     if ( fVerbose )
     {
@@ -2471,30 +2500,32 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
     If_DsdVecForEachObj( &p->vObjs, pObj, i )
         if ( i >= p->nObjsPrev )
             pObj->fMark = 0;
-    if ( p->vPerms == NULL )
-        p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
+    if ( p->vConfigs == NULL )
+        p->vConfigs = Vec_WrdStart( p->nConfigWords * Vec_PtrSize(&p->vObjs) );
     else
-        Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 );
+        Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs), 0 );
     pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
     If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
     {
         if ( (i & 0xFF) == 0 )
             Extra_ProgressBarUpdate( pProgress, i, NULL );
         nVars = If_DsdObjSuppSize(pObj);
-        if ( nVars <= LutSize )
-            continue;
+        //if ( nVars <= LutSize )
+        //    continue;
         pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
         if ( fVeryVerbose )
             Dau_DsdPrintFromTruth( pTruth, nVars );
         if ( fVerbose )
             printf( "%6d : %2d ", i, nVars );
-        Value = Ifn_NtkMatch( pNtk, pTruth, nVars, nConfls, fVerbose, fVeryVerbose, &Perm );
+        pConfig = Vec_WrdEntryP( p->vConfigs, p->nConfigWords * i );
+        Value = Ifn_NtkMatch( pNtk, pTruth, nVars, nConfls, fVerbose, fVeryVerbose, pConfig );
         if ( fVeryVerbose )
             printf( "\n" );
         if ( Value == 0 )
+        {
             If_DsdVecObjSetMark( &p->vObjs, i );
-        else
-            Vec_WrdWriteEntry( p->vPerms, i, Perm );
+            memset( pConfig, 0, sizeof(word) * p->nConfigWords );
+        }
     }
     p->nObjsPrev = 0;
     p->LutSize = 0;
@@ -2531,12 +2562,13 @@ typedef struct Ifn_ThData_t_
 {
     Ifn_Ntk_t * pNtk;    // network
     word        pTruth[DAU_MAX_WORD];
+    word        pConfig[10]; // configuration data
+    int         nConfigWords;// configuration data word count
     int         nVars;   // support
     int         Id;      // object
     int         nConfls; // conflicts
     int         Result;  // result
     int         Status;  // state
-    word        Perm;    // permutation
     abctime     clkUsed; // total runtime
 } Ifn_ThData_t;
 void * Ifn_WorkerThread( void * pArg )
@@ -2555,7 +2587,8 @@ void * Ifn_WorkerThread( void * pArg )
             return NULL;
         }
         clk = Abc_Clock();
-        pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0, &pThData->Perm );
+        memset( pThData->pConfig, 0, sizeof(word) * pThData->nConfigWords );
+        pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0, pThData->pConfig );
         pThData->clkUsed += Abc_Clock() - clk;
         pThData->Status = 0;
 //        printf( "Finished object %d\n", pThData->Id );
@@ -2597,6 +2630,9 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
         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
     LutSize = Ifn_NtkLutSizeMax(pNtk);
+    p->nTtBits = Ifn_NtkTtBits( pStruct );
+    p->nConfigWords = 1 + Abc_Bit6WordNum( p->nTtBits );
+    assert( p->nConfigWords <= 10 );
     if ( fVerbose )
     {
         printf( "Considering programmable cell: " );
@@ -2610,10 +2646,10 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
     If_DsdVecForEachObj( &p->vObjs, pObj, i )
         if ( i >= p->nObjsPrev )
             pObj->fMark = 0;
-    if ( p->vPerms == NULL )
-        p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
+    if ( p->vConfigs == NULL )
+        p->vConfigs = Vec_WrdStart( p->nConfigWords * Vec_PtrSize(&p->vObjs) );
     else
-        Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 );
+        Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs), 0 );
     pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
 
     // perform concurrent solving
@@ -2625,13 +2661,14 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
         // start the threads
         for ( i = 0; i < nProcs; i++ )
         {
-            ThData[i].pNtk    = Ifn_NtkParse( pStruct );
-            ThData[i].nVars   = -1;      // support
-            ThData[i].Id      = -1;      // object
-            ThData[i].nConfls = nConfls; // conflicts
-            ThData[i].Result  = -1;      // result
-            ThData[i].Status  =  0;      // state
-            ThData[i].clkUsed =  0;      // total runtime
+            ThData[i].pNtk     = Ifn_NtkParse( pStruct );
+            ThData[i].nVars    = -1;      // support
+            ThData[i].Id       = -1;      // object
+            ThData[i].nConfls  = nConfls; // conflicts
+            ThData[i].Result   = -1;      // result
+            ThData[i].Status   =  0;      // state
+            ThData[i].clkUsed  =  0;      // total runtime
+            ThData[i].nConfigWords = p->nConfigWords;
             status = pthread_create( WorkerThread + i, NULL, Ifn_WorkerThread, (void *)(ThData + i) );  assert( status == 0 );
         }
         // run the threads
@@ -2649,7 +2686,10 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
                     if ( ThData[i].Result == 0 )
                         If_DsdVecObjSetMark( &p->vObjs, ThData[i].Id );
                     else
-                        Vec_WrdWriteEntry( p->vPerms, ThData[i].Id, ThData[i].Perm );
+                    {
+                        word * pTtWords = Vec_WrdEntryP( p->vConfigs, p->nConfigWords * ThData[i].Id );
+                        memcpy( pTtWords, ThData[i].pConfig, sizeof(word) * p->nConfigWords );
+                    }
                     ThData[i].Id     = -1;
                     ThData[i].Result = -1;
                 }
@@ -2659,8 +2699,8 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
                         Extra_ProgressBarUpdate( pProgress, k, NULL );
                     pObj  = If_DsdVecObj( &p->vObjs, k );
                     nVars = If_DsdObjSuppSize(pObj);
-                    if ( nVars <= LutSize )
-                        continue;
+                    //if ( nVars <= LutSize )
+                    //    continue;
                     clk = Abc_Clock();
                     If_DsdManComputeTruthPtr( p, Abc_Var2Lit(k, 0), NULL, ThData[i].pTruth );
                     clkUsed += Abc_Clock() - clk;
@@ -2738,10 +2778,10 @@ void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose
     If_DsdVecForEachObj( &p->vObjs, pObj, i )
         if ( i >= p->nObjsPrev )
             pObj->fMark = 0;
-    if ( p->vPerms == NULL )
-        p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
+    if ( p->vConfigs == NULL )
+        p->vConfigs = Vec_WrdStart( Vec_PtrSize(&p->vObjs) );
     else
-        Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 );
+        Vec_WrdFillExtra( p->vConfigs, Vec_PtrSize(&p->vObjs), 0 );
     pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
     If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev )
     {
@@ -2767,7 +2807,7 @@ void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose
         if ( Value )
             If_DsdVecObjSetMark( &p->vObjs, i );
         else
-            Vec_WrdWriteEntry( p->vPerms, i, Perm );
+            Vec_WrdWriteEntry( p->vConfigs, i, Perm );
     }
     p->nObjsPrev = 0;
     p->LutSize = 0;
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index 8b7e9d1c..a0e95eaa 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -95,7 +95,7 @@ static inline word *       Ifn_ObjTruth( Ifn_Ntk_t * p, int i )  { return p->pTt
 // - primary inputs            [0;            p->nInps)
 // - internal nodes            [p->nInps;     p->nObjs)
 // - configuration params      [p->nObjs;     p->nParsVIni)
-// - variable selection params [p->nParsVIni; p->pPars)
+// - variable selection params [p->nParsVIni; p->nPars)
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -460,6 +460,16 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
 //    printf( "Finished parsing: " ); Ifn_NtkPrint(p);
     return p;
 }
+int Ifn_NtkTtBits( char * pStr )
+{
+    int i, Counter = 0;
+    Ifn_Ntk_t * pNtk = Ifn_NtkParse( pStr );
+    for ( i = pNtk->nInps; i < pNtk->nObjs; i++ )
+        if ( pNtk->Nodes[i].Type == IFN_DSD_PRIME )
+            Counter += (1 << pNtk->Nodes[i].nFanins);
+    ABC_FREE( pNtk );
+    return Counter;
+}
 
 
 
@@ -728,13 +738,21 @@ int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word P
   SeeAlso     []
 
 ***********************************************************************/
-int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues, Vec_Int_t * vCover )
+int If_ManSatDeriveGiaFromBits( Gia_Man_t * pNew, Ifn_Ntk_t * p, word * pConfigData, Vec_Int_t * vLeaves, 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 );
+    int i, k, iLit, iVar = 0, nVarsNew, pVarMap[1000];
+    int nTtBits = p->nParsVIni - p->nObjs;
+    int nPermBits = Abc_Base2Log(p->nInps + 1) + 1;
+    int fCompl = Abc_TtGetBit( pConfigData, nTtBits + nPermBits * p->nInps );
+    assert( Vec_IntSize(vLeaves) <= p->nInps && p->nParsVIni < 1000 );
+    for ( i = 0; i < p->nInps; i++ )
+    {
+        for ( iLit = k = 0; k < nPermBits; k++ )
+            if ( Abc_TtGetBit(pConfigData, nTtBits + i * nPermBits + k) )
+                iLit |= (1 << k);
+        assert( Abc_Lit2Var(iLit) < Vec_IntSize(vLeaves) );
+        pVarMap[i] = Abc_Lit2LitL( Vec_IntArray(vLeaves), iLit );
+    }
     for ( i = p->nInps; i < p->nObjs; i++ )
     {
         int Type = p->Nodes[i].Type;
@@ -768,7 +786,7 @@ int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues,
             word uTruth = 0;
             int nMints = (1 << nFans);
             for ( k = 0; k < nMints; k++ )
-                if ( Vec_IntEntry( vValues, iVar++ ) )
+                if ( Abc_TtGetBit(pConfigData, iVar++) )
                     uTruth |= ((word)1 << k);
             uTruth = Abc_Tt6Stretch( uTruth, nFans );
             // collect function
@@ -787,8 +805,89 @@ int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues,
         }
         else assert( 0 );
     }
-    assert( iVar == Vec_IntSize(vValues) );
-    return pVarMap[p->nObjs - 1];
+    assert( iVar == nTtBits );
+    return Abc_LitNotCond( pVarMap[p->nObjs - 1], fCompl );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive GIA using programmable bits.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * If_ManDeriveGiaFromCells( void * pGia )
+{
+    Gia_Man_t * p = (Gia_Man_t *)pGia;
+    Gia_Man_t * pNew, * pTemp;
+    Vec_Int_t * vCover, * vLeaves;
+    Ifn_Ntk_t * pNtkCell;
+    Gia_Obj_t * pObj; 
+    word * pConfigData;
+    //word * pTruth;
+    int k, i, iLut, iVar;
+    int nConfigInts, Count = 0;
+    assert( p->vConfigs != NULL );
+    assert( p->pCellStr != NULL );
+    assert( Gia_ManHasMapping(p) );
+    // derive cell network
+    pNtkCell = Ifn_NtkParse( p->pCellStr );
+    Ifn_Prepare( pNtkCell, NULL, pNtkCell->nInps );
+    nConfigInts = Vec_IntEntry( p->vConfigs, 1 );
+    // create new manager
+    pNew = Gia_ManStart( 6*Gia_ManObjNum(p)/5 + 100 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    // map primary inputs
+    Gia_ManFillValue(p);
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    // iterate through nodes used in the mapping
+    vLeaves = Vec_IntAlloc( 16 );
+    vCover  = Vec_IntAlloc( 1 << 16 );
+    Gia_ManHashStart( pNew );
+    //Gia_ObjComputeTruthTableStart( p, Gia_ManLutSizeMax(p) );
+    Gia_ManForEachAnd( p, pObj, iLut )
+    {
+        if ( Gia_ObjIsBuf(pObj) )
+        {
+            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+            continue;
+        }
+        if ( !Gia_ObjIsLut(p, iLut) )
+            continue;
+        // collect leaves
+        //Vec_IntClear( vLeaves );
+        //Gia_LutForEachFanin( p, iLut, iVar, k )
+        //    Vec_IntPush( vLeaves, iVar );
+        //pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, iLut), vLeaves );
+        // collect incoming literals
+        Vec_IntClear( vLeaves );
+        Gia_LutForEachFanin( p, iLut, iVar, k )
+            Vec_IntPush( vLeaves, Gia_ManObj(p, iVar)->Value );
+        pConfigData = (word *)Vec_IntEntryP( p->vConfigs, 2 + nConfigInts * Count++ );
+        Gia_ManObj(p, iLut)->Value = If_ManSatDeriveGiaFromBits( pNew, pNtkCell, pConfigData, vLeaves, vCover );
+    }
+    assert( Vec_IntEntry(p->vConfigs, 0) == Count );
+    assert( Vec_IntSize(p->vConfigs) == 2 + nConfigInts * Count );
+    //Gia_ObjComputeTruthTableStop( p );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    Vec_IntFree( vLeaves );
+    Vec_IntFree( vCover );
+    ABC_FREE( pNtkCell );
+    // perform cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+
 }
 
 /**Function*************************************************************
@@ -1196,6 +1295,21 @@ word Ifn_NtkMatchCollectPerm( Ifn_Ntk_t * p, sat_solver * pSat )
     }
     return Perm;
 }
+void Ifn_NtkMatchCollectConfig( Ifn_Ntk_t * p, sat_solver * pSat, word * pConfig )
+{
+    int i, v, Mint;
+    assert( p->nParsVNum <= 4 );
+    for ( i = 0; i < p->nInps; i++ )
+    {
+        for ( Mint = v = 0; v < p->nParsVNum; v++ )
+            if ( sat_solver_var_value(pSat, p->nParsVIni + i * p->nParsVNum + v) )
+                Mint |= (1 << v);
+        Abc_TtSetHex( pConfig, i, Mint );
+    }
+    for ( v = p->nObjs; v < p->nParsVIni; v++ )
+        if ( sat_solver_var_value(pSat, v) )
+            Abc_TtSetBit( pConfig + 1, v - p->nObjs );
+}
 void Ifn_NtkMatchPrintPerm( word Perm, int nInps )
 {
     int i;
@@ -1204,7 +1318,7 @@ void Ifn_NtkMatchPrintPerm( word Perm, int nInps )
         printf( "%c", 'a' + Abc_TtGetHex(&Perm, i) );
     printf( "\n" );
 }
-int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pPerm )
+int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pConfig )
 {
     word * pTruth1;
     int RetValue = 0;
@@ -1218,7 +1332,7 @@ int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVer
     Ifn_NtkAddConstraints( p, pSat );
     if ( fVeryVerbose )
         Ifn_NtkMatchPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk );
-    if ( pPerm ) *pPerm = 0;
+    if ( pConfig ) assert( *pConfig == 0 );
     for ( i = 0; i < nIterMax; i++ )
     {
         // get variable assignment
@@ -1248,8 +1362,8 @@ int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVer
         iMint = Abc_TtFindFirstBit( pTruth1, p->nVars );
         if ( iMint == -1 )
         {
-            if ( pPerm ) 
-                *pPerm = Ifn_NtkMatchCollectPerm( p, pSat );
+            if ( pConfig ) 
+                Ifn_NtkMatchCollectConfig( p, pSat, pConfig );
 /*
             if ( pPerm )
             {