luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Extending &satlut to work for 6-LUTs.

This commit is contained in:
Alan Mishchenko 2016-04-27 18:12:41 -07:00
parent 62f13100d0
commit e8f961671c
2 changed files with 17 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/aig/gia/giaSatLut.c
View File

@ -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

11
src/base/abci/abc.c
View File

@ -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: