Skip to content

A
abc
Commit 304c63e8 by Alan Mishchenko
Options

Experiments with don't-cares.

parent 44605f5a
Showing with 176 additions and 50 deletions
src/base/abci/abc.c
......@@ -5676,7 +5676,7 @@ int Abc_CommandMfse( Abc_Frame_t * pAbc, int argc, char ** argv )
Acb_Par_t Pars, * pPars = &Pars; int c;
Acb_ParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "IOWFLCavwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "IOWFLCadvwh" ) ) != EOF )
{
switch ( c )
{
......@@ -5749,6 +5749,9 @@ int Abc_CommandMfse( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'a':
pPars->fArea ^= 1;
break;
case 'd':
pPars->fUseAshen ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -5788,7 +5791,7 @@ int Abc_CommandMfse( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: mfse [-IOWFLC <num>] [-avwh]\n" );
Abc_Print( -2, "usage: mfse [-IOWFLC <num>] [-advwh]\n" );
Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" );
Abc_Print( -2, "\t-I <num> : the number of levels in the TFI cone (2 <= num) [default = %d]\n", pPars->nTfiLevMax );
Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
......@@ -5797,6 +5800,7 @@ usage:
Abc_Print( -2, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
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 [default = %s]\n", pPars->fArea? "area": "delay" );
Abc_Print( -2, "\t-d : toggle using Ashenhurst decomposition [default = %s]\n", pPars->fUseAshen? "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");
......@@ -12380,6 +12384,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Cba_PrsReadBlifTest();
// Cba_PrsReadBlifTest();
}
Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
src/base/acb/acbAbc.c
......@@ -44,27 +44,18 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p )
Acb_Ntk_t * Acb_NtkFromAbc2( Abc_Ntk_t * p )
{
int fTrack = 1;
Acb_Man_t * pMan = Acb_ManAlloc( Abc_NtkSpec(p), 1, NULL, NULL, NULL, NULL );
int i, k, NameId = Abc_NamStrFindOrAdd( pMan->pStrs, Abc_NtkName(p), NULL );
Acb_Ntk_t * pNtk = Acb_NtkAlloc( pMan, NameId, Abc_NtkCiNum(p), Abc_NtkCoNum(p), Abc_NtkObjNum(p) );
Abc_Obj_t * pObj, * pFanin;
assert( Abc_NtkIsSopLogic(p) );
pNtk->nFaninMax = 6;
if ( fTrack ) Vec_IntFill( &pNtk->vArray2, Abc_NtkObjNumMax(p), -1 );
Abc_NtkForEachCi( p, pObj, i )
{
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 );
if ( fTrack ) Vec_IntWriteEntry( &pNtk->vArray2, pObj->iTemp, Abc_ObjId(pObj) );
}
Abc_NtkForEachNode( p, pObj, i )
{
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_LUT, Abc_ObjFaninNum(pObj), 0 );
if ( fTrack ) Vec_IntWriteEntry( &pNtk->vArray2, pObj->iTemp, Abc_ObjId(pObj) );
// printf( "%d -> %d\n%s", i, pObj->iTemp, (char *)pObj->pData );
}
Abc_NtkForEachCo( p, pObj, i )
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CO, 1, 0 );
Abc_NtkForEachNode( p, pObj, i )
......@@ -79,6 +70,40 @@ Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p )
Acb_NtkAdd( pMan, pNtk );
return pNtk;
}
Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p )
{
Acb_Man_t * pMan = Acb_ManAlloc( Abc_NtkSpec(p), 1, NULL, NULL, NULL, NULL );
int i, k, NameId = Abc_NamStrFindOrAdd( pMan->pStrs, Abc_NtkName(p), NULL );
Acb_Ntk_t * pNtk = Acb_NtkAlloc( pMan, NameId, Abc_NtkCiNum(p), Abc_NtkCoNum(p), Abc_NtkObjNumMax(p)-1 );
Abc_Obj_t * pObj, * pFanin;
assert( Abc_NtkIsSopLogic(p) );
pNtk->nFaninMax = 6;
for ( i = 1; i < Abc_NtkObjNumMax(p); i++ )
{
pObj = Abc_NtkObj( p, i );
if ( pObj == NULL )
Acb_ObjAlloc( pNtk, ABC_OPER_NONE, 0, 0 );
else if ( Abc_ObjIsCi(pObj) )
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 );
else if ( Abc_ObjIsCo(pObj) )
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CO, 1, 0 );
else if ( Abc_ObjIsNode(pObj) )
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_LUT, Abc_ObjFaninNum(pObj), 0 );
else assert( 0 );
assert( pObj == NULL || pObj->iTemp == (int)Abc_ObjId(pObj) );
}
Abc_NtkForEachNode( p, pObj, i )
Abc_ObjForEachFanin( pObj, pFanin, k )
Acb_ObjAddFanin( pNtk, pObj->iTemp, pFanin->iTemp );
Abc_NtkForEachCo( p, pObj, i )
Acb_ObjAddFanin( pNtk, pObj->iTemp, Abc_ObjFanin(pObj, 0)->iTemp );
Acb_NtkCleanObjTruths( pNtk );
Abc_NtkForEachNode( p, pObj, i )
Acb_ObjSetTruth( pNtk, pObj->iTemp, Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj)) );
Acb_NtkSetRegNum( pNtk, Abc_NtkLatchNum(p) );
Acb_NtkAdd( pMan, pNtk );
return pNtk;
}
/**Function*************************************************************
......@@ -218,6 +243,7 @@ void Acb_ParSetDefault( Acb_Par_t * pPars )
pPars->nNodesMax = 0; // the maximum number of nodes to try
pPars->iNodeOne = 0; // one particular node to try
pPars->fArea = 1; // performs optimization for area
pPars->fUseAshen = 0; // use Ashenhurst decomposition
pPars->fMoreEffort = 0; // enables using more effort
pPars->fVerbose = 0; // enable basic stats
pPars->fVeryVerbose = 0; // enable detailed stats
......
src/base/acb/acbMfs.c
......@@ -430,15 +430,15 @@ void Acb_NtkPrintVec( Acb_Ntk_t * p, Vec_Int_t * vVec, char * pName )
int i;
printf( "%s: ", pName );
for ( i = 0; i < vVec->nSize; i++ )
printf( "%d ", Vec_IntEntry(&p->vArray2, vVec->pArray[i]) );
printf( "%d ", vVec->pArray[i] );
printf( "\n" );
}
void Acb_NtkPrintNode( Acb_Ntk_t * p, int Node )
{
int k, iFanin, * pFanins;
printf( "Node %d : ", Vec_IntEntry(&p->vArray2, Node) );
printf( "Node %d : ", Node );
Acb_ObjForEachFaninFast( p, Node, pFanins, iFanin, k )
printf( "%d ", Vec_IntEntry(&p->vArray2, iFanin) );
printf( "%d ", iFanin );
printf( "\n" );
}
void Acb_NtkPrintVec2( Acb_Ntk_t * p, Vec_Int_t * vVec, char * pName )
......@@ -579,7 +579,6 @@ void Acb_ObjMarkTfo2( Acb_Ntk_t * p, Vec_Int_t * vMarked )
int Acb_ObjLabelTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax, int fFirst )
{
int iFanout, i, Diff, fHasNone = 0;
//printf( "Visiting %d\n", Vec_IntEntry(&p->vArray2, iObj) );
if ( (Diff = Acb_ObjTravIdDiff(p, iObj)) <= 2 )
return Diff;
Acb_ObjSetTravIdDiff( p, iObj, 2 );
......@@ -871,15 +870,15 @@ static inline void Vec_IntRemap( Vec_Int_t * p, Vec_Int_t * vMap )
static inline void Acb_WinPrint( Acb_Ntk_t * p, Vec_Int_t * vWin, int Pivot, int nDivs )
{
int i, Node;
printf( "Window for node %d with %d divisors:\n", Vec_IntEntry(&p->vArray2, Pivot), nDivs );
printf( "Window for node %d with %d divisors:\n", Pivot, nDivs );
Vec_IntForEachEntry( vWin, Node, i )
{
if ( i == nDivs )
printf( " | " );
if ( Abc_Lit2Var(Node) == Pivot )
printf( "(%d) ", Vec_IntEntry(&p->vArray2, Pivot) );
printf( "(%d) ", Pivot );
else
printf( "%s%d ", Abc_LitIsCompl(Node) ? "*":"", Vec_IntEntry(&p->vArray2, Abc_Lit2Var(Node)) );
printf( "%s%d ", Abc_LitIsCompl(Node) ? "*":"", Abc_Lit2Var(Node) );
}
printf( "\n" );
}
......@@ -1316,7 +1315,7 @@ int Acb_NtkOptNode( Acb_Mfs_t * p, int Pivot )
p->timeWin += Abc_Clock() - clk;
PivotVar = Vec_IntFind( vWin, Abc_Var2Lit(Pivot, 0) );
if ( p->pPars->fVerbose )
printf( "Node %d: Window contains %d objects and %d divisors. ", Vec_IntEntry(&p->pNtk->vArray2, Pivot), Vec_IntSize(vWin), nDivs );
printf( "Node %d: Window contains %d objects and %d divisors. ", Pivot, Vec_IntSize(vWin), nDivs );
// Acb_WinPrint( p->pNtk, vWin, Pivot, nDivs );
// Acb_NtkPrintVecWin( p->pNtk, vWin, "Win" );
if ( Vec_IntSize(vWin) > p->pPars->nWinNodeMax )
......@@ -1445,7 +1444,7 @@ int Acb_NtkOptNode( Acb_Mfs_t * p, int Pivot )
}
//#if 0
if ( Acb_NtkObjMffcEstimate(p->pNtk, Pivot) >= 2 )// && Pivot != 70 )
if ( p->pPars->fUseAshen && Acb_NtkObjMffcEstimate(p->pNtk, Pivot) >= 2 )// && Pivot != 70 )
{
p->nTwoNodes++;
// derive SAT solver
......@@ -1614,7 +1613,7 @@ void Acb_NtkOpt( Acb_Ntk_t * pNtk, Acb_Par_t * pPars )
while ( Vec_QueTopPriority(pNtk->vQue) > 0 )
{
int iObj = Vec_QuePop(pNtk->vQue);
if ( Acb_ObjLevelD(pNtk, iObj) == 1 )
if ( !Acb_ObjType(pNtk, iObj) )
continue;
//if ( iObj != 28 )
// continue;
......
src/base/acb/acbPar.h
......@@ -46,6 +46,7 @@ struct Acb_Par_t_
int nGrowthLevel; // the maximum allowed growth in level
int nBTLimit; // the maximum number of conflicts in one SAT run
int nNodesMax; // the maximum number of nodes to try
int fUseAshen; // user Ashenhurst decomposition
int iNodeOne; // one particular node to try
int fArea; // performs optimization for area
int fMoreEffort; // performs high-affort minimization
......
src/base/acb/acbUtil.c
......@@ -133,13 +133,14 @@ int Acb_NtkComputeLevelR( Acb_Ntk_t * p, Vec_Int_t * vTfi )
{
// it is assumed that vTfi contains CI nodes
int i, iObj, Level = 0;
if ( !Acb_NtkHasObjLevelD( p ) )
Acb_NtkCleanObjLevelD( p );
if ( !Acb_NtkHasObjLevelR( p ) )
Acb_NtkCleanObjLevelR( p );
Vec_IntForEachEntryReverse( vTfi, iObj, i )
Acb_ObjComputeLevelR( p, iObj );
Acb_NtkForEachCi( p, iObj, i )
Level = Abc_MaxInt( Level, Acb_ObjLevelR(p, iObj) );
assert( p->LevelMax == Level );
// assert( p->LevelMax == Level );
p->LevelMax = Level;
return Level;
}
......@@ -176,16 +177,38 @@ int Acb_ObjComputePathD( Acb_Ntk_t * p, int iObj )
Path += Acb_ObjPathD(p, iFanin);
return Acb_ObjSetPathD( p, iObj, Path );
}
int Acb_NtkComputePathsD( Acb_Ntk_t * p, Vec_Int_t * vTfo )
int Acb_NtkComputePathsD( Acb_Ntk_t * p, Vec_Int_t * vTfo, int fReverse )
{
int i, iObj, Path = 0;
// it is assumed that vTfo contains CO nodes
//Vec_IntPrint( vTfo );
if ( !Acb_NtkHasObjPathD( p ) )
Acb_NtkCleanObjPathD( p );
// it is assumed that vTfo contains CI nodes
//assert( Acb_ObjSlack(p, Vec_IntEntry(vTfo, 0)) );
Vec_IntForEachEntryReverse( vTfo, iObj, i )
if ( !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathD( p, iObj );
else
Acb_ObjSetPathD( p, iObj, 0 );
if ( fReverse )
{
Vec_IntForEachEntryReverse( vTfo, iObj, i )
{
if ( Acb_ObjIsCi(p, iObj) )
Acb_ObjSetPathD( p, iObj, Acb_ObjSlack(p, iObj) == 0 );
else if ( Acb_ObjSlack(p, iObj) )
Acb_ObjSetPathD( p, iObj, 0 );
else
Acb_ObjComputePathD( p, iObj );
}
}
else
{
Vec_IntForEachEntry( vTfo, iObj, i )
{
if ( Acb_ObjIsCi(p, iObj) )
Acb_ObjSetPathD( p, iObj, Acb_ObjSlack(p, iObj) == 0 );
else if ( Acb_ObjSlack(p, iObj) )
Acb_ObjSetPathD( p, iObj, 0 );
else
Acb_ObjComputePathD( p, iObj );
}
}
Acb_NtkForEachCo( p, iObj, i )
Path += Acb_ObjPathD(p, iObj);
p->nPaths = Path;
......@@ -201,30 +224,69 @@ int Acb_ObjComputePathR( Acb_Ntk_t * p, int iObj )
Path += Acb_ObjPathR(p, iFanout);
return Acb_ObjSetPathR( p, iObj, Path );
}
int Acb_NtkComputePathsR( Acb_Ntk_t * p, Vec_Int_t * vTfi )
int Acb_NtkComputePathsR( Acb_Ntk_t * p, Vec_Int_t * vTfi, int fReverse )
{
int i, iObj, Path = 0;
// it is assumed that vTfi contains CI nodes
if ( !Acb_NtkHasObjPathR( p ) )
Acb_NtkCleanObjPathR( p );
// it is assumed that vTfi contains CO nodes
//assert( Acb_ObjSlack(p, Vec_IntEntry(vTfi, 0)) );
Vec_IntForEachEntryReverse( vTfi, iObj, i )
if ( !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathR( p, iObj );
else
Acb_ObjSetPathR( p, iObj, 0 );
if ( fReverse )
{
Vec_IntForEachEntryReverse( vTfi, iObj, i )
{
if ( Acb_ObjIsCo(p, iObj) )
Acb_ObjSetPathR( p, iObj, Acb_ObjSlack(p, iObj) == 0 );
else if ( Acb_ObjSlack(p, iObj) )
Acb_ObjSetPathR( p, iObj, 0 );
else
Acb_ObjComputePathR( p, iObj );
}
}
else
{
Vec_IntForEachEntry( vTfi, iObj, i )
{
if ( Acb_ObjIsCo(p, iObj) )
Acb_ObjSetPathR( p, iObj, Acb_ObjSlack(p, iObj) == 0 );
else if ( Acb_ObjSlack(p, iObj) )
Acb_ObjSetPathR( p, iObj, 0 );
else
Acb_ObjComputePathR( p, iObj );
}
}
Acb_NtkForEachCi( p, iObj, i )
Path += Acb_ObjPathR(p, iObj);
assert( p->nPaths == Path );
// assert( p->nPaths == Path );
p->nPaths = Path;
return Path;
}
void Acb_NtkPrintPaths( Acb_Ntk_t * p )
{
int iObj;
Acb_NtkForEachObj( p, iObj )
{
printf( "Obj = %5d : ", iObj );
printf( "PathD = %5d ", Acb_ObjPathD(p, iObj) );
printf( "PathR = %5d ", Acb_ObjPathR(p, iObj) );
printf( "Paths = %5d ", Acb_ObjPathD(p, iObj) + Acb_ObjPathR(p, iObj) );
printf( "\n" );
}
}
int Acb_NtkComputePaths( Acb_Ntk_t * p )
{
int LevelD, LevelR;
Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, -1, 1 );
Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, -1, 1 );
Acb_NtkComputeLevelD( p, vTfi );
Acb_NtkComputeLevelR( p, vTfo );
Acb_NtkComputePathsD( p, vTfi );
Acb_NtkComputePathsR( p, vTfo );
Acb_NtkComputeLevelD( p, vTfo );
LevelD = p->LevelMax;
Acb_NtkComputeLevelR( p, vTfi );
LevelR = p->LevelMax;
assert( LevelD == LevelR );
Acb_NtkComputePathsD( p, vTfo, 1 );
Acb_NtkComputePathsR( p, vTfi, 1 );
return p->nPaths;
}
void Abc_NtkComputePaths( Abc_Ntk_t * p )
......@@ -232,7 +294,9 @@ void Abc_NtkComputePaths( Abc_Ntk_t * p )
extern Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p );
Acb_Ntk_t * pNtk = Acb_NtkFromAbc( p );
Acb_NtkCreateFanout( pNtk );
Acb_NtkCleanObjCounts( pNtk );
printf( "Computed %d paths.\n", Acb_NtkComputePaths(pNtk) );
Acb_NtkPrintPaths( pNtk );
Acb_ManFree( pNtk->pDesign );
}
......@@ -251,6 +315,8 @@ void Abc_NtkComputePaths( Abc_Ntk_t * p )
void Acb_ObjUpdatePriority( Acb_Ntk_t * p, int iObj )
{
int nPaths;
if ( Acb_ObjIsCio(p, iObj) || Acb_ObjLevelD(p, iObj) == 1 )
return;
if ( p->vQue == NULL )
{
Acb_NtkCleanObjCounts( p );
......@@ -258,35 +324,63 @@ void Acb_ObjUpdatePriority( Acb_Ntk_t * p, int iObj )
Vec_QueSetPriority( p->vQue, Vec_FltArrayP(&p->vCounts) );
}
nPaths = Acb_ObjPathD(p, iObj) + Acb_ObjPathR(p, iObj);
if ( nPaths == 0 )
return;
Acb_ObjSetCounts( p, iObj, (float)nPaths );
if ( Vec_QueIsMember( p->vQue, iObj ) )
{
//printf( "Updating object %d with count %d\n", iObj, nPaths );
Vec_QueUpdate( p->vQue, iObj );
else
}
else if ( nPaths )
{
//printf( "Adding object %d with count %d\n", iObj, nPaths );
Vec_QuePush( p->vQue, iObj );
}
}
void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj )
{
int i, Entry, LevelMax = p->LevelMax;
// assuming that level of the new nodes is up to date
int LevelD, LevelR, nPaths1, nPaths2;
// assuming that direct level of the new nodes (including iObj) is up to date
Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, iObj, 1 );
Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, iObj, 1 );
if ( iObj > 0 )
{
assert( Vec_IntEntryLast(vTfi) == iObj );
assert( Vec_IntEntryLast(vTfo) == iObj );
Vec_IntPop( vTfo );
}
Acb_NtkComputeLevelD( p, vTfo );
LevelD = p->LevelMax;
Acb_NtkComputeLevelR( p, vTfi );
LevelR = p->LevelMax;
assert( LevelD == LevelR );
if ( iObj > 0 && LevelMax > p->LevelMax ) // reduced level
{
iObj = -1;
vTfi = Acb_ObjCollectTfi( p, -1, 1 );
vTfo = Acb_ObjCollectTfo( p, -1, 1 );
Vec_QueClear( p->vQue );
// add backup here
}
Acb_NtkComputePathsD( p, vTfo );
Acb_NtkComputePathsR( p, vTfi );
if ( iObj > 0 )
Acb_NtkComputePathsD( p, vTfi, 0 );
Acb_NtkComputePathsD( p, vTfo, 1 );
nPaths1 = p->nPaths;
if ( iObj > 0 )
Acb_NtkComputePathsR( p, vTfo, 0 );
Acb_NtkComputePathsR( p, vTfi, 1 );
nPaths2 = p->nPaths;
assert( nPaths1 == nPaths2 );
Vec_IntForEachEntry( vTfi, Entry, i )
Acb_ObjUpdatePriority( p, Entry );
if ( iObj > 0 )
Vec_IntForEachEntry( vTfo, Entry, i )
Acb_ObjUpdatePriority( p, Entry );
// printf( "Updating timing for object %d.\n", iObj );
// Acb_NtkPrintPaths( p );
// while ( (Entry = (int)Vec_QueTopPriority(p->vQue)) > 0 )
// printf( "Obj = %5d : Prio = %d.\n", Vec_QuePop(p->vQue), Entry );
}
/**Function*************************************************************
......@@ -341,6 +435,7 @@ void Acb_NtkResetNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp
void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp )
{
Acb_NtkResetNode( p, Pivot, uTruth, vSupp );
Acb_ObjComputeLevelD( p, Pivot );
if ( p->vQue == NULL )
Acb_NtkUpdateLevelD( p, Pivot );
else
......
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