Experiments with LUT mapping for small functions.

4 files changed, 275 insertions, 12 deletions

diff --git a/src/aig/gia/giaMinLut.c b/src/aig/gia/giaMinLut.c
index 80d4476e..957ee2c0 100644
--- a/src/aig/gia/giaMinLut.c
+++ b/src/aig/gia/giaMinLut.c
@@ -158,7 +158,7 @@ Gia_Man_t * Vec_WrdReadTest( char * pFileName )
     Vec_WecForEachLevel( vRes, vPart, i )
     {
         assert( Vec_IntSize(vPart) <= nBitsI );
-        pPart = Gia_TryPermOptCare( pFuncs + i * nBitsO * nWords, nBitsI, nBitsO, nWords, 10, 0 );
+        pPart = Gia_TryPermOptCare( pFuncs + i * nBitsO * nWords, nBitsI, nBitsO, nWords, 20, 0 );
         Gia_ManFillValue( pPart );
         Gia_ManConst0(pPart)->Value = 0;
         Gia_ManForEachCi( pPart, pObj, k )
diff --git a/src/aig/gia/giaMinLut2.c b/src/aig/gia/giaMinLut2.c
index 26310d34..277ce949 100644
--- a/src/aig/gia/giaMinLut2.c
+++ b/src/aig/gia/giaMinLut2.c
@@ -515,6 +515,209 @@ word * Abc_TtMinArray( word * p, int nOuts, int nVars, int * pnNodes, int fVerbo
   SeeAlso     []
 
 ***********************************************************************/
+static inline word Abc_TtSimple6Min_rec( Gia_Man_t * p, word uF, word uC, int nVars, Vec_Wrd_t * vNodes, int * piLit, int * pPerm )
+{
+    word uF0, uF1, uC0, uC1, uRes0, uRes1, uRes2; int i, Var, iLit0, iLit1;
+    word uFC =  uF & uC;
+    word uRC = ~uF & uC;
+    assert( nVars <= 6 );
+    *piLit = 0;
+    if ( !uFC )
+    {
+        *piLit = 0;
+        return 0;
+    }
+    if ( !uRC )
+    {
+        *piLit = 1;
+        return ~(word)0;
+    }
+    assert( nVars > 0 );
+    if ( 1 && vNodes )
+    {
+        int iLit;
+        int s = 0;
+        Vec_WrdForEachEntryDouble( vNodes, uRes2, iLit, i )
+            if ( !((uF ^ uRes2) & uC) )
+            {
+                *piLit = (unsigned)iLit;
+                return uRes2;
+            }
+            else if ( !((uF ^ ~uRes2) & uC) )
+            {
+                *piLit = Abc_LitNot( (unsigned)iLit );
+                return ~uRes2;
+            }
+    }
+    for ( Var = nVars-1; Var >= 0; Var-- )
+        if ( Abc_Tt6HasVar( uF, Var ) )
+             break;
+        else
+            uC = Abc_Tt6Cofactor0(uC, Var) | Abc_Tt6Cofactor1(uC, Var);
+    assert( Var >= 0 );
+    uF0 = Abc_Tt6Cofactor0( uF, Var );
+    uF1 = Abc_Tt6Cofactor1( uF, Var );
+    uC0 = Abc_Tt6Cofactor0( uC, Var );
+    uC1 = Abc_Tt6Cofactor1( uC, Var );
+    uRes0 = Abc_TtSimple6Min_rec( p, uF0, uC0, Var, vNodes, &iLit0, pPerm );
+    uRes1 = Abc_TtSimple6Min_rec( p, uF1, uC1, Var, vNodes, &iLit1, pPerm );
+    if ( uRes0 == uRes1 )
+    {
+        *piLit = iLit0;
+        return uRes0;
+    }
+    uRes2 = (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
+    Var = pPerm ? pPerm[Var] : Var;
+    //if ( !(uRes0 & ~uRes1 & uC1) )
+    if ( !(uRes0 & ~uRes1) )
+        *piLit = Gia_ManHashOr( p, Gia_ManHashAnd(p, Abc_Var2Lit(1+Var, 0), iLit1), iLit0 );
+    //else if ( !(uRes1 & ~uRes0 & uC0) )
+    else if ( !(uRes1 & ~uRes0) )
+        *piLit = Gia_ManHashOr( p, Gia_ManHashAnd(p, Abc_Var2Lit(1+Var, 1), iLit0), iLit1 );
+    else
+        *piLit = Gia_ManHashMux( p, Abc_Var2Lit(1+Var, 0), iLit1, iLit0 );
+    assert( !(uFC & ~uRes2) );
+    assert( !(uRes2 & uRC) );
+    if ( vNodes )
+        Vec_WrdPushTwo( vNodes, uRes2, (word)*piLit );
+    return uRes2;
+}
+word * Abc_TtSimpleMin_rec( Gia_Man_t * p, word * pF, word * pC, int nVars, Vec_Wrd_t * vMemory, Vec_Wrd_t * vNodes, Vec_Wec_t * vNodes2, int * piLit, int * pPerm )
+{
+    int i, Entry, Var, iLit0, iLit1, nWords = Abc_TtWordNum(nVars);
+    word * pRes0, * pRes1, * pRes2 = Vec_WrdFetch( vMemory, nWords );
+    *piLit = 0;
+    if ( nVars <= 6 )
+    {
+        pRes2[0] = Abc_TtSimple6Min_rec( p, pF[0], pC[0], nVars, vNodes, piLit, pPerm );
+        return pRes2;
+    }
+    if ( !Abc_TtIntersect(pF, pC, nWords, 0) )
+    {
+        *piLit = 0;
+        Abc_TtClear( pRes2, nWords );
+        return pRes2;
+    }
+    if ( !Abc_TtIntersect(pF, pC, nWords, 1) )
+    {
+        *piLit = 1;
+        Abc_TtFill( pRes2, nWords );
+        return pRes2;
+    }
+    nWords >>= 1;
+    if ( !Abc_TtHasVar( pF, nVars, nVars-1 ) )
+    {
+        word * pCn = Vec_WrdFetch( vMemory, nWords );
+        Abc_TtOr( pCn, pC, pC + nWords, nWords );
+        pRes0 = Abc_TtSimpleMin_rec( p, pF, pCn, nVars-1, vMemory, vNodes, vNodes2, piLit, pPerm );
+        Abc_TtCopy( pRes2,          pRes0, nWords, 0 );
+        Abc_TtCopy( pRes2 + nWords, pRes0, nWords, 0 );
+        return pRes2;
+    }
+    if ( 1 && vNodes2 )
+    {
+        Vec_Int_t * vLayer = Vec_WecEntry( vNodes2, nVars ); int iLit;
+        Vec_IntForEachEntryDouble( vLayer, Entry, iLit, i )
+        {
+            word * pTemp = Vec_WrdEntryP( vMemory, Entry );
+            if ( Abc_TtEqualCare(pTemp, pF, pC, 0, 2*nWords) )
+            {
+                *piLit = iLit;
+                return pTemp;
+            }
+            else if ( Abc_TtEqualCare(pTemp, pF, pC, 1, 2*nWords) )
+            {
+                *piLit = Abc_LitNot(iLit);
+                Abc_TtCopy( pRes2, pTemp, 2*nWords, 1 );
+                return pRes2;
+            }
+        }
+    }
+    assert( nVars > 6 );
+    pRes0 = Abc_TtSimpleMin_rec( p, pF,          pC,          nVars-1, vMemory, vNodes, vNodes2, &iLit0, pPerm );
+    pRes1 = Abc_TtSimpleMin_rec( p, pF + nWords, pC + nWords, nVars-1, vMemory, vNodes, vNodes2, &iLit1, pPerm );
+    if ( Abc_TtEqual(pRes0, pRes1, nWords) )
+    {
+        *piLit = iLit0;
+        Abc_TtCopy( pRes2,          pRes0, nWords, 0 );
+        Abc_TtCopy( pRes2 + nWords, pRes0, nWords, 0 );
+        return pRes2;
+    }
+    Abc_TtCopy( pRes2,          pRes0, nWords, 0 );
+    Abc_TtCopy( pRes2 + nWords, pRes1, nWords, 0 );
+    Var = pPerm ? pPerm[nVars-1] : nVars-1;
+    //if ( !Abc_TtIntersectCare(pRes1, pRes0, pC + nWords, nWords, 1) )
+    if ( !Abc_TtIntersect(pRes1, pRes0, nWords, 1) )
+        *piLit = Gia_ManHashOr( p, Gia_ManHashAnd(p, Abc_Var2Lit(1+Var, 0), iLit1), iLit0 );
+    //else if ( !Abc_TtIntersectCare(pRes0, pRes1, pC, nWords, 1) )
+    else if ( !Abc_TtIntersect(pRes0, pRes1, nWords, 1) )
+        *piLit = Gia_ManHashOr( p, Gia_ManHashAnd(p, Abc_Var2Lit(1+Var, 1), iLit0), iLit1 );
+    else
+        *piLit = Gia_ManHashMux( p, Abc_Var2Lit(1+Var, 0), iLit1, iLit0 );
+    assert( Abc_TtEqualCare(pRes2, pF, pC, 0, 2*nWords) );
+    if ( vNodes2 )
+    {
+        Vec_Int_t * vLayer = Vec_WecEntry( vNodes2, nVars ); 
+        Vec_IntPushTwo( vLayer, pRes2 - Vec_WrdArray(vMemory), *piLit );
+    }
+    return pRes2;
+}
+Gia_Man_t * Abc_TtSimpleMinArrayNew( word * p, int nVars, int nOuts, int * pnNodes, int fVerbose, int * pIPerm )
+{
+    Gia_Man_t * pNew, * pTemp;
+    int o, i, iLit, nWords = Abc_TtWordNum(nVars);
+    word * pF = ABC_ALLOC( word, nWords );
+    word * pR = ABC_ALLOC( word, nWords );
+    Vec_Wrd_t * vMemory = Vec_WrdAlloc( 100 );
+    Vec_Wrd_t * vNodes  = Vec_WrdAlloc( 100 );
+    Vec_Wec_t * vNodes2 = Vec_WecStart( nVars+1 );
+    Vec_WrdGrow( vMemory, 1 << 20 );
+    pNew = Gia_ManStart( 1000 );
+    pNew->pName = Abc_UtilStrsav( "muxes" );
+    for ( i = 0; i < nVars; i++ )
+        Gia_ManAppendCi(pNew);
+    Gia_ManHashAlloc( pNew );
+
+    for ( o = 0; o < nOuts; o++ )
+    {
+        word * pCare = p + nOuts*nWords;
+        word * pTruth = p + o*nWords;
+        for ( i = nVars; i < 6; i++ )
+            assert( !Abc_Tt6HasVar(pTruth[0], i) && !Abc_Tt6HasVar(pCare[0], i) );
+        Abc_TtSimpleMin_rec( pNew, pTruth, pCare, nVars, vMemory, vNodes, vNodes2, &iLit, pIPerm );
+        Gia_ManAppendCo( pNew, iLit );
+    }
+    if ( fVerbose )
+    printf( "Nodes = %5d.  Nodes2 = %5d.  Total = %5d.    ", 
+        Vec_WrdSize(vNodes), Vec_WecSizeSize(vNodes2), Vec_WrdSize(vNodes) + Vec_WecSizeSize(vNodes2) );
+    //printf( "Memory %d (Truth table %d)\n", Vec_WrdSize(vMemory), nWords );
+    if ( pnNodes )
+        *pnNodes = Vec_WrdSize(vNodes) + Vec_WecSizeSize(vNodes2);
+    Vec_WrdFree( vMemory );
+    Vec_WrdFree( vNodes );
+    Vec_WecFree( vNodes2 );
+    ABC_FREE( pF );
+    ABC_FREE( pR );
+
+    Gia_ManHashStop( pNew );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline word Abc_TtGia6Min_rec( Gia_Man_t * p, word uF, word uR, int nVars, Vec_Wrd_t * vNodes, int * piLit, int * pPerm )
 {
     word uF0, uF1, uR0, uR1, uRes0, uRes1, uRes2; int i, Var, iLit0, iLit1;
@@ -906,7 +1109,7 @@ Gia_Man_t * Gia_TryPermOptCare( word * pTruths, int nIns, int nOuts, int nWords,
     abctime clk = Abc_Clock();
     Gia_Man_t * pNew;
     word * pTruthDup  = Abc_TtDup( pTruths, nOuts*nWords, 0 );
-    word * pTruthBest = ABC_ALLOC( word, nOuts*nWords );
+    word * pTruthBest = ABC_FALLOC( word, (nOuts+1)*nWords );
     int pIPermBest[TREE_MAX_VARS] = {0};
     int pIPerm[TREE_MAX_VARS] = {0};
     int r, rBest = -1, nNodes = -1, nNodesBest = ABC_INFINITY;
@@ -932,7 +1135,8 @@ Gia_Man_t * Gia_TryPermOptCare( word * pTruths, int nIns, int nOuts, int nWords,
     ABC_FREE( pTruthDup );
     if ( fVerbose )
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-    pNew = Gia_ManCreateMuxGia( pTruthBest, nIns, nOuts, nWords, pIPermBest );
+    //pNew = Gia_ManCreateMuxGia( pTruthBest, nIns, nOuts, nWords, pIPermBest );
+    pNew = Abc_TtSimpleMinArrayNew( pTruthBest, nIns, nOuts, NULL, 0, pIPermBest );
     //Gia_ManDumpMuxGia( pTruthBest, nIns, nOuts, nWords, pIPermBest, "tt_end.aig" );
     ABC_FREE( pTruthBest );
     return pNew;
@@ -1033,7 +1237,8 @@ Gia_Man_t * Gia_TryPermOptNew( word * pTruths, int nIns, int nOuts, int nWords,
     {
         int nNodesAll = Gia_ManPermuteTreeOne( pTruthDup, nIns, nOuts, nWords, r>0, pIPerm, 0, fVerbose );
         Abc_TtPermute( pTruthDup + nOuts*nWords, pIPerm, nIns );
-        pTemp = Abc_TtGiaMinArrayNew( pTruthDup, nIns, nOuts, NULL, 0, pIPerm );
+        //pTemp = Abc_TtGiaMinArrayNew( pTruthDup, nIns, nOuts, NULL, 0, pIPerm );
+        pTemp = Abc_TtSimpleMinArrayNew( pTruthDup, nIns, nOuts, NULL, 0, pIPerm );
         nNodes2 = Gia_ManAndNum(pTemp);
         if ( nNodesBest > nNodes2 )
         {
@@ -1046,6 +1251,14 @@ Gia_Man_t * Gia_TryPermOptNew( word * pTruths, int nIns, int nOuts, int nWords,
             pTemp = NULL;
         }
         Gia_ManStopP( &pTemp );
+/*
+        for ( i = 0; i <= nOuts; i++ )
+        {
+            Abc_TtUnpermute( pTruthDup + i*nWords, pIPerm, nIns );
+            if ( !Abc_TtEqual(pTruthDup + i*nWords, pTruths + i*nWords, nWords) )
+                printf( "Verification failed for output %d (out of %d).\n", i, nOuts );
+        }
+*/
         Abc_TtCopy( pTruthDup, pTruths, (nOuts+1)*nWords, 0 );
         if ( fVerbose )
             printf( "Permuted = %5d.  AIG = %5d.\n", nNodesAll, nNodes2 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8fd38473..9ab01a90 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -41464,9 +41464,9 @@ int Abc_CommandAbc9LNetOpt( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Gia_Man_t * Gia_ManPerformLNetOptNew( Gia_Man_t * p, char * pFileName, int nIns, int nOuts, int Thresh, int nRounds, int fVerbose );
     Gia_Man_t * pTemp;
     char * pFileName = NULL;
-    int c, fTryNew = 1, nIns = 6, nOuts = 2, Limit = 0, nRounds = 100, fVerbose = 0;
+    int c, nIns = 6, nOuts = 2, Limit = 0, nRounds = 20, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "IORXxvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IORXvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -41506,9 +41506,6 @@ int Abc_CommandAbc9LNetOpt( Abc_Frame_t * pAbc, int argc, char ** argv )
             nRounds = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
-        case 'x':
-            fTryNew ^= 1;
-            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -41542,13 +41539,12 @@ int Abc_CommandAbc9LNetOpt( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &lnetopt [-IORX num] [-xvh] <file>\n" );
+    Abc_Print( -2, "usage: &lnetopt [-IORX num] [-vh] <file>\n" );
     Abc_Print( -2, "\t           performs specialized AIG optimization\n" );
     Abc_Print( -2, "\t-I num   : the input support size [default = %d]\n",                 nIns );
     Abc_Print( -2, "\t-O num   : the output group size [default = %d]\n",                  nOuts );
     Abc_Print( -2, "\t-R num   : patterns are cares starting this value [default = %d]\n", Limit );
     Abc_Print( -2, "\t-X num   : the number of optimization rounds [default = %d]\n",      nRounds );
-    Abc_Print( -2, "\t-x       : toggles using another computation [default = %s]\n",      fTryNew? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n",                 fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");
     Abc_Print( -2, "\t<file>   : file name with simulation information\n");
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 4c4b1422..7f3a7dd1 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -399,7 +399,23 @@ static inline int Abc_TtIntersect( word * pIn1, word * pIn2, int nWords, int fCo
     }
     return 0;
 }
-static inline int Abc_TtIntersectOne( word * pOut, int fComp, word * pIn, int fComp0, int nWords )
+static inline int Abc_TtIntersectCare( word * pIn1, word * pIn2, word * pCare, int nWords, int fCompl )
+{
+    int w;
+    if ( fCompl )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( ~pIn1[w] & pIn2[w] & pCare[w] )
+                return 1;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( pIn1[w] & pIn2[w] & pCare[w] )
+                return 1;
+    }
+    return 0;
+}static inline int Abc_TtIntersectOne( word * pOut, int fComp, word * pIn, int fComp0, int nWords )
 {
     int w;
     if ( fComp0 )
@@ -542,6 +558,23 @@ static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords )
             return 0;
     return 1;
 }
+static inline int Abc_TtEqualCare( word * pIn1, word * pIn2, word * pCare, int fComp, int nWords )
+{
+    int w;
+    if ( fComp )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( (~pIn1[w] ^ pIn2[w]) & pCare[w] )
+                return 0;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( (pIn1[w] ^ pIn2[w]) & pCare[w] )
+                return 0;
+    }
+    return 1;
+}
 static inline int Abc_TtOpposite( word * pIn1, word * pIn2, int nWords )
 {
     int w;
@@ -1804,6 +1837,25 @@ static inline word Abc_Tt6Permute_rec( word t, int * pPerm, int nVars )
 }
 static inline void Abc_TtPermute( word * p, int * pPerm, int nVars )
 {
+    int v, UnPerm[16], Perm[16];
+    assert( nVars <= 16 );
+    for ( v = 0; v < nVars; v++ )
+        UnPerm[v] = Perm[v] = v;
+    for ( v = nVars-1; v >= 0; v-- )
+    {
+        int Lev = UnPerm[pPerm[v]];
+        if ( v == Lev )
+            continue;
+        Abc_TtSwapVars( p, nVars, v, Lev );
+        ABC_SWAP( int, Perm[v], Perm[Lev] );
+        UnPerm[Perm[Lev]] = Lev;
+        UnPerm[Perm[v]] = v;
+    }
+    for ( v = 0; v < nVars; v++ )
+        assert( Perm[v] == pPerm[v] );
+}
+static inline void Abc_TtUnpermute( word * p, int * pPerm, int nVars )
+{
     int v, Perm[16];
     assert( nVars <= 16 );
     for ( v = 0; v < nVars; v++ )
@@ -1818,6 +1870,8 @@ static inline void Abc_TtPermute( word * p, int * pPerm, int nVars )
             Perm[vCur]= vCur;
         }
     }
+    for ( v = 0; v < nVars; v++ )
+        assert( Perm[v] == v );
 }
 
 /**Function*************************************************************