Merge remote-tracking branch 'upstream/master' into yosys-experimental

.github/workflows/build-posix-cmake.yml

@@ -6,10 +6,10 @@ on:
 
 jobs:
 
-  build-posix:
+  build-posix-cmake:
     strategy:
       matrix:
-        os: [macos-11, ubuntu-latest]
+        os: [macos-latest, ubuntu-latest]
         use_namespace: [false, true]
 
     runs-on: ${{ matrix.os }}
@@ -22,7 +22,7 @@ jobs:
     steps:
 
     - name: Git Checkout
-      uses: actions/checkout@v2
+      uses: actions/checkout@v4
       with:
         submodules: recursive
 
@@ -44,6 +44,10 @@ jobs:
       run: |
         cmake --build build
 
+    - name: Run Unit Tests
+      run: |
+        ctest --output-on-failure
+
     - name: Test Executable
       run: |
         ./build/abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec"
@@ -60,7 +64,7 @@ jobs:
        cp build/abc build/libabc.a staging/
 
     - name: Upload pacakge artifact
-      uses: actions/upload-artifact@v1
+      uses: actions/upload-artifact@v4
       with:
-        name: package
+        name: package-cmake-${{ matrix.os }}-${{ matrix.use_namespace }}
         path: staging/

.github/workflows/build-posix.yml

@@ -22,7 +22,7 @@ jobs:
     steps:
 
     - name: Git Checkout
-      uses: actions/checkout@v2
+      uses: actions/checkout@v4
       with:
         submodules: recursive
 
@@ -60,7 +60,7 @@ jobs:
        cp abc libabc.a staging/
 
     - name: Upload pacakge artifact
-      uses: actions/upload-artifact@v1
+      uses: actions/upload-artifact@v4
       with:
-        name: package
+        name: package-posix-${{ matrix.os }}-${{ matrix.use_namespace }}
         path: staging/

.github/workflows/build-windows.yml

@@ -13,7 +13,7 @@ jobs:
     steps:
 
     - name: Git Checkout
-      uses: actions/checkout@v2
+      uses: actions/checkout@v4
       with:
         submodules: recursive
 
@@ -46,7 +46,7 @@ jobs:
        copy UpgradeLog.htm staging/
 
     - name: Upload pacakge artifact
-      uses: actions/upload-artifact@v1
+      uses: actions/upload-artifact@v4
       with:
-        name: package
+        name: package-windows
         path: staging/

.gitignore

@@ -13,6 +13,7 @@ lib/m114*
 lib/bip*
 docs/
 .vscode/
+.cache/
 
 src/ext*
 src/xxx/

CMakeLists.txt

@@ -112,3 +112,17 @@ add_library(libabc-pic EXCLUDE_FROM_ALL ${ABC_SRC})
 abc_properties(libabc-pic PUBLIC)
 set_property(TARGET libabc-pic PROPERTY POSITION_INDEPENDENT_CODE ON)
 set_property(TARGET libabc-pic PROPERTY OUTPUT_NAME abc-pic)
+
+if(NOT DEFINED ABC_SKIP_TESTS)
+    enable_testing()
+    include(FetchContent)
+    FetchContent_Declare(
+    googletest
+    DOWNLOAD_EXTRACT_TIMESTAMP TRUE
+    # Specify the commit you depend on and update it regularly.
+    URL "https://github.com/google/googletest/archive/refs/tags/v1.14.0.zip"
+    )
+    FetchContent_MakeAvailable(googletest)
+    include(GoogleTest)
+    add_subdirectory(test)
+endif()

src/aig/gia/gia.h

@@ -554,9 +554,11 @@ static inline int          Gia_ObjFaninIdp( Gia_Man_t * p, Gia_Obj_t * pObj, int
 static inline int          Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId )     { return Abc_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); }
 static inline int          Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId )     { return Abc_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); }
 static inline int          Gia_ObjFaninLit2( Gia_Man_t * p, int ObjId )        { return (p->pMuxes && p->pMuxes[ObjId]) ? p->pMuxes[ObjId] : -1;           }
+static inline int          Gia_ObjFaninLit( Gia_Obj_t * pObj, int ObjId, int n ){ return n ? Gia_ObjFaninLit1(pObj, ObjId) : Gia_ObjFaninLit0(pObj, ObjId);}
 static inline int          Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) );    }
 static inline int          Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) );    }
 static inline int          Gia_ObjFaninLit2p( Gia_Man_t * p, Gia_Obj_t * pObj) { return (p->pMuxes && p->pMuxes[Gia_ObjId(p, pObj)]) ? p->pMuxes[Gia_ObjId(p, pObj)] : -1;    }
+static inline int          Gia_ObjFaninLitp( Gia_Man_t * p, Gia_Obj_t * pObj, int n ){ return n ? Gia_ObjFaninLit1p(p, pObj) : Gia_ObjFaninLit0p(p, pObj);}
 static inline void         Gia_ObjFlipFaninC0( Gia_Obj_t * pObj )              { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1;          }
 static inline int          Gia_ObjFaninNum( Gia_Man_t * p, Gia_Obj_t * pObj )  { if ( Gia_ObjIsMux(p, pObj) ) return 3; if ( Gia_ObjIsAnd(pObj) ) return 2; if ( Gia_ObjIsCo(pObj) ) return 1; return 0; }
 static inline int          Gia_ObjWhatFanin( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanin )  { if ( Gia_ObjFanin0(pObj) == pFanin ) return 0; if ( Gia_ObjFanin1(pObj) == pFanin ) return 1; if ( Gia_ObjFanin2(p, pObj) == pFanin ) return 2; assert(0); return -1; }
@@ -1729,6 +1731,7 @@ extern word                Gia_ManRandomW( int fReset );
 extern void                Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop );
 extern char *              Gia_TimeStamp();
 extern char *              Gia_FileNameGenericAppend( char * pBase, char * pSuffix );
+extern Vec_Ptr_t *         Gia_GetFakeNames( int nNames, int fCaps );
 extern void                Gia_ManIncrementTravId( Gia_Man_t * p );
 extern void                Gia_ManCleanMark01( Gia_Man_t * p );
 extern void                Gia_ManSetMark0( Gia_Man_t * p );
@@ -1755,6 +1758,7 @@ extern Vec_Int_t *         Gia_ManReverseLevel( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManRequiredLevel( Gia_Man_t * p );
 extern void                Gia_ManCreateValueRefs( Gia_Man_t * p );
 extern void                Gia_ManCreateRefs( Gia_Man_t * p );
+extern void                Gia_ManCreateLitRefs( Gia_Man_t * p );
 extern int *               Gia_ManCreateMuxRefs( Gia_Man_t * p );
 extern int                 Gia_ManCrossCut( Gia_Man_t * p, int fReverse );
 extern Vec_Int_t *         Gia_ManCollectPoIds( Gia_Man_t * p );

src/aig/gia/giaAiger.c

@@ -1464,6 +1464,18 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in
         Vec_StrFree( vStrExt );
         if ( fVerbose ) printf( "Finished writing extension \"m\".\n" );
     }
+    // write cell mapping
+    if ( Gia_ManHasCellMapping(p) )
+    {
+        extern Vec_Str_t * Gia_AigerWriteCellMappingDoc( Gia_Man_t * p );
+        fprintf( pFile, "M" );
+        vStrExt = Gia_AigerWriteCellMappingDoc( p );
+        Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
+        fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
+        Vec_StrFree( vStrExt );
+        if ( fVerbose ) printf( "Finished writing extension \"M\".\n" );
+
+    }
     // write placement
     if ( p->pPlacement )
     {

src/aig/gia/giaAigerExt.c

@@ -19,6 +19,9 @@
 ***********************************************************************/
 
 #include "gia.h"
+#include "misc/st/st.h"
+#include "map/mio/mio.h"
+#include "map/mio/mioInt.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -288,6 +291,101 @@ Vec_Str_t * Gia_AigerWriteMappingDoc( Gia_Man_t * p )
     return Vec_StrAllocArray( (char *)pBuffer, 4*nSize );
 }
 
+int Gia_AigerWriteCellMappingInstance( Gia_Man_t * p, unsigned char * pBuffer, int nSize2, int i )
+{
+    int k, iFan;
+    if ( !Gia_ObjIsCellInv(p, i) ) {
+        Gia_AigerWriteInt( pBuffer + nSize2, Gia_ObjCellId(p, i) ); nSize2 += 4;
+        Gia_AigerWriteInt( pBuffer + nSize2, i ); nSize2 += 4;
+        Gia_CellForEachFanin( p, i, iFan, k )
+        {
+            Gia_AigerWriteInt( pBuffer + nSize2, iFan );
+            nSize2 += 4;
+        }
+    } else {
+        Gia_AigerWriteInt( pBuffer + nSize2, 3 ); nSize2 += 4;
+        Gia_AigerWriteInt( pBuffer + nSize2, i ); nSize2 += 4;
+        Gia_AigerWriteInt( pBuffer + nSize2, Abc_LitNot(i) ); nSize2 += 4;
+    }
+
+    return nSize2;
+}
+
+Vec_Str_t * Gia_AigerWriteCellMappingDoc( Gia_Man_t * p )
+{
+    unsigned char * pBuffer;
+    int i, iFan, nCells = 0, nInstances = 0, nSize = 8, nSize2 = 0;
+    Mio_Cell2_t * pCells = Mio_CollectRootsNewDefault2( 6, &nCells, 0 );
+    assert( pCells );
+
+    for (int i = 0; i < nCells; i++)
+    {
+        Mio_Gate_t *pGate = (Mio_Gate_t *) pCells[i].pMioGate;
+        Mio_Pin_t *pPin;
+        nSize += strlen(Mio_GateReadName(pGate)) + 1;
+        nSize += strlen(Mio_GateReadOutName(pGate)) + 1 + 4;
+        Mio_GateForEachPin( pGate, pPin )
+            nSize += strlen(Mio_PinReadName(pPin)) + 1;
+    }
+
+    Gia_ManForEachCell( p, i )
+    {
+        assert ( !Gia_ObjIsCellBuf(p, i) ); // not implemented
+        nInstances++;
+        if ( Gia_ObjIsCellInv(p, i) )
+            nSize += 12;
+        else
+            nSize += Gia_ObjCellSize(p, i) * 4 + 8;
+    }
+
+    pBuffer = ABC_ALLOC( unsigned char, nSize );
+    Gia_AigerWriteInt( pBuffer + nSize2, nCells ); nSize2 += 4;
+    Gia_AigerWriteInt( pBuffer + nSize2, nInstances ); nSize2 += 4;
+
+    for (int i = 0; i < nCells; i++)
+    {
+        int nPins = 0;
+        Mio_Gate_t *pGate = (Mio_Gate_t *) pCells[i].pMioGate;
+        Mio_Pin_t *pPin;
+
+        strcpy((char *) pBuffer + nSize2, Mio_GateReadName(pGate));
+        nSize2 += strlen(Mio_GateReadName(pGate)) + 1;
+        strcpy((char *) pBuffer + nSize2, Mio_GateReadOutName(pGate));
+        nSize2 += strlen(Mio_GateReadOutName(pGate)) + 1;
+
+        Mio_GateForEachPin( pGate, pPin )
+            nPins++;
+        Gia_AigerWriteInt( pBuffer + nSize2, nPins ); nSize2 += 4;
+
+        Mio_GateForEachPin( pGate, pPin )
+        {
+            strcpy((char *) pBuffer + nSize2, Mio_PinReadName(pPin));
+            nSize2 += strlen(Mio_PinReadName(pPin)) + 1;
+        }
+    }
+
+    Gia_ManForEachCell( p, i )
+    {
+        if ( Gia_ObjIsCellBuf(p, i) )
+            continue;
+
+        if ( Gia_ObjIsCellInv(p, i) && !Abc_LitIsCompl(i) ) {
+            // swap the order so that the inverter is after the driver
+            // of the inverter's input
+            nSize2 = Gia_AigerWriteCellMappingInstance(p, pBuffer, nSize2, Abc_LitNot(i) );
+            nSize2 = Gia_AigerWriteCellMappingInstance(p, pBuffer, nSize2, i );
+            i += 1;
+            continue;
+        }
+
+        nSize2 = Gia_AigerWriteCellMappingInstance(p, pBuffer, nSize2, i );
+    }
+
+    assert( nSize2 == nSize );
+    ABC_FREE( pCells );
+    return Vec_StrAllocArray( (char *)pBuffer, nSize );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Read/write packing information.]

src/aig/gia/giaClp.c

@@ -42,42 +42,6 @@ extern int Gia_ManFactorNode( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves );
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Gia_GetFakeNames( int nNames )
-{
-    Vec_Ptr_t * vNames;
-    char Buffer[5];
-    int i;
-
-    vNames = Vec_PtrAlloc( nNames );
-    for ( i = 0; i < nNames; i++ )
-    {
-        if ( nNames < 26 )
-        {
-            Buffer[0] = 'a' + i;
-            Buffer[1] = 0;
-        }
-        else
-        {
-            Buffer[0] = 'a' + i%26;
-            Buffer[1] = '0' + i/26;
-            Buffer[2] = 0;
-        }
-        Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) );
-    }
-    return vNames;
-}
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -378,8 +342,8 @@ Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
     Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
     if ( fVerbose )
     {
-        Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) );
-        Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
+        Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p), 0 );
+        Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p), 1 );
         char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
         char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
         Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, 0 );
@@ -404,6 +368,41 @@ void Gia_ManCollapseTestTest( Gia_Man_t * p )
     Gia_ManStop( pNew );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintDsdOne( Dsd_Manager_t * pManDsd, int Output, int OffSet )
+{
+    Vec_Str_t * vStr = Vec_StrAlloc( 100 );
+    Dsd_TreePrint4( vStr, pManDsd, Output );
+    for ( int i = 0; i < OffSet; i++ )
+        printf( " " );
+    printf( "Supp %2d  nDsd %2d  %s\n", Dsd_TreeSuppSize(pManDsd, Output), Dsd_TreeNonDsdMax(pManDsd, Output), Vec_StrArray(vStr) );
+    Vec_StrFree( vStr );
+    fflush( stdout );      
+}
+void Gia_ManPrintDsd( Dsd_Manager_t * pManDsd, int Output, int nOutputs, int OffSet )
+{
+    if ( Output == -1 )
+    {
+        for ( int i = 0; i < nOutputs; i++ )
+            Gia_ManPrintDsdOne( pManDsd, i, OffSet );
+    }
+    else 
+    {
+        assert( Output >= 0 && Output < nOutputs );
+        Gia_ManPrintDsdOne( pManDsd, Output, OffSet );
+    }  
+}
+
 void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
 {
     DdManager * dd;
@@ -425,22 +424,89 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
         Cudd_Quit( dd );
         return;
     }
-    Dsd_Decompose( pManDsd, (DdNode **)vFuncs->pArray, Gia_ManCoNum(p) );
+    Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
+    
     if ( fVerbose )
     {
-        Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) );
-        Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
+        Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p), 0 );
+        Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p), 1 );
         char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
         char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
         Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, OffSet );
         Vec_PtrFreeFree( vNamesCi );
         Vec_PtrFreeFree( vNamesCo );
     }
+    else
+        Gia_ManPrintDsd( pManDsd, 0, Vec_PtrSize(vFuncs), 0 );
+
     Dsd_ManagerStop( pManDsd );
     Gia_ManCollapseDeref( dd, vFuncs );
     Extra_StopManager( dd );
 }
 
+Vec_Ptr_t * Gia_ManRecurDsdCof( DdManager * dd, Vec_Ptr_t * vFuncs, int iVar )
+{
+    Vec_Ptr_t * vNew = Vec_PtrAlloc( 2 * Vec_PtrSize(vFuncs) ); DdNode * bFunc; int i;
+    Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i ) {
+        DdNode * bCof0 = Cudd_Cofactor( dd, bFunc, Cudd_Not(Cudd_bddIthVar(dd, iVar)) ); Cudd_Ref( bCof0 );
+        DdNode * bCof1 = Cudd_Cofactor( dd, bFunc, Cudd_bddIthVar(dd, iVar) );           Cudd_Ref( bCof1 );
+        Vec_PtrPush( vNew, bCof0 );
+        Vec_PtrPush( vNew, bCof1 );        
+    }
+    return vNew;
+}
+void Gia_ManRecurDsd( Gia_Man_t * p, int fVerbose )
+{
+    DdManager * dd;
+    Dsd_Manager_t * pManDsd;
+    Vec_Ptr_t * vFuncs, * vAux;
+    dd = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+    vFuncs = Gia_ManCollapse( p, dd, 10000, 0 );
+    Cudd_AutodynDisable( dd );
+    if ( vFuncs == NULL ) 
+    {
+        Extra_StopManager( dd );
+        return;
+    }
+    pManDsd = Dsd_ManagerStart( dd, Gia_ManCiNum(p), 0 );
+    if ( pManDsd == NULL )
+    {
+        Gia_ManCollapseDeref( dd, vFuncs );
+        Cudd_Quit( dd );
+        return;
+    }
+    Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
+
+    printf( "Function:\n" );
+    Gia_ManPrintDsd( pManDsd, 0, Vec_PtrSize(vFuncs), 0 );
+
+    for ( int i = 0; i < 5 && Dsd_TreeNonDsdMax(pManDsd, -1) > 0; i++ ) 
+    {
+        int v, iBestV = -1, DsdMin = ABC_INFINITY, SuppMin = ABC_INFINITY;
+        for ( v = 0; v < Gia_ManCiNum(p); v++ ) 
+        {
+            Vec_Ptr_t * vTemp = Gia_ManRecurDsdCof( dd, vFuncs, v );
+            Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vTemp), Vec_PtrSize(vTemp) );
+            int DsdCur  = Dsd_TreeNonDsdMax( pManDsd, -1 );
+            int SuppCur = Dsd_TreeSuppSize( pManDsd, -1 );
+            if ( DsdMin > DsdCur || (DsdMin == DsdCur && SuppMin > SuppCur) )
+                DsdMin = DsdCur, SuppMin = SuppCur, iBestV = v;
+            Gia_ManCollapseDeref( dd, vTemp );
+        }
+        assert( iBestV >= 0 );
+        vFuncs = Gia_ManRecurDsdCof( dd, vAux = vFuncs, iBestV );
+        Gia_ManCollapseDeref( dd, vAux );        
+        printf( "Cofactoring variable %c:\n", (int)(iBestV >= 26 ? 'A' - 26 : 'a') + iBestV );
+        Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
+        Gia_ManPrintDsd( pManDsd, -1, Vec_PtrSize(vFuncs), (i+1)*2 );
+    }
+
+    Dsd_ManagerStop( pManDsd );
+    Gia_ManCollapseDeref( dd, vFuncs );
+    Extra_StopManager( dd );    
+}
+
 #else
 
 Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
@@ -452,6 +518,10 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
 {
 }
 
+void Gia_ManRecurDsd( Gia_Man_t * p, int fVerbose )
+{
+}
+
 #endif
 
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaCut.c

@@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 
 #define GIA_MAX_CUTSIZE    8
-#define GIA_MAX_CUTNUM     65
+#define GIA_MAX_CUTNUM     257
 #define GIA_MAX_TT_WORDS   ((GIA_MAX_CUTSIZE > 6) ? 1 << (GIA_MAX_CUTSIZE-6) : 1)
 
 #define GIA_CUT_NO_LEAF   0xF
@@ -45,6 +45,7 @@ struct Gia_Cut_t_
     unsigned        nTreeLeaves  : 28;         // tree leaves
     unsigned        nLeaves      :  4;         // leaf count
     int             pLeaves[GIA_MAX_CUTSIZE];  // leaves
+    float           CostF;
 };
 
 typedef struct Gia_Sto_t_ Gia_Sto_t; 
@@ -281,7 +282,7 @@ static inline int Gia_CutSetLastCutIsContained( Gia_Cut_t ** pCuts, int nCuts )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Gia_CutCompare( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 )
+static inline int Gia_CutCompare2( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 )
 {
     if ( pCut0->nTreeLeaves < pCut1->nTreeLeaves )  return -1;
     if ( pCut0->nTreeLeaves > pCut1->nTreeLeaves )  return  1;
@@ -289,6 +290,14 @@ static inline int Gia_CutCompare( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 )
     if ( pCut0->nLeaves     > pCut1->nLeaves )      return  1;
     return 0;
 }
+static inline int Gia_CutCompare( Gia_Cut_t * pCut0, Gia_Cut_t * pCut1 )
+{
+    if ( pCut0->CostF       > pCut1->CostF )         return -1;
+    if ( pCut0->CostF       < pCut1->CostF )         return  1;
+    if ( pCut0->nLeaves     < pCut1->nLeaves )      return -1;
+    if ( pCut0->nLeaves     > pCut1->nLeaves )      return  1;
+    return 0;
+}
 static inline int Gia_CutSetLastCutContains( Gia_Cut_t ** pCuts, int nCuts )
 {
     int i, k, fChanges = 0;
@@ -432,6 +441,13 @@ static inline int Gia_CutTreeLeaves( Gia_Sto_t * p, Gia_Cut_t * pCut )
         Cost += Vec_IntEntry( p->vRefs, pCut->pLeaves[i] ) == 1;
     return Cost;
 }
+static inline float Gia_CutGetCost( Gia_Sto_t * p, Gia_Cut_t * pCut )
+{
+    int i, Cost = 0;
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        Cost += Vec_IntEntry( p->vRefs, pCut->pLeaves[i] );
+    return (float)Cost / Abc_MaxInt(1, pCut->nLeaves);
+}
 static inline int Gia_StoPrepareSet( Gia_Sto_t * p, int iObj, int Index )
 {
     Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
@@ -445,6 +461,7 @@ static inline int Gia_StoPrepareSet( Gia_Sto_t * p, int iObj, int Index )
         pCutTemp->iFunc = pCut[pCut[0]+1];
         pCutTemp->Sign = Gia_CutGetSign( pCutTemp );
         pCutTemp->nTreeLeaves = Gia_CutTreeLeaves( p, pCutTemp );
+        pCutTemp->CostF = Gia_CutGetCost( p, pCutTemp );
     }
     return pList[0];
 }
@@ -512,6 +529,7 @@ void Gia_StoMergeCuts( Gia_Sto_t * p, int iObj )
         if ( p->fCutMin && Gia_CutComputeTruth(p, pCut0, pCut1, fComp0, fComp1, pCutsR[nCutsR], fIsXor) )
             pCutsR[nCutsR]->Sign = Gia_CutGetSign(pCutsR[nCutsR]);
         pCutsR[nCutsR]->nTreeLeaves = Gia_CutTreeLeaves( p, pCutsR[nCutsR] );
+        pCutsR[nCutsR]->CostF = Gia_CutGetCost( p, pCutsR[nCutsR] );        
         nCutsR = Gia_CutSetAddCut( pCutsR, nCutsR, nCutNum );
     }
     p->CutCount[3] += nCutsR;
@@ -1048,8 +1066,9 @@ Gia_Sto_t * Gia_ManMatchCutsInt( Gia_Man_t * pGia, int nCutSize0, int nCutNum0,
 void Gia_ManMatchCuts( Vec_Mem_t * vTtMem, Gia_Man_t * pGia, int nCutSize, int nCutNum, int fVerbose )
 {
     Gia_Sto_t * p = Gia_ManMatchCutsInt( pGia, nCutSize, nCutNum, fVerbose );
-    Vec_Int_t * vLevel; int i, k, * pCut;
+    Vec_Int_t * vLevel; int i, j, k, * pCut;
     Vec_Int_t * vNodes = Vec_IntAlloc( 100 );
+    Vec_Wec_t * vCuts = Vec_WecAlloc( 100 );
     abctime clkStart  = Abc_Clock();
     assert( Abc_Truth6WordNum(nCutSize) == Vec_MemEntrySize(vTtMem) );
     Vec_WecForEachLevel( p->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) )
@@ -1061,11 +1080,19 @@ void Gia_ManMatchCuts( Vec_Mem_t * vTtMem, Gia_Man_t * pGia, int nCutSize, int n
             if ( *pSpot == -1 )
                 continue;
             Vec_IntPush( vNodes, i );
+            vLevel = Vec_WecPushLevel( vCuts );
+            Vec_IntPush( vLevel, i );
+            for ( j = 1; j <= pCut[0]; j++ )
+                Vec_IntPush( vLevel, pCut[j] );
             break;
         }
     }
     printf( "Nodes with matching cuts: " );
     Vec_IntPrint( vNodes );
+    if ( Vec_WecSize(vCuts) > 32 )
+        Vec_WecShrink(vCuts, 32);
+    Vec_WecPrint( vCuts, 0 );
+    Vec_WecFree( vCuts );
     Vec_IntFree( vNodes );
     Gia_StoFree( p );
     if ( fVerbose )
@@ -1107,6 +1134,251 @@ Vec_Ptr_t * Gia_ManMatchCutsArray( Vec_Ptr_t * vTtMems, Gia_Man_t * pGia, int nC
     }
     return vRes;  
 }
