Improvements to technology mapping.

src/aig/gia/giaIf.c

@@ -1192,6 +1192,7 @@ int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * p
         }
         return RetValue;
     }
+    assert( If_DsdManSuppSize(pIfMan->pIfDsdMan, pCutBest->iCutDsd) == (int)pCutBest->nLeaves );
     // find the bound set
     uSetOld = If_DsdManCheckXY( pIfMan->pIfDsdMan, pCutBest->iCutDsd, nLutSize, 1, 1, 0 );
     // remap bound set
@@ -1313,7 +1314,7 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
                 word * pTruth = If_CutTruthW(pIfMan, pCutBest);
                 if ( pIfMan->pPars->fUseTtPerm )
                     for ( k = 0; k < (int)pCutBest->nLeaves; k++ )
-                        if ( (pCutBest->iCutDsd >> k) & 1 )
+                        if ( If_CutLeafBit(pCutBest, k) )
                             Abc_TtFlip( pTruth, Abc_TtWordNum(pCutBest->nLimit), k );
                 // perform decomposition of the cut
                 pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, pTruth, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u), pIfMan->pPars->fEnableCheck07 );

src/base/abci/abcIf.c

@@ -500,7 +500,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
             word * pTruth = If_CutTruthW(pIfMan, pCutBest);
             if ( pIfMan->pPars->fUseTtPerm )
                 for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
-                    if ( (pCutBest->iCutDsd >> i) & 1 )
+                    if ( If_CutLeafBit(pCutBest, i) )
                         Abc_TtFlip( pTruth, Abc_TtWordNum(pCutBest->nLimit), i );
             pNodeNew->pData = Kit_TruthToHop( (Hop_Man_t *)pNtkNew->pManFunc, (unsigned *)pTruth, If_CutLeaveNum(pCutBest), vCover );
         }

src/map/if/if.h

@@ -233,10 +233,10 @@ struct If_Man_t_
     int                nCutsCountAll;
     int                nCutsUselessAll;
     int                nCuts5, nCuts5a;
-    Vec_Mem_t *        vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table
     If_DsdMan_t *      pIfDsdMan;     // DSD manager
-    Vec_Int_t *        vTtDsds;       // mapping of truth table into DSD
-    Vec_Str_t *        vTtPerms;      // mapping of truth table into permutations
+    Vec_Mem_t *        vTtMem[IF_MAX_FUNC_LUTSIZE+1];   // truth table memory and hash table
+    Vec_Int_t *        vTtDsds[IF_MAX_FUNC_LUTSIZE+1];  // mapping of truth table into DSD
+    Vec_Str_t *        vTtPerms[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into permutations
     Hash_IntMan_t *    vPairHash;     // hashing pairs of truth tables
     Vec_Int_t *        vPairRes;      // resulting truth table
     Vec_Str_t *        vPairPerms;    // resulting permutation
@@ -543,6 +543,7 @@ extern int             If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLe
 extern char *          If_DsdManFileName( If_DsdMan_t * p );
 extern int             If_DsdManVarNum( If_DsdMan_t * p );
 extern int             If_DsdManLutSize( If_DsdMan_t * p );
+extern int             If_DsdManSuppSize( If_DsdMan_t * p, int iDsd );
 extern int             If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
 extern unsigned        If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fHighEffort, int fVerbose );
 /*=== ifLib.c =============================================================*/

src/map/if/ifCut.c

@@ -859,7 +859,7 @@ void If_CutPrint( If_Cut_t * pCut )
     unsigned i;
     Abc_Print( 1, "{" );
     for ( i = 0; i < pCut->nLeaves; i++ )
-        Abc_Print( 1, " %s%d", ((pCut->iCutDsd >> i) & 1) ? "!":"", pCut->pLeaves[i] );
+        Abc_Print( 1, " %s%d", If_CutLeafBit(pCut, i) ? "!":"", pCut->pLeaves[i] );
     Abc_Print( 1, " }\n" );
 }
 

src/map/if/ifDsd.c

@@ -150,6 +150,10 @@ int If_DsdManLutSize( If_DsdMan_t * p )
 {
     return p->LutSize;
 }
