Version abc90505

6 files changed, 396 insertions, 14 deletions

diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index d870a610..baf4e64b 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -481,6 +481,196 @@ Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk )
     return pNtkNew;
 }
 
+#include "giaAig.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Performs retiming with classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Abc_NtkRetimeWithClassesAig( Aig_Man_t * pMan, Vec_Int_t * vClasses, Vec_Int_t ** pvClasses, int fVerbose )
+{
+    Aig_Man_t * pManNew;
+    Gia_Man_t * pGia, * pGiaNew;
+    pGia = Gia_ManFromAigSimple( pMan );
+    assert( Gia_ManRegNum(pGia) == Vec_IntSize(vClasses) );
+    pGia->vFlopClasses = vClasses;
+    pGiaNew = Gia_ManRetimeForward( pGia, 10, fVerbose );
+    *pvClasses = pGiaNew->vFlopClasses; 
+    pGiaNew->vFlopClasses = NULL;
+    pManNew = Gia_ManToAig( pGiaNew, 0 );
+    Gia_ManStop( pGiaNew );
+    Gia_ManStop( pGia );
+    return pManNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs retiming with classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkRetimeWithClassesNtk( Abc_Ntk_t * pNtk, Vec_Int_t * vClasses, Vec_Int_t ** pvClasses, int fVerbose )
+{
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+    extern Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan );
+    Abc_Ntk_t * pNtkAig, * pNtkAigRet, * pNtkRes;
+    Aig_Man_t * pMan, * pManNew;
+    pNtkAig    = Abc_NtkStrash( pNtk, 0, 1, 0 );
+    pMan       = Abc_NtkToDar( pNtkAig, 0, 1 );
+    pManNew    = Abc_NtkRetimeWithClassesAig( pMan, vClasses, pvClasses, fVerbose );
+    pNtkAigRet = Abc_NtkFromDarSeqSweep( pNtkAig, pManNew );
+    pNtkRes    = Abc_NtkToLogic( pNtkAigRet );
+    Abc_NtkDelete( pNtkAigRet );
+    Abc_NtkDelete( pNtkAig );
+    Aig_ManStop( pManNew );
+    Aig_ManStop( pMan );
+    return pNtkRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns self-loops back into the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkTransformBack( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, Vec_Ptr_t * vControls, Vec_Int_t * vClasses )
+{
+    Abc_Obj_t * pObj, * pNodeNew, * pCtrl, * pDriver;
+    int i, Class;
+    assert( Abc_NtkPoNum(pNtkOld) == Abc_NtkPoNum(pNtkNew) );
+    // match the POs of the old into new
+    Abc_NtkForEachPo( pNtkOld, pObj, i )
+        pObj->pCopy = Abc_NtkPo( pNtkNew, i );
+    // remap the flops
+    Vec_PtrForEachEntry( vControls, pObj, i )
+    {
+        assert( Abc_ObjIsPo(pObj) && pObj->pNtk == pNtkOld );
+        Vec_PtrWriteEntry( vControls, i, pObj->pCopy );
+    }
+    // create self-loops
+    assert( Abc_NtkLatchNum(pNtkNew) == Vec_IntSize(vClasses) );
+    Abc_NtkForEachLatch( pNtkNew, pObj, i )
+    {
+        Class = Vec_IntEntry( vClasses, i );
+        if ( Class == -1 )
+            continue;
+        pDriver = Abc_ObjFanin0(Abc_ObjFanin0(pObj));
+        pCtrl = Vec_PtrEntry( vControls, Class );
+        pCtrl = Abc_ObjFanin0( pCtrl );
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );
+        Abc_ObjAddFanin( pNodeNew, pCtrl );
+        Abc_ObjAddFanin( pNodeNew, pDriver );
+        Abc_ObjAddFanin( pNodeNew, Abc_ObjFanout0(pObj) );
+        Abc_ObjSetData( pNodeNew, Abc_SopRegister(pNtkNew->pManFunc, "0-1 1\n11- 1\n") );
+        Abc_ObjPatchFanin( Abc_ObjFanin0(pObj), pDriver, pNodeNew );
+    }
+    // remove the useless POs
+    Vec_PtrForEachEntry( vControls, pObj, i )
+        Abc_NtkDeleteObj( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Classify flops.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCRetime( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Abc_Ntk_t * pNtkNew;
+    Vec_Ptr_t * vControls;
+    Vec_Int_t * vFlopClasses, * vFlopClassesNew;
+    Abc_Obj_t * pObj, * pDriver, * pFlopOut, * pObjPo;
+    int i, iFlop, CountN = 0, Count2 = 0, Count1 = 0, Count0 = 0;
+
+    // duplicate the AIG
+    pNtk = Abc_NtkDup( pNtk );
+
+    // update registers
+    vControls    = Vec_PtrAlloc( 100 );
+    vFlopClasses = Vec_IntAlloc( 100 );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        pFlopOut = Abc_ObjFanout0(pObj);
+        pDriver = Abc_ObjFanin0( Abc_ObjFanin0(pObj) );
+        if ( Abc_ObjFaninNum(pDriver) != 3 )
+        {
+            Vec_IntPush( vFlopClasses, -1 );
+            CountN++;
+            continue;
+        }
+        if ( Abc_ObjFanin(pDriver, 1) != pFlopOut && Abc_ObjFanin(pDriver, 2) != pFlopOut )
+        {
+            Vec_IntPush( vFlopClasses, -1 );
+            Count2++;
+            continue;
+        }
+        if ( Abc_ObjFanin(pDriver, 1) == pFlopOut )
+        {
+            Vec_IntPush( vFlopClasses, -1 );
+            Count1++;
+            continue;
+        }
+        assert( Abc_ObjFanin(pDriver, 2) == pFlopOut );
+        Count0++;
+        Vec_PtrPushUnique( vControls, Abc_ObjFanin0(pDriver) );
+        // set the flop class
+        iFlop = Vec_PtrFind( vControls, Abc_ObjFanin0(pDriver) );
+        Vec_IntPush( vFlopClasses, iFlop );
+        // update
+        Abc_ObjPatchFanin( Abc_ObjFanin0(pObj), pDriver, Abc_ObjFanin(pDriver, 1) );
+    }
+    if ( Count1 )
+        printf( "Opposite phase enable is present in %d flops (out of %d).\n", Count1, Abc_NtkLatchNum(pNtk) );
+    if ( fVerbose )
+    printf( "CountN = %4d. Count2 = %4d. Count1 = %4d. Count0 = %4d. Ctrls = %d.\n", 
+        CountN, Count2, Count1, Count0, Vec_PtrSize(vControls) );
+
+    // add the controls to the list of POs
+    Vec_PtrForEachEntry( vControls, pObj, i )
+    {
+        pObjPo = Abc_NtkCreatePo( pNtk );
+        Abc_ObjAddFanin( pObjPo, pObj );
+        Abc_ObjAssignName( pObjPo, Abc_ObjName(pObjPo), NULL );
+        Vec_PtrWriteEntry( vControls, i, pObjPo );
+    }
+    Abc_NtkOrderCisCos( pNtk );
+    Abc_NtkCleanup( pNtk, fVerbose );
+
+    // performs retiming with classes
+    pNtkNew = Abc_NtkRetimeWithClassesNtk( pNtk, vFlopClasses, &vFlopClassesNew, fVerbose );
+    Abc_NtkTransformBack( pNtk, pNtkNew, vControls, vFlopClassesNew );
+//    assert( Abc_NtkPoNum(pNtkNew) == Abc_NtkPoNum(pNtk) );
+    Abc_NtkDelete( pNtk );
+
+    Vec_PtrFree( vControls );
+//    Vec_IntFree( vFlopClasses );
+    Vec_IntFree( vFlopClassesNew );
+    return pNtkNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f8815321..946b7210 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -200,6 +200,7 @@ static int Abc_CommandUnseq          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandRetime         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDRetime        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFlowRetime     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCRetime        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqFpga        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqMap         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqSweep       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -519,6 +520,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "dretime",       Abc_CommandDRetime,          1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "fretime",       Abc_CommandFlowRetime,       1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "cretime",       Abc_CommandCRetime,          1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "ssweep",        Abc_CommandSeqSweep,         1 );
@@ -8258,6 +8260,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Amap_LibertyTest( char * pFileName );
     extern void Bbl_ManTest( Abc_Ntk_t * pNtk );
     extern void Bbl_ManSimpleDemo();
+    extern Abc_Ntk_t * Abc_NtkCRetime( Abc_Ntk_t * pNtk, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -8475,7 +8478,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Abc_NtkDarTest( pNtk );
 
 //    Bbl_ManTest( pNtk );
-
+/*
     {
     extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
     extern void Aig_ManFactorAlgebraicTest( Aig_Man_t * p );
@@ -8484,8 +8487,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Aig_ManFactorAlgebraicTest( pAig );
     Aig_ManStop( pAig );
     }
-
+*/
 //    Bbl_ManSimpleDemo();
+//    pNtkRes = Abc_NtkCRetime( pNtk );
+    pNtkRes = NULL;
+    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: test [-h] <file_name>\n" );
@@ -13886,6 +13898,79 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandCRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkCRetime( Abc_Ntk_t * pNtk, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose    = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Only works for logic networks.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "The network is combinational.\n" );
+        return 0;
+    }
+    // modify the current network
+    pNtkRes = Abc_NtkCRetime( pNtk, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Sequential cleanup has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: cretime [-vh]\n" );
+    fprintf( pErr, "\t         performs most-forward retiming with equiv classes\n" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -15260,11 +15345,11 @@ int Abc_CommandDarPhase( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
-    int nFrames;
+    int nFrames, nPref;
     int fIgnore;
     int fPrint;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, int fPrint, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -15272,11 +15357,12 @@ int Abc_CommandDarPhase( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nFrames     = 0;
+    nPref       = 0;
     fIgnore     = 0;
     fPrint      = 0;
     fVerbose    = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fipvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FPipvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15291,6 +15377,17 @@ int Abc_CommandDarPhase( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nFrames < 0 ) 
                 goto usage;
             break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPref = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPref < 0 ) 
+                goto usage;
+            break;
         case 'i':
             fIgnore ^= 1;
             break;
@@ -15323,11 +15420,11 @@ int Abc_CommandDarPhase( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( fPrint )
     {
-        Abc_NtkPhaseAbstract( pNtk, 0, fIgnore, 1, fVerbose );
+        Abc_NtkPhaseAbstract( pNtk, 0, nPref, fIgnore, 1, fVerbose );
         return 0;
     }
     // modify the current network
-    pNtkRes = Abc_NtkPhaseAbstract( pNtk, nFrames, fIgnore, 0, fVerbose );
+    pNtkRes = Abc_NtkPhaseAbstract( pNtk, nFrames, nPref, fIgnore, 0, fVerbose );
     if ( pNtkRes == NULL )
     {
 //        fprintf( pErr, "Phase abstraction has failed.\n" );
@@ -15338,10 +15435,11 @@ int Abc_CommandDarPhase( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: phase [-F <num>] [-ipvh]\n" );
+    fprintf( pErr, "usage: phase [-FP <num>] [-ipvh]\n" );
     fprintf( pErr, "\t         performs sequential cleanup of the current network\n" );
     fprintf( pErr, "\t         by removing nodes and latches that do not feed into POs\n" );
     fprintf( pErr, "\t-F num : the number of frames to abstract [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-P num : the number of prefix frames to skip [default = %d]\n", nPref );
     fprintf( pErr, "\t-i     : toggle ignoring the initial state [default = %s]\n", fIgnore? "yes": "no" );
     fprintf( pErr, "\t-p     : toggle printing statistics about generators [default = %s]\n", fPrint? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ab47d797..873b78d1 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2862,9 +2862,9 @@ Abc_Ntk_t * Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, int fPrint, int fVerbose )
+Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose )
 {
-    extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
+    extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
     Vec_Int_t * vInits;
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
@@ -2872,7 +2872,7 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
     if ( pMan == NULL )
         return NULL;
     vInits = Abc_NtkGetLatchValues(pNtk);
-    pMan = Saig_ManPhaseAbstract( pTemp = pMan, vInits, nFrames, fIgnore, fPrint, fVerbose );
+    pMan = Saig_ManPhaseAbstract( pTemp = pMan, vInits, nFrames, nPref, fIgnore, fPrint, fVerbose );
     Vec_IntFree( vInits );
     Aig_ManStop( pTemp );
     if ( pMan == NULL )
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 10e3ba2d..c9fb2834 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -1129,8 +1129,8 @@ void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk )
     {
         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 );
+        printf( "%5d  %20s :  Cone = %5d.  Supp = %5d.\n", 
+            i, Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
         Vec_PtrFree( vNodes );
         Vec_PtrFree( vSupp );
     }
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 75419e0f..e29a3009 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -62,6 +62,7 @@ static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteTruth  ( Abc_Frame_t * pAbc, int argc, char **argv );
 
 extern int glo_fMapped;
 
@@ -119,6 +120,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
 //    Cmd_CommandAdd( pAbc, "I/O", "write_verlib",  IoCommandWriteVerLib,  0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_sorter_cnf", IoCommandWriteSortCnf,  0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_truth",   IoCommandWriteTruth,   0 );
 }
 
 /**Function*************************************************************
@@ -2322,6 +2324,97 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    Vec_Int_t * vTruth;
+    Abc_Ntk_t * pNtk = pAbc->pNtkCur;
+    Abc_Obj_t * pNode;
+    char * pFileName;
+    FILE * pFile;
+    unsigned * pTruth;
+    int c;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        printf( "Current networks is not available.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        printf( "Current networks should not an AIG. Run \"logic\".\n" );
+        return 0;
+    }
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+    {
+        printf( "Current networks should have exactly one primary output.\n" );
+        return 0;
+    }
+    if ( Abc_NtkNodeNum(pNtk) != 1 )
+    {
+        printf( "Current networks should have exactly one node.\n" );
+        return 0;
+    }
+    pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
+    if ( Abc_ObjFaninNum(pNode) == 0 )
+    { 
+        printf( "Can only write logic function with 0 inputs.\n" );
+        return 0;
+    }
+    if ( Abc_ObjFaninNum(pNode) > 16 )
+    { 
+        printf( "Can only write logic function with no more than 16 inputs.\n" );
+        return 0;
+    }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    // convert to logic
+    Abc_NtkToAig( pNtk );
+    vTruth = Vec_IntAlloc( 0 );
+    pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vTruth, 0 );
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        Vec_IntFree( vTruth );
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return 0;
+    }
+    Extra_PrintBinary( pFile, pTruth, 1<<Abc_ObjFaninNum(pNode) );
+    fclose( pFile );
+    Vec_IntFree( vTruth );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_truth [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         writes truth table into a file\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/ioReadBench.c b/src/base/io/ioReadBench.c
index b6e0e15f..e7a2d2fe 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -224,7 +224,8 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                 else if ( strcmp(pType, "NOT") == 0 )
                     Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) );
                 else if ( strncmp(pType, "MUX", 3) == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "1-0 1\n-11 1\n") );
+//                    Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "1-0 1\n-11 1\n") );
+                    Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "0-1 1\n11- 1\n") );
                 else if ( strncmp(pType, "gnd", 3) == 0 )
                     Abc_ObjSetData( pNode, Abc_SopRegister( pNtk->pManFunc, " 0\n" ) );
                 else if ( strncmp(pType, "vdd", 3) == 0 )