+Vec_Ptr_t * Gia_ManMatchCutsMany( Vec_Mem_t * vTtMem, Vec_Int_t * vMap, int nFuncs, Gia_Man_t * pGia, int nCutSize, int nCutNum, int fVerbose )
+{
+    Gia_Sto_t * p = Gia_ManMatchCutsInt( pGia, nCutSize, nCutNum, fVerbose );
+    Vec_Int_t * vLevel; int i, j, k, * pCut;
+    abctime clkStart  = Abc_Clock();
+    assert( Abc_Truth6WordNum(nCutSize) == Vec_MemEntrySize(vTtMem) );
+    Vec_Ptr_t * vRes = Vec_PtrAlloc( nFuncs );
+    for ( i = 0; i < nFuncs; i++ )
+        Vec_PtrPush( vRes, Vec_WecAlloc(10) );
+    Vec_WecForEachLevel( p->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) )
+    {
+        Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) if ( pCut[0] > 1 )
+        {
+            word * pTruth = Vec_MemReadEntry( p->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]) );
+            assert( (pTruth[0] & 1) == 0 );
+            int * pSpot = Vec_MemHashLookup( vTtMem, pTruth );
+            if ( *pSpot == -1 )
+                continue;
+            int iFunc = vMap ? Vec_IntEntry( vMap, *pSpot ) : 0;
+            assert( iFunc < nFuncs );
+            Vec_Wec_t * vCuts = (Vec_Wec_t *)Vec_PtrEntry( vRes, iFunc );
+            vLevel = Vec_WecPushLevel( vCuts );
+            Vec_IntPush( vLevel, i );
+            for ( j = 1; j <= pCut[0]; j++ )
+                Vec_IntPush( vLevel, pCut[j] );
+            break;
+        }
+    }
+    Gia_StoFree( p );
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Cut matching time", Abc_Clock() - clkStart );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Function enumeration.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wrd_t * Gia_ManCollectCutFuncs( Gia_Man_t * p, int nCutSize, int nCutNum, int fVerbose )
+{
+    Gia_Sto_t * pSto = Gia_ManMatchCutsInt( p, nCutSize, nCutNum, 0 );
+    Vec_Wrd_t * vFuncs = Vec_WrdAlloc( 1000 ); Vec_Int_t * vLevel; int i, k, * pCut; 
+    Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) )
+        Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) if ( pCut[0] == nCutSize ) {
+            word * pTruth = Vec_MemReadEntry( pSto->vTtMem, Abc_Lit2Var(pCut[pCut[0]+1]) );
+            Vec_WrdPush( vFuncs, pTruth[0] );
+        }
+    Gia_StoFree( pSto );
+    if ( fVerbose )
+        printf( "Collected %d cut functions using the AIG with %d nodes.\n", Vec_WrdSize(vFuncs), Gia_ManAndNum(p) );
+    return vFuncs;
+}
+Vec_Int_t * Gia_ManCountNpnClasses( Vec_Mem_t * vTtMem, Vec_Int_t * vMap, int nClasses, Vec_Wrd_t * vOrig )
+{
+    assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vMap) );
+    Vec_Int_t * vClassCounts = Vec_IntStart( nClasses ); int i; word Func;
+    Vec_WrdForEachEntry( vOrig, Func, i ) {
+        int * pSpot = Vec_MemHashLookup( vTtMem, &Func );
+        if ( *pSpot == -1 )
+            continue;
+        int iClass = Vec_IntEntry( vMap, *pSpot );
+        if ( iClass == -1 )
+            continue;
+        assert( iClass < Vec_IntSize(vClassCounts) );
+        Vec_IntAddToEntry( vClassCounts, iClass, 1 );
+    }
+    return vClassCounts;
+}
+Vec_Wrd_t * Gia_ManMatchFilterClasses( Vec_Mem_t * vTtMem, Vec_Int_t * vMap, Vec_Int_t * vClassCounts, int nNumFuncs, int fVerbose )
+{
+    int * pPerm = Abc_MergeSortCost( Vec_IntArray(vClassCounts), Vec_IntSize(vClassCounts) );
+    Vec_Wrd_t * vBest = Vec_WrdAlloc( nNumFuncs );  int i, k, Entry;
+    Vec_Int_t * vMapNew = Vec_IntStartFull( Vec_IntSize(vMap) );  
+    for ( i = Vec_IntSize(vClassCounts)-1; i >= 0; i-- ) {
+        word Best = ~(word)0;
+        Vec_IntForEachEntry( vMap, Entry, k ) {
+            if ( Entry != pPerm[i] )
+                continue;
+            if ( Best > Vec_MemReadEntry(vTtMem, k)[0] )
+                 Best = Vec_MemReadEntry(vTtMem, k)[0];            
+            Vec_IntWriteEntry( vMapNew, k, Vec_WrdSize(vBest) );
+        }
+        Vec_WrdPush( vBest, Best );
+        assert( ~Best );
+        if ( Vec_WrdSize(vBest) == nNumFuncs )
+            break;
+    }
+    ABC_SWAP( Vec_Int_t, *vMap, *vMapNew );
+    Vec_IntFree( vMapNew );
+    ABC_FREE( pPerm );
+    if ( fVerbose )
+        printf( "Isolated %d (out of %d) most frequently occuring classes.\n", Vec_WrdSize(vBest), Vec_IntSize(vClassCounts) );
+    return vBest;
+}
+void Gia_ManMatchProfileFunctions( Vec_Wrd_t * vBestReprs, Vec_Mem_t * vTtMem, Vec_Int_t * vMap, Vec_Wrd_t * vFuncs, int nCutSize )
+{
+    int BarSize = 60;
+    extern void Dau_DsdPrintFromTruth( word * pTruth, int nVarsInit );
+    Vec_Int_t * vCounts = Gia_ManCountNpnClasses( vTtMem, vMap, Vec_WrdSize(vBestReprs), vFuncs ); 
+    word Repr; int c, i, MaxCount = Vec_IntFindMax( vCounts );
+    Vec_WrdForEachEntry( vBestReprs, Repr, c )
+    {
+        int nSymb = BarSize*Vec_IntEntry(vCounts, c)/Abc_MaxInt(MaxCount, 1);
+        printf( "Class%4d : ", c );
+        printf( "Count =%6d   ", Vec_IntEntry(vCounts, c) );
+        for ( i = 0; i < nSymb; i++ )
+            printf( "*" );
+        for ( i = nSymb; i < BarSize+3; i++ )
+            printf( " " );        
+        Dau_DsdPrintFromTruth( &Repr, nCutSize );
+    }
+    Vec_IntFree( vCounts );
+}
+void Gia_ManMatchCones( Gia_Man_t * pBig, Gia_Man_t * pSmall, int nCutSize, int nCutNum, int nNumFuncs, int nNumCones, int fVerbose )
+{
+    abctime clkStart  = Abc_Clock();
+    extern void Dau_CanonicizeArray( Vec_Wrd_t * vFuncs, int nVars, int fVerbose );
+    extern Vec_Mem_t * Dau_CollectNpnFunctionsArray( Vec_Wrd_t * vFuncs, int nVars, Vec_Int_t ** pvMap, int fVerbose );
+    Vec_Wrd_t * vFuncs = Gia_ManCollectCutFuncs( pSmall, nCutSize, nCutNum, fVerbose );
+    Vec_Wrd_t * vOrig = Vec_WrdDup( vFuncs );
+    Dau_CanonicizeArray( vFuncs, nCutSize, fVerbose );  
+    Vec_Int_t * vMap = NULL; int n;
+    Vec_Mem_t * vTtMem = Dau_CollectNpnFunctionsArray( vFuncs, nCutSize, &vMap, fVerbose );
+    Vec_WrdFree( vFuncs );
+    Vec_Int_t * vClassCounts = Gia_ManCountNpnClasses( vTtMem, vMap, Vec_IntEntryLast(vMap)+1, vOrig );
+    Vec_Wrd_t * vBestReprs = Gia_ManMatchFilterClasses( vTtMem, vMap, vClassCounts, nNumFuncs, fVerbose );
+    assert( Vec_WrdSize(vBestReprs) == nNumFuncs );
+    Vec_IntFree( vClassCounts );
+    printf( "Frequency profile for %d most popular classes in the small AIG:\n", nNumFuncs );
+    Gia_ManMatchProfileFunctions( vBestReprs, vTtMem, vMap, vOrig, nCutSize );
+    Vec_WrdFree( vOrig );
+    Abc_Random( 1 );
+    for ( n = 0; n < nNumCones; n++ ) {
+        int nRand = Abc_Random( 0 ) % Gia_ManCoNum(pBig);
+        Gia_Man_t * pCone = Gia_ManDupCones( pBig, &nRand, 1, 1 );
+        Vec_Wrd_t * vCutFuncs = Gia_ManCollectCutFuncs( pCone, nCutSize, nCutNum, 0 );
+        printf( "ITER %d: Considering output cone %d with %d and-nodes. ", n+1, nRand, Gia_ManAndNum(pCone) );
+        printf( "Profiling %d functions of %d-cuts:\n", Vec_WrdSize(vCutFuncs), nCutSize );
+        Gia_ManMatchProfileFunctions( vBestReprs, vTtMem, vMap, vCutFuncs, nCutSize );
+        Vec_WrdFree( vCutFuncs );
+        Gia_ManStop( pCone );
+    }
+    Vec_WrdFree( vBestReprs );
+    Vec_IntFree( vMap );
+    Vec_MemHashFree( vTtMem );
+    Vec_MemFree( vTtMem );
+    Abc_PrintTime( 1, "Total computation time", Abc_Clock() - clkStart );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Function enumeration.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManMatchConesMinimizeTts( Vec_Wrd_t * vSims, int nVarsMax )
+{
+    int nVars = 0;
+    int nWordsMax = Abc_Truth6WordNum( nVarsMax ), nWords;
+    int i, k = 0, nTruths = Vec_WrdSize(vSims) / nWordsMax;
+    assert( nTruths * nWordsMax == Vec_WrdSize(vSims) );
+    // support-minimize and find the largest supp size
+    for ( i = 0; i < nTruths; i++ ) {
+        word * pTruth = Vec_WrdEntryP( vSims, i * nWordsMax );
+        int nVarsCur = Abc_TtMinBase( pTruth, NULL, nVarsMax, nVarsMax );
+        nVars = Abc_MaxInt( nVars, nVarsCur );
+    }
+    // remap truth tables
+    nWords = Abc_Truth6WordNum( nVars );
+    for ( i = 0; i < nTruths; i++ ) {
+        word * pTruth = Vec_WrdEntryP( vSims, i * nWordsMax );
+        word * pTruth2 = Vec_WrdEntryP( vSims, k * nWords );
+        if ( Abc_TtSupportSize(pTruth, nVars) < 3 )
+            continue;
+        memmove( pTruth2, pTruth, nWords * sizeof(word) );
+        k++;
+        if ( 0 ) {
+            extern void Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars );
+            printf( "Type%d : ", i );
+            Extra_PrintHexadecimal( stdout, (unsigned *)pTruth2, nVars );
+            printf( "\n" );
+        }
+    }
+    Vec_WrdShrink ( vSims, k * nWords );
+    return nVars;
+}
+void Gia_ManMatchConesOutputPrint( Vec_Ptr_t * p, int fVerbose )
+{
+    Vec_Wec_t * vCuts; int i;
+    printf( "Nodes with matching cuts:\n" );
+    Vec_PtrForEachEntry( Vec_Wec_t *, p, vCuts, i ) {
+        if ( fVerbose ) {
+            printf( "Type %d:\n", i );
+            Vec_WecPrint( vCuts, 0 );
+        }
+        else 
+            printf( "Type %d present in %d cuts\n", i, Vec_WecSize(vCuts) );
+    }
+}
+void Gia_ManMatchConesOutputFree( Vec_Ptr_t * p )
+{
+    Vec_Wec_t * vCuts; int i;
+    Vec_PtrForEachEntry( Vec_Wec_t *, p, vCuts, i )
+        Vec_WecFree( vCuts );
+    Vec_PtrFree( p );
+}
+void Gia_ManMatchConesOutput( Gia_Man_t * pBig, Gia_Man_t * pSmall, int nCutNum, int fVerbose )
+{
+    abctime clkStart  = Abc_Clock();
+    extern Vec_Mem_t * Dau_CollectNpnFunctionsArray( Vec_Wrd_t * vFuncs, int nVars, Vec_Int_t ** pvMap, int fVerbose );
+    Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(pSmall) );
+    Vec_Wrd_t * vSims   = Gia_ManSimPatSimOut( pSmall, vSimsPi, 1 );
+    int nVars = Gia_ManMatchConesMinimizeTts( vSims, Gia_ManCiNum(pSmall) );
+    Vec_WrdFree( vSimsPi );
+    if ( nVars > 10 ) {
+        printf( "Some output functions have support size more than 10.\n" );
+        Vec_WrdFree( vSims );
+        return;
+    }
+    Vec_Int_t * vMap = NULL;
+    Vec_Mem_t * vTtMem = Dau_CollectNpnFunctionsArray( vSims, nVars, &vMap, fVerbose );
+    int nFuncs = Vec_WrdSize(vSims) / Abc_Truth6WordNum(nVars);
+    assert( Vec_WrdSize(vSims) == nFuncs * Abc_Truth6WordNum(nVars) );
+    Vec_WrdFree( vSims );
+    printf( "Using %d output functions with the support size between 3 and %d.\n", nFuncs, nVars );
+    Vec_Ptr_t * vRes = Gia_ManMatchCutsMany( vTtMem, vMap, nFuncs, pBig, nVars, nCutNum, fVerbose );
+    Vec_MemHashFree( vTtMem );
+    Vec_MemFree( vTtMem );
+    Vec_IntFree( vMap );
+    Gia_ManMatchConesOutputPrint( vRes, fVerbose );
+    Gia_ManMatchConesOutputFree( vRes );
+    Abc_PrintTime( 1, "Total computation time", Abc_Clock() - clkStart );    
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/aig/gia/giaEquiv.c

@@ -2732,6 +2732,54 @@ void Gia_ManTransferTest( Gia_Man_t * p )
     Gia_ManStop( pNew );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Transfer from new to old.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManTransferEquivs2( Gia_Man_t * p, Gia_Man_t * pOld )
