Integrating barrier buffers.

12 files changed, 128 insertions, 66 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 9a256302..d89888e0 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -390,6 +390,7 @@ static inline int          Gia_ManAndNum( Gia_Man_t * p )      { return p->nObjs
 static inline int          Gia_ManXorNum( Gia_Man_t * p )      { return p->nXors;                                                          }
 static inline int          Gia_ManMuxNum( Gia_Man_t * p )      { return p->nMuxes;                                                         }
 static inline int          Gia_ManBufNum( Gia_Man_t * p )      { return p->nBufs;                                                          }
+static inline int          Gia_ManAndNotBufNum( Gia_Man_t * p ){ return Gia_ManAndNum(p) - Gia_ManBufNum(p);                               }
 static inline int          Gia_ManCandNum( Gia_Man_t * p )     { return Gia_ManCiNum(p) + Gia_ManAndNum(p);                                }
 static inline int          Gia_ManConstrNum( Gia_Man_t * p )   { return p->nConstrs;                                                       }
 static inline void         Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1;                                                         } 
@@ -423,7 +424,8 @@ static inline int          Gia_ObjIsXor( Gia_Obj_t * pObj )                    {
 static inline int          Gia_ObjIsMuxId( Gia_Man_t * p, int iObj )           { return p->pMuxes && p->pMuxes[iObj] > 0;        } 
 static inline int          Gia_ObjIsMux( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Gia_ObjIsMuxId( p, Gia_ObjId(p, pObj) ); } 
 static inline int          Gia_ObjIsAndReal( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsAnd(pObj) && pObj->iDiff0 > pObj->iDiff1 && !Gia_ObjIsMux(p, pObj); } 
-static inline int          Gia_ObjIsBarBuf( Gia_Obj_t * pObj )                 { return pObj->iDiff0 == pObj->iDiff1 && !pObj->fTerm; } 
+static inline int          Gia_ObjIsBuf( Gia_Obj_t * pObj )                    { return pObj->iDiff0 == pObj->iDiff1 && pObj->iDiff0 != GIA_NONE && !pObj->fTerm;    } 
+static inline int          Gia_ObjIsAndNotBuf( Gia_Obj_t * pObj )              { return Gia_ObjIsAnd(pObj) && pObj->iDiff0 != pObj->iDiff1; } 
 static inline int          Gia_ObjIsCand( Gia_Obj_t * pObj )                   { return Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj); } 
 static inline int          Gia_ObjIsConst0( Gia_Obj_t * pObj )                 { return pObj->iDiff0 == GIA_NONE && pObj->iDiff1 == GIA_NONE;     } 
 static inline int          Gia_ManObjIsConst0( Gia_Man_t * p, Gia_Obj_t * pObj){ return pObj == p->pObjs;                        } 
@@ -500,10 +502,11 @@ static inline int          Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj )     {
 static inline void         Gia_ObjSetLevelId( Gia_Man_t * p, int Id, int l )   { Vec_IntSetEntry(p->vLevels, Id, l);                        }
 static inline void         Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int l )  { Gia_ObjSetLevelId( p, Gia_ObjId(p,pObj), l );       }
 static inline void         Gia_ObjSetCoLevel( Gia_Man_t * p, Gia_Obj_t * pObj )  { assert( Gia_ObjIsCo(pObj)  ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) );                                                }
+static inline void         Gia_ObjSetBufLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) );                                                }
 static inline void         Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
 static inline void         Gia_ObjSetXorLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsXor(pObj) ); Gia_ObjSetLevel( p, pObj, 2+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
 static inline void         Gia_ObjSetMuxLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsMux(p,pObj) ); Gia_ObjSetLevel( p, pObj, 2+Abc_MaxInt( Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))), Gia_ObjLevel(p,Gia_ObjFanin2(p,pObj))) ); }
-static inline void         Gia_ObjSetGateLevel( Gia_Man_t * p, Gia_Obj_t * pObj ){ if ( Gia_ObjIsMux(p,pObj) ) Gia_ObjSetMuxLevel(p, pObj); else if ( Gia_ObjIsXor(pObj) ) Gia_ObjSetXorLevel(p, pObj); else if ( Gia_ObjIsAnd(pObj) ) Gia_ObjSetAndLevel(p, pObj); }
+static inline void         Gia_ObjSetGateLevel( Gia_Man_t * p, Gia_Obj_t * pObj ){ if ( Gia_ObjIsBuf(pObj) ) Gia_ObjSetBufLevel(p, pObj); else if ( Gia_ObjIsMux(p,pObj) ) Gia_ObjSetMuxLevel(p, pObj); else if ( Gia_ObjIsXor(pObj) ) Gia_ObjSetXorLevel(p, pObj); else if ( Gia_ObjIsAnd(pObj) ) Gia_ObjSetAndLevel(p, pObj); }
 
 static inline int          Gia_ObjHasNumId( Gia_Man_t * p, int Id )                { return Vec_IntEntry(p->vTtNums, Id) > -ABC_INFINITY;     }
 static inline int          Gia_ObjNumId( Gia_Man_t * p, int Id )                   { return Vec_IntEntry(p->vTtNums, Id);                     }
