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

Updates to delay optimization project.

This commit is contained in:
Alan Mishchenko 2017-01-02 16:29:10 +07:00
parent 6e1df46cd3
commit 74c8d35f33
8 changed files with 272 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -2775,6 +2775,10 @@ SOURCE=.\src\opt\sbd\sbdLut.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbdPath.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbdSat.c
# End Source File
# Begin Source File

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

@ -41010,7 +41010,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, "KSNPWFMCacvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KSNPWFMCmcdpvwh" ) ) != EOF )
{
switch ( c )
{
@ -41102,11 +41102,17 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nBTLimit < 0 )
goto usage;
break;
case 'a':
pPars->fArea ^= 1;
case 'm':
pPars->fMapping ^= 1;
break;
case 'c':
pPars->fCover ^= 1;
pPars->fMoreCuts ^= 1;
break;
case 'd':
pPars->fFindDivs ^= 1;
break;
case 'p':
pPars->fUsePath ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
@ -41122,25 +41128,22 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Mfs(): There is no AIG.\n" );
Abc_Print( -1, "Abc_CommandAbc9Mfsd(): There is no AIG.\n" );
return 0;
}
if ( Gia_ManBufNum(pAbc->pGia) )
{
Abc_Print( -1, "Abc_CommandAbc9Mfs(): This command does not work with barrier buffers.\n" );
Abc_Print( -1, "Abc_CommandAbc9Mfsd(): This command does not work with barrier buffers.\n" );
return 1;
}
if ( Gia_ManHasMapping(pAbc->pGia) )
{
Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has mapping (run &st to unmap).\n" );
return 0;
}
Abc_Print( 1, "The current AIG has mapping, which can be used to determine critical path if \"-p\" is selected.\n" );
pTemp = Sbd_NtkPerform( pAbc->pGia, pPars );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &mfsd [-KSNPWFMC <num>] [-acvwh]\n" );
Abc_Print( -2, "usage: &mfsd [-KSNPWFMC <num>] [-mcdpvwh]\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-S <num> : the LUT structure size (1 <= num <= 2) [default = %d]\n", pPars->nLutNum );
@ -41150,8 +41153,10 @@ usage:
Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nTfoFanMax );
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-m : toggle generating delay-oriented mapping [default = %s]\n", pPars->fMapping? "area": "area+edges" );
Abc_Print( -2, "\t-c : toggle using several cuts at each node [default = %s]\n", pPars->fMoreCuts? "yes": "no" );
Abc_Print( -2, "\t-d : toggle additional search for good divisors [default = %s]\n", pPars->fFindDivs? "yes": "no" );
Abc_Print( -2, "\t-p : toggle optimizing critical path only [default = %s]\n", pPars->fUsePath? "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");

1
src/opt/sbd/module.make
View File

@ -4,5 +4,6 @@ SRC += src/opt/sbd/sbd.c \
src/opt/sbd/sbdCut.c \
src/opt/sbd/sbdCut2.c \
src/opt/sbd/sbdLut.c \
src/opt/sbd/sbdPath.c \
src/opt/sbd/sbdSat.c \
src/opt/sbd/sbdWin.c

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

@ -47,6 +47,10 @@ struct Sbd_Par_t_
int nWinSizeMax; // maximum window size (windowing)
int nBTLimit; // maximum number of SAT conflicts
int nWords; // simulation word count
int fMapping; // generate mapping
int fMoreCuts; // use several cuts
int fFindDivs; // perform divisor search
int fUsePath; // optimize only critical path
int fArea; // area-oriented optimization
int fCover; // use complete cover procedure
int fVerbose; // verbose flag

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

