diff options
| -rw-r--r-- | src/base/abci/abc.c | 4 | ||||
| -rw-r--r-- | src/map/mio/exp.h | 59 | ||||
| -rw-r--r-- | src/map/mio/mio.h | 3 | ||||
| -rw-r--r-- | src/map/mpm/mpmMan.c | 2 | ||||
| -rw-r--r-- | src/misc/util/utilTruth.h | 35 | ||||
| -rw-r--r-- | src/opt/sfm/sfmDec.c | 47 | ||||
| -rw-r--r-- | src/opt/sfm/sfmInt.h | 6 | ||||
| -rw-r--r-- | src/opt/sfm/sfmLib.c | 132 | ||||
| -rw-r--r-- | src/opt/sfm/sfmTime.c | 2 | 
9 files changed, 210 insertions, 80 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e1a11378..12e911a6 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -5233,7 +5233,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )              }              pPars->nVarMax = atoi(argv[globalUtilOptind]);              globalUtilOptind++; -            if ( pPars->nVarMax < 2 || pPars->nVarMax > 6 ) +            if ( pPars->nVarMax < 2 || pPars->nVarMax > 8 )                  goto usage;              break;          case 'L': @@ -5378,7 +5378,7 @@ usage:      Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevMax );      Abc_Print( -2, "\t-V <num> : the number of levels in the TFI/TFO cone (1 <= num) [default = %d]\n",         pPars->nTfiLevMax );      Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n",                pPars->nFanoutMax ); -    Abc_Print( -2, "\t-K <num> : the max number of variables (2 <= num <= 6 ) [default = %d]\n",                pPars->nVarMax ); +    Abc_Print( -2, "\t-K <num> : the max number of variables (2 <= num <= 8 ) [default = %d]\n",                pPars->nVarMax );      Abc_Print( -2, "\t-L <num> : the min size of max fanout-free cone (MFFC) (area-only) [default = %d]\n",     pPars->nMffcMin );      Abc_Print( -2, "\t-H <num> : the max size of max fanout-free cone (MFFC) (area-only) [default = %d]\n",     pPars->nMffcMax );      Abc_Print( -2, "\t-D <num> : the max number of decompositions to try (1 <= num <= 4) [default = %d]\n",     pPars->nDecMax ); diff --git a/src/map/mio/exp.h b/src/map/mio/exp.h index 1e14b1bd..962e218a 100644 --- a/src/map/mio/exp.h +++ b/src/map/mio/exp.h @@ -202,6 +202,65 @@ static inline word Exp_Truth6( int nVars, Vec_Int_t * p, word * puFanins )      ABC_FREE( puNodes );      return Res;  } +static inline void Exp_Truth8( int nVars, Vec_Int_t * p, word ** puFanins, word * puRes ) +{ +    word Truth8[8][4] = { +        { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) }, +        { ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) }, +        { ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) }, +        { ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) }, +        { ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) }, +        { ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) }, +        { ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) }, +        { ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) } +    }; +    word * puFaninsInt[8], * pStore, * pThis = NULL; +    int i, k, iRoot = Vec_IntEntryLast(p); +    if ( puFanins == NULL ) +    { +        puFanins = puFaninsInt; +        for ( k = 0; k < 8; k++ ) +            puFanins[k] = Truth8[k]; +    } +    if ( Exp_NodeNum(p) == 0 ) +    { +        assert( iRoot < 2 * nVars ); +        if ( iRoot == EXP_CONST0 || iRoot == EXP_CONST1 ) +            for ( k = 0; k < 4; k++ ) +                puRes[k] = iRoot == EXP_CONST0 ? 0 : ~(word)0; +        else +            for ( k = 0; k < 4; k++ ) +                puRes[k] = Abc_LitIsCompl(iRoot) ? ~puFanins[Abc_Lit2Var(iRoot)][k] : puFanins[Abc_Lit2Var(iRoot)][k]; +        return; +    } +    pStore = ABC_CALLOC( word, 4 * Exp_NodeNum(p) ); +    for ( i = 0; i < Exp_NodeNum(p); i++ ) +    { +        int iVar0 = Abc_Lit2Var( Vec_IntEntry(p, 2*i+0) ); +        int iVar1 = Abc_Lit2Var( Vec_IntEntry(p, 2*i+1) ); +        int fCompl0 = Abc_LitIsCompl( Vec_IntEntry(p, 2*i+0) ); +        int fCompl1 = Abc_LitIsCompl( Vec_IntEntry(p, 2*i+1) ); +        word * pIn0 = iVar0 < nVars ? puFanins[iVar0] : pStore + 4 * (iVar0 - nVars); +        word * pIn1 = iVar1 < nVars ? puFanins[iVar1] : pStore + 4 * (iVar1 - nVars); +        pThis = pStore + 4 * i; +        if ( fCompl0 && fCompl1 ) +            for ( k = 0; k < 4; k++ ) +                pThis[k] = ~pIn0[k] & ~pIn1[k]; +        else if ( fCompl0 && !fCompl1 ) +            for ( k = 0; k < 4; k++ ) +                pThis[k] = ~pIn0[k] &  pIn1[k]; +        else if ( !fCompl0 && fCompl1 ) +            for ( k = 0; k < 4; k++ ) +                pThis[k] =  pIn0[k] & ~pIn1[k]; +        else //if ( !fCompl0 && !fCompl1 ) +            for ( k = 0; k < 4; k++ ) +                pThis[k] =  pIn0[k] &  pIn1[k]; +    } +    assert( Abc_Lit2Var(iRoot) - nVars == i - 1 ); +    for ( k = 0; k < 4; k++ ) +        puRes[k] = Abc_LitIsCompl(iRoot) ? ~pThis[k] : pThis[k]; +    ABC_FREE( pStore ); +}  static inline void Exp_TruthLit( int nVars, int Lit, word ** puFanins, word ** puNodes, word * pRes, int nWords )  {      int w; diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h index a391e4a2..7db93dd8 100644 --- a/src/map/mio/mio.h +++ b/src/map/mio/mio.h @@ -59,7 +59,8 @@ struct Mio_Cell2_t_  {      char *          pName;          // name      Vec_Int_t *     vExpr;          // expression -    unsigned        Id       : 28;  // gate ID +    unsigned        Id       : 26;  // gate ID +    unsigned        Type     :  2;  // gate type      unsigned        nFanins  :  4;  // gate fanins      word            Area;           // area      word            uTruth;         // truth table diff --git a/src/map/mpm/mpmMan.c b/src/map/mpm/mpmMan.c index ae3bfc32..d2777b57 100644 --- a/src/map/mpm/mpmMan.c +++ b/src/map/mpm/mpmMan.c @@ -83,7 +83,7 @@ Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_Par_t * pPars )          p->vTtMem = Vec_MemAlloc( p->nTruWords, 12 ); // 32 KB/page for 6-var functions          Vec_MemHashAlloc( p->vTtMem, 10000 );          p->funcCst0 = Vec_MemHashInsert( p->vTtMem, p->Truth ); -        Abc_TtUnit( p->Truth, p->nTruWords ); +        Abc_TtUnit( p->Truth, p->nTruWords, 0 );          p->funcVar0 = Vec_MemHashInsert( p->vTtMem, p->Truth );      }      else if ( p->pPars->fUseDsd ) diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 4f8e7c02..fbd7ded5 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -113,6 +113,17 @@ static word Ps_PMasks[5][6][3] = {      }  }; +static word s_Truth8[8][4] = { +    { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) }, +    { ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) }, +    { ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) }, +    { ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) }, +    { ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) }, +    { ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) }, +    { ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) }, +    { ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) } +}; +  // the bit count for the first 256 integer numbers  static int Abc_TtBitCount8[256] = {      0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, @@ -204,6 +215,12 @@ static inline word Abc_Tt6Mask( int nBits )       { assert( nBits >= 0 && nBits    SeeAlso     []  ***********************************************************************/ +static inline void Abc_TtConst( word * pOut, int nWords, int fConst1 ) +{ +    int w; +    for ( w = 0; w < nWords; w++ ) +        pOut[w] = fConst1 ? ~(word)0 : 0; +}  static inline void Abc_TtClear( word * pOut, int nWords )  {      int w; @@ -216,11 +233,11 @@ static inline void Abc_TtFill( word * pOut, int nWords )      for ( w = 0; w < nWords; w++ )          pOut[w] = ~(word)0;  } -static inline void Abc_TtUnit( word * pOut, int nWords ) +static inline void Abc_TtUnit( word * pOut, int nWords, int fCompl )  {      int w;      for ( w = 0; w < nWords; w++ ) -        pOut[w] = s_Truths6[0]; +        pOut[w] = fCompl ? ~s_Truths6[0] : s_Truths6[0];  }  static inline void Abc_TtNot( word * pOut, int nWords )  { @@ -284,6 +301,14 @@ static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords )              return 0;      return 1;  } +static inline int Abc_TtOpposite( word * pIn1, word * pIn2, int nWords ) +{ +    int w; +    for ( w = 0; w < nWords; w++ ) +        if ( pIn1[w] != ~pIn2[w] ) +            return 0; +    return 1; +}  static inline int Abc_TtImply( word * pIn1, word * pIn2, int nWords )  {      int w; @@ -1116,15 +1141,15 @@ static inline int Abc_TtOnlyOneOne( word t )          return 0;      return (t & (t-1)) == 0;  } -static inline int Gia_ManTtIsAndType( word t, int nVars ) +static inline int Abc_Tt6IsAndType( word t, int nVars )  {      return Abc_TtOnlyOneOne( t & Abc_Tt6Mask(1 << nVars) );  } -static inline int Gia_ManTtIsOrType( word t, int nVars ) +static inline int Abc_Tt6IsOrType( word t, int nVars )  {      return Abc_TtOnlyOneOne( ~t & Abc_Tt6Mask(1 << nVars) );  } -static inline int Gia_ManTtIsXorType( word t, int nVars ) +static inline int Abc_Tt6IsXorType( word t, int nVars )  {      return ((((t & 1) ? ~t : t) ^ s_TruthXors[nVars]) & Abc_Tt6Mask(1 << nVars)) == 0;  } diff --git a/src/opt/sfm/sfmDec.c b/src/opt/sfm/sfmDec.c index ea0779ff..6310cb1a 100644 --- a/src/opt/sfm/sfmDec.c +++ b/src/opt/sfm/sfmDec.c @@ -117,8 +117,8 @@ struct Sfm_Dec_t_      int               nMaxWin;      word              nAllDivs;      word              nAllWin; -    int               nLuckySizes[10]; -    int               nLuckyGates[10]; +    int               nLuckySizes[SFM_SUPP_MAX+1]; +    int               nLuckyGates[SFM_SUPP_MAX+1];  };  #define SFM_MASK_PI     1  // supp(node) is contained in supp(TFI(pivot)) @@ -274,6 +274,7 @@ static inline word Sfm_ObjSimulate( Abc_Obj_t * pObj )      Sfm_Dec_t * p = Sfm_DecMan( pObj );      Vec_Int_t * vExpr = Mio_GateReadExpr( (Mio_Gate_t *)pObj->pData );      Abc_Obj_t * pFanin; int i; word uFanins[6]; +    assert( Abc_ObjFaninNum(pObj) <= 6 );      Abc_ObjForEachFanin( pObj, pFanin, i )          uFanins[i] = Sfm_DecObjSim( p, pFanin );      return Exp_Truth6( Abc_ObjFaninNum(pObj), vExpr, uFanins ); @@ -778,13 +779,14 @@ int Sfm_DecCombineDec( Sfm_Dec_t * p, word * pTruth0, word * pTruth1, int * pSup      {          memcpy( pSupp,  pSupp0,  sizeof(int)*nSupp0   );          memcpy( pTruth, pTruth0, sizeof(word)*nWords0 ); +        Abc_TtStretch6( pTruth, nSupp0, p->pPars->nVarMax );          return nSupp0;      }      // merge support variables      Vec_IntTwoMerge2Int( &vVec0, &vVec1, &vVec );      Vec_IntPushOrder( &vVec, Var );      nSupp = Vec_IntSize( &vVec ); -    if ( nSupp > SFM_SUPP_MAX ) +    if ( nSupp > p->pPars->nVarMax )          return -2;      // expand truth tables      Abc_TtStretch6( pTruth0, nSupp0, nSupp ); @@ -794,6 +796,7 @@ int Sfm_DecCombineDec( Sfm_Dec_t * p, word * pTruth0, word * pTruth1, int * pSup      // perform operation      iSuppVar = Vec_IntFind( &vVec, Var );      Abc_TtMux( pTruth, p->pTtElems[iSuppVar], pTruth1, pTruth0, Abc_TtWordNum(nSupp) ); +    Abc_TtStretch6( pTruth, nSupp, p->pPars->nVarMax );      return nSupp;  }  int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssump, int nAssump, word Masks[2], int fCofactor, int nSuppAdd ) @@ -835,7 +838,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu          {              p->nSatCallsUnsat++;              p->timeSatUnsat += Abc_Clock() - clk; -            pTruth[0] = c ? ~((word)0) : 0; +            Abc_TtConst( pTruth, Abc_TtWordNum(p->pPars->nVarMax), c );              if ( p->pPars->fVeryVerbose )                  printf( "Found constant %d.\n", c );              return 0; @@ -907,13 +910,13 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu          }          assert( Abc_Lit2Var(Impls[0]) == Abc_Lit2Var(Impls[1]) );          // found buffer/inverter -        pTruth[0] = Abc_LitIsCompl(Impls[0]) ? ~p->pTtElems[0][0] : p->pTtElems[0][0]; +        Abc_TtUnit( pTruth, Abc_TtWordNum(p->pPars->nVarMax), Abc_LitIsCompl(Impls[0]) );          pSupp[0] = Abc_Lit2Var(Impls[0]);          if ( p->pPars->fVeryVerbose )              printf( "Found variable %s%d.\n", Abc_LitIsCompl(Impls[0]) ? "!":"", pSupp[0] );          return 1;              } -    if ( nSuppAdd > 4 ) +    if ( nSuppAdd > p->pPars->nVarMax - 2 )      {          if ( p->pPars->fVeryVerbose )              printf( "The number of assumption is more than MFFC size.\n" ); @@ -969,6 +972,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu                      pSupp[i] = Abc_Lit2Var(pSupp[i]);                  }              } +            Abc_TtStretch6( pTruth, nFinal, p->pPars->nVarMax );              p->nNodesAndOr++;              if ( p->pPars->fVeryVerbose )                  printf( "Found %d-input AND/OR gate.\n", nFinal ); @@ -1028,7 +1032,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu      if ( Var >= 0 )      {          word uTruth[2][SFM_WORD_MAX], MasksNext[2]; -        int Supp[2][2*SFM_SUPP_MAX], nSupp[2] = {0}, nSuppAll; +        int Supp[2][2*SFM_SUPP_MAX], nSupp[2] = {0};          Vec_IntPush( &p->vObjDec, Var );          for ( i = 0; i < 2; i++ )          { @@ -1043,10 +1047,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu                  return -2;          }          // combine solutions -        nSuppAll = Sfm_DecCombineDec( p, uTruth[0], uTruth[1], Supp[0], Supp[1], nSupp[0], nSupp[1], pTruth, pSupp, Var ); -        if ( nSuppAll > 6 ) -            return -2; -        return nSuppAll; +        return Sfm_DecCombineDec( p, uTruth[0], uTruth[1], Supp[0], Supp[1], nSupp[0], nSupp[1], pTruth, pSupp, Var );      }      return -2;  } @@ -1114,13 +1115,19 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p, Abc_Obj_t * pObj )  //            Dau_DsdPrintFromTruth( uTruth[iBest], nSupp[iBest] );      }  //    return -1; -    RetValue = Sfm_LibImplement( p->pLib, uTruth[iBest][0], pSupp[iBest], nSupp[iBest], p->AreaMffc, &p->vObjGates, &p->vObjFanins, p->pPars->fZeroCost ); +    RetValue = Sfm_LibImplement( p->pLib, uTruth[iBest], pSupp[iBest], nSupp[iBest], p->AreaMffc, &p->vObjGates, &p->vObjFanins, p->pPars->fZeroCost );      if ( fVeryVerbose )          printf( "Area-reducing implementation %sfound.\n", RetValue < 0 ? "NOT " : "" );      if ( RetValue >= 0 ) +    { +        assert( nSupp[iBest] <= p->pPars->nVarMax );          p->nLuckySizes[nSupp[iBest]]++; +    }      if ( RetValue >= 0 ) +    { +        assert( RetValue <= 2 );          p->nLuckyGates[RetValue]++; +    }      return RetValue;  }  int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj ) @@ -1171,8 +1178,10 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )              Dau_DsdPrintFromTruth( uTruth[i], nSupp[i] );          if ( nSupp[i] < 2 )          { -            RetValue = Sfm_LibImplement( p->pLib, uTruth[i][0], pSupp[i], nSupp[i], p->AreaMffc, &p->vObjGates, &p->vObjFanins, p->pPars->fZeroCost ); -            p->nLuckySizes[nSupp[i]]++; +            RetValue = Sfm_LibImplement( p->pLib, uTruth[i], pSupp[i], nSupp[i], p->AreaMffc, &p->vObjGates, &p->vObjFanins, p->pPars->fZeroCost ); +            assert( nSupp[iBest] <= p->pPars->nVarMax ); +            p->nLuckySizes[nSupp[iBest]]++; +            assert( RetValue <= 2 );              p->nLuckyGates[RetValue]++;              return RetValue;          } @@ -1182,7 +1191,7 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )          //}          // try the delay -        nMatches = Sfm_LibFindMatches( p->pLib, uTruth[i][0], pSupp[i], nSupp[i], &p->vMatchGates, &p->vMatchFans ); +        nMatches = Sfm_LibFindMatches( p->pLib, uTruth[i], pSupp[i], nSupp[i], &p->vMatchGates, &p->vMatchFans );          DelayMin = DelayOrig = Sfm_TimReadObjDelay( p->pTim, Abc_ObjId(pObj) );          for ( k = 0; k < nMatches; k++ )          { @@ -1217,7 +1226,9 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )  //    if ( fVeryVerbose )  //        Dau_DsdPrintFromTruth( uTruth[iBest], nSupp[iBest] );      RetValue = Sfm_LibAddNewGates( p->pLib, pSupp[iBest], pGate1Best, pGate2Best, pFans1Best, pFans2Best, &p->vObjGates, &p->vObjFanins ); +    assert( nSupp[iBest] <= p->pPars->nVarMax );      p->nLuckySizes[nSupp[iBest]]++; +    assert( RetValue <= 2 );      p->nLuckyGates[RetValue]++;      p->DelayMin = DelayMin;      return 1; @@ -1629,13 +1640,13 @@ void Sfm_DecPrintStats( Sfm_Dec_t * p )      ABC_PRTP( "ALL   ", p->timeTotal,     p->timeTotal );      printf( "Cone sizes:  " ); -    for ( i = 0; i < 10; i++ ) +    for ( i = 0; i <= SFM_SUPP_MAX; i++ )          if ( p->nLuckySizes[i] )              printf( "%d=%d  ", i, p->nLuckySizes[i] );      printf( "  " );      printf( "Gate sizes:  " ); -    for ( i = 0; i < 10; i++ ) +    for ( i = 0; i <= SFM_SUPP_MAX; i++ )          if ( p->nLuckyGates[i] )              printf( "%d=%d  ", i, p->nLuckyGates[i] );      printf( "\n" ); @@ -1792,7 +1803,7 @@ clk = Abc_Clock();              Sfm_TimUpdateTiming( p->pTim, &p->vTemp );  p->timeTime += Abc_Clock() - clk;              pObjNew = Abc_NtkObj( pNtk, Abc_NtkObjNumMax(pNtk)-1 ); -            assert( p->DelayMin == Sfm_TimReadObjDelay(p->pTim, Abc_ObjId(pObjNew)) ); +            assert( p->DelayMin == 0 || p->DelayMin == Sfm_TimReadObjDelay(p->pTim, Abc_ObjId(pObjNew)) );              // report              if ( pPars->fVerbose )                  printf( "Node %5d :  I =%3d.  Cand = %5d (%6.2f %%)   Old =%8.2f.  New =%8.2f.  Final =%8.2f\n",  diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index e5f73e38..fb799582 100644 --- a/src/opt/sfm/sfmInt.h +++ b/src/opt/sfm/sfmInt.h @@ -50,7 +50,7 @@ ABC_NAMESPACE_HEADER_START  #define SFM_SAT_UNDEC 0x1234567812345678  #define SFM_SAT_SAT   0x8765432187654321 -#define SFM_SUPP_MAX  6 +#define SFM_SUPP_MAX  8  #define SFM_WORD_MAX ((SFM_SUPP_MAX>6) ? (1<<(SFM_SUPP_MAX-6)) : 1)  #define SFM_WIN_MAX   1000  #define SFM_DEC_MAX   4 @@ -201,9 +201,9 @@ extern int          Sfm_LibFindComplInputGate( Vec_Wrd_t * vFuncs, int iGate, in  extern Sfm_Lib_t *  Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose );  extern void         Sfm_LibPrint( Sfm_Lib_t * p );  extern void         Sfm_LibStop( Sfm_Lib_t * p ); -extern int          Sfm_LibFindMatches( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans ); +extern int          Sfm_LibFindMatches( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans );  extern int          Sfm_LibAddNewGates( Sfm_Lib_t * p, int * pFanins, Mio_Gate_t * pGateB, Mio_Gate_t * pGateT, char * pFansB, char * pFansT, Vec_Int_t * vGates, Vec_Wec_t * vFanins ); -extern int          Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins, int fZeroCost ); +extern int          Sfm_LibImplement( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins, int fZeroCost );  /*=== sfmNtk.c ==========================================================*/  extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );  extern void         Sfm_NtkPrepare( Sfm_Ntk_t * p ); diff --git a/src/opt/sfm/sfmLib.c b/src/opt/sfm/sfmLib.c index 00fc92e0..eb3c74c8 100644 --- a/src/opt/sfm/sfmLib.c +++ b/src/opt/sfm/sfmLib.c @@ -39,12 +39,13 @@ struct Sfm_Fun_t_  {      int             Next;          // next function in the list      int             Area;          // area of this function -    char            pFansT[8];     // top gate ID, followed by fanin perm -    char            pFansB[8];     // bottom gate ID, followed by fanin perm +    char            pFansT[SFM_SUPP_MAX+1];     // top gate ID, followed by fanin perm +    char            pFansB[SFM_SUPP_MAX+1];     // bottom gate ID, followed by fanin perm  };  struct Sfm_Lib_t_  {      int             nVars;         // variable count +    int             nWords;        // truth table words      int             fVerbose;      // verbose statistics      Mio_Cell2_t *   pCells;        // library gates      int             nCells;        // library gate count @@ -172,6 +173,7 @@ int Sfm_LibFindComplInputGate( Vec_Wrd_t * vFuncs, int iGate, int nFanins, int i              if ( uTruth == uTruthSwap )                  return i;      } +    // add checking for complemeting control input of a MUX      if ( piFaninNew ) *piFaninNew = -1;      return -1;  } @@ -191,6 +193,7 @@ int Sfm_LibFindComplInputGate( Vec_Wrd_t * vFuncs, int iGate, int nFanins, int i  Sfm_Lib_t * Sfm_LibStart( int nVars, int fDelay, int fVerbose )  {      Sfm_Lib_t * p = ABC_CALLOC( Sfm_Lib_t, 1 ); +    assert( nVars <= SFM_SUPP_MAX );      p->vTtMem = Vec_MemAllocForTT( nVars, 0 );         Vec_IntGrow( &p->vLists,  (1 << 16) );      Vec_IntGrow( &p->vCounts, (1 << 16) ); @@ -205,6 +208,7 @@ Sfm_Lib_t * Sfm_LibStart( int nVars, int fDelay, int fVerbose )      if ( fDelay ) Vec_IntGrow( &p->vStore,  (1 << 18) );      Vec_IntGrow( &p->vTemp, 16 );      p->nVars = nVars; +    p->nWords = Abc_TtWordNum( nVars );      p->fVerbose = fVerbose;      return p;  } @@ -216,7 +220,7 @@ void Sfm_LibStop( Sfm_Lib_t * p )          int i, nFanins;  word * pTruth;          Vec_MemForEachEntry( p->vTtMem, pTruth, i )          { -            if ( Vec_IntEntry(&p->vHits, i) == 0 ) +            if ( i < 2 || Vec_IntEntry(&p->vHits, i) == 0 )                  continue;              nFanins = Abc_TtSupportSize(pTruth, p->nVars);              printf( "%8d : ", i ); @@ -248,10 +252,10 @@ void Sfm_LibStop( Sfm_Lib_t * p )    SeeAlso     []  ***********************************************************************/ -word Sfm_LibTruthTwo( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop ) +word Sfm_LibTruth6Two( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop )  { +    word uFanins[SFM_SUPP_MAX]; int i, k;      word uTruthBot = Exp_Truth6( pCellBot->nFanins, pCellBot->vExpr, NULL ); -    word uFanins[6]; int i, k;      assert( InTop >= 0 && InTop < (int)pCellTop->nFanins );      for ( i = 0, k = pCellBot->nFanins; i < (int)pCellTop->nFanins; i++ )          if ( i == InTop ) @@ -262,6 +266,19 @@ word Sfm_LibTruthTwo( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop      uTruthBot = Exp_Truth6( pCellTop->nFanins, pCellTop->vExpr, uFanins );      return uTruthBot;  } +void Sfm_LibTruth8Two( Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop, word * pRes ) +{ +    word uTruthBot[4], * puFanins[SFM_SUPP_MAX]; int i, k; +    Exp_Truth8( pCellBot->nFanins, pCellBot->vExpr, NULL, uTruthBot ); +    assert( InTop >= 0 && InTop < (int)pCellTop->nFanins ); +    for ( i = 0, k = pCellBot->nFanins; i < (int)pCellTop->nFanins; i++ ) +        if ( i == InTop ) +            puFanins[i] = uTruthBot; +        else +            puFanins[i] = s_Truth8[k++]; +    assert( (int)pCellBot->nFanins + (int)pCellTop->nFanins == k + 1 ); +    Exp_Truth8( pCellTop->nFanins, pCellTop->vExpr, puFanins, pRes ); +}  /**Function************************************************************* @@ -305,12 +322,12 @@ static inline int Sfm_LibNewContains( Sfm_Fun_t * pObj, int * pProf, int Area, i              return 0;      return 1;  } -void Sfm_LibPrepareAdd( Sfm_Lib_t * p, word uTruth, int * Perm, int nFanins, Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop ) +void Sfm_LibPrepareAdd( Sfm_Lib_t * p, word * pTruth, int * Perm, int nFanins, Mio_Cell2_t * pCellBot, Mio_Cell2_t * pCellTop, int InTop )  {      Sfm_Fun_t * pObj; -    int InvPerm[6], Profile[6]; +    int InvPerm[SFM_SUPP_MAX], Profile[SFM_SUPP_MAX];      int Area = (int)pCellBot->Area + (pCellTop ? (int)pCellTop->Area : 0); -    int i, k, Id, Prev, Offset, * pProf, iFunc = Vec_MemHashInsert( p->vTtMem, &uTruth ); +    int i, k, Id, Prev, Offset, * pProf, iFunc = Vec_MemHashInsert( p->vTtMem, pTruth );      if ( iFunc == Vec_IntSize(&p->vLists) )      {          Vec_IntPush( &p->vLists, -1 ); @@ -413,23 +430,23 @@ Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )      abctime clk = Abc_Clock();      Sfm_Lib_t * p = Sfm_LibStart( nVars, fDelay, fVerbose );      Mio_Cell2_t * pCell1, * pCell2, * pLimit; -    int * pPerm[7], * Perm1, * Perm2, Perm[6]; -    int nPerms[7], i, f, n; -    Vec_Int_t * vUseful; -    word tTemp1, tCur; +    int * pPerm[SFM_SUPP_MAX+1], * Perm1, * Perm2, Perm[SFM_SUPP_MAX]; +    int nPerms[SFM_SUPP_MAX+1], i, f, n; +    word tTemp1[4], tCur[4];      char pRes[1000]; -    assert( nVars <= 6 ); +    assert( nVars <= SFM_SUPP_MAX );      // precompute gates -    p->pCells = Mio_CollectRootsNewDefault2( nVars, &p->nCells, 0 ); +    p->pCells = Mio_CollectRootsNewDefault2( Abc_MinInt(6, nVars), &p->nCells, 0 );      pLimit = p->pCells + p->nCells;      // find useful ones -    vUseful = Vec_IntStart( p->nCells ); -//    vUseful = Vec_IntStartFull( p->nCells );      for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )      {          word uTruth = pCell1->uTruth; -        if ( Dau_DsdDecompose(&uTruth, pCell1->nFanins, 0, 0, pRes) <= 3 ) -            Vec_IntWriteEntry( vUseful, pCell1 - p->pCells, 1 ); +        pCell1->Type = 0; +        if ( Abc_Tt6IsAndType(uTruth, pCell1->nFanins) || Abc_Tt6IsOrType(uTruth, pCell1->nFanins) ) +            pCell1->Type = 1; +        else if ( Dau_DsdDecompose(&uTruth, pCell1->nFanins, 0, 0, pRes) <= 3 ) +            pCell1->Type = 2;          else if ( p->fVerbose )              printf( "Skipping gate \"%s\" with non-DSD function %s\n", pCell1->pName, pRes );      } @@ -439,32 +456,33 @@ Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )      for ( i = 2; i <= nVars; i++ )          nPerms[i] = Extra_Factorial( i );      // add single cells -    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ ) -    if ( Vec_IntEntry(vUseful, pCell1 - p->pCells) ) +    for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ )       {          int nFanins = pCell1->nFanins; -        assert( nFanins >= 2 && nFanins <= 6 ); +        assert( nFanins >= 2 && nFanins <= nVars );          for ( i = 0; i < nFanins; i++ )              Perm[i] = i;          // permute truth table -        tCur = tTemp1 = pCell1->uTruth; +        tCur[0] = tTemp1[0] = pCell1->uTruth; +        if ( p->nVars > 6 ) +            tTemp1[1] = tTemp1[2] = tTemp1[3] = tCur[1] = tCur[2] = tCur[3] = tCur[0];          for ( n = 0; n < nPerms[nFanins]; n++ )          {              Sfm_LibPrepareAdd( p, tCur, Perm, nFanins, pCell1, NULL, -1 );              // update -            tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[nFanins][n] ); +            Abc_TtSwapAdjacent( tCur, p->nWords, pPerm[nFanins][n] );              Perm1 = Perm + pPerm[nFanins][n];              Perm2 = Perm1 + 1;              ABC_SWAP( int, *Perm1, *Perm2 );          } -        assert( tTemp1 == tCur ); +        assert( Abc_TtEqual(tTemp1, tCur, p->nWords) );      }      // add double cells      if ( fTwo )      for ( pCell1 = p->pCells + 4; pCell1 < pLimit; pCell1++ ) -    if ( Vec_IntEntry(vUseful, pCell1 - p->pCells) ) +    if ( pCell1->Type > 0 )      for ( pCell2 = p->pCells + 4; pCell2 < pLimit; pCell2++ ) -    if ( Vec_IntEntry(vUseful, pCell2 - p->pCells) ) +    if ( pCell2->Type > 0 && pCell1->Type + pCell2->Type <= 2 )      if ( (int)pCell1->nFanins + (int)pCell2->nFanins <= nVars + 1 )      for ( f = 0; f < (int)pCell2->nFanins; f++ )      { @@ -473,22 +491,27 @@ Sfm_Lib_t * Sfm_LibPrepare( int nVars, int fTwo, int fDelay, int fVerbose )          for ( i = 0; i < nFanins; i++ )              Perm[i] = i;          // permute truth table -        tCur = tTemp1 = Sfm_LibTruthTwo( pCell1, pCell2, f ); +        if ( p->nVars > 6 ) +        { +            Sfm_LibTruth8Two( pCell1, pCell2, f, tCur ); +            Abc_TtCopy( tTemp1, tCur, p->nWords, 0 ); +        } +        else +            tCur[0] = tTemp1[0] = Sfm_LibTruth6Two( pCell1, pCell2, f );          for ( n = 0; n < nPerms[nFanins]; n++ )          {              Sfm_LibPrepareAdd( p, tCur, Perm, nFanins, pCell1, pCell2, f );              // update -            tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[nFanins][n] ); +            Abc_TtSwapAdjacent( tCur, p->nWords, pPerm[nFanins][n] );              Perm1 = Perm + pPerm[nFanins][n];              Perm2 = Perm1 + 1;              ABC_SWAP( int, *Perm1, *Perm2 );          } -        assert( tTemp1 == tCur ); +        assert( Abc_TtEqual(tTemp1, tCur, p->nWords) );      }      // cleanup      for ( i = 2; i <= nVars; i++ )          ABC_FREE( pPerm[i] ); -    Vec_IntFree( vUseful );      if ( fVerbose )      {          printf( "Library processing: Var = %d. Cell = %d.  Fun = %d. Obj = %d. Ave = %.2f.  Skip = %d. Rem = %d.  ",  @@ -532,20 +555,25 @@ void Sfm_LibPrintObj( Sfm_Lib_t * p, Sfm_Fun_t * pObj )  }  void Sfm_LibPrint( Sfm_Lib_t * p )  { -    word * pTruth; Sfm_Fun_t * pObj; int iFunc, nSupp;  +    word * pTruth; Sfm_Fun_t * pObj; int iFunc, nSupp, Count;       Vec_MemForEachEntry( p->vTtMem, pTruth, iFunc )      {          if ( iFunc < 2 )               continue; -        nSupp = Abc_TtSupportSize(pTruth, 6); -        if ( nSupp > 3 ) -            continue;         +        nSupp = Abc_TtSupportSize(pTruth, p->nVars); +        //if ( nSupp > 3 ) +        //    continue;                  //if ( iFunc % 10000 )          //    continue; -        printf( "%d : Count = %d   ", iFunc, Vec_IntEntry(&p->vCounts, iFunc) ); +        printf( "%d : Supp = %d   Count = %d   ", iFunc, nSupp, Vec_IntEntry(&p->vCounts, iFunc) );          Dau_DsdPrintFromTruth( pTruth, nSupp ); +        Count = 0;          Sfm_LibForEachSuper( p, pObj, iFunc ) +        {              Sfm_LibPrintObj( p, pObj ); +            if ( Count++ == 5 ) +                break; +        }      }  }  void Sfm_LibTest() @@ -557,9 +585,9 @@ void Sfm_LibTest()          printf( "There is no current library.\n" );          return;      } -    p = Sfm_LibPrepare( 6, 1, 1, fVerbose ); -    //if ( fVerbose ) -    //    Sfm_LibPrint( p ); +    p = Sfm_LibPrepare( 7, 1, 1, fVerbose ); +    if ( fVerbose ) +        Sfm_LibPrint( p );      Sfm_LibStop( p );  } @@ -574,20 +602,26 @@ void Sfm_LibTest()    SeeAlso     []  ***********************************************************************/ -int Sfm_LibFindMatches( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans ) +int Sfm_LibFindMatches( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, Vec_Ptr_t * vGates, Vec_Ptr_t * vFans )  { -    Mio_Cell2_t * pCellB, * pCellT;      Sfm_Fun_t * pObj; +    Mio_Cell2_t * pCellB, * pCellT;      int iFunc; +//    word pCopy[4]; +//    Abc_TtCopy( pCopy, pTruth, 2, 0 ); +//    Dau_DsdPrintFromTruth( pCopy, 7 );      Vec_PtrClear( vGates );      Vec_PtrClear( vFans );      // look for gate -    assert( uTruth != 0 && uTruth != ~(word)0 && uTruth != s_Truths6[0] && uTruth != ~s_Truths6[0] ); -    iFunc = *Vec_MemHashLookup( p->vTtMem,  &uTruth ); +    assert( !Abc_TtIsConst0(pTruth, p->nWords) &&  +            !Abc_TtIsConst1(pTruth, p->nWords) &&  +            !Abc_TtEqual(pTruth, s_Truth8[0], p->nWords) &&  +            !Abc_TtOpposite(pTruth, s_Truth8[0], p->nWords) ); +    iFunc = *Vec_MemHashLookup( p->vTtMem,  pTruth );      if ( iFunc == -1 )      {          // print functions not found in the library -        //Dau_DsdPrintFromTruth( &uTruth, nFanins ); +        //Dau_DsdPrintFromTruth( pTruth, nFanins );          return 0;      }      Vec_IntAddToEntry( &p->vHits, iFunc, 1 ); @@ -638,7 +672,7 @@ int Sfm_LibAddNewGates( Sfm_Lib_t * p, int * pFanins, Mio_Gate_t * pGateB, Mio_G              Vec_IntPush( vLevel, pFanins[(int)pFansT[i]] );      return 2;  } -int Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins, int fZeroCost ) +int Sfm_LibImplement( Sfm_Lib_t * p, word * pTruth, int * pFanins, int nFanins, int AreaMffc, Vec_Int_t * vGates, Vec_Wec_t * vFanins, int fZeroCost )  {      Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();      Mio_Gate_t * pGate; @@ -646,25 +680,25 @@ int Sfm_LibImplement( Sfm_Lib_t * p, word uTruth, int * pFanins, int nFanins, in      Vec_Int_t * vLevel;      Sfm_Fun_t * pObj, * pObjMin = NULL;      int i, iFunc; -    if ( uTruth == 0 || uTruth == ~(word)0 ) +    if ( Abc_TtIsConst0(pTruth, p->nWords) || Abc_TtIsConst1(pTruth, p->nWords) )      {          assert( nFanins == 0 ); -        pGate = uTruth ? Mio_LibraryReadConst1(pLib) : Mio_LibraryReadConst0(pLib); +        pGate = Abc_TtIsConst1(pTruth, p->nWords) ? Mio_LibraryReadConst1(pLib) : Mio_LibraryReadConst0(pLib);          Vec_IntPush( vGates, Mio_GateReadValue(pGate) );          vLevel = Vec_WecPushLevel( vFanins );          return 1;      } -    if ( uTruth == s_Truths6[0] || uTruth == ~s_Truths6[0] ) +    if ( Abc_TtEqual(pTruth, s_Truth8[0], p->nWords) || Abc_TtOpposite(pTruth, s_Truth8[0], p->nWords) )      {          assert( nFanins == 1 ); -        pGate = uTruth == s_Truths6[0] ? Mio_LibraryReadBuf(pLib) : Mio_LibraryReadInv(pLib); +        pGate = Abc_TtEqual(pTruth, s_Truth8[0], p->nWords) ? Mio_LibraryReadBuf(pLib) : Mio_LibraryReadInv(pLib);          Vec_IntPush( vGates, Mio_GateReadValue(pGate) );          vLevel = Vec_WecPushLevel( vFanins );          Vec_IntPush( vLevel, pFanins[0] );          return 1;      }      // look for gate -    iFunc = *Vec_MemHashLookup( p->vTtMem,  &uTruth ); +    iFunc = *Vec_MemHashLookup( p->vTtMem, pTruth );      if ( iFunc == -1 )          return -1;      Vec_IntAddToEntry( &p->vHits, iFunc, 1 ); diff --git a/src/opt/sfm/sfmTime.c b/src/opt/sfm/sfmTime.c index 939bcd85..8334d291 100644 --- a/src/opt/sfm/sfmTime.c +++ b/src/opt/sfm/sfmTime.c @@ -253,7 +253,7 @@ Sfm_Tim_t * Sfm_TimStart( Mio_Library_t * pLib, Scl_Con_t * pExt, Abc_Ntk_t * pN  //        Vec_IntFillExtra( &p->vTimEdges, Vec_IntSize(Vec_IntSize(&p->vTimEdges)) + Abc_ObjFaninNum(pObj), 0 );  //    }      p->Delay = Sfm_TimTrace( p ); -    assert( DeltaCrit > 0 && DeltaCrit < 10000 ); +    assert( DeltaCrit > 0 && DeltaCrit < MIO_NUM*1000 );      p->DeltaCrit = DeltaCrit;      return p;  }  | 