+{
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vClass;
+    int i, k, iNode, iRepr;
+    assert( p->pReprs != NULL );
+    assert( p->pNexts != NULL );
+    assert( pOld->pReprs == NULL );
+    assert( pOld->pNexts == NULL );
+    // create map
+    Gia_ManFillValue( p );
+    Gia_ManForEachObj( pOld, pObj, i )
+        if ( ~pObj->Value )
+            Gia_ManObj(p, Abc_Lit2Var(pObj->Value))->Value = Abc_Var2Lit(i, 0);
+    // start representatives
+    pOld->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pOld) );
+    for ( i = 0; i < Gia_ManObjNum(pOld); i++ )
+        Gia_ObjSetRepr( pOld, i, GIA_VOID );
+    // iterate over constant candidates
+    Gia_ManForEachConst( p, i )
+        Gia_ObjSetRepr( pOld, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
+    // iterate over class candidates
+    vClass = Vec_IntAlloc( 100 );
+    Gia_ManForEachClass( p, i )
+    {
+        Vec_IntClear( vClass );
+        Gia_ClassForEachObj( p, i, k )
+            Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
+        assert( Vec_IntSize( vClass ) > 1 );
+        Vec_IntSort( vClass, 0 );
+        iRepr = Vec_IntEntry( vClass, 0 );
+        Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
+            Gia_ObjSetRepr( pOld, iNode, iRepr );
+    }
+    Vec_IntFree( vClass );
+    pOld->pNexts = Gia_ManDeriveNexts( pOld );
+}
 
 /**Function*************************************************************
 

src/aig/gia/giaGen.c

@@ -924,6 +924,384 @@ void Gia_ManTestWordFile( Gia_Man_t * p, char * pFileName, char * pDumpFile, int
     Abc_PrintTime( 1, "Total checking time", Abc_Clock() - clk );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManSumCount( char * p, Vec_Int_t * vDec, int b )
+{
+    int i, Ent, Count = 0, Sum = 0;
+    for ( i = 0; p[i]; i++ ) {
+        Ent = (p[i] >= '0' && p[i] <= '9') ? p[i]-'0' : p[i]-'A'+10;
+        Count += Vec_IntEntry(vDec, Ent) + b * (1 << (Sum += Ent));
+    }
+    return Count + b * ((1 << Sum) - 1);
+}
+Vec_Str_t * Gia_ManSumEnum_rec( int Num )
+{
+    if ( Num == 1 ) {
+        Vec_Str_t * vRes = Vec_StrAlloc(2);
+        Vec_StrPush( vRes, '1' );
+        Vec_StrPush( vRes, '\0' );        
+        return vRes;
+    }
+    Vec_Str_t * vRes = Vec_StrAlloc( 16 );
+    for ( int i = 1; i < Num; i++ ) {
+        Vec_Str_t * vRes0 = Gia_ManSumEnum_rec(i);
+        Vec_Str_t * vRes1 = Gia_ManSumEnum_rec(Num-i);
+        for ( int c0 = 0; c0 < Vec_StrSize(vRes0); c0 += strlen(Vec_StrEntryP(vRes0,c0))+1 )
+        for ( int c1 = 0; c1 < Vec_StrSize(vRes1); c1 += strlen(Vec_StrEntryP(vRes1,c1))+1 )
+            Vec_StrPrintF( vRes, "%s%s%c", Vec_StrEntryP(vRes0,c0), Vec_StrEntryP(vRes1,c1), '\0' );
+        Vec_StrPrintF( vRes, "%c%c", Num < 10 ? '0'+Num : 'A'+Num-10, '\0' );
+        Vec_StrFree( vRes0 );
+        Vec_StrFree( vRes1 );       
+    }
+    return vRes;
+}
+void Gia_ManSumEnum( int n, Vec_Int_t * vDec )
+{
+    Vec_Str_t * vRes = Gia_ManSumEnum_rec( n );
+    for ( int b = 1; b <= 256; b <<= 1 ) {
+        int iBest = -1, CountCur, CountBest = ABC_INFINITY;
+        for ( int c0 = 0; c0 < Vec_StrSize(vRes); c0 += strlen(Vec_StrEntryP(vRes,c0))+1 ) {
+            CountCur = Gia_ManSumCount( Vec_StrEntryP(vRes,c0), vDec, b );
+            if ( CountBest > CountCur )
+                CountBest = CountCur, iBest = c0;
+        }
+        printf( " %8d", CountBest );
+        //printf( " %8s", Vec_StrEntryP(vRes,iBest) );
+        //printf( " %.3f", (float)CountBest/(3*b*((1<<n)-1)) );
+    }
+//    Vec_StrPrint( vRes, 0 );
+    Vec_StrFree( vRes );
+}
+Vec_Int_t * Gia_ManSumGenDec( int n )
+{
+    Vec_Int_t * vDec = Vec_IntAlloc( n + 1 );
+    Vec_IntPush( vDec, 0 );
+    Vec_IntPush( vDec, 0 );
+    Vec_IntPush( vDec, 4 );
+    Vec_IntPush( vDec, 12 );    
+    for ( int i = 4; i <= n; i++ ) {
+        int Ent0 = Vec_IntEntry( vDec, i / 2 );
+        int Ent1 = Vec_IntEntry( vDec, i - i / 2 );        
+        assert( Vec_IntSize(vDec) == i );
+        Vec_IntPush( vDec, Ent0 + Ent1 + (1 << i / 2) * (1 << (i - i / 2)) );
+    }
+    return vDec;
+}
+void Gia_ManSumEnumTest()
+{
+    Vec_Int_t * vDec = Gia_ManSumGenDec( 16 );
+    printf( "    " );
+    for ( int b = 1; b <= 256; b <<= 1 )
+        printf( " %8d", b );
+    printf( "\n" );
+    for ( int i = 1; i <= 15; i++ ) {
+        printf( "%2d :", i );
+        Gia_ManSumEnum( i, vDec );        
+        printf( "\n" );
+    }
+    Vec_IntFree( vDec );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManGenNeuronDumpVerilog( Vec_Wrd_t * vData, int nIBits, int nOBits )
+{
+    FILE * pFile = fopen( "temp.v", "wb" );
+    if ( pFile == NULL ) {
+        printf( "Cannot open output file.\n" );
+        return;
+    }
+    fprintf( pFile, "module neuron_%d_%d_%d ( input [%d:0] i, output [%d:0] o );\n", 
+        Vec_WrdSize(vData)-1, nIBits, nOBits, (Vec_WrdSize(vData)-1)*nIBits-1, nOBits-1 );
+    fprintf( pFile, "assign o = %d'h%lX", nOBits, Vec_WrdEntryLast(vData) );
+    word Data; int i;
+    Vec_WrdForEachEntryStop( vData, Data, i, Vec_WrdSize(vData)-1 )
+        fprintf( pFile, "\n         + %d'h%lX * i[%d:%d]", nOBits, Data, nIBits*(i+1)-1, nIBits*i );
+    fprintf( pFile, ";\nendmodule\n\n" );
+    fclose( pFile );
+    printf( "Dumped the neuron specification into file \"temp.v\".\n" );
+}
+void Gia_ManGenNeuronAdder( Gia_Man_t * p, int nLits, int * pLitsA, int * pLitsB, int Carry, Vec_Int_t * vRes )
+{
+    extern void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps );
+    int i, Res = -1;
+    Vec_IntClear( vRes );
+    for ( i = 0; i < nLits; i++ ) {
+        Wlc_BlastFullAdder( p, pLitsA[i], pLitsB[i], Carry, &Carry, &Res );
+        Vec_IntPush( vRes, Res );
+    }
+}
+void Gia_ManGenCompact( Gia_Man_t * p, Vec_Int_t * vIn0, Vec_Int_t * vIn1, Vec_Int_t * vIn2, Vec_Int_t * vOut0, Vec_Int_t * vOut1 )
+{
+    extern void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps );
+    assert( Vec_IntSize(vIn0) == Vec_IntSize(vIn1) );
+    assert( Vec_IntSize(vIn0) == Vec_IntSize(vIn2) ); 
+    Vec_IntPush( vOut1, 0 );
+    int i, Lit0, Lit1, Lit2, Out0, Out1;
+    Vec_IntForEachEntryThree( vIn0, vIn1, vIn2, Lit0, Lit1, Lit2, i ) {
+        Wlc_BlastFullAdder( p, Lit0, Lit1, Lit2, &Out1, &Out0 );
+        Vec_IntPush( vOut0, Out0 );
+        Vec_IntPush( vOut1, Out1 );        
+    }
+    Vec_IntPop( vOut1 );
+    assert( Vec_IntSize(vIn0) == Vec_IntSize(vOut0) );
+    assert( Vec_IntSize(vIn0) == Vec_IntSize(vOut1) ); 
+}
+Vec_Wec_t * Gia_ManGenNeuronCreateArgs( Vec_Wrd_t * vData, int nIBits, int nOBits )
+{
+    word Data = Vec_WrdEntryLast(vData); int i, b, n, nLits = 2;
+    Vec_Wec_t * vArgs = Vec_WecAlloc( Vec_WrdSize(vData) * nIBits ); 
+    Vec_Int_t * vLev  = Vec_WecPushLevel( vArgs );
+    Vec_IntFill( vLev, nOBits, 0 );
+    for ( b = 0; b < nOBits; b++ )
+        if ( (Data >> b) & 1 )
+            Vec_IntWriteEntry( vLev, b, 1 );
+    Vec_WrdForEachEntryStop( vData, Data, i, Vec_WrdSize(vData)-1 ) {
+        for ( n = 0; n < nIBits; n++, nLits += 2 ) {
+            Vec_Int_t * vLev = Vec_WecPushLevel( vArgs );
+            Vec_IntFill( vLev, nOBits, 0 );
+            for ( b = 0; b < nOBits; b++ )
+                if ( ((Data >> b) & 1) && b+n < nOBits )
+                    Vec_IntWriteEntry( vLev, b+n, nLits );
+        }
+    }
+    return vArgs;
+}
+Vec_Wec_t * Gia_ManGenNeuronTransformArgs( Gia_Man_t * pNew, Vec_Wec_t * vArgs, int nLutSize, int nOBits )
+{
+    int i, nParts = (Vec_WecSize(vArgs) + nLutSize - 2) / nLutSize;
+    while ( Vec_WecSize(vArgs) < nLutSize*nParts+1 )
+        Vec_IntFill( Vec_WecPushLevel(vArgs), nOBits, 0 );
+    assert( Vec_WecSize(vArgs) == nLutSize*nParts+1 );
+    Vec_Wec_t * vNew = Vec_WecAlloc( nParts );
+    Vec_Int_t * vRes = Vec_WecPushLevel( vNew ), * vArg;
+    Vec_IntAppend( vRes, Vec_WecEntry(vArgs, 0) );
+    Vec_WecForEachLevelStart( vArgs, vArg, i, 1 ) {
+        Gia_ManGenNeuronAdder( pNew, nOBits, Vec_IntArray(vArg), Vec_IntArray(vRes), 0, vRes );
+        if ( (i-1) % nLutSize == nLutSize-1 && i < Vec_WecSize(vArgs)-1 ) {
+            vRes = Vec_WecPushLevel( vNew );
+            Vec_IntFill( vRes, nOBits, 0 );
+        }            
+    }
+    assert( Vec_WecSize(vNew) == nParts );
+    return vNew;
+}
+Vec_Wec_t * Gia_ManGenNeuronCompactArgs( Gia_Man_t * pNew, Vec_Wec_t * vArgs, int nLutSize, int nOBits )
+{
+    int i, nParts = Vec_WecSize(vArgs) / 3;
+    Vec_Wec_t * vNew = Vec_WecAlloc( 2 * nParts + Vec_WecSize(vArgs) % 3 );
+    for ( i = 0; i < nParts; i++ ) {
+        Vec_Int_t * vIn0 = Vec_WecEntry(vArgs, 3*i+0);
+        Vec_Int_t * vIn1 = Vec_WecEntry(vArgs, 3*i+1);
+        Vec_Int_t * vIn2 = Vec_WecEntry(vArgs, 3*i+2);
+        Vec_Int_t * vOut0 = Vec_WecPushLevel(vNew);
+        Vec_Int_t * vOut1 = Vec_WecPushLevel(vNew);
+        Gia_ManGenCompact( pNew, vIn0, vIn1, vIn2, vOut0, vOut1 );
+    }
+    for ( i = 3*nParts; i < Vec_WecSize(vArgs); i++ )
+        Vec_IntAppend( Vec_WecPushLevel(vNew), Vec_WecEntry(vArgs, i) );
+    assert( Vec_WecSize(vNew) == 2 * nParts + Vec_WecSize(vArgs) % 3 );
+    return vNew;
+}
+Vec_Int_t * Gia_ManGenNeuronFinal( Gia_Man_t * pNew, Vec_Wec_t * vArgs, int nOBits )
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( nOBits ), * vArg; int i;
+    Vec_IntAppend( vRes, Vec_WecEntry(vArgs, 0) );
+    Vec_WecForEachLevelStart( vArgs, vArg, i, 1 )
+        Gia_ManGenNeuronAdder( pNew, nOBits, Vec_IntArray(vArg), Vec_IntArray(vRes), 0, vRes );
+    return vRes;
+}
+int Gia_ManGenNeuronBitWidth( Vec_Wrd_t * vData, int nIBits )
+{   
+    int i, InMask = (1<<nIBits)-1; 
+    word Data, DataMax = Vec_WrdEntryLast(vData);
+    Vec_WrdForEachEntryStop( vData, Data, i, Vec_WrdSize(vData)-1 )
+        DataMax += InMask * Data;
+    return Abc_Base2LogW(DataMax);
+}
+Gia_Man_t * Gia_ManGenNeuron( char * pFileName, int nIBits, int nLutSize, int fDump, int fVerbose )
+{
+    int nWords = -1;
+    Vec_Wrd_t * vData = Vec_WrdReadHex( pFileName, &nWords, 0 );
+    if ( vData == NULL ) 
+        return NULL;
+
+    assert( nWords == 1 );
+    assert( 0 < nIBits && nIBits < 32 );
+    int i, Lit, nOBits = Gia_ManGenNeuronBitWidth( vData, nIBits );
+    if ( fDump ) Gia_ManGenNeuronDumpVerilog( vData, nIBits, nOBits );
+
+    Gia_Man_t * pTemp, * pNew = Gia_ManStart( 10000 );
+    pNew->pName = Abc_UtilStrsav( "neuron" );
+    for ( i = 0; i < nIBits * (Vec_WrdSize(vData)-1); i++ )
+        Gia_ManAppendCi( pNew );
+    Gia_ManHashAlloc( pNew );
+
+    Vec_Wec_t * vTemp, * vArgs = Gia_ManGenNeuronCreateArgs( vData, nIBits, nOBits );
+    Vec_WrdFree( vData );
+
+    if ( nLutSize ) {
+        vArgs = Gia_ManGenNeuronTransformArgs( pNew, vTemp = vArgs, nLutSize, nOBits );
+        Vec_WecFree( vTemp );
+        while ( Vec_WecSize(vArgs) > 2 ) {
+            vArgs = Gia_ManGenNeuronCompactArgs( pNew, vTemp = vArgs, nLutSize, nOBits );
+            Vec_WecFree( vTemp );
+        }
+    }
+
+    Vec_Int_t * vRes = Gia_ManGenNeuronFinal( pNew, vArgs, nOBits );    
+    Vec_IntForEachEntry( vRes, Lit, i )
+        Gia_ManAppendCo( pNew, Lit );
+    Vec_IntFree( vRes );
+    Vec_WecFree( vArgs );
+
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates minimum-node AIG for n-bit comparator (a > b).]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupGenComp( int nBits, int fInterleave )
+{
+    Gia_Man_t * pNew, * pTemp; int i, iLit = 1;
+    Vec_Int_t * vBitsA = Vec_IntAlloc( nBits + 1 );
+    Vec_Int_t * vBitsB = Vec_IntAlloc( nBits + 1 );
+    pNew = Gia_ManStart( 6*nBits+10 );
+    pNew->pName = Abc_UtilStrsav( "comp" );
+    Gia_ManHashAlloc( pNew );
+    if ( fInterleave ) {
+        for ( i = 0; i < nBits; i++ )
+            Vec_IntPush( vBitsA, Gia_ManAppendCi(pNew) ),
+            Vec_IntPush( vBitsB, Gia_ManAppendCi(pNew) );
+    }
+    else {
+        for ( i = 0; i < nBits; i++ )
+            Vec_IntPush( vBitsA, Gia_ManAppendCi(pNew) );
+        for ( i = 0; i < nBits; i++ )
+            Vec_IntPush( vBitsB, Gia_ManAppendCi(pNew) );
+    }
+    Vec_IntPush( vBitsA, 0 );
+    Vec_IntPush( vBitsB, 0 );
+    for ( i = 0; i < nBits; i++ ) {
+        int iLitA0  = Vec_IntEntry(vBitsA, i);
+        int iLitA1  = Vec_IntEntry(vBitsA, i+1);
+        int iLitB0  = Vec_IntEntry(vBitsB, i);
+        int iLitB1  = Vec_IntEntry(vBitsB, i+1);
+        int iOrLit0;
+        if ( i == 0 )
+            iOrLit0 = Gia_ManHashOr(pNew, Abc_LitNotCond(iLitA0, !(i&1)), Abc_LitNotCond(iLitB0, i&1));
+        else
+            iOrLit0 = Gia_ManHashAnd(pNew, Abc_LitNotCond(iLitA0, !(i&1)), Abc_LitNotCond(iLitB0, i&1));
+        int iOrLit1 = Gia_ManHashAnd(pNew, Abc_LitNotCond(iLitA1, !(i&1)), Abc_LitNotCond(iLitB1, i&1));
+        int iOrLit  = Gia_ManHashOr(pNew, iOrLit0, iOrLit1 );
+        iLit = Gia_ManHashOr(pNew, Abc_LitNot(iLit), iOrLit );
+    }
+    Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, nBits&1) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    Vec_IntFree( vBitsA );
+    Vec_IntFree( vBitsB );
+    return pNew;        
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates optimized AIG for the decoder and the multiplexer.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_GenDecoder( Gia_Man_t * p, int * pLits, int nLits )
+{
+    if ( nLits == 1 )
+    {
+        Vec_Int_t * vRes = Vec_IntAlloc( 2 );
+        Vec_IntPush( vRes, Abc_LitNot(pLits[0]) );
+        Vec_IntPush( vRes, pLits[0] );
+        return vRes;
+    }
+    assert( nLits > 1 );
+    int nPart1 = nLits / 2;
+    int nPart2 = nLits - nPart1;
+    Vec_Int_t * vRes1 = Gia_GenDecoder( p, pLits, nPart1 );
+    Vec_Int_t * vRes2 = Gia_GenDecoder( p, pLits+nPart1, nPart2 );
+    Vec_Int_t * vRes = Vec_IntAlloc( Vec_IntSize(vRes1) * Vec_IntSize(vRes2) );
+    int i, k, Lit1, Lit2;
+    Vec_IntForEachEntry( vRes2, Lit2, k )
+    Vec_IntForEachEntry( vRes1, Lit1, i )
+        Vec_IntPush( vRes, Gia_ManHashAnd(p, Lit1, Lit2) );
+    Vec_IntFree( vRes1 );
+    Vec_IntFree( vRes2 );
+    return vRes;   
+}
+Gia_Man_t * Gia_ManGenMux( int nIns, char * pNums )
+{
+    Vec_Int_t * vIns  = Vec_IntAlloc( nIns );
+    Vec_Int_t * vData = Vec_IntAlloc( 1 << nIns );    
+    Gia_Man_t * p = Gia_ManStart( 4*(1 << nIns) + nIns ), * pTemp; 
+    int i, iStart = 0, nSize = 1 << nIns;
+    p->pName = Abc_UtilStrsav( "mux" );
+    for ( i = 0; i < nIns; i++ )
+        Vec_IntPush( vIns, Gia_ManAppendCi(p) );
+    for ( i = 0; i < nSize; i++ )
+        Vec_IntPush( vData, Gia_ManAppendCi(p) );
+    Gia_ManHashAlloc( p );
+    for ( i = (int)strlen(pNums)-1; i >= 0; i-- )
+    {
+        int k, b, nBits = (int)(pNums[i] - '0');
+        Vec_Int_t * vDec = Gia_GenDecoder( p, Vec_IntEntryP(vIns, iStart), nBits );
+        for ( k = 0; k < nSize; k++ )
+            Vec_IntWriteEntry( vData, k, Gia_ManHashAnd(p, Vec_IntEntry(vData, k), Vec_IntEntry(vDec, k%Vec_IntSize(vDec))) );
+        for ( b = 0; b < nBits; b++, nSize /= 2 )
+            for ( k = 0; k < nSize/2; k++ )
+                Vec_IntWriteEntry( vData, k, Gia_ManHashOr(p, Vec_IntEntry(vData, 2*k), Vec_IntEntry(vData, 2*k+1)) );
+        Vec_IntFree( vDec );
+        iStart += nBits;
+    }
+    assert( nSize == 1 );
+    Gia_ManAppendCo( p, Vec_IntEntry(vData, 0) );
+    Vec_IntFree( vIns );
+    Vec_IntFree( vData );    
+    p = Gia_ManCleanup( pTemp = p );
+    Gia_ManStop( pTemp );
+    return p;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaIf.c

@@ -2208,7 +2208,7 @@ void Gia_ManMappingVerify( Gia_Man_t * p )
             continue;
         if ( !Gia_ObjIsLut(p, Gia_ObjId(p, pFanin)) )
         {
-            Abc_Print( -1, "Gia_ManMappingVerify: CO driver %d does not have mapping.\n", Gia_ObjId(p, pFanin) );
+            Abc_Print( -1, "Gia_ManMappingVerify: Buffer driver %d does not have mapping.\n", Gia_ObjId(p, pFanin) );
             Result = 0;
             continue;
         }

src/aig/gia/giaMinLut.c

@@ -193,7 +193,7 @@ Gia_Man_t * Vec_WrdReadTest( char * pFileName )
 void Vec_WrdReadText( char * pFileName, Vec_Wrd_t ** pvSimI, Vec_Wrd_t ** pvSimO, int nIns, int nOuts )
 {
     int i, nSize, iLine, nLines, nWords;
-    char pLine[1000];
+    char pLine[2000];
     Vec_Wrd_t * vSimI, * vSimO;
     FILE * pFile = fopen( pFileName, "rb" );
     if ( pFile == NULL )
@@ -214,7 +214,7 @@ void Vec_WrdReadText( char * pFileName, Vec_Wrd_t ** pvSimI, Vec_Wrd_t ** pvSimO
     nWords = (nLines + 63)/64;
     vSimI  = Vec_WrdStart( nIns *nWords );
     vSimO  = Vec_WrdStart( nOuts*nWords );
-    for ( iLine = 0; fgets( pLine, 1000, pFile ); iLine++ )
+    for ( iLine = 0; fgets( pLine, 2000, pFile ); iLine++ )
     {
         for ( i = 0; i < nIns; i++ )
             if ( pLine[nIns-1-i] == '1' )
@@ -233,7 +233,7 @@ void Vec_WrdReadText( char * pFileName, Vec_Wrd_t ** pvSimI, Vec_Wrd_t ** pvSimO
 int Vec_WrdReadText2( char * pFileName, Vec_Wrd_t ** pvSimI )
 {
     int i, nSize, iLine, nLines, nWords, nIns;
-    char pLine[1000];
+    char pLine[2000];
     Vec_Wrd_t * vSimI;
     FILE * pFile = fopen( pFileName, "rb" );
     if ( pFile == NULL )
@@ -241,7 +241,7 @@ int Vec_WrdReadText2( char * pFileName, Vec_Wrd_t ** pvSimI )
         printf( "Cannot open file \"%s\" for reading.\n", pFileName );
         return 0;
     }
-    if ( !fgets(pLine, 1000, pFile) || (nIns = strlen(pLine)-1) < 1 )
+    if ( !fgets(pLine, 2000, pFile) || (nIns = strlen(pLine)-1) < 1 )
     {
         printf( "Cannot find the number of inputs in file \"%s\".\n", pFileName );
         fclose( pFile );
@@ -259,7 +259,7 @@ int Vec_WrdReadText2( char * pFileName, Vec_Wrd_t ** pvSimI )
     nLines = nSize / (nIns + 1);
     nWords = (nLines + 63)/64;
     vSimI  = Vec_WrdStart( nIns *nWords );
-    for ( iLine = 0; fgets( pLine, 1000, pFile ); iLine++ )
+    for ( iLine = 0; fgets( pLine, 2000, pFile ); iLine++ )
     {
         for ( i = 0; i < nIns; i++ )
             if ( pLine[nIns-1-i] == '1' )

src/aig/gia/giaMulFind.c

@@ -31,6 +31,403 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManMulFindXors2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXor )
+{
+    if ( !Gia_ObjIsAnd(pObj) )
+        return;
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( !pObj->fMark0 ) 
+    {
+        if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) 
+           && Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) >= 4 
+           && Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) >= 4 )
+            Vec_IntPushTwo( vXor, Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninId1p(p, pObj) );
+        return;
+    }
+    Gia_Obj_t * pFan0, * pFan1;
+    int RetValue = Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1);
+    assert( RetValue );
+    Gia_ManMulFindXors2_rec( p, Gia_Regular(pFan0), vXor );
+    Gia_ManMulFindXors2_rec( p, Gia_Regular(pFan1), vXor );
+}
+Vec_Wec_t * Gia_ManMulFindXors2( Gia_Man_t * p )
+{
+    Vec_Wec_t * vXors = Vec_WecAlloc( 100 );
+    Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
+    Gia_Obj_t * pObj, * pFan0, * pFan1; int i;
+    Gia_ManCreateRefs( p );
+    Gia_ManCleanMark01( p );
+    Gia_ManForEachAnd( p, pObj, i ) {
+        if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+            continue;
+        Gia_Regular(pFan0)->fMark1 = 1;
+        Gia_Regular(pFan1)->fMark1 = 1;
+        pObj->fMark0 = 1;
+    }
+    Gia_ManForEachAnd( p, pObj, i ) {
+        if ( pObj->fMark0 && !pObj->fMark1 ) {
+            Gia_ManIncrementTravId( p );
+            Vec_IntClear( vTemp );
+            Gia_ManMulFindXors2_rec( p, pObj, vTemp );
+            if ( Vec_IntSize(vTemp) > 0 )
+                Vec_IntAppend( Vec_WecPushLevel(vXors), vTemp );
+        }
+    }
+    Vec_IntFree( vTemp );
+    return vXors;
+}
+int Gia_ManMulFindMaxSize( Vec_Wec_t * vXors, Vec_Int_t * vUsed )
+{
+    Vec_Int_t * vLevel; int i, iBest = -1, nBestSize = 0;
+    Vec_WecForEachLevel( vXors, vLevel, i )
+        if ( !Vec_IntEntry(vUsed, i) && nBestSize < Vec_IntSize(vLevel) )
+            nBestSize = Vec_IntSize(vLevel), iBest = i;
+    return iBest;
+}
+int Gia_ManMulFindGetOverlap( Vec_Int_t * p1, Vec_Int_t * p2 )
+{
+    int i, k, ObjI, ObjK, Counter = 0;
+    Vec_IntForEachEntry( p1, ObjI, i )
+    Vec_IntForEachEntry( p2, ObjK, k )
+        if ( ObjI == ObjK )
+            Counter++;
+    return Counter;
+}
+int Gia_ManMulFindGetOverlap2( Vec_Int_t * p1, Vec_Int_t * p2 )
+{
+    int i, k, ObjI, ObjK, Counter = 0;
+    Vec_IntForEachEntryStart( p1, ObjI, i, 1 )
+    Vec_IntForEachEntry( p2, ObjK, k )
+        if ( ObjI == ObjK )
+            Counter++;
+    return Counter;
+}
+int Gia_ManMulFindMaxOverlap( Vec_Wec_t * vXors, Vec_Int_t * vUsed, Vec_Int_t * vFound )
+{
+    Vec_Int_t * vLevel; int i, iBest = -1, nThisSize, nBestSize = 0;
+    Vec_WecForEachLevel( vXors, vLevel, i )
+        if ( !Vec_IntEntry(vUsed, i) && nBestSize < (nThisSize = Gia_ManMulFindGetOverlap(vFound, vLevel)) )
+            nBestSize = nThisSize, iBest = i;
+    return iBest;
+}
+Vec_Wec_t * Gia_ManMulFindSets( Gia_Man_t * p, Vec_Wec_t * vXors )
+{
+    Vec_Wec_t * vSets = Vec_WecAlloc( 100 );
+    Vec_Int_t * vUsed = Vec_IntStart( Vec_WecSize(vXors) );
+    Vec_Int_t * vFound = Vec_IntAlloc( 100 ); int Item, k, Obj;
+    while ( (Item = Gia_ManMulFindMaxSize(vXors, vUsed)) != -1 ) {
+        Vec_Int_t * vTemp = Vec_WecEntry(vXors, Item);
+        Vec_Int_t * vNew = Vec_WecPushLevel( vSets );
+        Vec_IntPush( vNew, Item );
+        Vec_IntWriteEntry( vUsed, Item, 1 );
+        Vec_IntClear( vFound );
+        Vec_IntAppend( vFound, vTemp );
+        while ( (Item = Gia_ManMulFindMaxOverlap(vXors, vUsed, vFound)) != -1 ) {
+            Vec_IntPush( vNew, Item );
+            Vec_IntWriteEntry( vUsed, Item, 1 );
+            vTemp = Vec_WecEntry(vXors, Item);
+            Vec_IntForEachEntry( vTemp, Obj, k )
+                Vec_IntPushUnique( vFound, Obj );
+        }
+    }
+    Vec_IntFree( vUsed );
+    Vec_IntFree( vFound );
+    return vSets;
+}
+int Gia_ManMulFindOne( Gia_Man_t * p, Vec_Wec_t * vXors, Vec_Int_t * vSet, Vec_Int_t * vMap, Vec_Int_t * vA, Vec_Int_t * vB, int fVerbose )
+{
+    Vec_Int_t * vObjs = Vec_IntAlloc( 100 ); int i, j, Obj, Obj1, Obj2;
+    Vec_IntForEachEntry( vSet, Obj, i )
+        Vec_IntAppend( vObjs, Vec_WecEntry(vXors, Obj) );
+    Vec_IntForEachEntry( vObjs, Obj, i )
+        Vec_IntAddToEntry( vMap, Obj, 1 );
+    Vec_IntForEachEntry( vSet, Obj, i ) {
+        Vec_Int_t * vTemp = Vec_WecEntry(vXors, Obj); int k = 0;
+        Vec_IntForEachEntryDouble( vTemp, Obj1, Obj2, j )
+            if ( Vec_IntEntry(vMap, Obj1) > 1 || Vec_IntEntry(vMap, Obj2) > 1 )
+                Vec_IntWriteEntry(vTemp, k++, Obj1), Vec_IntWriteEntry(vTemp, k++, Obj2);
+        Vec_IntShrink( vTemp, k );
+    }
+    Vec_IntForEachEntry( vObjs, Obj, i )
+        Vec_IntWriteEntry( vMap, Obj, 0 );
+    Vec_IntClear( vObjs );
+    Vec_IntForEachEntry( vSet, Obj, i )
+        Vec_IntAppend( vObjs, Vec_WecEntry(vXors, Obj) );        
+    if ( Vec_IntSize(vObjs) == 0 ) {
+        Vec_IntFree(vObjs);
+        return 0;
+    }
+
+    Vec_IntClear( vA );
+    Vec_IntClear( vB );
+    Vec_IntPush( vA, Vec_IntPop(vObjs) );
+    Vec_IntPush( vB, Vec_IntPop(vObjs) );
+    while ( Vec_IntSize(vObjs) > 0 ) {
+        int k = 0;
+        Vec_IntForEachEntryDouble( vObjs, Obj1, Obj2, j ) {
+            if ( Vec_IntFind(vA, Obj1) >= 0 )
+                Vec_IntPushUnique(vB, Obj2);
+            else if ( Vec_IntFind(vA, Obj2) >= 0 )
+                Vec_IntPushUnique(vB, Obj1);
+            else if ( Vec_IntFind(vB, Obj1) >= 0 )
+                Vec_IntPushUnique(vA, Obj2);
+            else if ( Vec_IntFind(vB, Obj2) >= 0 )
+                Vec_IntPushUnique(vA, Obj1);
+            else {
+                Vec_IntWriteEntry(vObjs, k++, Obj1);
+                Vec_IntWriteEntry(vObjs, k++, Obj2);
+            }
+        }
+        Vec_IntShrink( vObjs, k );
+    }
+    Vec_IntSort( vA, 0 );
+    Vec_IntSort( vB, 0 );
+    Vec_IntClear( vObjs );
+    Vec_IntForEachEntry( vSet, Obj, i )
+        Vec_IntAppend( vObjs, Vec_WecEntry(vXors, Obj) );
+    Vec_IntForEachEntryDouble( vObjs, Obj1, Obj2, j )
+        if ( !((Vec_IntFind(vA, Obj1) >= 0 && Vec_IntFind(vB, Obj2) >= 0) ||
+               (Vec_IntFind(vA, Obj2) >= 0 && Vec_IntFind(vB, Obj1) >= 0)) ) {
+            if ( fVerbose )
+            printf( "Internal verification failed.\n" );
+            Vec_IntFree( vObjs );
+            Vec_IntClear( vA );
+            Vec_IntClear( vB );
+            return 0;
+        }
+    if ( fVerbose )
+    printf( "Generated system with %d+%d+%d=%d variables and %d equations.\n", 
+        Vec_IntSize(vA),Vec_IntSize(vB),Vec_IntSize(vSet), 
+        Vec_IntSize(vA)+Vec_IntSize(vB)+Vec_IntSize(vSet), Vec_IntSize(vObjs)/2 );
+    Vec_IntFree( vObjs );
+    return 1;
+}
+Vec_Wec_t * Gia_ManMulFindAInputs2( Gia_Man_t * p, int fVerbose )
+{
+    Vec_Wec_t * vMuls = Vec_WecAlloc( 10 );
+    Vec_Wec_t * vXors = Gia_ManMulFindXors2( p );
+    Vec_Wec_t * vSets = Gia_ManMulFindSets( p, vXors );
+    Vec_Int_t * vMap  = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vA = Vec_IntAlloc( 100 );
+    Vec_Int_t * vB = Vec_IntAlloc( 100 );    
+    Vec_Int_t * vSet; int i;
+    Vec_WecForEachLevel( vSets, vSet, i )
+    {
+        if ( !Gia_ManMulFindOne(p, vXors, vSet, vMap, vA, vB, fVerbose) )
+            continue;
+        Vec_IntAppend( Vec_WecPushLevel(vMuls), vA );
+        Vec_IntAppend( Vec_WecPushLevel(vMuls), vB );
+        Vec_WecPushLevel(vMuls);
+    }
+    Vec_WecFree( vXors );
+    Vec_WecFree( vSets );
+    Vec_IntFree( vMap );
+    Vec_IntFree( vA );
+    Vec_IntFree( vB );
+    return vMuls;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManMulFindAddEntry1( Vec_Int_t * vPairs, int Obj )
+{
+    int Entry, Sum, k;
+    Vec_IntForEachEntryDouble( vPairs, Entry, Sum, k )
+        if ( Obj == Entry ) {
+            Vec_IntAddToEntry( vPairs, k+1, 1 );
+            break;
+        }
+    if ( k == Vec_IntSize(vPairs) )
+        Vec_IntPushTwo( vPairs, Obj, 1 );            
+}
+Vec_Int_t * Gia_ManMulFindCounts( Vec_Wec_t * vCuts4, Vec_Int_t * vSet )
+{
+    Vec_Int_t * vCounts = Vec_IntAlloc( 10 );
+    int i, k, Obj, Item;
+    Vec_IntForEachEntry( vSet, Item, i ) {
+        Vec_Int_t * vCut = Vec_WecEntry(vCuts4, Item);
+        Vec_IntForEachEntryStart( vCut, Obj, k, 1 )
+            Gia_ManMulFindAddEntry1( vCounts, Obj );
+    }
+    return vCounts;
+}
+int Gia_ManMulFindNextEntry( Vec_Wec_t * vCuts4, Vec_Int_t * vSet, int Entry )
+{
+    int i, Item;
+    Vec_IntForEachEntry( vSet, Item, i ) {
+        Vec_Int_t * vCut = Vec_WecEntry(vCuts4, Item);
+        if ( Vec_IntSize(vCut) == 0 )
+            continue;
+        assert( Vec_IntSize(vCut) == 3 );
+        int RetValue = -1;
+        if ( Vec_IntEntry(vCut, 1) == Entry )
+            RetValue = Vec_IntEntry(vCut, 2);
+        if ( Vec_IntEntry(vCut, 2) == Entry )
+            RetValue = Vec_IntEntry(vCut, 1);
+        if ( RetValue == -1 )
+            continue;
+        Vec_IntClear( vCut );
+        return RetValue;
+    }
+    return -1;
+}
+void Gia_ManMulFindArg1( Vec_Wec_t * vCuts4, Vec_Int_t * vSet, Vec_Int_t * vArg1 )
+{
+    Vec_Int_t * vCounts = Gia_ManMulFindCounts( vCuts4, vSet );
+    int Entry = -1, Sum, k;
+    Vec_IntClear( vArg1 );
+    Vec_IntForEachEntryDouble( vCounts, Entry, Sum, k )
+        if ( Sum == 1 ) {
+            Vec_IntPush( vArg1, Entry );
+            break;
+        }
+    assert( Entry != -1 );
+    while ( (Entry = Gia_ManMulFindNextEntry(vCuts4, vSet, Entry)) != -1 )
+        Vec_IntPush( vArg1, Entry );
+    Vec_IntFree( vCounts );
+}
+int Gia_ManMulFindNextEntryCount( Vec_Int_t * vCounts, int Entry0 )
+{
+    int Entry, Sum, k;
+    Vec_IntForEachEntryDouble( vCounts, Entry, Sum, k )
+        if ( Entry == Entry0 )
+            return Sum;
+    return -1;
+}
+int Gia_ManMulFindNextEntry2( Vec_Wec_t * vCuts4, Vec_Int_t * vSet, int Entry, Vec_Int_t * vCounts, int * pEntry0, int * pEntry1 )
+{
+    int i, Item;
+    Vec_IntForEachEntry( vSet, Item, i ) {
+        Vec_Int_t * vCut = Vec_WecEntry(vCuts4, Item);
+        if ( Vec_IntSize(vCut) == 0 )
+            continue;
+        assert( Vec_IntSize(vCut) == 4 );
+        int Entry0, Entry1, iPlace = Vec_IntFind( vCut, Entry );
+        if ( iPlace == -1 )
+            continue;
+        if ( iPlace == 1 )
+            Entry0 = Vec_IntEntry(vCut, 2), Entry1 = Vec_IntEntry(vCut, 3);
+        else if ( iPlace == 2 )
+            Entry0 = Vec_IntEntry(vCut, 1), Entry1 = Vec_IntEntry(vCut, 3);
+        else if ( iPlace == 3 )
+            Entry0 = Vec_IntEntry(vCut, 1), Entry1 = Vec_IntEntry(vCut, 2);
+        else assert( 0 );
+        int Count0 = Gia_ManMulFindNextEntryCount(vCounts, Entry0);
+        int Count1 = Gia_ManMulFindNextEntryCount(vCounts, Entry1);
+        *pEntry0 = Count0 <= Count1 ? Entry0 : Entry1;
+        *pEntry1 = Count0 <= Count1 ? Entry1 : Entry0;
+        // remove entries
+        Vec_IntForEachEntry( vSet, Item, i ) {
+            Vec_Int_t * vCut = Vec_WecEntry(vCuts4, Item);
+            if ( Vec_IntSize(vCut) == 0 )
+                continue;            
+            if ( Vec_IntFind( vCut, Entry ) >= 0 )
+                Vec_IntClear( vCut );
+        }
+        return 1;
+    }
+    return 0;
+}
+void Gia_ManMulFindArg2( Vec_Wec_t * vCuts5, Vec_Int_t * vSet, Vec_Int_t * vArg2, int Entry0, int Entry1 )
+{
+    Vec_Int_t * vCounts = Gia_ManMulFindCounts( vCuts5, vSet );
+    int Entry, Sum, k, SumMin = ABC_INFINITY, SumMax = 0;
+    Vec_IntForEachEntryDouble( vCounts, Entry, Sum, k ) {
+        SumMin = Abc_MinInt( SumMin, Sum );
+        SumMax = Abc_MaxInt( SumMax, Sum );
+    }
+    Vec_IntClear( vArg2 );
+    Vec_IntForEachEntryDouble( vCounts, Entry, Sum, k ) 
+        if ( Entry == Entry0 || Entry == Entry1 ) {
+            Vec_IntPush( vArg2, Entry == Entry0 ? Entry1 : Entry0 );
+            Vec_IntPush( vArg2, Entry );
+            break;
+        }
+    Entry = Vec_IntEntry(vArg2, 1);
+    while ( Gia_ManMulFindNextEntry2(vCuts5, vSet, Entry, vCounts, &Entry0, &Entry1) )
+        Vec_IntPushTwo( vArg2, Entry0, Entry1 ), Entry = Entry1;
+    Vec_IntFree( vCounts );
+}
+void Gia_ManMulFindAddEntry( Vec_Int_t * vPairs, int Obj0, int Obj1 )
+{
+    int Entry0, Entry1, Sum, k;
+    Vec_IntForEachEntryTriple( vPairs, Entry0, Entry1, Sum, k )
+        if ( Obj0 == Entry0 && Obj1 == Entry1 ) {
+            Vec_IntAddToEntry( vPairs, k+2, 1 );
+            break;
+        }
+    if ( k == Vec_IntSize(vPairs) )
+        Vec_IntPushThree( vPairs, Obj0, Obj1, 1 );            
+}
+Vec_Wec_t * Gia_ManMulFindBInputs2( Gia_Man_t * p, Vec_Wec_t * vCuts4, Vec_Wec_t * vCuts5, int fVerbose )
+{
+    Vec_Wec_t * vRes = Vec_WecAlloc( 10 );
+    Vec_Int_t * vPairs = Vec_IntAlloc( 1000 ); 
+    Vec_Int_t * vSet = Vec_IntAlloc( 100 ); 
+    Vec_Int_t * vCut, * vArg1, * vArg2;  
+    int i, j, k, n, Entry0, Entry1, Sum, Obj0, Obj1;
+    Vec_WecForEachLevel( vCuts4, vCut, i )
+    Vec_IntForEachEntryStart( vCut, Obj0, j, 1 )
+    Vec_IntForEachEntryStart( vCut, Obj1, k, j+1 )
+        Gia_ManMulFindAddEntry( vPairs, Obj0, Obj1 );
+    Vec_IntForEachEntryTriple( vPairs, Entry0, Entry1, Sum, n ) {
+        if ( Sum < 3 )
+            continue;
+        Vec_IntClear( vSet );
+        Vec_WecForEachLevel( vCuts4, vCut, i )
+        Vec_IntForEachEntryStart( vCut, Obj0, j, 1 )
+        Vec_IntForEachEntryStart( vCut, Obj1, k, j+1 )
+            if ( Obj0 == Entry0 && Obj1 == Entry1 ) {
+                Vec_IntPush( vSet, i );
+                Vec_IntDrop( vCut, k );
+                Vec_IntDrop( vCut, j );
+                j = k = Vec_IntSize(vCut);
+            }
+        vArg1 = Vec_WecPushLevel(vRes);
+        vArg2 = Vec_WecPushLevel(vRes);
+        Vec_WecPushLevel(vRes);        
+        Gia_ManMulFindArg1( vCuts4, vSet, vArg1 );
+        // find overlapping with arg1 and remove nodes in arg1
+        Vec_IntClear( vSet );
+        Vec_WecForEachLevel( vCuts5, vCut, i )
+            if ( Gia_ManMulFindGetOverlap2(vCut, vArg1) ) {
+                k = 1;
+                Vec_IntForEachEntryStart( vCut, Obj0, j, 1 )
+                    if ( Vec_IntFind(vArg1, Obj0) == -1 )
+                        Vec_IntWriteEntry( vCut, k++, Obj0 );
+                Vec_IntShrink( vCut, k );
+                Vec_IntPush( vSet, i );
+            }
+        Gia_ManMulFindArg2( vCuts5, vSet, vArg2, Entry0, Entry1 );
+    }
+    Vec_IntFree( vSet );
+    Vec_IntFree( vPairs );
+    return vRes;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -331,6 +728,7 @@ Vec_Wrd_t * Gia_ManMulFindSim( Vec_Wrd_t * vSim0, Vec_Wrd_t * vSim1, int fSigned
 }
 void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fVerbose )
 {
+    Abc_Random(1);
     for ( int m = 0; m < Vec_WecSize(vTerms)/3; m++ ) {
         Vec_Int_t * vIn0 = Vec_WecEntry(vTerms, 3*m+0);
         Vec_Int_t * vIn1 = Vec_WecEntry(vTerms, 3*m+1);
@@ -341,46 +739,47 @@ void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fVerbose )
         Vec_Wrd_t * vSimS = Gia_ManMulFindSim( vSim0, vSim1, 1 );
         Vec_Int_t * vTfo  = Gia_ManMulFindTfo( p, vIn0, vIn1 );
         Vec_Wrd_t * vSims = Gia_ManMulFindSimCone( p, vIn0, vIn1, vSim0, vSim1, vTfo );
+        Vec_Int_t * vOutU = Vec_IntAlloc( 100 );
+        Vec_Int_t * vOutS = Vec_IntAlloc( 100 );
         word Word; int w, iPlace;
-        assert( Vec_IntSize(vOut) == 0 );
         Vec_WrdForEachEntry( vSimU, Word, w ) {
             if ( (iPlace = Vec_WrdFind(vSims, Word)) >= 0 )
-                Vec_IntPush( vOut, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 0) );
+                Vec_IntPush( vOutU, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 0) );
             else if ( (iPlace = Vec_WrdFind(vSims, ~Word)) >= 0 )
-                Vec_IntPush( vOut, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 1) );
+                Vec_IntPush( vOutU, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 1) );
             else
-                break;                             
+                Vec_IntPush( vOutU, -1 );                  
         }
-        if ( w == Vec_WrdSize(vSimU) )
-            Vec_IntPush(vOut, 0);
-        else
-            Vec_IntClear(vOut);
-        if ( Vec_IntSize(vOut) == 0 )
+        Vec_WrdForEachEntry( vSimS, Word, w ) {
+            if ( (iPlace = Vec_WrdFind(vSims, Word)) >= 0 )
+                Vec_IntPush( vOutS, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 0) );
+            else if ( (iPlace = Vec_WrdFind(vSims, ~Word)) >= 0 )
+                Vec_IntPush( vOutS, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 1) );
+            else
+                Vec_IntPush( vOutS, -1 );
+        }
+        assert( Vec_IntSize(vOut) == 0 );
+        if ( Vec_IntCountEntry(vOutU, -1) < Vec_IntSize(vOutU) ||
+             Vec_IntCountEntry(vOutS, -1) < Vec_IntSize(vOutS) )
         {
-            Vec_IntClear(vOut);
-            Vec_WrdForEachEntry( vSimS, Word, w ) {
-                if ( (iPlace = Vec_WrdFind(vSims, Word)) >= 0 )
-                    Vec_IntPush( vOut, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 0) );
-                else if ( (iPlace = Vec_WrdFind(vSims, ~Word)) >= 0 )
-                    Vec_IntPush( vOut, Abc_Var2Lit(Vec_IntEntry(vTfo, iPlace), 1) );
-                else
-                    break;                             
-            }
-            if ( w == Vec_WrdSize(vSimS) )
-                Vec_IntPush(vOut, 1);
+            if ( Vec_IntCountEntry(vOutU, -1) < Vec_IntCountEntry(vOutS, -1) )
+                Vec_IntAppend( vOut, vOutU ), Vec_IntPush(vOut, 0);
             else
-                Vec_IntClear(vOut);
+                Vec_IntAppend( vOut, vOutS ), Vec_IntPush(vOut, 1);
         }
+        else
+        {
+            Vec_IntClear(vIn0);
+            Vec_IntClear(vIn1);
+        }        
         Vec_WrdFree( vSim0 );
         Vec_WrdFree( vSim1 );
         Vec_WrdFree( vSimU );
         Vec_WrdFree( vSimS );
         Vec_WrdFree( vSims );
         Vec_IntFree( vTfo );
-        if ( Vec_IntSize(vOut) )
-            continue;
-        Vec_IntClear(vIn0);
-        Vec_IntClear(vIn1);
+        Vec_IntFree( vOutU );
+        Vec_IntFree( vOutS );
     }
     Vec_WecRemoveEmpty( vTerms );
 }
@@ -413,7 +812,7 @@ Vec_Ptr_t * Gia_ManMulFindCuts( Gia_Man_t * p, int nCutNum, int fVerbose )
 Vec_Wec_t * Gia_ManMulFindA( Gia_Man_t * p, Vec_Wec_t * vCuts3, int fVerbose )
 {
     Vec_Wec_t * vXors = Gia_ManMulFindXors( p, vCuts3, fVerbose );
-    Vec_Wec_t * vTerms = Gia_ManMulFindAInputs( p, vXors, fVerbose );
+    Vec_Wec_t * vTerms = Gia_ManMulFindAInputs2( p, fVerbose );
     if ( Vec_WecSize(vTerms) )
         Gia_ManMulFindOutputs( p, vTerms, fVerbose );          
     Vec_WecFree( vXors );
@@ -423,7 +822,7 @@ Vec_Wec_t * Gia_ManMulFindB( Gia_Man_t * p, Vec_Wec_t * vCuts4, Vec_Wec_t * vCut
 {
     Vec_Wec_t * vTerms = Vec_WecAlloc( 12 );
     if ( Vec_WecSize(vCuts4) && Vec_WecSize(vCuts5) )
-        vTerms = Gia_ManMulFindBInputs( p, vCuts4, vCuts5, fVerbose );
+        vTerms = Gia_ManMulFindBInputs2( p, vCuts4, vCuts5, fVerbose );
     if ( Vec_WecSize(vTerms) )
         Gia_ManMulFindOutputs( p, vTerms, fVerbose );
     return vTerms;
@@ -432,8 +831,12 @@ void Gia_ManMulFindPrintSet( Vec_Int_t * vSet, int fLit, int fSkipLast )
 {
     int i, Temp, Limit = Vec_IntSize(vSet) - fSkipLast;
     printf( "{" );
-    Vec_IntForEachEntryStop( vSet, Temp, i, Limit )
-        printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" );
+    Vec_IntForEachEntryStop( vSet, Temp, i, Limit ) {
+        if ( Temp == -1 )
+            printf( "n/a%s", i < Limit-1 ? " ":"" );
+        else
+            printf( "%s%d%s", (fLit & Abc_LitIsCompl(Temp)) ? "~":"", fLit ? Abc_Lit2Var(Temp) : Temp, i < Limit-1 ? " ":"" );
+    }
     printf( "}" );
 }
 void Gia_ManMulFindPrintOne( Vec_Wec_t * vTerms, int m, int fBooth )
@@ -441,7 +844,7 @@ void Gia_ManMulFindPrintOne( Vec_Wec_t * vTerms, int m, int fBooth )
     Vec_Int_t * vIn0 = Vec_WecEntry(vTerms, 3*m+0);
     Vec_Int_t * vIn1 = Vec_WecEntry(vTerms, 3*m+1);
     Vec_Int_t * vOut = Vec_WecEntry(vTerms, 3*m+2);
-    printf( "%sooth %ssigned : ", fBooth ? "B" : "Non-b", Vec_IntEntryLast(vOut) ? "" : "un" );
+    printf( "%sooth %ssigned %d x %d: ", fBooth ? "B" : "Non-b", Vec_IntEntryLast(vOut) ? "" : "un", Vec_IntSize(vIn0), Vec_IntSize(vIn1) );
     Gia_ManMulFindPrintSet( vIn0, 0, 0 );
     printf( " * " );
     Gia_ManMulFindPrintSet( vIn1, 0, 0 );

src/aig/gia/giaPat2.c

@@ -1372,6 +1372,65 @@ void Min_ManTest2( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_GenerateCexesDumpBlif( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCexes )
+{
+    extern Vec_Ptr_t * Gia_GetFakeNames( int nNames, int fCaps );
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL ) {
+        printf( "Cannot open output file name \"%s\".\n", pFileName );
+        return;
+    }
+    int fFakeIns = 0, fFakeOuts = 0;
+    if ( p->vNamesIn == NULL )
+        p->vNamesIn = Gia_GetFakeNames( Gia_ManCiNum(p), 0 ), fFakeIns = 1;
+    if ( p->vNamesOut == NULL )
+        p->vNamesOut = Gia_GetFakeNames( Gia_ManCoNum(p), 1 ), fFakeOuts = 1;
+
+    Gia_Obj_t * pObj, * pObj2; 
+    char * pLine = ABC_CALLOC( char, Gia_ManCiNum(p)+3 );
+    int i, k, c, iLit, nOuts[2] = {0}, nCexes = Vec_WecSize(vCexes) / Gia_ManCoNum(p);
+    fprintf( pFile, "# Satisfying assignments for the primary outputs generated by ABC on %s\n", Gia_TimeStamp() );
+    fprintf( pFile, ".model %s\n", p->pName );
+    fprintf( pFile, ".inputs" );
+    Gia_ManForEachCi( p, pObj, i )
+        fprintf( pFile, " %s", Gia_ObjCiName(p, i) );
+    fprintf( pFile, "\n.outputs" );
+    Gia_ManForEachCo( p, pObj, i )
+        fprintf( pFile, " %s", Gia_ObjCoName(p, i) );
+    fprintf( pFile, "\n" );
+    Gia_ManForEachCo( p, pObj, i ) {
+        if ( Gia_ObjFaninLit0p(p, pObj) == 0 ) {
+            fprintf( pFile, ".names %s\n", Gia_ObjCoName(p, i) );
+            nOuts[0]++;
+        }
+        else if ( Gia_ObjFaninLit0p(p, pObj) == 1 ) {
+            fprintf( pFile, ".names %s\n 1\n", Gia_ObjCiName(p, i) );
+            nOuts[1]++;
+        }
+        else {
+            fprintf( pFile, ".names" );
+            Gia_ManForEachCi( p, pObj2, c )
+                fprintf( pFile, " %s", Gia_ObjCiName(p, c) );
+            fprintf( pFile, " %s\n", Gia_ObjCoName(p, i) );
+            for ( c = 0; c < nCexes; c++ ) {
+                Vec_Int_t * vPat = Vec_WecEntry( vCexes, i*nCexes+c );
+                memset(pLine, '-', Gia_ManCiNum(p) );
+                Vec_IntForEachEntry( vPat, iLit, k )
+                    pLine[Abc_Lit2Var(iLit)-1] = '1' - Abc_LitIsCompl(iLit);
+                fprintf( pFile, "%s 1\n", pLine );
+            }
+            nOuts[1]++;
+        }
+    }
+    fprintf( pFile, ".end\n\n" );
+    fclose( pFile );
+    printf( "Information about %d sat, %d unsat, and %d undecided primary outputs was written into BLIF file \"%s\".\n", 
+        nOuts[1], nOuts[0], Gia_ManCoNum(p)-nOuts[1]-nOuts[0], pFileName );    
+    free( pLine );
+
+    if ( fFakeIns )  Vec_PtrFreeFree( p->vNamesIn  ), p->vNamesIn  = NULL;
+    if ( fFakeOuts ) Vec_PtrFreeFree( p->vNamesOut ), p->vNamesOut = NULL;
+}
 void Gia_GenerateCexesDumpFile( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCexes, int fShort )
 {
     FILE * pFile = fopen( pFileName, "wb" );
@@ -1416,13 +1475,16 @@ void Gia_GenerateCexesDumpFile( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCe
     fclose( pFile );
     free( pLine );
 }
-void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fVerbose, int fVeryVerbose )
+void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fBlif, int fVerbose, int fVeryVerbose )
 {
     unsigned Start = Abc_Random(1);
     Vec_Int_t * vStats[3] = {0}; int i;
     Vec_Wec_t * vCexes  = Min_ManComputeCexes( p, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose );    
     assert( Vec_WecSize(vCexes) == Gia_ManCoNum(p) * nMinCexes );
-    Gia_GenerateCexesDumpFile( pFileName, p, vCexes, fShort );
+    if ( fBlif )
+        Gia_GenerateCexesDumpBlif( pFileName, p, vCexes );
+    else
+        Gia_GenerateCexesDumpFile( pFileName, p, vCexes, fShort );
     for ( i = 0; i < 3; i++ )
       Vec_IntFreeP( &vStats[i] );
     Vec_WecFree( vCexes );

src/aig/gia/giaTtopt.cpp

@@ -1176,6 +1176,17 @@ Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, c
     {
         vSupp = Gia_ManCollectSuppNew( p, g, nOuts );
         nInputs = Vec_IntSize( vSupp );
+        if ( nInputs == 0 )
+        {
+            for ( k = 0; k < nOuts; k++ )
+            {
+                pObj = Gia_ManCo( p, g+k );
+                pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ObjFanin0(pObj), vSupp );
+                Gia_ManAppendCo( pNew, pTruth[0] & 1 );
+            }
+            Vec_IntFree( vSupp );
+            continue;
+        }
         Ttopt::TruthTableLevelTSM tt( nInputs, nOuts );
         for ( k = 0; k < nOuts; k++ )
         {

src/aig/gia/giaUtil.c

@@ -140,6 +140,42 @@ char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix )
     return Buffer;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Gia_GetFakeNames( int nNames, int fCaps )
+{
+    Vec_Ptr_t * vNames;
+    char Buffer[5];
+    int i;
+
+    vNames = Vec_PtrAlloc( nNames );
+    for ( i = 0; i < nNames; i++ )
+    {
+        if ( nNames < 26 )
+        {
+            Buffer[0] = (fCaps ? 'A' : 'a') + i;
+            Buffer[1] = 0;
+        }
+        else
+        {
+            Buffer[0] = (fCaps ? 'A' : 'a') + i%26;
+            Buffer[1] = '0' + i/26;
+            Buffer[2] = 0;
+        }
+        Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) );
+    }
+    return vNames;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -760,6 +796,23 @@ void Gia_ManCreateRefs( Gia_Man_t * p )
             Gia_ObjRefFanin0Inc( p, pObj );
     }
 }
+void Gia_ManCreateLitRefs( Gia_Man_t * p )  
+{
+    Gia_Obj_t * pObj;
+    int i;
+    assert( p->pRefs == NULL );
+    p->pRefs = ABC_CALLOC( int, 2*Gia_ManObjNum(p) );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            p->pRefs[Gia_ObjFaninLit0(pObj, i)]++;
+            p->pRefs[Gia_ObjFaninLit1(pObj, i)]++;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+            p->pRefs[Gia_ObjFaninLit0(pObj, i)]++;
+    }
+}
 
 /**Function*************************************************************
 
@@ -3279,73 +3332,6 @@ void Gia_ManTestProblem()
     }
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_GenDecoder( Gia_Man_t * p, int * pLits, int nLits )
-{
-    if ( nLits == 1 )
-    {
-        Vec_Int_t * vRes = Vec_IntAlloc( 2 );
-        Vec_IntPush( vRes, Abc_LitNot(pLits[0]) );
-        Vec_IntPush( vRes, pLits[0] );
-        return vRes;
-    }
-    assert( nLits > 1 );
-    int nPart1 = nLits / 2;
-    int nPart2 = nLits - nPart1;
-    Vec_Int_t * vRes1 = Gia_GenDecoder( p, pLits, nPart1 );
-    Vec_Int_t * vRes2 = Gia_GenDecoder( p, pLits+nPart1, nPart2 );
-    Vec_Int_t * vRes = Vec_IntAlloc( Vec_IntSize(vRes1) * Vec_IntSize(vRes2) );
-    int i, k, Lit1, Lit2;
-    Vec_IntForEachEntry( vRes2, Lit2, k )
-    Vec_IntForEachEntry( vRes1, Lit1, i )
-        Vec_IntPush( vRes, Gia_ManHashAnd(p, Lit1, Lit2) );
-    Vec_IntFree( vRes1 );
-    Vec_IntFree( vRes2 );
-    return vRes;   
-}
-Gia_Man_t * Gia_ManGenMux( int nIns, char * pNums )
-{
-    Vec_Int_t * vIns  = Vec_IntAlloc( nIns );
-    Vec_Int_t * vData = Vec_IntAlloc( 1 << nIns );    
-    Gia_Man_t * p = Gia_ManStart( 4*(1 << nIns) + nIns ), * pTemp; 
-    int i, iStart = 0, nSize = 1 << nIns;
-    p->pName = Abc_UtilStrsav( "mux" );
-    for ( i = 0; i < nIns; i++ )
-        Vec_IntPush( vIns, Gia_ManAppendCi(p) );
-    for ( i = 0; i < nSize; i++ )
-        Vec_IntPush( vData, Gia_ManAppendCi(p) );
-    Gia_ManHashAlloc( p );
-    for ( i = (int)strlen(pNums)-1; i >= 0; i-- )
-    {
-        int k, b, nBits = (int)(pNums[i] - '0');
-        Vec_Int_t * vDec = Gia_GenDecoder( p, Vec_IntEntryP(vIns, iStart), nBits );
-        for ( k = 0; k < nSize; k++ )
-            Vec_IntWriteEntry( vData, k, Gia_ManHashAnd(p, Vec_IntEntry(vData, k), Vec_IntEntry(vDec, k%Vec_IntSize(vDec))) );
-        for ( b = 0; b < nBits; b++, nSize /= 2 )
-            for ( k = 0; k < nSize/2; k++ )
-                Vec_IntWriteEntry( vData, k, Gia_ManHashOr(p, Vec_IntEntry(vData, 2*k), Vec_IntEntry(vData, 2*k+1)) );
-        Vec_IntFree( vDec );
-        iStart += nBits;
-    }
-    assert( nSize == 1 );
-    Gia_ManAppendCo( p, Vec_IntEntry(vData, 0) );
-    Vec_IntFree( vIns );
-    Vec_IntFree( vData );    
-    p = Gia_ManCleanup( pTemp = p );
-    Gia_ManStop( pTemp );
-    return p;
-}
-
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if this window has a topo error (forward path from an output to an input).]

src/base/abci/abc.c

@@ -182,6 +182,7 @@ static int Abc_CommandSwapPos                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandRemovePo               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDropSat                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAddPi                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAddFlop                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAppend                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPutOnTop               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFrames                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -427,6 +428,7 @@ static int Abc_CommandAbc9Strash             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Topand             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Add1Hot            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Cof                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Cofs               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Trim               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Dfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Sim                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -613,6 +615,8 @@ static int Abc_CommandAbc9GenCex             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Odc                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GenRel             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GenMux             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9GenComp            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9GenNeuron          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Window             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9FunAbs             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9DsdInfo            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -978,6 +982,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "removepo",      Abc_CommandRemovePo,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "dropsat",       Abc_CommandDropSat,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "addpi",         Abc_CommandAddPi,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "addflop",       Abc_CommandAddFlop,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "append",        Abc_CommandAppend,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "putontop",      Abc_CommandPutOnTop,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "frames",        Abc_CommandFrames,           1 );
@@ -1221,6 +1226,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&topand",       Abc_CommandAbc9Topand,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&add1hot",      Abc_CommandAbc9Add1Hot,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&cof",          Abc_CommandAbc9Cof,          0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&cofs",         Abc_CommandAbc9Cofs,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&trim",         Abc_CommandAbc9Trim,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&dfs",          Abc_CommandAbc9Dfs,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&sim",          Abc_CommandAbc9Sim,          0 );
@@ -1413,6 +1419,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&odc",          Abc_CommandAbc9Odc,                    0 );    
     Cmd_CommandAdd( pAbc, "ABC9",         "&genrel",       Abc_CommandAbc9GenRel,                 0 );    
     Cmd_CommandAdd( pAbc, "ABC9",         "&genmux",       Abc_CommandAbc9GenMux,                 0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&gencomp",      Abc_CommandAbc9GenComp,                0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&genneuron",    Abc_CommandAbc9GenNeuron,              0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&window",       Abc_CommandAbc9Window,                 0 );    
     Cmd_CommandAdd( pAbc, "ABC9",         "&funabs",       Abc_CommandAbc9FunAbs,                 0 );    
     Cmd_CommandAdd( pAbc, "ABC9",         "&dsdinfo",      Abc_CommandAbc9DsdInfo,                0 );    
@@ -9802,7 +9810,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     Bmc_EsPar_t Pars, * pPars = &Pars;
     Bmc_EsParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "INKTiaogvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "INKTiaocgvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -9859,6 +9867,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'o':
             pPars->fFewerVars ^= 1;
             break;
+        case 'c':
+            pPars->fLutCascade ^= 1;
+            break;
         case 'g':
             pPars->fGlucose ^= 1;
             break;
@@ -9905,7 +9916,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: lutexact [-INKT <num>] [-iaogvh] <hex>\n" );
+    Abc_Print( -2, "usage: lutexact [-INKT <num>] [-iaocgvh] <hex>\n" );
     Abc_Print( -2, "\t           exact synthesis of I-input function using N K-input gates\n" );
     Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
     Abc_Print( -2, "\t-N <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes );
@@ -9914,6 +9925,7 @@ usage:
     Abc_Print( -2, "\t-i       : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" );
     Abc_Print( -2, "\t-a       : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
     Abc_Print( -2, "\t-o       : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" );
+    Abc_Print( -2, "\t-c       : toggle synthesizing a single-rail cascade [default = %s]\n", pPars->fLutCascade ? "yes" : "no" );
     Abc_Print( -2, "\t-g       : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n" );
@@ -11166,7 +11178,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAddPi( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes;
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int c;
 
     // set defaults
@@ -11188,14 +11200,14 @@ int Abc_CommandAddPi( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkDup( pNtk );
-    if ( Abc_NtkPiNum(pNtkRes) == 0 )
+    if ( Abc_NtkPiNum(pNtk) == 0 )
     {
+        Abc_Ntk_t * pNtkRes = Abc_NtkDup( pNtk );
         Abc_Obj_t * pObj = Abc_NtkCreatePi( pNtkRes );
         Abc_ObjAssignName( pObj, "dummy_pi", NULL );
         Abc_NtkOrderCisCos( pNtkRes );
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     }
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
@@ -11205,6 +11217,59 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAddFlop( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int c;
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n");
+        return 0;
+    }
+    // get the new network
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        Abc_Ntk_t * pNtkRes = Abc_NtkDup( pNtk );
+        Abc_NtkAddLatch( pNtkRes, Abc_AigConst1(pNtkRes), ABC_INIT_ONE );
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    }
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: addflop [-h]\n" );
+    Abc_Print( -2, "\t         if the network has no flops, add one dummy flop\n" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -32742,7 +32807,7 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     Abc_NtkInsertHierarchyGia( pNtkSpec, pAbc->pNtkCur, fVerbose );
-    Io_WriteVerilog( pNtkSpec, pFileName, 0 );
+    Io_WriteVerilog( pNtkSpec, pFileName, 0, 0 );
     Abc_NtkDelete( pNtkSpec );
     return 0;
 
@@ -33904,8 +33969,9 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fAddMuxes  = 0;
     int fStrMuxes  = 0;
     int fRehashMap = 0;
+    int fInvert    = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "LMbacmrsh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "LMbacmrsih" ) ) != EOF )
     {
         switch ( c )
         {
@@ -33949,6 +34015,9 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             fStrMuxes ^= 1;
             break;
+        case 'i':
+            fInvert ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -33960,6 +34029,13 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Strash(): There is no AIG.\n" );
         return 1;
     }
+    if ( fInvert )
+    {
+        Gia_Obj_t * pObj; int i;
+        Gia_ManForEachPo( pAbc->pGia, pObj, i )
+            Gia_ObjFlipFaninC0( pObj );
+        return 0;        
+    }
     if ( fAddBuffs )
     {
         extern Gia_Man_t * Gia_ManDupAddBufs( Gia_Man_t * p );
@@ -34041,7 +34117,7 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &st [-LM num] [-bacmrsh]\n" );
+    Abc_Print( -2, "usage: &st [-LM num] [-bacmrsih]\n" );
     Abc_Print( -2, "\t         performs structural hashing\n" );
     Abc_Print( -2, "\t-b     : toggle adding buffers at the inputs and outputs [default = %s]\n", fAddBuffs? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
@@ -34052,6 +34128,7 @@ usage:
     Abc_Print( -2, "\t-M num : create an AIG with additional primary inputs [default = %d]\n", Multi );
     Abc_Print( -2, "\t-r     : toggle rehashing AIG while preserving mapping [default = %s]\n", fRehashMap? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle using MUX restructuring [default = %s]\n", fStrMuxes? "yes": "no" );
+    Abc_Print( -2, "\t-i     : toggle complementing the POs of the AIG [default = %s]\n", fInvert? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -34276,6 +34353,96 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Cofs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManDupCofs( Gia_Man_t * p, Vec_Int_t * vVarNums );
+    Gia_Man_t * pTemp;  Vec_Int_t * vVars = NULL;
+    int c, iVar = 0, nVars = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "VNvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'V':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iVar = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iVar < 0 )
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nVars = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nVars < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Cof(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( iVar ) {
+        Abc_Print( 0, "Cofactoring one variable with ID %d.\n", iVar );
+        vVars = Vec_IntAlloc( 1 );
+        Vec_IntPush( vVars, iVar );
+    }
+    else if ( nVars ) {
+        Abc_Print( 0, "Cofactoring the first %d inputs.\n", nVars );
+        vVars = Vec_IntStartNatural( nVars );
+    }
+    else if ( globalUtilOptind < argc ) {
+        vVars = Vec_IntAlloc( argc );
+        for ( c = globalUtilOptind; c < argc; c++ )
+            Vec_IntPush( vVars, atoi(argv[c]) );
+    }
+    else {
+        Abc_Print( -1, "One of the parameters, -V <num> or -L <num>, should be set on the command line.\n" );
+        goto usage;
+    }
+    pTemp = Gia_ManDupCofs( pAbc->pGia, vVars );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    Vec_IntFree( vVars );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &cofs [-VN num] [-vh]\n" );
+    Abc_Print( -2, "\t         derives cofactors w.r.t the set of variables\n" );
+    Abc_Print( -2, "\t-V num : the zero-based ID of one variable to cofactor [default = %d]\n", iVar );
+    Abc_Print( -2, "\t-N num : cofactoring the given number of first input variables [default = %d]\n", nVars );
+    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    []
@@ -38518,6 +38685,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         Vec_Int_t * vStops = Gia_ManFindStopFlops( pAbc->pGia, nFlopIncFreq, pPars->fVerbose );
         if ( vStops )
         {
+            extern void Gia_ManTransferEquivs2( Gia_Man_t * p, Gia_Man_t * pNew );
             Gia_Man_t * pUsed = Gia_ManDupStopsAdd( pAbc->pGia, vStops );
             if ( pPars->nPartSize > 0 )
                 pTemp = Gia_SignalCorrespondencePart( pUsed, pPars );
@@ -38527,6 +38695,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
                 pTemp = Gia_ManScorrDivideTest( pUsed, pPars );
             else
                 pTemp = Cec_ManLSCorrespondence( pUsed, pPars );
+            Gia_ManTransferEquivs2( pUsed, pAbc->pGia );
             Gia_ManStop( pUsed );
             pTemp = Gia_ManDupStopsRem( pUsed = pTemp, vStops );
             Gia_ManStop( pUsed );
@@ -41314,7 +41483,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-
+    
     if ( pAbc->pGia == NULL )
     {
         if ( !Abc_FrameReadFlag("silentmode") )
@@ -52862,13 +53031,16 @@ int Abc_CommandAbc9AddFlop( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9AddFlop(): There is no AIG.\n" );
         return 0;
     }
-    pTemp = Gia_ManDupAddFlop( pAbc->pGia );
-    Abc_FrameUpdateGia( pAbc, pTemp );
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 ) 
+    {
+        pTemp = Gia_ManDupAddFlop( pAbc->pGia );
+        Abc_FrameUpdateGia( pAbc, pTemp );
+    }
     return 0;
 
 usage:
     Abc_Print( -2, "usage: &addflop [-vh]\n" );
-    Abc_Print( -2, "\t         adds one flop to the design\n" );
+    Abc_Print( -2, "\t         if the design has no flops, adds one flop to the design\n" );
     Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -53449,17 +53621,18 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fVerbose, int fVeryVerbose );
+    extern void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fBlif, int fVerbose, int fVeryVerbose );
     char * pFileName = (char *)"cexes.txt";
     int nMinCexes =  1;
     int nMaxTries = 10;
     int fUseSim   =  1;
     int fUseSat   =  1;
     int fShort    =  0;
+    int fBlif     =  0;
     int fVerbose  =  0;
     int c;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CMFstcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CMFstcbvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -53503,6 +53676,9 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             fShort ^= 1;
             break;
+        case 'b':
+            fBlif ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -53517,19 +53693,20 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Bmci(): There is no AIG.\n" );
         return 0;
     }
-    Gia_GenerateCexes( pFileName, pAbc->pGia, nMaxTries, nMinCexes, fUseSim, fUseSat, fShort, fVerbose, 0 );
+    Gia_GenerateCexes( pFileName, pAbc->pGia, nMaxTries, nMinCexes, fUseSim, fUseSat, fShort, fBlif, fVerbose, 0 );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcvh]\n" );
+    Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcbvh]\n" );
     Abc_Print( -2, "\t          generates satisfying assignments for each output of the miter\n" );
     Abc_Print( -2, "\t-C num  : the number of timeframes [default = %d]\n",                  nMinCexes );
     Abc_Print( -2, "\t-M num  : the max simulation runs before using SAT [default = %d]\n",  nMaxTries );
     Abc_Print( -2, "\t-F file : the output file name [default = %s]\n",                      pFileName );
-    Abc_Print( -2, "\t-s      : toggles using reverse simulation [default = %d]\n",          fUseSim  ? "yes": "no" );
-    Abc_Print( -2, "\t-t      : toggles using SAT solving [default = %d]\n",                 fUseSat  ? "yes": "no" );
-    Abc_Print( -2, "\t-c      : toggles outputing care literals only [default = %d]\n",      fShort   ? "yes": "no" );
-    Abc_Print( -2, "\t-v      : toggles printing verbose information [default = %d]\n",      fVerbose ? "yes": "no" );
+    Abc_Print( -2, "\t-s      : toggles using reverse simulation [default = %s]\n",          fUseSim  ? "yes": "no" );
+    Abc_Print( -2, "\t-t      : toggles using SAT solving [default = %s]\n",                 fUseSat  ? "yes": "no" );
+    Abc_Print( -2, "\t-c      : toggles outputing care literals only [default = %s]\n",      fShort   ? "yes": "no" );
+    Abc_Print( -2, "\t-b      : toggles outputing the BLIF file [default = %s]\n",           fBlif    ? "yes": "no" );
+    Abc_Print( -2, "\t-v      : toggles printing verbose information [default = %s]\n",      fVerbose ? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
     return 1;
 }
@@ -53739,36 +53916,9 @@ int Abc_CommandAbc9GenMux( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( argc == globalUtilOptind && nIns > 0 ) 
     {
-        if ( nIns == 2 )
-           pNums = "11";
-        else if ( nIns == 3 )
-           pNums = "111";
-        else if ( nIns == 4 )
-           pNums = "112";
-        else if ( nIns == 5 )
-           pNums = "113";
-        else if ( nIns == 6 )
-           pNums = "123";
-        else if ( nIns == 7 )
-           pNums = "1123";
-        else if ( nIns == 8 )
-           pNums = "1124";
-        else if ( nIns == 9 )
-           pNums = "1134";
-        else if ( nIns == 10 )
-           pNums = "1135";
-        else if ( nIns == 11 )
-           pNums = "1235";
-        else if ( nIns == 12 )
-           pNums = "1245";
-        else if ( nIns == 13 )
-           pNums = "1246";
-        else if ( nIns == 14 )
-           pNums = "1247";
-        else if ( nIns == 15 )
-           pNums = "1248";
-        else if ( nIns == 16 )
-           pNums = "1348";
+        extern char * Wlc_NtkMuxTreeString( int nIns );
+        if ( nIns <= 16 )
+            pNums = Wlc_NtkMuxTreeString( nIns );
         else
         {
             Abc_Print( -1, "Abc_CommandAbc9GenMux(): The number of controls should not be in the range: 2 <= n <= 16.\n" );
@@ -53808,6 +53958,154 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9GenComp( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManDupGenComp( int nBits, int fInterleave );
+    Gia_Man_t * pTemp = NULL;
+    int c, nBits = 0, fInter = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Kivh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBits = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBits < 0 )
+                goto usage;
+            break;
+        case 'i':
+            fInter ^= 1;
+            break;            
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( nBits == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9GenComp(): The number of inputs should be defined on the command line \"-K num\".\n" );
+        return 0;            
+    }    
+    pTemp = Gia_ManDupGenComp( nBits, fInter );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    if ( fVerbose )
+        Abc_Print( 1, "Generated %d-bit comparator.\n", nBits );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &gencomp [-K <num>] [-ivh]\n" );
+    Abc_Print( -2, "\t         generates the comparator\n" );
+    Abc_Print( -2, "\t-K num : the number of control inputs [default = undefined]\n" );
+    Abc_Print( -2, "\t-i     : toggles using interleaved variable ordering [default = %s]\n", fInter ? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "\tstring : the sizes of control input groups\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9GenNeuron( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManGenNeuron( char * pFileName, int nIBits, int nLutSize, int fDump, int fVerbose );
+    Gia_Man_t * pTemp = NULL;
+    int c, nBits = 0, nLutSize = 0, fDump = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IKdvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBits = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBits < 0 )
+                goto usage;
+            break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 )
+                goto usage;
+            break;
+        case 'd':
+            fDump ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( nBits < 1 || nBits > 31 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9GenNeuron(): The number of inputs (0 < K < 32) should be defined on the command line \"-K num\".\n" );
+        return 0;            
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        Abc_Print( 1, "Input file is not given.\n" );
+        return 0;
+    }
+    pTemp = Gia_ManGenNeuron( argv[globalUtilOptind], nBits, nLutSize, fDump, fVerbose );
+    if ( fVerbose )
+        printf( "Generated %d-argument neuron with %d-bit inputs and %d-bit output.\n", Gia_ManCiNum(pTemp)/nBits, nBits, Gia_ManCoNum(pTemp) );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &genneuron [-IK <num>] [-dvh] <file>\n" );
+    Abc_Print( -2, "\t         generates the implementation of one neuron\n" );
+    Abc_Print( -2, "\t-I num : the bit-width of each input [default = undefined]\n" );
+    Abc_Print( -2, "\t-K num : the LUT size for logic structuring [default = undefined]\n" );
+    Abc_Print( -2, "\t-d     : toggles dumping RTL Verilog [default = %s]\n", fDump ? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "\t<file> : the weights one per line followed by the bias (in hex notation)\n");
+    return 1;
+}
 
 /**Function*************************************************************
 
@@ -54008,9 +54306,10 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Gia_ManPrintDsdMatrix( Gia_Man_t * p, int iIn );
     extern void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose );
-    int c, iIn = -1, fDsd = 0, fAll = 0, fVerbose = 0;
+    extern void Gia_ManRecurDsd( Gia_Man_t * p, int fVerbose );
+    int c, iIn = -1, fDsd = 0, fAll = 0, fRecur = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Vdavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Vdarvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -54030,7 +54329,10 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
             break;            
         case 'a':
             fAll ^= 1;
-            break;            
+            break;
+        case 'r':
+            fRecur ^= 1;
+            break;                        
         case 'v':
             fVerbose ^= 1;
             break;
@@ -54045,16 +54347,22 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9DsdInfo(): There is no AIG.\n" );
         return 0;
     }
+    if ( fRecur )
+    {
+        Gia_ManRecurDsd( pAbc->pGia, fVerbose );
+        return 0;
+    }
     if ( fDsd ) 
     {
         if ( iIn == -1 ) {
-            Gia_ManCheckDsd( pAbc->pGia, 0, 1 );
+            printf( "Function = " );
+            Gia_ManCheckDsd( pAbc->pGia, 0, fVerbose );
             if ( fAll ) {
                 for ( iIn = 0; iIn < Gia_ManPiNum(pAbc->pGia); iIn++ )
                     for ( c = 0; c < 2; c++ ) {
                         Gia_Man_t * pTemp = Gia_ManDupCofactorVar( pAbc->pGia, iIn, c );
-                        printf( "%s %2d = %d:\n", c ? "   " : "Var", iIn, c );
-                        Gia_ManCheckDsd( pTemp, 12, 1 );
+                        printf( "Cof(%c=%d) = ", 'a' + iIn, c );
+                        Gia_ManCheckDsd( pTemp, 12, fVerbose );
                         Gia_ManStop( pTemp );
                     }                
             }
@@ -54062,14 +54370,14 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         for ( c = 0; c < 2; c++ ) {
             Gia_Man_t * pTemp = Gia_ManDupCofactorVar( pAbc->pGia, iIn, c );
-            printf( "Var %2d  Cof %d:\n", iIn, c );
-            Gia_ManCheckDsd( pTemp, 0, 1 );
+            printf( "    Cof(%c=%d) = ", 'a' + iIn, c );
+            Gia_ManCheckDsd( pTemp, 0, fVerbose );
             if ( fAll ) {
-                for ( int iIn = 0; iIn < Gia_ManPiNum(pAbc->pGia); iIn++ )
-                    for ( int c = 0; c < 2; c++ ) {
-                        Gia_Man_t * pTemp2 = Gia_ManDupCofactorVar( pTemp, iIn, c );
-                        printf( "%s %2d = %d:\n", c ? "   " : "Var", iIn, c );
-                        Gia_ManCheckDsd( pTemp2, 12, 1 );
+                for ( int iIn2 = 0; iIn2 < Gia_ManPiNum(pAbc->pGia); iIn2++ ) if ( iIn2 != iIn )
+                    for ( int c2 = 0; c2 < 2; c2++ ) {
+                        Gia_Man_t * pTemp2 = Gia_ManDupCofactorVar( pTemp, iIn2, c2 );
+                        printf( "Cof(%c=%d,%c=%d) = ", 'a' + iIn, c, 'a' + iIn2, c2 );
+                        Gia_ManCheckDsd( pTemp2, 12, fVerbose );
                         Gia_ManStop( pTemp2 );
                     }
             }
@@ -54086,10 +54394,11 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &dsdinfo [-V num] [-dvh]\n" );
+    Abc_Print( -2, "usage: &dsdinfo [-V num] [-drvh]\n" );
     Abc_Print( -2, "\t          computes and displays information related to DSD\n" );
     Abc_Print( -2, "\t-V num  : the zero-based index of the input variable [default = %d]\n", iIn );
     Abc_Print( -2, "\t-d      : toggles showing DSD structure [default = %s]\n", fDsd ? "yes": "no" );
+    Abc_Print( -2, "\t-r      : toggles recursive cofactoring to get a full DSD [default = %s]\n", fRecur ? "yes": "no" );
     Abc_Print( -2, "\t-v      : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
     return 1;
@@ -54111,10 +54420,12 @@ int Abc_CommandAbc9FunTrace( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Vec_Mem_t * Dau_CollectNpnFunctions( word * p, int nVars, int fVerbose );
     extern void Gia_ManMatchCuts( Vec_Mem_t * vTtMem, Gia_Man_t * pGia, int nCutSize, int nCutNum, int fVerbose );
-    int c, nVars, nVars2, nCutNum = 8, fVerbose = 0; word * pTruth = NULL;
-    char * pStr = NULL; Vec_Mem_t * vTtMem = NULL;
+    extern Vec_Mem_t * Abc_TruthDecRead( char * pFileName, int nVarNum );
+    extern void Abc_TtStoreDump( char * pFileName, Vec_Mem_t * vTtMem, int nBytes );
+    int c, nVars, nVars2, nCutNum = 8, nCutSize = 0, nNumFuncs = 5, nNumCones = 3, fOutputs = 0, fVerbose = 0; word * pTruth = NULL;
+    char * pStr = NULL, * pFuncFileName = "_npn_member_funcs_.data"; Vec_Mem_t * vTtMem = NULL; Gia_Man_t * pTemp;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CKNMFovh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -54129,6 +54440,51 @@ int Abc_CommandAbc9FunTrace( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nCutNum < 0 )
                 goto usage;
             break;            
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCutSize < 0 )
+                goto usage;
+            break;            
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nNumFuncs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNumFuncs < 0 )
+                goto usage;
+            break;            
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nNumCones = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNumCones < 0 )
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pFuncFileName = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;            
+        case 'o':
+            fOutputs ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -54143,9 +54499,53 @@ int Abc_CommandAbc9FunTrace( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9FunTrace(): There is no AIG.\n" );
         return 0;
     }
-    if ( argc != globalUtilOptind + 1 )
+    if ( argc == globalUtilOptind )
     {
-        Abc_Print( -1, "Abc_CommandAbc9FunTrace(): Truth table in hex notation should be given on the command line.\n" );
+        abctime clkStart = Abc_Clock();
+        int nFileSize = Gia_FileSize( pFuncFileName );
+        if ( nFileSize == 0 )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9FunTrace(): Truth table in hex notation (or file name with the functions) should be given on the command line.\n" );
+            return 0;
+        }
+        if ( nCutSize == 0 )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9FunTrace(): The cut size needs to be specified on the command line (-K <num>) when precomputed functions are used.\n" );
+            return 0;            
+        }
+        vTtMem = Abc_TruthDecRead( pFuncFileName, nCutSize );
+        printf( "Finished reading %d %d-input function from file \"%s\".  ", nFileSize / 8 / Abc_Truth6WordNum(nCutSize), nCutSize, pFuncFileName );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
+        Gia_ManMatchCuts( vTtMem, pAbc->pGia, nCutSize, nCutNum, fVerbose );
+        Vec_MemHashFree( vTtMem );
+        Vec_MemFree( vTtMem );
+        return 0;        
+    }
+    if ( strstr(argv[globalUtilOptind], ".aig") ) 
+    { // the entry on the command line is an AIGER file
+        extern void Gia_ManMatchCones( Gia_Man_t * pBig, Gia_Man_t * pSmall, int nCutSize, int nCutNum, int nNumFuncs, int nNumCones, int fVerbose );
+        extern void Gia_ManMatchConesOutput( Gia_Man_t * pBig, Gia_Man_t * pSmall, int nCutNum, int fVerbose );
+        pTemp = Gia_AigerRead( argv[globalUtilOptind], 0, 0, 0 );
+        if ( pTemp == NULL ) {
+            Abc_Print( -1, "Abc_CommandAbc9FunTrace(): Cannot read input AIG \"%s\".\n", argv[globalUtilOptind] );
+            return 0;                
+        }
+        if ( fOutputs ) {
+            if ( Gia_ManCiNum(pTemp) > 16 ) {
+                Abc_Print( -1, "Abc_CommandAbc9FunTrace(): The AIG \"%s\" has more than 16 primary inputs.\n", argv[globalUtilOptind] );
+                Gia_ManStop( pTemp );
+                return 0;                   
+            }
+            Gia_ManMatchConesOutput( pAbc->pGia, pTemp, nCutNum, fVerbose );
+        }
+        else  {
+            if ( nCutSize == 0 ) {
+                Abc_Print( -1, "Abc_CommandAbc9FunTrace(): The LUT size for profiling should be given on the command line.\n" );
+                return 0;            
+            }
+            Gia_ManMatchCones( pAbc->pGia, pTemp, nCutSize, nCutNum, nNumFuncs, nNumCones, fVerbose );
+        }
+        Gia_ManStop( pTemp );
         return 0;
     }
     pStr = argv[globalUtilOptind];
@@ -54168,17 +54568,27 @@ int Abc_CommandAbc9FunTrace( Abc_Frame_t * pAbc, int argc, char ** argv )
     //Abc_TtPrintHexRev( stdout, pTruth, nVars ); printf( "\n" );
     vTtMem = Dau_CollectNpnFunctions( pTruth, nVars, fVerbose );
     Gia_ManMatchCuts( vTtMem, pAbc->pGia, nVars, nCutNum, fVerbose );
+    if ( pFuncFileName ) {
+        Abc_TtStoreDump( pFuncFileName, vTtMem, 8 * Vec_MemEntrySize(vTtMem) );
+        printf( "Dumped %d NPN class member functions into file \"%s\".\n", Vec_MemEntryNum(vTtMem), pFuncFileName );
+    }
     Vec_MemHashFree( vTtMem );
     Vec_MemFree( vTtMem );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &funtrace [-C num] [-vh] <truth>\n" );
+    Abc_Print( -2, "usage: &funtrace [-CKNM num] [-F file] [-ovh] {<truth> or <file.aig>}\n" );
     Abc_Print( -2, "\t          traces the presence of the function in the current AIG\n" );
     Abc_Print( -2, "\t-C num  : the number of cuts to compute at each node [default = %d]\n", nCutNum );
+    Abc_Print( -2, "\t-K num  : the LUT size to use when <file.aig> is given [default = %d]\n", nCutSize );
+    Abc_Print( -2, "\t-N num  : the number of functions to use when <file.aig> or -F <file> are used [default = %d]\n", nNumFuncs );
+    Abc_Print( -2, "\t-M num  : the number of logic cones to use when <file.aig> is given [default = %d]\n", nNumCones );
+    Abc_Print( -2, "\t-F file : the file name to store the NPN member functions [default = %s]\n", pFuncFileName );
+    Abc_Print( -2, "\t-o      : toggles using AIG output functions instead of frequent cut functions [default = %s]\n", fOutputs ? "yes": "no" );
     Abc_Print( -2, "\t-v      : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
-    Abc_Print( -2, "\t<truth> : truth table in the hexadecimal notation\n");
+    Abc_Print( -2, "\t<truth> : truth table in the hexadecimal notation used for tracing\n");
+    Abc_Print( -2, "\t<file>  : AIG whose K-input functions will be used for tracing\n");
     return 1;
 }
 

src/base/abci/abcDec.c

@@ -458,6 +458,31 @@ void Abc_TtStoreLoadSave( char * pFileName )
     printf( "Input file \"%s\" was copied into output file \"%s\".\n", pFileInput, pFileOutput );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Read truth tables from input file and write them into output file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_TtStoreDump( char * pFileName, Vec_Mem_t * vTtMem, int nBytes )
+{ 
+    word * pTruth;  int i;
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return;
+    }
+    Vec_MemForEachEntry( vTtMem, pTruth, i )
+        fwrite( pTruth, nBytes, 1, pFile );  
+    fclose( pFile );  
+}
+
 /**Function*************************************************************
 
   Synopsis    [Read truth tables in binary text form and write them into file as binary data.]
@@ -709,6 +734,38 @@ void Abc_TruthDecTest( char * pFileName, int DecType, int nVarNum, int fVerbose
 //    printf( "Finished decomposing truth tables from file \"%s\".\n", pFileName );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Read truth tables from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Mem_t * Abc_TruthDecRead( char * pFileName, int nVarNum )
+{
+    Abc_TtStore_t * p; int i;
+    if ( nVarNum < 6 )
+        nVarNum = 6;
+
+    // allocate data-structure
+    p = Abc_TtStoreLoad( pFileName, nVarNum );
+    if ( p == NULL ) return NULL;
+
+    // consider functions from the file
+    Vec_Mem_t * vTtMem = Vec_MemAllocForTTSimple( nVarNum );
+    for ( i = 0; i < p->nFuncs; i++ )
+        Vec_MemHashInsert( vTtMem, (word *)p->pFuncs[i] );
+
+    // delete data-structure
+    Abc_TtStoreFree( p, nVarNum );
+//    printf( "Finished decomposing truth tables from file \"%s\".\n", pFileName );
+    return vTtMem;
+}
+
 
 /**Function*************************************************************
 

src/base/abci/abcFx.c

@@ -287,8 +287,11 @@ int Abc_NtkFxCheck( Abc_Ntk_t * pNtk )
 //    Abc_NtkForEachObj( pNtk, pNode, i )
 //        Abc_ObjPrint( stdout, pNode );
     Abc_NtkForEachNode( pNtk, pNode, i )
-        if ( !Vec_IntCheckUniqueSmall( &pNode->vFanins ) )
+        if ( !Vec_IntCheckUniqueSmall( &pNode->vFanins ) ) {
+            printf( "Fanins of node %d: ", i );
+            Vec_IntPrint( &pNode->vFanins );
             return 0;
+        }
     return 1;
 }
 

src/base/abci/abcResub.c

@@ -170,6 +170,8 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nMinS
     pManRes->nNodesBeg = Abc_NtkNodeNum(pNtk);
     nNodes = Abc_NtkObjNumMax(pNtk);
     pProgress = Extra_ProgressBarStart( stdout, nNodes );
+    //clear markAB at the beginning
+    Abc_NtkCleanMarkAB( pNtk );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );

src/base/io/io.c

@@ -59,6 +59,7 @@ static int IoCommandReadStatus  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadGig     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadJson    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadSF      ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadRom     ( Abc_Frame_t * pAbc, int argc, char **argv );
 
 static int IoCommandWrite       ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteHie    ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -133,6 +134,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "&read_gig",     IoCommandReadGig,      0 );
     Cmd_CommandAdd( pAbc, "I/O", "read_json",     IoCommandReadJson,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "read_sf",       IoCommandReadSF,       0 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_rom",      IoCommandReadRom,      1 );
 
     Cmd_CommandAdd( pAbc, "I/O", "write",         IoCommandWrite,        0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_hie",     IoCommandWriteHie,     0 );
@@ -1927,6 +1929,73 @@ usage:
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandReadRom( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Io_TransformROM2PLA( char * pNameIn, char * pNameOut );
+
+    Abc_Ntk_t * pNtk;
+    FILE * pFile;
+    char * pFileName, * pFileTemp = "_temp_rom_.pla";
+    int c;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
+        return 1;
+    }
+    fclose( pFile );
+    Io_TransformROM2PLA( pFileName, pFileTemp );
+    pNtk = Io_Read( pFileTemp, IO_FILE_PLA, 1, 0 );
+    //unlink( pFileTemp );
+    if ( pNtk == NULL )
+        return 1;
+    ABC_FREE( pNtk->pName );
+    pNtk->pName = Extra_FileNameGeneric( pFileName );
+    ABC_FREE( pNtk->pSpec );
+    pNtk->pSpec = Abc_UtilStrsav( pFileName );
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    Abc_FrameClearVerifStatus( pAbc );
+
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_rom [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         reads ROM file\n" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -3530,13 +3599,13 @@ usage:
 ***********************************************************************/
 int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
 {
-    extern void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules );
+    extern void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules, int fNewInterface );
     char * pFileName;
-    int c, fFixed = 0, fOnlyAnds = 0, fNoModules = 0;
+    int c, fFixed = 0, fOnlyAnds = 0, fNoModules = 0, fNewInterface = 0;
     int nLutSize = -1;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Kfamh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Kfamnh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3560,6 +3629,9 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
             case 'm':
                 fNoModules ^= 1;
                 break;
+            case 'n':
+                fNewInterface ^= 1;
+                break;                
             case 'h':
                 goto usage;
             default:
@@ -3578,27 +3650,26 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the corresponding file writer
-    if ( fOnlyAnds )
+    if ( nLutSize >= 2 && nLutSize <= 6 )
+        Io_WriteVerilogLut( pAbc->pNtkCur, pFileName, nLutSize, fFixed, fNoModules, fNewInterface );
+    else
     {
         Abc_Ntk_t * pNtkTemp = Abc_NtkToNetlist( pAbc->pNtkCur );
         if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
             Abc_NtkToAig( pNtkTemp );
-        Io_WriteVerilog( pNtkTemp, pFileName, 1 );
+        Io_WriteVerilog( pNtkTemp, pFileName, fOnlyAnds, fNewInterface );
         Abc_NtkDelete( pNtkTemp );
     }
-    else if ( nLutSize >= 2 && nLutSize <= 6 )
-        Io_WriteVerilogLut( pAbc->pNtkCur, pFileName, nLutSize, fFixed, fNoModules );
-    else
-        Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_VERILOG );
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_verilog [-K num] [-famh] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_verilog [-K num] [-famnh] <file>\n" );
     fprintf( pAbc->Err, "\t         writes the current network in Verilog format\n" );
     fprintf( pAbc->Err, "\t-K num : write the network using instances of K-LUTs (2 <= K <= 6) [default = not used]\n" );
     fprintf( pAbc->Err, "\t-f     : toggle using fixed format [default = %s]\n", fFixed? "yes":"no" );
     fprintf( pAbc->Err, "\t-a     : toggle writing expressions with only ANDs (without XORs and MUXes) [default = %s]\n", fOnlyAnds? "yes":"no" );
     fprintf( pAbc->Err, "\t-m     : toggle writing additional modules [default = %s]\n", !fNoModules? "yes":"no" );
