Changes to LUT mappers.

5 files changed, 31 insertions, 251 deletions

diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index ea5ec003..b1321685 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -135,14 +135,14 @@ Vec_Int_t * Gia_ManOrderWithBoxes( Gia_Man_t * p )
             {
                 int iCiNum  = p->iData2;
                 int iBoxNum = Tim_ManBoxFindFromCiNum( pManTime, iCiNum );
-                printf( "Boxes are not in a topological order. The command has to terminate.\n" );
+                printf( "The command has to terminate. Boxes are not in a topological order.\n" );
                 printf( "The following information may help debugging (numbers are 0-based):\n" );
                 printf( "Input %d of BoxA %d (1stCI = %d; 1stCO = %d) has TFI with CI %d,\n", 
                     k, i, Tim_ManBoxOutputFirst(pManTime, i), Tim_ManBoxInputFirst(pManTime, i), iCiNum );
                 printf( "which corresponds to output %d of BoxB %d (1stCI = %d; 1stCO = %d).\n", 
                     iCiNum - Tim_ManBoxOutputFirst(pManTime, iBoxNum), iBoxNum, 
                     Tim_ManBoxOutputFirst(pManTime, iBoxNum), Tim_ManBoxInputFirst(pManTime, iBoxNum) );
-                printf( "In a correct topological order, BoxB should preceed BoxA.\n" );
+                printf( "In a correct topological order, BoxB should precede BoxA.\n" );
                 Vec_IntFree( vNodes );
                 p->iData2 = 0;
                 return NULL;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 103764ab..807b66a8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -231,6 +231,7 @@ static int Abc_CommandSuperChoiceLut         ( Abc_Frame_t * pAbc, int argc, cha
 //static int Abc_CommandFpgaFast               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIf                     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIfif                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static int Abc_CommandDsdSave                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDsdLoad                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDsdFree                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -790,11 +791,12 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga",         Abc_CommandFpgaFast,         1 );
     Cmd_CommandAdd( pAbc, "FPGA mapping", "if",            Abc_CommandIf,               1 );
     Cmd_CommandAdd( pAbc, "FPGA mapping", "ifif",          Abc_CommandIfif,             1 );
-    Cmd_CommandAdd( pAbc, "FPGA mapping", "dsd_save",      Abc_CommandDsdSave,          0 );
-    Cmd_CommandAdd( pAbc, "FPGA mapping", "dsd_load",      Abc_CommandDsdLoad,          0 );
-    Cmd_CommandAdd( pAbc, "FPGA mapping", "dsd_free",      Abc_CommandDsdFree,          0 );
-    Cmd_CommandAdd( pAbc, "FPGA mapping", "dsd_ps",        Abc_CommandDsdPs,            0 );
-    Cmd_CommandAdd( pAbc, "FPGA mapping", "dsd_tune",      Abc_CommandDsdTune,          0 );
+
+    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_save",      Abc_CommandDsdSave,          0 );
+    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_load",      Abc_CommandDsdLoad,          0 );
+    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_free",      Abc_CommandDsdFree,          0 );
+    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_ps",        Abc_CommandDsdPs,            0 );
+    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_tune",      Abc_CommandDsdTune,          0 );
 
 //    Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
@@ -15586,9 +15588,9 @@ usage:
 ***********************************************************************/
 int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    int c, fVerbose = 0, fFast = 0, fSpec = 0, LutSize = 0;
+    int c, fVerbose = 0, fFast = 0, fAdd = 0, fSpec = 0, LutSize = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Kfsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Kfasvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15606,6 +15608,9 @@ int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             fFast ^= 1;
             break;
+        case 'a':
+            fAdd ^= 1;
+            break;
         case 's':
             fSpec ^= 1;
             break;
@@ -15623,14 +15628,15 @@ int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "The DSD manager is not started.\n" );
         return 0;
     }