+int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd )
+{
+    return If_DsdVecLitSuppSize( &p->vObjs, iDsd );
+}
 int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
 {
     return If_DsdVecObjMark( &p->vObjs, Abc_Lit2Var(iDsd) );
@@ -845,10 +849,10 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word
 {
     int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem[nLits], pTruth) : -1;
     unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
-abctime clk;
+//abctime clk;
     if ( *pSpot )
         return (int)*pSpot;
-clk = Abc_Clock();
+//clk = Abc_Clock();
     if ( p->LutSize && truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs[nLits]) )
     {
         Vec_Int_t * vSets = Dau_DecFindSets_int( pTruth, nLits, p->pSched );
@@ -863,7 +867,7 @@ clk = Abc_Clock();
 //        printf( "%d ", Gia_ManAndNum(p->pTtGia)-nObjOld );
         Gia_ManAppendCo( p->pTtGia, Lit );
     }
-p->timeCheck += Abc_Clock() - clk;
+//p->timeCheck += Abc_Clock() - clk;
     *pSpot = Vec_PtrSize( &p->vObjs );
     objId = If_DsdObjCreate( p, Type, pLits, nLits, truthId );
     if ( Vec_PtrSize(&p->vObjs) > p->nBins )
@@ -1661,13 +1665,6 @@ unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDeri
 {
     If_DsdObj_t * pObj, * pTemp; 
     int i, Mask, iFirst;
-/*
-    if ( 193 == iDsd )
-    {
-        int s = 0;
-        If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
-    }
-*/
     pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsd) );
     if ( fVerbose )
     If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 );
@@ -1740,7 +1737,7 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
     unsigned uSet = If_DsdManCheckXY_int( p, iDsd, LutSize, fDerive, fVerbose );
     if ( uSet == 0 && fHighEffort )
     {
-        abctime clk = Abc_Clock();
+//        abctime clk = Abc_Clock();
         int nVars = If_DsdVecLitSuppSize( &p->vObjs, iDsd );
         word * pRes = If_DsdManComputeTruth( p, iDsd, NULL );
         uSet = If_ManSatCheckXYall( p->pSat, LutSize, pRes, nVars, p->vTemp1 );
@@ -1749,8 +1746,7 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
 //            If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
 //            Dau_DecPrintSet( uSet, nVars, 1 );
         }
-//        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-        p->timeCheck2 += Abc_Clock() - clk;
+//        p->timeCheck2 += Abc_Clock() - clk;
     }
     return uSet;
 }
@@ -1788,27 +1784,23 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
     char pDsd[DAU_MAX_STR];
     int iDsd, nSizeNonDec, nSupp = 0;
     int nWords = Abc_TtWordNum(nLeaves);
-    abctime clk;
+    abctime clk = 0;
     assert( nLeaves <= DAU_MAX_VAR );
     Abc_TtCopy( pCopy, pTruth, nWords, 0 );
-clk = Abc_Clock();
+//clk = Abc_Clock();
     nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 1, pDsd );
-p->timeDsd += Abc_Clock() - clk;
-//    if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") )
-//    {
-//        int x = 0;
-//    }
+//p->timeDsd += Abc_Clock() - clk;
     if ( nSizeNonDec > 0 )
         Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars );
     memset( pPerm, 0xFF, nLeaves );
-clk = Abc_Clock();
+//clk = Abc_Clock();
     iDsd = If_DsdManAddDsd( p, pDsd, pCopy, pPerm, &nSupp );
-p->timeCanon += Abc_Clock() - clk;
+//p->timeCanon += Abc_Clock() - clk;
     assert( nSupp == nLeaves );
     // verify the result
-clk = Abc_Clock();
+//clk = Abc_Clock();
     pRes = If_DsdManComputeTruth( p, iDsd, pPerm );
-p->timeVerify += Abc_Clock() - clk;
+//p->timeVerify += Abc_Clock() - clk;
     if ( !Abc_TtEqual(pRes, pTruth, nWords) )
     {
 //        If_DsdManPrint( p, NULL );
@@ -1821,6 +1813,7 @@ p->timeVerify += Abc_Clock() - clk;
         printf( "\n" );
     }
     If_DsdVecObjIncRef( &p->vObjs, Abc_Lit2Var(iDsd) );
+    assert( If_DsdVecLitSuppSize(&p->vObjs, iDsd) == nLeaves );
     return iDsd;
 }
 

src/map/if/ifMan.c