@@ -993,9 +996,9 @@ static inline int         Gia_ObjCellId( Gia_Man_t * p, int iLit )          { re
 #define Gia_ManForEachObjReverse1( p, pObj, i )                         \
     for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- )
 #define Gia_ManForEachBuf( p, pObj, i )                                 \
-    for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )      if ( !Gia_ObjIsBarBuf(pObj) ) {} else
+    for ( i = Gia_ManBufNum(p) ? 0 : p->nObjs; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )      if ( !Gia_ObjIsBuf(pObj) ) {} else
 #define Gia_ManForEachBufId( p, i )                                     \
-    for ( i = 0; (i < p->nObjs); i++ )                                     if ( !Gia_ObjIsBarBuf(Gia_ManObj(p, i)) ) {} else
+    for ( i = 0; (i < p->nObjs); i++ )                                     if ( !Gia_ObjIsBuf(Gia_ManObj(p, i)) ) {} else
 #define Gia_ManForEachAnd( p, pObj, i )                                 \
     for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )      if ( !Gia_ObjIsAnd(pObj) ) {} else
 #define Gia_ManForEachAndId( p, i )                                     \
diff --git a/src/aig/gia/giaBalAig.c b/src/aig/gia/giaBalAig.c
index 74ff84ba..dc9ffecd 100644
--- a/src/aig/gia/giaBalAig.c
+++ b/src/aig/gia/giaBalAig.c
@@ -227,6 +227,7 @@ void Gia_ManCreateGate( Gia_Man_t * pNew, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
 }
 int Gia_ManBalanceGate( Gia_Man_t * pNew, Gia_Obj_t * pObj, Vec_Int_t * vSuper, int * pLits, int nLits )
 {
+    assert( !Gia_ObjIsBuf(pObj) );
     Vec_IntClear( vSuper );
     if ( nLits == 1 )
         Vec_IntPush( vSuper, pLits[0] );
@@ -280,6 +281,7 @@ void Gia_ManBalance_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
     if ( ~pObj->Value )
         return;
     assert( Gia_ObjIsAnd(pObj) );
+    assert( !Gia_ObjIsBuf(pObj) );
     // handle MUX
     if ( Gia_ObjIsMux(p, pObj) )
     {
@@ -329,6 +331,12 @@ Gia_Man_t * Gia_ManBalanceInt( Gia_Man_t * p )
         pObj->Value = Gia_ManAppendCi( pNew );
     // create internal nodes
     Gia_ManHashStart( pNew );
+    Gia_ManForEachBuf( p, pObj, i )
+    {
+        Gia_ManBalance_rec( pNew, p, Gia_ObjFanin0(pObj) );
+        pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        Gia_ObjSetGateLevel( pNew, Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value)) );
+    }
     Gia_ManForEachCo( p, pObj, i )
     {
         Gia_ManBalance_rec( pNew, p, Gia_ObjFanin0(pObj) );
@@ -428,6 +436,11 @@ void Dam_ManCollectSets_rec( Dam_Man_t * p, int Id )
     pObj = Gia_ManObj(p->pGia, Id);
     if ( Gia_ObjIsCi(pObj) )
         return;
+    if ( Gia_ObjIsBuf(pObj) )
+    {
+        Dam_ManCollectSets_rec( p, Gia_ObjFaninId0(pObj, Id) );
+        return;
+    }
     if ( Gia_ObjIsMux(p->pGia, pObj) )
     {
         if ( pObj->fMark0 )
@@ -714,6 +727,12 @@ Gia_Man_t * Dam_ManMultiAig( Dam_Man_t * pMan )
     }
     // create internal nodes
     Gia_ManHashStart( pNew );
+    Gia_ManForEachBuf( p, pObj, i )
+    {
+        Dam_ManMultiAig_rec( pMan, pNew, p, Gia_ObjFanin0(pObj) );
+        pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        Gia_ObjSetGateLevel( pNew, Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value)) );
+    }
     Gia_ManForEachCo( p, pObj, i )
     {
         Dam_ManMultiAig_rec( pMan, pNew, p, Gia_ObjFanin0(pObj) );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 8454eca7..ddd47600 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -562,7 +562,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachObj1( p, pObj, i )
     {
-        if ( Gia_ObjIsBarBuf(pObj) )
+        if ( Gia_ObjIsBuf(pObj) )
             pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
         else if ( Gia_ObjIsAnd(pObj) )
         {
@@ -992,17 +992,18 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
     {
         if ( pObj->fMark0 )
         {
+            assert( Gia_ObjIsAnd(pObj) && !Gia_ObjIsBuf(pObj) );
             pObj->fMark0 = 0;
             continue;
         }
-        if ( Gia_ObjIsAnd(pObj) )
+        if ( Gia_ObjIsBuf(pObj) )
+            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        else if ( Gia_ObjIsAnd(pObj) )
         {
             if ( Gia_ObjIsXor(pObj) )
                 pObj->Value = Gia_ManAppendXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
             else if ( Gia_ObjIsMux(p, pObj) )
                 pObj->Value = Gia_ManAppendMuxReal( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) );
-            else if ( Gia_ObjIsBarBuf(pObj) )
-                pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
             else
                 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         }
@@ -1036,6 +1037,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
                 continue;
             if ( !~pRepr->Value )
                 continue;
+            assert( !Gia_ObjIsBuf(pObj) );
             if ( Abc_Lit2Var(pObj->Value) != Abc_Lit2Var(pRepr->Value) )
                 Gia_ObjSetRepr( pNew, Abc_Lit2Var(pObj->Value), Abc_Lit2Var(pRepr->Value) ); 
         }
@@ -1054,6 +1056,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
                 continue;
             if ( !~pSibl->Value )
                 continue;
+            assert( !Gia_ObjIsBuf(pObj) );
             assert( Abc_Lit2Var(pObj->Value) > Abc_Lit2Var(pSibl->Value) );
             pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(pSibl->Value);
         }
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index c28745e9..489c7739 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -729,6 +729,9 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash )
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachObj( p, pObj, i )
     {
+        //if ( Gia_ObjIsBuf(pObj) )
+        //    pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        //else 
         if ( Gia_ObjIsAnd(pObj) )
             pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         else if ( Gia_ObjIsCi(pObj) )
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index ed186c62..7d0047dc 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -1786,7 +1786,7 @@ int Gia_ManMappingVerify_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
     if ( Gia_ObjIsTravIdCurrent(p, pObj) )
         return 1;
     Gia_ObjSetTravIdCurrent(p, pObj);
-    if ( !Gia_ObjIsAnd(pObj) )
+    if ( !Gia_ObjIsAndNotBuf(pObj) )
         return 1;
     if ( !Gia_ObjIsLut(p, Gia_ObjId(p, pObj)) )
     {
@@ -1805,10 +1805,23 @@ void Gia_ManMappingVerify( Gia_Man_t * p )
     int i, Result = 1;
     assert( Gia_ManHasMapping(p) );
     Gia_ManIncrementTravId( p );
+    Gia_ManForEachBuf( p, pObj, i )
+    {
+        pFanin = Gia_ObjFanin0(pObj);
+        if ( !Gia_ObjIsAndNotBuf(pFanin) )
+            continue;
+        if ( !Gia_ObjIsLut(p, Gia_ObjId(p, pFanin)) )
+        {
+            Abc_Print( -1, "Gia_ManMappingVerify: CO driver %d does not have mapping.\n", Gia_ObjId(p, pFanin) );
+            Result = 0;
+            continue;
+        }
+        Result &= Gia_ManMappingVerify_rec( p, pFanin );
+    }
     Gia_ManForEachCo( p, pObj, i )
     {
         pFanin = Gia_ObjFanin0(pObj);
-        if ( !Gia_ObjIsAnd(pFanin) )
+        if ( !Gia_ObjIsAndNotBuf(pFanin) )
             continue;
         if ( !Gia_ObjIsLut(p, Gia_ObjId(p, pFanin)) )
         {
diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c
index e0434338..da767c52 100644
--- a/src/aig/gia/giaJf.c
+++ b/src/aig/gia/giaJf.c
@@ -251,7 +251,7 @@ float * Jf_ManInitRefs( Jf_Man_t * pMan )
     Gia_ManForEachAnd( p, pObj, i )
     {
         Gia_ObjRefFanin0Inc( p, pObj );
-        if ( Gia_ObjIsBarBuf(pObj) )
+        if ( Gia_ObjIsBuf(pObj) )
             continue;
         Gia_ObjRefFanin1Inc( p, pObj );
         if ( !Gia_ObjIsMuxType(pObj) )
@@ -311,7 +311,7 @@ void Jf_ManProfileClasses( Jf_Man_t * p )
     int i, iFunc, Total = 0, CostTotal = 0, Other = 0, CostOther = 0;
     printf( "DSD classes that appear in more than %.1f %% of mapped nodes:\n", 0.1 * p->pPars->nVerbLimit );
     Gia_ManForEachAnd( p->pGia, pObj, i )
-        if ( !Gia_ObjIsBarBuf(pObj) && Gia_ObjRefNumId(p->pGia, i) )
+        if ( !Gia_ObjIsBuf(pObj) && Gia_ObjRefNumId(p->pGia, i) )
         {
             iFunc = Jf_CutFuncClass( Jf_ObjCutBest(p, i) );
             assert( iFunc < 595 );
@@ -1100,7 +1100,7 @@ static inline void Jf_ObjAssignCut( Jf_Man_t * p, Gia_Obj_t * pObj )
 {
     int iObj = Gia_ObjId(p->pGia, pObj);
     int pClause[3] = { 1, Jf_CutSetAll(2, 0, 1), Jf_ObjLit(iObj, 0) }; // set function
-    assert( Gia_ObjIsCi(pObj) || Gia_ObjIsBarBuf(pObj) );
+    assert( Gia_ObjIsCi(pObj) || Gia_ObjIsBuf(pObj) );
     Vec_IntWriteEntry( &p->vCuts, iObj, Vec_SetAppend( &p->pMem, pClause, 3 ) );
 }
 static inline void Jf_ObjPropagateBuf( Jf_Man_t * p, Gia_Obj_t * pObj, int fReverse )
@@ -1108,7 +1108,7 @@ static inline void Jf_ObjPropagateBuf( Jf_Man_t * p, Gia_Obj_t * pObj, int fReve
     int iObj = Gia_ObjId( p->pGia, pObj );
     int iFanin = Gia_ObjFaninId0( pObj, iObj );
     assert( 0 );
-    assert( Gia_ObjIsBarBuf(pObj) );
+    assert( Gia_ObjIsBuf(pObj) );
     if ( fReverse )
         ABC_SWAP( int, iObj, iFanin );
     Vec_IntWriteEntry( &p->vArr,  iObj, Jf_ObjArr(p, iFanin) );
@@ -1247,9 +1247,9 @@ void Jf_ManComputeCuts( Jf_Man_t * p, int fEdge )
     }
     Gia_ManForEachObj( p->pGia, pObj, i )
     {
-        if ( Gia_ObjIsCi(pObj) || Gia_ObjIsBarBuf(pObj) )
+        if ( Gia_ObjIsCi(pObj) || Gia_ObjIsBuf(pObj) )
             Jf_ObjAssignCut( p, pObj );
-        if ( Gia_ObjIsBarBuf(pObj) )
+        if ( Gia_ObjIsBuf(pObj) )
             Jf_ObjPropagateBuf( p, pObj, 0 );
         else if ( Gia_ObjIsAnd(pObj) )
             Jf_ObjComputeCuts( p, pObj, fEdge );
@@ -1291,7 +1291,7 @@ int Jf_ManComputeDelay( Jf_Man_t * p, int fEval )
     if ( fEval )
     {
         Gia_ManForEachObj( p->pGia, pObj, i )
-            if ( Gia_ObjIsBarBuf(pObj) )
+            if ( Gia_ObjIsBuf(pObj) )
                 Jf_ObjPropagateBuf( p, pObj, 0 );
             else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
                 Vec_IntWriteEntry( &p->vArr, i, Jf_CutArr(p, Jf_ObjCutBest(p, i)) );
@@ -1314,7 +1314,7 @@ int Jf_ManComputeRefs( Jf_Man_t * p )
     p->pPars->Area = p->pPars->Edge = 0;
     Gia_ManForEachObjReverse( p->pGia, pObj, i )
     {
-        if ( Gia_ObjIsCo(pObj) || Gia_ObjIsBarBuf(pObj) )
+        if ( Gia_ObjIsCo(pObj) || Gia_ObjIsBuf(pObj) )
             Gia_ObjRefInc( p->pGia, Gia_ObjFanin0(pObj) );
         else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
         {
@@ -1381,7 +1381,7 @@ void Jf_ManPropagateFlow( Jf_Man_t * p, int fEdge )
     Gia_Obj_t * pObj; 
     int i;
     Gia_ManForEachObj( p->pGia, pObj, i )
-        if ( Gia_ObjIsBarBuf(pObj) )
+        if ( Gia_ObjIsBuf(pObj) )
             Jf_ObjPropagateBuf( p, pObj, 0 );
         else if ( Gia_ObjIsAnd(pObj) && Jf_ObjIsUnit(pObj) )
             Jf_ObjComputeBestCut( p, pObj, fEdge, 0 );
@@ -1393,7 +1393,7 @@ void Jf_ManPropagateEla( Jf_Man_t * p, int fEdge )
     int i, CostBef, CostAft;
     p->pPars->Area = p->pPars->Edge = p->pPars->Clause = 0;
     Gia_ManForEachObjReverse( p->pGia, pObj, i )
-        if ( Gia_ObjIsBarBuf(pObj) )
+        if ( Gia_ObjIsBuf(pObj) )
             Jf_ObjPropagateBuf( p, pObj, 1 );
         else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
         {
@@ -1457,7 +1457,7 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p )
     // iterate through nodes used in the mapping
     Gia_ManForEachAnd( p->pGia, pObj, i )
     {
-       if ( Gia_ObjIsBarBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
+       if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
             continue;
         pCut = Jf_ObjCutBest( p, i );
 //        printf( "Best cut of node %d:  ", i );  Jf_CutPrint(pCut);
@@ -1549,7 +1549,7 @@ void Jf_ManDeriveMapping( Jf_Man_t * p )
     Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 );
     Gia_ManForEachAnd( p->pGia, pObj, i )
     {
-        if ( Gia_ObjIsBarBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
+        if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
             continue;
         pCut = Jf_ObjCutBest( p, i );
         Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) );
@@ -1599,7 +1599,7 @@ Gia_Man_t * Jf_ManDeriveGia( Jf_Man_t * p )
     Gia_ManHashStart( pNew );
     Gia_ManForEachAnd( p->pGia, pObj, i )
     {
-       if ( Gia_ObjIsBarBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
+       if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
             continue;
         pCut = Jf_ObjCutBest( p, i );
 //        printf( "Best cut of node %d:  ", i );  Jf_CutPrint(pCut);
@@ -1713,6 +1713,7 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
 {
     Gia_Man_t * pNew = pGia;
     Jf_Man_t * p; int i;
+    assert( !Gia_ManBufNum(pGia) );
     assert( !pPars->fCutMin || !pPars->fFuncDsd || pPars->nLutSize <= 6 );
     if ( pPars->fGenCnf )
         pPars->fCutMin = 1, pPars->fFuncDsd = 1, pPars->fOptEdge = 0;
diff --git a/src/aig/gia/giaKf.c b/src/aig/gia/giaKf.c
index 87f9bfbe..caa88bfc 100644
--- a/src/aig/gia/giaKf.c
+++ b/src/aig/gia/giaKf.c
@@ -914,7 +914,7 @@ int Kf_ManComputeRefs( Kf_Man_t * p )
     p->pPars->Area = p->pPars->Edge = 0;
     Gia_ManForEachObjReverse( p->pGia, pObj, i )
     {
-        if ( Gia_ObjIsCo(pObj) || Gia_ObjIsBarBuf(pObj) )
+        if ( Gia_ObjIsCo(pObj) || Gia_ObjIsBuf(pObj) )
             Gia_ObjRefInc( p->pGia, Gia_ObjFanin0(pObj) );
         else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
         {
@@ -1270,7 +1270,7 @@ Gia_Man_t * Kf_ManDerive( Kf_Man_t * p )
     Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 );
     Gia_ManForEachAnd( p->pGia, pObj, i )
     {
-        if ( Gia_ObjIsBarBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
+        if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
             continue;
         pCut = Kf_ObjCutBest( p, i );
         Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) );
diff --git a/src/aig/gia/giaMuxes.c b/src/aig/gia/giaMuxes.c
index b59f51f7..972b9261 100644
--- a/src/aig/gia/giaMuxes.c
+++ b/src/aig/gia/giaMuxes.c
@@ -63,7 +63,7 @@ void Gia_ManPrintMuxStats( Gia_Man_t * p )
     int nAnds, nMuxes, nXors, nTotal;
     if ( p->pMuxes )
     {
-        nAnds  = Gia_ManAndNum(p)-Gia_ManXorNum(p)-Gia_ManMuxNum(p);
+        nAnds  = Gia_ManAndNotBufNum(p)-Gia_ManXorNum(p)-Gia_ManMuxNum(p);
         nXors  = Gia_ManXorNum(p);
         nMuxes = Gia_ManMuxNum(p);
         nTotal = nAnds + 3*nXors + 3*nMuxes;
@@ -71,14 +71,14 @@ void Gia_ManPrintMuxStats( Gia_Man_t * p )
     else 
     {
         Gia_ManCountMuxXor( p, &nMuxes, &nXors );
-        nAnds  = Gia_ManAndNum(p) - 3*nMuxes - 3*nXors;
-        nTotal = Gia_ManAndNum(p);
+        nAnds  = Gia_ManAndNotBufNum(p) - 3*nMuxes - 3*nXors;
+        nTotal = Gia_ManAndNotBufNum(p);
     }
     Abc_Print( 1, "stats:  " );
     Abc_Print( 1, "xor =%8d %6.2f %%   ", nXors,  300.0*nXors/nTotal );
     Abc_Print( 1, "mux =%8d %6.2f %%   ", nMuxes, 300.0*nMuxes/nTotal );
     Abc_Print( 1, "and =%8d %6.2f %%   ", nAnds,  100.0*nAnds/nTotal );
-    Abc_Print( 1, "obj =%8d  ", Gia_ManAndNum(p) );
+    Abc_Print( 1, "obj =%8d  ", Gia_ManAndNotBufNum(p) );
     fflush( stdout );
 }
 
@@ -117,7 +117,7 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit )
             pObj->Value = Gia_ManAppendCi( pNew );
         else if ( Gia_ObjIsCo(pObj) )
             pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-        else if ( Gia_ObjIsBarBuf(pObj) )
+        else if ( Gia_ObjIsBuf(pObj) )
             pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
         else if ( !Gia_ObjIsMuxType(pObj) || Gia_ObjSibl(p, Gia_ObjFaninId0(pObj, i)) || Gia_ObjSibl(p, Gia_ObjFaninId1(pObj, i)) )
             pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -174,7 +174,7 @@ Gia_Man_t * Gia_ManDupNoMuxes( Gia_Man_t * p )
             pObj->Value = Gia_ManAppendCi( pNew );
         else if ( Gia_ObjIsCo(pObj) )
             pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-        else if ( Gia_ObjIsBarBuf(pObj) )
+        else if ( Gia_ObjIsBuf(pObj) )
             pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
         else if ( Gia_ObjIsMuxId(p, i) )
             pObj->Value = Gia_ManHashMux( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) );
diff --git a/src/aig/gia/giaScl.c b/src/aig/gia/giaScl.c
index 3aaf91dc..70bc9fe8 100644
--- a/src/aig/gia/giaScl.c
+++ b/src/aig/gia/giaScl.c
@@ -33,7 +33,7 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Marks unreachable internal nodes and returned their number.]
+  Synopsis    [Marks unreachable internal nodes and returns their number.]
 
   Description []
                
@@ -50,30 +50,21 @@ int Gia_ManCombMarkUsed_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
         return 0;
     pObj->fMark0 = 0;
     assert( Gia_ObjIsAnd(pObj) );
+    assert( !Gia_ObjIsBuf(pObj) );
     return 1 + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin0(pObj) )
              + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) )
              + (p->pNexts ? Gia_ManCombMarkUsed_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pObj)) ) : 0)
              + (p->pSibls ? Gia_ManCombMarkUsed_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)) ) : 0)
              + (p->pMuxes ? Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin2(p, pObj) ) : 0);
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Marks unreachable internal nodes and returned their number.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Gia_ManCombMarkUsed( Gia_Man_t * p )
 {
     Gia_Obj_t * pObj;
     int i, nNodes = 0;
     Gia_ManForEachObj( p, pObj, i )
-        pObj->fMark0 = Gia_ObjIsAnd(pObj);
+        pObj->fMark0 = Gia_ObjIsAnd(pObj) && !Gia_ObjIsBuf(pObj);
+    Gia_ManForEachBuf( p, pObj, i )
+        nNodes += Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin0(pObj) );
     Gia_ManForEachCo( p, pObj, i )
         nNodes += Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin0(pObj) );
     return nNodes;
diff --git a/src/aig/gia/giaScript.c b/src/aig/gia/giaScript.c
index f89e1404..b4408226 100644
--- a/src/aig/gia/giaScript.c
+++ b/src/aig/gia/giaScript.c
@@ -285,7 +285,7 @@ Gia_Man_t * Gia_ManDupFromBarBufs( Gia_Man_t * p )
         Vec_IntPush( vBufObjs, Gia_ManAppendCi(pNew) );
     Gia_ManForEachAnd( p, pObj, i )
     {
-        if ( Gia_ObjIsBarBuf(pObj) )
+        if ( Gia_ObjIsBuf(pObj) )
         {
             pObj->Value = Vec_IntEntry( vBufObjs, k );
             Vec_IntWriteEntry( vBufObjs, k++, Gia_ObjFanin0Copy(pObj) );
@@ -306,8 +306,9 @@ Gia_Man_t * Gia_ManDupToBarBufs( Gia_Man_t * p, int nBarBufs )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
-    int i, nPiReal = Gia_ManCiNum(p) - nBarBufs;
-    int k, nPoReal = Gia_ManCoNum(p) - nBarBufs;
+    int nPiReal = Gia_ManCiNum(p) - nBarBufs;
+    int nPoReal = Gia_ManCoNum(p) - nBarBufs;
+    int i, k = 0;
     assert( Gia_ManBufNum(p) == 0 );
     assert( Gia_ManRegNum(p) == 0 );
     assert( Gia_ManHasChoices(p) );
@@ -320,22 +321,25 @@ Gia_Man_t * Gia_ManDupToBarBufs( Gia_Man_t * p, int nBarBufs )
     Gia_ManConst0(p)->Value = 0;
     for ( i = 0; i < nPiReal; i++ )
         Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
-    k = 0;
     Gia_ManForEachAnd( p, pObj, i )
     {
-        while ( ~Gia_ObjFanin0Copy(Gia_ManCo(p, k)) )
-        {
-            Gia_ManCi(p, nPiReal + k)->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, k)) );
-            k++;            
-        }
+        for ( ; k < nBarBufs; k++ )
+            if ( ~Gia_ObjFanin0Copy(Gia_ManCo(p, k)) )
+                Gia_ManCi(p, nPiReal + k)->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, k)) );
         pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
             pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value);  
     }
