Several improvements to CBA data-structure.

7 files changed, 552 insertions, 16 deletions

diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index 716eaf43..8e910c00 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -61,6 +61,7 @@ typedef enum {
     CBA_BOX_XOR,  
     CBA_BOX_XNOR, 
     CBA_BOX_SHARP,
+    CBA_BOX_SHARPL,
     CBA_BOX_MUX,  
     CBA_BOX_MAJ,  
 
@@ -71,6 +72,13 @@ typedef enum {
     CBA_BOX_RXOR,
     CBA_BOX_RXNOR,
 
+    CBA_BOX_LAND,
+    CBA_BOX_LNAND,
+    CBA_BOX_LOR,
+    CBA_BOX_LNOR,
+    CBA_BOX_LXOR,
+    CBA_BOX_LXNOR,
+
     CBA_BOX_NMUX,  
     CBA_BOX_SEL,
     CBA_BOX_PSEL,
@@ -110,6 +118,7 @@ typedef enum {
     CBA_BOX_RAMR,
     CBA_BOX_RAMW,
     CBA_BOX_RAMWC,
+    CBA_BOX_RAMBOX,
 
     CBA_BOX_LATCH,
     CBA_BOX_LATCHRS,
@@ -151,9 +160,11 @@ struct Cba_Ntk_t_
     Vec_Int_t    vFanin;   // fanin
     Vec_Int_t    vIndex;   // index
     Vec_Int_t    vName;    // original NameId or InstId
+    Vec_Int_t    vFanout;  // fanout
     Vec_Int_t    vCopy;    // copy
     // other
     Vec_Int_t    vArray;
+    Vec_Int_t    vArray2;
 };
 
 // design
@@ -233,11 +244,14 @@ static inline int            Cba_NtkInfoIndex( Cba_Ntk_t * p, int i, int j ) { i
 static inline void           Cba_NtkAddInfo( Cba_Ntk_t * p,int i,int b,int e){ Vec_IntPush(&p->vInfo, i); Vec_IntPushTwo(&p->vInfo, b, e);                                 }
 static inline void           Cba_NtkSetInfoName( Cba_Ntk_t * p, int i, int n){ Vec_IntWriteEntry( &p->vInfo, 3*i, n );                                                     }
 
-static inline void           Cba_NtkStartNames( Cba_Ntk_t * p )              { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vName,  Cba_NtkObjNumAlloc(p),  0);          }
-static inline void           Cba_NtkStartCopies( Cba_Ntk_t * p )             { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vCopy,  Cba_NtkObjNumAlloc(p), -1);          }
+static inline void           Cba_NtkStartNames( Cba_Ntk_t * p )              { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vName,   Cba_NtkObjNumAlloc(p),  0);         }
+static inline void           Cba_NtkStartFanouts( Cba_Ntk_t * p )            { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vFanout, Cba_NtkObjNumAlloc(p),  0);         }
+static inline void           Cba_NtkStartCopies( Cba_Ntk_t * p )             { assert(Cba_NtkObjNumAlloc(p)); Vec_IntFill(&p->vCopy,   Cba_NtkObjNumAlloc(p), -1);         }
 static inline void           Cba_NtkFreeNames( Cba_Ntk_t * p )               { Vec_IntErase(&p->vName);                                                                    }
+static inline void           Cba_NtkFreeFanouts( Cba_Ntk_t * p )             { Vec_IntErase(&p->vFanout);                                                                  }
 static inline void           Cba_NtkFreeCopies( Cba_Ntk_t * p )              { Vec_IntErase(&p->vCopy);                                                                    }
 static inline int            Cba_NtkHasNames( Cba_Ntk_t * p )                { return p->vName.pArray != NULL;                                                             }
+static inline int            Cba_NtkHasFanouts( Cba_Ntk_t * p )              { return p->vFanout.pArray != NULL;                                                           }
 static inline int            Cba_NtkHasCopies( Cba_Ntk_t * p )               { return p->vCopy.pArray != NULL;                                                             }
 
 static inline int            Cba_TypeIsBox( Cba_ObjType_t Type )             { return Type >= CBA_OBJ_BOX && Type < CBA_BOX_UNKNOWN;                                       }
@@ -260,17 +274,21 @@ static inline int            Cba_ObjIsCio( Cba_Ntk_t * p, int i )            { r
 
 static inline int            Cba_ObjFanin( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsCo(p, i)); return Vec_IntEntry(&p->vFanin, i);                              }
 static inline int            Cba_ObjIndex( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsCio(p, i)); return Vec_IntEntry(&p->vIndex, i);                             }
-static inline int            Cba_ObjFaninTwo( Cba_Ntk_t * p, int i )         { return Cba_ObjFanin(p, Cba_ObjFanin(p, i));                                                 }
 static inline int            Cba_ObjNameInt( Cba_Ntk_t * p, int i )          { assert(!Cba_ObjIsCo(p, i)); return Vec_IntEntry(&p->vName, i);                              }
 static inline int            Cba_ObjName( Cba_Ntk_t * p, int i )             { return Cba_ObjIsCo(p, i) ? Cba_ObjNameInt(p, Cba_ObjFanin(p,i)) : Cba_ObjNameInt(p, i);     }
 static inline Cba_NameType_t Cba_ObjNameType( Cba_Ntk_t * p, int i )         { assert(!Cba_ObjIsCo(p, i)); return Cba_NameType( Cba_ObjName(p, i) );                       }
 static inline int            Cba_ObjNameId( Cba_Ntk_t * p, int i )           { assert(!Cba_ObjIsCo(p, i)); return Abc_Lit2Var2( Cba_ObjName(p, i) );                       }
 static inline char *         Cba_ObjNameStr( Cba_Ntk_t * p, int i )          { assert(Cba_ObjNameType(p, i) <= CBA_NAME_WORD); return Cba_NtkStr(p, Cba_ObjNameId(p, i));  }
 static inline int            Cba_ObjCopy( Cba_Ntk_t * p, int i )             { return Vec_IntEntry(&p->vCopy, i);                                                          }