@@ -92,12 +92,20 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->puTempW   = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words[p->pPars->nLutSize] ) : NULL;
     if ( pPars->fUseDsd )
     {
-        p->vTtDsds = Vec_IntAlloc( 1000 );
-        Vec_IntPush( p->vTtDsds, 0 );
-        Vec_IntPush( p->vTtDsds, 2 );
-        p->vTtPerms = Vec_StrAlloc( 10000 );
-        Vec_StrFill( p->vTtPerms, 2 * p->pPars->nLutSize, IF_BIG_CHAR );
-        Vec_StrWriteEntry( p->vTtPerms, p->pPars->nLutSize, 0 );
+        for ( v = 6; v <= p->pPars->nLutSize; v++ )
+        {
+            p->vTtDsds[v] = Vec_IntAlloc( 1000 );
+            Vec_IntPush( p->vTtDsds[v], 0 );
+            Vec_IntPush( p->vTtDsds[v], 2 );
+            p->vTtPerms[v] = Vec_StrAlloc( 10000 );
+            Vec_StrFill( p->vTtPerms[v], 2 * v, IF_BIG_CHAR );
+            Vec_StrWriteEntry( p->vTtPerms[v], v, 0 );
+        }
+        for ( v = 0; v < 6; v++ )
+        {
+            p->vTtDsds[v]  = p->vTtDsds[6];
+            p->vTtPerms[v] = p->vTtPerms[6];
+        }
     }
     if ( pPars->fUseTtPerm )
     {
@@ -204,8 +212,10 @@ void If_ManStop( If_Man_t * p )
     Vec_PtrFreeP( &p->vObjsRev );
     Vec_PtrFreeP( &p->vLatchOrder );
     Vec_IntFreeP( &p->vLags );
-    Vec_IntFreeP( &p->vTtDsds );
-    Vec_StrFreeP( &p->vTtPerms );
+    for ( i = 6; i <= p->pPars->nLutSize; i++ )
+        Vec_IntFreeP( &p->vTtDsds[i] );
+    for ( i = 6; i <= p->pPars->nLutSize; i++ )
+        Vec_StrFreeP( &p->vTtPerms[i] );
     Vec_IntFreeP( &p->vCutData );
     Vec_IntFreeP( &p->vPairRes );
     Vec_StrFreeP( &p->vPairPerms );

src/map/if/ifMap.c

@@ -208,24 +208,25 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
             {
                 extern void If_ManCacheRecord( If_Man_t * p, int iDsd0, int iDsd1, int nShared, int iDsd );
                 int truthId = Abc_Lit2Var(pCut->iCutFunc);
-                if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 )
+                if ( Vec_IntSize(p->vTtDsds[pCut->nLeaves]) <= truthId || Vec_IntEntry(p->vTtDsds[pCut->nLeaves], truthId) == -1 )
                 {
                     pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
-                    while ( Vec_IntSize(p->vTtDsds) <= truthId )
+                    while ( Vec_IntSize(p->vTtDsds[pCut->nLeaves]) <= truthId )
                     {
-                        Vec_IntPush( p->vTtDsds, -1 );
-                        for ( v = 0; v < p->pPars->nLutSize; v++ )
-                            Vec_StrPush( p->vTtPerms, IF_BIG_CHAR );
+                        Vec_IntPush( p->vTtDsds[pCut->nLeaves], -1 );
+                        for ( v = 0; v < Abc_MaxInt(6, pCut->nLeaves); v++ )
+                            Vec_StrPush( p->vTtPerms[pCut->nLeaves], IF_BIG_CHAR );
                     }
-                    Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
+                    Vec_IntWriteEntry( p->vTtDsds[pCut->nLeaves], truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
                     for ( v = 0; v < (int)pCut->nLeaves; v++ )
-                        Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] );
+                        Vec_StrWriteEntry( p->vTtPerms[pCut->nLeaves], truthId * Abc_MaxInt(6, pCut->nLeaves) + v, (char)pCut->pPerm[v] );
                 }
                 else
                 {
-                    pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
+                    pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds[pCut->nLeaves], truthId), Abc_LitIsCompl(pCut->iCutFunc) );
                     for ( v = 0; v < (int)pCut->nLeaves; v++ )
-                        pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v );
+                        pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms[pCut->nLeaves], truthId * Abc_MaxInt(6, pCut->nLeaves) + v );
+//                    assert( If_DsdManSuppSize(p->pIfDsdMan, pCut->iCutDsd) == (int)pCut->nLeaves );
                 }
 //                If_ManCacheRecord( p, pCut0->iCutDsd, pCut1->iCutDsd, nShared, pCut->iCutDsd );
             }