@ -38,6 +38,7 @@ struct Sbd_Man_t_
Vec_Wec_t * vTfos; // TFO for each node (roots are marked) (windowing)
Vec_Int_t * vLutLevs; // LUT level for each node after resynthesis
Vec_Int_t * vLutCuts; // LUT cut for each nodes after resynthesis
Vec_Int_t * vLutCuts2; // LUT cut for each nodes after resynthesis
Vec_Int_t * vMirrors; // alternative node
Vec_Wrd_t * vSims[4]; // simulation information (main, backup, controlability)
Vec_Int_t * vCover; // temporary
@ -73,7 +74,8 @@ struct Sbd_Man_t_
sat_solver * pSat; // SAT solver
};
static inline int * Sbd_ObjCut( Sbd_Man_t * p, int i ) { return Vec_IntEntryP( p->vLutCuts, (p->pPars->nLutSize + 1) * i ); }
static inline int * Sbd_ObjCut( Sbd_Man_t * p, int i ) { return Vec_IntEntryP( p->vLutCuts, (p->pPars->nLutSize + 1) * i ); }
static inline int * Sbd_ObjCut2( Sbd_Man_t * p, int i ) { return Vec_IntEntryP( p->vLutCuts2, (p->pPars->nLutSize + 1) * i ); }
static inline word * Sbd_ObjSim0( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[0], p->pPars->nWords * i ); }
static inline word * Sbd_ObjSim1( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[1], p->pPars->nWords * i ); }
@ -107,6 +109,10 @@ void Sbd_ParSetDefault( Sbd_Par_t * pPars )
pPars->nWinSizeMax = 2000; // maximum window size (windowing)
pPars->nBTLimit = 0; // maximum number of SAT conflicts
pPars->nWords = 1; // simulation word count
pPars->fMapping = 1; // generate mapping
pPars->fMoreCuts = 0; // use several cuts
pPars->fFindDivs = 0; // perform divisor search
pPars->fUsePath = 0; // optimize only critical path
pPars->fArea = 0; // area-oriented optimization
pPars->fCover = 0; // use complete cover procedure
pPars->fVerbose = 0; // verbose flag
@ -231,8 +237,13 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
for ( w = 0; w < p->pPars->nWords; w++ )
Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 );
// cut enumeration
p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nLutSize, pPars->nCutNum, 1, 1 );
p->pSrv = Sbd_ManCutServerStart( pGia, p->vMirrors, p->vLutLevs, NULL, NULL, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, 0 );
if ( pPars->fMoreCuts )
p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, !pPars->fMapping, 1 );
else
{
p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nLutSize, pPars->nCutNum, !pPars->fMapping, 1 );
p->pSrv = Sbd_ManCutServerStart( pGia, p->vMirrors, p->vLutLevs, NULL, NULL, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, 0 );
}
return p;
}
void Sbd_ManStop( Sbd_Man_t * p )
@ -258,8 +269,8 @@ void Sbd_ManStop( Sbd_Man_t * p )
Vec_IntFree( p->vCounts[1] );
Vec_WrdFree( p->vMatrix );
sat_solver_delete_p( &p->pSat );
Sbd_StoFree( p->pSto );
Sbd_ManCutServerStop( p->pSrv );
if ( p->pSto ) Sbd_StoFree( p->pSto );
if ( p->pSrv ) Sbd_ManCutServerStop( p->pSrv );
ABC_FREE( p );
}
@ -1830,7 +1841,7 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
{
Gia_Obj_t * pObj = NULL;
//Gia_Obj_t * pObj = NULL;
int i, k, w, iLit, Node;
int iObjLast = Gia_ManObjNum(p->pGia);
int iCurLev = Vec_IntEntry(p->vLutLevs, Pivot);
@ -1903,6 +1914,7 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
//Vec_IntPush( p->vLevs, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObjI, i)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObjI, i))) );
Vec_IntPush( p->vObj2Var, 0 );
Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 );
Sbd_StoSaveBestDelayCut( p->pSto, i, Sbd_ObjCut(p, i) );
//Sbd_ManFindCut( p, i, p->vLits );
for ( k = 0; k < 4; k++ )
for ( w = 0; w < p->pPars->nWords; w++ )
@ -1912,7 +1924,7 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
iNewLev = Vec_IntEntry( p->vLutLevs, Abc_Lit2Var(iLit) );
assert( !iNewLev || iNewLev < iCurLev );
// update delay of the initial node
pObj = Gia_ManObj( p->pGia, Pivot );
//pObj = Gia_ManObj( p->pGia, Pivot );
assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
//Vec_IntWriteEntry( p->vLevs, Pivot, Pivot ? 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObj, Pivot)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObj, Pivot))) : 0 );
@ -1930,6 +1942,70 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
SeeAlso []
***********************************************************************/
void Sbd_ManDeriveMapping_rec( Sbd_Man_t * p, Gia_Man_t * pNew, int iObj )
{
Gia_Obj_t * pObj; int k, * pCut;
if ( Gia_ObjIsTravIdCurrentId(pNew, iObj) )
return;
Gia_ObjSetTravIdCurrentId(pNew, iObj);
pObj = Gia_ManObj( pNew, iObj );
if ( Gia_ObjIsCi(pObj) )
return;
assert( Gia_ObjIsAnd(pObj) );
pCut = Sbd_ObjCut2( p, iObj );
for ( k = 1; k <= pCut[0]; k++ )
Sbd_ManDeriveMapping_rec( p, pNew, pCut[k] );
// add mapping
Vec_IntWriteEntry( pNew->vMapping, iObj, Vec_IntSize(pNew->vMapping) );
for ( k = 0; k <= pCut[0]; k++ )
Vec_IntPush( pNew->vMapping, pCut[k] );
Vec_IntPush( pNew->vMapping, iObj );
}
void Sbd_ManDeriveMapping( Sbd_Man_t * p, Gia_Man_t * pNew )
{
Gia_Obj_t * pObj, * pFan;
int i, k, iFan, iObjNew, * pCut, * pCutNew;
Vec_Int_t * vLeaves = Vec_IntAlloc( 100 );
// derive cuts for the new manager
p->vLutCuts2 = Vec_IntStart( Gia_ManObjNum(pNew) * (p->pPars->nLutSize + 1) );
Gia_ManForEachAnd( p->pGia, pObj, i )
{
if ( Vec_IntEntry(p->vMirrors, i) >= 0 )
continue;
if ( pObj->Value == ~0 )
continue;
iObjNew = Abc_Lit2Var( pObj->Value );
if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, iObjNew)) )
continue;
pCutNew = Sbd_ObjCut2( p, iObjNew );
pCut = Sbd_ObjCut( p, i );
Vec_IntClear( vLeaves );
for ( k = 1; k <= pCut[0]; k++ )
{
iFan = Vec_IntEntry(p->vMirrors, pCut[k]) >= 0 ? Abc_Lit2Var(Vec_IntEntry(p->vMirrors, pCut[k])) : pCut[k];
pFan = Gia_ManObj( p->pGia, iFan );
if ( pFan->Value == ~0 )
continue;
iObjNew = Abc_Lit2Var( pFan->Value );
if ( iObjNew == 0 )
continue;
Vec_IntPushUniqueOrder( vLeaves, iObjNew );
}
assert( Vec_IntSize(vLeaves) <= p->pPars->nLutSize );
assert( Vec_IntSize(vLeaves) > 1 );
pCutNew[0] = Vec_IntSize(vLeaves);
memcpy( pCutNew+1, Vec_IntArray(vLeaves), sizeof(int) * Vec_IntSize(vLeaves) );
}
Vec_IntFree( vLeaves );
// create new mapping
Vec_IntFreeP( &pNew->vMapping );
pNew->vMapping = Vec_IntAlloc( (p->pPars->nLutSize + 2) * Gia_ManObjNum(pNew) );
Vec_IntFill( pNew->vMapping, Gia_ManObjNum(pNew), 0 );
Gia_ManIncrementTravId( pNew );
Gia_ManForEachCo( pNew, pObj, i )
Sbd_ManDeriveMapping_rec( p, pNew, Gia_ObjFaninId0p(pNew, pObj) );
Vec_IntFreeP( &p->vLutCuts2 );
}
void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * vMirrors )
{
Gia_Obj_t * pObj;
@ -1951,7 +2027,7 @@ void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * v
if ( Obj != Node )
Gia_ManObj(p, Node)->Value = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(Vec_IntEntry(vMirrors, Node)) );
}
Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
Gia_Man_t * Sbd_ManDerive( Sbd_Man_t * pMan, Gia_Man_t * p, Vec_Int_t * vMirrors )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
@ -1973,9 +2049,12 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
Gia_ManTransferTiming( pNew, p );
if ( pMan->pPars->fMapping )
Sbd_ManDeriveMapping( pMan, pNew );
// remove dangling nodes
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManTransferTiming( pNew, pTemp );
Gia_ManTransferMapping( pNew, pTemp );
Gia_ManStop( pTemp );
return pNew;
}
@ -1993,7 +2072,7 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
***********************************************************************/
void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
{
Sbd_Str_t Strs[SBD_DIV_MAX]; //word Truth = 0;
Sbd_Str_t Strs[SBD_DIV_MAX]; word Truth = 0;
int RetValue, nStrs = 0;
if ( !p->pSto && Sbd_ManMergeCuts( p, Pivot ) )
return;
@ -2009,8 +2088,7 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
if ( p->pPars->fVerbose ) printf( "Node %5d: Detected constant %d.\n", Pivot, RetValue );
}
/*
else if ( p->pPars->nLutNum >= 1 && Sbd_ManExplore2( p, Pivot, &Truth ) )
else if ( p->pPars->fFindDivs && p->pPars->nLutNum >= 1 && Sbd_ManExplore2( p, Pivot, &Truth ) )
{
int i;
Strs->fLut = 1;
@ -2021,7 +2099,6 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
Sbd_ManImplement2( p, Pivot, 1, Strs );
if ( p->pPars->fVerbose ) printf( "Node %5d: Detected LUT%d\n", Pivot, p->pPars->nLutSize );
}
*/
else if ( p->pPars->nLutNum >= 2 && Sbd_ManExplore3( p, Pivot, &nStrs, Strs ) )
{
Sbd_ManImplement2( p, Pivot, nStrs, Strs );
@ -2041,6 +2118,7 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
Vec_Bit_t * vPath;
Sbd_Man_t * p = Sbd_ManStart( pGia, pPars );
int nNodesOld = Gia_ManObjNum(pGia);
int k, Pivot;
@ -2049,6 +2127,7 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
Gia_ManForEachObj( p->pGia, pObj, Pivot )
Sbd_StoRefObj( p->pSto, Pivot, -1 );
//return NULL;
vPath = (pPars->fUsePath && Gia_ManHasMapping(pGia)) ? Sbc_ManCriticalPath(pGia) : NULL;
if ( pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)pGia->pManTime) )
{
Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( pGia );
@ -2065,9 +2144,10 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
{
abctime clk = Abc_Clock();
int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
Sbd_StoSaveBestDelayCut( p->pSto, Pivot, Sbd_ObjCut(p, Pivot) );
p->timeCut += Abc_Clock() - clk;
Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
if ( Delay > 1 )//&& Gia_ObjRefNumId(p->pGia, Pivot) > 1 )
if ( Delay > 1 && (!vPath || Vec_BitEntry(vPath, Pivot)) )
Sbd_NtkPerformOne( p, Pivot );
}
else if ( Gia_ObjIsCi(pObj) )
@ -2102,22 +2182,25 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
{
abctime clk = Abc_Clock();
int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
Sbd_StoSaveBestDelayCut( p->pSto, Pivot, Sbd_ObjCut(p, Pivot) );
p->timeCut += Abc_Clock() - clk;
Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
if ( Delay > 1 )//&& Gia_ObjRefNumId(p->pGia, Pivot) > 1 )
if ( Delay > 1 && (!vPath || Vec_BitEntry(vPath, Pivot)) )
Sbd_NtkPerformOne( p, Pivot );
}
//if ( nNodesOld != Gia_ManObjNum(pGia) )
// break;
}
}
Vec_BitFreeP( &vPath );
printf( "K = %d. S = %d. N = %d. P = %d. ",
p->pPars->nLutSize, p->pPars->nLutNum, p->pPars->nCutSize, p->pPars->nCutNum );
printf( "Try = %d. Use = %d. C = %d. 1 = %d. 2 = %d. 3a = %d. 3b = %d. Lev = %d. ",
p->nTried, p->nUsed, p->nLuts[0], p->nLuts[1], p->nLuts[2], p->nLuts[3], p->nLuts[4], Sbd_ManDelay(p) );
p->timeTotal = Abc_Clock() - p->timeTotal;
Abc_PrintTime( 1, "Time", p->timeTotal );
pNew = Sbd_ManDerive( pGia, p->vMirrors );
//Sbd_ManDeriveMapping2( p );
pNew = Sbd_ManDerive( p, pGia, p->vMirrors );
// print runtime statistics
p->timeOther = p->timeTotal - p->timeWin - p->timeCut - p->timeCov - p->timeCnf - p->timeSat - p->timeQbf;
//if ( p->pPars->fVerbose )

