diff options
| -rw-r--r-- | src/aig/gia/giaSatLut.c | 15 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 11 |
2 files changed, 17 insertions, 9 deletions
diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c index 2c734f2b..6062588b 100644 --- a/src/aig/gia/giaSatLut.c +++ b/src/aig/gia/giaSatLut.c @@ -50,6 +50,7 @@ struct Sbl_Man_t_ int nLargeWins; // the number of large windows int nIterOuts; // the number of iters exceeded // parameters + int LutSize; // LUT size int nBTLimit; // conflicts int DelayMax; // external delay int nEdges; // the number of edges @@ -621,14 +622,19 @@ static int Sbl_ManFindAndPrintCut( Sbl_Man_t * p, int c ) { return Sbl_ManPrintCut( Vec_WrdEntry(p->vCutsI1, c), Vec_WrdEntry(p->vCutsI2, c), Vec_WrdEntry(p->vCutsN1, c), Vec_WrdEntry(p->vCutsN2, c) ); } -static inline int Sbl_CutIsFeasible( word CutI1, word CutI2, word CutN1, word CutN2 ) +static inline int Sbl_CutIsFeasible( word CutI1, word CutI2, word CutN1, word CutN2, int LutSize ) { int Count = (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0); + assert( LutSize <= 6 ); CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0); CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0); CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0); CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0); - return Count <= 4; + if ( LutSize <= 4 ) + return Count <= 4; + CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0); + CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0); + return Count <= 6; } static inline int Sbl_CutPushUncontained( Vec_Wrd_t * vCutsI1, Vec_Wrd_t * vCutsI2, Vec_Wrd_t * vCutsN1, Vec_Wrd_t * vCutsN2, word CutI1, word CutI2, word CutN1, word CutN2 ) { @@ -681,7 +687,7 @@ static inline void Sbl_ManComputeCutsOne( Sbl_Man_t * p, int Fan0, int Fan1, int Vec_WrdClear( p->vTempN2 ); for ( i = Start0; i < Limit0; i++ ) for ( k = Start1; k < Limit1; k++ ) - if ( Sbl_CutIsFeasible(pCutsI1[i] | pCutsI1[k], pCutsI2[i] | pCutsI2[k], pCutsN1[i] | pCutsN1[k], pCutsN2[i] | pCutsN2[k]) ) + if ( Sbl_CutIsFeasible(pCutsI1[i] | pCutsI1[k], pCutsI2[i] | pCutsI2[k], pCutsN1[i] | pCutsN1[k], pCutsN2[i] | pCutsN2[k], p->LutSize) ) Sbl_CutPushUncontained( p->vTempI1, p->vTempI2, p->vTempN1, p->vTempN2, pCutsI1[i] | pCutsI1[k], pCutsI2[i] | pCutsI2[k], pCutsN1[i] | pCutsN1[k], pCutsN2[i] | pCutsN2[k] ); Vec_IntPush( p->vCutsStart, Vec_WrdSize(p->vCutsI1) ); Vec_IntPush( p->vCutsNum, Vec_WrdSize(p->vTempI1) + 1 ); @@ -1174,10 +1180,11 @@ void Sbl_ManPrintRuntime( Sbl_Man_t * p ) ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); ABC_PRTP( "ALL ", p->timeTotal, p->timeTotal ); } -void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVerbose, int fVeryVerbose ) +void Gia_ManLutSat( Gia_Man_t * pGia, int LutSize, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVerbose, int fVeryVerbose ) { int iLut, nImproveCount = 0; Sbl_Man_t * p = Sbl_ManAlloc( pGia, nNumber ); + p->LutSize = LutSize; // LUT size p->nBTLimit = nBTLimit; // conflicts p->DelayMax = DelayMax; // external delay p->nEdges = nEdges; // the number of edges diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2cd9c0b9..632edb78 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -34973,8 +34973,8 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVerbose, int fVeryVerbose ); - int c, nNumber = 32, nImproves = 0, nBTLimit = 100, DelayMax = 0, nEdges = 0; + extern void Gia_ManLutSat( Gia_Man_t * p, int LutSize, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVerbose, int fVeryVerbose ); + int c, LutSize = 0, nNumber = 32, nImproves = 0, nBTLimit = 100, DelayMax = 0, nEdges = 0; int fDelay = 0, fReverse = 0, fVeryVerbose = 0, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "NICDQdrwvh" ) ) != EOF ) @@ -35059,10 +35059,11 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Current AIG has no mapping. Run \"&if\".\n" ); return 1; } - if ( Gia_ManLutSizeMax(pAbc->pGia) > 4 ) - Abc_Print( 0, "Current AIG is mapped into %d-LUTs (only 4-LUT mapping is currently supported).\n", Gia_ManLutSizeMax(pAbc->pGia) ); + LutSize = Gia_ManLutSizeMax(pAbc->pGia); + if ( LutSize > 6 ) + Abc_Print( 0, "Current AIG is mapped into %d-LUTs (only 6-LUT mapping is currently supported).\n", Gia_ManLutSizeMax(pAbc->pGia) ); else - Gia_ManLutSat( pAbc->pGia, nNumber, nImproves, nBTLimit, DelayMax, nEdges, fDelay, fReverse, fVerbose, fVeryVerbose ); + Gia_ManLutSat( pAbc->pGia, LutSize, nNumber, nImproves, nBTLimit, DelayMax, nEdges, fDelay, fReverse, fVerbose, fVeryVerbose ); return 0; usage: |