-    If_DsdManTune( (If_DsdMan_t *)Abc_FrameReadManDsd(), LutSize, fFast, fSpec, fVerbose );
+    If_DsdManTune( (If_DsdMan_t *)Abc_FrameReadManDsd(), LutSize, fFast, fAdd, fSpec, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dsd_tune [-K num] [-fsvh]\n" );
+    Abc_Print( -2, "usage: dsd_tune [-K num] [-fasvh]\n" );
     Abc_Print( -2, "\t         tunes DSD manager for the given LUT size\n" );
     Abc_Print( -2, "\t-K num : LUT size used for tuning [default = %d]\n",        LutSize );
     Abc_Print( -2, "\t-f     : toggles using fast check [default = %s]\n",        fFast? "yes": "no" );
+    Abc_Print( -2, "\t-a     : toggles adding tuning to the current one [default = %s]\n",    fAdd? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggles using specialized check [default = %s]\n", fSpec? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggles verbose output [default = %s]\n",          fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 60bdfa3c..30a8d0d8 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -520,7 +520,7 @@ extern int             If_CluCheckExt3( void * p, word * pTruth, int nVars, int
 extern If_DsdMan_t *   If_DsdManAlloc( int nVars, int nLutSize );
 extern void            If_DsdManDump( If_DsdMan_t * p );
 extern void            If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int fVerbose );
-extern void            If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVerbose );
+extern void            If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose );
 extern void            If_DsdManFree( If_DsdMan_t * p, int fVerbose );
 extern void            If_DsdManSave( If_DsdMan_t * p, char * pFileName );
 extern If_DsdMan_t *   If_DsdManLoad( char * pFileName );
@@ -575,12 +575,10 @@ extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, i
 extern void            If_ManImproveMapping( If_Man_t * p );
 /*=== ifSat.c ==========================================================*/
 extern void *          If_ManSatBuildXY( int nLutSize );
-extern void *          If_ManSatBuild55();
 extern void *          If_ManSatBuildXYZ( int nLutSize );
 extern void            If_ManSatUnbuild( void * p );
 extern int             If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits );
 extern unsigned        If_ManSatCheckXYall( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits );
-extern unsigned        If_ManSatCheck55all( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits );
 /*=== ifSeq.c =============================================================*/
 extern int             If_ManPerformMappingSeq( If_Man_t * p );
 /*=== ifTime.c ============================================================*/
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 6269b5b6..7afec99e 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -875,48 +875,6 @@ int If_DsdManCheckInv_rec( If_DsdMan_t * p, int iLit )
     assert( 0 );
     return 0;
 }
-/*
-int If_DsdManPushInv_rec( If_DsdMan_t * p, int iLit, unsigned char * pPerm )
-{
-    If_DsdObj_t * pObj;
-    int i, iFanin, RetValue;
-    pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iLit) );
-    if ( If_DsdObjType(pObj) == IF_DSD_VAR )
-    {
-        pPerm[0] = (unsigned char)Abc_LitNot((int)pPerm[0]);
-        return 1;
-    }
-    if ( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_PRIME )
-        return 0;
-    if ( If_DsdObjType(pObj) == IF_DSD_XOR )
-    {
-        If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
-        {
-            if ( If_DsdManCheckInv_rec(p, iFanin) )
-            {
-                RetValue = If_DsdManPushInv_rec(p, iFanin, pPerm);  assert( RetValue );
-                return 1;
-            }
-            pPerm += If_DsdVecLitSuppSize(p->vObjs, iFanin);
-        }
-        return 0;
-    }
-    if ( If_DsdObjType(pObj) == IF_DSD_MUX )
-    {
-        if ( If_DsdManCheckInv_rec(p, pObj->pFans[1]) && If_DsdManCheckInv_rec(p, pObj->pFans[2]) )
-        {
-            pPerm += If_DsdVecLitSuppSize(p->vObjs, pObj->pFans[0]);
-            RetValue = If_DsdManPushInv_rec(p, pObj->pFans[1], pPerm);  assert( RetValue );
-            pPerm += If_DsdVecLitSuppSize(p->vObjs, pObj->pFans[1]);
-            RetValue = If_DsdManPushInv_rec(p, pObj->pFans[2], pPerm);  assert( RetValue );
-            return 1;
-        }
-        return 0;
-    }
-    assert( 0 );
-    return 0;
-}
-*/
 int If_DsdManPushInv_rec( If_DsdMan_t * p, int iLit, unsigned char * pPerm )
 {
     If_DsdObj_t * pObj;
@@ -1577,20 +1535,18 @@ void If_DsdManTest()
   SeeAlso     []
 
 ***********************************************************************/
-void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVerbose )
+void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose )
 {
     ProgressBar * pProgress = NULL;
     If_DsdObj_t * pObj;
     sat_solver * pSat = NULL;
-    sat_solver * pSat5 = NULL;
     Vec_Int_t * vLits = Vec_IntAlloc( 1000 );
     int i, Value, nVars;
     word * pTruth;
     pSat = (sat_solver *)If_ManSatBuildXY( LutSize );
-    if ( LutSize == 5 && fSpec )
-        pSat5 = (sat_solver *)If_ManSatBuild55();
-    If_DsdVecForEachObj( p->vObjs, pObj, i )
-        pObj->fMark = 0;
+    if ( !fAdd )
+        If_DsdVecForEachObj( p->vObjs, pObj, i )
+            pObj->fMark = 0;
     pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(p->vObjs) );
     If_DsdVecForEachObj( p->vObjs, pObj, i )
     {
@@ -1598,37 +1554,17 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVer
         nVars = If_DsdObjSuppSize(pObj);
         if ( nVars <= LutSize )
             continue;
-        if ( LutSize == 5 && fSpec )
-        {
-            if ( nVars == 9 )
-            {
-                pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
-                Value = If_ManSatCheck55all( pSat5, pTruth, nVars, vLits );
-            }
-            else
-            {
-                if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0) )
-                    continue;
-                if ( fFast )
-                    Value = 0;
-                else
-                {
-                    pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
-                    Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits );
-                }
-            }
-        }
+        if ( fAdd && !pObj->fMark )
+            continue;
+        pObj->fMark = 0;
+        if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0) )
+            continue;
+        if ( fFast )
+            Value = 0;
         else
         {
-            if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0) )
-                continue;
-            if ( fFast )
-                Value = 0;
-            else
-            {
-                pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
-                Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits );
-            }
+            pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
+            Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits );
         }
         if ( Value )
             continue;
