Shrink for 6-LUTs.

Makefile

@@ -20,7 +20,7 @@ MODULES := \
 	src/opt/ret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
 	src/opt/cgt src/opt/csw src/opt/dar src/opt/dau \
 	src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \
-	src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
+	src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky src/bool/rsb \
 	src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \
 	src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \
 	src/proof/abs \

abclib.dsp

@@ -3543,6 +3543,10 @@ SOURCE=.\src\aig\gia\giaShrink.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaShrink6.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaSim.c
 # End Source File
 # Begin Source File
@@ -3786,6 +3790,26 @@ SOURCE=.\src\bool\lucky\luckySwap.c
 SOURCE=.\src\bool\lucky\luckySwapIJ.c
 # End Source File
 # End Group
+# Begin Group "rsb"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bool\rsb\rsb.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bool\rsb\rsbDec6.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bool\rsb\rsbInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bool\rsb\rsbMan.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "prove"
 

src/aig/gia/gia.h

@@ -980,6 +980,7 @@ extern Gia_Man_t *         Gia_ManSeqCleanup( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose );
 /*=== giaShrink.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose );
+extern Gia_Man_t *         Gia_ManMapShrink6( Gia_Man_t * p, int fKeepLevel, int fVerbose );
 /*=== giaSort.c ============================================================*/
 extern int *               Gia_SortFloats( float * pArray, int * pPerm, int nSize );
 /*=== giaSim.c ============================================================*/

src/aig/gia/giaShrink.c

@@ -85,6 +85,7 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose
         if ( Gia_ObjIsCi(pObj) )
         {
             pObj->Value = Gia_ManAppendCi( pNew );
+            if ( p->vLevels )
                 Gia_ObjSetLevel( pNew, Gia_ObjFromLit(pNew, Gia_ObjValue(pObj)), Gia_ObjLevel(p, pObj) );
         }
         else if ( Gia_ObjIsCo(pObj) )

src/aig/gia/module.make

@@ -31,6 +31,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaRetime.c \
     src/aig/gia/giaScl.c \
     src/aig/gia/giaShrink.c \
+    src/aig/gia/giaShrink6.c \
     src/aig/gia/giaSim.c \
     src/aig/gia/giaSim2.c \
     src/aig/gia/giaSort.c \

src/base/abci/abc.c

