Updating code to support barrier buffers.

8 files changed, 62 insertions, 13 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 2a1e7d7d..db7d380d 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -107,6 +107,7 @@ struct Aig_Man_t_
     int              nTruePos;       // the number of true primary outputs
     int              nAsserts;       // the number of asserts among POs (asserts are first POs)
     int              nConstrs;       // the number of constraints (model checking only)
+    int              nBarBufs;       // the number of barrier buffers
     // AIG node counters
     int              nObjs[AIG_OBJ_VOID];// the number of objects by type
     int              nDeleted;       // the number of deleted objects
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 67b71d61..86ad2104 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -55,6 +55,7 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
@@ -192,6 +193,7 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
@@ -283,6 +285,7 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
@@ -351,6 +354,7 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
@@ -416,6 +420,7 @@ Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p )
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     // create the PIs
     Aig_ManCleanData( p );
     // duplicate internal nodes
@@ -466,6 +471,7 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
@@ -565,6 +571,7 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // duplicate representation of choice nodes
@@ -695,6 +702,7 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // duplicate representation of choice nodes
@@ -764,6 +772,7 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // duplicate representation of choice nodes
@@ -918,6 +927,7 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the const and primary inputs
@@ -992,6 +1002,7 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the const and primary inputs
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index f43b7edd..0a9ebd4c 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -274,6 +274,7 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the const and primary inputs
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 5dc79d7f..731fa333 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -54,6 +54,7 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     assert( p->vFlopNums == NULL || Vec_IntSize(p->vFlopNums) == p->nRegs );
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 93e0d02b..f5e6a694 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -508,7 +508,7 @@ static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_At
 #define Abc_NtkForEachCo( pNtk, pCo, i )                                                           \
     for ( i = 0; (i < Abc_NtkCoNum(pNtk)) && (((pCo) = Abc_NtkCo(pNtk, i)), 1); i++ )
 #define Abc_NtkForEachLiPo( pNtk, pCo, i )                                                         \
-for ( i = 0; (i < Abc_NtkCoNum(pNtk)) && (((pCo) = Abc_NtkCo(pNtk, i < pNtk->nBarBufs ? Abc_NtkCoNum(pNtk) - pNtk->nBarBufs + i : i - pNtk->nBarBufs)), 1); i++ )
+    for ( i = 0; (i < Abc_NtkCoNum(pNtk)) && (((pCo) = Abc_NtkCo(pNtk, i < pNtk->nBarBufs ? Abc_NtkCoNum(pNtk) - pNtk->nBarBufs + i : i - pNtk->nBarBufs)), 1); i++ )
 // fanin and fanouts
 #define Abc_ObjForEachFanin( pObj, pFanin, i )                                                     \
     for ( i = 0; (i < Abc_ObjFaninNum(pObj)) && (((pFanin) = Abc_ObjFanin(pObj, i)), 1); i++ )
diff --git a/src/base/abc/abcBarBuf.c b/src/base/abc/abcBarBuf.c
index 555b1240..927c718f 100644
--- a/src/base/abc/abcBarBuf.c
+++ b/src/base/abc/abcBarBuf.c
@@ -256,7 +256,7 @@ Abc_Ntk_t * Abc_NtkFromBarBufs( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkNew, * pTemp;
     Vec_Ptr_t * vLiMaps, * vLoMaps;
     Abc_Obj_t * pObj, * pLiMap, * pLoMap;
-    int i;
+    int i, k;
     assert( pNtkBase->pDesign != NULL );
     assert( Abc_NtkIsNetlist(pNtk) );
     assert( Abc_NtkIsNetlist(pNtkBase) );
@@ -271,8 +271,8 @@ Abc_Ntk_t * Abc_NtkFromBarBufs( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtk )
     Vec_PtrForEachEntry( Abc_Ntk_t *, pNtkBase->pDesign->vModules, pTemp, i )
         pTemp->pCopy = Abc_NtkStartFrom( pTemp, pNtk->ntkType, pNtk->ntkFunc );
     // update box models
-    Vec_PtrForEachEntry( Abc_Ntk_t *, pNtkBase->pDesign->vTops, pTemp, i )
-        Abc_NtkForEachBox( pTemp, pObj, i )
+    Vec_PtrForEachEntry( Abc_Ntk_t *, pNtkBase->pDesign->vModules, pTemp, i )
+        Abc_NtkForEachBox( pTemp, pObj, k )
             if ( Abc_ObjIsWhitebox(pObj) || Abc_ObjIsBlackbox(pObj) )
                 pObj->pCopy->pData = Abc_ObjModel(pObj)->pCopy;
     // create the design
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 22d4fdff..d5fdd1de 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -158,6 +158,7 @@ Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap )
     // create network
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
     pMan->nConstrs = pNtk->nConstrs;