+    for ( ; k < nBarBufs; k++ )
+        if ( ~Gia_ObjFanin0Copy(Gia_ManCo(p, k)) )
+            Gia_ManCi(p, nPiReal + k)->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, k)) );
     assert( k == nBarBufs );
     for ( i = 0; i < nPoReal; i++ )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p, nBarBufs+i)) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    assert( Gia_ManBufNum(pNew) == nBarBufs );
+    assert( Gia_ManCiNum(pNew) == nPiReal );
+    assert( Gia_ManCoNum(pNew) == nPoReal );
     return pNew;
 }
 
@@ -407,22 +411,27 @@ Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * pInit, void * pPars0, int nLutSize )
         pGia1 = (Gia_Man_t *)Dsm_ManDeriveGia( pTemp = pGia1, 0 );
         Gia_ManStop( pTemp );
     }
-    // perform LUT balancing
-    pGia2 = Gia_ManLutBalance( pGia1, nLutSize, 1, 1, 1, 0 );
     // perform balancing
-    pGia2 = Gia_ManAreaBalance( pTemp = pGia2, 0, ABC_INFINITY, 0, 0 );
+    if ( Gia_ManBufNum(pGia1) )
+        pGia2 = Gia_ManAreaBalance( pGia1, 0, ABC_INFINITY, 0, 0 );
+    else
+    {
+        pGia2 = Gia_ManLutBalance( pGia1, nLutSize, 1, 1, 1, 0 );
+        pGia2 = Gia_ManAreaBalance( pTemp = pGia2, 0, ABC_INFINITY, 0, 0 );
+        Gia_ManStop( pTemp );
+    }
     if ( fVerbose )     Gia_ManPrintStats( pGia2, NULL );