-static inline void           Cba_ObjSetFanin( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjFanin(p, i) == -1 && Cba_ObjIsCo(p, i)); Vec_IntWriteEntry( &p->vFanin, i, x);}
-static inline void           Cba_ObjSetIndex( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjIndex(p, i) == -1); Vec_IntWriteEntry( &p->vIndex, i, x );                    }
-static inline void           Cba_ObjSetName( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjName(p, i) == 0 && !Cba_ObjIsCo(p, i)); Vec_IntWriteEntry( &p->vName, i, x ); }
-static inline void           Cba_ObjSetCopy( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjCopy(p, i) == -1);  Vec_IntWriteEntry( &p->vCopy,  i, x );                    }
+static inline int            Cba_ObjFanout( Cba_Ntk_t * p, int i )           { assert(Cba_ObjIsCi(p, i)); return Vec_IntEntry(&p->vFanout, i);                             }
+static inline int            Cba_ObjNextFanout( Cba_Ntk_t * p, int i )       { assert(Cba_ObjIsCo(p, i)); return Vec_IntEntry(&p->vFanout, i);                             }
+static inline void           Cba_ObjSetFanout( Cba_Ntk_t * p, int i, int x ) { assert(Cba_ObjIsCi(p, i)); Vec_IntSetEntry(&p->vFanout, i, x);                              }
+static inline void           Cba_ObjSetNextFanout( Cba_Ntk_t * p,int i,int x){ assert(Cba_ObjIsCo(p, i)); Vec_IntSetEntry(&p->vFanout, i, x);                              }
+static inline void           Cba_ObjCleanFanin( Cba_Ntk_t * p, int i )       { assert(Cba_ObjFanin(p, i) >= 0 && Cba_ObjIsCo(p, i)); Vec_IntSetEntry( &p->vFanin, i, -1);  }
+static inline void           Cba_ObjSetFanin( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjFanin(p, i) == -1 && Cba_ObjIsCo(p, i)); Vec_IntSetEntry( &p->vFanin, i, x);  }
+static inline void           Cba_ObjSetIndex( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjIndex(p, i) == -1); Vec_IntSetEntry( &p->vIndex, i, x );                      }
+static inline void           Cba_ObjSetName( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjName(p, i) == 0 && !Cba_ObjIsCo(p, i)); Vec_IntSetEntry( &p->vName, i, x );   }
+static inline void           Cba_ObjSetCopy( Cba_Ntk_t * p, int i, int x )   { assert(Cba_ObjCopy(p, i) == -1);  Vec_IntSetEntry( &p->vCopy,  i, x );                      }
 
 static inline int            Cba_BoxBiNum( Cba_Ntk_t * p, int i )            { int s = i-1; assert(Cba_ObjIsBox(p, i)); while (--i >= 0               && Cba_ObjIsBi(p, i)); return s - i;  }
 static inline int            Cba_BoxBoNum( Cba_Ntk_t * p, int i )            { int s = i+1; assert(Cba_ObjIsBox(p, i)); while (++i < Cba_NtkObjNum(p) && Cba_ObjIsBo(p, i)); return i - s;  }
@@ -280,9 +298,10 @@ static inline int            Cba_BoxBo( Cba_Ntk_t * p, int b, int i )        { a
 static inline int            Cba_BoxBiBox( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsBi(p, i)); return i + 1 + Cba_ObjIndex(p, i);                               }
 static inline int            Cba_BoxBoBox( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsBo(p, i)); return i - 1 - Cba_ObjIndex(p, i);                               }
 static inline int            Cba_BoxFanin( Cba_Ntk_t * p, int b, int i )     { return Cba_ObjFanin(p, Cba_BoxBi(p, b, i));                                                 }
+static inline int            Cba_BoxFaninBox( Cba_Ntk_t * p, int b, int i )  { return Cba_BoxBoBox(p, Cba_BoxFanin(p, b, i));                                              }
 
 static inline int            Cba_BoxNtkId( Cba_Ntk_t * p, int i )            { assert(Cba_ObjIsBox(p, i)); return Vec_IntEntry(&p->vFanin, i);                             }
