Structural mapper into structures.

8 files changed, 754 insertions, 2 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 92aa14bd..c8d85b9f 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3715,6 +3715,10 @@ SOURCE=.\src\aig\gia\giaIf.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaIff.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaIso.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/giaCut.h b/src/aig/gia/giaCut.h
new file mode 100644
index 00000000..080d74d6
--- /dev/null
+++ b/src/aig/gia/giaCut.h
@@ -0,0 +1,349 @@
+/**CFile****************************************************************
+
+  FileName    [giaCut.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaCut.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__gia__giaAig_h
+#define ABC__aig__gia__giaAig_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "gia.h"
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define GIA_CUT_LEAF_MAX   8
+#define GIA_CUT_WORD_MAX  ((GIA_CUT_LEAF_MAX > 6) ? 1 << (GIA_CUT_LEAF_MAX-6) : 1)
+#define GIA_CUT_NUM_MAX   16
+
+typedef struct Gia_Cut_t_ Gia_Cut_t; 
+struct Gia_Cut_t_
+{
+    word             Sign;        // signature
+    int              Id;          // cut ID
+    int              iFunc;       // function 
+    int              iNext;       // next cut
+    int              iFan0;       // left child
+    int              iFan1;       // right child
+    int              nLeaves;     // number of leaves
+    int              pLeaves[GIA_CUT_LEAF_MAX]; // cut
+    int              pCompls[GIA_CUT_LEAF_MAX]; // polarity
+};
+
+static inline int    Gia_CutSize( int * pCut )       { return pCut[0] & 0xF; }  //  4 bits
+
+#define Gia_ObjForEachCut( pList, pCut, i, AddOn )   for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += Gia_CutSize(pCut) + AddOn )
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+// loads cuts from storage
+static inline int Gia_ObjLoadCuts( Gia_Cut_t * pCutsI, int * pCuts, int AddOn )
+{
+    Gia_Cut_t * pCutsICur;
+    int i, k, Lit, * pCut; 
+    assert( AddOn == 1 || AddOn == 2 );
+    Gia_ObjForEachCut( pCuts, pCut, i, AddOn )
+    {
+        pCutsICur = pCutsI + i;
+        pCutsICur->Id = i;
+        pCutsICur->Sign = 0;
+        pCutsICur->iFunc = (AddOn == 1) ? -1 : pCut[pCut[0] + 1];
+        pCutsICur->nLeaves = pCut[0];    
+        for ( k = 0; k < pCut[0]; k++ )
+        {
+            Lit = pCut[k+1];
+            pCutsICur->pCompls[k] = Abc_LitIsCompl(Lit);
+            pCutsICur->pLeaves[k] = Abc_Lit2Var(Lit);
+            pCutsICur->Sign |= 1 << (Abc_Lit2Var(Lit) & 0x3F);
+        }
+    }
+    return i;
+}
+
+static inline int Gia_CutId( Gia_Cut_t * pCutsOut, Gia_Cut_t * pCut )
+{
+    return pCut - pCutsOut;
+}
+static inline void Gia_CutInsert( Gia_Cut_t * pCutsOut, Gia_Cut_t * pCut ) // inserts cut into the list
+{
+    int * pPlace = &pCutsOut[pCut->nLeaves].iNext;
+    pCut->iNext = *pPlace; *pPlace = pCut - pCutsOut;
+}
+static inline void Gia_CutRemove( int * pPlace, Gia_Cut_t * pCut ) // removes cut from the list
+{
+    *pPlace = pCut->iNext;
+}
+static inline word Gia_CutGetSign( Gia_Cut_t * pCut )
+{
+    word Sign = 0; int i; 
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        Sign |= ((word)1) << (pCut->pLeaves[i] & 0x3F);
+    return Sign;
+}
+static inline int Gia_CutCountBits( word i )
+{
+    i = i - ((i >> 1) & 0x5555555555555555);
+    i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333);
+    i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
+    return (i*(0x0101010101010101))>>56;
+}
+
+static inline int Gia_CutIsContainedOrder( Gia_Cut_t * pBase, Gia_Cut_t * pCut ) // check if pCut is contained pBase
+{
+    int i, k;
+    if ( pBase->nLeaves == pCut->nLeaves )
+    {
+        for ( i = 1; i <= pCut->nLeaves; i++ )
+            if ( pBase->pLeaves[i] != pCut->pLeaves[i] )
+                return 0;
+        return 1;
+    }
+    assert( pBase->nLeaves > pCut->nLeaves ); 
+    for ( i = k = 1; i <= pBase->nLeaves; i++ )
+    {
+        if ( pBase->pLeaves[i] > pCut->pLeaves[k] )
+            return 0;
+        if ( pBase->pLeaves[i] == pCut->pLeaves[k] )
+        {
+            if ( k++ == pCut->nLeaves )
+                return 1;
+        }
+    }
+    return 0;
+}
+
+
+// check if the given cut is contained in previous cuts
+static inline int Gia_ObjCheckContainInPrev( Gia_Cut_t * pCutsOut, Gia_Cut_t * pCut )
+{
+    Gia_Cut_t * pPrev;
+    for ( pPrev = pCutsOut; pPrev->iNext; pPrev = pCutsOut + pPrev->iNext )
+    {
+        if ( pPrev->iFunc == -2 ) // skip sentinels
+            continue;
+        if ( pPrev->nLeaves > pCut->nLeaves ) // stop when we reached bigger cuts
+            return 0;
+        if ( (pCut->Sign & pPrev->Sign) != pPrev->Sign )
+            continue;
+        if ( Gia_CutIsContainedOrder(pPrev, pCut) )
+            return 1;
+    }
+    assert( 0 );
+    return 1;
+}
+
+// check if the given cut contains following cuts
+static inline void Gia_ObjCheckContainsNext( Gia_Cut_t * pCutsOut, Gia_Cut_t * pCut, int ** ppPlace )
+{
+    Gia_Cut_t * pNext;
+    int * pPlace = &pCut->iNext;
+    while ( *pPlace )
+    {
+        pNext = pCutsOut + pNext->iNext;
+        if ( pNext->iFunc == -2 ) // skip sentinels
+            continue;
+        assert( pNext != pCut && pNext->nLeaves >= pCut->nLeaves );
+        if ( (pNext->Sign & pCut->Sign) != pCut->Sign )
+            continue;
+        if ( !Gia_CutIsContainedOrder(pCut, pNext) )
+        {
+            pPlace = &pNext->iNext;
+            continue;
+        }
+        // shift the pointer
+        if ( *ppPlace == &pNext->iNext )
+            *ppPlace = pPlace;
+         // remove pNext
+        Gia_CutRemove( pPlace, pNext );
+    }
+}
+
+static inline int Gia_ObjMergeCutsOrder( Gia_Cut_t * pCut, Gia_Cut_t * pCut0, Gia_Cut_t * pCut1, int LutSize )
+{
+    int nSize0 = pCut0->nLeaves;
+    int nSize1 = pCut1->nLeaves;
+    int * pC0 = pCut0->pLeaves;
+    int * pC1 = pCut1->pLeaves;
+    int * pC = pCut->pLeaves;
+    int i, k, c, s;
+    // the case of the largest cut sizes
+    if ( nSize0 == LutSize && nSize1 == LutSize )
+    {
+        for ( i = 0; i < nSize0; i++ )
+        {
+            if ( pC0[i] != pC1[i] )
+                return 0;
+            pC[i] = pC0[i];
+        }
+        pCut->nLeaves = LutSize;
+        return 1;
+    }
+    // compare two cuts with different numbers
+    i = k = c = s = 0;
+    while ( 1 )
+    {
+        if ( c == LutSize ) return 0;
+        if ( pC0[i] < pC1[k] )
+        {
+            pC[c++] = pC0[i++];
+            if ( i >= nSize0 ) goto FlushCut1;
+        }
+        else if ( pC0[i] > pC1[k] )
+        {
+            pC[c++] = pC1[k++];
+            if ( k >= nSize1 ) goto FlushCut0;
+        }
+        else
+        {
+            pC[c++] = pC0[i++]; k++;
+            if ( i >= nSize0 ) goto FlushCut1;
+            if ( k >= nSize1 ) goto FlushCut0;
+        }
+    }
+
+FlushCut0:
+    if ( c + nSize0 > LutSize + i ) return 0;
+    while ( i < nSize0 )
+        pC[c++] = pC0[i++];
+    pCut->nLeaves = c;
+    return 1;
+
+FlushCut1:
+    if ( c + nSize1 > LutSize + k ) return 0;
+    while ( k < nSize1 )
+        pC[c++] = pC1[k++];
+    pCut->nLeaves = c;
+    return 1;
+}
+
+static inline int Gia_ObjCombineCuts( Gia_Cut_t * pCutsOut, Gia_Cut_t * pCut, Gia_Cut_t * pCut0, Gia_Cut_t * pCut1, int LutSize )
+{
+    if ( !Gia_ObjMergeCutsOrder(pCut, pCut0, pCut1, LutSize) )
+        return 0;
+    pCut->Sign = pCut0->Sign | pCut1->Sign;
+    if ( !Gia_ObjCheckContainInPrev(pCutsOut, pCut) )
+        return 0;
+    Gia_CutInsert( pCutsOut, pCut );
+    pCut->Id = pCut - pCutsOut;
+    pCut->iFan0 = pCut0->Id;
+    pCut->iFan1 = pCut1->Id;
+    pCut->iFunc = -1;
+    return 1;
+}
+
+int Gia_TtComputeForCut( Vec_Mem_t * vTtMem, int iFuncLit0, int iFuncLit1, Gia_Cut_t * pCut0, Gia_Cut_t * pCut1, Gia_Cut_t * pCut, int LutSize )
+{
+    word uTruth[GIA_CUT_WORD_MAX], uTruth0[GIA_CUT_WORD_MAX], uTruth1[GIA_CUT_WORD_MAX];
+    int fCompl, truthId;
+    int nWords     = Abc_Truth6WordNum(LutSize);
+    word * pTruth0 = Vec_MemReadEntry(vTtMem, Abc_Lit2Var(iFuncLit0));
+    word * pTruth1 = Vec_MemReadEntry(vTtMem, Abc_Lit2Var(iFuncLit1));
+    Abc_TtCopy( uTruth0, pTruth0, nWords, Abc_LitIsCompl(iFuncLit0) );
+    Abc_TtCopy( uTruth1, pTruth1, nWords, Abc_LitIsCompl(iFuncLit1) );
+    Abc_TtStretch( uTruth0, LutSize, pCut0->pLeaves, pCut0->nLeaves, pCut->pLeaves, pCut->nLeaves );
+    Abc_TtStretch( uTruth1, LutSize, pCut1->pLeaves, pCut1->nLeaves, pCut->pLeaves, pCut->nLeaves );
+    fCompl         = (int)(uTruth0[0] & uTruth1[0] & 1);
+    Abc_TtAnd( uTruth, uTruth0, uTruth1, nWords, fCompl );
+    pCut->nLeaves  = Abc_TtMinBase( uTruth, pCut->pLeaves, pCut->nLeaves, LutSize );
+    assert( (uTruth[0] & 1) == 0 );
+    truthId        = Vec_MemHashInsert(vTtMem, uTruth);
+    return Abc_Var2Lit( truthId, fCompl );
+}
+
+//  Gia_Cut_t pCutsOut[GIA_CUT_LEAF_MAX + 2 + GIA_CUT_NUM_MAX * GIA_CUT_NUM_MAX]; // LutSize+1 placeholders + CutNum ^ 2 + 1
+static inline int Gia_ObjComputeCuts( Gia_Cut_t * pCutsOut, int * pCuts0, int * pCuts1, Vec_Mem_t * vTtMem, int AddOn, int nLutSize, int nCutNum, int fCompl0, int fCompl1 )
+{
+    Gia_Cut_t * pCut;
+    Gia_Cut_t pCuts0i[GIA_CUT_NUM_MAX];
+    Gia_Cut_t pCuts1i[GIA_CUT_NUM_MAX];
+    int i, nCuts0i = Gia_ObjLoadCuts( pCuts0i, pCuts0, AddOn );
+    int k, nCuts1i = Gia_ObjLoadCuts( pCuts1i, pCuts1, AddOn );
+    int * pPlace, c = GIA_CUT_NUM_MAX + 1;
+    assert( nCuts0i <= GIA_CUT_NUM_MAX );
+    assert( nCuts1i <= GIA_CUT_NUM_MAX );
+    // prepare cuts
+    for ( i = 0; i <= GIA_CUT_NUM_MAX; i++ )
+    {
+        pCut = pCutsOut + i;
+        pCut->nLeaves =   i;
+        pCut->iNext   = i+1;
+        pCut->iFunc   =  -2;
+        pCut->Id      =   i;
+    }
+    pCut->iNext = 0;
+    // enumerate pairs
+    for ( i = 0; i < nCuts0i; i++ )
+    for ( k = 0; k < nCuts1i; k++ )
+        if ( Gia_CutCountBits(pCuts0i[i].Sign | pCuts1i[k].Sign) <= nLutSize )
+            Gia_ObjCombineCuts( pCutsOut, pCutsOut + c++, pCuts0i + i, pCuts1i + k, nLutSize );
+    assert( c <= GIA_CUT_LEAF_MAX + 2 + GIA_CUT_NUM_MAX * GIA_CUT_NUM_MAX );
+    // check containment for cuts
+    for ( pPlace = &pCutsOut->iNext; *pPlace; pPlace = &pCut->iNext )
+    {
+        pCut = pCutsOut + *pPlace;
+        if ( pCut->iFunc == -2 )
+            continue;
+        // compute truth table
+        if ( AddOn == 2 )
+        {
+            Gia_Cut_t * pCut0 = pCuts0i + pCut->iFan0;
+            Gia_Cut_t * pCut1 = pCuts1i + pCut->iFan1;
+            int iLit0 = Abc_LitNotCond( pCut0->iFunc, fCompl0 );
+            int iLit1 = Abc_LitNotCond( pCut1->iFunc, fCompl1 );
+            int nLeavesOld = pCut->nLeaves;
+            pCut->iFunc = Gia_TtComputeForCut( vTtMem, iLit0, iLit1, pCut0, pCut1, pCut, nLutSize );
+            // if size has changed, move the cut closer
+            if ( nLeavesOld != pCut->nLeaves )
+            {
+                Gia_CutRemove( pPlace, pCut );
+                Gia_CutInsert( pCutsOut, pCut );
+                pCut->Sign = Gia_CutGetSign( pCut );
+            }
+        }
+        // check containment after this cut
+        Gia_ObjCheckContainsNext( pCutsOut, pCut, &pPlace );
+    }
+}
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 425445c9..bcd63166 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -1461,6 +1461,7 @@ void Gia_ManTransferPacking( Gia_Man_t * pGia, Gia_Man_t * p )
 ***********************************************************************/
 Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp, int fNormalized )
 {
+    extern void Gia_ManIffTest( Gia_Man_t * pGia, If_LibLut_t * pLib, int fVerbose );
     Gia_Man_t * pNew;
     If_Man_t * pIfMan;
     If_Par_t * pPars = (If_Par_t *)pp;
@@ -1529,6 +1530,8 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp, int fNormalized )
     Gia_ManStop( p );
 //    printf( "PERFORMING VERIFICATION:\n" );
 //    Gia_ManVerifyWithBoxes( pNew, NULL );
