From e0ad9de7ea8c8fd34072a712f4579767b9055d6e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 3 Apr 2016 16:44:13 -0700 Subject: Improvements to delay-optimization in &satlut. --- src/aig/gia/giaSatLut.c | 261 ++++++++++++++++++++++++++++++++++++++++++------ src/aig/gia/giaSplit.c | 121 +++++++++++++--------- src/base/abci/abc.c | 35 +++++-- 3 files changed, 330 insertions(+), 87 deletions(-) diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c index f985eb50..3c8eb320 100644 --- a/src/aig/gia/giaSatLut.c +++ b/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 @@ -66,6 +72,155 @@ struct Sbl_Man_t_ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**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 [] @@ -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; } diff --git a/src/aig/gia/giaSplit.c b/src/aig/gia/giaSplit.c index 8bb5d3c0..b402f2ac 100644 --- a/src/aig/gia/giaSplit.c +++ b/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 ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 05712ada..5c3a573a 100644 --- a/src/base/abci/abc.c +++ b/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"); -- cgit v1.2.3