@@ -1636,7 +1572,6 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVer
     }
     if ( pProgress )
         Extra_ProgressBarStop( pProgress );
-    If_ManSatUnbuild( pSat5 );
     If_ManSatUnbuild( pSat );
     Vec_IntFree( vLits );
     if ( fVerbose )
diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c
index 9f4ea631..4af55203 100644
--- a/src/map/if/ifSat.c
+++ b/src/map/if/ifSat.c
@@ -82,27 +82,6 @@ void * If_ManSatBuildXYZ( int nLutSize )
             iVarM + m );
     return p;
 }
-void * If_ManSatBuild55()
-{
-    int nMintsL =  16;
-    int nMintsF = 512;
-    int nVars   = 2 * nMintsL + nMintsF;
-    int iVarP0  = 0;           // LUT0 parameters (total nMintsL)
-    int iVarP1  = nMintsL;     // LUT1 parameters (total nMintsL)
-    int m,iVarM = 2 * nMintsL; // MUX vars        (total nMintsF)
-    sat_solver * p = sat_solver_new();
-    sat_solver_setnvars( p, nVars );
-    for ( m = 0; m < nMintsF; m++ )
-    {
-        int iVar0 = (((m >> 2) & 7) << 1) | ((m & 3) == 3);
-        int iVar1 =  ((m >> 6) & 7);
-        if ( (m >> 5) & 1 )
-            sat_solver_add_mux( p, iVarP0 + iVar0, iVarP1 + 2 * iVar1 + 1, iVarP1 + 2 * iVar1, iVarM + m );
-        else
-            sat_solver_add_buffer( p, iVarP1 + 2 * iVar1, iVarM + m, 0 );
-    }
-    return p;
-}
 void If_ManSatUnbuild( void * p )
 {
     if ( p )
@@ -268,128 +247,6 @@ int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsig
     }
     return 1;
 }
-int If_ManSatCheck55( void * pSat, word * pTruth, int nVars, int * pPerm9, word * pTBound, word * pTFree, Vec_Int_t * vLits )
-{
-    sat_solver * p = (sat_solver *)pSat;
-    int v, Value, m, mNew;
-    int nMintsL = 16;
-    // remap minterms
-    Vec_IntFill( vLits, 512, -1 );
-    for ( m = 0; m < (1 << nVars); m++ )
-    {
-        mNew = 0;
-        for ( v = 0; v < 9; v++ )
-        {
-            assert( pPerm9[v] < nVars );
-            if ( ((m >> pPerm9[v]) & 1) )
-                mNew |= (1 << v);
-        }
-        assert( Vec_IntEntry(vLits, mNew) == -1 );
-        Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
-    }
-    // find assumptions
-    v = 0;
-    Vec_IntForEachEntry( vLits, Value, m )
-        if ( Value >= 0 )
-            Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) );
-    Vec_IntShrink( vLits, v );
-    // run SAT solver
-    Value = sat_solver_solve( p, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
-    if ( Value != l_True )
-        return 0;
-    if ( pTBound && pTFree )
-    {
-        // collect config
-        *pTBound = 0;
-        for ( m = 0; m < nMintsL; m++ )
-            if ( sat_solver_var_value(p, m) )
-                Abc_TtSetBit( pTBound, m );
-        *pTBound = Abc_Tt6Stretch( *pTBound, 4 );
-        // collect configs
-        *pTFree = 0;
-        for ( m = 0; m < nMintsL; m++ )
-            if ( sat_solver_var_value(p, nMintsL+m) )
-                Abc_TtSetBit( pTFree, m );
-        *pTFree = Abc_Tt6Stretch( *pTFree, 4 );
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns config string for the given truth table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned If_ManSatCheck55all_int( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits )
-{
-    int Combs[10][5] = {
-        {0,1,2,3,4}, 
-        {0,2,1,3,4}, 
-        {0,3,1,2,4}, 
-        {0,4,1,2,3}, 
-        {1,2,0,3,4}, 
-        {1,3,0,2,4}, 
-        {1,4,0,2,3}, 
-        {2,3,0,1,4}, 
-        {2,4,0,1,3}, 
-        {3,4,0,1,2}
-    };
-    int pPerm9[9], Mark[9], i[6], k, n, c;
-    assert( nVars == 9 || nVars == 8 || nVars == 7 );
-    for ( i[0] = 0;      i[0] < nVars; i[0]++ )
-    for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
-    for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
-    for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
-    for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
-    {
-        // add remaining ones
-        n = 5;
-        for ( k = 0; k < nVars; k++ )
-            Mark[k] = 0;
-        for ( k = 0; k < 5; k++ )
-            Mark[i[k]] = 1;
-        for ( k = 0; k < nVars; k++ )
-            if ( Mark[k] == 0 )
-                pPerm9[n++] = k;
-        assert( n == nVars );
-        for ( ; n < 9; n++ )
-            pPerm9[n] = pPerm9[n-1];
-        assert( n == 9 );
-        // current ones
-        for ( c = 0; c < 10; c++ )
-        {
-            for ( n = 0; n < 5; n++ )
-                pPerm9[n] = i[Combs[c][n]];
-            // try different combinations
-            for ( k = 5; k < nVars; k++ )
-            {
-                ABC_SWAP( int, pPerm9[5], pPerm9[k] );
-                if ( If_ManSatCheck55(pSat, pTruth, nVars, pPerm9, NULL, NULL, vLits) )
-                {
-//                    for ( k = 0; k < 9; k++ )
-//                        printf( "%c", 'a' + pPerm9[k] );
-//                    printf( "\n" );
-                    return 1;
-                }
-                ABC_SWAP( int, pPerm9[5], pPerm9[k] );
-            }
-        }
-    }
-    return 0;
-}
-unsigned If_ManSatCheck55all( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits )
-{
-//    abctime clk = Abc_Clock();
-    unsigned Value = If_ManSatCheck55all_int( pSat, pTruth, nVars, vLits );
-//    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-    return Value;
-}
 
 /**Function*************************************************************
 
@@ -680,22 +537,6 @@ void If_ManSatTest3()
     sat_solver_delete(p);
     Vec_IntFree( vLits );
 }
-void If_ManSatTest()
-{
-    int nVars = 9;
-    sat_solver * p = (sat_solver *)If_ManSatBuild55();
-//    char * pDsd = "[([(ab)cde]f)ghi]";
-//    char * pDsd = "[([(hi)cde]f)gab]";
-    char * pDsd = "[(0123{(hi)cde}f)gab]";
-    word * pTruth = Dau_DsdToTruth( pDsd, nVars );
-    Vec_Int_t * vLits = Vec_IntAlloc( 1000 );
-    if ( If_ManSatCheck55all( p, pTruth, nVars, vLits ) )
-        printf( "Found!\n" );
-    else
-        printf( "Not found!\n" );
-    sat_solver_delete(p);
-    Vec_IntFree( vLits );
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///