Skip to content

A
abc
Commit 9268c100 by Alan Mishchenko
Options

New MFS package.

parent d5234332
Showing with 61 additions and 32 deletions
src/base/abci/abcMfs.c
...@@ -53,7 +53,11 @@ Vec_Ptr_t * Abc_NtkAssignIDs( Abc_Ntk_t * pNtk ) ...@@ -53,7 +53,11 @@ Vec_Ptr_t * Abc_NtkAssignIDs( Abc_Ntk_t * pNtk )
Abc_NtkForEachPi( pNtk, pObj, i ) Abc_NtkForEachPi( pNtk, pObj, i )
pObj->iTemp = i; pObj->iTemp = i;
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
{
pObj->iTemp = Abc_NtkPiNum(pNtk) + i; pObj->iTemp = Abc_NtkPiNum(pNtk) + i;
//printf( "%d->%d ", pObj->Id, pObj->iTemp );
}
//printf( "\n" );
Abc_NtkForEachPo( pNtk, pObj, i ) Abc_NtkForEachPo( pNtk, pObj, i )
pObj->iTemp = Abc_NtkPiNum(pNtk) + Vec_PtrSize(vNodes) + i; pObj->iTemp = Abc_NtkPiNum(pNtk) + Vec_PtrSize(vNodes) + i;
return vNodes; return vNodes;
...@@ -119,6 +123,7 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p ) ...@@ -119,6 +123,7 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
Vec_Int_t * vMap, * vArray; Vec_Int_t * vMap, * vArray;
Abc_Obj_t * pNode; Abc_Obj_t * pNode;
int i, k, Fanin; int i, k, Fanin;
word * pTruth;
// map new IDs into old nodes // map new IDs into old nodes
vMap = Vec_IntStart( Abc_NtkObjNumMax(pNtk) ); vMap = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachPi( pNtk, pNode, i ) Abc_NtkForEachPi( pNtk, pNode, i )
...@@ -131,17 +136,26 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p ) ...@@ -131,17 +136,26 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
Abc_ObjRemoveFanins( pNode ); Abc_ObjRemoveFanins( pNode );
// create new fanins // create new fanins
Abc_NtkForEachNode( pNtk, pNode, i ) Abc_NtkForEachNode( pNtk, pNode, i )
if ( pNode->iTemp > 0 && !Sfm_NodeReadFixed(p, pNode->iTemp) )
{ {
vArray = Sfm_NodeReadFanins( p, pNode->iTemp ); if ( pNode->iTemp == 0 || Sfm_NodeReadFixed(p, pNode->iTemp) )
if ( Vec_IntSize(vArray) == 0 ) continue;
if ( !Sfm_NodeReadUsed(p, pNode->iTemp) )
{ {
Abc_NtkDeleteObj( pNode ); Abc_NtkDeleteObj( pNode );
continue; continue;
} }
// update fanins
vArray = Sfm_NodeReadFanins( p, pNode->iTemp );
Vec_IntForEachEntry( vArray, Fanin, k ) Vec_IntForEachEntry( vArray, Fanin, k )
Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) ); Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)Sfm_NodeReadTruth(p, pNode->iTemp) ); // update function
pTruth = Sfm_NodeReadTruth( p, pNode->iTemp );
if ( pTruth[0] == 0 )
pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 0\n" );
else if ( ~pTruth[0] == 0 )
pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 1\n" );
else
pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)pTruth );
} }
Vec_IntFree( vMap ); Vec_IntFree( vMap );
} }
......
src/opt/mfs/mfsCore.c
...@@ -101,7 +101,7 @@ int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode) ...@@ -101,7 +101,7 @@ int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
return 1; return 1;
// compute the divisors of the window // compute the divisors of the window
p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 ); p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
p->nTotalDivs += Vec_PtrSize(p->vDivs); p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
// construct AIG for the window // construct AIG for the window
p->pAigWin = Abc_NtkConstructAig( p, pNode ); p->pAigWin = Abc_NtkConstructAig( p, pNode );
// translate it into CNF // translate it into CNF
...@@ -250,7 +250,7 @@ p->timeWin += clock() - clk; ...@@ -250,7 +250,7 @@ p->timeWin += clock() - clk;
// compute the divisors of the window // compute the divisors of the window
clk = clock(); clk = clock();
p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 ); p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
p->nTotalDivs += Vec_PtrSize(p->vDivs); p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
p->timeDiv += clock() - clk; p->timeDiv += clock() - clk;
// construct AIG for the window // construct AIG for the window
clk = clock(); clk = clock();
......
src/opt/mfs/mfsCore_.c
...@@ -89,7 +89,7 @@ p->timeWin += clock() - clk; ...@@ -89,7 +89,7 @@ p->timeWin += clock() - clk;
// compute the divisors of the window // compute the divisors of the window
clk = clock(); clk = clock();
p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 ); p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
p->nTotalDivs += Vec_PtrSize(p->vDivs); p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
p->timeDiv += clock() - clk; p->timeDiv += clock() - clk;
// construct AIG for the window // construct AIG for the window
clk = clock(); clk = clock();
......
src/opt/sfm/sfm.h
...@@ -73,6 +73,7 @@ extern void Sfm_NtkFree( Sfm_Ntk_t * p ); ...@@ -73,6 +73,7 @@ extern void Sfm_NtkFree( Sfm_Ntk_t * p );
extern Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i ); extern Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i );
extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i ); extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
extern int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i ); extern int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i );
extern int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i );
/*=== sfmSat.c ==========================================================*/ /*=== sfmSat.c ==========================================================*/
......
src/opt/sfm/sfmCnf.c
...@@ -122,12 +122,12 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p ) ...@@ -122,12 +122,12 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
Vec_Wec_t * vCnfs; Vec_Wec_t * vCnfs;
Vec_Str_t * vCnf, * vCnfBase; Vec_Str_t * vCnf, * vCnfBase;
word uTruth; word uTruth;
int i; int i, nCubes;
vCnf = Vec_StrAlloc( 100 ); vCnf = Vec_StrAlloc( 100 );
vCnfs = Vec_WecStart( p->nObjs ); vCnfs = Vec_WecStart( p->nObjs );
Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos ) Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
{ {
Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf ); nCubes = Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i ); vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) ); Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) ); memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) );
......
src/opt/sfm/sfmCore.c
...@@ -48,8 +48,8 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars ) ...@@ -48,8 +48,8 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
pPars->nTfoLevMax = 2; // the maximum fanout levels pPars->nTfoLevMax = 2; // the maximum fanout levels
pPars->nFanoutMax = 10; // the maximum number of fanouts pPars->nFanoutMax = 10; // the maximum number of fanouts
pPars->nDepthMax = 0; // the maximum depth to try pPars->nDepthMax = 0; // the maximum depth to try
pPars->nDivNumMax = 200; // the maximum number of divisors pPars->nDivNumMax = 300; // the maximum number of divisors
pPars->nWinSizeMax = 500; // the maximum window size pPars->nWinSizeMax = 300; // the maximum window size
pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run
pPars->fFixLevel = 1; // does not allow level to increase pPars->fFixLevel = 1; // does not allow level to increase
pPars->fArea = 0; // performs optimization for area pPars->fArea = 0; // performs optimization for area
...@@ -111,14 +111,18 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly ) ...@@ -111,14 +111,18 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
clock_t clk; clock_t clk;
assert( Sfm_ObjIsNode(p, iNode) ); assert( Sfm_ObjIsNode(p, iNode) );
assert( f >= 0 && f < Sfm_ObjFaninNum(p, iNode) ); assert( f >= 0 && f < Sfm_ObjFaninNum(p, iNode) );
if ( iNode == 211 )
{
int i = 0;
}
if ( fRemoveOnly ) if ( fRemoveOnly )
p->nTryRemoves++; p->nTryRemoves++;
else else
p->nTryResubs++; p->nTryResubs++;
// report init stats // report init stats
if ( p->pPars->fVeryVerbose ) if ( p->pPars->fVeryVerbose )
printf( "Node %5d : Level = %2d. Divs = %3d. Fanin = %d (out of %d). MFFC = %d\n", printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Div=%3d. Fanin = %d/%d. MFFC = %d\n",
iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vDivs), f, Sfm_ObjFaninNum(p, iNode), iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), f, Sfm_ObjFaninNum(p, iNode),
Sfm_ObjFanoutNum(p, Sfm_ObjFanin(p, iNode, f)) == 1 ? Sfm_ObjMffcSize(p, iNode) : 0 ); Sfm_ObjFanoutNum(p, Sfm_ObjFanin(p, iNode, f)) == 1 ? Sfm_ObjMffcSize(p, iNode) : 0 );
// clean simulation info // clean simulation info
p->nCexes = 0; p->nCexes = 0;
...@@ -187,9 +191,9 @@ finish: ...@@ -187,9 +191,9 @@ finish:
if ( p->pPars->fVeryVerbose ) if ( p->pPars->fVeryVerbose )
{ {
if ( iVar == -1 ) if ( iVar == -1 )
printf( "Node %d: Fanin %d can be removed. ", iNode, f ); printf( "Node %d: Fanin %d (%d) can be removed. ", iNode, f, Sfm_ObjFanin(p, iNode, f) );
else else
printf( "Node %d: Fanin %d can be replaced by divisor %d. ", iNode, f, iVar ); printf( "Node %d: Fanin %d (%d) can be replaced by divisor %d. ", iNode, f, Sfm_ObjFanin(p, iNode, f), iVar );
Kit_DsdPrintFromTruth( (unsigned *)&uTruth, Vec_IntSize(p->vDivIds) ); printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned *)&uTruth, Vec_IntSize(p->vDivIds) ); printf( "\n" );
} }
if ( iVar == -1 ) if ( iVar == -1 )
...@@ -205,9 +209,10 @@ finish: ...@@ -205,9 +209,10 @@ finish:
int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode ) int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
{ {
int i, iFanin; int i, iFanin;
p->nNodesTried++;
// prepare SAT solver // prepare SAT solver
Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ); if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) )
return 0;
p->nNodesTried++;
Sfm_NtkWindowToSolver( p ); Sfm_NtkWindowToSolver( p );
Sfm_NtkPrepareDivisors( p, iNode ); Sfm_NtkPrepareDivisors( p, iNode );
// try replacing area critical fanins // try replacing area critical fanins
......
src/opt/sfm/sfmNtk.c
...@@ -243,6 +243,10 @@ void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin ) ...@@ -243,6 +243,10 @@ void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode ) void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
{ {
int i, iFanin; int i, iFanin;
if ( iNode == 202 )
{
int s = 0;
}
if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) ) if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) )
return; return;
assert( Sfm_ObjIsNode(p, iNode) ); assert( Sfm_ObjIsNode(p, iNode) );
...@@ -304,6 +308,10 @@ int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i ) ...@@ -304,6 +308,10 @@ int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i )
{ {
return (int)Vec_StrEntry( p->vFixed, i ); return (int)Vec_StrEntry( p->vFixed, i );
} }
int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i )
{
return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0);
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
src/opt/sfm/sfmSat.c
...@@ -123,8 +123,14 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) ...@@ -123,8 +123,14 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
RetValue = sat_solver_addclause( pSat1, &Lit, &Lit + 1 ); RetValue = sat_solver_addclause( pSat1, &Lit, &Lit + 1 );
assert( RetValue ); assert( RetValue );
// finalize // finalize
sat_solver_compress( pSat0 ); RetValue = sat_solver_simplify( pSat0 );
sat_solver_compress( pSat1 ); assert( RetValue );
RetValue = sat_solver_simplify( pSat1 );
if ( RetValue == 0 )
{
Sat_SolverWriteDimacs( pSat1, "test.cnf", NULL, NULL, 0 );
}
assert( RetValue );
// return the result // return the result
if ( p->pSat0 ) sat_solver_delete( p->pSat0 ); if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
if ( p->pSat1 ) sat_solver_delete( p->pSat1 ); if ( p->pSat1 ) sat_solver_delete( p->pSat1 );
......
src/opt/sfm/sfmWin.c
...@@ -179,7 +179,7 @@ int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode ) ...@@ -179,7 +179,7 @@ int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode ) void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
{ {
int i, iFanout; int i, iFanout;
Sfm_ObjForEachFanout( p, iNode, iFanout, i ) Sfm_ObjForEachFanout( p, iNode, iFanout, i )
...@@ -187,7 +187,7 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode ) ...@@ -187,7 +187,7 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode )
// skip TFI nodes, PO nodes, and nodes with high fanout or nodes with high logic level // skip TFI nodes, PO nodes, and nodes with high fanout or nodes with high logic level
if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) ||
Sfm_ObjFanoutNum(p, iFanout) >= p->pPars->nFanoutMax || Sfm_ObjFanoutNum(p, iFanout) >= p->pPars->nFanoutMax ||
(p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= Sfm_ObjLevel(p, iNode)) ) (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) )
continue; continue;
// handle single-input nodes // handle single-input nodes
if ( Sfm_ObjFaninNum(p, iFanout) == 1 ) if ( Sfm_ObjFaninNum(p, iFanout) == 1 )
...@@ -235,23 +235,18 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) ...@@ -235,23 +235,18 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
{ {
int i, iTemp; int i, iTemp;
clock_t clk = clock(); clock_t clk = clock();
/*
if ( iNode == 7 )
{
int iLevel = Sfm_ObjLevel(p, iNode);
int s = 0;
}
*/
assert( Sfm_ObjIsNode( p, iNode ) ); assert( Sfm_ObjIsNode( p, iNode ) );
Vec_IntClear( p->vLeaves ); // leaves Vec_IntClear( p->vLeaves ); // leaves
Vec_IntClear( p->vNodes ); // internal Vec_IntClear( p->vNodes ); // internal
Vec_IntClear( p->vDivs ); // divisors Vec_IntClear( p->vDivs ); // divisors
Vec_IntClear( p->vRoots ); // roots
Vec_IntClear( p->vTfo ); // roots
// collect transitive fanin // collect transitive fanin
Sfm_NtkIncrementTravId( p ); Sfm_NtkIncrementTravId( p );
Sfm_NtkCollectTfi_rec( p, iNode ); Sfm_NtkCollectTfi_rec( p, iNode );
if ( Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) > p->pPars->nWinSizeMax )
return 0;
// collect TFO (currently use only one level of TFO) // collect TFO (currently use only one level of TFO)
Vec_IntClear( p->vRoots ); // roots
Vec_IntClear( p->vTfo ); // roots
if ( Sfm_NtkCheckFanouts(p, iNode) ) if ( Sfm_NtkCheckFanouts(p, iNode) )
{ {
Sfm_ObjForEachFanout( p, iNode, iTemp, i ) Sfm_ObjForEachFanout( p, iNode, iTemp, i )
...@@ -271,8 +266,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) ...@@ -271,8 +266,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
Vec_IntAppend( p->vDivs, p->vNodes ); Vec_IntAppend( p->vDivs, p->vNodes );
Sfm_NtkIncrementTravId2( p ); Sfm_NtkIncrementTravId2( p );
Vec_IntForEachEntry( p->vDivs, iTemp, i ) Vec_IntForEachEntry( p->vDivs, iTemp, i )
if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax ) if ( iTemp != iNode && Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
Sfm_NtkAddDivisors( p, iTemp ); Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) );
p->nTotalDivs += Vec_IntSize(p->vDivs); p->nTotalDivs += Vec_IntSize(p->vDivs);
p->timeDiv += clock() - clk; p->timeDiv += clock() - clk;
if ( !fVerbose ) if ( !fVerbose )
......
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