Adding switch to &if to consider special type of 6-input cuts.

7 files changed, 151 insertions, 3 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4eafa0b9..69d6db89 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36701,7 +36701,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->fExpRed ^= 1;
             break;
         case 'l':
-            pPars->fLatchPaths ^= 1;
+            pPars->fLut6Filter ^= 1;
             break;
         case 'e':
             pPars->fEdge ^= 1;
@@ -36961,7 +36961,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->nLutSize    =  pPars->nGateSize;
     }
 
-    if ( pPars->fUseDsd || pPars->fUseTtPerm )
+    if ( pPars->fUseDsd || pPars->fUseTtPerm || pPars->fLut6Filter )
     {
         pPars->fTruth      =  1;
         pPars->fCutMin     =  1;
@@ -37077,7 +37077,8 @@ usage:
     Abc_Print( -2, "\t-q       : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
     Abc_Print( -2, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
     Abc_Print( -2, "\t-r       : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
-    Abc_Print( -2, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
+//    Abc_Print( -2, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
+    Abc_Print( -2, "\t-l       : toggle restricting the type of 6-input lookup tables [default = %s]\n", pPars->fLut6Filter? "yes": "no" );
     Abc_Print( -2, "\t-e       : uses edge-based cut selection heuristics [default = %s]\n", pPars->fEdge? "yes": "no" );
     Abc_Print( -2, "\t-p       : uses power-aware cut selection heuristics [default = %s]\n", pPars->fPower? "yes": "no" );
     Abc_Print( -2, "\t-m       : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index eb81d64e..aa9608c9 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -117,6 +117,7 @@ struct If_Par_t_
     int                fFancy;        // a fancy feature
     int                fExpRed;       // expand/reduce of the best cuts
     int                fLatchPaths;   // reset timing on latch paths
+    int                fLut6Filter;   // uses filtering of 6-LUT functions
     int                fEdge;         // uses edge-based cut selection heuristics
     int                fPower;        // uses power-aware cut selection heuristics
     int                fCutMin;       // performs cut minimization by removing functionally reducdant variables
@@ -260,6 +261,7 @@ struct If_Man_t_
     Hash_IntMan_t *    vPairHash;     // hashing pairs of truth tables
     Vec_Int_t *        vPairRes;      // resulting truth table
     Vec_Str_t *        vPairPerms;    // resulting permutation
+    Vec_Mem_t *        vTtMem6;
     char               pCanonPerm[IF_MAX_LUTSIZE];
     unsigned           uCanonPhase;
     int                nCacheHits;
@@ -652,6 +654,8 @@ extern void            If_ManComputeRequired( If_Man_t * p );
 extern void            If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
 extern int             If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
 extern int             If_CutComputeTruthPerm( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
+extern Vec_Mem_t *     If_DeriveHashTable6( int nVars, word Truth );
+extern int             If_CutCheckTruth6( If_Man_t * p, If_Cut_t * pCut );
 /*=== ifTune.c ===========================================================*/
 extern Ifn_Ntk_t *     Ifn_NtkParse( char * pStr );
 extern int             Ifn_NtkTtBits( char * pStr );
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 27d7245e..4027b780 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -284,6 +284,11 @@ void If_ManStop( If_Man_t * p )
     for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ )
         Vec_IntFreeP( &p->vTtOccurs[i] );
     Mem_FixedStop( p->pMemObj, 0 );
+    if ( p->vTtMem6 )
+    {
+        Vec_MemHashFree( p->vTtMem6 );
+        Vec_MemFreeP( &p->vTtMem6 );
+    }
     ABC_FREE( p->pMemCi );
     ABC_FREE( p->pMemAnd );
     ABC_FREE( p->puTemp[0] );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index b5ae6b11..afeba005 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -292,6 +292,8 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                 p->timeCache[4] += Abc_Clock() - clk;
             if ( !p->pPars->fSkipCutFilter && fChange && If_CutFilter( pCutSet, pCut, fSave0 ) )
                 continue;
+            if ( p->pPars->fLut6Filter && pCut->nLeaves == 6 && !If_CutCheckTruth6(p, pCut) )
+                continue;
             if ( p->pPars->fUseDsd )
             {
                 extern void If_ManCacheRecord( If_Man_t * p, int iDsd0, int iDsd1, int nShared, int iDsd );
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index 7c8892d3..83c40952 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -330,6 +330,79 @@ p->timeCache[2] += Abc_Clock() - clk;
     return 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Check the function of 6-input LUT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Mem_t * If_DeriveHashTable6( int nVars, word uTruth )
+{
+    int fVerbose = 0;
+    int nMints   = (1 << nVars);
+    int nPerms   = Extra_Factorial( nVars );
+    int * pComp  = Extra_GreyCodeSchedule( nVars );
+    int * pPerm  = Extra_PermSchedule( nVars );
+    word Canon   = ABC_CONST(0xFFFFFFFFFFFFFFFF);
+    word tCur, tTemp1, tTemp2;
+    Vec_Mem_t * vTtMem6 = Vec_MemAllocForTTSimple( nVars );
+    int i, p, c;
+    for ( i = 0; i < 2; i++ )
+    {
+        tCur = i ? ~uTruth : uTruth;
+        tTemp1 = tCur;
+        for ( p = 0; p < nPerms; p++ )
+        {
+            tTemp2 = tCur;
+            for ( c = 0; c < nMints; c++ )
+            {
+                if ( Canon > tCur )
+                    Canon = tCur;
+                Vec_MemHashInsert( vTtMem6, &tCur );
+                tCur = Abc_Tt6Flip( tCur, pComp[c] );
+            }
+            assert( tTemp2 == tCur );
+            tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[p] );
+        }
+        assert( tTemp1 == tCur );
+    }
+    ABC_FREE( pComp );
+    ABC_FREE( pPerm );
+    if ( fVerbose )
+    {
+/*
+        word * pEntry;
+        Vec_MemForEachEntry( vTtMem6, pEntry, i )
+        {
+            Extra_PrintHex( stdout, (unsigned*)pEntry, nVars );  
+            printf( ", " );
+            if ( i % 4 == 3 )
+                printf( "\n" );
+        }
+*/
+        Extra_PrintHex( stdout, (unsigned*)&uTruth, nVars );  printf( "\n" );
+        Extra_PrintHex( stdout, (unsigned*)&Canon,  nVars );  printf( "\n" );
+        printf( "Members = %d.\n", Vec_MemEntryNum(vTtMem6) );
+    }
+    return vTtMem6;
+}
+
+int If_CutCheckTruth6( If_Man_t * p, If_Cut_t * pCut )
+{
+    if ( pCut->nLeaves != 6 )
+        return 0;
+    if ( p->vTtMem6 == NULL )
+        p->vTtMem6 = If_DeriveHashTable6( 6, ABC_CONST(0xfedcba9876543210) );
+    if ( *Vec_MemHashLookup( p->vTtMem6, If_CutTruthWR(p, pCut) ) == -1 )
+        return 0;
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecMem.h b/src/misc/vec/vecMem.h
index ef2d2af7..e8ddd44a 100644
--- a/src/misc/vec/vecMem.h
+++ b/src/misc/vec/vecMem.h
@@ -397,6 +397,13 @@ static int Vec_MemHashInsert( Vec_Mem_t * p, word * pEntry )
   SeeAlso     []
 
 ***********************************************************************/
+static inline Vec_Mem_t * Vec_MemAllocForTTSimple( int nVars )
+{
+    int nWords = (nVars <= 6 ? 1 : (1 << (nVars - 6)));
+    Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 12 );
+    Vec_MemHashAlloc( vTtMem, 10000 );
+    return vTtMem;
+}
 static inline Vec_Mem_t * Vec_MemAllocForTT( int nVars, int fCompl )
 {
     int Value, nWords = (nVars <= 6 ? 1 : (1 << (nVars - 6)));
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c
index 66ee2fb7..d6cf10a9 100644
--- a/src/proof/acec/acecMult.c
+++ b/src/proof/acec/acecMult.c
@@ -158,6 +158,62 @@ unsigned s_Classes4c[768] = {
   SeeAlso     []
 
 ***********************************************************************/
+word Extra_TruthCanonNPN3( word uTruth, int nVars, Vec_Wrd_t * vRes )
+{
+    int nMints  = (1 << nVars);
+    int nPerms  = Extra_Factorial( nVars );
+    int * pComp = Extra_GreyCodeSchedule( nVars );
+    int * pPerm = Extra_PermSchedule( nVars );
+    word tCur, tTemp1, tTemp2;
+    word uTruthMin = ABC_CONST(0xFFFFFFFFFFFFFFFF);
+    int i, p, c;
+    Vec_WrdClear( vRes );
+    for ( i = 0; i < 2; i++ )
+    {
+        tCur = i ? ~uTruth : uTruth;
+        tTemp1 = tCur;
+        for ( p = 0; p < nPerms; p++ )
+        {
+            tTemp2 = tCur;
+            for ( c = 0; c < nMints; c++ )
+            {
+                if ( uTruthMin > tCur )
+                    uTruthMin = tCur;
+                Vec_WrdPushUnique( vRes, tCur );
+                tCur = Abc_Tt6Flip( tCur, pComp[c] );
+            }
+            assert( tTemp2 == tCur );
+            tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[p] );
+        }
+        assert( tTemp1 == tCur );
+    }
+    ABC_FREE( pComp );
+    ABC_FREE( pPerm );
+    return uTruthMin;
+}
+void Acec_MultFuncTest6()
+{
+    Vec_Wrd_t * vRes = Vec_WrdAlloc( 10000 );
+    int i; word Entry;
+
+    word Truth = ABC_CONST(0xfedcba9876543210);
+    word Canon = Extra_TruthCanonNPN3( Truth, 6, vRes );
+
+    Extra_PrintHex( stdout, (unsigned*)&Truth, 6 );  printf( "\n" );
+    Extra_PrintHex( stdout, (unsigned*)&Canon, 6 );  printf( "\n" );
+
+    printf( "Members = %d.\n", Vec_WrdSize(vRes) );
+    Vec_WrdForEachEntry( vRes, Entry, i )
+    {
+        Extra_PrintHex( stdout, (unsigned*)&Entry, 6 );  
+        printf( ", " );
+        if ( i % 8 == 7 )
+            printf( "\n" );
+    }
+
+    Vec_WrdFree( vRes );
+}
+
 unsigned Extra_TruthCanonNPN2( unsigned uTruth, int nVars, Vec_Int_t * vRes )
 {
     static int nVarsOld, nPerms;