22
src/opt/sbd/sbdCut.c
View File

@ -65,10 +65,11 @@ struct Sbd_Sto_t_
Sbd_Cut_t * ppCuts[SBD_MAX_CUTNUM]; // temporary cut pointers
int nCutsR; // the number of cuts
int Pivot; // current object
double CutCount[4]; // cut counters
int iCutBest; // best-delay cut
int nCutsSpec; // special cuts
int nCutsOver; // overflow cuts
int DelayMin; // minimum delay
double CutCount[4]; // cut counters
abctime clkStart; // starting time
};
@ -540,6 +541,7 @@ static inline void Sbd_StoComputeDelay( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pC
{
int i, v, Delay, DelayMin = ABC_INFINITY;
assert( nCuts > 0 );
p->iCutBest = -1;
for ( i = 0; i < nCuts; i++ )
{
if ( (int)pCuts[i]->nLeaves > p->nLutSize )
@ -547,8 +549,16 @@ static inline void Sbd_StoComputeDelay( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pC
Delay = 0;
for ( v = 0; v < (int)pCuts[i]->nLeaves; v++ )
Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vDelays, pCuts[i]->pLeaves[v]) );
DelayMin = Abc_MinInt( DelayMin, Delay );
//DelayMin = Abc_MinInt( DelayMin, Delay );
if ( DelayMin > Delay )
{
DelayMin = Delay;
p->iCutBest = i;
}
else if ( DelayMin == Delay && p->iCutBest >= 0 && pCuts[p->iCutBest]->nLeaves > pCuts[i]->nLeaves )
p->iCutBest = i;
}
assert( p->iCutBest >= 0 );
assert( DelayMin < ABC_INFINITY );
DelayMin = (nCuts > 1 || pCuts[0]->nLeaves > 1) ? DelayMin + 1 : DelayMin;
Vec_IntWriteEntry( p->vDelays, iObj, DelayMin );
@ -725,6 +735,14 @@ int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj )
Sbd_StoMergeCuts( p, iObj );
return Vec_IntEntry( p->vDelays, iObj );
}
void Sbd_StoSaveBestDelayCut( Sbd_Sto_t * p, int iObj, int * pCut )
{
Sbd_Cut_t * pCutBest = p->ppCuts[p->iCutBest]; int i;
assert( iObj == p->Pivot );
pCut[0] = pCutBest->nLeaves;
for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
pCut[i+1] = pCutBest->pLeaves[i];
}
int Sbd_StoObjRefs( Sbd_Sto_t * p, int iObj )
{
return Vec_IntEntry(p->vRefs, iObj);

3
src/opt/sbd/sbdInt.h
View File

@ -92,6 +92,7 @@ extern void Sbd_StoComputeCutsConst0( Sbd_Sto_t * p, int iObj );
extern void Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level );
extern void Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level );
extern int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj );
extern void Sbd_StoSaveBestDelayCut( Sbd_Sto_t * p, int iObj, int * pCut );
extern int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves );
/*=== sbdCut2.c ==========================================================*/
extern Sbd_Srv_t * Sbd_ManCutServerStart( Gia_Man_t * pGia, Vec_Int_t * vMirrors,
@ -104,6 +105,8 @@ extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar,
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, int fQbf );
extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds );
extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset );
/*=== sbdPath.c ==========================================================*/
extern Vec_Bit_t * Sbc_ManCriticalPath( Gia_Man_t * p );
/*=== sbdQbf.c ==========================================================*/
extern int Sbd_ProblemSolve(
Gia_Man_t * p, Vec_Int_t * vMirrors,

124
src/opt/sbd/sbdPath.c Normal file
View File

@ -0,0 +1,124 @@
/**CFile****************************************************************
FileName [sbdPath.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based optimization using internal don't-cares.]
Synopsis [Critical path.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: sbdPath.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sbdInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sbc_ManAddInternalToPath_rec( Gia_Man_t * p, int iObj, Vec_Bit_t * vPath )
{
Gia_Obj_t * pObj;
int k, iFan, Value = 0;
if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
return Vec_BitEntry(vPath, iObj);
Gia_ObjSetTravIdCurrentId(p, iObj);
pObj = Gia_ManObj( p, iObj );
if ( Gia_ObjIsCi(pObj) )
return 0;
assert( Gia_ObjIsAnd(pObj) );
Gia_LutForEachFanin( p, iObj, iFan, k )
Value |= Sbc_ManAddInternalToPath_rec( p, iFan, vPath );
if ( Value )
Vec_BitWriteEntry( vPath, iObj, 1 );
return Value;
}
void Sbc_ManAddInternalToPath( Gia_Man_t * p, Vec_Bit_t * vPath )
{
int iObj;
Gia_ManForEachLut( p, iObj )
{
if ( !Vec_BitEntry(vPath, iObj) )
continue;
Gia_ManIncrementTravId( p );
Sbc_ManAddInternalToPath_rec( p, iObj, vPath );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sbc_ManCriticalPath_rec( Gia_Man_t * p, int * pLevels, int iObj, int LevelFan, Vec_Bit_t * vPath )
{
Gia_Obj_t * pObj; int k, iFan;
if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
return;
Gia_ObjSetTravIdCurrentId(p, iObj);
pObj = Gia_ManObj( p, iObj );
if ( Gia_ObjIsCi(pObj) )
return;
assert( Gia_ObjIsAnd(pObj) );
Vec_BitWriteEntry( vPath, iObj, 1 );
Gia_LutForEachFanin( p, iObj, iFan, k )
if ( pLevels[iFan] == LevelFan )
Sbc_ManCriticalPath_rec( p, pLevels, iFan, LevelFan-1, vPath );
}
Vec_Bit_t * Sbc_ManCriticalPath( Gia_Man_t * p )
{
int * pLevels = NULL, k, iDriver;
int nLevels = p->pManTime ? Gia_ManLutLevelWithBoxes(p) : Gia_ManLutLevel(p, &pLevels);
Vec_Bit_t * vPath = Vec_BitStart( Gia_ManObjNum(p) );
if ( p->pManTime )
pLevels = Vec_IntArray( p->vLevels );
Gia_ManIncrementTravId( p );
Gia_ManForEachCoDriverId( p, iDriver, k )
if ( pLevels[iDriver] == nLevels && iDriver )
Sbc_ManCriticalPath_rec( p, pLevels, iDriver, nLevels-1, vPath );
if ( !p->pManTime )
ABC_FREE( pLevels );
Sbc_ManAddInternalToPath( p, vPath );
return vPath;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END