+    fprintf( pAbc->Err, "\t-n     : toggle writing generic PO names and assign-statements [default = %s]\n", fNewInterface? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
     return 1;

src/base/io/ioAbc.h

@@ -137,7 +137,7 @@ extern int                Io_WriteMoPla( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteSmv.c ===========================================================*/
 extern int                Io_WriteSmv( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteVerilog.c =======================================================*/
-extern void               Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName, int fOnlyAnds );
+extern void               Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName, int fOnlyAnds, int fNewInterface );
 /*=== abcUtil.c ===============================================================*/
 extern Io_FileType_t      Io_ReadFileType( char * pFileName );
 extern Io_FileType_t      Io_ReadLibType( char * pFileName );

src/base/io/ioUtil.c

@@ -20,6 +20,7 @@
 
 #include "ioAbc.h"
 #include "base/main/main.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -464,7 +465,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
     {
         if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
             Abc_NtkToAig( pNtkTemp );
-        Io_WriteVerilog( pNtkTemp, pFileName, 0 );
+        Io_WriteVerilog( pNtkTemp, pFileName, 0, 0 );
     }
     else 
         fprintf( stderr, "Unknown file format.\n" );
@@ -592,7 +593,7 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
             if ( !Abc_NtkHasAig(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) )
                 Abc_NtkToAig( pNtkResult );
         }
-        Io_WriteVerilog( pNtkResult, pFileName, 0 );
+        Io_WriteVerilog( pNtkResult, pFileName, 0, 0 );
     }
     else if ( Io_ReadFileType(pFileName) == IO_FILE_BLIFMV )
     {
@@ -890,7 +891,7 @@ void Io_TransformSF2PLA( char * pNameIn, char * pNameOut )
     if ( pFileOut == NULL )
     {
         if ( pFileIn )  fclose( pFileIn );
-        printf( "Cannot open file \"%s\" for reading.\n", pNameOut );
+        printf( "Cannot open file \"%s\" for writing.\n", pNameOut );
         return;
     }
     pBuffer = ABC_ALLOC( char, Size );
@@ -920,6 +921,58 @@ void Io_TransformSF2PLA( char * pNameIn, char * pNameOut )
     ABC_FREE( pBuffer );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Tranform SF into PLA.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_TransformROM2PLA( char * pNameIn, char * pNameOut )
+{
+    FILE * pFileOut = fopen( pNameOut, "wb" );
+    if ( pFileOut == NULL ) {
+        printf( "Cannot open file \"%s\" for writing.\n", pNameOut );
+        return;
+    }
+    int nWords = -1;
+    Vec_Wrd_t * vData = Vec_WrdReadHex( pNameIn, &nWords, 0 );
+    if ( vData == NULL ) {
+        fclose( pFileOut );
+        return;
+    }
+    //Vec_WrdDumpHex( "temp.txt", vData, 1, 1 );
+    int v, i, nLines = Vec_WrdSize(vData) / nWords;
+    int nIns = Abc_Base2Log(nLines), nOuts;
+    assert( nLines * nWords == Vec_WrdSize(vData) );
+    word * pTemp = ABC_CALLOC( word, nWords );
+    for ( i = 0; i < nLines; i++ )
+        Abc_TtOr( pTemp, pTemp, Vec_WrdEntryP(vData, nWords*i), nWords );
+    for ( nOuts = nWords*64; nOuts > 0; nOuts-- )
+        if ( Abc_TtGetBit(pTemp, nOuts-1) )
+            break;
+    ABC_FREE( pTemp );
+    assert( nOuts > 0 );
+    fprintf( pFileOut, ".i %d\n", nIns );
+    fprintf( pFileOut, ".o %d\n", nOuts );
+    fprintf( pFileOut, ".p %d\n", nLines );
+    fprintf( pFileOut, ".type fr\n" );
+    for ( i = 0; i < nLines; i++ ) {
+        word * pData = Vec_WrdEntryP(vData, nWords*i);
+        for ( v = 0; v < nIns; v++ )
+            fprintf( pFileOut, "%d", (i >> v) & 1 );
+        fprintf( pFileOut, " " );
+        for ( v = 0; v < nOuts; v++ )
+            fprintf( pFileOut, "%d", Abc_TtGetBit(pData, v) );
+        fprintf( pFileOut, "\n" );
+    }
+    fprintf( pFileOut, ".e\n\n" );
+    fclose( pFileOut );
+}
 /**Function*************************************************************
 
   Synopsis    [Reads CNF from file.]

src/base/io/ioWriteVerilog.c

@@ -29,9 +29,10 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds );
+static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds, int fNewInterface );
 static void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
-static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start, int fNewInterface );
+static void Io_WriteVerilogAssigns( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
@@ -54,11 +55,12 @@ static char * Io_WriteVerilogGetName( char * pName );
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fOnlyAnds )
+void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fOnlyAnds, int fNewInterface )
 {
     Abc_Ntk_t * pNetlist;
     FILE * pFile;
     int i;
+    
     // can only write nodes represented using local AIGs
     if ( !Abc_NtkIsAigNetlist(pNtk) && !Abc_NtkIsMappedNetlist(pNtk) )
     {
@@ -81,7 +83,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fOnlyAnds )
     if ( pNtk->pDesign )
     {
         // write the network first
-        Io_WriteVerilogInt( pFile, pNtk, fOnlyAnds );
+        Io_WriteVerilogInt( pFile, pNtk, fOnlyAnds, fNewInterface );
         // write other things
         Vec_PtrForEachEntry( Abc_Ntk_t *, pNtk->pDesign->vModules, pNetlist, i )
         {
@@ -89,12 +91,12 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fOnlyAnds )
             if ( pNetlist == pNtk )
                 continue;
             fprintf( pFile, "\n" );
-            Io_WriteVerilogInt( pFile, pNetlist, fOnlyAnds );
+            Io_WriteVerilogInt( pFile, pNetlist, fOnlyAnds, fNewInterface );
         }
     }
     else
     {
-        Io_WriteVerilogInt( pFile, pNtk, fOnlyAnds );
+        Io_WriteVerilogInt( pFile, pNtk, fOnlyAnds, fNewInterface );
     }
 
     fprintf( pFile, "\n" );
@@ -112,7 +114,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fOnlyAnds )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
+void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds, int fNewInterface )
 {
     // write inputs and outputs
 //    fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
@@ -128,7 +130,7 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
         fprintf( pFile, ",\n   " );
     }
     if ( Abc_NtkPoNum(pNtk) > 0  )
-        Io_WriteVerilogPos( pFile, pNtk, 3 );
+        Io_WriteVerilogPos( pFile, pNtk, 3, fNewInterface );
     fprintf( pFile, "  );\n" );
     // add the clock signal if it does not exist
     if ( Abc_NtkLatchNum(pNtk) > 0 && Nm_ManFindIdByName(pNtk->pManName, "clock", ABC_OBJ_PI) == -1 )
@@ -144,7 +146,7 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
     if ( Abc_NtkPoNum(pNtk) > 0  )
     {
         fprintf( pFile, "  output" );
-        Io_WriteVerilogPos( pFile, pNtk, 5 );
+        Io_WriteVerilogPos( pFile, pNtk, 5, fNewInterface );
         fprintf( pFile, ";\n" );
     }
     // if this is not a blackbox, write internal signals
@@ -168,6 +170,8 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
         if ( Abc_NtkLatchNum(pNtk) > 0 )
             Io_WriteVerilogLatches( pFile, pNtk );
     }
+    if ( fNewInterface )
+        Io_WriteVerilogAssigns( pFile, pNtk );
     // finalize the file
     fprintf( pFile, "endmodule\n\n" );
 } 
@@ -222,9 +226,10 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start, int fNewInterface )
 {
     Abc_Obj_t * pTerm, * pNet, * pSkip;
+    char Name[100], * pName = Name;
     int LineLength;
     int AddedLength;
     int NameCounter;
@@ -252,7 +257,11 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
         }
         
         // get the line length after this name is written
-        AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
+        if ( fNewInterface )
+            sprintf( Name, "po_username%d", i );
+        else
+            pName = Abc_ObjName(pNet);
+        AddedLength = strlen(Io_WriteVerilogGetName(pName)) + 2;
         if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
         { // write the line extender
             fprintf( pFile, "\n   " );
@@ -260,7 +269,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             LineLength  = 3;
             NameCounter = 0;
         }
-        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(Abc_ObjName(pNet)), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," );
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pName), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -274,6 +283,37 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogAssigns( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pTerm, * pNet, * pSkip;
+    int i;
+    Abc_NtkForEachPo( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanin0(pTerm);
+        if ( Abc_ObjIsPi(Abc_ObjFanin0(pNet)) )
+        {
+            // Skip this output since it is a feedthrough -- the same
+            // name will appear as an input and an output which other
+            // tools reading verilog do not like.
+            
+            pSkip = pNet;   // save an example of skipped net
+            continue;
+        }
+        fprintf( pFile, "  assign po_username%d = %s;\n", i, Abc_ObjName(pNet) );
+    }
+}
+
 /**Function*************************************************************
 
   Synopsis    [Writes the wires.]
@@ -816,7 +856,7 @@ void Io_WriteVerilogObjectsLut( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, in
         fprintf( pFile, "}, %*s );\n", Length, Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
     }
 }
-void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fFixed )
+void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fFixed, int fNewInterface )
 {
     // write inputs and outputs
 //    fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
@@ -832,7 +872,7 @@ void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fF
         fprintf( pFile, ",\n   " );
     }
     if ( Abc_NtkPoNum(pNtk) > 0  )
-        Io_WriteVerilogPos( pFile, pNtk, 3 );
+        Io_WriteVerilogPos( pFile, pNtk, 3, fNewInterface );
     fprintf( pFile, "  );\n\n" );
     // add the clock signal if it does not exist
     if ( Abc_NtkLatchNum(pNtk) > 0 && Nm_ManFindIdByName(pNtk->pManName, "clock", ABC_OBJ_PI) == -1 )
@@ -848,7 +888,7 @@ void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fF
     if ( Abc_NtkPoNum(pNtk) > 0  )
     {
         fprintf( pFile, "  output" );
-        Io_WriteVerilogPos( pFile, pNtk, 5 );
+        Io_WriteVerilogPos( pFile, pNtk, 5, fNewInterface );
         fprintf( pFile, ";\n\n" );
     }
     // if this is not a blackbox, write internal signals
@@ -875,10 +915,12 @@ void Io_WriteVerilogLutInt( FILE * pFile, Abc_Ntk_t * pNtk, int nLutSize, int fF
             Io_WriteVerilogLatches( pFile, pNtk );
         }
     }
+    if ( fNewInterface )
+        Io_WriteVerilogAssigns( pFile, pNtk );
     // finalize the file
     fprintf( pFile, "\nendmodule\n\n" );
 } 
-void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules )
+void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules, int fNewInterface )
 {
     FILE * pFile;
     Abc_Ntk_t * pNtkTemp;
@@ -917,7 +959,7 @@ void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int f
     }
     pNtkTemp = Abc_NtkToNetlist( pNtk );
     Abc_NtkToSop( pNtkTemp, -1, ABC_INFINITY );
-    Io_WriteVerilogLutInt( pFile, pNtkTemp, nLutSize, fFixed );
+    Io_WriteVerilogLutInt( pFile, pNtkTemp, nLutSize, fFixed, fNewInterface );
     Abc_NtkDelete( pNtkTemp );
 
     fprintf( pFile, "\n" );

src/base/wlc/wlc.h

@@ -223,6 +223,7 @@ struct Wlc_BstPar_t_
     int                    fCreateWordMiter;
     int                    fDecMuxes;
     int                    fSaveFfNames;
+    int                    fBlastNew;
     int                    fVerbose;
     Vec_Int_t *            vBoxIds;
 };

src/base/wlc/wlcBlast.c

@@ -20,6 +20,8 @@
 
 #include "wlc.h"
 #include "misc/tim/tim.h"
+#include "base/main/main.h"
+#include "base/cmd/cmd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -131,6 +133,61 @@ int Wlc_NtkMuxTree2( Gia_Man_t * pNew, int * pCtrl, int nCtrl, Vec_Int_t * vData
         Vec_IntPush( vTemp, Abc_LitNot( Gia_ManHashAnd(pNew, iLit, Vec_IntEntry(vData, m)) ) );
     return Abc_LitNot( Gia_ManHashAndMulti(pNew, vTemp) );
 }
+int Wlc_NtkMuxTree3( Gia_Man_t * p, Vec_Int_t * vData, char * pNums, Vec_Int_t ** pvDecs )
+{
+    int i, iStart = 0, nSize = Vec_IntSize(vData);
+    for ( i = (int)strlen(pNums)-1; i >= 0; i-- )
+    {
+        int k, b, nBits = (int)(pNums[i] - '0');
+        Vec_Int_t * vDec = pvDecs[i];
+        for ( k = 0; k < nSize; k++ )
+            Vec_IntWriteEntry( vData, k, Gia_ManHashAnd(p, Vec_IntEntry(vData, k), Vec_IntEntry(vDec, k%Vec_IntSize(vDec))) );
+        for ( b = 0; b < nBits; b++, nSize /= 2 )
+            for ( k = 0; k < nSize/2; k++ )
+                Vec_IntWriteEntry( vData, k, Gia_ManHashOr(p, Vec_IntEntry(vData, 2*k), Vec_IntEntry(vData, 2*k+1)) );
+        iStart += nBits;
+    }
+    assert( nSize == 1 );
+    return Vec_IntEntry(vData, 0);
+}
+Vec_Int_t ** Wlc_NtkMuxTree3DecsDerive( Gia_Man_t * p, int * pIns, int nIns, char * pNums )
+{
+    extern Vec_Int_t * Wlc_BlastDecoder2_rec( Gia_Man_t * p, int * pLits, int nLits );
+    Vec_Int_t ** pvDecs = ABC_ALLOC( Vec_Int_t *, strlen(pNums) ); int i, iStart = 0;
+    for ( i = (int)strlen(pNums)-1; i >= 0; i-- ) {
+        pvDecs[i] = Wlc_BlastDecoder2_rec( p, pIns + iStart, (int)(pNums[i] - '0') );
+        iStart += (int)(pNums[i] - '0');
+    }
+    assert( iStart == nIns );
+    return pvDecs;
+}
+void Wlc_NtkMuxTree3DecsFree( Vec_Int_t ** pvDecs, char * pNums )
+{
+    int i;
+    for ( i = (int)strlen(pNums)-1; i >= 0; i-- )
+        Vec_IntFree( pvDecs[i] );
+    ABC_FREE( pvDecs );
+}
+char * Wlc_NtkMuxTreeString( int nIns )
+{
+    if ( nIns == 1 )    return (char*)"1";    
+    if ( nIns == 2 )    return (char*)"11";
+    if ( nIns == 3 )    return (char*)"111";
+    if ( nIns == 4 )    return (char*)"112";
+    if ( nIns == 5 )    return (char*)"1112";
+    if ( nIns == 6 )    return (char*)"1113";
+    if ( nIns == 7 )    return (char*)"1114";
+    if ( nIns == 8 )    return (char*)"1124";
+    if ( nIns == 9 )    return (char*)"11124";
+    if ( nIns == 10 )   return (char*)"11125";
+    if ( nIns == 11 )   return (char*)"11126";
+    if ( nIns == 12 )   return (char*)"11136";
+    if ( nIns == 13 )   return (char*)"11137";
+    if ( nIns == 14 )   return (char*)"11147";
+    if ( nIns == 15 )   return (char*)"11148";
+    if ( nIns == 16 )   return (char*)"11248";
+    return NULL;
+}
 void Wlc_NtkPrintNameArray( Vec_Ptr_t * vNames )
 {
     int i; char * pTemp;
@@ -317,6 +374,30 @@ int Wlc_BlastLessSigned( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits )
     int iDiffSign = Gia_ManHashXor( pNew, pArg0[nBits-1], pArg1[nBits-1] );
     return Gia_ManHashMux( pNew, iDiffSign, pArg0[nBits-1], Wlc_BlastLess(pNew, pArg0, pArg1, nBits-1) );
 }
+int Wlc_BlastLess3( Gia_Man_t * p, int * pArg1, int * pArg0, int nBits )
+{
+    int i, iLit = 1;
+    for ( i = 0; i < nBits; i++ ) {
+        int iLitA0  = pArg0[i];
+        int iLitA1  = i == nBits-1 ? 0 : pArg0[i+1];
+        int iLitB0  = pArg1[i];
+        int iLitB1  = i == nBits-1 ? 0 : pArg1[i+1];
+        int iOrLit0;
+        if ( i == 0 )
+            iOrLit0 = Gia_ManHashOr(p, Abc_LitNotCond(iLitA0, !(i&1)), Abc_LitNotCond(iLitB0, i&1));
+        else
+            iOrLit0 = Gia_ManHashAnd(p, Abc_LitNotCond(iLitA0, !(i&1)), Abc_LitNotCond(iLitB0, i&1));
+        int iOrLit1 = Gia_ManHashAnd(p, Abc_LitNotCond(iLitA1, !(i&1)), Abc_LitNotCond(iLitB1, i&1));
+        int iOrLit  = Gia_ManHashOr(p, iOrLit0, iOrLit1 );
+        iLit = Gia_ManHashOr(p, Abc_LitNot(iLit), iOrLit );
+    }
+    return Abc_LitNotCond(iLit, nBits&1);
+}
+int Wlc_BlastLessSigned3( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits )
+{
+    int iDiffSign = Gia_ManHashXor( pNew, pArg0[nBits-1], pArg1[nBits-1] );
+    return Gia_ManHashMux( pNew, iDiffSign, pArg0[nBits-1], Wlc_BlastLess3(pNew, pArg0, pArg1, nBits-1) );
+}
 void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps )
 {
     int fUseXor = 0;
@@ -1127,6 +1208,37 @@ void Wlc_BlastDecoder( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp,
         Vec_IntPush( vRes, iMint );
     }
 }
+Vec_Int_t * Wlc_BlastDecoder2_rec( Gia_Man_t * p, int * pLits, int nLits )
+{
+    if ( nLits == 1 )
+    {
+        Vec_Int_t * vRes = Vec_IntAlloc( 2 );
+        Vec_IntPush( vRes, Abc_LitNot(pLits[0]) );
+        Vec_IntPush( vRes, pLits[0] );
+        return vRes;
+    }
+    assert( nLits > 1 );
+    int nPart1 = nLits / 2;
+    int nPart2 = nLits - nPart1;
+    Vec_Int_t * vRes1 = Wlc_BlastDecoder2_rec( p, pLits, nPart1 );
+    Vec_Int_t * vRes2 = Wlc_BlastDecoder2_rec( p, pLits+nPart1, nPart2 );
+    Vec_Int_t * vRes = Vec_IntAlloc( Vec_IntSize(vRes1) * Vec_IntSize(vRes2) );
+    int i, k, Lit1, Lit2;
+    Vec_IntForEachEntry( vRes2, Lit2, k )
+    Vec_IntForEachEntry( vRes1, Lit1, i )
+        Vec_IntPush( vRes, Gia_ManHashAnd(p, Lit1, Lit2) );
+    Vec_IntFree( vRes1 );
+    Vec_IntFree( vRes2 );
+    return vRes;   
+}
+Vec_Int_t * Wlc_BlastDecoder2( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp, Vec_Int_t * vRes )
+{
+    Vec_Int_t * vRes2 = Wlc_BlastDecoder2_rec( pNew, pNum, nNum );
+    Vec_IntClear( vRes );
+    Vec_IntAppend( vRes, vRes2 );
+    Vec_IntFree( vRes2 );
+    return vRes;
+}
 void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose )
 {
     Vec_Wec_t * vProds  = Vec_WecStart( nArgA + nArgB + 3 );
@@ -1162,6 +1274,7 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
             int Prev = i ? pArgA[i-1] : 0;
             int Part = Gia_ManHashOr( pNew, Gia_ManHashAnd(pNew, One, This), Gia_ManHashAnd(pNew, Two, Prev) );
             pp = Gia_ManHashXor( pNew, Part, Neg );
+            if ( fVerbose ) printf( "%4d = PP(%5d %5d  %5d %5d %5d)\n", pp, Prev, This, Q2jM1, Q2j, Q2jP1 );
             if ( pp == 0 || (fSigned && i == nArgA) )
                 continue;
             if ( pp )
@@ -1208,6 +1321,8 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
     //Vec_WecShrink( vLevels, nArgA + nArgB );   
     if ( fVerbose )
         Vec_WecPrint( vProds, 0 );
+    if ( fVerbose ) 
+        printf( "Total PPs = %d.\n", Vec_WecSizeSize(vProds) );
     //Wlc_BlastPrintMatrix( pNew, vProds, 1 );
     //printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) );
     if ( pvProds )
@@ -1548,34 +1663,60 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
             Wlc_ObjForEachFanin( pObj, iFanin, k )
                 if ( k > 0 )
                     fSigned &= Wlc_NtkObj(p, iFanin)->Signed;
-            Vec_IntClear( vTemp1 );
-            if ( pPar->fDecMuxes )
+            if ( pParIn->fBlastNew && nRange0 <= 16 )
             {
-                for ( k = 0; k < (1 << nRange0); k++ )
+                char * pNums = Wlc_NtkMuxTreeString( nRange0 );
+                Vec_Int_t ** pvDecs = Wlc_NtkMuxTree3DecsDerive( pNew, pFans0, nRange0, pNums );
+                for ( b = 0; b < nRange; b++ )
                 {
-                    int iLitAnd = 1;
-                    for ( b = 0; b < nRange0; b++ )
-                        iLitAnd = Gia_ManHashAnd( pNew, iLitAnd, Abc_LitNotCond(pFans0[b], ((k >> b) & 1) == 0) );
-                    Vec_IntPush( vTemp1, iLitAnd );
-                }
-            }
-            for ( b = 0; b < nRange; b++ )
-            {
-                Vec_IntClear( vTemp0 );
-                Wlc_ObjForEachFanin( pObj, iFanin, k )
-                    if ( k > 0 )
-                    {
-                        nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
-                        pFans1  = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) );
-                        if ( Wlc_ObjFaninNum(pObj) == 3 ) // Statement 1
-                            Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (fSigned? pFans1[nRange1-1] : 0) );
-                        else // Statement 2
-                            Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (Wlc_NtkObj(p, iFanin)->Signed? pFans1[nRange1-1] : 0) );
+                    Vec_IntClear( vTemp0 );
+                    Wlc_ObjForEachFanin( pObj, iFanin, k ) {
+                        if ( k > 0 )
+                        {
+                            nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
+                            pFans1  = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) );
+                            if ( Wlc_ObjFaninNum(pObj) == 3 ) // Statement 1
+                                Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (fSigned? pFans1[nRange1-1] : 0) );
+                            else // Statement 2
+                                Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (Wlc_NtkObj(p, iFanin)->Signed? pFans1[nRange1-1] : 0) );
+                        }
                     }
+                    assert( (1 << nRange0) == Vec_IntSize(vTemp0) );
+                    Vec_IntPush( vRes, Wlc_NtkMuxTree3(pNew, vTemp0, pNums, pvDecs) );
+                }
+                Wlc_NtkMuxTree3DecsFree( pvDecs, pNums );
+            }
+            else
+            {
+                Vec_IntClear( vTemp1 );
                 if ( pPar->fDecMuxes )
-                    Vec_IntPush( vRes, Wlc_NtkMuxTree2(pNew, pFans0, nRange0, vTemp0, vTemp1, vTemp2) );
-                else
-                    Vec_IntPush( vRes, Wlc_NtkMuxTree_rec(pNew, pFans0, nRange0, vTemp0, 0) );
+                {
+                    for ( k = 0; k < (1 << nRange0); k++ )
+                    {
+                        int iLitAnd = 1;
+                        for ( b = 0; b < nRange0; b++ )
+                            iLitAnd = Gia_ManHashAnd( pNew, iLitAnd, Abc_LitNotCond(pFans0[b], ((k >> b) & 1) == 0) );
+                        Vec_IntPush( vTemp1, iLitAnd );
+                    }
+                }
+                for ( b = 0; b < nRange; b++ )
+                {
+                    Vec_IntClear( vTemp0 );
+                    Wlc_ObjForEachFanin( pObj, iFanin, k )
+                        if ( k > 0 )
+                        {
+                            nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
+                            pFans1  = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) );
+                            if ( Wlc_ObjFaninNum(pObj) == 3 ) // Statement 1
+                                Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (fSigned? pFans1[nRange1-1] : 0) );
+                            else // Statement 2
+                                Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (Wlc_NtkObj(p, iFanin)->Signed? pFans1[nRange1-1] : 0) );
+                        }
+                    if ( pPar->fDecMuxes )
+                        Vec_IntPush( vRes, Wlc_NtkMuxTree2(pNew, pFans0, nRange0, vTemp0, vTemp1, vTemp2) );
+                    else
+                        Vec_IntPush( vRes, Wlc_NtkMuxTree_rec(pNew, pFans0, nRange0, vTemp0, 0) );
+                }
             }
         }
         else if ( pObj->Type == WLC_OBJ_SEL )
@@ -1779,9 +1920,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
             int fCompl = (pObj->Type == WLC_OBJ_COMP_MOREEQU || pObj->Type == WLC_OBJ_COMP_LESSEQU);
             if ( fSwap ) ABC_SWAP( int *, pArg0, pArg1 );
             if ( fSigned )
-                iLit = Wlc_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax );
+                iLit = pParIn->fBlastNew ? Wlc_BlastLessSigned3( pNew, pArg0, pArg1, nRangeMax ) :  Wlc_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax );
             else
-                iLit = Wlc_BlastLess( pNew, pArg0, pArg1, nRangeMax );
+                iLit = pParIn->fBlastNew ? Wlc_BlastLess3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLess( pNew, pArg0, pArg1, nRangeMax );
             iLit = Abc_LitNotCond( iLit, fCompl );
             Vec_IntFill( vRes, 1, iLit );
             for ( k = 1; k < nRange; k++ )
@@ -1842,7 +1983,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
                 int nRangeMax = Abc_MaxInt(nRange0, nRange1);
                 int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, fSigned );
                 int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned );
-                if ( Wlc_NtkCountConstBits(pArg0, nRangeMax) < Wlc_NtkCountConstBits(pArg1, nRangeMax) )
+                if ( nRange0 == nRange1 && Wlc_NtkCountConstBits(pArg0, nRangeMax) < Wlc_NtkCountConstBits(pArg1, nRangeMax) )
                     ABC_SWAP( int *, pArg0, pArg1 );
                 if ( pPar->fBooth )
                     Wlc_BlastBooth( pNew, pArg0, pArg1, nRange0, nRange1, vRes, fSigned, pPar->fCla, NULL, pParIn->fVerbose );
@@ -1912,7 +2053,10 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
         else if ( pObj->Type == WLC_OBJ_DEC )
         {
             int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange0, 0 );
-            Wlc_BlastDecoder( pNew, pArg0, nRange0, vTemp2, vRes );
+            if ( pParIn->fBlastNew )
+                Wlc_BlastDecoder2( pNew, pArg0, nRange0, vTemp2, vRes );
+            else
+                Wlc_BlastDecoder( pNew, pArg0, nRange0, vTemp2, vRes );
             if ( nRange > Vec_IntSize(vRes) )
                 Vec_IntFillExtra( vRes, nRange, 0 );
             else
@@ -2745,6 +2889,47 @@ void Wlc_TransferPioNames( Wlc_Ntk_t * p, Gia_Man_t * pNew )
         printf( "Successfully transferred the primary input/output names from the word-level design to the current AIG.\n" );
 }
     
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_MultBlastFileGen( int a, int b, int s )
+{
+    FILE * pFile = fopen( "_test13_.v", "wb" );
+    fprintf( pFile, "module test ( a, b, z );\n" );
+    fprintf( pFile, "input %s [%d:0] a;\n", s ? "signed":"", a-1 );
+    fprintf( pFile, "input %s [%d:0] b;\n", s ? "signed":"", b-1 );
+    fprintf( pFile, "output %s [%d:0] z;\n", s ? "signed":"", a+b-1 );
+    fprintf( pFile, "assign z = a * b;\n" );
+    fprintf( pFile, "endmodule\n" );    
+    fclose( pFile );
+}
+void Wlc_MultBlastTest()
+{
+    char * Command = "%read _test13_.v; %blast; &ps; &w 1.aig;  %read _test13_.v; %blast -b; &ps; &w 2.aig; cec -n 1.aig 2.aig";
+    int a, b, s, Iters = 0;
+    for ( a = 1; a < 8; a++ )
+    for ( b = 1; b < 8; b++ )
+    for ( s = 0; s < 2; s++ )
+    {
+        Wlc_MultBlastFileGen( a, b, s );
+        if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) )
+        {
+            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
+            return;
+        }
+        Iters++;
+    }
+    printf( "Finished %d iterations.\n", Iters );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/wlc/wlcCom.c

@@ -1046,7 +1046,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_BstParDefault( pPar );
     pPar->nOutputRange = 2;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombqaydestrnizvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombqaydestrfnizvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -1131,9 +1131,12 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             fReorder ^= 1;
             break;
-        case 'n':
+        case 'f':
             fDumpNames ^= 1;
             break;
+        case 'n':
+            pPar->fBlastNew ^= 1;
+            break;            
         case 'i': 
             fPrintInputInfo ^= 1; 
             break;
@@ -1222,7 +1225,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameUpdateGia( pAbc, pNew );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%blast [-ORAM num] [-combqaydestrnizvh]\n" );
+    Abc_Print( -2, "usage: %%blast [-ORAM num] [-combqaydestrfnizvh]\n" );
     Abc_Print( -2, "\t         performs bit-blasting of the word-level design\n" );
     Abc_Print( -2, "\t-O num : zero-based index of the first word-level PO to bit-blast [default = %d]\n", pPar->iOutput );
     Abc_Print( -2, "\t-R num : the total number of word-level POs to bit-blast [default = %d]\n",          pPar->nOutputRange );
@@ -1240,7 +1243,8 @@ usage:
     Abc_Print( -2, "\t-s     : toggle creating decoded MUXes [default = %s]\n",                            pPar->fDecMuxes? "yes": "no" );
     Abc_Print( -2, "\t-t     : toggle creating regular multi-output miter [default = %s]\n",               fMiter? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using interleaved variable ordering [default = %s]\n",               fReorder? "yes": "no" );
-    Abc_Print( -2, "\t-n     : toggle dumping signal names into a text file [default = %s]\n",             fDumpNames? "yes": "no" );
+    Abc_Print( -2, "\t-f     : toggle dumping signal names into a text file [default = %s]\n",             fDumpNames? "yes": "no" );
+    Abc_Print( -2, "\t-n     : toggle using improved bit-blasting procedures [default = %s]\n",            pPar->fBlastNew? "yes": "no" );
     Abc_Print( -2, "\t-i     : toggle to print input names after blasting [default = %s]\n",               fPrintInputInfo ? "yes": "no" );
     Abc_Print( -2, "\t-z     : toggle saving flop names after blasting [default = %s]\n",                  pPar->fSaveFfNames ? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                      pPar->fVerbose? "yes": "no" );

src/bdd/dsd/dsd.h

@@ -117,7 +117,11 @@ extern Dsd_Node_t **   Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNo
 extern Dsd_Node_t **   Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes );
 extern void            Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output, int OffSet );
 extern void            Dsd_TreePrint2( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int Output );
+extern void            Dsd_TreePrint3( void * pStr, Dsd_Manager_t * pDsdMan, int Output );
+extern void            Dsd_TreePrint4( void * pStr, Dsd_Manager_t * pDsdMan, int Output );
 extern void            Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode );
+extern int             Dsd_TreeNonDsdMax( Dsd_Manager_t * pDsdMan, int Output );
+extern int             Dsd_TreeSuppSize( Dsd_Manager_t * pDsdMan, int Output );
 /*=== dsdLocal.c =======================================================*/
 extern DdNode *        Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode );
 

src/bdd/dsd/dsdTree.c

@@ -627,6 +627,195 @@ void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], in
     ppNodes[ (*pnNodes)++ ] = pNode;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the size of the largest non-DSD block.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dsd_TreeNonDsdMax_rec( Dsd_Node_t * pNode )
+{
+    if ( pNode->Type == DSD_NODE_CONST1 )
+        return 0;
+    if ( pNode->Type == DSD_NODE_BUF )
+        return 0;
+    int MaxBlock = pNode->Type == DSD_NODE_PRIME ? pNode->nDecs : 0;
+    for ( int i = 0; i < pNode->nDecs; i++ )
+    {
+        int MaxThis = Dsd_TreeNonDsdMax_rec( Dsd_Regular( pNode->pDecs[i] ) );
+        MaxBlock = Abc_MaxInt( MaxBlock, MaxThis );
+    }
+    return MaxBlock;
+}
+int Dsd_TreeNonDsdMax( Dsd_Manager_t * pDsdMan, int Output )
+{
+    if ( Output == -1 ) 
+    {
+        int i, Res = 0;
+        for ( i = 0; i < pDsdMan->nRoots; i++ )
+            Res = Abc_MaxInt( Res, Dsd_TreeNonDsdMax_rec( Dsd_Regular( pDsdMan->pRoots[i] ) ) );
+        return Res;
+    }
+    else 
+    {
+        assert( Output >= 0 && Output < pDsdMan->nRoots );
+        return Dsd_TreeNonDsdMax_rec( Dsd_Regular( pDsdMan->pRoots[Output] ) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the support size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dsd_TreeSuppSize_rec( Dsd_Node_t * pNode )
+{
+    if ( pNode->Type == DSD_NODE_CONST1 )
+        return 0;
+    if ( pNode->Type == DSD_NODE_BUF )
+        return 1;
+    int nSuppSize = 0;
+    for ( int i = 0; i < pNode->nDecs; i++ )
+        nSuppSize += Dsd_TreeSuppSize_rec( Dsd_Regular( pNode->pDecs[i] ) );
+    return nSuppSize;
+}
+int Dsd_TreeSuppSize( Dsd_Manager_t * pDsdMan, int Output )
+{
+    if ( Output == -1 ) 
+    {
+        int i, Res = 0;
+        for ( i = 0; i < pDsdMan->nRoots; i++ )
+            Res += Dsd_TreeSuppSize_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
+        return Res;
+    }
+    else 
+    {
+        assert( Output >= 0 && Output < pDsdMan->nRoots );
+        return Dsd_TreeSuppSize_rec( Dsd_Regular( pDsdMan->pRoots[Output] ) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the decompostion tree into a string.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dsd_TreePrint3_rec( Vec_Str_t * p, Dsd_Node_t * pNode )
+{
+    if ( pNode->Type == DSD_NODE_BUF ) {
+        Vec_StrPush( p, (int)(pNode->S->index >= 26 ? 'A' - 26 : 'a') + pNode->S->index );
+        return;
+    }
+    if ( pNode->Type == DSD_NODE_PRIME )
+        Vec_StrPush( p, '{' );
+    else if ( pNode->Type == DSD_NODE_OR )
+        Vec_StrPush( p, '(' );
+    else if ( pNode->Type == DSD_NODE_EXOR )
+        Vec_StrPush( p, '[' );
+    else assert( 0 );
+    for ( int i = 0; i < pNode->nDecs; i++ )
+    {
+        Dsd_Node_t * pInput = Dsd_Regular( pNode->pDecs[i] );
+        if ( pInput != pNode->pDecs[i] )
+            Vec_StrPush( p, '~' );
+        Dsd_TreePrint3_rec( p, pInput );
+    }
+    if ( pNode->Type == DSD_NODE_PRIME )
+        Vec_StrPush( p, '}' );
+    else if ( pNode->Type == DSD_NODE_OR )
+        Vec_StrPush( p, ')' );
+    else if ( pNode->Type == DSD_NODE_EXOR )
+        Vec_StrPush( p, ']' );
+    else assert( 0 );
+}
+void Dsd_TreePrint3( void * pStr, Dsd_Manager_t * pDsdMan, int Output )
+{
+    Vec_Str_t * p = (Vec_Str_t *)pStr;
+    assert( Output >= 0 && Output < pDsdMan->nRoots );
+    Dsd_Node_t * pNode = Dsd_Regular( pDsdMan->pRoots[Output] );
+    int fCompl = pNode != pDsdMan->pRoots[Output];
+    if ( pNode->Type == DSD_NODE_CONST1 ) 
+        Vec_StrPush( p, fCompl ? '0' : '1' );
+    else {
+        if ( fCompl )
+            Vec_StrPush( p, '~' );
+        Dsd_TreePrint3_rec( p, pNode );
+    }    
+    Vec_StrPush( p, '\0' );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the decompostion tree into a string.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dsd_TreePrint4_rec( Vec_Str_t * p, Dsd_Node_t * pNode )
+{
+    if ( pNode->Type == DSD_NODE_BUF ) {
+        Vec_StrPush( p, (int)(pNode->S->index >= 26 ? 'A' - 26 : 'a') + pNode->S->index );
+        return;
+    }
+    if ( pNode->Type == DSD_NODE_PRIME )
+        Vec_StrPush( p, '{' );
+    else if ( pNode->Type == DSD_NODE_OR )
+        Vec_StrPush( p, '(' );
+    else if ( pNode->Type == DSD_NODE_EXOR )
+        Vec_StrPush( p, '[' );
+    else assert( 0 );
+    for ( int i = 0; i < pNode->nDecs; i++ )
+    {
+        Dsd_Node_t * pInput = Dsd_Regular( pNode->pDecs[i] );
+        if ( (pInput != pNode->pDecs[i]) ^ (pNode->Type == DSD_NODE_OR) ^ (pInput->Type == DSD_NODE_OR) )
+            Vec_StrPush( p, '~' );
+        Dsd_TreePrint4_rec( p, pInput );
+    }
+    if ( pNode->Type == DSD_NODE_PRIME )
+        Vec_StrPush( p, '}' );
+    else if ( pNode->Type == DSD_NODE_OR )
+        Vec_StrPush( p, ')' );
+    else if ( pNode->Type == DSD_NODE_EXOR )
+        Vec_StrPush( p, ']' );
+    else assert( 0 );
+}
+void Dsd_TreePrint4( void * pStr, Dsd_Manager_t * pDsdMan, int Output )
+{
+    Vec_Str_t * p = (Vec_Str_t *)pStr;
+    assert( Output >= 0 && Output < pDsdMan->nRoots );
+    Dsd_Node_t * pNode = Dsd_Regular( pDsdMan->pRoots[Output] );
+    int fCompl = pNode != pDsdMan->pRoots[Output];
+    if ( pNode->Type == DSD_NODE_CONST1 ) 
+        Vec_StrPush( p, fCompl ? '0' : '1' );
+    else {
+        if ( fCompl ^ (pNode->Type == DSD_NODE_OR) )
+            Vec_StrPush( p, '~' );
+        Dsd_TreePrint4_rec( p, pNode );
+    }    
+    Vec_StrPush( p, '\0' );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Prints the decompostion tree into file.]

src/bdd/extrab/extraLutCas.h

@@ -32,7 +32,9 @@
 #include <string.h>
 #include <assert.h>
 
+#include "aig/miniaig/miniaig.h"
 #include "bdd/cudd/cuddInt.h"
+#include "bdd/dsd/dsd.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -50,6 +52,8 @@ ABC_NAMESPACE_HEADER_START
     If the LUT cascade contains a 6-LUT followed by a 4-LUT, the record contains 1+10+8=19 words.
 */
 
+#define Mini_AigForEachNonPo( p, i )  for (i = 1; i < Mini_AigNodeNum(p); i++) if ( Mini_AigNodeIsPo(p, i) ) {} else 
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -61,12 +65,128 @@ ABC_NAMESPACE_HEADER_START
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_LutCasCollapseDeref( DdManager * dd, Vec_Ptr_t * vFuncs )
+{
+    DdNode * bFunc; int i;
+    Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
+        if ( bFunc )
+            Cudd_RecursiveDeref( dd, bFunc );
+    Vec_PtrFree( vFuncs );
+}
+Vec_Ptr_t * Abc_LutCasCollapse( Mini_Aig_t * p, DdManager * dd, int nBddLimit, int fVerbose )
+{
+    DdNode * bFunc0, * bFunc1, * bFunc;  int Id, nOuts = 0;
+    Vec_Ptr_t * vFuncs = Vec_PtrStart( Mini_AigNodeNum(p) );
+    Vec_PtrWriteEntry( vFuncs, 0, Cudd_ReadLogicZero(dd) ), Cudd_Ref(Cudd_ReadLogicZero(dd));
+    Mini_AigForEachPi( p, Id )
+      Vec_PtrWriteEntry( vFuncs, Id, Cudd_bddIthVar(dd,Id-1) ), Cudd_Ref(Cudd_bddIthVar(dd,Id-1));
+    Mini_AigForEachAnd( p, Id ) {
+        bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Mini_AigLit2Var(Mini_AigNodeFanin0(p, Id))), Mini_AigLitIsCompl(Mini_AigNodeFanin0(p, Id)) );
+        bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Mini_AigLit2Var(Mini_AigNodeFanin1(p, Id))), Mini_AigLitIsCompl(Mini_AigNodeFanin1(p, Id)) );
+        bFunc  = Cudd_bddAndLimit( dd, bFunc0, bFunc1, nBddLimit );  
+        if ( bFunc == NULL )
+        {
+            Abc_LutCasCollapseDeref( dd, vFuncs );
+            return NULL;
+        }        
+        Cudd_Ref( bFunc );
+        Vec_PtrWriteEntry( vFuncs, Id, bFunc );
+    }
+    Mini_AigForEachPo( p, Id ) {
+        bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Mini_AigLit2Var(Mini_AigNodeFanin0(p, Id))), Mini_AigLitIsCompl(Mini_AigNodeFanin0(p, Id)) );
+        Vec_PtrWriteEntry( vFuncs, Id, bFunc0 ); Cudd_Ref( bFunc0 );
+    }
+    Mini_AigForEachNonPo( p, Id ) {
+      bFunc = (DdNode *)Vec_PtrEntry(vFuncs, Id);
+      Cudd_RecursiveDeref( dd, bFunc );
+      Vec_PtrWriteEntry( vFuncs, Id, NULL );
+    }
+    Mini_AigForEachPo( p, Id ) 
+        Vec_PtrWriteEntry( vFuncs, nOuts++, Vec_PtrEntry(vFuncs, Id) );
+    Vec_PtrShrink( vFuncs, nOuts );
+    return vFuncs;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_LutCasFakeNames( int nNames )
+{
+    Vec_Ptr_t * vNames;
+    char Buffer[5];
+    int i;
+
+    vNames = Vec_PtrAlloc( nNames );
+    for ( i = 0; i < nNames; i++ )
+    {
+        if ( nNames < 26 )
+        {
+            Buffer[0] = 'a' + i;
+            Buffer[1] = 0;
+        }
+        else
+        {
+            Buffer[0] = 'a' + i%26;
+            Buffer[1] = '0' + i/26;
+            Buffer[2] = 0;
+        }
+        Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) );
+    }
+    return vNames;
+}
+void Abc_LutCasPrintDsd( DdManager * dd, DdNode * bFunc, int fVerbose )
+{
+    Dsd_Manager_t * pManDsd = Dsd_ManagerStart( dd, dd->size, 0 );
+    Dsd_Decompose( pManDsd, &bFunc, 1 );
+    if ( fVerbose )
+    {
+        Vec_Ptr_t * vNamesCi = Abc_LutCasFakeNames( dd->size );
+        Vec_Ptr_t * vNamesCo = Abc_LutCasFakeNames( 1 );
+        char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
+        char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
+        Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, 0 );
+        Vec_PtrFreeFree( vNamesCi );
+        Vec_PtrFreeFree( vNamesCo );
+    }
+    Dsd_ManagerStop( pManDsd );
+}    
+DdNode * Abc_LutCasBuildBdds( Mini_Aig_t * p, DdManager ** pdd )
+{
+    DdManager * dd = Cudd_Init( Mini_AigPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+    Vec_Ptr_t * vFuncs = Abc_LutCasCollapse( p, dd, 10000, 0 );
+    Cudd_AutodynDisable( dd );
+    if ( vFuncs == NULL ) {
+        Extra_StopManager( dd );
+        return NULL;
+    }
+    DdNode * bNode = (DdNode *)Vec_PtrEntry(vFuncs, 0);
+    Vec_PtrFree(vFuncs);
+    *pdd = dd;
+    return bNode;
+}
 static inline word * Abc_LutCascade( Mini_Aig_t * p, int nLutSize, int fVerbose )
 {
+    DdManager * dd = NULL;
+    DdNode * bFunc = Abc_LutCasBuildBdds( p, &dd );
+    if ( bFunc == NULL ) return NULL;
+    Abc_LutCasPrintDsd( dd, bFunc, 1 );
+    Cudd_RecursiveDeref( dd, bFunc );
+    Extra_StopManager( dd );
+
     word * pLuts = NULL;
     return pLuts;
 }
 
 ABC_NAMESPACE_HEADER_END
 
-#endif /* __EXTRA_H__ */
+#endif /* ABC__misc__extra__extra_lutcas_h */

src/map/if/acd/ac_decomposition.hpp

@@ -510,7 +510,7 @@ private:
       }
     } while ( combinations_offset_next( free_set_size, offset, pComb, pInvPerm, tt ) );
 
-    std::array<uint32_t, max_num_vars> res_perm;
+    std::array<uint32_t, max_num_vars> res_perm = {0};
     
     if ( best_cost > ( 1 << ( ps.lut_size - free_set_size ) ) )
     {
@@ -543,7 +543,7 @@ private:
     }
 
     /* enumerate combinations */
