Skip to content

A
abc
Commit e0ad9de7 by Alan Mishchenko
Options

Improvements to delay-optimization in &satlut.

parent d53161a7
Showing with 330 additions and 87 deletions
src/aig/gia/giaSatLut.c
......@@ -46,6 +46,11 @@ struct Sbl_Man_t_
Vec_Int_t * vNodes; // internal LUTs
Vec_Int_t * vRoots; // driver nodes (a subset of vAnds)
Vec_Int_t * vRootVars; // driver nodes (as SAT variables)
// timing
Vec_Int_t * vArrs; // arrival times
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)
// cuts
Vec_Wrd_t * vCutsI; // input bit patterns
Vec_Wrd_t * vCutsN; // node bit patterns
......@@ -54,8 +59,9 @@ struct Sbl_Man_t_
Vec_Int_t * vCutsObj; // object to which this cut belongs
Vec_Wrd_t * vTempI; // temporary cuts
Vec_Wrd_t * vTempN; // temporary cuts
Vec_Int_t * vSolCuts; // cuts belonging to solution
Vec_Int_t * vSolCuts2; // cuts belonging to solution
Vec_Int_t * vSolInit; // initial solution
Vec_Int_t * vSolCur; // current solution
Vec_Int_t * vSolBest; // best solution
// temporary
Vec_Int_t * vLits; // literals
Vec_Int_t * vAssump; // literals
......@@ -68,6 +74,155 @@ struct Sbl_Man_t_
/**Function*************************************************************
Synopsis [Timing computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sbl_ManComputeDelay( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins )
{
int k, iFan, Delay = 0;
Vec_IntForEachEntry( vFanins, iFan, k )
Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vArrs, iFan) + 1 );
return Delay;
}
void Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart )
{
Vec_Int_t * vFanins;
int DelayMax = DelayStart, Delay, iLut, iFan, k;
// compute arrival times
Vec_IntFill( p->vArrs, Gia_ManObjNum(p->pGia), 0 );
Gia_ManForEachLut2( p->pGia, iLut )
{
vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
Vec_IntWriteEntry( p->vArrs, iLut, Delay );
DelayMax = Abc_MaxInt( DelayMax, Delay );
}
// compute required times
Vec_IntFill( p->vReqs, Gia_ManObjNum(p->pGia), ABC_INFINITY );
Gia_ManForEachCoDriverId( p->pGia, iLut, k )
Vec_IntDowndateEntry( p->vReqs, iLut, DelayMax );
Gia_ManForEachLut2Reverse( p->pGia, iLut )
{
Delay = Vec_IntEntry(p->vReqs, iLut) - 1;
vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
Vec_IntForEachEntry( vFanins, iFan, k )
Vec_IntDowndateEntry( p->vReqs, iFan, Delay );
}
}
/**Function*************************************************************
Synopsis [For each node in the window, create fanins.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sbl_ManGetCurrentMapping( Sbl_Man_t * p )
{
Vec_Int_t * vObj;
word CutI, CutN;
int i, c, b, iObj;
Vec_WecClear( p->vWindow );
Vec_WecInit( p->vWindow, Vec_IntSize(p->vAnds) );
assert( Vec_IntSize(p->vSolCur) > 0 );
Vec_IntForEachEntry( p->vSolCur, c, i )
{
CutI = Vec_WrdEntry( p->vCutsI, c );
CutN = Vec_WrdEntry( p->vCutsN, c );
iObj = Vec_IntEntry( p->vCutsObj, c );
//iObj = Vec_IntEntry( p->vAnds, iObj );
vObj = Vec_WecEntry( p->vWindow, iObj );
assert( Vec_IntSize(vObj) == 0 );
for ( b = 0; b < 64; b++ )
if ( (CutI >> b) & 1 )
Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) );
for ( b = 0; b < 64; b++ )
if ( (CutN >> b) & 1 )
Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, b) );
}
}
/**Function*************************************************************
Synopsis [Given mapping in p->vSolCur, check the critical path.]
Description [Returns 1 if the mapping satisfies the timing. Returns 0,
if the critical path is detected.]
SideEffects []
SeeAlso []
***********************************************************************/
int Sbl_ManCriticalFanin( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins )
{
int k, iFan, Delay = Vec_IntEntry(p->vArrs, iLut);
Vec_IntForEachEntry( vFanins, iFan, k )
if ( Vec_IntEntry(p->vArrs, iFan) + 1 == Delay )
return iFan;
return -1;
}
int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo )
{
Vec_Int_t * vFanins;
int i, iLut, iAnd, Delay, Required;
Vec_IntClear( p->vPath );
// derive timing
Sbl_ManCreateTiming( p, DelayGlo );
// update new timing
Sbl_ManGetCurrentMapping( p );
Vec_IntForEachEntry( p->vAnds, iLut, i )
{
vFanins = Vec_WecEntry( p->vWindow, i );
Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
Vec_IntWriteEntry( p->vArrs, iLut, Delay );
}
// compare timing at the root nodes
Vec_IntForEachEntry( p->vRoots, iLut, i )
{
Delay = Vec_IntEntry( p->vArrs, iLut );
Required = Vec_IntEntry( p->vReqs, iLut );
if ( Delay > Required ) // updated timing exceeded original timing
break;
}
if ( i == Vec_IntSize(p->vRoots) )
return 1;
// derive the critical path
// find SAT variable of the node whose GIA ID is "iLut"
iAnd = Vec_IntFind( p->vAnds, iLut );
assert( iAnd >= 0 );
// critical path begins in node "iLut", which is i-th root of the window
assert( iAnd == Vec_IntEntry(p->vRootVars, i) );
while ( 1 )
{
Vec_IntPush( p->vPath, Abc_Var2Lit(iAnd, 1) );
// find fanins of this node
vFanins = Vec_WecEntry( p->vWindow, iAnd );
// find critical fanin
iLut = Sbl_ManCriticalFanin( p, iLut, vFanins );
assert( iLut > 0 );
// find SAT variable of the node whose GIA ID is "iLut"
iAnd = Vec_IntFind( p->vAnds, iLut );
if ( iAnd == -1 )
break;
}
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
......@@ -83,7 +238,7 @@ void Sbl_ManUpdateMapping( Sbl_Man_t * p )
Vec_Int_t * vObj;
word CutI, CutN;
int i, c, b, iObj, iTemp;
assert( Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) );
assert( Vec_IntSize(p->vSolBest) < Vec_IntSize(p->vSolInit) );
Vec_IntForEachEntry( p->vAnds, iObj, i )
{
vObj = Vec_WecEntry(p->pGia->vMapping2, iObj);
......@@ -91,7 +246,7 @@ void Sbl_ManUpdateMapping( Sbl_Man_t * p )
Gia_ObjLutRefDecId( p->pGia, iTemp );
Vec_IntClear( vObj );
}
Vec_IntForEachEntry( p->vSolCuts2, c, i )
Vec_IntForEachEntry( p->vSolBest, c, i )
{
CutI = Vec_WrdEntry( p->vCutsI, c );
CutN = Vec_WrdEntry( p->vCutsN, c );
......@@ -274,7 +429,7 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
}
// create current solution
Vec_IntClear( p->vPolar );
Vec_IntClear( p->vSolCuts );
Vec_IntClear( p->vSolInit );
Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
{
word CutI = 0, CutN = 0;
......@@ -284,7 +439,7 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
assert( (int)pObj->Value == Vec_IntSize(p->vLeaves) + i );
// add node
Vec_IntPush( p->vPolar, i );
Vec_IntPush( p->vSolCuts, i );
Vec_IntPush( p->vSolInit, i );
// add its cut
//Gia_LutForEachFaninObj( p->pGia, Obj, pFanin, k )
vFanins = Gia_ObjLutFanins2( p->pGia, Obj );
......@@ -390,14 +545,20 @@ Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN )
p->vNodes = Vec_IntAlloc( 64 );
p->vRoots = Vec_IntAlloc( 64 );
p->vRootVars = Vec_IntAlloc( 64 );
// timing
p->vArrs = Vec_IntAlloc( 0 );
p->vReqs = Vec_IntAlloc( 0 );
p->vWindow = Vec_WecAlloc( 128 );
p->vPath = Vec_IntAlloc( 32 );
// cuts
p->vCutsI = Vec_WrdAlloc( 1000 ); // input bit patterns
p->vCutsN = Vec_WrdAlloc( 1000 ); // node bit patterns
p->vCutsNum = Vec_IntAlloc( 64 ); // cut counts for each obj
p->vCutsStart = Vec_IntAlloc( 64 ); // starting cuts for each obj
p->vCutsObj = Vec_IntAlloc( 1000 );
p->vSolCuts = Vec_IntAlloc( 64 );
p->vSolCuts2 = Vec_IntAlloc( 64 );
p->vSolInit = Vec_IntAlloc( 64 );
p->vSolCur = Vec_IntAlloc( 64 );
p->vSolBest = Vec_IntAlloc( 64 );
p->vTempI = Vec_WrdAlloc( 32 );
p->vTempN = Vec_WrdAlloc( 32 );
// internal
......@@ -419,14 +580,20 @@ void Sbl_ManStop( Sbl_Man_t * p )
Vec_IntFree( p->vNodes );
Vec_IntFree( p->vRoots );
Vec_IntFree( p->vRootVars );
// timing
Vec_IntFree( p->vArrs );
Vec_IntFree( p->vReqs );
Vec_WecFree( p->vWindow );
Vec_IntFree( p->vPath );
// cuts
Vec_WrdFree( p->vCutsI );
Vec_WrdFree( p->vCutsN );
Vec_IntFree( p->vCutsNum );
Vec_IntFree( p->vCutsStart );
Vec_IntFree( p->vCutsObj );
Vec_IntFree( p->vSolCuts );
Vec_IntFree( p->vSolCuts2 );
Vec_IntFree( p->vSolInit );
Vec_IntFree( p->vSolCur );
Vec_IntFree( p->vSolBest );
Vec_WrdFree( p->vTempI );
Vec_WrdFree( p->vTempN );
// temporary
......@@ -473,13 +640,15 @@ int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot )
return Count;
}
int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, 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 );
fVerbose |= fVeryVerbose;
// compute one window
Count = Sbl_ManWindow2( p, iPivot );
......@@ -499,7 +668,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
return 0;
}
if ( Vec_IntSize(p->vAnds) < 20 )
if ( Vec_IntSize(p->vAnds) < 10 )
{
if ( fVerbose )
printf( "Skipping.\n" );
......@@ -512,10 +681,10 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
// derive SAT instance
Sbl_ManCreateCnf( p );
if ( fVerbose )
Vec_IntPrint( p->vSolCuts );
if ( fVeryVerbose )
Vec_IntPrint( p->vSolInit );
if ( fVerbose )
if ( fVeryVerbose )
printf( "All clauses = %d. Multi clauses = %d. Binary clauses = %d. Other clauses = %d.\n\n",
sat_solver_nclauses(p->pSat), Vec_IntSize(p->vAnds), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vAnds),
sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI) );
......@@ -532,15 +701,14 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) );
// Vec_IntPrint( p->vAssump );
Vec_IntClear( p->vSolCuts2 );
StartSol = Vec_IntSize(p->vSolCuts) + 1;
StartSol = Vec_IntSize(p->vSolInit) + 1;
// StartSol = 30;
while ( fKeepTrying && StartSol-fKeepTrying > 0 )
{
int nConfBef, nConfAft;
if ( fVerbose )
printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying );
// for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ )
// for ( i = Vec_IntSize(p->vSolInit)-5; i < nVars; i++ )
// Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) );
Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) );
// solve the problem
......@@ -554,7 +722,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
if ( status == l_True )
{
int Count = 0, LitCount = 0;
if ( fVerbose )
if ( fVeryVerbose )
{
printf( "Inputs = %d. ANDs = %d. Total = %d. All vars = %d.\n",
Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds),
......@@ -574,25 +742,52 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
// printf( "%d", sat_solver_var_value(p->pSat, i) );
// printf( "\n" );
Count = 1;
Vec_IntClear( p->vSolCuts2 );
Vec_IntClear( p->vSolCur );
for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
if ( sat_solver_var_value(p->pSat, i) )
{
if ( fVerbose )
if ( fVeryVerbose )
printf( "Cut %3d : Node = %3d Node = %6d ", Count++, Vec_IntEntry(p->vCutsObj, i-p->FirstVar), Vec_IntEntry(p->vAnds, Vec_IntEntry(p->vCutsObj, i-p->FirstVar)) );
if ( fVerbose )
if ( fVeryVerbose )
LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar );
Vec_IntPush( p->vSolCuts2, i-p->FirstVar );
Vec_IntPush( p->vSolCur, i-p->FirstVar );
}
if ( fVerbose )
if ( fVeryVerbose )
printf( "LitCount = %d.\n", LitCount );
if ( fVerbose )
if ( fVeryVerbose )
Vec_IntPrint( p->vRootVars );
//Vec_IntPrint( p->vRoots );
//Vec_IntPrint( p->vAnds );
//Vec_IntPrint( p->vLeaves );
}
fKeepTrying = status == l_True ? fKeepTrying + 1 : 0;
// fKeepTrying = status == l_True ? fKeepTrying + 1 : 0;
// check the timing
if ( status == l_True )
{
if ( fDelay && !Sbl_ManEvaluateMapping(p, DelayMax) )
{
int iLit, value;
if ( fVerbose )
{
printf( "Critical path of length (%d) is detected: ", Vec_IntSize(p->vPath) );
Vec_IntForEachEntry( p->vPath, iLit, i )
printf( "%d=%d ", i, Vec_IntEntry(p->vAnds, Abc_Lit2Var(iLit)) );
printf( "\n" );
}
// add the clause
value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vPath), Vec_IntLimit(p->vPath) );
assert( value );
}
else
{
Vec_IntClear( p->vSolBest );
Vec_IntAppend( p->vSolBest, p->vSolCur );
fKeepTrying++;
}
}
else
fKeepTrying = 0;
if ( fVerbose )
{
if ( status == l_False )
......@@ -601,17 +796,21 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
printf( "SAT " );
else
printf( "UNDEC " );
printf( "confl =%8d. ", nConfAft - nConfBef );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
printf( "Total " );
printf( "confl =%8d. ", nConfTotal );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
printf( "\n" );
}
}
// update solution
if ( Vec_IntSize(p->vSolCuts2) > 0 && Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) )
if ( Vec_IntSize(p->vSolBest) > 0 && Vec_IntSize(p->vSolBest) < Vec_IntSize(p->vSolInit) )
{
Sbl_ManUpdateMapping( p );
printf( "Object %d : Saved %d nodes. (Conf = %d.)\n", iPivot, Vec_IntSize(p->vSolCuts)-Vec_IntSize(p->vSolCuts2), nConfTotal );
printf( "Object %5d : Saved %d nodes. (Conf =%8d.)\n", iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal );
Sbl_ManStop( p );
return 2;
}
......@@ -619,7 +818,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
return 1;
}
void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nConfl, int fReverse, int fVerbose )
void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nBTLimit, int DelayMax, int fDelay, int fReverse, int fVeryVerbose, int fVerbose )
{
int iLut;
Gia_ManComputeOneWinStart( pGia, fReverse );
......@@ -627,7 +826,7 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nConfl, int fReverse, int
{
// if ( iLut > 259 )
// break;
if ( Sbl_ManTestSat( pGia, nConfl, iLut, fVerbose ) != 2 )
if ( Sbl_ManTestSat( pGia, nBTLimit, iLut, DelayMax, fDelay, fVeryVerbose, fVerbose ) != 2 )
continue;
// break;
}
......
src/aig/gia/giaSplit.c
......@@ -209,12 +209,14 @@ void Spl_ManWinFindLeavesRoots( Spl_Man_t * p )
iFan = Gia_ObjFaninId0( pObj, iObj );
if ( !Vec_BitEntry(p->vMarksAnd, iFan) )
{
assert( Gia_ObjIsLut2(p->pGia, iFan) || Vec_BitEntry(p->vMarksCIO, iFan) );
Vec_BitWriteEntry(p->vMarksAnd, iFan, 1);
Vec_IntPush( p->vLeaves, iFan );
}
iFan = Gia_ObjFaninId1( pObj, iObj );
if ( !Vec_BitEntry(p->vMarksAnd, iFan) )
{
assert( Gia_ObjIsLut2(p->pGia, iFan) || Vec_BitEntry(p->vMarksCIO, iFan) );
Vec_BitWriteEntry(p->vMarksAnd, iFan, 1);
Vec_IntPush( p->vLeaves, iFan );
}
......@@ -297,6 +299,28 @@ int Spl_ManCountMarkedFanins( Gia_Man_t * p, int iObj, Vec_Bit_t * vMarks )
Count++;
return Count;
}
int Spl_ManFindGoodCand( Spl_Man_t * p )
{
int i, iObj;
int Res = 0, InCount, InCountMax = -1;
// mark leaves
Vec_IntForEachEntry( p->vInputs, iObj, i )
Vec_BitWriteEntry( p->vMarksIn, iObj, 1 );
// find candidate with maximum input overlap
Vec_IntForEachEntry( p->vCands, iObj, i )
{
InCount = Spl_ManCountMarkedFanins( p->pGia, iObj, p->vMarksIn );
if ( InCountMax < InCount )
{
InCountMax = InCount;
Res = iObj;
}
}
// unmark leaves
Vec_IntForEachEntry( p->vInputs, iObj, i )
Vec_BitWriteEntry( p->vMarksIn, iObj, 0 );
return Res;
}
/**Function*************************************************************
......@@ -313,45 +337,58 @@ int Spl_ManFindOne( Spl_Man_t * p )
{
Vec_Int_t * vVec;
int nFanouts, iObj, iFan, i, k;
int Res = 0, InCount, InCountMax = -1;
Vec_IntClear( p->vCands );
Vec_IntClear( p->vInputs );
int Res = 0;
// deref
Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
Vec_IntForEachEntry( vVec, iFan, k )
Gia_ObjLutRefDecId( p->pGia, iFan );
// consider LUT inputs - get one that has no refs
if ( p->fReverse )
{
Gia_ManForEachLut2VecReverse( p->vNodes, p->pGia, vVec, iObj, i )
Vec_IntForEachEntry( vVec, iFan, k )
if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) )
{
if ( !Gia_ObjLutRefNumId(p->pGia, iFan) )
{
Res = iFan;
goto finish;
}
Vec_IntPush( p->vCands, iFan );
Vec_IntPush( p->vInputs, iFan );
}
}
else
// collect external nodes
if ( p->fReverse && (Vec_IntSize(p->vNodes) & 1) )
{
Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
Vec_IntForEachEntry( vVec, iFan, k )
if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) )
{
if ( !Gia_ObjLutRefNumId(p->pGia, iFan) )
{
Res = iFan;
goto finish;
}
Vec_IntPush( p->vCands, iFan );
Vec_IntPush( p->vInputs, iFan );
}
Vec_IntForEachEntry( p->vNodes, iObj, i )
{
if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 0 )
continue;
assert( Gia_ObjLutRefNumId(p->pGia, iObj) > 0 );
if ( Gia_ObjLutRefNumId(p->pGia, iObj) >= 5 ) // skip nodes with high fanout!
continue;
nFanouts = Spl_ManLutFanouts( p->pGia, iObj, p->vFanouts, p->vMarksNo, p->vMarksCIO );
if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 1 && nFanouts == 1 )
{
Res = Vec_IntEntry(p->vFanouts, 0);
goto finish;
}
//Vec_IntAppend( p->vCands, p->vFanouts );
}
}
// consider LUT inputs - get one that has no refs
Vec_IntClear( p->vCands );
Vec_IntClear( p->vInputs );
Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
Vec_IntForEachEntry( vVec, iFan, k )
if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) && !Gia_ObjLutRefNumId(p->pGia, iFan) )
{
Vec_IntPush( p->vCands, iFan );
Vec_IntPush( p->vInputs, iFan );
}
Res = Spl_ManFindGoodCand( p );
if ( Res )
goto finish;
// collect candidates
Vec_IntClear( p->vCands );
Vec_IntClear( p->vInputs );
Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
Vec_IntForEachEntry( vVec, iFan, k )
if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) )
{
Vec_IntPush( p->vCands, iFan );
Vec_IntPush( p->vInputs, iFan );
}
// all inputs have refs - collect external nodes
Vec_IntForEachEntry( p->vNodes, iObj, i )
{
......@@ -369,22 +406,10 @@ int Spl_ManFindOne( Spl_Man_t * p )
Vec_IntAppend( p->vCands, p->vFanouts );
}
// mark leaves
Vec_IntForEachEntry( p->vInputs, iObj, i )
Vec_BitWriteEntry( p->vMarksIn, iObj, 1 );
// find candidate with maximum input overlap
Vec_IntForEachEntry( p->vCands, iObj, i )
{
InCount = Spl_ManCountMarkedFanins( p->pGia, iObj, p->vMarksIn );
if ( InCountMax < InCount )
{
InCountMax = InCount;
Res = iObj;
}
}
// unmark leaves
Vec_IntForEachEntry( p->vInputs, iObj, i )
Vec_BitWriteEntry( p->vMarksIn, iObj, 0 );
// choose among not-so-good ones
Res = Spl_ManFindGoodCand( p );
if ( Res )
goto finish;
// get the first candidate
if ( Res == 0 && Vec_IntSize(p->vCands) > 0 )
......
src/base/abci/abc.c
......@@ -34827,10 +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 nConfl, int fReverse, int fVerbose );
int c, nNumber = 64, nConfl = 500, fReverse = 0, fVerbose = 0;
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;
int fDelay = 0, fReverse = 0, fVeryVerbose = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NCrvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NCDdrwvh" ) ) != EOF )
{
switch ( c )
{
......@@ -34854,12 +34855,27 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-C\" should be followed by a positive integer.\n" );
goto usage;
}
nConfl = atoi(argv[globalUtilOptind]);
nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by a positive integer.\n" );
goto usage;
}
DelayMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'd':
fDelay ^= 1;
break;
case 'r':
fReverse ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -34880,15 +34896,18 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( Gia_ManLutSizeMax(pAbc->pGia) > 4 )
Abc_Print( 0, "Current AIG has mapping into %d-LUTs.\n", Gia_ManLutSizeMax(pAbc->pGia) );
Gia_ManLutSat( pAbc->pGia, nNumber, nConfl, fReverse, fVerbose );
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 );
return 0;
usage:
Abc_Print( -2, "usage: &satlut [-NC num] [-rvh]\n" );
Abc_Print( -2, "usage: &satlut [-NCD 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", 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-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" );
Abc_Print( -2, "\t-h : prints the command usage\n");
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment