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

Improvements to delay-optimization in &satlut.

This commit is contained in:
Alan Mishchenko 2016-04-04 08:43:22 -07:00
parent e0ad9de7ea
commit 4a954c1b23
4 changed files with 112 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/gia/gia.h
View File

@ -1499,6 +1499,7 @@ extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ManPrint( Gia_Man_t * p );
extern void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeaves, Vec_Int_t * vNodes );
extern void Gia_ManPrintConeMulti( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Int_t * vLeaves, Vec_Int_t * vNodes );
extern void Gia_ManPrintCone2( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
extern void Gia_ManInvertPos( Gia_Man_t * pAig );

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

@ -39,6 +39,7 @@ struct Sbl_Man_t_
int FirstVar; // first variable to be used
int LitShift; // shift in terms of literals (2*Gia_ManCiNum(pGia)+2)
int nInputs; // the number of inputs
int nEdges; // the number of edges
// window
Gia_Man_t * pGia;
Vec_Int_t * vLeaves; // leaf nodes
@ -51,6 +52,7 @@ struct Sbl_Man_t_
Vec_Int_t * vReqs; // required times
Vec_Wec_t * vWindow; // fanins of each node in the window
Vec_Int_t * vPath; // critical path (as SAT variables)
Vec_Int_t * vEdges; // fanin edges
// cuts
Vec_Wrd_t * vCutsI; // input bit patterns
Vec_Wrd_t * vCutsN; // node bit patterns
@ -83,25 +85,52 @@ struct Sbl_Man_t_
SeeAlso []
***********************************************************************/
int Sbl_ManComputeDelay( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins )
int Sbl_ManComputeDelay( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins, int * pEdges )
{
int k, iFan, Delay = 0;
int k, iFan, DelayMax = -1, Count = 0, iFanMax = -1;
*pEdges = -1;
Vec_IntForEachEntry( vFanins, iFan, k )
Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vArrs, iFan) + 1 );
return Delay;
{
int Delay = Vec_IntEntry(p->vArrs, iFan) + 1;
if ( DelayMax < Delay )
{
DelayMax = Delay;
iFanMax = k;
Count = 1;
}
else if ( DelayMax == Delay )
Count++;
}
if ( p->nEdges == 0 )
return DelayMax;
if ( p->nEdges == 1 )
{
if ( Count == 1 )
{
*pEdges = iFanMax;
return DelayMax - 1;
}
return DelayMax;
}
assert( 0 );
return 0;
}
void Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart )
int Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart, int * pnEdges )
{
Vec_Int_t * vFanins;
int DelayMax = DelayStart, Delay, iLut, iFan, k;
int DelayMax = DelayStart, Delay;
int iLut, iFan, k, Edges, nCountEdges = 0;
// compute arrival times
Vec_IntFill( p->vArrs, Gia_ManObjNum(p->pGia), 0 );
Vec_IntFill( p->vEdges, Gia_ManObjNum(p->pGia), -1 );
Gia_ManForEachLut2( p->pGia, iLut )
{
vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
Delay = Sbl_ManComputeDelay( p, iLut, vFanins, &Edges );
Vec_IntWriteEntry( p->vArrs, iLut, Delay );
Vec_IntWriteEntry( p->vEdges, iLut, Edges );
DelayMax = Abc_MaxInt( DelayMax, Delay );
nCountEdges += (Edges >= 0);
}
// compute required times
Vec_IntFill( p->vReqs, Gia_ManObjNum(p->pGia), ABC_INFINITY );
@ -110,10 +139,18 @@ void Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart )
Gia_ManForEachLut2Reverse( p->pGia, iLut )
{
Delay = Vec_IntEntry(p->vReqs, iLut) - 1;
Edges = Vec_IntEntry(p->vEdges, iLut);
assert( p->nEdges > 0 || Edges == -1 );
vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
Vec_IntForEachEntry( vFanins, iFan, k )
Vec_IntDowndateEntry( p->vReqs, iFan, Delay );
if ( k != Edges )
Vec_IntDowndateEntry( p->vReqs, iFan, Delay );
else
Vec_IntDowndateEntry( p->vReqs, iFan, Delay + 1 );
}
if ( pnEdges )
*pnEdges = nCountEdges;
return DelayMax;
}
/**Function*************************************************************
@ -175,17 +212,18 @@ int Sbl_ManCriticalFanin( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins )
int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo )
{
Vec_Int_t * vFanins;
int i, iLut, iAnd, Delay, Required;
int i, iLut = -1, iAnd, Delay, Required, Edges;
Vec_IntClear( p->vPath );
// derive timing
Sbl_ManCreateTiming( p, DelayGlo );
Sbl_ManCreateTiming( p, DelayGlo, NULL );
// update new timing
Sbl_ManGetCurrentMapping( p );
Vec_IntForEachEntry( p->vAnds, iLut, i )
{
vFanins = Vec_WecEntry( p->vWindow, i );
Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
Delay = Sbl_ManComputeDelay( p, iLut, vFanins, &Edges );
Vec_IntWriteEntry( p->vArrs, iLut, Delay );
Vec_IntWriteEntry( p->vEdges, iLut, Edges );
}
// compare timing at the root nodes
Vec_IntForEachEntry( p->vRoots, iLut, i )
@ -447,6 +485,10 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
{
Gia_Obj_t * pFanin = Gia_ManObj( p->pGia, Fanin );
assert( (int)pFanin->Value < Vec_IntSize(p->vLeaves) || Gia_ObjIsLut2(p->pGia, Fanin) );
// if ( ~pFanin->Value == 0 )
// Gia_ManPrintConeMulti( p->pGia, p->vAnds, p->vLeaves, p->vPath );
if ( ~pFanin->Value == 0 )
continue;
assert( ~pFanin->Value );
if ( (int)pFanin->Value < Vec_IntSize(p->vLeaves) )
CutI |= ((word)1 << pFanin->Value);
@ -457,7 +499,7 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
Index = Sbl_ManFindCut( p, Vec_IntSize(p->vLeaves) + i, CutI, CutN );
if ( Index < 0 )
{
printf( "Cannot find the available cut.\n" );
//printf( "Cannot find the available cut.\n" );
continue;
}
assert( Index >= 0 );
@ -550,6 +592,7 @@ Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN )
p->vReqs = Vec_IntAlloc( 0 );
p->vWindow = Vec_WecAlloc( 128 );
p->vPath = Vec_IntAlloc( 32 );
p->vEdges = Vec_IntAlloc( 32 );
// cuts
p->vCutsI = Vec_WrdAlloc( 1000 ); // input bit patterns
p->vCutsN = Vec_WrdAlloc( 1000 ); // node bit patterns
@ -585,6 +628,7 @@ void Sbl_ManStop( Sbl_Man_t * p )
Vec_IntFree( p->vReqs );
Vec_WecFree( p->vWindow );
Vec_IntFree( p->vPath );
Vec_IntFree( p->vEdges );
// cuts
Vec_WrdFree( p->vCutsI );
Vec_WrdFree( p->vCutsN );
@ -640,15 +684,17 @@ int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot )
return Count;
}
int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, int fDelay, int fVeryVerbose, int fVerbose )
int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, int nEdges, int fDelay, int fVeryVerbose, int fVerbose )
{
int fKeepTrying = 1;
abctime clk = Abc_Clock(), clk2;
int i, LogN = 6, nVars = 1 << LogN, status, Root;
Sbl_Man_t * p = Sbl_ManAlloc( pGia, LogN );
int StartSol, Count, nConfTotal = 0;
Vec_IntClear( p->vSolBest );
int StartSol, Count, nConfTotal = 0, nIters = 0;
p->nEdges = nEdges;
fVerbose |= fVeryVerbose;
Vec_IntClear( p->vSolBest );
// compute one window
Count = Sbl_ManWindow2( p, iPivot );
@ -717,6 +763,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), nBTLimit, 0, 0, 0 );
nConfAft = (int)p->pSat->stats.conflicts;
nConfTotal += nConfAft - nConfBef;
nIters++;
if ( status == l_Undef )
break;
if ( status == l_True )
@ -809,8 +856,11 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
// update solution
if ( Vec_IntSize(p->vSolBest) > 0 && Vec_IntSize(p->vSolBest) < Vec_IntSize(p->vSolInit) )
{
int nDelay, nEdges;
nDelay = Sbl_ManCreateTiming( p, DelayMax, &nEdges );
Sbl_ManUpdateMapping( p );
printf( "Object %5d : Saved %d nodes. (Conf =%8d.)\n", iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal );
printf( "Object %5d : Saved %d nodes (Conf =%8d) Iter =%3d Delay = %d Edges = %4d\n",
iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal, nIters, nDelay, nEdges );
Sbl_ManStop( p );
return 2;
}
@ -818,7 +868,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
return 1;
}
void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nBTLimit, int DelayMax, int fDelay, int fReverse, int fVeryVerbose, int fVerbose )
void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVeryVerbose, int fVerbose )
{
int iLut;
Gia_ManComputeOneWinStart( pGia, fReverse );
@ -826,7 +876,7 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nBTLimit, int DelayMax, i
{
// if ( iLut > 259 )
// break;
if ( Sbl_ManTestSat( pGia, nBTLimit, iLut, DelayMax, fDelay, fVeryVerbose, fVerbose ) != 2 )
if ( Sbl_ManTestSat( pGia, nBTLimit, iLut, DelayMax, nEdges, fDelay, fVeryVerbose, fVerbose ) != 2 )
continue;
// break;
}

28
src/aig/gia/giaUtil.c
View File

@ -1341,6 +1341,22 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
printf( " mark0" );
if ( pObj->fMark1 )
printf( " mark1" );
if ( Gia_ManHasMapping(p) && Gia_ObjIsLut(p, Gia_ObjId(p, pObj)) )
{
int i, iFan;
printf( " Cut = { " );
Gia_LutForEachFanin( p, Gia_ObjId(p, pObj), iFan, i )
printf( "%d ", iFan );
printf( "}" );
}
if ( Gia_ManHasMapping2(p) && Gia_ObjIsLut2(p, Gia_ObjId(p, pObj)) )
{
int i, iFan;
printf( " Cut = { " );
Gia_LutForEachFanin2( p, Gia_ObjId(p, pObj), iFan, i )
printf( "%d ", iFan );
printf( "}" );
}
printf( "\n" );
/*
if ( p->pRefs )
@ -1417,6 +1433,18 @@ void Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeav
Gia_ManForEachObjVec( vNodes, p, pObj, i )
Gia_ObjPrint( p, pObj );
}
void Gia_ManPrintConeMulti( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
{
Gia_Obj_t * pObj;
int i;
Vec_IntClear( vNodes );
Vec_IntAppend( vNodes, vLeaves );
Gia_ManForEachObjVec( vObjs, p, pObj, i )
Gia_ManPrintCollect_rec( p, pObj, vNodes );
printf( "GIA logic cone for %d nodes:\n", Vec_IntSize(vObjs) );
Gia_ManForEachObjVec( vNodes, p, pObj, i )
Gia_ObjPrint( p, pObj );
}
void Gia_ManPrintCollect2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
{

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

@ -34827,11 +34827,11 @@ usage:
***********************************************************************/
int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nBTLimit, int DelayMax, int fDelay, int fReverse, int fVeryVerbose, int fVerbose );
int c, nNumber = 64, nBTLimit = 500, DelayMax = 0;
extern void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVeryVerbose, int fVerbose );
int c, nNumber = 64, nBTLimit = 500, DelayMax = 0, nEdges = 0;
int fDelay = 0, fReverse = 0, fVeryVerbose = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NCDdrwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NCDQdrwvh" ) ) != EOF )
{
switch ( c )
{
@ -34867,6 +34867,15 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
DelayMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'Q':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-Q\" should be followed by a positive integer.\n" );
goto usage;
}
nEdges = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'd':
fDelay ^= 1;
break;
@ -34898,15 +34907,16 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
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) );
else
Gia_ManLutSat( pAbc->pGia, nNumber, nBTLimit, DelayMax, fDelay, fReverse, fVeryVerbose, fVerbose );
Gia_ManLutSat( pAbc->pGia, nNumber, nBTLimit, DelayMax, nEdges, fDelay, fReverse, fVeryVerbose, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &satlut [-NCD num] [-drwvh]\n" );
Abc_Print( -2, "usage: &satlut [-NCDQ num] [-drwvh]\n" );
Abc_Print( -2, "\t performs SAT-based remapping of the 4-LUT network\n" );
Abc_Print( -2, "\t-N num : the limit on the number of AIG nodes in the window [default = %d]\n", nNumber );
Abc_Print( -2, "\t-C num : the limit on the number of conflicts [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-D num : the user-specified required times at the outputs [default = %d]\n", DelayMax );
Abc_Print( -2, "\t-Q num : the maximum number of edges [default = %d]\n", nEdges );
Abc_Print( -2, "\t-d : toggles delay optimization [default = %s]\n", fDelay? "yes": "no" );
Abc_Print( -2, "\t-r : toggles using reverse search [default = %s]\n", fReverse? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );