Logic restruturing after mapping.

5 files changed, 141 insertions, 1 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 67bf081e..bbbc0fae 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1083,6 +1083,10 @@ SOURCE=.\src\base\acb\acbPar.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\acb\acbPush.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\acb\acbSets.c
 # End Source File
 # Begin Source File
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f9f2f2e0..98870a20 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -124,6 +124,7 @@ static int Abc_CommandMfs                    ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandMfs2                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMfs3                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMfse                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandLogicPush              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTrace                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandGlitch                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSpeedup                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -781,6 +782,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "mfs2",          Abc_CommandMfs2,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "mfs3",          Abc_CommandMfs3,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "mfse",          Abc_CommandMfse,              1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "logicpush",     Abc_CommandLogicPush,        1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "trace",         Abc_CommandTrace,            0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "glitch",        Abc_CommandGlitch,           0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "speedup",       Abc_CommandSpeedup,          1 );
@@ -5807,6 +5809,73 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandLogicPush( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Abc_Ntk_t * Abc_NtkOptPush( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose );
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    Abc_Ntk_t * pNtkRes;
+    int nLutSize = 4;
+    int fVerbose = 0;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Kvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        Abc_Print( -1, "This command can only be applied to a logic network.\n" );
+        return 1;
+    }
+    Abc_NtkToSop( pNtk, -1, ABC_INFINITY );
+    pNtkRes = Abc_NtkOptPush( pNtk, nLutSize, fVerbose );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: logicpush [-K num] [-vh]\n" );
+    Abc_Print( -2, "\t           performs logic pushing to reduce structural bias\n" );
+    Abc_Print( -2, "\t-K <num> : the LUT size used in the mapping [default = %d]\n", nLutSize );
+    Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/acb/acbAbc.c b/src/base/acb/acbAbc.c
index 2b07a202..7b215a56 100644
--- a/src/base/acb/acbAbc.c
+++ b/src/base/acb/acbAbc.c
@@ -271,6 +271,28 @@ Abc_Ntk_t * Abc_NtkOptMfse( Abc_Ntk_t * pNtk, Acb_Par_t * pPars )
     return pNtkNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkOptPush( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose )
+{
+    extern void Acb_NtkPushLogic( Acb_Ntk_t * p, int nLutSize, int fVerbose );
+    Abc_Ntk_t * pNtkNew;
+    Acb_Ntk_t * p = Acb_NtkFromAbc( pNtk );
+    Acb_NtkPushLogic( p, nLutSize, fVerbose );
+    pNtkNew = Acb_NtkToAbc( pNtk, p );
+    Acb_ManFree( p->pDesign );
+    return pNtkNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/acb/module.make b/src/base/acb/module.make
index 06affeff..46294f9f 100644
--- a/src/base/acb/module.make
+++ b/src/base/acb/module.make
@@ -3,5 +3,6 @@ SRC +=    src/base/acb/acbAbc.c \
     src/base/acb/acbCom.c \
     src/base/acb/acbFunc.c \
     src/base/acb/acbMfs.c \
+    src/base/acb/acbPush.c \
     src/base/acb/acbSets.c \
     src/base/acb/acbUtil.c 
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index e04ffbc9..f02a9835 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -2209,7 +2209,51 @@ static inline int Abc_Tt6EsopVerify( word t, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Check if the function is decomposable with the given pair.]
+  Synopsis    [Check if the function is output-decomposable with the given var.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtCheckOutAnd( word t, int i, word * pOut )
+{
+    word c0 = Abc_Tt6Cofactor0( t, i );
+    word c1 = Abc_Tt6Cofactor1( t, i );
+    assert( c0 == c1 );
+    if ( c0 == 0 ) //  F = i * G
+    {
+        if ( pOut ) *pOut = c1;
+        return 0;
+    }
+    if ( c1 == 0 ) //  F = ~i * G
+    {
+        if ( pOut ) *pOut = c0;
+        return 1;
+    }
+    if ( ~c0 == 0 ) //  F = ~i + G
+    {
+        if ( pOut ) *pOut = c1;
+        return 2;
+    }
+    if ( ~c1 == 0 ) //  F = i + G
+    {
+        if ( pOut ) *pOut = c0;
+        return 3;
+    }
+    if ( c0 == ~c1 ) //  F = i # G
+    {
+        if ( pOut ) *pOut = c0;
+        return 4;
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the function is input-decomposable with the given pair.]
 
   Description []