Experiments with new network data-structure.

7 files changed, 2026 insertions, 0 deletions

diff --git a/src/base/acb/acb.c b/src/base/acb/acb.c
new file mode 100644
index 00000000..9d44ae3f
--- /dev/null
+++ b/src/base/acb/acb.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [acb.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 21, 2015.]
+
+  Revision    [$Id: acb.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acb.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/acb/acb.h b/src/base/acb/acb.h
new file mode 100644
index 00000000..0979c545
--- /dev/null
+++ b/src/base/acb/acb.h
@@ -0,0 +1,978 @@
+/**CFile****************************************************************
+
+  FileName    [acb.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 21, 2015.]
+
+  Revision    [$Id: acb.h,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__base__acb__acb_h
+#define ABC__base__acb__acb_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig/gia/gia.h"
+#include "misc/extra/extra.h"
+#include "misc/util/utilNam.h"
+#include "misc/vec/vecHash.h"
+#include "aig/miniaig/abcOper.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START 
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+typedef struct Acb_Aig_t_ Acb_Aig_t;
+typedef struct Acb_Ntk_t_ Acb_Ntk_t;
+typedef struct Acb_Man_t_ Acb_Man_t;
+
+// network
+struct Acb_Ntk_t_
+{
+    Acb_Man_t *     pDesign;    // design
+    int             Id;         // network ID
+    int             NameId;     // name ID 
+    int             iCopy;      // copy module
+    unsigned        Mark : 1;   // visit mark 
+    unsigned        fComb: 1;   // the network is combinational
+    unsigned        fSeq : 1;   // the network is sequential
+    // interface
+    Vec_Int_t       vCis;       // inputs 
+    Vec_Int_t       vCos;       // outputs
+    Vec_Int_t       vOrder;     // order
+    Vec_Int_t       vSeq;       // sequential objects
+    int             nRegs;      // flop count
+    int             nFaninMax;  // default fanin count
+    int             nObjTravs;  // trav ID
+    // stucture
+    Vec_Str_t       vObjType;   // type     
+    Vec_Int_t       vObjFans;   // fanin offsets
+    Vec_Int_t       vFanSto;    // fanin storage
+    Vec_Wec_t       vFanouts;   // fanouts
+    // optional
+    Vec_Int_t       vObjCopy;   // copy
+    Vec_Int_t       vObjFunc;   // function
+    Vec_Int_t       vObjWeight; // weight
+    Vec_Wrd_t       vObjTruth;  // function
+    Vec_Int_t       vObjName;   // name
+    Vec_Int_t       vObjRange;  // range
+    Vec_Int_t       vObjTrav;   // trav ID
+    Vec_Int_t       vObjBits;   // obj mapping into AIG nodes
+    Vec_Int_t       vObjAttr;   // attribute offset
+    Vec_Int_t       vAttrSto;   // attribute storage
+    Vec_Int_t       vNtkObjs;   // instances
+    Vec_Int_t       vTargets;   // targets
+    // other
+    Vec_Int_t       vArray0;
+    Vec_Int_t       vArray1;
+};
+
+// design
+struct Acb_Man_t_
+{
+    // design names
+    char *          pName;      // design name
+    char *          pSpec;      // spec file name
+    Abc_Nam_t *     pStrs;      // string manager
+    Abc_Nam_t *     pFuns;      // constant manager
+    Abc_Nam_t *     pMods;      // module name manager
+    Hash_IntMan_t * vHash;      // variable ranges
+    Vec_Int_t       vNameMap;   // mapping names
+    Vec_Int_t       vNameMap2;  // mapping names
+    Vec_Int_t       vUsed;      // used map entries
+    Vec_Int_t       vUsed2;     // used map entries
+    char *          pTypeNames[ABC_OPER_LAST];
+    int             nObjs[ABC_OPER_LAST]; // counter of objects of each type
+    int             nAnds[ABC_OPER_LAST]; // counter of AND gates after blasting
+    // internal data
+    int             iRoot;      // root network
+    Vec_Ptr_t       vNtks;      // networks
+    // user data
+    int             nOpens;
+    Vec_Str_t       vOut;     
+    Vec_Str_t       vOut2;     
+    void *          pMioLib;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline char *         Acb_ManName( Acb_Man_t * p )                    { return p->pName;                                                                            }
+static inline char *         Acb_ManSpec( Acb_Man_t * p )                    { return p->pSpec;                                                                            }
+static inline int            Acb_ManNtkNum( Acb_Man_t * p )                  { return Vec_PtrSize(&p->vNtks)-1;                                                            }
+static inline int            Acb_ManNtkIsOk( Acb_Man_t * p, int i )          { return i > 0 && i <= Acb_ManNtkNum(p);                                                      }
+static inline Acb_Ntk_t *    Acb_ManNtk( Acb_Man_t * p, int i )              { return Acb_ManNtkIsOk(p, i) ? (Acb_Ntk_t *)Vec_PtrEntry(&p->vNtks, i) : NULL;               }
+static inline int            Acb_ManNtkFindId( Acb_Man_t * p, char * pName ) { return Abc_NamStrFind(p->pMods, pName);                                                     }
+static inline Acb_Ntk_t *    Acb_ManNtkFind( Acb_Man_t * p, char * pName )   { return Acb_ManNtk( p, Acb_ManNtkFindId(p, pName) );                                         }
+static inline Acb_Ntk_t *    Acb_ManRoot( Acb_Man_t * p )                    { return Acb_ManNtk(p, p->iRoot);                                                             }
+static inline char *         Acb_ManStr( Acb_Man_t * p, int i )              { return Abc_NamStr(p->pStrs, i);                                                             }
+static inline int            Acb_ManStrId( Acb_Man_t * p, char * pStr )      { return Abc_NamStrFind(p->pStrs, pStr);                                                      }
+static inline int            Acb_ManNameIdMax( Acb_Man_t * p )               { return Abc_NamObjNumMax(p->pStrs) + 1;                                                      }
+static inline char *         Acb_ManConst( Acb_Man_t * p, int i )            { return Abc_NamStr(p->pFuns, i);                                                             }
+static inline int            Acb_ManConstId( Acb_Man_t * p, char * pStr )    { return Abc_NamStrFind(p->pFuns, pStr);                                                      }
+static inline int            Acb_ManConstIdMax( Acb_Man_t * p )              { return Abc_NamObjNumMax(p->pFuns) + 1;                                                      }
+
+static inline Acb_Man_t *    Acb_NtkMan( Acb_Ntk_t * p )                     { return p->pDesign;                                                                          }
+static inline Acb_Ntk_t *    Acb_NtkNtk( Acb_Ntk_t * p, int i )              { return Acb_ManNtk(p->pDesign, i);                                                           }
+static inline int            Acb_NtkId( Acb_Ntk_t * p )                      { return p->Id;                                                                               }
+static inline int            Acb_NtkCi( Acb_Ntk_t * p, int i )               { return Vec_IntEntry(&p->vCis, i);                                                           }
+static inline int            Acb_NtkCo( Acb_Ntk_t * p, int i )               { return Vec_IntEntry(&p->vCos, i);                                                           }
+static inline int            Acb_NtkCioOrder( Acb_Ntk_t * p, int i )         { return Vec_IntEntry(&p->vOrder, i);                                                         }
+static inline int            Acb_NtkBoxSeq( Acb_Ntk_t * p, int i )           { return Vec_IntEntry(&p->vSeq, i);                                                           }
+static inline Abc_Nam_t *    Acb_NtkNam( Acb_Ntk_t * p )                     { return p->pDesign->pStrs;                                                                   }
+static inline char *         Acb_NtkStr( Acb_Ntk_t * p, int i )              { return Acb_ManStr(p->pDesign, i);                                                           }
+static inline int            Acb_NtkStrId( Acb_Ntk_t * p, char * pName )     { return Acb_ManStrId(p->pDesign, pName);                                                     }
+static inline char *         Acb_NtkConst( Acb_Ntk_t * p, int i )            { return Acb_ManConst(p->pDesign, i);                                                         }
+static inline char *         Acb_NtkSop( Acb_Ntk_t * p, int i )              { return Acb_ManConst(p->pDesign, i);                                                         }
+static inline int            Acb_NtkNameId( Acb_Ntk_t * p )                  { return p->NameId;                                                                           }
+static inline char *         Acb_NtkName( Acb_Ntk_t * p )                    { return Acb_NtkStr(p, p->NameId);                                                            }
+static inline char *         Acb_NtkTypeName( Acb_Ntk_t * p, int Type )      { return p->pDesign->pTypeNames[Type];                                                        }
+static inline int            Acb_NtkCopy( Acb_Ntk_t * p )                    { return p->iCopy;                                                                            }
+static inline Acb_Ntk_t *    Acb_NtkCopyNtk(Acb_Man_t * pNew, Acb_Ntk_t * p) { return Acb_ManNtk(pNew, Acb_NtkCopy(p));                                                    }
+static inline void           Acb_NtkSetCopy( Acb_Ntk_t * p, int i )          { assert(p->iCopy == 0); p->iCopy = i;                                                        }
+static inline int            Acb_NtkHashRange( Acb_Ntk_t * p, int l, int r ) { return Hash_Int2ManInsert( p->pDesign->vHash, l, r, 0 );                                    }
+static inline int            Acb_NtkRangeLeft( Acb_Ntk_t * p, int h )        { return h ? Hash_IntObjData0( p->pDesign->vHash, h ) : 0;                                    }
+static inline int            Acb_NtkRangeRight( Acb_Ntk_t * p, int h )       { return h ? Hash_IntObjData1( p->pDesign->vHash, h ) : 0;                                    }
+static inline int            Acb_NtkRangeSize( Acb_Ntk_t * p, int h )        { int l = Acb_NtkRangeLeft(p, h), r = Acb_NtkRangeRight(p, h); return 1 + (l > r ? l-r : r-l);}
+
+static inline int            Acb_NtkCiNum( Acb_Ntk_t * p )                   { return Vec_IntSize(&p->vCis);                                                               }
+static inline int            Acb_NtkCoNum( Acb_Ntk_t * p )                   { return Vec_IntSize(&p->vCos);                                                               }
+static inline int            Acb_NtkCioNum( Acb_Ntk_t * p )                  { return Acb_NtkCiNum(p) + Acb_NtkCoNum(p);                                                   }
+static inline int            Acb_NtkCiNumAlloc( Acb_Ntk_t * p )              { return Vec_IntCap(&p->vCis);                                                                }
+static inline int            Acb_NtkCoNumAlloc( Acb_Ntk_t * p )              { return Vec_IntCap(&p->vCos);                                                                }
+static inline int            Acb_NtkRegNum( Acb_Ntk_t * p )                  { return p->nRegs;                                                                            }
+static inline void           Acb_NtkSetRegNum( Acb_Ntk_t * p, int nRegs )    { p->nRegs = nRegs;                                                                           }
+static inline int            Acb_NtkPiNum( Acb_Ntk_t * p )                   { return Acb_NtkCiNum(p) - Acb_NtkRegNum(p);                                                  }
+static inline int            Acb_NtkPoNum( Acb_Ntk_t * p )                   { return Acb_NtkCoNum(p) - Acb_NtkRegNum(p);                                                  }
+static inline int            Acb_NtkCioOrderNum( Acb_Ntk_t * p )             { return Vec_IntSize(&p->vOrder);                                                             }
+static inline int            Acb_NtkObjNum( Acb_Ntk_t * p )                  { return Vec_StrSize(&p->vObjType)-1;                                                         }
+static inline int            Acb_NtkObjNumAlloc( Acb_Ntk_t * p )             { return Vec_StrCap(&p->vObjType)-1;                                                          }
+static inline int            Acb_NtkTypeNum( Acb_Ntk_t * p, int Type )       { return Vec_StrCountEntry(&p->vObjType, (char)Type);                                         }
+static inline int            Acb_NtkBoxNum( Acb_Ntk_t * p )                  { return Acb_NtkTypeNum(p, ABC_OPER_BOX);                                                      }
+static inline int            Acb_NtkNodeNum( Acb_Ntk_t * p )                 { return Vec_StrCountLarger(&p->vObjType, (char)ABC_OPER_BOX);                                 }
+static inline int            Acb_NtkSeqNum( Acb_Ntk_t * p )                  { return Vec_IntSize(&p->vSeq);                                                               }
+
+static inline void           Acb_NtkCleanObjCopies( Acb_Ntk_t * p )          { Vec_IntFill(&p->vObjCopy,  Vec_StrCap(&p->vObjType), -1);                                   }
+static inline void           Acb_NtkCleanObjFuncs( Acb_Ntk_t * p )           { Vec_IntFill(&p->vObjFunc,  Vec_StrCap(&p->vObjType),  0);                                   }
+static inline void           Acb_NtkCleanObjWeights( Acb_Ntk_t * p )         { Vec_IntFill(&p->vObjWeight,Vec_StrCap(&p->vObjType),  0);                                   }
+static inline void           Acb_NtkCleanObjTruths( Acb_Ntk_t * p )          { Vec_WrdFill(&p->vObjTruth, Vec_StrCap(&p->vObjType),  0);                                   }
+static inline void           Acb_NtkCleanObjNames( Acb_Ntk_t * p )           { Vec_IntFill(&p->vObjName,  Vec_StrCap(&p->vObjType),  0);                                   }
+static inline void           Acb_NtkCleanObjRanges( Acb_Ntk_t * p )          { Vec_IntFill(&p->vObjRange, Vec_StrCap(&p->vObjType),  0);                                   }
+static inline void           Acb_NtkCleanObjTravs( Acb_Ntk_t * p )           { Vec_IntFill(&p->vObjTrav,  Vec_StrCap(&p->vObjType),  0);                                   }
+static inline void           Acb_NtkCleanObjAttrs( Acb_Ntk_t * p )           { Vec_IntFill(&p->vObjAttr,  Vec_StrCap(&p->vObjType),  0); Vec_IntFill(&p->vAttrSto, 1, -1); }
+
+static inline int            Acb_NtkHasObjCopies( Acb_Ntk_t * p )            { return Vec_IntSize(&p->vObjCopy)  > 0; }
+static inline int            Acb_NtkHasObjFuncs( Acb_Ntk_t * p )             { return Vec_IntSize(&p->vObjFunc)  > 0; }
+static inline int            Acb_NtkHasObjWeights( Acb_Ntk_t * p )           { return Vec_IntSize(&p->vObjWeight)> 0; }
+static inline int            Acb_NtkHasObjTruths( Acb_Ntk_t * p )            { return Vec_WrdSize(&p->vObjTruth) > 0; }
+static inline int            Acb_NtkHasObjNames( Acb_Ntk_t * p )             { return Vec_IntSize(&p->vObjName)  > 0; }
+static inline int            Acb_NtkHasObjRanges( Acb_Ntk_t * p )            { return Vec_IntSize(&p->vObjRange) > 0; }
+static inline int            Acb_NtkHasObjTravs( Acb_Ntk_t * p )             { return Vec_IntSize(&p->vObjTrav)  > 0; }
+static inline int            Acb_NtkHasObjAttrs( Acb_Ntk_t * p )             { return Vec_IntSize(&p->vObjAttr)  > 0; }
+
+static inline void           Acb_NtkFreeObjCopies( Acb_Ntk_t * p )           { Vec_IntErase(&p->vObjCopy);            }
+static inline void           Acb_NtkFreeObjFuncs( Acb_Ntk_t * p )            { Vec_IntErase(&p->vObjFunc);            }
+static inline void           Acb_NtkFreeObjWeights( Acb_Ntk_t * p )          { Vec_IntErase(&p->vObjWeight);          }
+static inline void           Acb_NtkFreeObjTruths( Acb_Ntk_t * p )           { Vec_WrdErase(&p->vObjTruth);           }
+static inline void           Acb_NtkFreeObjNames( Acb_Ntk_t * p )            { Vec_IntErase(&p->vObjName);            }
+static inline void           Acb_NtkFreeObjRanges( Acb_Ntk_t * p )           { Vec_IntErase(&p->vObjRange);           }
+static inline void           Acb_NtkFreeObjTravs( Acb_Ntk_t * p )            { Vec_IntErase(&p->vObjTrav);            }
+static inline void           Acb_NtkFreeObjAttrs( Acb_Ntk_t * p )            { Vec_IntErase(&p->vObjAttr);            }
+
+static inline Acb_ObjType_t  Acb_ObjType( Acb_Ntk_t * p, int i )             { assert(i>0); return (Acb_ObjType_t)(int)(unsigned char)Vec_StrEntry(&p->vObjType, i);        }
+static inline void           Acb_ObjCleanType( Acb_Ntk_t * p, int i )        { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)ABC_OPER_NONE );                      }
+static inline int            Acb_TypeIsSeq( Acb_ObjType_t Type )             { return Type >= ABC_OPER_RAM && Type <= ABC_OPER_DFFRS;                                       }
+static inline int            Acb_TypeIsUnary( Acb_ObjType_t Type )           { return Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_BIT_INV || Type == ABC_OPER_LOGIC_NOT || Type == ABC_OPER_ARI_MIN || Type == ABC_OPER_ARI_SQRT || Type == ABC_OPER_ARI_ABS || (Type >= ABC_OPER_RED_AND && Type <= ABC_OPER_RED_NXOR);  }
+static inline int            Acb_TypeIsMux( Acb_ObjType_t Type )             { return Type == ABC_OPER_BIT_MUX || Type == ABC_OPER_SEL_NMUX || Type == ABC_OPER_SEL_SEL || Type == ABC_OPER_SEL_PSEL;  }
+
+static inline int            Acb_ObjIsCi( Acb_Ntk_t * p, int i )             { return Acb_ObjType(p, i) == ABC_OPER_CI;                                                     }
+static inline int            Acb_ObjIsCo( Acb_Ntk_t * p, int i )             { return Acb_ObjType(p, i) == ABC_OPER_CO;                                                     }
+static inline int            Acb_ObjIsCio( Acb_Ntk_t * p, int i )            { return Acb_ObjIsCi(p, i) || Acb_ObjIsCo(p, i);                                               }
+static inline int            Acb_ObjIsFon( Acb_Ntk_t * p, int i )            { return Acb_ObjType(p, i) == ABC_OPER_FON;                                                    }
+static inline int            Acb_ObjIsBox( Acb_Ntk_t * p, int i )            { return Acb_ObjType(p, i) == ABC_OPER_BOX;                                                    }
+static inline int            Acb_ObjIsGate( Acb_Ntk_t * p, int i )           { return Acb_ObjType(p, i) == ABC_OPER_GATE;                                                   }
+static inline int            Acb_ObjIsSlice( Acb_Ntk_t * p, int i )          { return Acb_ObjType(p, i) == ABC_OPER_SLICE;                                                  }
+static inline int            Acb_ObjIsConcat( Acb_Ntk_t * p, int i )         { return Acb_ObjType(p, i) == ABC_OPER_CONCAT;                                                 }
+static inline int            Acb_ObjIsUnary( Acb_Ntk_t * p, int i )          { return Acb_TypeIsUnary(Acb_ObjType(p, i));                                                   }
+ 
+static inline int            Acb_ObjFanOffset( Acb_Ntk_t * p, int i )        { assert(i>0); return Vec_IntEntry(&p->vObjFans, i);                                           }
+static inline int *          Acb_ObjFanins( Acb_Ntk_t * p, int i )           { return Vec_IntEntryP(&p->vFanSto, Acb_ObjFanOffset(p, i));                                   }
+static inline int            Acb_ObjFanin( Acb_Ntk_t * p, int i, int k )     { return Acb_ObjFanins(p, i)[k+1];                                                             }
+static inline int            Acb_ObjFaninNum( Acb_Ntk_t * p, int i )         { return Acb_ObjFanins(p, i)[0];                                                               }
+static inline int            Acb_ObjFanin0( Acb_Ntk_t * p, int i )           { return Acb_ObjFanins(p, i)[1];                                                               }
+static inline int            Acb_ObjCioId( Acb_Ntk_t * p, int i )            { return Acb_ObjFanins(p, i)[2];                                                               }
+ 
+static inline int            Acb_ObjCopy( Acb_Ntk_t * p, int i )             { assert(i>0); assert( Acb_NtkHasObjCopies(p) ); return Vec_IntGetEntryFull(&p->vObjCopy, i);  }
+static inline int            Acb_ObjFunc( Acb_Ntk_t * p, int i )             { assert(i>0); assert( Acb_NtkHasObjFuncs(p) );  return Vec_IntGetEntry(&p->vObjFunc, i);      }
+static inline int            Acb_ObjWeight( Acb_Ntk_t * p, int i )           { assert(i>0); assert( Acb_NtkHasObjWeights(p) );return Vec_IntGetEntry(&p->vObjWeight, i);    }
+static inline word           Acb_ObjTruth( Acb_Ntk_t * p, int i )            { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdGetEntry(&p->vObjTruth, i);     }
+static inline int            Acb_ObjName( Acb_Ntk_t * p, int i )             { assert(i>0); assert( Acb_NtkHasObjNames(p) );  return Vec_IntGetEntry(&p->vObjName, i);      }
+static inline char *         Acb_ObjNameStr( Acb_Ntk_t * p, int i )          { assert(i>0); return Acb_NtkStr(p, Acb_ObjName(p, i));                                        }
+static inline int            Acb_ObjAttr( Acb_Ntk_t * p, int i )             { assert(i>=0); return Acb_NtkHasObjAttrs(p) ? Vec_IntGetEntry(&p->vObjAttr, i) : 0;           }
+static inline int            Acb_ObjAttrSize( Acb_Ntk_t * p, int i )         { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntry(&p->vAttrSto, Acb_ObjAttr(p, i)) : 0;  }
+static inline int *          Acb_ObjAttrArray( Acb_Ntk_t * p, int i )        { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntryP(&p->vAttrSto, Acb_ObjAttr(p, i)+1) : NULL; }
+static inline int            Acb_ObjAttrValue( Acb_Ntk_t * p, int i, int x ) { int k, s = Acb_ObjAttrSize(p, i), * a = Acb_ObjAttrArray(p, i); for ( k = 0; k < s; k += 2)  if (a[k] == x) return a[k+1]; return 0; }
+
+static inline void           Acb_ObjSetCopy( Acb_Ntk_t * p, int i, int x )   { assert(Acb_ObjCopy(p, i) == -1); Vec_IntSetEntry( &p->vObjCopy, i, x );                      }
+static inline void           Acb_ObjSetFunc( Acb_Ntk_t * p, int i, int x )   { assert(Acb_ObjFunc(p, i) ==  0); Vec_IntSetEntry( &p->vObjFunc, i, x );                      }
+static inline void           Acb_ObjSetWeight( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjWeight(p, i) ==  0); Vec_IntSetEntry( &p->vObjWeight, i, x );                  }
+static inline void           Acb_ObjSetTruth( Acb_Ntk_t * p, int i, word x ) { assert(Acb_ObjTruth(p, i) ==  0);Vec_WrdSetEntry( &p->vObjTruth, i, x );                     }
+static inline void           Acb_ObjSetName( Acb_Ntk_t * p, int i, int x )   { assert(Acb_ObjName(p, i) ==  0); Vec_IntSetEntry( &p->vObjName, i, x );                      }
+static inline void           Acb_ObjSetAttrs( Acb_Ntk_t * p, int i, int * a, int s )  { assert(Acb_ObjAttr(p, i) == 0); if ( !a ) return; Vec_IntSetEntry(&p->vObjAttr, i, Vec_IntSize(&p->vAttrSto)); Vec_IntPush(&p->vAttrSto, s); Vec_IntPushArray(&p->vAttrSto, a, s);  }
+
+static inline int            Acb_ObjNtkId( Acb_Ntk_t * p, int i )            { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjFanin(p, i, Acb_ObjFaninNum(p, i)) : 0;      }
+static inline Acb_Ntk_t *    Acb_ObjNtk( Acb_Ntk_t * p, int i )              { assert(i>0); return Acb_NtkNtk(p, Acb_ObjNtkId(p, i));                                       }
+static inline int            Acb_ObjIsSeq( Acb_Ntk_t * p, int i )            { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjNtk(p, i)->fSeq : Acb_TypeIsSeq(Acb_ObjType(p, i));  }
+
+static inline int            Acb_ObjRangeId( Acb_Ntk_t * p, int i )          { return Acb_NtkHasObjRanges(p) ? Vec_IntGetEntry(&p->vObjRange, i) : 0;                       }
+static inline int            Acb_ObjRange( Acb_Ntk_t * p, int i )            { return Abc_Lit2Var( Acb_ObjRangeId(p, i) );                                                  }
+static inline int            Acb_ObjLeft( Acb_Ntk_t * p, int i )             { return Acb_NtkRangeLeft(p, Acb_ObjRange(p, i));                                              }
+static inline int            Acb_ObjRight( Acb_Ntk_t * p, int i )            { return Acb_NtkRangeRight(p, Acb_ObjRange(p, i));                                             }
+static inline int            Acb_ObjSigned( Acb_Ntk_t * p, int i )           { return Abc_LitIsCompl(Acb_ObjRangeId(p, i));                                                 }
+static inline int            Acb_ObjRangeSize( Acb_Ntk_t * p, int i )        { return Acb_NtkRangeSize(p, Acb_ObjRange(p, i));                                              }
+static inline void           Acb_ObjSetRangeSign( Acb_Ntk_t * p, int i, int x )     { assert(Acb_NtkHasObjRanges(p));  Vec_IntSetEntry(&p->vObjRange, i, x);                }
+static inline void           Acb_ObjSetRange( Acb_Ntk_t * p, int i, int x )         { assert(Acb_NtkHasObjRanges(p));  Vec_IntSetEntry(&p->vObjRange, i, Abc_Var2Lit(x,0)); }
+static inline void           Acb_ObjHashRange( Acb_Ntk_t * p, int i, int l, int r ) { Acb_ObjSetRange( p, i, Acb_NtkHashRange(p, l, r) );                                   }
+static inline int            Acb_ObjRangeSign( Acb_Ntk_t * p, int i )        { return Abc_Var2Lit( Acb_ObjRangeSize(p, i), Acb_ObjSigned(p, i) );                           }
+
+static inline int            Acb_ObjTravId( Acb_Ntk_t * p, int i )           { return Vec_IntGetEntry(&p->vObjTrav, i);                                                     }
+static inline int            Acb_ObjIsTravIdCur( Acb_Ntk_t * p, int i )      { return Acb_ObjTravId(p, i) == p->nObjTravs;                                                  }
+static inline int            Acb_ObjIsTravIdPrev( Acb_Ntk_t * p, int i )     { return Acb_ObjTravId(p, i) == p->nObjTravs-1;                                                }
+static inline int            Acb_ObjSetTravIdCur( Acb_Ntk_t * p, int i )     { int r = Acb_ObjIsTravIdCur(p, i);   Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs);   return r; }
+static inline int            Acb_ObjSetTravIdPrev( Acb_Ntk_t * p, int i )    { int r = Acb_ObjSetTravIdPrev(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-1); return r; }
+static inline int            Acb_NtkTravId( Acb_Ntk_t * p )                  { return p->nObjTravs;                                                                         }
+static inline void           Acb_NtkIncTravId( Acb_Ntk_t * p )               { if ( !Acb_NtkHasObjTravs(p) ) Acb_NtkCleanObjTravs(p); p->nObjTravs++;                       }
+
+////////////////////////////////////////////////////////////////////////
+///                          ITERATORS                               ///
+////////////////////////////////////////////////////////////////////////
+
+#define Acb_ManForEachNtk( p, pNtk, i )                                   \
+    for ( i = 1; (i <= Acb_ManNtkNum(p)) && (((pNtk) = Acb_ManNtk(p, i)), 1); i++ ) 
+
+#define Acb_NtkForEachPi( p, iObj, i )                                    \
+    for ( i = 0; (i < Acb_NtkPiNum(p))  && (((iObj) = Acb_NtkCi(p, i)), 1); i++ ) 
+#define Acb_NtkForEachPo( p, iObj, i )                                    \
+    for ( i = 0; (i < Acb_NtkPoNum(p))  && (((iObj) = Acb_NtkCo(p, i)), 1); i++ ) 
+
+#define Acb_NtkForEachCi( p, iObj, i )                                    \
+    for ( i = 0; (i < Acb_NtkCiNum(p))  && (((iObj) = Acb_NtkCi(p, i)), 1); i++ ) 
+#define Acb_NtkForEachCo( p, iObj, i )                                    \
+    for ( i = 0; (i < Acb_NtkCoNum(p))  && (((iObj) = Acb_NtkCo(p, i)), 1); i++ ) 
+
+#define Acb_NtkForEachBoxSeq( p, iObj, i )                                \
+    for ( i = 0; (i < Acb_NtkSeqNum(p))  && (((iObj) = Acb_NtkBoxSeq(p, i)), 1); i++ ) 
+#define Acb_NtkForEachCioOrder( p, iObj, i )                              \
+    for ( i = 0; (i < Acb_NtkCioOrderNum(p))  && (((iObj) = Acb_NtkCioOrder(p, i)), 1); i++ ) 
+
+#define Acb_NtkForEachCoDriver( p, iObj, i )                              \
+    for ( i = 0; (i < Acb_NtkCoNum(p))  && (((iObj) = Acb_ObjFanin(p, Acb_NtkCo(p, i), 0)), 1); i++ ) 
+
+#define Acb_NtkForEachObj( p, i )                                         \
+    for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Acb_ObjType(p, i) ) {} else   
+#define Acb_NtkForEachObjType( p, Type, i )                               \
+    for ( i = 1; i < Vec_StrSize(&p->vObjType) && (((Type) = Acb_ObjType(p, i)), 1); i++ ) if ( !Type ) {} else
+#define Acb_NtkForEachBox( p, i )                                         \
+    for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Acb_ObjIsBox(p, i) ) {} else
+
+#define Acb_ObjForEachFanin( p, iObj, iFanin, k )                         \
+    for ( k = 0; k < Acb_ObjFaninNum(p, iObj) && ((iFanin = Acb_ObjFanin(p, iObj, k)), 1); k++ )
+#define Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )            \
+    for ( k = 0, pFanins = Acb_ObjFanins(p, iObj); k < pFanins[0] && ((iFanin = pFanins[k+1]), 1); k++ )
+
+#define Acb_ObjForEachFon( p, iObj, iFon )                                \
+    for ( assert(Acb_ObjIsBox(p, iObj)), iFon = iObj + 1; iFon < Acb_NtkObjNum(p) && Acb_ObjIsFon(p, iFon); iFon++ ) 
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Object APIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Acb_ObjFonNum( Acb_Ntk_t * p, int iObj )
+{
+    int i, Count = 0;
+    if ( !Acb_ObjIsBox(p, iObj) ) 
+        return 0;
+    Acb_ObjForEachFon( p, iObj, i )
+        Count++;
+    return Count;
+}
+static inline void Acb_ObjAddFanin( Acb_Ntk_t * p, int iObj, int iFanin )
+{
+    int * pFanins = Acb_ObjFanins( p, iObj );
+    assert( pFanins[ 1 + pFanins[0] ] == -1 );
+    pFanins[ 1 + pFanins[0]++ ] = iFanin;
+}
+static inline void Acb_ObjSetNtkId( Acb_Ntk_t * p, int iObj, int iNtk ) // should be called after fanins are added
+{
+    int * pFanins = Acb_ObjFanins( p, iObj );
+    assert( pFanins[ 1 + pFanins[0] ] == -1 );
+    pFanins[ 1 + pFanins[0] ] = iNtk;
+}
+static inline int Acb_ObjAlloc( Acb_Ntk_t * p, Acb_ObjType_t Type, int nFans, int nFons )
+{
+    int i, nFansReal, CioId = -1, iObj = Vec_StrSize(&p->vObjType);
+    Vec_StrPush( &p->vObjType, (char)Type );
+    if ( Type == ABC_OPER_CI )
+    {
+        assert( nFans == 0 );
+        CioId = Vec_IntSize( &p->vCis );
+        Vec_IntPush( &p->vCis, iObj );
+        nFansReal = 2;
+    }
+    else if ( Type == ABC_OPER_CO )
+    {
+        assert( nFans == 1 );
+        CioId = Vec_IntSize( &p->vCos );
+        Vec_IntPush( &p->vCos, iObj );
+        nFansReal = 2;
+    }
+    else 
+        nFansReal = Abc_MaxInt( nFans + Acb_ObjIsBox(p, iObj), p->nFaninMax );
+    // add fins
+    Vec_IntPush( &p->vObjFans, Vec_IntSize(&p->vFanSto) );
+    Vec_IntPush( &p->vFanSto, 0 );
+    for ( i = 0; i < nFansReal; i++ )
+        Vec_IntPush( &p->vFanSto, (CioId >= 0 && i == 1) ? CioId : -1 );
+    // add fons
+    assert( !Acb_ObjIsBox(p, iObj) || nFons > 0 );
+    for ( i = 0; i < nFons; i++ )
+        Acb_ObjAddFanin( p, Acb_ObjAlloc(p, ABC_OPER_FON, 1, 0), iObj );
+    return iObj;
+}
+static inline int Acb_ObjDup( Acb_Ntk_t * pNew, Acb_Ntk_t * p, int i )
+{
+    int iObj = Acb_ObjAlloc( pNew, Acb_ObjType(p, i), Acb_ObjFaninNum(p, i), Acb_ObjFonNum(p, i) );
+    Acb_ObjSetCopy( p, i, iObj );
+    return iObj;
+}
+static inline void Acb_ObjDelete( Acb_Ntk_t * p, int iObj )
+{
+    int i;
+    Acb_ObjCleanType( p, iObj );
+    if ( !Acb_ObjIsBox(p, iObj) ) 
+        return;
+    Acb_ObjForEachFon( p, iObj, i )
+        Acb_ObjCleanType( p, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Network APIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Acb_Ntk_t *  Acb_NtkAlloc( Acb_Man_t * p, int NameId, int nCis, int nCos, int nObjs )
+{    
+    Acb_Ntk_t * pNew = ABC_CALLOC( Acb_Ntk_t, 1 );
+    assert( nCis >= 0 && nCos >= 0 && nObjs >= 0 );
+    pNew->Id      = Vec_PtrSize(&p->vNtks);   Vec_PtrPush( &p->vNtks, pNew );
+    pNew->NameId  = NameId;
+    pNew->pDesign = p;
+    Vec_IntGrow( &pNew->vCis, nCis );
+    Vec_IntGrow( &pNew->vCos, nCos );
+    Vec_StrGrow( &pNew->vObjType, nObjs+1 );  Vec_StrPush( &pNew->vObjType,  (char)ABC_OPER_NONE );
+    Vec_IntGrow( &pNew->vObjFans, nObjs+1 );  Vec_IntPush( &pNew->vObjFans, -1 );
+    Vec_IntGrow( &pNew->vFanSto,  3*nObjs );  
+    return pNew;
+}
+static inline void Acb_NtkFree( Acb_Ntk_t * p )
+{
+    // interface
+    Vec_IntErase( &p->vCis );
+    Vec_IntErase( &p->vCos );
+    Vec_IntErase( &p->vOrder );
+    Vec_IntErase( &p->vSeq );
+    // stucture
+    Vec_StrErase( &p->vObjType );
+    Vec_IntErase( &p->vObjFans );    
+    Vec_IntErase( &p->vFanSto );
+    Vec_WecErase( &p->vFanouts );
+    // optional
+    Vec_IntErase( &p->vObjCopy );    
+    Vec_IntErase( &p->vObjFunc );    
+    Vec_IntErase( &p->vObjWeight );    
+    Vec_WrdErase( &p->vObjTruth );    
+    Vec_IntErase( &p->vObjName );    
+    Vec_IntErase( &p->vObjRange );    
+    Vec_IntErase( &p->vObjTrav );    
+    Vec_IntErase( &p->vObjBits );    
+    Vec_IntErase( &p->vObjAttr );    
+    Vec_IntErase( &p->vAttrSto );    
+    Vec_IntErase( &p->vNtkObjs );    
+    Vec_IntErase( &p->vTargets );    
+    // other
+    Vec_IntErase( &p->vArray0 );    
+    Vec_IntErase( &p->vArray1 );    
+    ABC_FREE( p );
+}
+static inline int Acb_NtkNewStrId( Acb_Ntk_t * pNtk, const char * format, ...  )
+{
+    Abc_Nam_t * p = Acb_NtkNam( pNtk );
+    Vec_Str_t * vBuf = Abc_NamBuffer( p );
+    int nAdded, nSize = 1000; 
+    va_list args;   va_start( args, format );
+    Vec_StrGrow( vBuf, Vec_StrSize(vBuf) + nSize );
+    nAdded = vsnprintf( Vec_StrLimit(vBuf), nSize, format, args );
+    if ( nAdded > nSize )
+    {
+        Vec_StrGrow( vBuf, Vec_StrSize(vBuf) + nAdded + nSize );
+        nSize = vsnprintf( Vec_StrLimit(vBuf), nAdded, format, args );
+        assert( nSize == nAdded );
+    }
+    va_end( args );
+    return Abc_NamStrFindOrAddLim( p, Vec_StrLimit(vBuf), Vec_StrLimit(vBuf) + nAdded, NULL );
+}
+static inline int Acb_ManNewConstId( Acb_Ntk_t * p, Vec_Str_t * vBits ) 
+{ 
+    Vec_Str_t * vOut = Abc_NamBuffer(Acb_NtkNam(p)); 
+    Vec_StrPrintF( vOut, "%d\'b%s", Vec_StrSize(vBits)-1, Vec_StrArray(vBits) );
+    return Abc_NamStrFindOrAdd(p->pDesign->pFuns, Vec_StrArray(vOut), NULL);
+}
+static inline int Acb_ManNewConstZero( Acb_Ntk_t * p, int nBits ) 
+{ 
+    Vec_Str_t * vOut = Abc_NamBuffer(Acb_NtkNam(p)); 
+    Vec_StrPrintF( vOut, "%d\'b%0s", nBits, "" );
+    return Abc_NamStrFindOrAdd(p->pDesign->pFuns, Vec_StrArray(vOut), NULL);
+}
+static inline void Acb_NtkAdd( Acb_Man_t * p, Acb_Ntk_t * pNtk )
+{    
+    int fFound, NtkId = Abc_NamStrFindOrAdd( p->pMods, Acb_NtkName(pNtk), &fFound );
+    if ( fFound )
+        printf( "Network with name \"%s\" already exists.\n", Acb_NtkName(pNtk) );
+    else
+        assert( NtkId == pNtk->Id );
+}
+static inline void Acb_NtkUpdate( Acb_Man_t * p, Acb_Ntk_t * pNtk )
+{
+    int fFound, NtkId = Abc_NamStrFindOrAdd( p->pMods, Acb_NtkName(pNtk), &fFound );
+    if ( !fFound )
+        printf( "Network with name \"%s\" does not exist.\n", Acb_NtkName(pNtk) );
+    else
+    {
+        Acb_NtkFree( Acb_ManNtk(p, NtkId) );
+        Vec_PtrWriteEntry( &p->vNtks, NtkId, pNtk );
+    }
+}
+static inline Vec_Int_t * Acb_NtkCollect( Acb_Ntk_t * p )
+{
+    int iObj;
+    Vec_Int_t * vObjs = Vec_IntAlloc( Acb_NtkObjNum(p) );
+    Acb_NtkForEachObj( p, iObj )
+        Vec_IntPush( vObjs, iObj );
+    return vObjs;
+}
+static inline int Acb_NtkIsSeq( Acb_Ntk_t * p )
+{
+    int iObj;
+    if ( p->fSeq )
+        return 1;
+    if ( p->fComb )
+        return 0;
+    assert( !p->fSeq && !p->fComb );
+    Acb_NtkForEachBox( p, iObj )
+        if ( Acb_ObjIsBox(p, iObj) )
+        {
+            if ( Acb_NtkIsSeq( Acb_ObjNtk(p, iObj) ) )
+            {
+                p->fSeq = 1;
+                return 1;
+            }
+        }
+        else if ( Acb_ObjIsSeq(p, iObj) )
+        {
+            p->fSeq = 1;
+            return 1;
+        }
+    p->fComb = 1;
+    return 0;
+}
+static inline void Acb_NtkPrepareSeq( Acb_Ntk_t * p )
+{
+    int iObj;
+    assert( Acb_NtkSeqNum(p) == 0 );
+    if ( !Acb_NtkIsSeq(p) )
+        return;
+    Acb_NtkForEachBox( p, iObj )
+        if ( Acb_ObjIsSeq(p, iObj) )
+            Vec_IntPush( &p->vSeq, iObj );
+    // Acb_NtkObjOrder( p, &p->vSeq, NULL );
+}
+static inline Acb_Ntk_t * Acb_NtkDup( Acb_Man_t * pMan, Acb_Ntk_t * p, Vec_Int_t * vObjs )
+{
+    Acb_Ntk_t * pNew;
+    int i, k, iObj, iObjNew, iFanin;
+    pNew = Acb_NtkAlloc( pMan, Acb_NtkNameId(p), Acb_NtkCiNum(p), Acb_NtkCoNum(p), Vec_IntSize(vObjs) );
+    Acb_NtkCleanObjCopies( p );
+    Vec_IntForEachEntry( vObjs, iObj, i )
+        iObjNew = Acb_ObjDup( pNew, p, iObj );
+    Vec_IntForEachEntry( vObjs, iObj, i )
+    {
+        iObjNew = Acb_ObjCopy( p, iObj );
+        Acb_ObjForEachFanin( p, iObj, iFanin, k )
+            Acb_ObjAddFanin( pNew, iObjNew, Acb_ObjCopy(p, iFanin) );
+    }
+    //Acb_NtkFreeObjCopies( p );
+    assert( Acb_NtkObjNum(pNew) == Acb_NtkObjNumAlloc(pNew) );
+    Acb_NtkSetCopy( p, Acb_NtkId(pNew) );
+    Acb_NtkSetRegNum( pNew, Acb_NtkRegNum(p) );
+    return pNew;
+}
+static inline Acb_Ntk_t * Acb_NtkDupOrder( Acb_Man_t * pMan, Acb_Ntk_t * p, Vec_Int_t*(* pFuncOrder)(Acb_Ntk_t*) )
+{
+    Acb_Ntk_t * pNew;
+    Vec_Int_t * vObjs = pFuncOrder ? pFuncOrder(p) : Acb_NtkCollect(p);
+    if ( vObjs == NULL )
+        return NULL;
+    pNew = Acb_NtkDup( pMan, p, vObjs );
+    Vec_IntFree( vObjs );
+    //Acb_NtkPrepareSeq( pNew );
+    return pNew;
+}
+static inline void Acb_NtkDupAttrs( Acb_Ntk_t * pNew, Acb_Ntk_t * p )
+{
+    int i, iObj;
+    assert( Vec_IntSize(&pNew->vOrder) == 0 );
+    Acb_NtkForEachCioOrder( p, iObj, i )
+        Vec_IntPush( &pNew->vOrder, Acb_ObjCopy(p, iObj) );
+//    Vec_IntRemapArray( &p->vObjCopy, &p->vOrder,    &pNew->vOrder,    Acb_NtkCioOrderNum(p) );
+//    Vec_IntRemapArray( &p->vObjCopy, &p->vSeq,      &pNew->vSeq,      Acb_NtkSeqNum(p) );
+    // transfer object attributes
+    Vec_IntRemapArray( &p->vObjCopy, &p->vObjFunc,   &pNew->vObjFunc,   Acb_NtkObjNum(pNew) + 1 );
+    Vec_IntRemapArray( &p->vObjCopy, &p->vObjWeight, &pNew->vObjWeight, Acb_NtkObjNum(pNew) + 1 );
+//    Vec_WrdRemapArray( &p->vObjCopy, &p->vObjTruth,  &pNew->vObjTruth,  Acb_NtkObjNum(pNew) + 1 );
+    Vec_IntRemapArray( &p->vObjCopy, &p->vObjName,   &pNew->vObjName,   Acb_NtkObjNum(pNew) + 1 );
+    Vec_IntRemapArray( &p->vObjCopy, &p->vObjRange,  &pNew->vObjRange,  Acb_NtkObjNum(pNew) + 1 );
+    Vec_IntRemapArray( &p->vObjCopy, &p->vObjAttr,   &pNew->vObjAttr,   Acb_NtkObjNum(pNew) + 1 );
+    // duplicate attributes
+    Vec_IntAppend( &pNew->vAttrSto, &p->vAttrSto );
+}
+static inline int Acb_NtkMemory( Acb_Ntk_t * p )
+{
+    int nMem = sizeof(Acb_Ntk_t);
+    // interface
+    nMem += (int)Vec_IntMemory(&p->vCis);
+    nMem += (int)Vec_IntMemory(&p->vCos);
+    nMem += (int)Vec_IntMemory(&p->vOrder);
+    nMem += (int)Vec_IntMemory(&p->vSeq);
+    // stucture
+    nMem += (int)Vec_StrMemory(&p->vObjType);
+    nMem += (int)Vec_IntMemory(&p->vObjFans);
+    nMem += (int)Vec_IntMemory(&p->vFanSto);
+    nMem += (int)Vec_WecMemory(&p->vFanouts);
+    // optional
+    nMem += (int)Vec_IntMemory(&p->vObjCopy );  
+    nMem += (int)Vec_IntMemory(&p->vObjFunc );  
+    nMem += (int)Vec_IntMemory(&p->vObjWeight );  
+    nMem += (int)Vec_WrdMemory(&p->vObjTruth );  
+    nMem += (int)Vec_IntMemory(&p->vObjName );  
+    nMem += (int)Vec_IntMemory(&p->vObjRange );  
+    nMem += (int)Vec_IntMemory(&p->vObjTrav );  
+    nMem += (int)Vec_IntMemory(&p->vObjBits );  
+    nMem += (int)Vec_IntMemory(&p->vObjAttr );  
+    nMem += (int)Vec_IntMemory(&p->vAttrSto );  
+    nMem += (int)Vec_IntMemory(&p->vNtkObjs );  
+    nMem += (int)Vec_IntMemory(&p->vTargets );  
+    // other
+    nMem += (int)Vec_IntMemory(&p->vArray1 );
+    nMem += (int)Vec_IntMemory(&p->vArray1 );
+    return nMem;
+}
+static inline void Acb_NtkPrintStats( Acb_Ntk_t * p )
+{
+    printf( "pi =%5d  ",   Acb_NtkPiNum(p) );
+    printf( "po =%5d  ",   Acb_NtkPoNum(p) );
+    printf( "ff =%5d  ",   Acb_NtkRegNum(p) );
+    printf( "node =%5d  ", Acb_NtkNodeNum(p) );
+    printf( "box =%5d  ",  Acb_NtkBoxNum(p) );
+    //printf( "topo =%4s  ", Acb_NtkIsTopoOrder(p) ? "yes" : "no" );
+    printf( "  %s ",       Acb_NtkName(p) );
+    if ( Vec_IntSize(&p->vNtkObjs) )
+        printf( "-> %s",   Acb_NtkName(Acb_NtkNtk(p, Vec_IntEntry(&p->vNtkObjs, 0))) );
+    printf( "\n" );
+//    Vec_StrIntPrint( &p->vObjType );
+}
+static inline void Acb_NtkPrint( Acb_Ntk_t * p )
+{
+    int i, Type;
+    printf( "Interface (%d):\n", Acb_NtkCioNum(p) );
+    printf( "Objects (%d):\n", Acb_NtkObjNum(p) );
+    Acb_NtkForEachObjType( p, Type, i )
+    {
+        printf( "%6d : ", i );
+        printf( "Type =%3d  ", Type );
+        printf( "Fanins = %d  ", Acb_ObjFaninNum(p, i) );
+        if ( Acb_NtkHasObjNames(p) && Acb_ObjName(p, i) )
+            printf( "%s", Acb_ObjNameStr(p, i) );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Manager APIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Acb_Man_t * Acb_ManAlloc( char * pFileName, int nNtks, Abc_Nam_t * pStrs, Abc_Nam_t * pFuns, Abc_Nam_t * pMods, Hash_IntMan_t * vHash )
+{
+    Acb_Man_t * pNew = ABC_CALLOC( Acb_Man_t, 1 );
+    pNew->pName = Extra_FileDesignName( pFileName );
+    pNew->pSpec = Abc_UtilStrsav( pFileName );
+    pNew->pStrs = pStrs ? pStrs : Abc_NamStart( 1000, 24 );
+    pNew->pFuns = pFuns ? pFuns : Abc_NamStart( 100, 24 );
+    pNew->pMods = pMods ? pMods : Abc_NamStart( 100, 24 );
+    pNew->vHash = vHash ? vHash : Hash_IntManStart( 1000 );
+    if ( pFuns == NULL )
+    {
+        Abc_NamStrFindOrAdd(pNew->pFuns, "1\'b0", NULL);
+        Abc_NamStrFindOrAdd(pNew->pFuns, "1\'b1", NULL);
+        Abc_NamStrFindOrAdd(pNew->pFuns, "1\'bx", NULL);
+        Abc_NamStrFindOrAdd(pNew->pFuns, "1\'bz", NULL);
+    }
+//    if ( vHash == NULL )
+//        Hash_Int2ManInsert( pNew->vHash, 0, 0, 0 );
+    Vec_PtrGrow( &pNew->vNtks,  nNtks+1 ); Vec_PtrPush( &pNew->vNtks, NULL );
+    // set default root module
+    pNew->iRoot = 1;
+    return pNew;
+}
+static inline void Acb_ManDupTypeNames( Acb_Man_t * pNew, Acb_Man_t * p )
+{
+   memcpy( pNew->pTypeNames, p->pTypeNames, sizeof(void *) * ABC_OPER_LAST );
+}
+static inline Acb_Man_t * Acb_ManDup( Acb_Man_t * p, Vec_Int_t*(* pFuncOrder)(Acb_Ntk_t*) )
+{
+    Acb_Ntk_t * pNtk, * pNtkNew; int i;
+    Acb_Man_t * pNew = Acb_ManAlloc( p->pSpec, Acb_ManNtkNum(p), Abc_NamRef(p->pStrs), Abc_NamRef(p->pFuns), Abc_NamStart(100, 24), Hash_IntManRef(p->vHash) );
+    Acb_ManDupTypeNames( pNew, p );
+    Acb_ManForEachNtk( p, pNtk, i )
+    {
+        pNtkNew = Acb_NtkDupOrder( pNew, pNtk, pFuncOrder );
+        Acb_NtkAdd( pNew, pNtkNew );
+        Acb_NtkDupAttrs( pNtkNew, pNtk );
+    }
+//    Acb_ManForEachNtk( p, pNtk, i )
+//        if ( (pHost = Acb_NtkHostNtk(pNtk)) )
+//            Acb_NtkSetHost( Acb_NtkCopyNtk(pNew, pNtk), Acb_NtkCopy(pHost), Acb_ObjCopy(pHost, Acb_NtkHostObj(pNtk)) );
+    pNew->iRoot = Acb_ManNtkNum(pNew);
+    return pNew;
+}
+static inline void Acb_ManPrepareSeq( Acb_Man_t * p )
+{
+    Acb_Ntk_t * pNtk; int i;
+    Acb_ManForEachNtk( p, pNtk, i )
+        Acb_NtkPrepareSeq( pNtk );
+}
+static inline void Acb_ManFree( Acb_Man_t * p )
+{
+    Acb_Ntk_t * pNtk; int i;
+    Acb_ManForEachNtk( p, pNtk, i )
+        Acb_NtkFree( pNtk );
+    ABC_FREE( p->vNtks.pArray );
+    Abc_NamDeref( p->pStrs );
+    Abc_NamDeref( p->pFuns );
+    Abc_NamDeref( p->pMods );
+    Hash_IntManDeref( p->vHash );
+    Vec_IntErase( &p->vNameMap );
+    Vec_IntErase( &p->vUsed );
+    Vec_IntErase( &p->vNameMap2 );
+    Vec_IntErase( &p->vUsed2 );
+    Vec_StrErase( &p->vOut );
+    Vec_StrErase( &p->vOut2 );
+    ABC_FREE( p->pName );
+    ABC_FREE( p->pSpec );
+    ABC_FREE( p );
+}
+static inline int Acb_ManGetMap( Acb_Man_t * p, int i )
+{
+    return Vec_IntGetEntry(&p->vNameMap, i);
+}
+static inline void Acb_ManSetMap( Acb_Man_t * p, int i, int x )
+{
+    assert( Vec_IntGetEntry(&p->vNameMap, i) == 0 );
+    Vec_IntSetEntry( &p->vNameMap, i, x );
+    Vec_IntPush( &p->vUsed, i );
+}
+static inline void Acb_ManUnsetMap( Acb_Man_t * p, int i )
+{
+    Vec_IntSetEntry( &p->vNameMap, i, 0 );
+}
+static inline void Acb_ManCleanMap( Acb_Man_t * p )
+{
+    int i, Entry;
+    Vec_IntForEachEntry( &p->vUsed, Entry, i )
+        Vec_IntWriteEntry( &p->vNameMap, Entry, 0 );
+    Vec_IntClear( &p->vUsed );
+}
+static inline int  Acb_NtkGetMap( Acb_Ntk_t * p, int i )          { return Acb_ManGetMap(p->pDesign, i); }
+static inline void Acb_NtkSetMap( Acb_Ntk_t * p, int i, int x )   { Acb_ManSetMap(p->pDesign, i, x);     }
+static inline void Acb_NtkUnsetMap( Acb_Ntk_t * p, int i )        { Acb_ManUnsetMap(p->pDesign, i);      }
+static inline void Acb_NtkCleanMap( Acb_Ntk_t * p )               { Acb_ManCleanMap(p->pDesign);         }
+
+static inline int Acb_ManGetMap2( Acb_Man_t * p, int i )
+{
+    return Vec_IntGetEntry(&p->vNameMap2, i);
+}
+static inline void Acb_ManSetMap2( Acb_Man_t * p, int i, int x )
+{
+    assert( Vec_IntGetEntry(&p->vNameMap2, i) == 0 );
+    Vec_IntSetEntry( &p->vNameMap2, i, x );
+    Vec_IntPush( &p->vUsed2, i );
+}
+static inline void Acb_ManUnsetMap2( Acb_Man_t * p, int i )
+{
+    Vec_IntSetEntry( &p->vNameMap2, i, 0 );
+}
+static inline void Acb_ManCleanMap2( Acb_Man_t * p )
+{
+    int i, Entry;
+    Vec_IntForEachEntry( &p->vUsed2, Entry, i )
+        Vec_IntWriteEntry( &p->vNameMap2, Entry, 0 );
+    Vec_IntClear( &p->vUsed2 );
+}
+static inline int  Acb_NtkGetMap2( Acb_Ntk_t * p, int i )          { return Acb_ManGetMap2(p->pDesign, i); }
+static inline void Acb_NtkSetMap2( Acb_Ntk_t * p, int i, int x )   { Acb_ManSetMap2(p->pDesign, i, x);     }
+static inline void Acb_NtkUnsetMap2( Acb_Ntk_t * p, int i )        { Acb_ManUnsetMap2(p->pDesign, i);      }
+static inline void Acb_NtkCleanMap2( Acb_Ntk_t * p )               { Acb_ManCleanMap2(p->pDesign);         }
+
+static inline int Acb_ManMemory( Acb_Man_t * p )
+{
+    Acb_Ntk_t * pNtk; int i;
+    int nMem = sizeof(Acb_Man_t);
+    nMem += p->pName ? (int)strlen(p->pName) : 0;
+    nMem += p->pSpec ? (int)strlen(p->pSpec) : 0;
+    nMem += Abc_NamMemUsed(p->pStrs);
+    nMem += Abc_NamMemUsed(p->pFuns);
+    nMem += Abc_NamMemUsed(p->pMods);
+    nMem += (int)Vec_IntMemory(&p->vNameMap );   
+    nMem += (int)Vec_IntMemory(&p->vUsed );  
+    nMem += (int)Vec_StrMemory(&p->vOut );   
+    nMem += (int)Vec_StrMemory(&p->vOut2 );  
+    nMem += (int)Vec_PtrMemory(&p->vNtks);
+    Acb_ManForEachNtk( p, pNtk, i )
+        nMem += Acb_NtkMemory( pNtk );
+    return nMem;
+}
+static inline int Acb_ManObjNum( Acb_Man_t * p )
+{
+    Acb_Ntk_t * pNtk; int i, Count = 0;
+    Acb_ManForEachNtk( p, pNtk, i )
+        Count += Acb_NtkObjNum(pNtk);
+    return Count;
+}
+static inline int Acb_ManBoxNum( Acb_Man_t * p )
+{
+    Acb_Ntk_t * pNtk; int i, Count = 0;
+    Acb_ManForEachNtk( p, pNtk, i )
+        Count += Acb_NtkBoxNum( pNtk );
+    return Count;
+}
+static inline void Acb_ManBoxNumRec_rec( Acb_Ntk_t * p, int * pCountP, int * pCountU )
+{
+    int iObj, Id = Acb_NtkId(p);
+    if ( pCountP[Id] >= 0 )
+        return;
+    pCountP[Id] = pCountU[Id] = 0;
+    Acb_NtkForEachObj( p, iObj )
+    {
+        if ( Acb_ObjIsBox(p, iObj) )
+        {
+            Acb_ManBoxNumRec_rec( Acb_ObjNtk(p, iObj), pCountP, pCountU );
+            pCountP[Id] += pCountP[Acb_ObjNtkId(p, iObj)];
+            pCountU[Id] += pCountU[Acb_ObjNtkId(p, iObj)] + 1;
+        }
+        else
+            pCountP[Id] += 1;
+    }
+}
+static inline void Acb_ManBoxNumRec( Acb_Man_t * p, int * pnPrims, int * pnUsers )
+{
+    Acb_Ntk_t * pNtk = Acb_ManRoot(p);
+    int * pCountP = ABC_FALLOC( int, Acb_ManNtkNum(p) + 1 );
+    int * pCountU = ABC_FALLOC( int, Acb_ManNtkNum(p) + 1 );
+    Acb_ManBoxNumRec_rec( pNtk, pCountP, pCountU );
+    *pnPrims = pCountP[Acb_NtkId(pNtk)];
+    *pnUsers = pCountU[Acb_NtkId(pNtk)];
+    ABC_FREE( pCountP );
+    ABC_FREE( pCountU );
+}
+static inline void Acb_ManPrintStats( Acb_Man_t * p, int nModules, int fVerbose )
+{
+    Acb_Ntk_t * pNtk; int i, nPrims, nUsers;
+    Acb_Ntk_t * pRoot = Acb_ManRoot( p );
+    Acb_ManBoxNumRec( p, &nPrims, &nUsers );
+    printf( "%-12s : ",     Acb_ManName(p) );
+    printf( "pi =%5d  ",    Acb_NtkCiNum(pRoot) );
+    printf( "po =%5d  ",    Acb_NtkCoNum(pRoot) );
+    printf( "mod =%5d  ",   Acb_ManNtkNum(p) );
+    printf( "box =%5d  ",   nPrims + nUsers );
+    printf( "prim =%5d  ",  nPrims );
+    printf( "user =%5d  ",  nUsers );
+    printf( "mem =%6.3f MB", 1.0*Acb_ManMemory(p)/(1<<20) );
+    printf( "\n" );
+    Acb_ManForEachNtk( p, pNtk, i )
+    {
+        if ( i == nModules+1 )
+            break;
+        printf( "Module %5d : ", i );
+        Acb_NtkPrintStats( pNtk );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Name handling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+static inline void Acb_NtkAddMissingFonNames( Acb_Ntk_t * p, char * pPref )
+{
+    int iFon, NameId, Index;
+    // populate map
+    Acb_ManCleanMap( p->pDesign );
+    Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
+        if ( NameId )
+            Acb_ManSetMap( p->pDesign, NameId, iFon );
+    // check remaining ones
+    Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
+    {
+        if ( NameId )
+            continue;
+        NameId = Acb_NtkNewStrId(p, "%s%d", pPref, iFon);
+        for ( Index = 1; Acb_ManGetMap(p->pDesign, NameId); Index++ )
+            NameId = Acb_NtkNewStrId(p, "%s%d_%d", pPref, iFon, Index);
+        Acb_FonSetName( p, iFon, NameId );
+        Acb_ManSetMap( p->pDesign, NameId, iFon );
+    }
+}
+static inline void Acb_NtkCreateFonNames( Acb_Ntk_t * p, char * pPref )
+{
+    int i, iObj, iFon;//, NameId;
+    Acb_NtkCleanFonNames( p );
+    Acb_NtkForEachPiFon( p, iObj, iFon, i )
+        if ( !Acb_FonName(p, iFon) )
+            Acb_FonSetName( p, iFon, Acb_ObjName(p, iObj) );
+    Acb_NtkForEachPoDriverFon( p, iObj, iFon, i )
+        if ( Acb_FonIsReal(iFon) && !Acb_FonName(p, iFon) )
+            Acb_FonSetName( p, iFon, Acb_ObjName(p, iObj) );
+//    Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
+//        if ( NameId == 0 )
+//            Vec_IntWriteEntry( &p->vFonName, iFon, Acb_NtkNewStrId(p, "%s%d", pPref, iFon) );
+    Acb_NtkAddMissingFonNames( p, pPref );
+}
+static inline void Acb_NtkMissingFonNames( Acb_Ntk_t * p, char * pPref )
+{
+    int i, iObj, iFon;//, NameId;
+    Acb_NtkForEachPiFon( p, iObj, iFon, i )
+        if ( !Acb_FonName(p, iFon) )
+            Acb_FonSetName( p, iFon, Acb_ObjName(p, iObj) );
+    Acb_NtkForEachPoDriverFon( p, iObj, iFon, i )
+        if ( Acb_FonIsReal(iFon) && !Acb_FonName(p, iFon) )
+            Acb_FonSetName( p, iFon, Acb_ObjName(p, iObj) );
+//    Vec_IntForEachEntryStart( &p->vFonName, NameId, iFon, 1 )
+//        if ( NameId == 0 )
+//            Acb_FonSetName( p, iFon, Acb_NtkNewStrId(p, "%s%d", pPref, iFon) );
+    Acb_NtkAddMissingFonNames( p, pPref );
+}
+*/
+
+
+/*=== acbBlast.c =============================================================*/
+extern Gia_Man_t *   Acb_ManBlast( Acb_Man_t * p, int fBarBufs, int fSeq, int fVerbose );
+extern Acb_Man_t *   Acb_ManInsertGia( Acb_Man_t * p, Gia_Man_t * pGia );
+extern Acb_Man_t *   Acb_ManInsertAbc( Acb_Man_t * p, void * pAbc );
+/*=== acbCba.c ===============================================================*/
+extern Acb_Man_t *   Acb_ManReadCba( char * pFileName );
+extern void          Acb_ManWriteCba( char * pFileName, Acb_Man_t * p );
+/*=== acbCom.c ===============================================================*/
+/*=== acbNtk.c ===============================================================*/
+extern void          Acb_NtkPrintStatsFull( Acb_Ntk_t * p, int fDistrib, int fVerbose );
+extern void          Acb_NtkPrintNodes( Acb_Ntk_t * p, int Type );
+extern void          Acb_NtkPrintDistribOld( Acb_Ntk_t * p );
+extern void          Acb_ManPrintDistrib( Acb_Man_t * p );
+//extern void           Acb_ManPrepareTypeNames( Acb_Man_t * p );
+extern void          Acb_NtkObjOrder( Acb_Ntk_t * p, Vec_Int_t * vObjs, Vec_Int_t * vNameIds );
+extern int           Acb_NtkCiFonNum( Acb_Ntk_t * p );
+extern int           Acb_NtkCoFinNum( Acb_Ntk_t * p );
+extern int           Acb_NtkCheckComboLoop( Acb_Ntk_t * p );
+extern int           Acb_ManIsTopoOrder( Acb_Man_t * p );
+extern Vec_Int_t *   Acb_NtkCollectDfs( Acb_Ntk_t * p );
+extern Acb_Man_t *   Acb_ManCollapse( Acb_Man_t * p );
+extern Acb_Man_t *   Acb_ManExtractGroup( Acb_Man_t * p, Vec_Int_t * vObjs );
+extern Acb_Man_t *   Acb_ManDeriveFromGia( Acb_Man_t * p, Gia_Man_t * pGia, int fUseXor );
+extern Acb_Man_t *   Acb_ManInsertGroup( Acb_Man_t * p, Vec_Int_t * vObjs, Acb_Ntk_t * pSyn );
+/*=== acbReadBlif.c ==========================================================*/
+extern Acb_Man_t *   Prs_ManBuildCbaBlif( char * pFileName, Vec_Ptr_t * vDes );
+extern void          Prs_ManReadBlifTest( char * pFileName );
+extern Acb_Man_t *   Acb_ManReadBlif( char * pFileName );
+/*=== acbReadVer.c ===========================================================*/
+extern Acb_Man_t *   Prs_ManBuildCbaVerilog( char * pFileName, Vec_Ptr_t * vDes );
+extern void          Prs_ManReadVerilogTest( char * pFileName );
+extern Acb_Man_t *   Acb_ManReadVerilog( char * pFileName );
+/*=== acbWriteBlif.c =========================================================*/
+extern void          Prs_ManWriteBlif( char * pFileName, Vec_Ptr_t * p );
+extern void          Acb_ManWriteBlif( char * pFileName, Acb_Man_t * p );
+/*=== acbWriteVer.c ==========================================================*/
+extern void          Acb_ManCreatePrimMap( char ** pMap );
+extern char *        Acb_ManGetSliceName( Acb_Ntk_t * p, int iFon, int RangeId );
+extern void          Prs_ManWriteVerilog( char * pFileName, Vec_Ptr_t * p );
+extern void          Acb_ManWriteVerilog( char * pFileName, Acb_Man_t * p, int fInlineConcat );
+
+ABC_NAMESPACE_HEADER_END
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/acb/acbAbc.c b/src/base/acb/acbAbc.c
new file mode 100644
index 00000000..7aba364e
--- /dev/null
+++ b/src/base/acb/acbAbc.c
@@ -0,0 +1,153 @@
+/**CFile****************************************************************
+
+  FileName    [acbAbc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    [Bridge.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 21, 2015.]
+
+  Revision    [$Id: acbAbc.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acb.h"
+#include "base/abc/abc.h"
+#include "aig/miniaig/ndr.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p )
+{
+    Acb_Man_t * pMan = Acb_ManAlloc( Abc_NtkSpec(p), 1, NULL, NULL, NULL, NULL );
+    int i, k, NameId = Abc_NamStrFindOrAdd( pMan->pStrs, Abc_NtkName(p), NULL );
+    Acb_Ntk_t * pNtk = Acb_NtkAlloc( pMan, NameId, Abc_NtkCiNum(p), Abc_NtkCoNum(p), Abc_NtkObjNum(p) );
+    Abc_Obj_t * pObj, * pFanin;
+    assert( Abc_NtkIsSopLogic(p) );
+    Abc_NtkForEachCi( p, pObj, i )
+        pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 );
+    Abc_NtkForEachNode( p, pObj, i )
+        pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_LUT, Abc_ObjFaninNum(pObj), 0 );
+    Abc_NtkForEachCo( p, pObj, i )
+        pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CO, 1, 0 );
+    Abc_NtkForEachNode( p, pObj, i )
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Acb_ObjAddFanin( pNtk, pObj->iTemp, pFanin->iTemp );
+    Abc_NtkForEachCo( p, pObj, i )
+        Acb_ObjAddFanin( pNtk, pObj->iTemp, Abc_ObjFanin(pObj, 0)->iTemp );
+    Acb_NtkCleanObjTruths( pNtk );
+    Abc_NtkForEachNode( p, pObj, i )
+        Acb_ObjSetTruth( pNtk, pObj->iTemp, Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj)) );
+    Acb_NtkSetRegNum( pNtk, Abc_NtkLatchNum(p) );
+    Acb_NtkAdd( pMan, pNtk );
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames, Vec_Int_t * vWeights, int nNameIdMax )
+{
+    Ndr_Data_t * p   = (Ndr_Data_t *)pModule; 
+    Acb_Man_t * pMan = Acb_ManAlloc( pFileName, 1, Abc_NamRef(pNames), NULL, NULL, NULL );
+    int k, NameId = Abc_NamStrFindOrAdd( pMan->pStrs, pMan->pName, NULL );
+    int Mod = 0, Obj, Type, nArray, * pArray, ObjId;
+    Acb_Ntk_t * pNtk = Acb_NtkAlloc( pMan, NameId, Ndr_DataCiNum(p, Mod), Ndr_DataCoNum(p, Mod), Ndr_DataObjNum(p, Mod) );
+    Vec_Int_t * vMap = Vec_IntStart( nNameIdMax );
+    Acb_NtkCleanObjWeights( pNtk );
+    Acb_NtkCleanObjNames( pNtk );
+    Ndr_ModForEachPi( p, Mod, Obj )
+    {
+        NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
+        ObjId  = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 );
+        Vec_IntWriteEntry( vMap, NameId, ObjId );
+        Acb_ObjSetName( pNtk, ObjId, NameId );
+    }
+    Ndr_ModForEachPi( p, Mod, Obj )
+    {
+        NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
+        ObjId  = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 );
+        Vec_IntWriteEntry( vMap, NameId, ObjId );
+        Acb_ObjSetName( pNtk, ObjId, NameId );
+    }
+    Ndr_ModForEachTarget( p, Mod, Obj )
+    {
+        NameId = Ndr_DataEntry( p, Obj );
+        ObjId  = Acb_ObjAlloc( pNtk, ABC_OPER_CONST_F, 0, 0 );
+        Vec_IntWriteEntry( vMap, NameId, ObjId );
+        Acb_ObjSetName( pNtk, ObjId, NameId );
+        Vec_IntPush( &pNtk->vTargets, ObjId );
+    }
+    Ndr_ModForEachNode( p, Mod, Obj )
+    {
+        NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
+        nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
+        Type   = Ndr_ObjReadBody( p, Obj, NDR_OPERTYPE );
+        ObjId  = Acb_ObjAlloc( pNtk, Type, nArray, 0 );
+        Vec_IntWriteEntry( vMap, NameId, ObjId );
+        Acb_ObjSetName( pNtk, ObjId, NameId );
+    }
+    Ndr_ModForEachNode( p, Mod, Obj )
+    {
+        NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
+        ObjId  = Vec_IntEntry( vMap, NameId );
+        nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
+        for ( k = 0; k < nArray; k++ )
+            Acb_ObjAddFanin( pNtk, ObjId, Vec_IntEntry(vMap, pArray[k]) );
+        Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 0 );
+    }
+    Ndr_ModForEachPo( p, Mod, Obj )
+    {
+        nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
+        assert( nArray == 1 );
+        ObjId  = Acb_ObjAlloc( pNtk, ABC_OPER_CO, 1, 0 );
+        Acb_ObjAddFanin( pNtk, ObjId, Vec_IntEntry(vMap, pArray[0]) );
+        Acb_ObjSetName( pNtk, ObjId, pArray[0] );
+    }
+    Vec_IntFree( vMap );
+    Acb_NtkSetRegNum( pNtk, 0 );
+    Acb_NtkAdd( pMan, pNtk );
+    return pNtk;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/acb/acbAig.c b/src/base/acb/acbAig.c
new file mode 100644
index 00000000..384c2ba7
--- /dev/null
+++ b/src/base/acb/acbAig.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [acbAig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 21, 2015.]
+
+  Revision    [$Id: acbAig.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acb.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/acb/acbCom.c b/src/base/acb/acbCom.c
new file mode 100644
index 00000000..a9b06c6d
--- /dev/null
+++ b/src/base/acb/acbCom.c
@@ -0,0 +1,731 @@
+/**CFile****************************************************************
+
+  FileName    [acbCom.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    [Command handlers.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 29, 2014.]
+
+  Revision    [$Id: acbCom.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acb.h"
+#include "proof/cec/cec.h"
+#include "base/main/mainInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int  Acb_CommandRead     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Acb_CommandWrite    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Acb_CommandPs       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Acb_CommandPut      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Acb_CommandGet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Acb_CommandClp      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Acb_CommandBlast    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Acb_CommandCec      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Acb_CommandTest     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static inline Acb_Man_t * Acb_AbcGetMan( Abc_Frame_t * pAbc )                   { return (Acb_Man_t *)pAbc->pAbcCba;                        }
+static inline void        Acb_AbcFreeMan( Abc_Frame_t * pAbc )                  { if ( pAbc->pAbcCba ) Acb_ManFree(Acb_AbcGetMan(pAbc));    }
+static inline void        Acb_AbcUpdateMan( Abc_Frame_t * pAbc, Acb_Man_t * p ) { Acb_AbcFreeMan(pAbc); pAbc->pAbcCba = p;                  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Acb_Init( Abc_Frame_t * pAbc )
+{
+    Cmd_CommandAdd( pAbc, "New word level", "@read",       Acb_CommandRead,      0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@write",      Acb_CommandWrite,     0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@ps",         Acb_CommandPs,        0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@put",        Acb_CommandPut,       0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@get",        Acb_CommandGet,       0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@clp",        Acb_CommandClp,       0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@blast",      Acb_CommandBlast,     0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@cec",        Acb_CommandCec,       0 );
+    Cmd_CommandAdd( pAbc, "New word level", "@test",       Acb_CommandTest,      0 );
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Acb_End( Abc_Frame_t * pAbc )
+{
+    Acb_AbcFreeMan( pAbc );
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Acb_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pFile;
+    Acb_Man_t * p = NULL;
+    char * pFileName = NULL;
+    int c, fTest = 0, fDfs = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "tdvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 't':
+            fTest ^= 1;
+            break;
+        case 'd':
+            fDfs ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        printf( "Acb_CommandRead(): Input file name should be given on the command line.\n" );
+        return 0;
+    }
+        // get the file name
+    pFileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".blif", ".smt", ".acb", NULL )) )
+            Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
+        Abc_Print( 1, "\n" );
+        return 0;
+    }
+    fclose( pFile );
+    if ( fTest )
+    {
+        if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" )  )
+            Prs_ManReadBlifTest( pFileName );
+        else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
+            Prs_ManReadVerilogTest( pFileName );
+        else 
+        {
+            printf( "Unrecognized input file extension.\n" );
+            return 0;
+        }
+        return 0;
+    }
+    if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" )  )
+        p = Acb_ManReadBlif( pFileName );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
+        p = Acb_ManReadVerilog( pFileName );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" )  )
+        p = Acb_ManReadCba( pFileName );
+    else 
+    {
+        printf( "Unrecognized input file extension.\n" );
+        return 0;
+    }
+    if ( fDfs )
+    {
+        Acb_Man_t * pTemp;
+        p = Acb_ManDup( pTemp = p, Acb_NtkCollectDfs );
+        Acb_ManFree( pTemp );
+    }
+    Acb_AbcUpdateMan( pAbc, p );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @read [-tdvh] <file_name>\n" );
+    Abc_Print( -2, "\t         reads hierarchical design\n" );
+    Abc_Print( -2, "\t-t     : toggle testing the parser [default = %s]\n", fTest? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle computing DFS ordering [default = %s]\n", fDfs? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Acb_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Acb_Man_t * p = Acb_AbcGetMan(pAbc);
+    char * pFileName = NULL;
+    int fInclineCats =    0;
+    int c, fVerbose  =    0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'c':
+            fInclineCats ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( p == NULL )
+    {
+        Abc_Print( 1, "Acb_CommandWrite(): There is no current design.\n" );
+        return 0;
+    }
+
+    if ( argc == globalUtilOptind + 1 )
+        pFileName = argv[globalUtilOptind];
+    else if ( argc == globalUtilOptind && p )
+    {
+        pFileName = Extra_FileNameGenericAppend( Acb_ManSpec(p) ? Acb_ManSpec(p) : Acb_ManName(p), "_out.v" );
+        printf( "Generated output file name \"%s\".\n", pFileName );
+    }
+    else 
+    {
+        printf( "Output file name should be given on the command line.\n" );
+        return 0;
+    }
+    // perform writing
+    if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" )  )
+        Acb_ManWriteBlif( pFileName, p );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
+        Acb_ManWriteVerilog( pFileName, p, fInclineCats );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" )  )
+        Acb_ManWriteCba( pFileName, p );
+    else 
+    {
+        printf( "Unrecognized output file extension.\n" );
+        return 0;
+    }
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @write [-cvh]\n" );
+    Abc_Print( -2, "\t         writes the design into a file in BLIF or Verilog\n" );
+    Abc_Print( -2, "\t-c     : toggle inlining input concatenations [default = %s]\n",  fInclineCats? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Acb_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Acb_Man_t * p = Acb_AbcGetMan(pAbc);
+    int nModules     = 0;
+    int fShowMulti   = 0;
+    int fShowAdder   = 0;
+    int fDistrib     = 0;
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Mmadvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nModules = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nModules < 0 )
+                goto usage;
+            break;
+        case 'm':
+            fShowMulti ^= 1;
+            break;
+        case 'a':
+            fShowAdder ^= 1;
+            break;
+        case 'd':
+            fDistrib ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( p == NULL )
+    {
+        Abc_Print( 1, "Acb_CommandPs(): There is no current design.\n" );
+        return 0;
+    }
+    if ( nModules )
+    {
+        Acb_ManPrintStats( p, nModules, fVerbose );
+        return 0;
+    }
+    Acb_NtkPrintStatsFull( Acb_ManRoot(p), fDistrib, fVerbose );
+    if ( fShowMulti )
+        Acb_NtkPrintNodes( Acb_ManRoot(p), ABC_OPER_ARI_MUL );
+    if ( fShowAdder )
+        Acb_NtkPrintNodes( Acb_ManRoot(p), ABC_OPER_ARI_ADD );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @ps [-M num] [-madvh]\n" );
+    Abc_Print( -2, "\t         prints statistics\n" );
+    Abc_Print( -2, "\t-M num : the number of first modules to report [default = %d]\n", nModules );
+    Abc_Print( -2, "\t-m     : toggle printing multipliers [default = %s]\n",         fShowMulti? "yes": "no" );
+    Abc_Print( -2, "\t-a     : toggle printing adders [default = %s]\n",              fShowAdder? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle printing distrubition [default = %s]\n",        fDistrib? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Acb_CommandPut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Acb_Man_t * p = Acb_AbcGetMan(pAbc);
+    Gia_Man_t * pGia = NULL;
+    int c, fBarBufs = 1, fSeq = 0, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "bsvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'b':
+            fBarBufs ^= 1;
+            break;
+        case 's':
+            fSeq ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( p == NULL )
+    {
+        Abc_Print( 1, "Acb_CommandPut(): There is no current design.\n" );
+        return 0;
+    }
+    pGia = Acb_ManBlast( p, fBarBufs, fSeq, fVerbose );
+    if ( pGia == NULL )
+    {
+        Abc_Print( 1, "Acb_CommandPut(): Conversion to AIG has failed.\n" );
+        return 0;
+    }
+    Abc_FrameUpdateGia( pAbc, pGia );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @put [-bsvh]\n" );
+    Abc_Print( -2, "\t         extracts AIG from the hierarchical design\n" );
+    Abc_Print( -2, "\t-b     : toggle using barrier buffers [default = %s]\n", fBarBufs? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle blasting sequential elements [default = %s]\n", fSeq? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Acb_CommandGet( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Acb_Man_t * pNew = NULL, * p = Acb_AbcGetMan(pAbc);
+    int c, fMapped = 0, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'm':
+            fMapped ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( p == NULL )
+    {
+        Abc_Print( 1, "Acb_CommandGet(): There is no current design.\n" );
+        return 0;
+    }
+
+    if ( fMapped )
+    {
+        if ( pAbc->pNtkCur == NULL )
+        {
+            Abc_Print( 1, "Acb_CommandGet(): There is no current mapped design.\n" );
+            return 0;
+        }
+        pNew = Acb_ManInsertAbc( p, pAbc->pNtkCur );
+    }
+    else
+    {
+        if ( pAbc->pGia == NULL )
+        {
+            Abc_Print( 1, "Acb_CommandGet(): There is no current AIG.\n" );
+            return 0;
+        }
+        pNew = Acb_ManInsertGia( p, pAbc->pGia );
+    }
+    Acb_AbcUpdateMan( pAbc, pNew );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @get [-mvh]\n" );
+    Abc_Print( -2, "\t         extracts AIG or mapped network into the hierarchical design\n" );
+    Abc_Print( -2, "\t-m     : toggle using mapped network from main-space [default = %s]\n", fMapped? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Acb_CommandClp( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Acb_Man_t * pNew = NULL, * p = Acb_AbcGetMan(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( p == NULL )
+    {
+        Abc_Print( 1, "Acb_CommandGet(): There is no current design.\n" );
+        return 0;
+    }
+    pNew = Acb_ManCollapse( p );
+    Acb_AbcUpdateMan( pAbc, pNew );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @clp [-vh]\n" );
+    Abc_Print( -2, "\t         collapses the current hierarchical design\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Acb_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pNew = NULL;
+    Acb_Man_t * p = Acb_AbcGetMan(pAbc);
+    int c, fSeq = 0, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 's':
+            fSeq ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( p == NULL )
+    {
+        Abc_Print( 1, "Acb_CommandBlast(): There is no current design.\n" );
+        return 0;
+    }
+    pNew = Acb_ManBlast( p, 0, fSeq, fVerbose );
+    if ( pNew == NULL )
+    {
+        Abc_Print( 1, "Acb_CommandBlast(): Bit-blasting has failed.\n" );
+        return 0;
+    }
+    Abc_FrameUpdateGia( pAbc, pNew );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @blast [-svh]\n" );
+    Abc_Print( -2, "\t         performs bit-blasting of the word-level design\n" );
+    Abc_Print( -2, "\t-s     : toggle blasting sequential elements [default = %s]\n", fSeq? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Acb_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Acb_Man_t * p = Acb_AbcGetMan(pAbc), * pTemp;
+    Gia_Man_t * pFirst, * pSecond, * pMiter;
+    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+    char * pFileName, * pStr, ** pArgvNew;
+    int c, nArgcNew, fDumpMiter = 0;
+    FILE * pFile;
+    Cec_ManCecSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( p == NULL )
+    {
+        Abc_Print( 1, "Acb_CommandCec(): There is no current design.\n" );
+        return 0;
+    }
+
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 1 )
+    {
+        if ( p->pSpec == NULL )
+        {
+            Abc_Print( -1, "File name is not given on the command line.\n" );
+            return 1;
+        }
+        pFileName = p->pSpec;
+    }
+    else
+        pFileName = pArgvNew[0];
+    // fix the wrong symbol
+    for ( pStr = pFileName; *pStr; pStr++ )
+        if ( *pStr == '>' )
+            *pStr = '\\';
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        Abc_Print( -1, "Cannot open input file \"%s\". ", pFileName );
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".blif", NULL, NULL, NULL )) )
+            Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
+        Abc_Print( 1, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // extract AIG from the current design
+    pFirst = Acb_ManBlast( p, 0, 0, 0 );
+    if ( pFirst == NULL )
+    {
+        Abc_Print( -1, "Extracting AIG from the current design has failed.\n" );
+        return 0;
+    }
+    // extract AIG from the second design
+
+    if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" )  )
+        pTemp = Acb_ManReadBlif( pFileName );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
+        pTemp = Acb_ManReadVerilog( pFileName );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" )  )
+        pTemp = Acb_ManReadCba( pFileName );
+    else assert( 0 );
+    pSecond = Acb_ManBlast( pTemp, 0, 0, 0 );
+    Acb_ManFree( pTemp );
+    if ( pSecond == NULL )
+    {
+        Gia_ManStop( pFirst );
+        Abc_Print( -1, "Extracting AIG from the original design has failed.\n" );
+        return 0;
+    }
+    // compute the miter
+    pMiter = Gia_ManMiter( pFirst, pSecond, 0, 1, 0, 0, pPars->fVerbose );
+    if ( pMiter )
+    {
+        if ( fDumpMiter )
+        {
+            Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
+            Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+        }
+        pAbc->Status = Cec_ManVerify( pMiter, pPars );
+        //Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
+        Gia_ManStop( pMiter );
+    }
+    Gia_ManStop( pFirst );
+    Gia_ManStop( pSecond );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @cec [-vh]\n" );
+    Abc_Print( -2, "\t         combinational equivalence checking\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Acb_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Acb_Man_t * p = Acb_AbcGetMan(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( p == NULL )
+    {
+        Abc_Print( 1, "Acb_CommandTest(): There is no current design.\n" );
+        return 0;
+    }
+    return 0;
+usage:
+    Abc_Print( -2, "usage: @test [-vh]\n" );
+    Abc_Print( -2, "\t         experiments with word-level networks\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
new file mode 100644
index 00000000..40f37dfd
--- /dev/null
+++ b/src/base/acb/acbFunc.c
@@ -0,0 +1,56 @@
+/**CFile****************************************************************
+
+  FileName    [abcFunc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Experimental procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcFunc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acb.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_NtkTestRun( char * pFileNames[3], int fVerbose )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/acb/module.make b/src/base/acb/module.make
new file mode 100644
index 00000000..038641a1
--- /dev/null
+++ b/src/base/acb/module.make
@@ -0,0 +1,4 @@
+SRC +=    src/base/acb/acbAbc.c \
+    src/base/acb/abcAig.c \
+    src/base/acb/abcCom.c \
+    src/base/acb/acbFunc.c