+    if ( pPars->fRepack )
+        Gia_ManIffTest( pNew, pPars->pLutLib, pPars->fVerbose );
     return pNew;
 }
 
diff --git a/src/aig/gia/giaIff.c b/src/aig/gia/giaIff.c
new file mode 100644
index 00000000..f4b6f9a5
--- /dev/null
+++ b/src/aig/gia/giaIff.c
@@ -0,0 +1,382 @@
+/**CFile****************************************************************
+
+  FileName    [giaIff.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Hierarchical mapping of AIG with white boxes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaIff.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "map/if/if.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Iff_Man_t_ Iff_Man_t;
+struct Iff_Man_t_
+{
+    Gia_Man_t *   pGia;          // mapped GIA
+    If_LibLut_t * pLib;          // LUT library
+    int           nLutSize;      // LUT size
+    int           nDegree;       // degree 
+    Vec_Flt_t *   vTimes;        // arrival times
+    Vec_Int_t *   vMatch[4];     // matches
+};
+
+static inline float Iff_ObjTimeId( Iff_Man_t * p, int iObj, int Type )                      { return Vec_FltEntry( p->vTimes, iObj );                      }
+static inline float Iff_ObjTime( Iff_Man_t * p, Gia_Obj_t * pObj, int Type )                { return Iff_ObjTimeId( p, Gia_ObjId(p->pGia, pObj), Type );   }
+static inline void  Iff_ObjSetTimeId( Iff_Man_t * p, int iObj, int Type, float Time )       { Vec_FltWriteEntry( p->vTimes, iObj, Time );                  }
+static inline void  Iff_ObjSetTime( Iff_Man_t * p, Gia_Obj_t * pObj, int Type, float Time ) { Iff_ObjSetTimeId( p, Gia_ObjId(p->pGia, pObj), Type, Time ); }
+
+static inline int   Iff_ObjMatchId( Iff_Man_t * p, int iObj, int Type )                     { return Vec_IntEntry( p->vMatch[Type], iObj );                }
+static inline int   Iff_ObjMatch( Iff_Man_t * p, Gia_Obj_t * pObj, int Type )               { return Iff_ObjTimeId( p, Gia_ObjId(p->pGia, pObj), Type );   }
+static inline void  Iff_ObjSetMatchId( Iff_Man_t * p, int iObj, int Type, int Match )       { Vec_IntWriteEntry( p->vMatch[Type], iObj, Match );           }
+static inline void  Iff_ObjSetMatch( Iff_Man_t * p, Gia_Obj_t * pObj, int Type, int Match ) { Iff_ObjSetTimeId( p, Gia_ObjId(p->pGia, pObj), Type, Match );}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Iff_Man_t * Gia_ManIffStart( Gia_Man_t * pGia )
+{
+    Iff_Man_t * p = ABC_CALLOC( Iff_Man_t, 1 );
+    p->vTimes    = Vec_FltStartFull( Gia_ManObjNum(pGia) );
+    p->vMatch[2] = Vec_IntStartFull( Gia_ManObjNum(pGia) );
+    p->vMatch[3] = Vec_IntStartFull( Gia_ManObjNum(pGia) );
+    return p;
+}
+void Gia_ManIffStop( Iff_Man_t * p )
+{
+    Vec_FltFree( p->vTimes );
+    Vec_IntFree( p->vMatch[2] );
+    Vec_IntFree( p->vMatch[3] );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Gia_IffObjTimeBest( Iff_Man_t * p, int iObj )
+{
+    return Abc_MinFloat( Iff_ObjTimeId(p, iObj, 1), Iff_ObjTimeId(p, iObj, 2) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of unique fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_IffObjCount( Gia_Man_t * pGia, int iObj, int iFaninSkip, int iFaninSkip2 )
+{
+    int i, iFanin, Count = 0;
+    Gia_ManIncrementTravId( pGia );
+    Gia_LutForEachFanin( pGia, iObj, iFanin, i )
+    {
+        if ( iFanin == iFaninSkip || iFanin == iFaninSkip2 )
+            continue;
+        if ( Gia_ObjIsTravIdCurrentId( pGia, iFanin ) )
+            continue;
+        Gia_ObjSetTravIdCurrentId( pGia, iFanin );
+        Count++;
+    }
+    if ( iFaninSkip >= 0 )
+    {
+        Gia_LutForEachFanin( pGia, iFaninSkip, iFanin, i )
+        {
+            if ( iFanin == iFaninSkip2 )
+                continue;
+            if ( Gia_ObjIsTravIdCurrentId( pGia, iFanin ) )
+                continue;
+            Gia_ObjSetTravIdCurrentId( pGia, iFanin );
+            Count++;
+        }
+    }
+    if ( iFaninSkip2 >= 0 )
+    {
+        Gia_LutForEachFanin( pGia, iFaninSkip2, iFanin, i )
+        {
+            if ( Gia_ObjIsTravIdCurrentId( pGia, iFanin ) )
+                continue;
+            Gia_ObjSetTravIdCurrentId( pGia, iFanin );
+            Count++;
+        }
+    }
+    return Count;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Gia_IffObjTimeOne( Iff_Man_t * p, int iObj, int iFaninSkip, int iFaninSkip2 )
+{
+    int i, iFanin;
+    float Best = -ABC_INFINITY;
+    Gia_LutForEachFanin( p->pGia, iObj, iFanin, i )
+        if ( iFanin != iFaninSkip && iFanin != iFaninSkip2 && Best < Iff_ObjTimeId(p, iFanin, 1) )
+            Best = Iff_ObjTimeId(p, iFanin, 1);
+    assert( i == Gia_ObjLutSize(p->pGia, iObj) );
+    if ( iFaninSkip == -1 )
+        return Best + p->pLib->pLutDelays[i][0];
+    Gia_LutForEachFanin( p->pGia, iFaninSkip, iFanin, i )
+        if ( Best < Iff_ObjTimeId(p, iFanin, 1) )
+            Best = Iff_ObjTimeId(p, iFanin, 1);
+    if ( iFaninSkip2 == -1 )
+        return Best;
+    Gia_LutForEachFanin( p->pGia, iFaninSkip2, iFanin, i )
+        if ( Best < Iff_ObjTimeId(p, iFanin, 1) )
+            Best = Iff_ObjTimeId(p, iFanin, 1);
+    assert( Best >= 0 );
+    return Best;
+}
+float Gia_IffObjTimeTwo( Iff_Man_t * p, int iObj, int * piFanin )
+{
+    int i, iFanin, nSize;
+    float This, Best = -ABC_INFINITY;
+    *piFanin = -1;
+    Gia_LutForEachFanin( p->pGia, iObj, iFanin, i )
+    {
+        This = Gia_IffObjTimeOne( p, iObj, iFanin, -1 );
+        nSize = Abc_MinInt( Gia_ObjLutSize(p->pGia, iObj) + Gia_ObjLutSize(p->pGia, iFanin) - 1, p->pLib->LutMax );
+        This += p->pLib->pLutDelays[nSize][0];
+        if ( Best < This )
+        {
+            Best = This;
+            *piFanin = iFanin;
+        }
+    }
+    return Best;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Iff_Man_t * Gia_ManIffPerform( Gia_Man_t * pGia, If_LibLut_t * pLib, Tim_Man_t * pTime, int nLutSize, int nDegree )
+{
+    Iff_Man_t * p;
+    Gia_Obj_t * pObj;
+    float arrTime1, arrTime2; 
+    int iObj, iFanin;
+    assert( nDegree == 2 );//|| nDegree == 3 );
+    // start the mapping manager and set its parameters
+    p = Gia_ManIffStart( pGia );
+    p->pGia     = pGia;
+    p->pLib     = pLib;
+    p->nLutSize = nLutSize;
+    p->nDegree  = nDegree;
+    // compute arrival times of each node
+    Iff_ObjSetTimeId( p, 0, 1, 0 );
+    Iff_ObjSetTimeId( p, 0, 2, 0 );
+    Iff_ObjSetTimeId( p, 0, 3, 0 );
+    Tim_ManIncrementTravId( pTime );
+    Gia_ManForEachObj1( pGia, pObj, iObj )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            if ( !Gia_ObjIsLut(pGia, iObj) )
+                continue;
+            // compute arrival times of LUT inputs
+            arrTime1 = Gia_IffObjTimeOne( p, iObj, -1, -1 );
+            // compute arrival times of LUT pairs
+            arrTime2 = Gia_IffObjTimeTwo( p, iObj, &iFanin );
+            // check arrival times
+            Iff_ObjSetTimeId( p, iObj, 1, arrTime2 );
+            if ( arrTime2 < arrTime1 )
+                Iff_ObjSetMatchId( p, iObj, 2, iFanin );
+            // compute arrival times of LUT triples
+        }
+        else if ( Gia_ObjIsCi(pObj) )
+        {
+            arrTime1 = Tim_ManGetCiArrival( pTime, Gia_ObjCioId(pObj) );
+            Iff_ObjSetTime( p, pObj, 1, arrTime1 );
+            Iff_ObjSetTime( p, pObj, 2, arrTime1 );
+            Iff_ObjSetTime( p, pObj, 3, arrTime1 );
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            arrTime1 = Gia_IffObjTimeBest( p, Gia_ObjFaninId0p(pGia, pObj) );
+            Tim_ManSetCoArrival( pTime, Gia_ObjCioId(pObj), arrTime1 );
+            Iff_ObjSetTime( p, pObj, 1, arrTime1 );
+            Iff_ObjSetTime( p, pObj, 2, arrTime1 );
+            Iff_ObjSetTime( p, pObj, 3, arrTime1 );
+        }
+        else assert( 0 );
+    }
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+void Gia_ManIffSelect_rec( Iff_Man_t * p, int iObj, Vec_Int_t * vPacking )
+{
+    int i, iFanin, iFaninSkip;
+    if ( Gia_ObjIsTravIdCurrentId( p->pGia, iObj ) )
+        return;
+    Gia_ObjSetTravIdCurrentId( p->pGia, iObj );
+    assert( Gia_ObjIsLut(p->pGia, iObj) );
+    iFaninSkip = Iff_ObjMatchId(p, iObj, 2);
+    if ( iFaninSkip == -1 )
+    {
+        Gia_LutForEachFanin( p->pGia, iObj, iFanin, i )
+            Gia_ManIffSelect_rec( p, iFanin, vPacking );
+        Vec_IntPush( vPacking, 1 );
+        Vec_IntPush( vPacking, iObj );
+    }
+    else
+    {
+        Gia_LutForEachFanin( p->pGia, iFaninSkip, iFanin, i )
+                Gia_ManIffSelect_rec( p, iFanin, vPacking );
+        Gia_LutForEachFanin( p->pGia, iObj, iFanin, i )
+            if ( iFanin != iFaninSkip )
+                Gia_ManIffSelect_rec( p, iFanin, vPacking );
+        Vec_IntPush( vPacking, 2 );
+        Vec_IntPush( vPacking, iFaninSkip );
+        Vec_IntPush( vPacking, iObj );
+    }
+    Vec_IntAddToEntry( vPacking, 0, 1 );
+}
+Vec_Int_t * Gia_ManIffSelect( Iff_Man_t * p )
+{
+    Vec_Int_t * vPacking;
+    Gia_Obj_t * pObj; int i;
+    vPacking = Vec_IntAlloc( Gia_ManObjNum(p->pGia) );
+    Vec_IntPush( vPacking, 0 );
+    // mark const0 and PIs
+    Gia_ManIncrementTravId( p->pGia );
+    Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) );
+    Gia_ManForEachCi( p->pGia, pObj, i )
+        Gia_ObjSetTravIdCurrent( p->pGia, pObj );
+    // recursively collect internal nodes
+    Gia_ManForEachCo( p->pGia, pObj, i )
+        Gia_ManIffSelect_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), vPacking );
+    return vPacking;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This command performs hierarhical mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+void Gia_ManIffTest( Gia_Man_t * pGia, If_LibLut_t * pLib, int fVerbose )
+{
+    Iff_Man_t * p;
+    int nDegree = -1;
+    int nLutSize = Gia_ManLutSizeMax( pGia );
+    if ( nLutSize <= 4 )
+    {
+        nLutSize = 4;
+        if ( pLib->LutMax <= 7 )
+            nDegree = 2;
+        else if ( pLib->LutMax <= 10 )
+            nDegree = 3;
+        else
+            { printf( "Degree is more than 3.\n" ); return; }
+    }
+    else if ( nLutSize <= 6 )
+    {
+        nLutSize = 6;
+        if ( pLib->LutMax <= 11 )
+            nDegree = 2;
+        else if ( pLib->LutMax <= 16 )
+            nDegree = 3;
+        else
+            { printf( "Degree is more than 3.\n" ); return; }
+    }
+    else
+    {
+        printf( "The LUT size is more than 6.\n" );
+        return;
+    }
+    if ( fVerbose )
+        printf( "Performing %d-clustering with %d-LUTs:\n", nDegree, nLutSize );
+    // create timing manager
+    if ( pGia->pManTime == NULL )
+        pGia->pManTime = Tim_ManStart( Gia_ManCiNum(pGia), Gia_ManCoNum(pGia) );
+    // perform timing computation
+    p = Gia_ManIffPerform( pGia, pLib, pGia->pManTime, nLutSize, nDegree );
+    // derive clustering
+    Vec_IntFreeP( &pGia->vPacking );
+    pGia->vPacking = Gia_ManIffSelect( p );
+    Gia_ManIffStop( p );
+    // print statistics
+    if ( fVerbose )
+        Gia_ManPrintPackingStats( pGia );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index c0a84507..50807bf5 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -27,6 +27,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaGlitch.c \
     src/aig/gia/giaHash.c \
     src/aig/gia/giaIf.c \
+    src/aig/gia/giaIff.c \
     src/aig/gia/giaIso.c \
     src/aig/gia/giaIso2.c \
     src/aig/gia/giaJf.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6400cfd6..b7d8954a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -29741,7 +29741,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     pPars->pLutLib = (If_LibLut_t *)pAbc->pLibLut;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSqalepmrsdbgyojikfuzvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSqalepmrsdbgyojikfuztvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -29917,6 +29917,9 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'z':
             pPars->fDeriveLuts ^= 1;
             break;
+        case 't':
+            pPars->fRepack ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -30111,7 +30114,7 @@ usage:
         sprintf(LutSize, "library" );
     else
         sprintf(LutSize, "%d", pPars->nLutSize );
-    Abc_Print( -2, "usage: &if [-KCFAGR num] [-DEW float] [-S str] [-qarlepmsdbgyojikfuczvh]\n" );
+    Abc_Print( -2, "usage: &if [-KCFAGR num] [-DEW float] [-S str] [-qarlepmsdbgyojikfucztvh]\n" );
     Abc_Print( -2, "\t           performs FPGA technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -30142,6 +30145,7 @@ usage:
     Abc_Print( -2, "\t-f       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75? "yes": "no" );
     Abc_Print( -2, "\t-u       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75u? "yes": "no" );
     Abc_Print( -2, "\t-z       : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" );
+    Abc_Print( -2, "\t-t       : toggles repacking LUTs into new structures [default = %s]\n", pPars->fRepack? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");
     return 1;
diff --git a/src/map/if/if.h b/src/map/if/if.h
index c51fa940..62992138 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -123,6 +123,7 @@ struct If_Par_t_
     int                fEnableCheck75u;// enable additional checking
     int                fUseDsd;       // compute DSD of the cut functions
     int                fDeriveLuts;   // enables deriving LUT structures
+    int                fRepack;       // repack after mapping
     int                fVerbose;      // the verbosity flag
     char *             pLutStruct;    // LUT structure
     float              WireDelay;     // wire delay
diff --git a/src/misc/vec/vecFlt.h b/src/misc/vec/vecFlt.h
index d5184268..57bfe3c1 100644
--- a/src/misc/vec/vecFlt.h
+++ b/src/misc/vec/vecFlt.h
@@ -106,6 +106,14 @@ static inline Vec_Flt_t * Vec_FltStart( int nSize )
     memset( p->pArray, 0, sizeof(float) * nSize );
     return p;
 }
+static inline Vec_Flt_t * Vec_FltStartFull( int nSize )
+{
+    Vec_Flt_t * p;
+    p = Vec_FltAlloc( nSize );
+    p->nSize = nSize;
+    memset( p->pArray, 0xFF, sizeof(float) * nSize );
+    return p;
+}
 
 /**Function*************************************************************