-static inline void           Cba_BoxSetNtkId( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjIsBox(p, i) && Cba_ManNtkIsOk(p->pDesign, x)); Vec_IntWriteEntry(&p->vFanin, i, x);            }
+static inline void           Cba_BoxSetNtkId( Cba_Ntk_t * p, int i, int x )  { assert(Cba_ObjIsBox(p, i)&&Cba_ManNtkIsOk(p->pDesign, x));Vec_IntSetEntry(&p->vFanin, i, x);}
 static inline int            Cba_BoxBiNtkId( Cba_Ntk_t * p, int i )          { assert(Cba_ObjIsBi(p, i)); return Cba_BoxNtkId(p, Cba_BoxBiBox(p, i));                      }
 static inline int            Cba_BoxBoNtkId( Cba_Ntk_t * p, int i )          { assert(Cba_ObjIsBo(p, i)); return Cba_BoxNtkId(p, Cba_BoxBoBox(p, i));                      }
 static inline Cba_Ntk_t *    Cba_BoxNtk( Cba_Ntk_t * p, int i )              { return Cba_ManNtk( p->pDesign, Cba_BoxNtkId(p, i) );                                        }
@@ -331,9 +350,9 @@ static inline int Cba_NtkNameRanges( char * pName, int * pRanges, char * pSymbs
     pSymbs[nSigs] = Symb, pRanges[nSigs++] = Num;
     return nSigs;
 }
-static inline void Cba_NtkReadRangesPrim( char * pName, Vec_Int_t * vRanges, int fPo )
+static inline int Cba_NtkReadRangesPrim( char * pName, Vec_Int_t * vRanges, int fPo )
 {
-    char * pTemp; int Last, Num = 0;
+    char * pTemp; int Last, Num = 0, Count = 0;
     assert( !strncmp(pName, "ABC", 3) );
     for ( pTemp = pName; *pTemp && !Cba_CharIsDigit(*pTemp); pTemp++ );
     assert( Cba_CharIsDigit(*pTemp) );
@@ -343,17 +362,18 @@ static inline void Cba_NtkReadRangesPrim( char * pName, Vec_Int_t * vRanges, int
         if ( Cba_CharIsDigit(*pTemp) )
             Num = 10 * Num + *pTemp - '0';
         else
-            Vec_IntPush( vRanges, Num ), Num = 0;
+            Vec_IntPush( vRanges, Num ), Count += Num, Num = 0;
     }
     assert( Num > 0 );
-    Vec_IntPush( vRanges, Num );
+    Vec_IntPush( vRanges, Num );  Count += Num;
     Last = Vec_IntPop(vRanges);
     if ( !fPo )
-        return;
+        return Count;
     if ( !strncmp(pName, "ABCADD", 6) )
         Vec_IntFillTwo( vRanges, 2, Last - 1, 1 );
     else
         Vec_IntFill( vRanges, 1, Last );
+    return Vec_IntSum(vRanges);
 }
 static inline int Cba_NtkReadRangesUser( Cba_Ntk_t * p, Vec_Int_t * vRanges, int fPo )
 {
@@ -459,6 +479,13 @@ static inline int Cba_ObjGetRange( Cba_Ntk_t * p, int iObj, int * pBeg, int * pE
 
 #define Cba_BoxForEachFanin( p, iBox, iFanin, i )                         \
     for ( i = 0; iBox - 1 - i >= 0 && Cba_ObjIsBi(p, iBox - 1 - i) && (((iFanin) = Cba_BoxFanin(p, iBox, i)), 1); i++ )
+#define Cba_BoxForEachFaninBox( p, iBox, iFanin, i )                      \
+    for ( i = 0; iBox - 1 - i >= 0 && Cba_ObjIsBi(p, iBox - 1 - i) && (((iFanin) = Cba_BoxFaninBox(p, iBox, i)), 1); i++ )
+
+#define Cba_ObjForEachFanout( p, iCi, iCo )                               \
+    for ( iCo = Cba_ObjFanout(p, iCi); iCo; iCo = Cba_ObjNextFanout(p, iCo) )
+#define Cba_BoxForEachFanoutBox( p, iBox, iCo, iFanBox )                  \
+    for ( assert(Cba_BoxBoNum(p, iBox) == 1), iCo = Cba_ObjFanout(p, Cba_BoxBo(p, iBox, 0)); iCo && ((iFanBox = Cba_BoxBiBox(p, iCo)), 1); iCo = Cba_ObjNextFanout(p, iCo) )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -519,6 +546,28 @@ static inline int Cba_BoxDup( Cba_Ntk_t * pNew, Cba_Ntk_t * p, int iBox )
         Cba_ObjDup( pNew, p, iTerm );
     return iBoxNew;
 }
+static inline void Cba_BoxDelete( Cba_Ntk_t * p, int iBox )
+{
+    int iStart = iBox - Cba_BoxBiNum(p, iBox);
+    int i, iStop = iBox + Cba_BoxBoNum(p, iBox);
+    for ( i = iStart; i <= iStop; i++ )
+    {
+        Vec_StrWriteEntry( &p->vType,  i, (char)0 );
+        Vec_IntWriteEntry( &p->vFanin, i, -1 );
+        if ( Cba_NtkHasNames(p) )
+            Vec_IntWriteEntry( &p->vName, i, 0 );
+        if ( Cba_NtkHasFanouts(p) )
+            Vec_IntWriteEntry( &p->vFanout, i, 0 );
+    }
+}
+static inline void Cba_BoxReplace( Cba_Ntk_t * p, int iBox, int * pArray, int nSize )
+{
+    extern void Cba_NtkUpdateFanout( Cba_Ntk_t * p, int iOld, int iNew );
+    int i, Limit = Cba_BoxBoNum(p, iBox);
+    assert( Limit == nSize );
+    for ( i = 0; i < Limit; i++ )
+        Cba_NtkUpdateFanout( p, Cba_BoxBo(p, iBox, i), pArray[i] );
+}
 
 
 /**Function*************************************************************
@@ -647,8 +696,10 @@ static inline void Cba_NtkFree( Cba_Ntk_t * p )
     Vec_IntErase( &p->vFanin );    
     Vec_IntErase( &p->vIndex );
     Vec_IntErase( &p->vName );    
+    Vec_IntErase( &p->vFanout );    
     Vec_IntErase( &p->vCopy );    
     Vec_IntErase( &p->vArray );    
+    Vec_IntErase( &p->vArray2 );    
 }
 static inline int Cba_NtkMemory( Cba_Ntk_t * p )
 {
@@ -660,6 +711,7 @@ static inline int Cba_NtkMemory( Cba_Ntk_t * p )
     nMem += Vec_IntMemory(&p->vFanin);
     nMem += Vec_IntMemory(&p->vIndex);
     nMem += Vec_IntMemory(&p->vName);
+    nMem += Vec_IntMemory(&p->vFanout);
     nMem += Vec_IntMemory(&p->vCopy);
     return nMem;
 }
@@ -985,6 +1037,8 @@ extern void *      Cba_ManInsertAbc( Cba_Man_t * p, void * pAbc );
 extern Cba_Man_t * Cba_ManReadCba( char * pFileName );
 extern void        Cba_ManWriteCba( char * pFileName, Cba_Man_t * p );
 /*=== cbaNtk.c ===============================================================*/
+extern void        Cba_NtkUpdateFanout( Cba_Ntk_t * p, int iOld, int iNew );
+extern void        Cba_ManDeriveFanout( Cba_Man_t * p );
 extern void        Cba_ManAssignInternNames( Cba_Man_t * p );
 extern void        Cba_ManAssignInternWordNames( Cba_Man_t * p );
 extern Cba_Man_t * Cba_ManCollapse( Cba_Man_t * p );
diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c
index 0c49e248..15e433fc 100644
--- a/src/base/cba/cbaBlast.c
+++ b/src/base/cba/cbaBlast.c
@@ -165,11 +165,12 @@ int Cba_ManExtract_rec( Gia_Man_t * pNew, Cba_Ntk_t * p, int i, int fBuffers, Ve
                         iRes = Abc_LitNot( pLits[0] );
                     else assert( 0 );
                 }
-                else
+                else if ( nLits == 2 )
                 {
-                    assert( nLits == 2 );
                     if ( Type == CBA_BOX_AND )
                         iRes = Gia_ManHashAnd( pNew, pLits[0], pLits[1] );
+                    else if ( Type == CBA_BOX_NAND )
+                        iRes = Abc_LitNot( Gia_ManHashAnd( pNew, pLits[0], pLits[1] ) );
                     else if ( Type == CBA_BOX_OR )
                         iRes = Gia_ManHashOr( pNew, pLits[0], pLits[1] );
                     else if ( Type == CBA_BOX_NOR )
@@ -180,9 +181,30 @@ int Cba_ManExtract_rec( Gia_Man_t * pNew, Cba_Ntk_t * p, int i, int fBuffers, Ve
                         iRes = Abc_LitNot( Gia_ManHashXor( pNew, pLits[0], pLits[1] ) );
                     else if ( Type == CBA_BOX_SHARP )
                         iRes = Gia_ManHashAnd( pNew, pLits[0], Abc_LitNot(pLits[1]) );
+                    else if ( Type == CBA_BOX_SHARPL )
+                        iRes = Gia_ManHashAnd( pNew, Abc_LitNot(pLits[0]), pLits[1] );
                     else assert( 0 );
                 }
-                //printf("%d input\n", nLits );
+                else if ( nLits == 3 )
+                {
+                    if ( Type == CBA_BOX_MUX )
+                        iRes = Gia_ManHashMux( pNew, pLits[0], pLits[1], pLits[2] );
+                    else if ( Type == CBA_BOX_MAJ )
+                        iRes = Gia_ManHashMaj( pNew, pLits[0], pLits[1], pLits[2] );
+                    else if ( Type == CBA_BOX_ADD )
+                    {
+                        int iRes0 = Gia_ManHashAnd( pNew, pLits[1], pLits[2] );
+                        int iRes1 = Gia_ManHashOr( pNew, pLits[1], pLits[2] );
+                        assert( Cba_BoxBoNum(p, iBox) == 2 );
+                        if ( Cba_BoxBo(p, iBox, 0) == i ) // sum
+                            iRes = Gia_ManHashXor( pNew, pLits[0], Gia_ManHashAnd(pNew, Abc_LitNot(iRes0), iRes1) );
+                        else if ( Cba_BoxBo(p, iBox, 1) == i ) // cout
+                            iRes = Gia_ManHashOr( pNew, iRes0, Gia_ManHashAnd(pNew, pLits[0], iRes1) );
+                        else assert( 0 );
+                    }
+                    else assert( 0 );
+                }
+                else assert( 0 );
             }
         }
     }
