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

New SAT-based optimization package.

This commit is contained in:
Alan Mishchenko 2016-12-04 21:59:10 -08:00
parent 91aab10757
commit 8ba6071a76
6 changed files with 168 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/giaMuxes.c
View File

@ -100,7 +100,7 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit )
Gia_Obj_t * pObj, * pFan0, * pFan1, * pFanC, * pSiblNew, * pObjNew;
int i;
assert( p->pMuxes == NULL );
assert( Limit >= 1 ); // allows to create AIG with XORs without MUXes
assert( Limit >= 0 ); // allows to create AIG with XORs without MUXes
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p );
// start the new manager

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

@ -27643,6 +27643,7 @@ static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int
*pnBestLuts = nCurLuts;
*pnBestEdges = nCurEdges;
*pnBestLevels = nCurLevels;
//printf( "\nUpdating best (%d %d %d).\n\n", nCurLuts, nCurEdges, nCurLevels );
return 1;
}
return 0;
@ -31023,7 +31024,7 @@ usage:
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
Abc_Print( -2, "\t-K num : the target LUT size for downstream mapping [default = %d]\n", nLutSize );
Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -40852,7 +40853,7 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
Sbd_Par_t Pars, * pPars = &Pars;
Sbd_ParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCavwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCacvwh" ) ) != EOF )
{
switch ( c )
{
@ -40914,6 +40915,9 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'a':
pPars->fArea ^= 1;
break;
case 'c':
pPars->fCover ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -40946,7 +40950,7 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &mfsd [-KWFMC <num>] [-avwh]\n" );
Abc_Print( -2, "usage: &mfsd [-KWFMC <num>] [-acvwh]\n" );
Abc_Print( -2, "\t performs SAT-based delay-oriented AIG optimization\n" );
Abc_Print( -2, "\t-K <num> : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n", pPars->nLutSize );
Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevels );
@ -40954,6 +40958,7 @@ usage:
Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
Abc_Print( -2, "\t-c : toggle using complete slow covering procedure [default = %s]\n", pPars->fCover? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");

8
src/opt/dau/dauGia.c
View File

@ -243,7 +243,11 @@ int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd )
if ( fAnd )
iFan = Gia_ManAppendAnd( pGia, iFan0, iFan1 );
else if ( pGia->pMuxes )
iFan = Gia_ManAppendXorReal( pGia, iFan0, iFan1 );
{
int fCompl = Abc_LitIsCompl(iFan0) ^ Abc_LitIsCompl(iFan1);
iFan = Gia_ManAppendXorReal( pGia, Abc_LitRegular(iFan0), Abc_LitRegular(iFan1) );
iFan = Abc_LitNotCond( iFan, fCompl );
}
else
iFan = Gia_ManAppendXor( pGia, iFan0, iFan1 );
}
@ -369,7 +373,7 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
pObj = Gia_ManObj(pGia, Abc_Lit2Var(Res));
if ( Gia_ObjIsAnd(pObj) )
{
if ( pGia->pMuxes )
if ( pGia->pMuxes && pGia->pHTable != NULL )
Gia_ObjSetMuxLevel( pGia, pObj );
else
{

1
src/opt/sbd/sbd.h
View File

@ -45,6 +45,7 @@ struct Sbd_Par_t_
int nBTLimit; // maximum number of SAT conflicts
int nWords; // simulation word count
int fArea; // area-oriented optimization
int fCover; // use complete cover procedure
int fVerbose; // verbose flag
int fVeryVerbose; // verbose flag
};

180
src/opt/sbd/sbdCore.c
View File

@ -20,6 +20,7 @@
#include "sbdInt.h"
#include "opt/dau/dau.h"
#include "misc/tim/tim.h"
ABC_NAMESPACE_IMPL_START
@ -97,6 +98,7 @@ void Sbd_ParSetDefault( Sbd_Par_t * pPars )
pPars->nBTLimit = 0; // maximum number of SAT conflicts
pPars->nWords = 1; // simulation word count
pPars->fArea = 0; // area-oriented optimization
pPars->fCover = 0; // use complete cover procedure
pPars->fVerbose = 0; // verbose flag
pPars->fVeryVerbose = 0; // verbose flag
}
@ -467,6 +469,14 @@ int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots );
p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots );
p->timeCnf += Abc_Clock() - clk;
if ( p->pSat == NULL )
{
if ( p->pPars->fVerbose )
printf( "Found stuck-at-%d node %d.\n", 0, Pivot );
Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
p->nConsts++;
return 0;
}
//return -1;
//Sbd_ManPrintObj( p, Pivot );
@ -822,7 +832,7 @@ static inline int Sbd_ManAddCube2( word Cover[2][64], int nRows, word Cube[2] )
return nRows;
}
static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDivs )
{
int c0, c1, c2, c3;
word Target = Cover[nDivs];
@ -871,6 +881,72 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
return 0;
}
static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
{
int Ones[64], Order[64];
int Limits[4] = { nDivs/4+1, nDivs/3+2, nDivs/2+3, nDivs };
int c0, c1, c2, c3;
word Target = Cover[nDivs];
if ( nDivs < 8 || p->pPars->fCover )
return Sbd_ManFindCandsSimple( p, Cover, nDivs );
Vec_IntClear( p->vDivVars );
for ( c0 = 0; c0 < nDivs; c0++ )
if ( Cover[c0] == Target )
{
Vec_IntPush( p->vDivVars, c0 );
return 1;
}
for ( c0 = 0; c0 < nDivs; c0++ )
for ( c1 = c0+1; c1 < nDivs; c1++ )
if ( (Cover[c0] | Cover[c1]) == Target )
{
Vec_IntPush( p->vDivVars, c0 );
Vec_IntPush( p->vDivVars, c1 );
return 1;
}
// count ones
for ( c0 = 0; c0 < nDivs; c0++ )
Ones[c0] = Abc_TtCountOnes( Cover[c0] );
// sort by the number of ones
for ( c0 = 0; c0 < nDivs; c0++ )
Order[c0] = c0;
Vec_IntSelectSortCost2Reverse( Order, nDivs, Ones );
// sort with limits
for ( c0 = 0; c0 < Limits[0]; c0++ )
for ( c1 = c0+1; c1 < Limits[1]; c1++ )
for ( c2 = c1+1; c2 < Limits[2]; c2++ )
if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]]) == Target )
{
Vec_IntPush( p->vDivVars, Order[c0] );
Vec_IntPush( p->vDivVars, Order[c1] );
Vec_IntPush( p->vDivVars, Order[c2] );
return 1;
}
for ( c0 = 0; c0 < Limits[0]; c0++ )
for ( c1 = c0+1; c1 < Limits[1]; c1++ )
for ( c2 = c1+1; c2 < Limits[2]; c2++ )
for ( c3 = c2+1; c3 < Limits[3]; c3++ )
{
if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]] | Cover[Order[c3]]) == Target )
{
Vec_IntPush( p->vDivVars, Order[c0] );
Vec_IntPush( p->vDivVars, Order[c1] );
Vec_IntPush( p->vDivVars, Order[c2] );
Vec_IntPush( p->vDivVars, Order[c3] );
return 1;
}
}
return 0;
}
int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
{
int fVerbose = 0;
@ -1158,7 +1234,7 @@ int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
assert( pCutRes[0] <= p->pPars->nLutSize );
memcpy( Sbd_ObjCut(p, Node), pCutRes, sizeof(int) * (pCutRes[0] + 1) );
//printf( "Setting node %d with delay %d.\n", Node, LevCur );
return LevCur == Abc_MaxInt(Level0, Level1);
return LevCur == 1; // LevCur == Abc_MaxInt(Level0, Level1);
}
int Sbd_ManDelay( Sbd_Man_t * p )
{
@ -1223,11 +1299,11 @@ void Sbd_ManFindCut( Sbd_Man_t * p, int Node, Vec_Int_t * vCutLits )
int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
{
Gia_Obj_t * pObj;
int i, k, w, iLit, Entry, Node;
int iObjLast = Gia_ManObjNum(p->pGia);
int iCurLev = Vec_IntEntry(p->vLutLevs, Pivot);
int iNewLev;
Gia_Obj_t * pObj;
// collect leaf literals
Vec_IntClear( p->vLits );
Vec_IntForEachEntry( p->vDivVars, Node, i )
@ -1239,12 +1315,13 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
Vec_IntPush( p->vLits, Abc_Var2Lit(Node, 0) );
}
// pretend to have MUXes
assert( p->pGia->pMuxes == NULL );
if ( p->pGia->nXors )
// assert( p->pGia->pMuxes == NULL );
if ( p->pGia->nXors && p->pGia->pMuxes == NULL )
p->pGia->pMuxes = (unsigned *)p;
// derive new function of the node
iLit = Dsm_ManTruthToGia( p->pGia, &Truth, p->vLits, p->vCover );
p->pGia->pMuxes = NULL;
if ( p->pGia->pMuxes == (unsigned *)p )
p->pGia->pMuxes = NULL;
// remember this function
assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 );
Vec_IntWriteEntry( p->vMirrors, Pivot, iLit );
@ -1323,6 +1400,8 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
if ( p->pMuxes )
pNew->pMuxes = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
Gia_ManConst0(p)->Value = 0;
Gia_ManHashAlloc( pNew );
Gia_ManForEachCi( p, pObj, i )
@ -1333,6 +1412,7 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
Gia_ManTransferTiming( pNew, p );
return pNew;
}
@ -1347,36 +1427,69 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
SeeAlso []
***********************************************************************/
void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
{
int RetValue; word Truth = 0;
if ( Sbd_ManMergeCuts( p, Pivot ) )
return;
//if ( Pivot != 344 )
// continue;
if ( p->pPars->fVerbose )
printf( "\nLooking at node %d\n", Pivot );
if ( Sbd_ManWindow( p, Pivot ) )
return;
RetValue = Sbd_ManCheckConst( p, Pivot );
if ( RetValue >= 0 )
Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
else if ( Sbd_ManExplore( p, Pivot, &Truth ) )
Sbd_ManImplement( p, Pivot, Truth );
}
Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
Sbd_Man_t * p = Sbd_ManStart( pGia, pPars );
int nNodesOld = Gia_ManObjNum(pGia);//, Count = 0;
int RetValue, Pivot; word Truth = 0;
int k, Pivot;
assert( pPars->nLutSize <= 6 );
//Sbd_ManMergeTest( p );
//return NULL;
Gia_ManForEachAndId( pGia, Pivot )
if ( pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)pGia->pManTime) )
{
if ( Pivot >= nNodesOld )
break;
if ( Sbd_ManMergeCuts( p, Pivot ) )
continue;
//if ( Pivot != 344 )
// continue;
if ( p->pPars->fVerbose )
printf( "\nLooking at node %d\n", Pivot );
if ( Sbd_ManWindow( p, Pivot ) )
continue;
RetValue = Sbd_ManCheckConst( p, Pivot );
if ( RetValue >= 0 )
Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
else if ( Sbd_ManExplore( p, Pivot, &Truth ) )
Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( pGia );
Tim_Man_t * pTimOld = (Tim_Man_t *)pGia->pManTime;
pGia->pManTime = Tim_ManDup( pTimOld, 1 );
Tim_ManIncrementTravId( (Tim_Man_t *)pGia->pManTime );
Gia_ManForEachObjVec( vNodes, pGia, pObj, k )
{
Sbd_ManImplement( p, Pivot, Truth );
//if ( Count++ == 1 )
// break;
Pivot = Gia_ObjId( pGia, pObj );
if ( Pivot >= nNodesOld )
continue;
if ( Gia_ObjIsAnd(pObj) )
Sbd_NtkPerformOne( p, Pivot );
else if ( Gia_ObjIsCi(pObj) )
{
int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj) );
Vec_IntWriteEntry( p->vLutLevs, Pivot, arrTime );
}
else if ( Gia_ObjIsCo(pObj) )
{
int arrTime = Vec_IntEntry( p->vLutLevs, Gia_ObjFaninId0(pObj, Pivot) );
Tim_ManSetCoArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj), arrTime );
}
else if ( !Gia_ObjIsConst0(pObj) )
assert( 0 );
}
//Tim_ManPrint( pGia->pManTime );
Tim_ManStop( (Tim_Man_t *)pGia->pManTime );
pGia->pManTime = pTimOld;
Vec_IntFree( vNodes );
}
else
{
Gia_ManForEachAndId( pGia, Pivot )
if ( Pivot < nNodesOld )
Sbd_NtkPerformOne( p, Pivot );
}
printf( "Found %d constants and %d replacements with delay %d. ", p->nConsts, p->nChanges, Sbd_ManDelay(p) );
p->timeTotal = Abc_Clock() - p->timeTotal;
@ -1384,13 +1497,16 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
pNew = Sbd_ManDerive( pGia, p->vMirrors );
// print runtime statistics
p->timeOther = p->timeTotal - p->timeWin - p->timeCnf - p->timeSat - p->timeCov - p->timeEnu;
ABC_PRTP( "Win", p->timeWin , p->timeTotal );
ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal );
ABC_PRTP( "Sat", p->timeSat , p->timeTotal );
ABC_PRTP( "Cov", p->timeCov , p->timeTotal );
ABC_PRTP( "Enu", p->timeEnu , p->timeTotal );
ABC_PRTP( "Oth", p->timeOther, p->timeTotal );
ABC_PRTP( "ALL", p->timeTotal, p->timeTotal );
if ( 0 )
{
ABC_PRTP( "Win", p->timeWin , p->timeTotal );
ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal );
ABC_PRTP( "Sat", p->timeSat , p->timeTotal );
ABC_PRTP( "Cov", p->timeCov , p->timeTotal );
ABC_PRTP( "Enu", p->timeEnu , p->timeTotal );
ABC_PRTP( "Oth", p->timeOther, p->timeTotal );
ABC_PRTP( "ALL", p->timeTotal, p->timeTotal );
}
Sbd_ManStop( p );
return pNew;
}

5
src/opt/sbd/sbdWin.c
View File

@ -123,7 +123,10 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vFaninVars), Vec_IntLimit(vFaninVars) );
Vec_IntFree( vFaninVars );
if ( RetValue == 0 )
return 0;
{
sat_solver_delete( pSat );
return NULL;
}
assert( sat_solver_nvars(pSat) == nVars + 32 );
}
// finalize