Version abc51222

20 files changed, 914 insertions, 60 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e43ee31b..e0a27f9a 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -209,8 +209,9 @@ struct Abc_Ntk_t_
 #define ABC_INFINITY      (10000000)
 
 // transforming floats into ints and back
-static inline int         Abc_Float2Int( float Val )                 { return *((int *)&Val);           }
-static inline float       Abc_Int2Float( int Num )                   { return *((float *)&Num);         }
+static inline int         Abc_Float2Int( float Val )                 { return *((int *)&Val);               }
+static inline float       Abc_Int2Float( int Num )                   { return *((float *)&Num);             }
+static inline int         Abc_BitWordNum( int nBits )                { return nBits/32 + ((nBits%32) > 0);  }
 
 // checking the network type
 static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )       { return pNtk->ntkType == ABC_NTK_NETLIST; }
@@ -570,7 +571,7 @@ extern void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
 extern void               Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
 extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
-extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile );
+extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
 extern void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
 /*=== abcReconv.c ==========================================================*/
 extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
@@ -600,12 +601,13 @@ extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int n
 extern char *             Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
-extern char *             Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars );
+extern char *             Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
 extern char *             Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
 extern char *             Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
 extern char *             Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
+extern char *             Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateInv( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 742c8c8d..2ab3842f 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -93,27 +93,41 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
     DdNode * bSum, * bCube, * bTemp, * bVar;
     char * pCube;
     int nVars, Value, v;
+    extern int Abc_SopIsExorType( char * pSop );
+
     // start the cover
     nVars = Abc_SopGetVarNum(pSop);
-    // check the logic function of the node
     bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
-    Abc_SopForEachCube( pSop, nVars, pCube )
+    if ( Abc_SopIsExorType(pSop) )
+    {
+        for ( v = 0; v < nVars; v++ )
+        {
+            bSum  = Cudd_bddXor( dd, bTemp = bSum, Cudd_bddIthVar(dd, v) );   Cudd_Ref( bSum );
+            Cudd_RecursiveDeref( dd, bTemp );
+        }
+    }
+    else
     {
-        bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
-        Abc_CubeForEachVar( pCube, Value, v )
+        // check the logic function of the node
+        Abc_SopForEachCube( pSop, nVars, pCube )
         {
-            if ( Value == '0' )
-                bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
-            else if ( Value == '1' )
-                bVar = Cudd_bddIthVar( dd, v );
-            else
-                continue;
-            bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
+            bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
+            Abc_CubeForEachVar( pCube, Value, v )
+            {
+                if ( Value == '0' )
+                    bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
+                else if ( Value == '1' )
+                    bVar = Cudd_bddIthVar( dd, v );
+                else
+                    continue;
+                bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
+                Cudd_RecursiveDeref( dd, bTemp );
+            }
+            bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   
+            Cudd_Ref( bSum );
             Cudd_RecursiveDeref( dd, bTemp );
+            Cudd_RecursiveDeref( dd, bCube );
         }
-        bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   Cudd_Ref( bSum );
-        Cudd_RecursiveDeref( dd, bTemp );
-        Cudd_RecursiveDeref( dd, bCube );
     }
     // complement the result if necessary
     bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) );
@@ -246,16 +260,18 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) );
     if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) )
     {
+        if ( fMode == -1 ) // if the phase is not known, write constant 1
+            fMode = 1;
         Vec_StrFill( vCube, nFanins, '-' );
         Vec_StrPush( vCube, '\0' );
         if ( pMan )
             pSop = Extra_MmFlexEntryFetch( pMan, nFanins + 4 );
         else
             pSop = ALLOC( char, nFanins + 4 );
-        if ( bFuncOn == Cudd_ReadLogicZero(dd) )
-            sprintf( pSop, "%s 0\n", vCube->pArray );
+        if ( bFuncOn == Cudd_ReadOne(dd) )
+            sprintf( pSop, "%s %d\n", vCube->pArray, fMode );
         else
-            sprintf( pSop, "%s 1\n", vCube->pArray );
+            sprintf( pSop, "%s %d\n", vCube->pArray, !fMode );
         return pSop;
     }
 
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 53f8c1e9..65cc6e2e 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -342,7 +342,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
         if ( !Abc_NodeIsConst(pObj) )
         {
             Abc_NtkDupObj( pNtkNew, pObj );
-            pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2 );
+            pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2, NULL );
         }
         if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
             pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index dc69f651..4152dd0a 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -156,13 +156,14 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars )
+char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
 {
     char * pSop;
     int i;
     pSop = Abc_SopStart( pMan, 1, nVars );
     for ( i = 0; i < nVars; i++ )
-        pSop[i] = '1';
+        pSop[i] = '1' - (pfCompl? pfCompl[i] : 0);
+    pSop[nVars + 1] = '1';
     return pSop;
 }
 
@@ -275,6 +276,26 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
+  Synopsis    [Starts the multi-input XOR cover (special case).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars )
+{
+    char * pSop;
+    pSop = Abc_SopCreateAnd( pMan, nVars, NULL );
+    pSop[nVars+1] = 'x';
+    assert( pSop[nVars+2] == '\n' );
+    return pSop;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Starts the multi-input XNOR cover.]
 
   Description []
@@ -402,9 +423,9 @@ int Abc_SopGetVarNum( char * pSop )
 int Abc_SopGetPhase( char * pSop )
 {
     int nVars = Abc_SopGetVarNum( pSop );
-    if ( pSop[nVars+1] == '0' )
+    if ( pSop[nVars+1] == '0' || pSop[nVars+1] == 'n' )
         return 0;
-    if ( pSop[nVars+1] == '1' )
+    if ( pSop[nVars+1] == '1' || pSop[nVars+1] == 'x' )
         return 1;
     assert( 0 );
     return -1;
@@ -453,6 +474,10 @@ void Abc_SopComplement( char * pSop )
                 *(pCur - 1) = '1';
             else if ( *(pCur - 1) == '1' )
                 *(pCur - 1) = '0';
+            else if ( *(pCur - 1) == 'x' )
+                *(pCur - 1) = 'n';
+            else if ( *(pCur - 1) == 'n' )
+                *(pCur - 1) = 'x';
             else
                 assert( 0 );
         }
@@ -474,7 +499,7 @@ bool Abc_SopIsComplement( char * pSop )
     char * pCur;
     for ( pCur = pSop; *pCur; pCur++ )
         if ( *pCur == '\n' )
-            return (int)(*(pCur - 1) == '0');
+            return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n');
     assert( 0 );
     return 0;
 }
@@ -616,6 +641,27 @@ bool Abc_SopIsOrType( char * pSop )
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_SopIsExorType( char * pSop )
+{
+    char * pCur;
+    for ( pCur = pSop; *pCur; pCur++ )
+        if ( *pCur == '\n' )
+            return (int)(*(pCur - 1) == 'x' || *(pCur - 1) == 'n');
+    assert( 0 );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 bool Abc_SopCheck( char * pSop, int nFanins )
 {
     char * pCubes, * pCubesOld;
@@ -638,7 +684,7 @@ bool Abc_SopCheck( char * pSop, int nFanins )
             fFound0 = 1;
         else if ( *pCubes == '1' )
             fFound1 = 1;
-        else
+        else if ( *pCubes != 'x' && *pCubes != 'n' )
         {
             fprintf( stdout, "Abc_SopCheck: SOP has a strange character in the output part of its cube.\n" );
             return 0;
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 8e1615d7..9d95fade 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -76,6 +76,8 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk )
     assert( Abc_NtkHasSop(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
         assert( pNode->pData );
         nCubes += Abc_SopGetCubeNum( pNode->pData );
     }
@@ -153,6 +155,8 @@ int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsBddLogic(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
         assert( pNode->pData );
         nNodes += pNode->pData? Cudd_DagSize( pNode->pData ) : 0;
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b6de6cbf..71b76cf6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -77,6 +77,7 @@ static int Abc_CommandExdcFree     ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandExdcGet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcSet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCut          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandXyz          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -173,6 +174,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "exdc_get",      Abc_CommandExdcGet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_set",      Abc_CommandExdcSet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
+    Cmd_CommandAdd( pAbc, "Various",      "xyz",           Abc_CommandXyz,              1 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
@@ -648,6 +650,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pNode;
     int c;
+    int fListNodes;
     int fProfile;
 
     pNtk = Abc_FrameReadNet(pAbc);
@@ -655,12 +658,16 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fProfile = 1;
+    fListNodes = 0;
+    fProfile   = 1;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "ph" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "nph" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'n':
+            fListNodes ^= 1;
+            break;
         case 'p':
             fProfile ^= 1;
             break;
@@ -701,12 +708,13 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     // process all COs
-    Abc_NtkPrintLevel( pOut, pNtk, fProfile );
+    Abc_NtkPrintLevel( pOut, pNtk, fProfile, fListNodes );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_level [-ph] <node>\n" );
+    fprintf( pErr, "usage: print_level [-nph] <node>\n" );
     fprintf( pErr, "\t        prints information about node level and cone size\n" );
+    fprintf( pErr, "\t-n    : toggles printing nodes by levels [default = %s]\n", fListNodes? "yes": "no" );
     fprintf( pErr, "\t-p    : toggles printing level profile [default = %s]\n", fProfile? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     fprintf( pErr, "\tnode  : (optional) one node to consider\n");
@@ -732,6 +740,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fVerbose;
     extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
+    extern void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -759,6 +768,11 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+
+    // print support information
+    Abc_NtkPrintStrSupports( pNtk );
+    return 0;
+
     if ( !Abc_NtkIsComb(pNtk) )
     {
         fprintf( pErr, "This command works only for combinational networks.\n" );
@@ -3649,11 +3663,102 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
+    int fVerbose;
+    int fUseInvs;
+    int nFaninMax;
+    extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 0;
+    fUseInvs = 1;
+    nFaninMax = 128;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "Nivh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFaninMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nFaninMax < 0 ) 
+                goto usage;
+            break;
+        case 'i':
+            fUseInvs ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Only works for strashed networks.\n" );
+        return 1;
+    }
+
+    // run the command
+    pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: xyz [-N num] [-ivh]\n" );
+    fprintf( pErr, "\t         specilized AND/OR/EXOR decomposition\n" );
+    fprintf( pErr, "\t-N num : maximum number of inputs [default = %d]\n", nFaninMax );
+    fprintf( pErr, "\t-i     : toggle the use of interters [default = %s]\n", fUseInvs? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;//, * pNtkRes;
+    int c;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3676,6 +3781,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Only works for strashed networks.\n" );
+        return 1;
+    }
+
+//    Abc_NtkDeriveEsops( pNtk );
+//    Abc_NtkXyz( pNtk, 128, 0, 0, 0 );
+    printf( "This command is currently not used.\n" );
+
+/*
     // run the command
     pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
     if ( pNtkRes == NULL )
@@ -3685,6 +3802,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+*/
     return 0;
 
 usage:
@@ -3696,7 +3814,6 @@ usage:
 
 
 
-
 /**Function*************************************************************
 
   Synopsis    []
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 1adbfef7..fed89dbb 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -102,6 +102,42 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
 
 /**Function*************************************************************
 
+  Synopsis    [Randomizes the node positions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeBalanceRandomize( Vec_Ptr_t * vSuper )
+{
+    Abc_Obj_t * pNode1, * pNode2;
+    int i, Signature;
+    if ( Vec_PtrSize(vSuper) < 3 )
+        return;
+    pNode1 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-2 );
+    pNode2 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-3 );
+    if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level )
+        return;
+    // some reordering will be performed
+    Signature = rand();
+    for ( i = Vec_PtrSize(vSuper)-2; i > 0; i-- )
+    {
+        pNode1 = Vec_PtrEntry( vSuper, i );
+        pNode2 = Vec_PtrEntry( vSuper, i-1 );
+        if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level )
+            return;
+        if ( Signature & (1 << (i % 10)) )
+            continue;
+        Vec_PtrWriteEntry( vSuper, i,   pNode2 );
+        Vec_PtrWriteEntry( vSuper, i-1, pNode1 );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Rebalances the multi-input node rooted at pNodeOld.]
 
   Description []
@@ -143,6 +179,9 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
     assert( vSuper->nSize > 1 );
     while ( vSuper->nSize > 1 )
     {
+        // randomize the node positions
+//        Abc_NodeBalanceRandomize( vSuper );
+        // pull out the last two nodes
         pNode1 = Vec_PtrPop(vSuper);
         pNode2 = Vec_PtrPop(vSuper);
         Abc_VecObjPushUniqueOrderByLevel( vSuper, Abc_AigAnd(pMan, pNode1, pNode2) );
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index bfc992ef..d59f21a0 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -56,7 +56,7 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int f
 {
     Fraig_Params_t * pPars = pParams;
     Abc_Ntk_t * pNtkNew;
-    Fraig_Man_t * pMan;
+    Fraig_Man_t * pMan; 
     // check if EXDC is present
     if ( fExdc && pNtk->pExdc == NULL )
         fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 82325619..6791f08c 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -79,7 +79,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
             fprintf( pFile, "  lit(fac) = %5d",  Abc_NtkGetLitFactNum(pNtk) );
     }
     else if ( Abc_NtkHasBdd(pNtk) )
-        fprintf( pFile, "  bdd = %5d",  Abc_NtkGetBddNodeNum(pNtk) );
+        fprintf( pFile, "  bdd  = %5d",  Abc_NtkGetBddNodeNum(pNtk) );
     else if ( Abc_NtkHasMapping(pNtk) )
     {
         fprintf( pFile, "  area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
@@ -423,10 +423,26 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
+void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes )
 {
     Abc_Obj_t * pNode;
-    int i, Length;
+    int i, k, Length;
+
+    if ( fListNodes )
+    {
+        int nLevels;
+        nLevels = Abc_NtkGetLevelNum(pNtk);
+        printf( "Nodes by level:\n" );
+        for ( i = 0; i <= nLevels; i++ )
+        {
+            printf( "%2d : ", i );
+            Abc_NtkForEachNode( pNtk, pNode, k )
+                if ( (int)pNode->Level == i )
+                    printf( " %s", Abc_ObjName(pNode) );
+            printf( "\n" );
+        }
+        return;
+    }
 
     // print the delay profile
     if ( fProfile && Abc_NtkHasMapping(pNtk) )
@@ -716,6 +732,34 @@ void Abc_NtkPrintSharing( Abc_Ntk_t * pNtk )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints info for each output cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vSupp, * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+    printf( "Structural support info:\n" );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        vSupp  = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+        vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+        printf( "%20s :  Cone = %5d.  Supp = %5d.\n", 
+            Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vSupp );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index ab594667..b3b30d9a 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -109,6 +109,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
     // print stats
     if ( fVerbose )
         Rwr_ManPrintStats( pManRwr );
+//        Rwr_ManPrintStatsFile( pManRwr );
     // delete the managers
     Rwr_ManStop( pManRwr );
     Cut_ManStop( pManCut );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 1a35d143..4a65659c 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -24,8 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
-static void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
+static int  Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
+static int  Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -57,6 +57,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
     // load clauses into the solver
     clk = clock();
     pSat = Abc_NtkMiterSatCreate( pNtk );
+    if ( pSat == NULL )
+        return 1;
 //    printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
 
@@ -69,7 +71,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
     {
         solver_delete( pSat );
 //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
-        return -1;
+        return 1;
     }
 
     // solve the miter
@@ -143,13 +145,19 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
         // derive SOPs for both phases of the node
         Abc_NodeBddToCnf( pNode, pMmFlex, vCube, &pSop0, &pSop1 );
         // add the clauses to the solver
-        Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars );
+        if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) )
+        {
+            solver_delete( pSat );
+            return NULL;
+        }
     }
-    // add clauses for each PO
-//    Abc_NtkForEachPo( pNtk, pNode, i )
-//        Abc_NodeAddClausesTop( pSat, pNode, vVars );
-
-    Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars );
+    // add clauses for the POs
+    if ( !Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars ) )
+    {
+        solver_delete( pSat );
+        return NULL;
+    }
+//    Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 );
 
     // delete
     Vec_StrFree( vCube );
@@ -169,7 +177,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
     Abc_Obj_t * pFanin;
     int i, c, nFanins;
@@ -177,6 +185,16 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
 
     nFanins = Abc_ObjFaninNum( pNode );
     assert( nFanins == Abc_SopGetVarNum( pSop0 ) );
+
+    if ( nFanins == 0 )
+    {
+        vVars->nSize = 0;
+        if ( Abc_SopIsConst1(pSop1) )
+            Vec_IntPush( vVars, toLit(pNode->Id) );
+        else
+            Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    }
  
     // add clauses for the negative phase
     for ( c = 0; ; c++ )
@@ -195,7 +213,8 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
                 Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
         }
         Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
     }
 
     // add clauses for the positive phase
@@ -215,8 +234,10 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
                 Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
         }
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
     }
+    return 1;
 }
 
 /**Function*************************************************************
@@ -230,7 +251,7 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
     Abc_Obj_t * pFanin;
 
@@ -240,29 +261,33 @@ void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars
         vVars->nSize = 0;
         Vec_IntPush( vVars, toLit(pFanin->Id) );
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
 
         vVars->nSize = 0;
         Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
         Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
     }
     else
     {
         vVars->nSize = 0;
         Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
         Vec_IntPush( vVars, toLit(pNode->Id) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
 
         vVars->nSize = 0;
         Vec_IntPush( vVars, toLit(pFanin->Id) );
         Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
-        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+            return 0;
     }
 
     vVars->nSize = 0;
     Vec_IntPush( vVars, toLit(pNode->Id) );
-    solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
 
 
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index d1734d88..72f4215b 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -29,6 +29,7 @@
 // static functions
 static void        Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes );
 static Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
+static Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
 static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
 
 extern char *      Mio_GateReadSop( void * pGate );
@@ -182,6 +183,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
 {
     int fUseFactor = 1;
     char * pSop;
+    extern int Abc_SopIsExorType( char * pSop );
 
     assert( Abc_ObjIsNode(pNode) );
 
@@ -203,6 +205,10 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
     if ( Abc_NodeIsConst(pNode) )
         return Abc_ObjNotCond( Abc_NtkConst1(pNtkNew), Abc_SopIsConst0(pSop) );
 
+    // consider the special case of EXOR function
+    if ( Abc_SopIsExorType(pSop) )
+        return Abc_NodeStrashExor( pNtkNew, pNode, pSop );
+
     // decide when to use factoring
     if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
         return Abc_NodeStrashFactor( pNtkNew, pNode, pSop );
@@ -254,6 +260,37 @@ Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pS
 
 /**Function*************************************************************
 
+  Synopsis    [Strashed n-input XOR function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop )
+{
+    Abc_Aig_t * pMan = pNtkNew->pManFunc;
+    Abc_Obj_t * pFanin, * pSum;
+    int i, nFanins;
+    // get the number of node's fanins
+    nFanins = Abc_ObjFaninNum( pNode );
+    assert( nFanins == Abc_SopGetVarNum(pSop) );
+    // go through the cubes of the node's SOP
+    pSum = Abc_ObjNot( Abc_NtkConst1(pNtkNew) );
+    for ( i = 0; i < nFanins; i++ )
+    {
+        pFanin = Abc_ObjFanin( pNode, i );
+        pSum = Abc_AigXor( pMan, pSum, pFanin->pCopy );
+    }
+    if ( Abc_SopIsComplement(pSop) )
+        pSum = Abc_ObjNot(pSum);
+    return pSum;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Strashes one logic node using its SOP.]
 
   Description []
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index bbaca5a9..f20855ab 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1245,6 +1245,12 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
     fclose( pFile );
 
+    if ( Abc_NtkIsMappedLogic(pNtk) )
+    {
+        Abc_NtkUnmap(pNtk);
+        printf( "The current network is unmapped before calling SIS.\n" );
+    }
+
     // write out the current network
     pNetlist = Abc_NtkLogicToNetlist(pNtk);
     Io_WriteBlif( pNetlist, "_sis_in.blif", 1 );
@@ -1375,6 +1381,11 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
     fclose( pFile );
 
+    if ( Abc_NtkIsMappedLogic(pNtk) )
+    {
+        Abc_NtkUnmap(pNtk);
+        printf( "The current network is unmapped before calling MVSIS.\n" );
+    }
 
     // write out the current network
     pNetlist = Abc_NtkLogicToNetlist(pNtk);
diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c
index 2f74c2a5..9b7fb49f 100644
--- a/src/base/cmd/cmdUtils.c
+++ b/src/base/cmd/cmdUtils.c
@@ -245,7 +245,7 @@ int CmdApplyAlias( Abc_Frame_t * pAbc, int *argcp, char ***argvp, int *loop )
     argc = *argcp;
     argv = *argvp;
     stopit = 0;
-    for ( ; *loop < 20; ( *loop )++ )
+    for ( ; *loop < 200; ( *loop )++ )
     {
         if ( argc == 0 )
             return 0;
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 1330d114..69b60000 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -44,6 +44,7 @@ static int IoCommandWriteEqn    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteGml    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteList   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -81,6 +82,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_gml",     IoCommandWriteGml,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_list",    IoCommandWriteList,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_pla",     IoCommandWritePla,     0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
 }
 
 /**Function*************************************************************
@@ -1383,6 +1385,69 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+    char * FileName;
+    int c;
+
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    pNtk = pAbc->pNtkCur;
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
+
+    if ( argc != util_optind + 1 )
+    {
+        goto usage;
+    }
+    // get the input file name
+    FileName = argv[util_optind];
+
+    // derive the netlist
+    pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+    if ( pNtkTemp == NULL )
+    {
+        fprintf( pAbc->Out, "Writing PLA has failed.\n" );
+        return 0;
+    }
+    Io_WriteVerilog( pNtkTemp, FileName );
+    Abc_NtkDelete( pNtkTemp );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_verilog [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         write a very special subset of Verilog\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/io.h b/src/base/io/io.h
index cb8678b3..286b570c 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -90,6 +90,8 @@ extern void               Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName );
 extern void               Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost );
 /*=== abcWritePla.c ==========================================================*/
 extern int                Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
+/*=== abcWriteVerilog.c ==========================================================*/
+extern void               Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 510167a8..d8ad8f71 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -127,7 +127,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                 pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, nNames );
                 // assign the cover
                 if ( strcmp(pType, "AND") == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopCreateAnd(pNtk->pManFunc, nNames) );
+                    Abc_ObjSetData( pNode, Abc_SopCreateAnd(pNtk->pManFunc, nNames, NULL) );
                 else if ( strcmp(pType, "OR") == 0 )
                     Abc_ObjSetData( pNode, Abc_SopCreateOr(pNtk->pManFunc, nNames, NULL) );
                 else if ( strcmp(pType, "NAND") == 0 )
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index e23bfdb7..b8a2ed01 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -504,7 +504,7 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
             Vec_StrAppend( p->vCubes, vTokens->pArray[0] );
             // check the char 
             Char = ((char *)vTokens->pArray[1])[0];
-            if ( Char != '0' && Char != '1' )
+            if ( Char != '0' && Char != '1' && Char != 'x' && Char != 'n' )
             {
                 p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
                 sprintf( p->sError, "The output character in the constant cube is wrong." );
diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c
index 63345fd7..a2a2f527 100644
--- a/src/base/io/ioReadEdif.c
+++ b/src/base/io/ioReadEdif.c
@@ -191,7 +191,7 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         if ( strncmp( pObj->pData, "And", 3 ) == 0 )
-            Abc_ObjSetData( pObj, Abc_SopCreateAnd(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+            Abc_ObjSetData( pObj, Abc_SopCreateAnd(pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
         else if ( strncmp( pObj->pData, "Or", 2 ) == 0 )
             Abc_ObjSetData( pObj, Abc_SopCreateOr(pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
         else if ( strncmp( pObj->pData, "Nand", 4 ) == 0 )
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
new file mode 100644
index 00000000..f56da052
--- /dev/null
+++ b/src/base/io/ioWriteVerilog.c
@@ -0,0 +1,445 @@
+/**CFile****************************************************************
+
+  FileName    [ioWriteVerilog.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to output a special subset of Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteVerilog.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk );
+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_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros );
+static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
+static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Write verilog.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    FILE * pFile;
+
+    if ( !Abc_NtkIsSopNetlist(pNtk) || !Io_WriteVerilogCheckNtk(pNtk) )
+    {
+        printf( "Io_WriteVerilog(): Can write Verilog for a very special subset of logic networks.\n" );
+        printf( "The current network is not in the subset; writing Verilog is not performed.\n" );
+        return;
+    }
+
+    if ( Abc_NtkLatchNum(pNtk) > 0 )
+        printf( "Io_WriteVerilog(): Warning: only combinational portion is being written.\n" );
+
+    // start the output stream
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+
+    // write the equations for the network
+    Io_WriteVerilogInt( pFile, pNtk );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes verilog.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    // write inputs and outputs
+    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+    fprintf( pFile, "module %s (\n   ", Abc_NtkName(pNtk) );
+    Io_WriteVerilogPis( pFile, pNtk, 3 );
+    fprintf( pFile, ",\n   " );
+    Io_WriteVerilogPos( pFile, pNtk, 3 );
+    fprintf( pFile, "  );\n" );
+    // write inputs, outputs and wires
+    fprintf( pFile, "  input" );
+    Io_WriteVerilogPis( pFile, pNtk, 5 );
+    fprintf( pFile, ";\n" );
+    fprintf( pFile, "  output" );
+    Io_WriteVerilogPos( pFile, pNtk, 5 );
+    fprintf( pFile, ";\n" );
+    fprintf( pFile, "  wire" );
+    Io_WriteVerilogWires( pFile, pNtk, 4 );
+    fprintf( pFile, ";\n" );
+    // write the nodes
+    Io_WriteVerilogNodes( pFile, pNtk );
+    // finalize the file
+    fprintf( pFile, "endmodule\n\n" );
+    fclose( pFile );
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachCi( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanout0(pTerm);
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkCiNum(pNtk)-1)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachCo( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanin0(pTerm);
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkCoNum(pNtk)-1)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the wires.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i, Counter, nNodes;
+
+    // count the number of wires
+    nNodes = 0;
+    Abc_NtkForEachNode( pNtk, pTerm, i )
+    {
+        if ( i == 0 ) 
+            continue;
+        pNet = Abc_ObjFanout0(pTerm);
+        if ( Abc_ObjIsCo(Abc_ObjFanout0(pNet)) )
+            continue;
+        nNodes++;
+    }
+
+    // write the wires
+    Counter = 0;
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachNode( pNtk, pTerm, i )
+    {
+        if ( i == 0 ) 
+            continue;
+        pNet = Abc_ObjFanout0(pTerm);
+        if ( Abc_ObjIsCo(Abc_ObjFanout0(pNet)) )
+            continue;
+        Counter++;
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the wires.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i, nCubes, nFanins, Counter, nDigits, fPadZeros;
+    char * pName;
+    extern int Abc_SopIsExorType( char * pSop );
+
+    nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
+    Counter = 1;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        nFanins = Abc_ObjFaninNum(pObj);
+        nCubes = Abc_SopGetCubeNum(pObj->pData);
+        if ( Abc_SopIsAndType(pObj->pData) )
+            pName = "ts_and", fPadZeros = 1;
+        else if ( Abc_SopIsExorType(pObj->pData) )
+            pName = "ts_xor", fPadZeros = 1;
+        else // if ( Abc_SopIsOrType(pObj->pData) )
+            pName = "ts_or",  fPadZeros = 0;
+
+        assert( nCubes < 2 );
+        if ( nCubes == 0 )
+        {
+            fprintf( pFile, "  ts_gnd g%0*d ", nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 0, fPadZeros );
+        }
+        else if ( nCubes == 1 && nFanins == 0 )
+        {
+            fprintf( pFile, "  ts_vdd g%0*d ", nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 0, fPadZeros );
+        }
+        else if ( nFanins == 1 && Abc_SopIsInv(pObj->pData) )
+        {
+            fprintf( pFile, "  ts_inv g%0*d ", nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 1, fPadZeros );
+        }
+        else if ( nFanins == 1 )
+        {
+            fprintf( pFile, "  ts_buf g%0*d ", nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 1, fPadZeros );
+        }
+        else if ( nFanins <= 4 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 4, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 4, fPadZeros );
+        }
+        else if ( nFanins <= 6 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 6, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 6, fPadZeros );
+        }
+        else if ( nFanins == 7 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 7, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 7, fPadZeros );
+        }
+        else if ( nFanins == 8 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 8, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 8, fPadZeros );
+        }
+        else if ( nFanins <= 16 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 16, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 16, fPadZeros );
+        }
+        else if ( nFanins <= 32 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 32, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 32, fPadZeros );
+        }
+        else if ( nFanins <= 64 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 64, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 64, fPadZeros );
+        }
+        else if ( nFanins <= 128 )
+        {
+            fprintf( pFile, "  %s%d g%0*d ", pName, 128, nDigits, Counter++ );
+            Io_WriteVerilogArgs( pFile, pObj, 128, fPadZeros );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros )
+{
+    Abc_Obj_t * pFanin;
+    int i, Counter = 2;
+    fprintf( pFile, "(.z (%s)", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+    {
+        if ( Counter++ % 4 == 0 )
+            fprintf( pFile, "\n   " );
+        fprintf( pFile, " .i%d (%s)", i+1, Io_WriteVerilogGetName(Abc_ObjFanin(pObj,i)) );
+    }
+    for ( ; i < nInMax; i++ )
+    {
+        if ( Counter++ % 4 == 0 )
+            fprintf( pFile, "\n   " );
+        fprintf( pFile, " .i%d (%s)", i+1, fPadZeros? "1\'b0" : "1\'b1" );
+    }
+    fprintf( pFile, ");\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    char * pSop;
+    int i, k, nFanins;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_SopGetCubeNum(pObj->pData) > 1 )
+        {
+            printf( "Node %s contains a cover with more than one cube.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins < 2 )
+            continue;
+        pSop = pObj->pData;
+        for ( k = 0; k < nFanins; k++ )
+            if ( pSop[k] != '1' )
+            {
+                printf( "Node %s contains a cover with non-positive literals.\n", Abc_ObjName(pObj) );
+                return 0;
+            }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the name for writing the Verilog file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Io_WriteVerilogGetName( Abc_Obj_t * pObj )
+{
+    static char Buffer[20];
+    char * pName;
+    pName = Abc_ObjName(pObj);
+    if ( pName[0] != '[' )
+        return pName;
+    // replace opening bracket by the escape sign and closing bracket by space
+    // as a result of this transformation, the length of the name does not change
+    strcpy( Buffer, pName );
+    Buffer[0] = '\\';
+    Buffer[strlen(Buffer)-1] = ' ';
+    return Buffer;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+