+    pMan->nBarBufs = pNtk->nBarBufs;
     pMan->pName = Extra_UtilStrsav( pNtk->pName );
 
     // transfer the pointers to the basic nodes
@@ -277,6 +278,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
     pMan->fCatchExor = fExors;
     pMan->nConstrs = pNtk->nConstrs;
+    pMan->nBarBufs = pNtk->nBarBufs;
 
     pMan->pName = Extra_UtilStrsav( pNtk->pName );
     // transfer the pointers to the basic nodes
@@ -359,6 +361,7 @@ Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk )
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
     pMan->pName = Extra_UtilStrsav( pNtk->pName );
     pMan->nConstrs = pNtk->nConstrs;
+    pMan->nBarBufs = pNtk->nBarBufs;
     if ( Abc_NtkGetChoiceNum(pNtk) )
     {
         pMan->pEquivs = ABC_ALLOC( Aig_Obj_t *, Abc_NtkObjNum(pNtk) );
@@ -473,6 +476,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     // perform strashing
     pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
     pNtkNew->nConstrs = pMan->nConstrs;
+    pNtkNew->nBarBufs = pMan->nBarBufs;
     // consider the case of target enlargement
     if ( Abc_NtkCiNum(pNtkNew) < Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) )
     {
@@ -592,6 +596,7 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
     // perform strashing
     pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkNew->nConstrs = pMan->nConstrs;
+    pNtkNew->nBarBufs = pMan->nBarBufs;
     // duplicate the name and the spec
 //    pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
 //    pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
@@ -821,6 +826,7 @@ Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld )
     // perform strashing
     pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkNew->nConstrs = pMan->nConstrs;
+    pNtkNew->nBarBufs = pMan->nBarBufs;
     // duplicate the name and the spec
 //    pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
 //    pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
@@ -964,6 +970,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     // perform strashing
     pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
     pNtkNew->nConstrs = pMan->nConstrs;
+    pNtkNew->nBarBufs = pMan->nBarBufs;
     // transfer the pointers to the basic nodes
     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     Aig_ManForEachCi( pMan, pObj, i )
diff --git a/src/opt/dar/darBalance.c b/src/opt/dar/darBalance.c
index 5f6fb93c..4c77ab56 100644
--- a/src/opt/dar/darBalance.c
+++ b/src/opt/dar/darBalance.c
@@ -562,6 +562,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
+    pNew->nBarBufs = p->nBarBufs;
     pNew->Time2Quit = p->Time2Quit;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -619,18 +620,45 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
             pObjNew->Level = pObj->Level;
             pObj->pData = pObjNew;
         }
-        Aig_ManForEachCo( p, pObj, i )
+        if ( p->nBarBufs == 0 )
         {
-            pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-            pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
-            if ( pObjNew == NULL )
+            Aig_ManForEachCo( p, pObj, i )
             {
-                Vec_VecFree( vStore );
-                Aig_ManStop( pNew );
-                return NULL;
+                pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+                pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+                if ( pObjNew == NULL )
+                {
+                    Vec_VecFree( vStore );
+                    Aig_ManStop( pNew );
+                    return NULL;
+                }
+                pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+                pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
+            }
+        }
+        else
+        {
+            Vec_Ptr_t * vLits = Vec_PtrStart( Aig_ManCoNum(p) );
+            Aig_ManForEachCo( p, pObj, i )
+            {
+                int k = i < p->nBarBufs ? Aig_ManCoNum(p) - p->nBarBufs + i : i - p->nBarBufs;
+                pObj = Aig_ManCo( p, k );
+                pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+                pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+                if ( pObjNew == NULL )
+                {
+                    Vec_VecFree( vStore );
+                    Aig_ManStop( pNew );
+                    return NULL;
+                }
+                pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+                Vec_PtrWriteEntry( vLits, k, pObjNew );
+                if ( i < p->nBarBufs )
+                    Aig_ManCi(pNew, Aig_ManCiNum(p) - p->nBarBufs + i)->Level = Aig_Regular(pObjNew)->Level;
             }
-            pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
-            pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
+            Aig_ManForEachCo( p, pObj, i )
+                Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vLits, i) );
+            Vec_PtrFree(vLits);
         }
     }
     Vec_VecFree( vStore );