-    Gia_ManStop( pTemp );
     // perform mapping
     pGia2 = Lf_ManPerformMapping( pTemp = pGia2, pPars );
     if ( fVerbose )     Gia_ManPrintStats( pGia2, NULL );
     if ( pTemp != pGia2 )
         Gia_ManStop( pTemp );
     // perform balancing
-    if ( pParsDch->fLightSynth )
+    if ( pParsDch->fLightSynth || Gia_ManBufNum(pGia2) )
         pGia3 = Gia_ManAreaBalance( pGia2, 0, ABC_INFINITY, 0, 0 );
     else
     {
+        assert( Gia_ManBufNum(pGia2) == 0 );
         pGia2 = Gia_ManAreaBalance( pTemp = pGia2, 0, ABC_INFINITY, 0, 0 );
         if ( fVerbose )     Gia_ManPrintStats( pGia2, NULL );
         Gia_ManStop( pTemp );
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 3704867b..bd77847b 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -167,7 +167,10 @@ Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
         printf( "Warning: Shuffled CI order to be correct sequential AIG.\n" );
     }
     Gia_ManForEachAnd( p, pObj, i )
-        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( Gia_ObjIsBuf(pObj) )
+            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        else 
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
@@ -254,6 +257,13 @@ int Gia_ManOrderWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNod
         return 1;
     }
     assert( Gia_ObjIsAnd(pObj) );
