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

Adding timeout to AIG rewriting inside 'int'.

This commit is contained in:
Alan Mishchenko 2013-07-07 22:37:29 -07:00
parent 76875cd18d
commit 07d3351c31
6 changed files with 51 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/aig/aig.h
View File

@ -160,6 +160,7 @@ struct Aig_Man_t_
Vec_Int_t * vProbs; // probability of node being 1
Vec_Int_t * vCiNumsOrig; // original CI names
int nComplEdges; // complemented edges
abctime Time2Quit;
// timing statistics
abctime time1;
abctime time2;

17
src/opt/dar/darBalance.c
View File

@ -521,6 +521,8 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
{
pObjNew = Dar_Balance_rec( pNew, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
if ( pObjNew == NULL )
return NULL;
vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement((Aig_Obj_t *)vSuper->pArray[i]) );
}
// build the supergate
@ -529,6 +531,8 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
#else
pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
#endif
if ( pNew->Time2Quit && !(Aig_Regular(pObjNew)->Id & 255) && Abc_Clock() > pNew->Time2Quit )
return NULL;
// make sure the balanced node is not assigned
// assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
assert( pObjOld->pData == NULL );
@ -559,6 +563,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nAsserts = p->nAsserts;
pNew->nConstrs = p->nConstrs;
pNew->Time2Quit = p->Time2Quit;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// map the PI nodes
@ -588,6 +593,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
// perform balancing
pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
if ( pObjNew == NULL )
{
Vec_VecFree( vStore );
Aig_ManStop( pNew );
return NULL;
}
pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
// save arrival time of the output
arrTime = (float)Aig_Regular(pObjNew)->Level;
@ -613,6 +624,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
{
pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
if ( pObjNew == NULL )
{
Vec_VecFree( vStore );
Aig_ManStop( pNew );
return NULL;
}
pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
}

2
src/opt/dar/darCore.c
View File

@ -112,6 +112,8 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
// Aig_ManOrderStart( pAig );
// Aig_ManForEachNodeInOrder( pAig, pObj )
{
if ( pAig->Time2Quit && !(i & 256) && Abc_Clock() > pAig->Time2Quit )
break;
// Bar_ProgressUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL );
// Bar_ProgressUpdate( pProgress, i, NULL );
if ( !Aig_ObjIsNode(pObj) )

2
src/opt/dar/darRefact.c
View File

@ -526,6 +526,8 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
continue;
if ( i > nNodesOld )
break;
if ( pAig->Time2Quit && !(i & 256) && Abc_Clock() > pAig->Time2Quit )
break;
Vec_VecClear( p->vCuts );
//printf( "\nConsidering node %d.\n", pObj->Id );

18
src/opt/dar/darScript.c
View File

@ -72,6 +72,7 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
//alias rwsat "st; rw -l; b -l; rw -l; rf -l"
{
Aig_Man_t * pTemp;
abctime Time = pAig->Time2Quit;
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
@ -92,41 +93,56 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
// balance
if ( fBalance )
{
pAig->Time2Quit = Time;
pAig = Dar_ManBalance( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
if ( Time && Abc_Clock() > Time )
{ if ( pAig ) Aig_ManStop( pAig ); return NULL; }
}
//Aig_ManDumpBlif( pAig, "inter.blif", NULL, NULL );
//printf( "3" );
// rewrite
pAig->Time2Quit = Time;
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
if ( Time && Abc_Clock() > Time )
{ if ( pAig ) Aig_ManStop( pAig ); return NULL; }
//printf( "4" );
// refactor
pAig->Time2Quit = Time;
Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
if ( Time && Abc_Clock() > Time )
{ if ( pAig ) Aig_ManStop( pAig ); return NULL; }
//printf( "5" );
// balance
if ( fBalance )
{
pAig->Time2Quit = Time;
pAig = Dar_ManBalance( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
if ( Time && Abc_Clock() > Time )
{ if ( pAig ) Aig_ManStop( pAig ); return NULL; }
}
//printf( "6" );
// rewrite
pAig->Time2Quit = Time;
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
if ( Time && Abc_Clock() > Time )
{ if ( pAig ) Aig_ManStop( pAig ); return NULL; }
//printf( "7" );
return pAig;

12
src/proof/int/intCore.c
View File

@ -280,10 +280,22 @@ p->timeEqu += Abc_Clock() - clk;
clk = Abc_Clock();
if ( p->pInterNew )
{
Abc_PrintTime( 1, "Before time", clock() - clkTotal );
// save the timeout value
p->pInterNew->Time2Quit = nTimeNewOut;
// Ioa_WriteAiger( p->pInterNew, "interpol.aig", 0, 0 );
p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
// p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 0, 0 );
Abc_PrintTime( 1, "After time", clock() - clkTotal );
Aig_ManStop( pAigTemp );
if ( p->pInterNew == NULL )
{
printf( "Reached timeout (%d seconds) during rewriting.\n", pPars->nSecLimit );
p->timeTotal = Abc_Clock() - clkTotal;
Inter_ManStop( p, 1 );
Inter_CheckStop( pCheck );
return -1;
}
}
p->timeRwr += Abc_Clock() - clk;