-    std::array<uint32_t, max_num_vars> res_perm;
+    std::array<uint32_t, max_num_vars> res_perm = {0};
 
     do
     {

src/map/scl/scl.c

@@ -185,13 +185,14 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVeryVerbose = 0;
     int fMerge = 0;
     int fUsePrefix = 0;
+    int fUseAll = 0;
     
     SC_DontUse dont_use = {0};
     dont_use.dont_use_list = ABC_ALLOC(char *, argc);
     dont_use.size = 0;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SGMXdnuvwmph" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SGMXdnuvwmpah" ) ) != EOF )
     {
         switch ( c )
         {
@@ -259,6 +260,9 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             fUsePrefix ^= 1;
             break;            
+        case 'a':
+            fUseAll ^= 1;
+            break;            
         case 'h':
             goto usage;
         default:
@@ -318,13 +322,13 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv )
     // extract genlib library
     if ( pAbc->pLibScl )
     {
-        Abc_SclInstallGenlib( pAbc->pLibScl, Slew, Gain, nGatesMin );
+        Abc_SclInstallGenlib( pAbc->pLibScl, Slew, Gain, fUseAll, nGatesMin );
         Mio_LibraryTransferCellIds();
     }
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: read_lib [-SG float] [-M num] [-dnuvwmph] [-X cell_name] <file> <file2>\n" );
+    fprintf( pAbc->Err, "usage: read_lib [-SG float] [-M num] [-dnuvwmpah] [-X cell_name] <file> <file2>\n" );
     fprintf( pAbc->Err, "\t           reads Liberty library from file\n" );
     fprintf( pAbc->Err, "\t-S float : the slew parameter used to generate the library [default = %.2f]\n", Slew );
     fprintf( pAbc->Err, "\t-G float : the gain parameter used to generate the library [default = %.2f]\n", Gain );
@@ -336,6 +340,7 @@ usage:
     fprintf( pAbc->Err, "\t-v       : toggle writing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pAbc->Err, "\t-w       : toggle writing information about skipped gates [default = %s]\n", fVeryVerbose? "yes": "no" );
     fprintf( pAbc->Err, "\t-m       : toggle merging library with exisiting library [default = %s]\n", fMerge? "yes": "no" );
+    fprintf( pAbc->Err, "\t-a       : toggle using prefix for the cell names [default = %s]\n", fUseAll? "yes": "no" );
     fprintf( pAbc->Err, "\t-p       : toggle using prefix for the cell names [default = %s]\n", fUsePrefix? "yes": "no" );
     fprintf( pAbc->Err, "\t-h       : prints the command summary\n" );
     fprintf( pAbc->Err, "\t<file>   : the name of a file to read\n" );
@@ -606,7 +611,7 @@ int Scl_CommandReadScl( Abc_Frame_t * pAbc, int argc, char ** argv )
     // extract genlib library
     if ( pAbc->pLibScl )
     {
-        Abc_SclInstallGenlib( pAbc->pLibScl, 0, 0, 0 );
+        Abc_SclInstallGenlib( pAbc->pLibScl, 0, 0, 0, 0 );
         Mio_LibraryTransferCellIds();
     }
     return 0;

src/map/scl/sclBufSize.c

@@ -345,7 +345,7 @@ Abc_Obj_t * Abc_SclAddOneInv( Bus_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFano
     SC_Cell * pCellNew;
     Abc_Obj_t * pFanout, * pInv;
     float Target = SC_CellPinCap(p->pInv, 0) * Gain;
-    float LoadWirePrev, LoadWireThis, LoadNew, Load = 0;
+    float LoadWirePrev, LoadWireThis, Load = 0;
     int Limit = Abc_MinInt( p->pPars->nDegree, Vec_PtrSize(vFanouts) );
     int i, iStop;
     Bus_SclCheckSortedFanout( vFanouts );
@@ -384,8 +384,7 @@ Abc_Obj_t * Abc_SclAddOneInv( Bus_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFano
     Vec_IntSetEntry( p->pNtk->vGates, Abc_ObjId(pInv), pCellNew->Id );
     // set departure and load
     Abc_NtkComputeNodeDeparture( pInv, p->pPars->Slew );
-    LoadNew = Abc_NtkComputeNodeLoad( p, pInv );
-    assert( LoadNew - Load < 1 && Load - LoadNew < 1 );
+    Abc_NtkComputeNodeLoad( p, pInv );
     // set fanout info for the inverter
     Bus_SclObjSetCin( pInv, SC_CellPinCap(pCellNew, 0) );
     Bus_SclObjSetETime( pInv, Abc_NtkComputeEdgeDept(pInv, 0, p->pPars->Slew) );
@@ -400,7 +399,7 @@ void Abc_SclBufSize( Bus_Man_t * p, float Gain )
     Abc_Obj_t * pObj, * pFanout;
     abctime clk = Abc_Clock();
     int i, k, nObjsOld = Abc_NtkObjNumMax(p->pNtk);
-    float GainGate, GainInv, Load, LoadNew, Cin, DeptMax = 0;
+    float GainGate, GainInv, Load, Cin, DeptMax = 0;
     GainGate = p->pPars->fAddBufs ? (float)pow( (double)Gain, (double)2.0 ) : Gain;
     GainInv  = p->pPars->fAddBufs ? (float)pow( (double)Gain, (double)2.0 ) : Gain;
     Abc_NtkForEachObjReverse( p->pNtk, pObj, i )
@@ -453,8 +452,7 @@ void Abc_SclBufSize( Bus_Man_t * p, float Gain )
                 if ( Abc_ObjFaninNum(pFanout) == 0 )
                     Abc_ObjAddFanin( pFanout, pObj );
             Bus_SclObjSetLoad( pObj, 0 );
-            LoadNew = Abc_NtkComputeNodeLoad( p, pObj );
-            assert( LoadNew - Load < 1 && Load - LoadNew < 1 );
+            Abc_NtkComputeNodeLoad( p, pObj );
         } 
         if ( Abc_ObjIsCi(pObj) )
             continue;

src/map/scl/sclLib.h

@@ -766,7 +766,7 @@ extern SC_WireLoad * Abc_SclFetchWireLoadModel( SC_Lib * p, char * pName );
 extern int           Abc_SclHasDelayInfo( void * pScl );
 extern float         Abc_SclComputeAverageSlew( SC_Lib * p );
 extern void          Abc_SclDumpGenlib( char * pFileName, SC_Lib * p, float Slew, float Gain, int nGatesMin );
-extern void          Abc_SclInstallGenlib( void * pScl, float Slew, float Gain, int nGatesMin );
+extern void          Abc_SclInstallGenlib( void * pScl, float Slew, float Gain, int fUseAll, int nGatesMin );
 
 
 ABC_NAMESPACE_HEADER_END

src/map/scl/sclLibUtil.c

@@ -867,13 +867,13 @@ Mio_Library_t * Abc_SclDeriveGenlibSimple( void * pScl )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Str_t * Abc_SclProduceGenlibStr( SC_Lib * p, float Slew, float Gain, int nGatesMin, int * pnCellCount )
+Vec_Str_t * Abc_SclProduceGenlibStr( SC_Lib * p, float Slew, float Gain, int nGatesMin, int fUseAll, int * pnCellCount )
 {
     char Buffer[200];
     Vec_Str_t * vStr;
     SC_Cell * pRepr;
-    SC_Pin * pPin;
-    int i, k, Count = 2, nClassMax = 0;
+    SC_Pin * pPin, * pPinOut;
+    int i, j, k, Count = 2, nClassMax = 0;
     // find the largest number of cells in a class
     SC_LibForEachCellClass( p, pRepr, i )
         if ( pRepr->n_outputs == 1 )
@@ -886,38 +886,80 @@ Vec_Str_t * Abc_SclProduceGenlibStr( SC_Lib * p, float Slew, float Gain, int nGa
     vStr = Vec_StrAlloc( 1000 );
     Vec_StrPrintStr( vStr, "GATE _const0_            0.00 z=CONST0;\n" );
     Vec_StrPrintStr( vStr, "GATE _const1_            0.00 z=CONST1;\n" );
-    SC_LibForEachCellClass( p, pRepr, i )
+    if ( fUseAll )
     {
-        if ( pRepr->n_inputs == 0 )
-            continue;
-        if ( pRepr->n_outputs > 1 )
-            continue;
-        if ( nGatesMin && pRepr->n_inputs > 2 && Abc_SclClassCellNum(pRepr) < nGatesMin )
-            continue;
-        assert( strlen(pRepr->pName) < 200 );
-        Vec_StrPrintStr( vStr, "GATE " );
-        sprintf( Buffer, "%-16s", pRepr->pName );
-        Vec_StrPrintStr( vStr, Buffer );
-        Vec_StrPrintStr( vStr, " " );
-//        sprintf( Buffer, "%7.2f", Abc_SclComputeAreaClass(pRepr) );
-        sprintf( Buffer, "%7.2f", pRepr->area );
-        Vec_StrPrintStr( vStr, Buffer );
-        Vec_StrPrintStr( vStr, " " );
-        Vec_StrPrintStr( vStr, SC_CellPinName(pRepr, pRepr->n_inputs) );
-        Vec_StrPrintStr( vStr, "=" );
-        Vec_StrPrintStr( vStr, SC_CellPinOutFunc(pRepr, 0) ? SC_CellPinOutFunc(pRepr, 0) : "?" );
-        Vec_StrPrintStr( vStr, ";\n" );
-        SC_CellForEachPinIn( pRepr, pPin, k )
+        SC_LibForEachCell( p, pRepr, i )
         {
-            float Delay = Abc_SclComputeDelayClassPin( p, pRepr, k, Slew, Gain );
-            assert( Delay > 0 );
-            Vec_StrPrintStr( vStr, "         PIN " );
-            sprintf( Buffer, "%-4s", pPin->pName );
-            Vec_StrPrintStr( vStr, Buffer );
-            sprintf( Buffer, " UNKNOWN  1  999  %7.2f  0.00  %7.2f  0.00\n", Delay, Delay );
-            Vec_StrPrintStr( vStr, Buffer );
+            if ( pRepr->n_inputs == 0 )
+                continue;
+            //if ( pRepr->n_outputs > 1 )
+            //    continue;
+            if ( nGatesMin && pRepr->n_inputs > 2 && Abc_SclClassCellNum(pRepr) < nGatesMin )
+                continue;
+            SC_CellForEachPinOut( pRepr, pPinOut, j )
+            {
+                assert( strlen(pRepr->pName) < 200 );
+                Vec_StrPrintStr( vStr, "GATE " );
+                sprintf( Buffer, "%-16s", pRepr->pName );
+                Vec_StrPrintStr( vStr, Buffer );
+                Vec_StrPrintStr( vStr, " " );
+        //        sprintf( Buffer, "%7.2f", Abc_SclComputeAreaClass(pRepr) );
+                sprintf( Buffer, "%7.2f", pRepr->area );
+                Vec_StrPrintStr( vStr, Buffer );
+                Vec_StrPrintStr( vStr, " " );
+                Vec_StrPrintStr( vStr, SC_CellPinName(pRepr, j) );
+                Vec_StrPrintStr( vStr, "=" );
+                Vec_StrPrintStr( vStr, SC_CellPinOutFunc(pRepr, j-pRepr->n_inputs) ? SC_CellPinOutFunc(pRepr, j-pRepr->n_inputs) : "?" );
+                Vec_StrPrintStr( vStr, ";\n" );
+                SC_CellForEachPinIn( pRepr, pPin, k )
+                {
+                    float Delay = Abc_SclComputeDelayClassPin( p, pRepr, k, Slew, Gain );
+                    assert( Delay > 0 );
+                    Vec_StrPrintStr( vStr, "         PIN " );
+                    sprintf( Buffer, "%-4s", pPin->pName );
+                    Vec_StrPrintStr( vStr, Buffer );
+                    sprintf( Buffer, " UNKNOWN  1  999  %7.2f  0.00  %7.2f  0.00\n", Delay, Delay );
+                    Vec_StrPrintStr( vStr, Buffer );
+                }
+                Count++;
+            }
+        }
+    }
+    else
+    {
+        SC_LibForEachCellClass( p, pRepr, i )
+        {
+            if ( pRepr->n_inputs == 0 )
+                continue;
+            if ( pRepr->n_outputs > 1 )
+                continue;
+            if ( nGatesMin && pRepr->n_inputs > 2 && Abc_SclClassCellNum(pRepr) < nGatesMin )
+                continue;
+            assert( strlen(pRepr->pName) < 200 );
+            Vec_StrPrintStr( vStr, "GATE " );
+            sprintf( Buffer, "%-16s", pRepr->pName );
+            Vec_StrPrintStr( vStr, Buffer );
+            Vec_StrPrintStr( vStr, " " );
+    //        sprintf( Buffer, "%7.2f", Abc_SclComputeAreaClass(pRepr) );
+            sprintf( Buffer, "%7.2f", pRepr->area );
+            Vec_StrPrintStr( vStr, Buffer );
+            Vec_StrPrintStr( vStr, " " );
+            Vec_StrPrintStr( vStr, SC_CellPinName(pRepr, pRepr->n_inputs) );
+            Vec_StrPrintStr( vStr, "=" );
+            Vec_StrPrintStr( vStr, SC_CellPinOutFunc(pRepr, 0) ? SC_CellPinOutFunc(pRepr, 0) : "?" );
+            Vec_StrPrintStr( vStr, ";\n" );
+            SC_CellForEachPinIn( pRepr, pPin, k )
+            {
+                float Delay = Abc_SclComputeDelayClassPin( p, pRepr, k, Slew, Gain );
+                assert( Delay > 0 );
+                Vec_StrPrintStr( vStr, "         PIN " );
+                sprintf( Buffer, "%-4s", pPin->pName );
+                Vec_StrPrintStr( vStr, Buffer );
+                sprintf( Buffer, " UNKNOWN  1  999  %7.2f  0.00  %7.2f  0.00\n", Delay, Delay );
+                Vec_StrPrintStr( vStr, Buffer );
+            }
+            Count++;
         }
-        Count++;
     }
     Vec_StrPrintStr( vStr, "\n.end\n" );
     Vec_StrPush( vStr, '\0' );
@@ -1012,7 +1054,7 @@ void Abc_SclDumpGenlib( char * pFileName, SC_Lib * p, float SlewInit, float Gain
         printf( "Cannot open file \"%s\" for writing.\n", FileName );
         return;
     }
-    vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, &nCellCount );
+    vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, 0, &nCellCount );
     fprintf( pFile, "%s", Vec_StrArray(vStr) );
     Vec_StrFree( vStr );
     fclose( pFile );
@@ -1026,7 +1068,7 @@ Mio_Library_t * Abc_SclDeriveGenlib( void * pScl, void * pMio, float SlewInit, f
     Vec_Str_t * vStr;
     Mio_Library_t * pLib;
     if ( pMio == NULL )
-        vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, &nCellCount );
+        vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, 0, &nCellCount );
     else
         vStr = Abc_SclProduceGenlibStrProfile( p, (Mio_Library_t *)pMio, Slew, Gain, nGatesMin, &nCellCount );
     pLib = Mio_LibraryRead( p->pFileName, Vec_StrArray(vStr), NULL, 0, 0 );  
@@ -1049,7 +1091,7 @@ Mio_Library_t * Abc_SclDeriveGenlib( void * pScl, void * pMio, float SlewInit, f
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_SclInstallGenlib( void * pScl, float SlewInit, float Gain, int nGatesMin )
+void Abc_SclInstallGenlib( void * pScl, float SlewInit, float Gain, int fUseAll, int nGatesMin )
 {
     SC_Lib * p = (SC_Lib *)pScl;
     Vec_Str_t * vStr, * vStr2;
@@ -1058,7 +1100,7 @@ void Abc_SclInstallGenlib( void * pScl, float SlewInit, float Gain, int nGatesMi
     if ( Gain == 0 )
         vStr = Abc_SclProduceGenlibStrSimple(p);
     else
-        vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, &nGateCount );
+        vStr = Abc_SclProduceGenlibStr( p, Slew, Gain, nGatesMin, fUseAll, &nGateCount );
     vStr2 = Vec_StrDup( vStr );
     RetValue = Mio_UpdateGenlib2( vStr, vStr2, p->pName, 0 );
     Vec_StrFree( vStr );

src/misc/extra/extraUtilFile.c

@@ -18,6 +18,13 @@
 
 ***********************************************************************/
 
+#ifdef WIN32
+#include <windows.h>
+#define PATH_MAX MAX_PATH
+#else
+#include <limits.h>
+#endif
+
 #include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -184,9 +191,9 @@ char * Extra_FileNameGeneric( char * FileName )
 ***********************************************************************/
 char * Extra_FileNameGenericAppend( char * pBase, char * pSuffix )
 {
-    static char Buffer[1000];
+    static char Buffer[PATH_MAX];
     char * pDot;
-    assert( strlen(pBase) + strlen(pSuffix) < 1000 );
+    assert( strlen(pBase) + strlen(pSuffix) < PATH_MAX );
     strcpy( Buffer, pBase );
     if ( (pDot = strrchr( Buffer, '.' )) )
         *pDot = 0;

src/misc/util/abc_global.h

@@ -287,6 +287,9 @@ static inline double   Abc_Word2Dbl( word Num )               { union { word x;
 static inline int      Abc_Base2Log( unsigned n )             { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n >>= 1, r++ ) {}; return r; }
 static inline int      Abc_Base10Log( unsigned n )            { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 10, r++ ) {}; return r; }
 static inline int      Abc_Base16Log( unsigned n )            { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 16, r++ ) {}; return r; }
+static inline int      Abc_Base2LogW( word n )                { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n >>= 1, r++ ) {}; return r; }
+static inline int      Abc_Base10LogW( word n )               { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 10, r++ ) {}; return r; }
+static inline int      Abc_Base16LogW( word n )               { int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n /= 16, r++ ) {}; return r; }
 static inline char *   Abc_UtilStrsav( char * s )             { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL;  }
 static inline char *   Abc_UtilStrsavTwo( char * s, char * a ){ char * r; if (!a) return Abc_UtilStrsav(s); r = ABC_ALLOC(char, strlen(s)+strlen(a)+1); sprintf(r, "%s%s", s, a ); return r; }
 static inline char *   Abc_UtilStrsavNum( char * s, int n )   { char * r; if (!s) return NULL;              r = ABC_ALLOC(char, strlen(s)+12+1);        sprintf(r, "%s%d", s, n ); return r; }

src/misc/util/utilTruth.h

@@ -225,6 +225,33 @@ static inline void Abc_TtMask( word * pTruth, int nWords, int nBits )
             pTruth[w] = 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline word Abc_TtWordReverseBits( word w )
+{
+    int Rev[16] = {0, 8, 4, 12, 2, 10, 6, 14, 1, 9, 5, 13, 3, 11, 7, 15};
+    word r = 0; int i;
+    for ( i = 0; i < 16; i++ )
+        r |= (word)Rev[(w >> (i<<2))&15] << ((15-i)<<2);
+    return r;
+}
+static inline word Abc_TtWordReverseHexDigits( word w ) 
+{
+    word r = 0; int i;
+    for ( i = 0; i < 16; i++ )
+        r |= ((w >> (i<<2))&15) << ((15-i)<<2);
+    return r;
+}
+
 /**Function*************************************************************
 
   Synopsis    []

src/misc/vec/vecInt.h

@@ -65,6 +65,8 @@ struct Vec_Int_t_
     for ( i = Start; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- )
 #define Vec_IntForEachEntryTwo( vVec1, vVec2, Entry1, Entry2, i )                           \
     for ( i = 0; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ )
+#define Vec_IntForEachEntryThree( vVec1, vVec2, vVec3, Entry1, Entry2, Entry3, i )          \
+    for ( i = 0; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1) && (((Entry3) = Vec_IntEntry(vVec3, i)), 1); i++ )
 #define Vec_IntForEachEntryTwoStart( vVec1, vVec2, Entry1, Entry2, i, Start )               \
     for ( i = Start; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ )
 #define Vec_IntForEachEntryDouble( vVec, Entry1, Entry2, i )                                \

src/opt/dau/dauNpn.c

@@ -859,6 +859,128 @@ Vec_Mem_t * Dau_CollectNpnFunctions( word * p, int nVars, int fVerbose )
     return vTtMem;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Compute NPN class members.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Mem_t * Dau_CollectNpnFunctionsArray( Vec_Wrd_t * vFuncs, int nVars, Vec_Int_t ** pvMap, int fVerbose )
+{
+    assert( nVars <= 10 );
+    abctime clkStart = Abc_Clock();
+    Vec_Int_t * vMap = Vec_IntAlloc( 100 );
+    Vec_Int_t * vCnts = Vec_IntAlloc( Vec_WrdSize(vFuncs) );
+    Vec_Mem_t * vTtMem = Vec_MemAllocForTTSimple( nVars );
+    int nWords  = Abc_Truth6WordNum(nVars);
+    int nPerms  = Extra_Factorial( nVars );
+    int nMints  = 1 << nVars;
+    int * pPerm = Extra_PermSchedule( nVars );
+    int * pComp = Extra_GreyCodeSchedule( nVars );
+    int m, i, k, t, Entry;
+    word * pCopy = ABC_ALLOC( word, nWords );
+    int nClasses = Vec_WrdSize(vFuncs) / nWords;
+    assert( nClasses * nWords == Vec_WrdSize(vFuncs) );
+    for ( t = 0; t < nClasses; t++ )
+    {
+        word * pTruth = Vec_WrdEntryP( vFuncs, nWords * t );
+        int nFuncs = Vec_MemEntryNum(vTtMem);
+        Abc_TtCopy( pCopy, pTruth, nWords, pTruth[0] & 1 );
+        Vec_MemHashInsert( vTtMem, pCopy );
+        for ( m = 0; m < nMints; m++ ) {
+            Abc_TtFlip( pCopy, nWords, pComp[m] );
+            if ( pCopy[0] & 1 ) {
+                Abc_TtNot( pCopy, nWords );
+                assert( (pCopy[0] & 1) == 0 );
+                Vec_MemHashInsert( vTtMem, pCopy );
+                Abc_TtNot( pCopy, nWords );
+            }
+            else
+                Vec_MemHashInsert( vTtMem, pCopy );
+        }
+        if (  pTruth[0] & 1 )
+            assert( Abc_TtOpposite(pCopy, pTruth, nWords) );
+        else
+            assert( Abc_TtEqual(pCopy, pTruth, nWords) );
+        int nFuncs2 = Vec_MemEntryNum(vTtMem);
+        for ( i = nFuncs; i < nFuncs2; i++ ) {
+            Abc_TtCopy( pCopy, Vec_MemReadEntry(vTtMem, i), nWords, 0 );
+            for ( k = 0; k < nPerms; k++ ) {
+                Abc_TtSwapAdjacent( pCopy, nWords, pPerm[k] );
+                assert( (pCopy[0] & 1) == 0 );
+                Vec_MemHashInsert( vTtMem, pCopy );
+            }        
+            assert( Abc_TtEqual(pCopy, Vec_MemReadEntry(vTtMem, i), nWords) );
+        }
+        for ( i = nFuncs; i < Vec_MemEntryNum(vTtMem); i++ )
+            Vec_IntPush( vMap, t );
+        Vec_IntPush( vCnts, Vec_MemEntryNum(vTtMem) - nFuncs );
+    }
+    ABC_FREE( pCopy );
+    ABC_FREE( pPerm );    
+    ABC_FREE( pComp );
+    if ( fVerbose ) {
+        int Lim = Abc_MinInt( Vec_IntSize(vCnts), 7 );
+        printf( "Collected %d", Vec_MemEntryNum(vTtMem) );
+        Vec_IntForEachEntryStop( vCnts, Entry, i, Lim )
+            printf( " %c %d", i ? '+' : '=', Entry );
+        if ( Vec_IntSize(vCnts) > Lim )
+            printf( " + ..." );
+        printf( " NPN class members.  " );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); 
+        fflush(stdout);
+    }
+    Vec_IntFree( vCnts );
+    if ( pvMap )
+        *pvMap = vMap;
+    else
+        Vec_IntFree( vMap );
+    return vTtMem;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Canonicize a set of functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dau_CanonicizeArray( Vec_Wrd_t * vFuncs, int nVars, int fVerbose )
+{
+    abctime clkStart  = Abc_Clock();
+    extern unsigned Abc_TtCanonicizeCA(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres);
+    if ( fVerbose )   printf( "Functions: %d (original) ", Vec_WrdSize(vFuncs) );
+    unsigned uCanonPhase; char pCanonPerm[16]; word Func; int i;
+    Vec_WrdUniqify( vFuncs );
+
+    if ( fVerbose )   printf( "-> %d (unique) ", Vec_WrdSize(vFuncs) );
+    Vec_WrdForEachEntry( vFuncs, Func, i ) {
+        uCanonPhase = Abc_TtCanonicize( &Func, nVars, pCanonPerm );
+        Vec_WrdWriteEntry( vFuncs, i, Func );
+    }
+    Vec_WrdUniqify( vFuncs );
+    if ( fVerbose )   printf( "-> %d (approx NPN) ", Vec_WrdSize(vFuncs) );
+	Abc_TtHieMan_t * pMan = Abc_TtHieManStart(nVars, 5);
+    Vec_WrdForEachEntry( vFuncs, Func, i ) {
+        uCanonPhase = Abc_TtCanonicizeWrap(Abc_TtCanonicizeCA, pMan, &Func, nVars, pCanonPerm, 1);
+        Vec_WrdWriteEntry( vFuncs, i, Func );
+    }
+    Vec_WrdUniqify( vFuncs );
+    if ( fVerbose )   printf( "-> %d (exact NPN).  ", Vec_WrdSize(vFuncs) );
+	Abc_TtHieManStop(pMan);
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
+    fflush( stdout );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/opt/fxu/fxuReduce.c

@@ -84,6 +84,8 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
                 nBitsMax = nFanins;
         }
     assert( iPair == nPairsTotal );
+    if ( nBitsMax == -1 )
+        nBitsMax = 0;
 
     // allocate storage for counters of cube pairs by difference
     pnPairCounters = ABC_CALLOC( int, 2 * nBitsMax );

src/proof/cec/cecCorr.c

@@ -1320,8 +1320,12 @@ Vec_Int_t * Gia_ManFindStopFlops( Gia_Man_t * p, int nFlopIncFreq, int fVerbose
         if ( Spot >= 0 && Vec_IntEntry(vAvail, i) == 0 )
             Vec_IntPush( vHeads, i );
     Vec_IntForEachEntry( vHeads, Spot, i ) {
-        for ( k = 0, Temp = Spot; Vec_IntEntry(vNexts, Temp) >= 0; k++, Temp = Vec_IntEntry(vNexts, Temp) )
-            ;
+        Vec_IntFill( vAvail, Gia_ManRegNum(p), 0 );
+        for ( k = 0, Temp = Spot; Vec_IntEntry(vNexts, Temp) >= 0; k++, Temp = Vec_IntEntry(vNexts, Temp) ) {
+            if ( Vec_IntEntry(vAvail, Temp) )
+                break;
+            Vec_IntWriteEntry( vAvail, Temp, 1 );
+        }
         if ( k > 100 )
         {
             nItems++;

src/sat/bmc/bmc.h

@@ -62,6 +62,7 @@ struct Bmc_EsPar_t_
     int        fFewerVars;
     int        fQuadrEnc;
     int        fUniqFans;
+    int        fLutCascade;
     int        RuntimeLim;
     int        fVerbose; 
     char *     pTtStr;
@@ -84,7 +85,8 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
     pPars->fEnumSols   = 0; 
     pPars->fFewerVars  = 0; 
     pPars->fQuadrEnc   = 0; 
-    pPars->fUniqFans   = 0; 
+    pPars->fUniqFans   = 0;
+    pPars->fLutCascade = 0;
     pPars->RuntimeLim  = 0;
     pPars->fVerbose    = 1; 
 }

src/sat/bmc/bmcMaj.c

@@ -24,6 +24,8 @@
 #include "sat/glucose/AbcGlucose.h"
 #include "aig/miniaig/miniaig.h"
 #include "base/io/ioResub.h"
+#include "base/main/main.h"
+#include "base/cmd/cmd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -1045,6 +1047,23 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
     // assign connectivity variables
     for ( i = p->nVars; i < p->nObjs; i++ )
     {
+        if ( p->pPars->fLutCascade )
+        {
+            if ( i > p->nVars ) 
+            {
+                Vec_WecPush( p->vOutLits, i-1, Abc_Var2Lit(p->iVar, 0) );
+                p->VarMarks[i][0][i-1] = p->iVar++;
+            }
+            for ( k = (int)(i > p->nVars); k < p->nLutSize; k++ )
+            {
+                for ( j = 0; j < p->nVars - k + (int)(i > p->nVars); j++ )
+                {
+                    Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
+                    p->VarMarks[i][k][j] = p->iVar++;
+                }
+            }
+            continue;
+        }        
         for ( k = 0; k < p->nLutSize; k++ )
         {
             if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 )
@@ -1209,6 +1228,61 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
+{
+    int i, k, b, iVar;
+    char pFileName[1000];
+    sprintf( pFileName, "%s.blif", p->pPars->pTtStr );
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL ) return;
+    fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() );
+    fprintf( pFile, ".model %s\n", p->pPars->pTtStr );
+    fprintf( pFile, ".inputs" );
+    for ( k = 0; k < p->nVars; k++ )
+        fprintf( pFile, " %c", 'a'+k );
+    fprintf( pFile, "\n.outputs F\n" );    
+    for ( i = p->nObjs - 1; i >= p->nVars; i-- )
+    {
+        fprintf( pFile, ".names" );
+        for ( k = 0; k < p->nLutSize; k++ )
+        {
+            iVar = Exa3_ManFindFanin( p, i, k );
+            if ( iVar >= 0 && iVar < p->nVars )
+                fprintf( pFile, " %c", 'a'+iVar );
+            else
+                fprintf( pFile, " %02d", iVar );
+        }
+        if ( i == p->nObjs - 1 )
+            fprintf( pFile, " F\n" );
+        else 
+            fprintf( pFile, " %02d\n", i );
+        int iVarStart = 1 + p->LutMask*(i - p->nVars);
+        for ( k = 0; k < p->LutMask; k++ )
+        {
+            int Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+k); 
+            if ( Val == 0 )
+                continue;
+            for ( b = 0; b < p->nLutSize; b++ )
+                fprintf( pFile, "%d", ((k+1) >> b) & 1 );
+            fprintf( pFile, " %d\n", i != p->nObjs - 1 || !fCompl );
+        }
+    }
+    fprintf( pFile, ".end\n\n" );
+    fclose( pFile );
+    printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
+}
+
 
 /**Function*************************************************************
 
@@ -1464,8 +1538,10 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
     else 
         printf( "The problem has no solution.\n" );
     printf( "Added = %d.  Tried = %d.  ", p->nUsed[1], p->nUsed[0] );
-    Exa3_ManFree( p );
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
+    if ( iMint == -1 )
+        Exa3_ManDumpBlif( p, fCompl );
+    Exa3_ManFree( p );
 }
 
 /**Function*************************************************************
@@ -3916,6 +3992,62 @@ void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize )
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Exa_NpnCascadeTest()
+{
+    char Buffer[100];
+    char Command[1000]; int i;
+    FILE * pFile = fopen( "npn3.txt", "r" );
+    for ( i = 0; i < 14; i++ )
+//    FILE * pFile = fopen( "npn4.txt", "r" );
+//    for ( i = 0; i < 222; i++ )
+//    FILE * pFile = fopen( "npn5.txt", "r" );
+//    for ( i = 0; i < 616126; i++ )
+    {
+        int Value = fscanf( pFile, "%s", Buffer );
+        assert( Value == 1 );
+        if ( i == 0 ) continue;
+        if ( Buffer[strlen(Buffer)-1] == '\n' )
+            Buffer[strlen(Buffer)-1] = '\0';
+        if ( Buffer[strlen(Buffer)-1] == '\r' )
+            Buffer[strlen(Buffer)-1] = '\0';
+        sprintf( Command, "lutexact -I 3 -N 2 -K 2 -gvc %s", Buffer+2 );
+        printf( "\nNPN class %6d : Command \"%s\":\n", i, Command );
+        if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) )
+        {
+            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
+            return;
+        }
+    }
+    fclose( pFile );
+}
+void Exa_NpnCascadeTest6()
+{
+    char Command[1000]; int i;
+    Abc_Random(1);
+    for ( i = 0; i < 10000; i++ ) 
+    {
+        word Truth = Abc_RandomW(0);        
+        sprintf( Command, "lutexact -I 6 -N 2 -K 5 -gvc %016lx", Truth );
+        printf( "\nIter %4d : Command \"%s\":\n", i, Command );
+        if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) )
+        {
+            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
+            return;
+        }
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/sat/bmc/bmcMaj2.c

@@ -944,6 +944,23 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
     // assign connectivity variables
     for ( i = p->nVars; i < p->nObjs; i++ )
     {
+        if ( p->pPars->fLutCascade )
+        {
+            if ( i > p->nVars ) 
+            {
+                Vec_WecPush( p->vOutLits, i-1, Abc_Var2Lit(p->iVar, 0) );
+                p->VarMarks[i][0][i-1] = p->iVar++;
+            }
+            for ( k = (int)(i > p->nVars); k < p->nLutSize; k++ )
+            {
+                for ( j = 0; j < p->nVars - k + (int)(i > p->nVars); j++ )
+                {
+                    Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
+                    p->VarMarks[i][k][j] = p->iVar++;
+                }
+            }
+            continue;
+        }        
         for ( k = 0; k < p->nLutSize; k++ )
         {
             if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 )
@@ -1159,6 +1176,61 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
+{
+    int i, k, b, iVar;
+    char pFileName[1000];
+    sprintf( pFileName, "%s.blif", p->pPars->pTtStr );
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL ) return;
+    fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() );
+    fprintf( pFile, ".model %s\n", p->pPars->pTtStr );
+    fprintf( pFile, ".inputs" );
+    for ( k = 0; k < p->nVars; k++ )
+        fprintf( pFile, " %c", 'a'+k );
+    fprintf( pFile, "\n.outputs F\n" );    
+    for ( i = p->nObjs - 1; i >= p->nVars; i-- )
+    {
+        fprintf( pFile, ".names" );
+        for ( k = 0; k < p->nLutSize; k++ )
+        {
+            iVar = Exa3_ManFindFanin( p, i, k );
+            if ( iVar >= 0 && iVar < p->nVars )
+                fprintf( pFile, " %c", 'a'+iVar );
+            else
+                fprintf( pFile, " %02d", iVar );
+        }
+        if ( i == p->nObjs - 1 )
+            fprintf( pFile, " F\n" );
+        else 
+            fprintf( pFile, " %02d\n", i );
+        int iVarStart = 1 + p->LutMask*(i - p->nVars);
+        for ( k = 0; k < p->LutMask; k++ )
+        {
+            int Val = sat_solver_var_value(p->pSat, iVarStart+k); 
+            if ( Val == 0 )
+                continue;
+            for ( b = 0; b < p->nLutSize; b++ )
+                fprintf( pFile, "%d", ((k+1) >> b) & 1 );
+            fprintf( pFile, " %d\n", i != p->nObjs - 1 || !fCompl );
+        }
+    }
+    fprintf( pFile, ".end\n\n" );
+    fclose( pFile );
+    printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
+}
+
 
 /**Function*************************************************************
 
@@ -1347,8 +1419,10 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars )
     }
     if ( iMint == -1 )
         Exa3_ManPrintSolution( p, fCompl );
-    Exa3_ManFree( p );
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
+    if ( iMint == -1 )
+        Exa3_ManDumpBlif( p, fCompl );
+    Exa3_ManFree( p );
 }
 
 

test.ps

@@ -0,0 +1,388 @@
+%!PS-Adobe-3.0
+%%Creator: graphviz version 2.43.0 (0)
+%%Title: network
+%%Pages: (atend)
+%%BoundingBox: (atend)
+%%EndComments
+save
+%%BeginProlog
+/DotDict 200 dict def
+DotDict begin
+
+/setupLatin1 {
+mark
+/EncodingVector 256 array def
+ EncodingVector 0
+
+ISOLatin1Encoding 0 255 getinterval putinterval
+EncodingVector 45 /hyphen put
+
+% Set up ISO Latin 1 character encoding
+/starnetISO {
+        dup dup findfont dup length dict begin
+        { 1 index /FID ne { def }{ pop pop } ifelse
+        } forall
+        /Encoding EncodingVector def
+        currentdict end definefont
+} def
+/Times-Roman starnetISO def
+/Times-Italic starnetISO def
+/Times-Bold starnetISO def
+/Times-BoldItalic starnetISO def
+/Helvetica starnetISO def
+/Helvetica-Oblique starnetISO def
+/Helvetica-Bold starnetISO def
+/Helvetica-BoldOblique starnetISO def
+/Courier starnetISO def
+/Courier-Oblique starnetISO def
+/Courier-Bold starnetISO def
+/Courier-BoldOblique starnetISO def
+cleartomark
+} bind def
+
+%%BeginResource: procset graphviz 0 0
+/coord-font-family /Times-Roman def
+/default-font-family /Times-Roman def
+/coordfont coord-font-family findfont 8 scalefont def
+
+/InvScaleFactor 1.0 def
+/set_scale {
+       dup 1 exch div /InvScaleFactor exch def
+       scale
+} bind def
+
+% styles
+/solid { [] 0 setdash } bind def
+/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
+/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
+/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
+/bold { 2 setlinewidth } bind def
+/filled { } bind def
+/unfilled { } bind def
+/rounded { } bind def
+/diagonals { } bind def
+/tapered { } bind def
+
+% hooks for setting color 
+/nodecolor { sethsbcolor } bind def
+/edgecolor { sethsbcolor } bind def
+/graphcolor { sethsbcolor } bind def
+/nopcolor {pop pop pop} bind def
+
+/beginpage {	% i j npages
+	/npages exch def
+	/j exch def
+	/i exch def
+	/str 10 string def
+	npages 1 gt {
+		gsave
+			coordfont setfont
+			0 0 moveto
+			(\() show i str cvs show (,) show j str cvs show (\)) show
+		grestore
+	} if
+} bind def
+
+/set_font {
+	findfont exch
+	scalefont setfont
+} def
+
+% draw text fitted to its expected width
+/alignedtext {			% width text
+	/text exch def
+	/width exch def
+	gsave
+		width 0 gt {
+			[] 0 setdash
+			text stringwidth pop width exch sub text length div 0 text ashow
+		} if
+	grestore
+} def
+
+/boxprim {				% xcorner ycorner xsize ysize
+		4 2 roll
+		moveto
+		2 copy
+		exch 0 rlineto
+		0 exch rlineto
+		pop neg 0 rlineto
+		closepath
+} bind def
+
+/ellipse_path {
+	/ry exch def
+	/rx exch def
+	/y exch def
+	/x exch def
+	matrix currentmatrix
+	newpath
+	x y translate
+	rx ry scale
+	0 0 1 0 360 arc
+	setmatrix
+} bind def
+
+/endpage { showpage } bind def
+/showpage { } def
+
+/layercolorseq
+	[	% layer color sequence - darkest to lightest
+		[0 0 0]
+		[.2 .8 .8]
+		[.4 .8 .8]
+		[.6 .8 .8]
+		[.8 .8 .8]
+	]
+def
+
+/layerlen layercolorseq length def
+
+/setlayer {/maxlayer exch def /curlayer exch def
+	layercolorseq curlayer 1 sub layerlen mod get
+	aload pop sethsbcolor
+	/nodecolor {nopcolor} def
+	/edgecolor {nopcolor} def
+	/graphcolor {nopcolor} def
+} bind def
+
+/onlayer { curlayer ne {invis} if } def
+
+/onlayers {
+	/myupper exch def
+	/mylower exch def
+	curlayer mylower lt
+	curlayer myupper gt
+	or
+	{invis} if
+} def
+
+/curlayer 0 def
+
+%%EndResource
+%%EndProlog
+%%BeginSetup
+14 default-font-family set_font
+% /arrowlength 10 def
+% /arrowwidth 5 def
+
+% make sure pdfmark is harmless for PS-interpreters other than Distiller
+/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
+% make '<<' and '>>' safe on PS Level 1 devices
+/languagelevel where {pop languagelevel}{1} ifelse
+2 lt {
+    userdict (<<) cvn ([) cvn load put
+    userdict (>>) cvn ([) cvn load put
+} if
+
+%%EndSetup
+setupLatin1
+%%Page: 1 1
+%%PageBoundingBox: 37 212 575 580
+%%PageOrientation: Portrait
+0 0 1 beginpage
+gsave
+37 212 538 368 boxprim clip newpath
+1 1 set_scale 0 rotate 41 216 translate
+% LevelTitle1
+gsave
+grestore
+% LevelTitle2
+gsave
+grestore
+% LevelTitle1->LevelTitle2
+% Level2
+gsave
+grestore
+% LevelTitle2->Level2
+% Level1
+gsave
+grestore
+% Level2->Level1
+% Level0
+gsave
+grestore
+% Level1->Level0
+% title1
+gsave
+0 0 0 nodecolor
+20 /Times-Roman set_font
+151.5 340 moveto 299 (Network structure visualized by ABC) alignedtext
+0 0 0 nodecolor
+20 /Times-Roman set_font
+80 318 moveto 442 (Benchmark "test". Time was Fri Sep  6 06:13:38 2024. ) alignedtext
+grestore
+% title2
+gsave
+0 0 0 nodecolor
+18 /Times-Roman set_font
+119 249.6 moveto 364 (The network contains 1 logic nodes and 0 latches.) alignedtext
+grestore
+% title1->title2
+% Node4
+gsave
+1 setlinewidth
+0.043137 0.68627 1 nodecolor
+newpath 263 154 moveto
+290.0966 188.5 lineto
+235.9034 188.5 lineto
+closepath stroke
+0 0 0 nodecolor
+14 /Times-Roman set_font
+260.5 173.3 moveto 5 (f) alignedtext
+grestore
+% title2->Node4
+% Node5
+gsave
+1 setlinewidth
+0.043137 0.68627 1 nodecolor
+newpath 338 154 moveto
+367.795 188.5 lineto
+308.205 188.5 lineto
+closepath stroke
+0 0 0 nodecolor
+14 /Times-Roman set_font
+334.5 173.3 moveto 7 (g) alignedtext
+grestore
+% title2->Node5
+% Node4->Node5
+% Node6
+gsave
+1 setlinewidth
+0 0 0 nodecolor
+300 100 27 18 ellipse_path stroke
+0 0 0 nodecolor
+14 /Times-Roman set_font
+296.5 96.3 moveto 7 (6) alignedtext
+grestore
+% Node4->Node6
+gsave
+1 setlinewidth
+solid
+0 0 0 edgecolor
+newpath 274.2701 153.1552 moveto
+279.9849 141.5712 286.7919 127.7731 291.9687 117.2797 curveto
+stroke
+0 0 0 edgecolor
+newpath 271.0718 151.7273 moveto
+269.7864 162.2438 lineto
+277.3495 154.8243 lineto
+closepath fill
+1 setlinewidth
+solid
+0 0 0 edgecolor
+newpath 271.0718 151.7273 moveto
+269.7864 162.2438 lineto
+277.3495 154.8243 lineto
+closepath stroke
+grestore
+% Node5->Node6
+gsave
+1 setlinewidth
+solid
+0 0 0 edgecolor
+newpath 326.2775 152.8634 moveto
+320.4603 141.3822 313.571 127.785 308.3062 117.3939 curveto
+stroke
+0 0 0 edgecolor
+newpath 323.2107 154.5546 moveto
+330.8525 161.8931 lineto
+329.4549 151.3908 lineto
+closepath fill
+1 setlinewidth
+solid
+0 0 0 edgecolor
+newpath 323.2107 154.5546 moveto
+330.8525 161.8931 lineto
+329.4549 151.3908 lineto
+closepath stroke
+grestore
+% Node1
+gsave
+1 setlinewidth
+0.043137 0.68627 1 nodecolor
+newpath 261 46 moveto
+231.205 11.5 lineto
+290.795 11.5 lineto
+closepath stroke
+0 0 0 nodecolor
+14 /Times-Roman set_font
+257.5 19.3 moveto 7 (a) alignedtext
+grestore
+% Node6->Node1
+gsave
+1 setlinewidth
+solid
+0 0 0 edgecolor
+newpath 286.8586 73.7282 moveto
+280.7027 61.8898 273.5973 48.2257 268.3944 38.2199 curveto
+stroke
+0 0 0 edgecolor
+newpath 283.8187 75.4687 moveto
+291.5376 82.7261 lineto
+290.0293 72.2392 lineto
+closepath fill
+1 setlinewidth
+solid
+0 0 0 edgecolor
+newpath 283.8187 75.4687 moveto
+291.5376 82.7261 lineto
+290.0293 72.2392 lineto
+closepath stroke
+grestore
+% Node2
+gsave
+1 setlinewidth
+0.043137 0.68627 1 nodecolor
+newpath 339 46 moveto
+309.205 11.5 lineto
+368.795 11.5 lineto
+closepath stroke
+0 0 0 nodecolor
+14 /Times-Roman set_font
+335.5 19.3 moveto 7 (b) alignedtext
+grestore
+% Node6->Node2
+gsave
+1 setlinewidth
+solid
+0 0 0 edgecolor
+newpath 313.1414 73.7282 moveto
+319.2973 61.8898 326.4027 48.2257 331.6056 38.2199 curveto
+stroke
+0 0 0 edgecolor
+newpath 309.9707 72.2392 moveto
+308.4624 82.7261 lineto
+316.1813 75.4687 lineto
+closepath fill
+1 setlinewidth
+solid
+0 0 0 edgecolor
+newpath 309.9707 72.2392 moveto
+308.4624 82.7261 lineto
+316.1813 75.4687 lineto
+closepath stroke
+grestore
+% Node3
+gsave
+1 setlinewidth
+0.043137 0.68627 1 nodecolor
+newpath 417 46 moveto
+387.205 11.5 lineto
+446.795 11.5 lineto
+closepath stroke
+0 0 0 nodecolor
+14 /Times-Roman set_font
+413.5 19.3 moveto 7 (c) alignedtext
+grestore
+endpage
+showpage
+grestore
+%%PageTrailer
+%%EndPage: 1
+%%Trailer
+%%Pages: 1
+%%BoundingBox: 37 212 575 580
+end
+restore
+%%EOF

test/CMakeLists.txt

@@ -0,0 +1 @@
+add_subdirectory(gia)

test/gia/CMakeLists.txt

@@ -0,0 +1,11 @@
+add_executable(gia_test gia_test.cc)
+
+target_link_libraries(gia_test
+    gtest
+    gtest_main
+    libabc
+)
+
+gtest_discover_tests(gia_test
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)

test/gia/gia_test.cc

@@ -0,0 +1,54 @@
+#include "gtest/gtest.h"
+
+#include "aig/gia/gia.h"
+
+ABC_NAMESPACE_IMPL_START
+
+TEST(GiaTest, CanAllocateGiaManager) {
+  Gia_Man_t* aig_manager =  Gia_ManStart(100);
+
+  EXPECT_TRUE(aig_manager != nullptr);
+  Gia_ManStop(aig_manager);
+}
+
+TEST(GiaTest, CanAddACi) {
+  Gia_Man_t* aig_manager =  Gia_ManStart(100);
+  Gia_ManAppendCi(aig_manager);
+
+  EXPECT_EQ(Gia_ManCiNum(aig_manager), 1);
+  Gia_ManStop(aig_manager);
+}
+
+TEST(GiaTest, CanAddACo) {
+  Gia_Man_t* aig_manager =  Gia_ManStart(100);
+  int input1 = Gia_ManAppendCi(aig_manager);
+  Gia_ManAppendCo(aig_manager, input1);
+
+  EXPECT_EQ(Gia_ManCiNum(aig_manager), 1);
+  EXPECT_EQ(Gia_ManCoNum(aig_manager), 1);
+  Gia_ManStop(aig_manager);
+}
+
+TEST(GiaTest, CanAddAnAndGate) {
+  Gia_Man_t* aig_manager =  Gia_ManStart(100);
+
+  int input1 = Gia_ManAppendCi(aig_manager);
+  int input2 = Gia_ManAppendCi(aig_manager);
+
+  int and_output = Gia_ManAppendAnd(aig_manager, input1, input2);
+  Gia_ManAppendCo(aig_manager, and_output);
+
+  Vec_Wrd_t* stimulus = Vec_WrdAlloc(2);
+  Vec_WrdPush(stimulus, /*A*/1);
+  Vec_WrdPush(stimulus, /*B*/1);
+  Vec_Wrd_t* output = Gia_ManSimPatSimOut(aig_manager, stimulus, /*fouts*/1);
+
+  EXPECT_EQ(Gia_ManCiNum(aig_manager), 2);
+  EXPECT_EQ(Gia_ManCoNum(aig_manager), 1);
+  // A = 1, B = 1 -> A & B == 1
+  EXPECT_EQ(Vec_WrdGetEntry(output, 0), 1);
+  Vec_WrdFree(output);
+  Gia_ManStop(aig_manager);
+}
+
+ABC_NAMESPACE_IMPL_END