+    if ( Gia_ObjIsBuf(pObj) )
+    {
+        if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) )
+            return 1;
+        Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+        return 0;
+    }
     if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
         if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)), vNodes ) )
             return 1;
@@ -366,6 +376,7 @@ Gia_Man_t * Gia_ManDupUnnormalize( Gia_Man_t * p )
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
     int i;
+    assert( !Gia_ManBufNum(p) );
     vNodes = Gia_ManOrderWithBoxes( p );
     if ( vNodes == NULL )
         return NULL;
@@ -377,7 +388,9 @@ Gia_Man_t * Gia_ManDupUnnormalize( Gia_Man_t * p )
         pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) );
     Gia_ManForEachObjVec( vNodes, p, pObj, i )
     {
-        if ( Gia_ObjIsAnd(pObj) )
+        if ( Gia_ObjIsBuf(pObj) )
+            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        else if ( Gia_ObjIsAnd(pObj) )
         {
             pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
             if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
@@ -460,6 +473,7 @@ int Gia_ManLevelWithBoxes( Gia_Man_t * p )
     Gia_Obj_t * pObj, * pObjIn;
     int i, k, j, curCi, curCo, LevelMax;
     assert( Gia_ManRegNum(p) == 0 );
+    assert( Gia_ManBufNum(p) == 0 );
     // copy const and real PIs
     Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
     Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 69903830..ae32b91e 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -510,7 +510,9 @@ int Gia_ManLevelNum( Gia_Man_t * p )
     p->nLevels = 0;
     Gia_ManForEachObj( p, pObj, i )
     {
-        if ( Gia_ObjIsAnd(pObj) )
+        if ( Gia_ObjIsBuf(pObj) )
+            Gia_ObjSetBufLevel( p, pObj );
+        else if ( Gia_ObjIsAnd(pObj) )
             Gia_ObjSetGateLevel( p, pObj );
         else if ( Gia_ObjIsCo(pObj) )
             Gia_ObjSetCoLevel( p, pObj );
@@ -610,6 +612,10 @@ Vec_Int_t * Gia_ManReverseLevel( Gia_Man_t * p )
             Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId0(pObj, i), LevelR + 2 );
             Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId1(pObj, i), LevelR + 2 );
         }