@@ -26155,7 +26155,8 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Shrink( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Gia_Man_t * pTemp;
+    Gia_Man_t * pTemp = NULL;
+    int nLutSize;
     int c,fVerbose = 0;
     int fKeepLevel = 0;
     Extra_UtilGetoptReset();
@@ -26185,7 +26186,14 @@ int Abc_CommandAbc9Shrink( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Shrink(): Mapping of the AIG is not defined.\n" );
         return 1;
     }
+    nLutSize = Gia_ManLutSizeMax( pAbc->pGia );
+    if ( nLutSize <= 4 )
         pTemp = Gia_ManPerformMapShrink( pAbc->pGia, fKeepLevel, fVerbose );
+    else if ( nLutSize <= 6 )
+        pTemp = Gia_ManMapShrink6( pAbc->pGia, fKeepLevel, fVerbose );
+    else
+        Abc_Print( -1, "Abc_CommandAbc9Shrink(): Works only for 4-LUTs and 6-LUTs.\n" );
+    if ( pTemp )
         Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 

src/bool/rsb/module.make

+SRC +=    src/bool/rsb/rsbDec6.c \
+    src/bool/rsb/rsbMan.c

src/bool/rsb/rsb.h

+/**CFile****************************************************************
+
+  FileName    [rsb.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table based resubstitution.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rsb.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__bool_Rsb_h
+#define ABC__bool_Rsb_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Rsb_Man_t_ Rsb_Man_t;
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== rsbMan.c ==========================================================*/
+extern Rsb_Man_t *  Rsb_ManAlloc( int nLeafMax, int nDivMax, int nDecMax, int fVerbose );
+extern void         Rsb_ManFree( Rsb_Man_t * p );
+extern Vec_Int_t *  Rsb_ManGetFanins( Rsb_Man_t * p );
+extern Vec_Int_t *  Rsb_ManGetFaninsOld( Rsb_Man_t * p );
+/*=== rsbDec6.c ==========================================================*/
+extern int          Rsb_ManPerformResub6( Rsb_Man_t * p, int nVars, word uTruth, Vec_Wrd_t * vDivTruths, word * puTruth0, word * puTruth1, int fVerbose );
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/bool/rsb/rsbInt.h

+/**CFile****************************************************************
+
+  FileName    [rsbInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table based resubstitution.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rsbInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__bool_RsbInt_h
+#define ABC__bool_RsbInt_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "misc/vec/vec.h"
+#include "misc/util/utilTruth.h"
+#include "bool/kit/kit.h"
+#include "rsb.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// truth table computation manager
+struct Rsb_Man_t_
+{
+    // parameters
+    int                nLeafMax;     // the max number of leaves of a cut
+    int                nDivMax;      // the max number of divisors to collect
+    int                nDecMax;      // the max number of decompositions
+    int                fVerbose;     // verbosity level
+    // decomposition
+    Vec_Wrd_t *        vCexes;       // counter-examples
+    Vec_Int_t *        vDecPats;     // decomposition patterns
+    Vec_Int_t *        vFanins;      // the result of decomposition
+    Vec_Int_t *        vFaninsOld;   // original fanins
+    Vec_Int_t *        vTries;       // intermediate
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== rsbMan.c ==========================================================*/
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/bool/rsb/rsbMan.c

+/**CFile****************************************************************
+
+  FileName    [rsbMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table based resubstitution.]
+
+  Synopsis    [Manager maintenance.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rsbMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rsbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rsb_Man_t * Rsb_ManAlloc( int nLeafMax, int nDivMax, int nDecMax, int fVerbose )
+{
+    Rsb_Man_t * p;
+    assert( nLeafMax <= 20 );
+    assert( nDivMax  <= 200 );
+    p = ABC_CALLOC( Rsb_Man_t, 1 );
+    p->nLeafMax   = nLeafMax;
+    p->nDivMax    = nDivMax;
+    p->nDecMax    = nDecMax;
+    p->fVerbose   = fVerbose;
+    // decomposition
+    p->vCexes     = Vec_WrdAlloc( nDivMax + 150 );
+    p->vDecPats   = Vec_IntAlloc( Abc_TtWordNum(nLeafMax) );
+    p->vFanins    = Vec_IntAlloc( 10 );
+    p->vFaninsOld = Vec_IntAlloc( 10 );
+    p->vTries     = Vec_IntAlloc( 10 );
+    return p;
+}
+void Rsb_ManFree( Rsb_Man_t * p )
+{
+    Vec_WrdFree( p->vCexes );
+    Vec_IntFree( p->vDecPats );
+    Vec_IntFree( p->vFanins );
+    Vec_IntFree( p->vFaninsOld );
+    Vec_IntFree( p->vTries );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Rsb_ManGetFanins( Rsb_Man_t * p )
+{
+    return p->vFanins;
+}
+Vec_Int_t * Rsb_ManGetFaninsOld( Rsb_Man_t * p )
+{
+    return p->vFaninsOld;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/misc/util/utilTruth.h

@@ -116,6 +116,18 @@ static inline int  Abc_TtHexDigitNum( int nVars ) { return nVars <= 2 ? 1 : 1 <<
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Abc_TtClear( word * pOut, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] = 0;
+}
+static inline void Abc_TtFill( word * pOut, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] = ~(word)0;
+}
 static inline void Abc_TtNot( word * pOut, int nWords )
 {
     int w;
@@ -142,6 +154,18 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords,
         for ( w = 0; w < nWords; w++ )
             pOut[w] = pIn1[w] & pIn2[w];
 }
+static inline void Abc_TtSharp( word * pOut, word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] = pIn1[w] & ~pIn2[w];
+}
+static inline void Abc_TtOr( word * pOut, word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] = pIn1[w] | pIn2[w];
+}
 static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
 {
     int w;
@@ -756,10 +780,10 @@ static inline int Abc_TtReadHex( word * pTruth, char * pString )
 static inline void Abc_TtPrintBinary( word * pTruth, int nVars )
 {
     word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
-    int k;
+    int k, Limit = Abc_MinInt( 64, (1 << nVars) );
     assert( nVars >= 2 );
     for ( pThis = pTruth; pThis < pLimit; pThis++ )
-        for ( k = 0; k < 64; k++ )
+        for ( k = 0; k < Limit; k++ )
             printf( "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
     printf( "\n" );
 }
@@ -1109,6 +1133,75 @@ static inline int Abc_TtCountOnes( word x )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Abc_Tt6FirstBit( word t )
+{
+    int n = 0;
+    if ( t == 0 ) return -1;
+    if ( (t & 0x00000000FFFFFFFF) == 0 ) { n += 32; t >>= 32; }
+    if ( (t & 0x000000000000FFFF) == 0 ) { n += 16; t >>= 16; }
+    if ( (t & 0x00000000000000FF) == 0 ) { n +=  8; t >>=  8; }
+    if ( (t & 0x000000000000000F) == 0 ) { n +=  4; t >>=  4; }
+    if ( (t & 0x0000000000000003) == 0 ) { n +=  2; t >>=  2; }
+    if ( (t & 0x0000000000000001) == 0 ) { n++; }
+    return n;
+}
+static inline int Abc_Tt6LastBit( word t )
+{
+    int n = 0;
+    if ( t == 0 ) return -1;
+    if ( (t & 0xFFFFFFFF00000000) == 0 ) { n += 32; t <<= 32; }
+    if ( (t & 0xFFFF000000000000) == 0 ) { n += 16; t <<= 16; }
+    if ( (t & 0xFF00000000000000) == 0 ) { n +=  8; t <<=  8; }
+    if ( (t & 0xF000000000000000) == 0 ) { n +=  4; t <<=  4; }
+    if ( (t & 0xC000000000000000) == 0 ) { n +=  2; t <<=  2; }
+    if ( (t & 0x8000000000000000) == 0 ) { n++; }
+    return 63-n;
+}
+static inline int Abc_TtFindFirstBit( word * pIn, int nVars )
+{
+    int w, nWords = Abc_TtWordNum(nVars);
+    for ( w = 0; w < nWords; w++ )
+        if ( pIn[w] )
+            return 64*w + Abc_Tt6FirstBit(pIn[w]);
+    return -1;
+}
+static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
+{
+    int w, nWords = Abc_TtWordNum(nVars);
+    for ( w = 0; w < nWords; w++ )
+        if ( ~pIn[w] )
+            return 64*w + Abc_Tt6FirstBit(~pIn[w]);
+    return -1;
+}
+static inline int Abc_TtFindLastBit( word * pIn, int nVars )
+{
+    int w, nWords = Abc_TtWordNum(nVars);
+    for ( w = nWords - 1; w >= 0; w-- )
+        if ( pIn[w] )
+            return 64*w + Abc_Tt6LastBit(pIn[w]);
+    return -1;
+}
+static inline int Abc_TtFindLastZero( word * pIn, int nVars )
+{
+    int w, nWords = Abc_TtWordNum(nVars);
+    for ( w = nWords - 1; w >= 0; w-- )
+        if ( ~pIn[w] )
+            return 64*w + Abc_Tt6LastBit(~pIn[w]);
+    return -1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Abc_TtReverseVars( word * pTruth, int nVars )
 {
     int k;
@@ -1146,6 +1239,49 @@ static inline void Abc_TtReverseBits( word * pTruth, int nVars )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Computes ISOP for 6 variables or less.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars )
+{
+    word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
+    int Var;
+    assert( nVars <= 5 );
+    assert( (uOn & ~uOnDc) == 0 );
+    if ( uOn == 0 )
+        return 0;
+    if ( uOnDc == ~(word)0 )
+        return ~(word)0;
+    assert( nVars > 0 );
+    // find the topmost var
+    for ( Var = nVars-1; Var >= 0; Var-- )
+        if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
+             break;
+    assert( Var >= 0 );
+    // cofactor
+    uOn0   = Abc_Tt6Cofactor0( uOn,   Var );
+    uOn1   = Abc_Tt6Cofactor1( uOn  , Var );
+    uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
+    uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
+    // solve for cofactors
+    uRes0 = Abc_Tt6Isop( uOn0 & ~uOnDc1, uOnDc0, Var );
+    uRes1 = Abc_Tt6Isop( uOn1 & ~uOnDc0, uOnDc1, Var );
+    uRes2 = Abc_Tt6Isop( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var );
+    // derive the final truth table
+    uRes2 |= (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
+    assert( (uOn & ~uRes2) == 0 );
+    assert( (uRes2 & ~uOnDc) == 0 );
+    return uRes2;
+}
+
 /*=== utilTruth.c ===========================================================*/