Updating &if for new cut function representation.

6 files changed, 66 insertions, 16 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 697f7e6f..0416dd3d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14762,7 +14762,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     fLutMux = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGNDEWSTqaflepmrsdbugyojiknvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGNDEWSTqaflepmrsdbugyojikncvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -14949,6 +14949,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'n':
             pPars->fUseDsd ^= 1;
             break;
+        case 'c':
+            pPars->fUseTtPerm ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -15110,7 +15113,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->nLutSize    =  pPars->nGateSize;
     }
 
-    if ( pPars->fUseDsd )
+    if ( pPars->fUseDsd || pPars->fUseTtPerm )
     {
         pPars->fTruth      =  1;
         pPars->fCutMin     =  1;
@@ -15213,7 +15216,7 @@ usage:
         sprintf(LutSize, "library" );
     else
         sprintf(LutSize, "%d", pPars->nLutSize );
-    Abc_Print( -2, "usage: if [-KCFANGT num] [-DEW float] [-S str] [-qarlepmsdbugyojikcnvh]\n" );
+    Abc_Print( -2, "usage: if [-KCFANGT num] [-DEW float] [-S str] [-qarlepmsdbugyojikncvh]\n" );
     Abc_Print( -2, "\t           performs FPGA technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -15245,6 +15248,7 @@ usage:
     Abc_Print( -2, "\t-i       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" );
     Abc_Print( -2, "\t-k       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck10? "yes": "no" );
     Abc_Print( -2, "\t-n       : toggles computing DSDs of the cut functions [default = %s]\n", pPars->fUseDsd? "yes": "no" );
+    Abc_Print( -2, "\t-c       : toggles computing truth tables in a new way [default = %s]\n", pPars->fUseTtPerm? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");
     return 1;
@@ -29499,7 +29503,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     pPars->pLutLib = (If_LibLut_t *)pAbc->pLibLut;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgyojikfuztnvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgyojikfuztncvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -29692,6 +29696,9 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'n':
             pPars->fUseDsd ^= 1;
             break;
+        case 'c':
+            pPars->fUseTtPerm ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -29855,8 +29862,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->nLutSize    =  pPars->nGateSize;
     }
 
-
-    if ( pPars->fUseDsd )
+    if ( pPars->fUseDsd || pPars->fUseTtPerm )
     {
         pPars->fTruth      =  1;
         pPars->fCutMin     =  1;
@@ -29918,7 +29924,7 @@ usage:
         sprintf(LutSize, "library" );
     else
         sprintf(LutSize, "%d", pPars->nLutSize );
-    Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgyojikfucztnvh]\n" );
+    Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgyojikfucztncvh]\n" );
     Abc_Print( -2, "\t           performs FPGA technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -29952,6 +29958,7 @@ usage:
     Abc_Print( -2, "\t-z       : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" );
     Abc_Print( -2, "\t-t       : toggles repacking LUTs into new structures [default = %s]\n", pPars->fRepack? "yes": "no" );
     Abc_Print( -2, "\t-n       : toggles computing DSDs of the cut functions [default = %s]\n", pPars->fUseDsd? "yes": "no" );
+    Abc_Print( -2, "\t-c       : toggles computing truth tables in a new way [default = %s]\n", pPars->fUseTtPerm? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");
     return 1;
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 591361ba..320139a0 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -38,6 +38,7 @@
 #include "misc/vec/vecMem.h"
 #include "misc/util/utilTruth.h"
 #include "opt/dau/dau.h"
+#include "misc/vec/vecHash.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -125,6 +126,7 @@ struct If_Par_t_
     int                fEnableCheck75;// enable additional checking
     int                fEnableCheck75u;// enable additional checking
     int                fUseDsd;       // compute DSD of the cut functions
+    int                fUseTtPerm;    // compute truth tables of the cut functions
     int                fDeriveLuts;   // enables deriving LUT structures
     int                fRepack;       // repack after mapping
     int                fVerbose;      // the verbosity flag
@@ -235,6 +237,7 @@ struct If_Man_t_
     Vec_Mem_t *        vTtMem;        // truth table memory and hash table
     Vec_Int_t *        vTtDsds;       // mapping of truth table into DSD
     Vec_Str_t *        vTtPerms;      // mapping of truth table into permutations
+    Hash_IntMan_t *    vPairHash;     // hashing pairs of truth tables
     int                nBestCutSmall[2];
     int                nCountNonDec[2];
     Vec_Int_t *        vCutData;      // cut data storage
@@ -593,6 +596,7 @@ extern void            If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, I
 /*=== ifTruth.c ===========================================================*/
 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 );
 /*=== ifUtil.c ============================================================*/
 extern void            If_ManCleanNodeCopy( If_Man_t * p );
 extern void            If_ManCleanCutData( If_Man_t * p );
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index a822f0bb..15094c80 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -52,6 +52,7 @@ extern abctime s_TimeComp[4];
 If_Man_t * If_ManStart( If_Par_t * pPars )
 {
     If_Man_t * p;
+    assert( !pPars->fUseDsd || !pPars->fUseTtPerm );
     // start the manager
     p = ABC_ALLOC( If_Man_t, 1 );
     memset( p, 0, sizeof(If_Man_t) );
@@ -92,6 +93,15 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
         Vec_StrFill( p->vTtPerms, 2 * p->pPars->nLutSize, IF_BIG_CHAR );
         Vec_StrWriteEntry( p->vTtPerms, p->pPars->nLutSize, 0 );
     }
+    if ( pPars->fUseTtPerm )
+    {
+        word uTruth = 0;
+        Vec_MemHashInsert( p->vTtMem, &uTruth );
+        uTruth = ABC_CONST(0xAAAAAAAAAAAAAAAA);
+        Vec_MemHashInsert( p->vTtMem, &uTruth );
+        p->vPairHash = Hash_IntManStart( 10000 );
+        p->vTtPerms = Vec_StrAlloc( 10000 );
+    }
     // create the constant node
     p->pConst1   = If_ManSetupObj( p );
     p->pConst1->Type   = IF_CONST1;
@@ -171,8 +181,6 @@ void If_ManStop( If_Man_t * p )
     }
 //    if ( p->pPars->fVerbose && p->nCuts5 )
 //        Abc_Print( 1, "Statistics about 5-cuts: Total = %d  Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 );
-//    if ( p->pPars->fUseDsd )
-//        If_DsdManFree( p->pIfDsdMan, p->pPars->fVerbose );
     if ( p->pIfDsdMan )
         p->pIfDsdMan = NULL;
     if ( p->pPars->fUseDsd && (p->nCountNonDec[0] || p->nCountNonDec[1]) )
@@ -194,6 +202,8 @@ void If_ManStop( If_Man_t * p )
     Vec_IntFreeP( &p->vTtDsds );
     Vec_StrFreeP( &p->vTtPerms );
     Vec_IntFreeP( &p->vCutData );
+    if ( p->vPairHash )
+        Hash_IntManStop( p->vPairHash );
     Vec_MemHashFree( p->vTtMem );
     Vec_MemFreeP( &p->vTtMem );
     Mem_FixedStop( p->pMemObj, 0 );
@@ -443,9 +453,9 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId )
     pCut->pLeaves[0] = p->pPars->fLiftLeaves? (ObjId << 8) : ObjId;
     pCut->uSign      = If_ObjCutSign( pCut->pLeaves[0] );
     pCut->iCutFunc   = p->pPars->fTruth ? 2 : -1;
-    pCut->iCutDsd    = p->pPars->fUseDsd ? 2 : -1;
+    pCut->iCutDsd    = (p->pPars->fUseDsd || p->pPars->fUseTtPerm) ? 2 : -1;
     assert( pCut->pLeaves[0] < p->vObjs->nSize );
-    if ( p->pPars->fUseDsd )
+    if ( p->pPars->fUseDsd || p->pPars->fUseTtPerm )
         pCut->pPerm[0] = 0;
 }
 
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index fe4b146b..7ee7db22 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -215,7 +215,10 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         if ( p->pPars->fTruth )
         {
 //            abctime clk = Abc_Clock();
-            If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
+            if ( p->pPars->fUseTtPerm )
+                If_CutComputeTruthPerm( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
+            else
+                If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
 //            p->timeTruth += Abc_Clock() - clk;
             if ( p->pPars->fUseDsd )
             {
@@ -246,6 +249,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
             pCut->fUseless = 0;
             if ( p->pPars->pFuncCell )
             {
+                assert( p->pPars->fUseTtPerm == 0 );
                 assert( pCut->nLimit >= 4 && pCut->nLimit <= 16 );
                 if ( p->pPars->fUseDsd )
                     pCut->fUseless = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd );
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index f20936c7..9a20ac71 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void If_CutTruthPermute( word * pTruth, int nLeaves, int nVars, int nWords, float * pDelays, int * pVars )
+void If_CutTruthPermute( word * pTruth, int nLeaves, int nVars, int nWords, float * pDelays, int * pVars, char * pPerm )
 {
     while ( 1 )
     {
@@ -55,6 +55,8 @@ void If_CutTruthPermute( word * pTruth, int nLeaves, int nVars, int nWords, floa
                 continue;
             ABC_SWAP( float, pDelays[i], pDelays[i+1] );
             ABC_SWAP( int, pVars[i], pVars[i+1] );
+            if ( pPerm )
+                ABC_SWAP( char, pPerm[i], pPerm[i+1] );
             if ( pTruth )
                 Abc_TtSwapAdjacent( pTruth, nWords, i );
             fChange = 1;
@@ -72,11 +74,16 @@ void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut )
         PinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
     if ( p->vTtMem == NULL )
     {
-        If_CutTruthPermute( NULL, If_CutLeaveNum(pCut), pCut->nLimit, p->nTruth6Words, PinDelays, If_CutLeaves(pCut) );
+        If_CutTruthPermute( NULL, If_CutLeaveNum(pCut), pCut->nLimit, p->nTruth6Words, PinDelays, If_CutLeaves(pCut), NULL );
+        return;
+    }
+    if ( p->pPars->fUseTtPerm )
+    {
+        If_CutTruthPermute( NULL, If_CutLeaveNum(pCut), pCut->nLimit, p->nTruth6Words, PinDelays, If_CutLeaves(pCut), pCut->pPerm );
         return;
     }
     Abc_TtCopy( p->puTempW, If_CutTruthWR(p, pCut), p->nTruth6Words, 0 );
-    If_CutTruthPermute( p->puTempW, If_CutLeaveNum(pCut), pCut->nLimit, p->nTruth6Words, PinDelays, If_CutLeaves(pCut) );
+    If_CutTruthPermute( p->puTempW, If_CutLeaveNum(pCut), pCut->nLimit, p->nTruth6Words, PinDelays, If_CutLeaves(pCut), NULL );
     truthId        = Vec_MemHashInsert( p->vTtMem, p->puTempW );
     pCut->iCutFunc = Abc_Var2Lit( truthId, If_CutTruthIsCompl(pCut) );
     assert( (p->puTempW[0] & 1) == 0 );
@@ -133,6 +140,24 @@ int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutComputeTruthPerm( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+    int i;
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        pCut->pPerm[i] = (char)i;
+    return 0;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 90706f6f..3a84e496 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1555,7 +1555,7 @@ clk2 = Abc_Clock();
             status = Saig_ManCallSolver( p, Lit );
 clkSatRun = Abc_Clock() - clk2;
             if ( pLogFile )
-                fprintf( pLogFile, "Frame %5d  Output %5d  Time(ms) %8d\n", f, i, Lit < 2 ? 0 : clkSatRun );
+                fprintf( pLogFile, "Frame %5d  Output %5d  Time(ms) %8d\n", f, i, Lit < 2 ? 0 : (int)clkSatRun );
             if ( p->pTime4Outs )
             {
                 abctime timeSince = Abc_Clock() - clkOne;