+        else if ( Gia_ObjIsBuf(pObj) )
+        {
+            Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId0(pObj, i), LevelR );
+        }
         else
         {
             Vec_IntUpdateEntry( vLevelRev, Gia_ObjFaninId0(pObj, i), LevelR + 1 );
@@ -882,7 +888,7 @@ int Gia_ObjIsMuxType( Gia_Obj_t * pNode )
     // check that the node is regular
     assert( !Gia_IsComplement(pNode) );
     // if the node is not AND, this is not MUX
-    if ( !Gia_ObjIsAnd(pNode) || Gia_ObjIsBarBuf(pNode) )
+    if ( !Gia_ObjIsAnd(pNode) || Gia_ObjIsBuf(pNode) )
         return 0;
     // if the children are not complemented, this is not MUX
     if ( !Gia_ObjFaninC0(pNode) || !Gia_ObjFaninC1(pNode) )
@@ -916,7 +922,7 @@ int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** pp
 {
     Gia_Obj_t * p0, * p1;
     assert( !Gia_IsComplement(pObj) );
-    if ( !Gia_ObjIsAnd(pObj) || Gia_ObjIsBarBuf(pObj) )
+    if ( !Gia_ObjIsAnd(pObj) || Gia_ObjIsBuf(pObj) )
         return 0;
     assert( Gia_ObjIsAnd(pObj) );
     p0 = Gia_ObjChild0(pObj);
@@ -1273,7 +1279,7 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
         printf( "RO( %4d%s )", Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)), (Gia_ObjFaninC0(Gia_ObjRoToRi(p, pObj))? "\'" : " ") );
     else if ( Gia_ObjIsCo(pObj) )
         printf( "RI( %4d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
-//    else if ( Gia_ObjIsBarBuf(pObj) )
+//    else if ( Gia_ObjIsBuf(pObj) )
 //        printf( "BUF( %d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
     else if ( Gia_ObjIsXor(pObj) )
         printf( "XOR( %4d%s, %4d%s )", 
@@ -1308,7 +1314,7 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
             printf( "Node %4d : ", Gia_ObjId(pFanout) );
             if ( Gia_ObjIsPo(pFanout) )
                 printf( "PO( %4d%s )", Gia_ObjFanin0(pFanout)->Id, (Gia_ObjFaninC0(pFanout)? "\'" : " ") );
-            else if ( Gia_ObjIsBarBuf(pFanout) )
+            else if ( Gia_ObjIsBuf(pFanout) )
                 printf( "BUF( %d%s )", Gia_ObjFanin0(pFanout)->Id, (Gia_ObjFaninC0(pFanout)? "\'" : " ") );
             else
                 printf( "AND( %4d%s, %4d%s )",