diff --git a/src/base/cba/cbaNtk.c b/src/base/cba/cbaNtk.c
index 435cd83a..15aacd2e 100644
--- a/src/base/cba/cbaNtk.c
+++ b/src/base/cba/cbaNtk.c
@@ -32,6 +32,67 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Replaces fanin iOld by iNew in all fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cba_NtkUpdateFanout( Cba_Ntk_t * p, int iOld, int iNew )
+{
+    int iCo;
+    assert( Cba_ObjIsCi(p, iOld) );
+    assert( Cba_ObjIsCi(p, iNew) );
+    Cba_ObjForEachFanout( p, iOld, iCo )
+    {
+        assert( Cba_ObjFanin(p, iCo) == iOld );
+        Cba_ObjCleanFanin( p, iCo );
+        Cba_ObjSetFanin( p, iCo, iNew );
+    }
+    Cba_ObjSetFanout( p, iNew, Cba_ObjFanout(p, iOld) );
+    Cba_ObjSetFanout( p, iOld, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cba_NtkDeriveFanout( Cba_Ntk_t * p )
+{
+    int iCi, iCo;
+    assert( !Cba_NtkHasFanouts(p) );
+    Cba_NtkStartFanouts( p );
+    Cba_NtkForEachCo( p, iCo )
+    {
+        assert( !Cba_ObjNextFanout(p, iCo) );
+        iCi = Cba_ObjFanin(p, iCo);
+        if ( Cba_ObjFanout(p, iCi) )
+            Cba_ObjSetNextFanout( p, Cba_ObjFanout(p, iCi), iCo );
+        Cba_ObjSetFanout( p, iCi, iCo );
+    }
+    Cba_NtkForEachCo( p, iCo )
+        if ( !Cba_ObjNextFanout(p, iCo) )
+            Cba_ObjSetFanout( p, Cba_ObjFanin(p, iCo), iCo );
+}
+void Cba_ManDeriveFanout( Cba_Man_t * p )
+{
+    Cba_Ntk_t * pNtk; int i;
+    Cba_ManForEachNtk( p, pNtk, i )
+        Cba_NtkDeriveFanout( pNtk );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Assigns word-level names.]
 
   Description []
diff --git a/src/base/cba/cbaOper.c b/src/base/cba/cbaOper.c
new file mode 100644
index 00000000..bc160fd3
--- /dev/null
+++ b/src/base/cba/cbaOper.c
@@ -0,0 +1,365 @@
+/**CFile****************************************************************
+
+  FileName    [cbaOper.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    [Operator procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: cbaOper.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cba.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cba_BoxCreate( Cba_Ntk_t * p, Cba_ObjType_t Type, Vec_Int_t * vFanins, int nInA, int nInB, int nOuts )
+{
+    char pName[100]; int i, iObj, iFanin;
+    assert( CBA_OBJ_BOX < Type && Type < CBA_BOX_UNKNOWN );
+    if ( CBA_BOX_CF <= Type && Type <= CBA_BOX_CZ )
+    {
+        sprintf( pName, "ABCCTo%d", nOuts );
+        assert( 0 == Vec_IntSize(vFanins) );
+        iObj = Cba_BoxAlloc( p, Type, 0, nOuts, Abc_NamStrFindOrAdd(p->pDesign->pMods, pName, NULL) );
+    }
+    else if ( CBA_BOX_BUF <= Type && Type <= CBA_BOX_INV )
+    {
+        char * pPref[2] = { "ABCBUF", "ABCINV" };
+        assert( nInA == nOuts );
+        assert( nInA == Vec_IntSize(vFanins) );
+        sprintf( pName, "%sa%do%d", pPref[Type - CBA_BOX_BUF], nInA, nOuts );
+        iObj = Cba_BoxAlloc( p, Type, Vec_IntSize(vFanins), nOuts, Abc_NamStrFindOrAdd(p->pDesign->pMods, pName, NULL) );
+    }
+    else if ( CBA_BOX_AND <= Type && Type <= CBA_BOX_XNOR )
+    {
+        char * pPref[6] = { "ABCAND", "ABCNAND", "ABCOR", "ABCNOR", "ABCXOR", "ABCXNOR" };
+        assert( nInA == nOuts && nInB == nOuts );
+        assert( nInA + nInB == Vec_IntSize(vFanins) );
+        sprintf( pName, "%sa%db%do%d", pPref[Type - CBA_BOX_AND], nInA, nInB, nOuts );
+        iObj = Cba_BoxAlloc( p, Type, Vec_IntSize(vFanins), nOuts, Abc_NamStrFindOrAdd(p->pDesign->pMods, pName, NULL) );
+    }
+    else if ( Type == CBA_BOX_MUX )
+    {
+        char * pPref[1] = { "ABCMUX" };
+        assert( nInA == nOuts && nInB == nOuts );
+        assert( 1 + nInA + nInB == Vec_IntSize(vFanins) );
+        sprintf( pName, "%sc%da%db%do%d", pPref[Type - CBA_BOX_MUX], 1, nInA, nInB, nOuts );
+        iObj = Cba_BoxAlloc( p, Type, Vec_IntSize(vFanins), nOuts, Abc_NamStrFindOrAdd(p->pDesign->pMods, pName, NULL) );
+    }
+    else if ( Type == CBA_BOX_MAJ )
+    {
+        char * pPref[1] = { "ABCMAJ" };
+        assert( nInA == 1 && nInB == 1 && nOuts == 1 );
+        assert( 3 == Vec_IntSize(vFanins) );
+        sprintf( pName, "%sa%db%dc%do%d", pPref[Type - CBA_BOX_MAJ], 1, 1, 1, 1 );
+        iObj = Cba_BoxAlloc( p, Type, Vec_IntSize(vFanins), nOuts, Abc_NamStrFindOrAdd(p->pDesign->pMods, pName, NULL) );
+    }
+    else if ( CBA_BOX_RAND <= Type && Type <= CBA_BOX_RXNOR )
+    {
+        char * pPref[6] = { "ABCRAND", "ABCRNAND", "ABCROR", "ABCRNOR", "ABCRXOR", "ABCRXNOR" };
+        assert( nInA == nInB && 1 == nOuts );
+        assert( nInA + nInB == Vec_IntSize(vFanins) );
+        sprintf( pName, "%sa%db%do%d", pPref[Type - CBA_BOX_RAND], nInA, nInB, nOuts );
+        iObj = Cba_BoxAlloc( p, Type, Vec_IntSize(vFanins), nOuts, Abc_NamStrFindOrAdd(p->pDesign->pMods, pName, NULL) );
+    }
+    else if ( Type == CBA_BOX_SEL )
+    {
+        char * pPref[1] = { "ABCSEL" };
+        assert( nInA * nOuts == nInB );
+        assert( nInA + nInB == Vec_IntSize(vFanins) );
+        sprintf( pName, "%sa%db%do%d", pPref[Type - CBA_BOX_SEL], nInA, nInB, nOuts );
+        iObj = Cba_BoxAlloc( p, Type, Vec_IntSize(vFanins), nOuts, Abc_NamStrFindOrAdd(p->pDesign->pMods, pName, NULL) );
+    }
+    else if ( Type == CBA_BOX_PSEL )
+    {
+        char * pPref[1] = { "ABCPSEL" };
+        assert( nInA * nOuts == nInB );
+        assert( 1 + nInA + nInB == Vec_IntSize(vFanins) );
+        sprintf( pName, "%si%da%db%do%d", pPref[Type - CBA_BOX_SEL], 1, nInA, nInB, nOuts );
+        iObj = Cba_BoxAlloc( p, Type, Vec_IntSize(vFanins), nOuts, Abc_NamStrFindOrAdd(p->pDesign->pMods, pName, NULL) );
+    }
+    // add fanins
+    Vec_IntForEachEntry( vFanins, iFanin, i )
+        Cba_ObjSetFanin( p, Cba_BoxBi(p, iObj, i), iFanin );
+    return iObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cba_ObjClpWide( Cba_Ntk_t * p, int iBox )
+{
+    Cba_ObjType_t Type = Cba_ObjType( p, iBox );
+    int nBis = Cba_BoxBiNum(p, iBox);
+    int nBos = Cba_BoxBoNum(p, iBox);
+    int i, k, iObj;
+    assert( nBos > 1 );
+    Vec_IntClear( &p->vArray );
+    if ( CBA_BOX_BUF <= Type && Type <= CBA_BOX_INV )
+    {
+        for ( i = 0; i < nBos; i++ )
+        {
+            Vec_IntFill( &p->vArray2, 1, Cba_BoxFanin(p, iBox, i) );
+            iObj = Cba_BoxCreate( p, Type, &p->vArray2, 1, -1, 1 );
+            Vec_IntPush( &p->vArray, Cba_BoxBo(p, iObj, 0) );
+        }
+    }
+    else if ( CBA_BOX_AND <= Type && Type <= CBA_BOX_XNOR )
+    {
+        assert( nBis == 2 * nBos );
+        for ( i = 0; i < nBos; i++ )
+        {
+            Vec_IntFillTwo( &p->vArray2, 2, Cba_BoxFanin(p, iBox, i), Cba_BoxFanin(p, iBox, nBos+i) );
+            iObj = Cba_BoxCreate( p, Type, &p->vArray2, 1, 1, 1 );
+            Vec_IntPush( &p->vArray, Cba_BoxBo(p, iObj, 0) );
+        }
+    }
+    else if ( Type == CBA_BOX_MUX )
+    {
+        assert( nBis - 1 == 2 * nBos );
+        for ( i = 0; i < nBos; i++ )
+        {
+            Vec_IntFill( &p->vArray2, 1, Cba_BoxFanin(p, iBox, 0) );
+            Vec_IntPushTwo( &p->vArray2, Cba_BoxFanin(p, iBox, 1+i), Cba_BoxFanin(p, iBox, 1+nBos+i) );
+            iObj = Cba_BoxCreate( p, Type, &p->vArray2, 1, 1, 1 );
+            Vec_IntPush( &p->vArray, Cba_BoxBo(p, iObj, 0) );
+        }
+    }
+    else if ( Type == CBA_BOX_NMUX )
+    {
+        int n, nIns = nBis / nBos;
+        assert( nBis % nBos == 0 );
+        for ( n = 1; n < 32; n++ )
+            if ( n + (1 << n) == nIns )
+                break;
+        assert( n > 1 && n < 32 );
+        for ( i = 0; i < nBos; i++ )
+        {
+            Vec_IntClear( &p->vArray2 );
+            for ( k = 0; k < n; k++ )
+                Vec_IntPush( &p->vArray2, Cba_BoxFanin(p, iBox, k) );
+            for ( k = 0; k < (1 << n); k++ )
+                Vec_IntPush( &p->vArray2, Cba_BoxFanin(p, iBox, n + (1 << n) * i + k) );
+            iObj = Cba_BoxCreate( p, Type, &p->vArray2, n, (1 << n), 1 );
+            Vec_IntPush( &p->vArray, Cba_BoxBo(p, iObj, 0) );
+        }
+    }
+    else if ( Type == CBA_BOX_SEL )
+    {
+    }
+    else if ( Type == CBA_BOX_PSEL )
+    {
+    }
+    else if ( Type == CBA_BOX_DFF || Type == CBA_BOX_LATCH )
+    {
+    }
+    else if ( Type == CBA_BOX_DFFRS || Type == CBA_BOX_LATCHRS )
+    {
+    }
+    else assert( 0 );
+    Cba_BoxReplace( p, iBox, Vec_IntArray(&p->vArray), Vec_IntSize(&p->vArray) );
+    return iBox;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cba_ObjClpArith( Cba_Ntk_t * p, int iBox )
+{
+    Cba_ObjType_t Type = Cba_ObjType( p, iBox );
+    int i, iObj = -1;
+    int nBis = Cba_NtkReadRangesPrim( Cba_BoxNtkName(p, iObj), &p->vArray, 0 );
+    assert( nBis == Cba_BoxBiNum(p, iBox) );
+    if ( Type == CBA_BOX_ADD )
+    {
+        int Carry = Cba_BoxFanin(p, iBox, 0);
+        int nBits = Vec_IntEntry(&p->vArray, 1);
+        assert( Vec_IntSize(&p->vArray) == 3 );
+        assert( Vec_IntEntry(&p->vArray, 0) == 1 );
+        assert( Vec_IntEntry(&p->vArray, 2) == nBits );
+        Vec_IntClear( &p->vArray );
+        for ( i = 0; i < nBits; i++ )
+        {
+            Vec_IntFill( &p->vArray2, 1, Carry );
+            Vec_IntPushTwo( &p->vArray2, Cba_BoxFanin(p, iBox, 1+i), Cba_BoxFanin(p, iBox, 1+nBits+i) );
+            iObj = Cba_BoxCreate( p, CBA_BOX_ADD, &p->vArray2, 1, 1, 1 );
+            Carry = Cba_BoxBo(p, iObj, 1);
+            Vec_IntPush( &p->vArray, Cba_BoxBo(p, iObj, 0) );
+        }
+        Vec_IntPush( &p->vArray, Carry );
+    }
+    else if ( Type == CBA_BOX_SUB )
+    {
+        int iConst, nBits = Vec_IntEntry(&p->vArray, 0);
+        assert( Vec_IntSize(&p->vArray) == 2 );
+        assert( Vec_IntEntry(&p->vArray, 1) == nBits );
+        // create inverter
+        Vec_IntClear( &p->vArray2 );
+        for ( i = 0; i < nBits; i++ )
+            Vec_IntPush( &p->vArray2, Cba_BoxFanin(p, iBox, nBits+i) );
+        iObj = Cba_BoxCreate( p, CBA_BOX_INV, &p->vArray2, nBits, -1, nBits );
+        // create constant
+        Vec_IntClear( &p->vArray2 );
+        iConst = Cba_BoxCreate( p, CBA_BOX_CT, &p->vArray2, -1, -1, 1 );
+        // collect fanins
+        Vec_IntFill( &p->vArray2, 1, iConst+1 );
+        for ( i = 0; i < nBits; i++ )
+            Vec_IntPush( &p->vArray2, Cba_BoxFanin(p, iBox, i) );
+        for ( i = 0; i < nBits; i++ )
+            Vec_IntPush( &p->vArray2, Cba_BoxBo(p, iObj, i) );
+        // create adder
+        iObj = Cba_BoxCreate( p, CBA_BOX_ADD, &p->vArray2, nBits, nBits, nBits );
+        // collect fanins
+        Vec_IntClear( &p->vArray );
+        for ( i = 0; i < nBits; i++ )
+            Vec_IntPush( &p->vArray, Cba_BoxBo(p, iObj, i) );
+    }
+    else if ( Type == CBA_BOX_MUL )
+    {
+    }
+    else if ( Type == CBA_BOX_DIV )
+    {
+    }
+    else if ( Type == CBA_BOX_MOD )
+    {
+    }
+    else if ( Type == CBA_BOX_REM )
+    {
+    }
+    else if ( Type == CBA_BOX_POW )
+    {
+    }
+    else if ( Type == CBA_BOX_MIN )
+    {
+    }
+    else if ( Type == CBA_BOX_ABS )
+    {
+    }
+
+    else if ( Type == CBA_BOX_LTHAN )
+    {
+    }
+    else if ( Type == CBA_BOX_LETHAN )
+    {
+    }
+    else if ( Type == CBA_BOX_METHAN )
+    {
+    }
+    else if ( Type == CBA_BOX_MTHAN )
+    {
+    }
+    else if ( Type == CBA_BOX_EQU )
+    {
+    }
+    else if ( Type == CBA_BOX_NEQU )
+    {
+    }
+
+    else if ( Type == CBA_BOX_SHIL )
+    {
+    }
+    else if ( Type == CBA_BOX_SHIR )
+    {
+    }
+    else if ( Type == CBA_BOX_ROTL )
+    {
+    }
+    else if ( Type == CBA_BOX_ROTR )
+    {
+    }
+    Cba_BoxReplace( p, iBox, Vec_IntArray(&p->vArray), Vec_IntSize(&p->vArray) );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cba_ObjClpMemory( Cba_Ntk_t * p, int iBox )
+{
+    int i, En, iNext, nItems = Cba_BoxBiNum(p, iBox);
+    assert( Cba_ObjType(p, iBox) == CBA_BOX_RAMBOX );
+    assert( Cba_BoxBiNum(p, iBox) == Cba_BoxBoNum(p, iBox) );
+    // for each fanin of RAMBOX, make sure address width is the same
+    Cba_BoxForEachFaninBox( p, iBox, iNext, i )
+        assert( Cba_ObjType(p, iNext) == CBA_BOX_RAMWC );
+
+    // create decoders, selectors and flops
+    for ( i = 0; i < nItems; i++ )
+    {
+        int BoxW = Cba_ObjFanin(p, Cba_BoxBi(p, iBox, i));
+        int BoxR = Cba_ObjFanout(p, Cba_BoxBo(p, iBox, 0));
+        assert( Cba_ObjType(p, BoxW) == CBA_BOX_RAMWC );
+        assert( Cba_ObjType(p, BoxR) == CBA_BOX_RAMR );
+        // create enable
+        Vec_IntFillTwo( &p->vArray2, 2, Cba_BoxFanin(p, BoxW, 1), Cba_BoxFanin(p, BoxR, 0) );
+        En = Cba_BoxCreate( p, CBA_BOX_AND, &p->vArray2, 1, 1, 1 );
+        En = Cba_BoxBo( p, En, 0 );
+        // collect address
+    }
+    // for each fanout of RAMBOX, makes ure address width is the same
+    Cba_BoxForEachFanoutBox( p, iBox, iNext, i )
+        assert( Cba_ObjType(p, iNext) == CBA_BOX_RAMR );
+    // create selectors and connect them
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/cba/cbaPrs.h b/src/base/cba/cbaPrs.h
index b82a3591..76f7d060 100644
--- a/src/base/cba/cbaPrs.h
+++ b/src/base/cba/cbaPrs.h
@@ -55,6 +55,10 @@ struct Prs_Ntk_t_
     int          iModuleName;
     unsigned     fMapped : 1;
     unsigned     fSlices : 1;
+    unsigned     fHasC0s : 1;
+    unsigned     fHasC1s : 1;
+    unsigned     fHasCXs : 1;
+    unsigned     fHasCZs : 1;
     Abc_Nam_t *  pStrs;
     // interface
     Vec_Int_t    vOrder;     // order of signals
diff --git a/src/base/cba/cbaReadBlif.c b/src/base/cba/cbaReadBlif.c
index 0cadfd7b..4b982868 100644
--- a/src/base/cba/cbaReadBlif.c
+++ b/src/base/cba/cbaReadBlif.c
@@ -222,6 +222,16 @@ static inline int Prs_ManReadCube( Prs_Man_t * p )
 static inline void Prs_ManSaveCover( Prs_Man_t * p )
 {
     int iToken;
+    if ( Vec_StrSize(&p->vCover) == 0 )
+        p->pNtk->fHasC0s = 1;
+    else if ( Vec_StrSize(&p->vCover) == 2 )
+    {
+        if ( Vec_StrEntryLast(&p->vCover) == '0' )
+            p->pNtk->fHasC0s = 1;
+        else if ( Vec_StrEntryLast(&p->vCover) == '1' )
+            p->pNtk->fHasC1s = 1;
+        else assert( 0 );
+    }
     assert( Vec_StrSize(&p->vCover) > 0 );
     Vec_StrPush( &p->vCover, '\0' );
     //iToken = Abc_NamStrFindOrAdd( p->pStrs, Vec_StrArray(&p->vCover), NULL );
diff --git a/src/base/cba/cbaReadVer.c b/src/base/cba/cbaReadVer.c
index 312a4471..84bb1737 100644
--- a/src/base/cba/cbaReadVer.c
+++ b/src/base/cba/cbaReadVer.c
@@ -326,19 +326,39 @@ static inline int Prs_ManReadConstant( Prs_Man_t * p )
     {
         p->pCur++;
         while ( Prs_CharIsDigitB(*p->pCur) ) 
+        {
+            if ( *p->pCur == '0' )
+                p->pNtk->fHasC0s = 1;
+            else if ( *p->pCur == '1' )
+                p->pNtk->fHasC1s = 1;
+            else if ( *p->pCur == 'x' )
+                p->pNtk->fHasCXs = 1;
+            else if ( *p->pCur == 'z' )
+                p->pNtk->fHasCZs = 1;
             p->pCur++;
+        }
     }
     else if ( Prs_ManIsChar(p, 'h') )
     {
         p->pCur++;
+        p->pNtk->fHasC0s = 1;
         while ( Prs_CharIsDigitH(*p->pCur) ) 
+        {
+            if ( *p->pCur != '0' )
+                p->pNtk->fHasC1s = 1;
             p->pCur++;
+        }
     }
     else if ( Prs_ManIsChar(p, 'd') )
     {
         p->pCur++;
+        p->pNtk->fHasC0s = 1;
         while ( Prs_ManIsDigit(p) ) 
+        {
+            if ( *p->pCur != '0' )
+                p->pNtk->fHasC1s = 1;
             p->pCur++;
+        }
     }
     else                                    return Prs_ManErrorSet(p, "Cannot read radix of constant.", 0);
     return Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur, NULL );