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

Cumulative update to BDD-based reachability, speeding up &reachm and other changes.

This commit is contained in:
Alan Mishchenko 2011-02-28 14:52:51 -08:00
parent 39839c3feb
commit 6119f7068a
4 changed files with 279 additions and 126 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

228
src/aig/llb/llb3Image.c
View File

@ -50,7 +50,6 @@ struct Llb_Mgr_t_
Vec_Ptr_t * vLeaves; // leaves in the AIG manager
Vec_Ptr_t * vRoots; // roots in the AIG manager
DdManager * dd; // working BDD manager
DdNode * bCurrent; // current state functions in terms of vLeaves
int * pVars2Q; // variables to quantify
// internal
Llb_Prt_t ** pParts; // partitions
@ -613,6 +612,38 @@ void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar )
Vec_IntPush( p->pParts[iPart]->vVars, iVar );
}
/**Function*************************************************************
Synopsis [Starts non-linear quantification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinAddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc )
{
int k, nSuppSize;
assert( !Cudd_IsConstant(bFunc) );
// create partition
p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 );
p->pParts[i]->iPart = i;
p->pParts[i]->bFunc = bFunc;
p->pParts[i]->vVars = Vec_IntAlloc( 8 );
// add support dependencies
nSuppSize = 0;
Extra_SupportArray( p->dd, bFunc, p->pSupp );
for ( k = 0; k < p->nVars; k++ )
{
nSuppSize += p->pSupp[k];
if ( p->pSupp[k] && p->pVars2Q[k] )
Llb_NonlinAddPair( p, bFunc, i, k );
}
p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize );
}
/**Function*************************************************************
Synopsis [Starts non-linear quantification scheduling.]
@ -627,39 +658,16 @@ void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar )
int Llb_NonlinStart( Llb_Mgr_t * p, int TimeOut )
{
Vec_Ptr_t * vRootBdds;
Llb_Prt_t * pPart;
DdNode * bFunc;
int i, k, nSuppSize;
int i;
// create and collect BDDs
vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd, TimeOut ); // come referenced
if ( vRootBdds == NULL )
return 0;
Vec_PtrPush( vRootBdds, p->bCurrent );
// add pairs (refs are consumed inside)
Vec_PtrForEachEntry( DdNode *, vRootBdds, bFunc, i )
{
assert( !Cudd_IsConstant(bFunc) );
// create partition
p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 );
p->pParts[i]->iPart = i;
p->pParts[i]->bFunc = bFunc;
p->pParts[i]->vVars = Vec_IntAlloc( 8 );
// add support dependencies
nSuppSize = 0;
Extra_SupportArray( p->dd, bFunc, p->pSupp );
for ( k = 0; k < p->nVars; k++ )
{
nSuppSize += p->pSupp[k];
if ( p->pSupp[k] && p->pVars2Q[k] )
Llb_NonlinAddPair( p, bFunc, i, k );
}
p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize );
}
Llb_NonlinAddPartition( p, i, bFunc );
Vec_PtrFree( vRootBdds );
// remove singles
Llb_MgrForEachPart( p, pPart, i )
if ( Llb_NonlinHasSingletonVars(p, pPart) )
Llb_NonlinQuantify1( p, pPart, 0 );
return 1;
}
@ -672,8 +680,7 @@ int Llb_NonlinStart( Llb_Mgr_t * p, int TimeOut )
SideEffects []
SeeAlso []
***********************************************************************/
**********************************************************************/
void Llb_NonlinCheckVars( Llb_Mgr_t * p )
{
Llb_Var_t * pVar;
@ -736,7 +743,7 @@ int Llb_NonlinNextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t **
SeeAlso []
***********************************************************************/
void Llb_NonlinReorder( DdManager * dd, int fVerbose )
void Llb_NonlinReorder( DdManager * dd, int fTwice, int fVerbose )
{
int clk = clock();
if ( fVerbose )
@ -744,9 +751,12 @@ void Llb_NonlinReorder( DdManager * dd, int fVerbose )
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
if ( fTwice )
{
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
}
if ( fVerbose )
Abc_PrintTime( 1, "Time", clock() - clk );
}
@ -815,7 +825,7 @@ void Llb_NonlinVerifyScores( Llb_Mgr_t * p )
SeeAlso []
***********************************************************************/
Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, DdManager * dd, DdNode * bCurrent )
Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, DdManager * dd )
{
Llb_Mgr_t * p;
p = ABC_CALLOC( Llb_Mgr_t, 1 );
@ -823,12 +833,11 @@ Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t *
p->vLeaves = vLeaves;
p->vRoots = vRoots;
p->dd = dd;
p->bCurrent = bCurrent;
p->pVars2Q = pVars2Q;
p->nVars = Cudd_ReadSize(dd);
p->iPartFree = Vec_PtrSize(vRoots) + 1;
p->iPartFree = Vec_PtrSize(vRoots);
p->pVars = ABC_CALLOC( Llb_Var_t *, p->nVars );
p->pParts = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree );
p->pParts = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree + 2 );
p->pSupp = ABC_ALLOC( int, Cudd_ReadSize(dd) );
return p;
}
@ -880,17 +889,24 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo
int clk = clock(), clk2;
// start the manager
clk2 = clock();
p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd, bCurrent );
p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd );
if ( !Llb_NonlinStart( p, TimeOut ) )
{
Llb_NonlinFree( p );
return NULL;
}
// add partition
Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent );
// remove singles
Llb_MgrForEachPart( p, pPart, i )
if ( Llb_NonlinHasSingletonVars(p, pPart) )
Llb_NonlinQuantify1( p, pPart, 0 );
timeBuild += clock() - clk2;
timeInside = clock() - clk2;
// compute scores
Llb_NonlinRecomputeScores( p );
// save permutation
if ( pOrder )
memcpy( pOrder, dd->invperm, sizeof(int) * dd->size );
// iteratively quantify variables
while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
@ -907,6 +923,111 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo
if ( nReorders < Cudd_ReadReorderings(dd) )
Llb_NonlinRecomputeScores( p );
// else
// Llb_NonlinVerifyScores( p );
}
// load partitions
bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc );
Llb_MgrForEachPart( p, pPart, i )
{
bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( p->dd, bTemp );
}
nSuppMax = p->nSuppMax;
Llb_NonlinFree( p );
// reorder variables
if ( fReorder )
Llb_NonlinReorder( dd, 0, fVerbose );
timeOther += clock() - clk - timeInside;
// return
Cudd_Deref( bFunc );
return bFunc;
}
static Llb_Mgr_t * p = NULL;
/**Function*************************************************************
Synopsis [Starts image computation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst )
{
DdManager * dd;
int clk = clock();
assert( p == NULL );
// start a new manager (disable reordering)
dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_ShuffleHeap( dd, pOrder );
// if ( fFirst )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
// start the manager
p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd );
if ( !Llb_NonlinStart( p, 0 ) )
{
Llb_NonlinFree( p );
return NULL;
}
timeBuild += clock() - clk;
// if ( !fFirst )
// Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
return dd;
}
/**Function*************************************************************
Synopsis [Performs image computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder )
{
Llb_Prt_t * pPart, * pPart1, * pPart2;
DdNode * bFunc, * bTemp;
int i, nReorders, timeInside = 0;
int clk = clock(), clk2;
// add partition
Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent );
// remove singles
Llb_MgrForEachPart( p, pPart, i )
if ( Llb_NonlinHasSingletonVars(p, pPart) )
Llb_NonlinQuantify1( p, pPart, 0 );
// reorder
if ( fReorder )
Llb_NonlinReorder( p->dd, 0, 0 );
// save permutation
memcpy( pOrder, p->dd->invperm, sizeof(int) * p->dd->size );
// compute scores
Llb_NonlinRecomputeScores( p );
// iteratively quantify variables
while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
{
clk2 = clock();
nReorders = Cudd_ReadReorderings(p->dd);
if ( !Llb_NonlinQuantify2( p, pPart1, pPart2, 0, 0 ) )
{
Llb_NonlinFree( p );
return NULL;
}
timeAndEx += clock() - clk2;
timeInside += clock() - clk2;
if ( nReorders < Cudd_ReadReorderings(p->dd) )
Llb_NonlinRecomputeScores( p );
// else
// Llb_NonlinVerifyScores( p );
}
// load partitions
@ -924,16 +1045,43 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo
Cudd_RecursiveDeref( p->dd, bTemp );
}
nSuppMax = p->nSuppMax;
Llb_NonlinFree( p );
// reorder variables
if ( fReorder )
Llb_NonlinReorder( dd, fVerbose );
// if ( fReorder )
// Llb_NonlinReorder( p->dd, 0, fVerbose );
// save permutation
// memcpy( pOrder, p->dd->invperm, sizeof(int) * Cudd_ReadSize(p->dd) );
timeOther += clock() - clk - timeInside;
// return
Cudd_Deref( bFunc );
return bFunc;
}
/**Function*************************************************************
Synopsis [Quits image computation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinImageQuit()
{
DdManager * dd;
if ( p == NULL )
return;
dd = p->dd;
Llb_NonlinFree( p );
if ( dd->bFunc )
Cudd_RecursiveDeref( dd, dd->bFunc );
Extra_StopManager( dd );
// Cudd_Quit ( dd );
p = NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

167
src/aig/llb/llb3Nonlin.c
View File

@ -42,13 +42,18 @@ struct Llb_Mnn_t_
Vec_Ptr_t * vLeaves;
Vec_Ptr_t * vRoots;
int * pVars2Q;
int * pOrder;
int * pOrderL;
int * pOrderL2;
int * pOrderG;
Vec_Int_t * vCs2Glo; // cur state variables into global variables
Vec_Int_t * vNs2Glo; // next state variables into global variables
Vec_Int_t * vGlo2Cs; // global variables into cur state variables
Vec_Int_t * vGlo2Ns; // global variables into next state variables
int ddLocReos;
int ddLocGrbs;
int timeImage;
int timeTran1;
int timeTran2;
@ -297,7 +302,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
//Extra_bddPrintSupport( p->dd, bRing ); printf( "\n" );
// compute the next states
bImage = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bState,
p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY, ABC_INFINITY ); // consumed reference
p->pPars->fReorder, p->pPars->fVeryVerbose, NULL, ABC_INFINITY, ABC_INFINITY ); // consumed reference
assert( bImage != NULL );
Cudd_Ref( bImage );
//Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
@ -382,6 +387,33 @@ int Llb_NonlinReoHook( DdManager * dd, char * Type, void * Method )
return 1;
}
/**Function*************************************************************
Synopsis [Perform reachability with hints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinCompPerms( DdManager * dd, int * pVar2Lev )
{
DdSubtable * pSubt;
int i, Sum = 0, Entry;
for ( i = 0; i < dd->size; i++ )
{
pSubt = &(dd->subtables[dd->perm[i]]);
if ( pSubt->keys == pSubt->dead + 1 )
continue;
Entry = ABC_MAX(dd->perm[i], pVar2Lev[i]) - ABC_MIN(dd->perm[i], pVar2Lev[i]);
Sum += Entry;
//printf( "%d-%d(%d) ", dd->perm[i], pV2L[i], Entry );
}
return Sum;
}
/**Function*************************************************************
Synopsis [Perform reachability with hints.]
@ -395,8 +427,8 @@ int Llb_NonlinReoHook( DdManager * dd, char * Type, void * Method )
***********************************************************************/
int Llb_NonlinReachability( Llb_Mnn_t * p )
{
DdNode * bCurrent, * bNext, * bTemp;
int iVar, nIters, nBddSize0, nBddSize, Limit = p->pPars->nBddMax;
DdNode * bTemp, * bNext;
int nIters, nBddSize0, nBddSize, NumCmp, Limit = p->pPars->nBddMax;
int clk2, clk3, clk = clock();
assert( Aig_ManRegNum(p->pAig) > 0 );
@ -425,7 +457,9 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
}
Cudd_Ref( p->ddR->bFunc );
// compute the starting set of states
bCurrent = Llb_NonlinComputeInitState( p->pAig, p->dd ); Cudd_Ref( bCurrent );
Cudd_Quit( p->dd );
p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 1 );
p->dd->bFunc = Llb_NonlinComputeInitState( p->pAig, p->dd ); Cudd_Ref( p->dd->bFunc ); // current
p->ddG->bFunc = Llb_NonlinComputeInitState( p->pAig, p->ddG ); Cudd_Ref( p->ddG->bFunc ); // reached
p->ddG->bFunc2 = Llb_NonlinComputeInitState( p->pAig, p->ddG ); Cudd_Ref( p->ddG->bFunc2 ); // frontier
for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
@ -437,18 +471,18 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
Llb_NonlinImageQuit();
return -1;
}
// save the onion ring
bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, Vec_IntArray(p->vCs2Glo) );
bTemp = Extra_TransferPermute( p->dd, p->ddR, p->dd->bFunc, Vec_IntArray(p->vCs2Glo) );
if ( bTemp == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during ring transfer.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
Llb_NonlinImageQuit();
return -1;
}
Cudd_Ref( bTemp );
@ -460,7 +494,6 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
assert( p->pInit->pSeqModel == NULL );
if ( !p->pPars->fBackward )
p->pInit->pSeqModel = Llb_NonlinDeriveCex( p );
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
if ( !p->pPars->fSilent )
{
if ( !p->pPars->fBackward )
@ -469,85 +502,32 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
Abc_PrintTime( 1, "Time", clock() - clk );
}
Llb_NonlinImageQuit();
return 0;
}
// check the size
if ( Cudd_DagSize(bCurrent) > p->pPars->nBddMax )
{
DdNode * bVar, * bVarG;
// find the best variable
iVar = Llb_NonlinFindBestVar( p->dd, bCurrent, p->pAig );
// get cofactor in the working manager
bVar = Cudd_bddIthVar( p->dd, Aig_ObjId(Saig_ManLo(p->pAig,iVar)) );
bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, Cudd_Not(bVar) ); Cudd_Ref( bCurrent );
Cudd_RecursiveDeref( p->dd, bTemp );
// get cofactor in the global manager
bVarG = Cudd_bddIthVar(p->ddG, iVar);
p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(bVarG) ); Cudd_Ref( p->ddG->bFunc2 );
Cudd_RecursiveDeref( p->ddG, bTemp );
}
// compute the next states
clk3 = clock();
nBddSize0 = Cudd_DagSize( bCurrent );
bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent,
// p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, nIters ? p->pPars->nBddMax : ABC_INFINITY );
p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY, p->pPars->TimeTarget );
// Abc_PrintTime( 1, "Image time", clock() - clk3 );
nBddSize0 = Cudd_DagSize( p->dd->bFunc );
bNext = Llb_NonlinImageCompute( p->dd->bFunc, p->pPars->fReorder, 0, 1, p->pOrderL ); // consumes ref
// bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent,
// p->pPars->fReorder, p->pPars->fVeryVerbose, NULL, ABC_INFINITY, p->pPars->TimeTarget );
if ( bNext == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during image computation in quantification.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
Llb_NonlinImageQuit();
return -1;
}
if ( bNext == NULL ) // Llb_NonlimImage() consumes reference of bCurrent!!!
{
DdNode * bVar, * bVarG;
// if ( !p->pPars->fSilent )
// printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit );
// p->pPars->iFrame = nIters - 1;
// return -1;
printf( "Should never happen!\n" );
// get the frontier in the working manager
bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); Cudd_Ref( bCurrent );
// find the best variable
iVar = Llb_NonlinFindBestVar( p->dd, bCurrent, p->pAig );
// get cofactor in the working manager
bVar = Cudd_bddIthVar( p->dd, Aig_ObjId(Saig_ManLo(p->pAig,iVar)) );
bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, Cudd_Not(bVar) ); Cudd_Ref( bCurrent );
Cudd_RecursiveDeref( p->dd, bTemp );
// get cofactor in the global manager
bVarG = Cudd_bddIthVar(p->dd, iVar);
p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(bVarG) ); Cudd_Ref( p->ddG->bFunc2 );
Cudd_RecursiveDeref( p->ddG, bTemp );
// Cudd_ReduceHeap( p->dd, CUDD_REORDER_SIFT, 1 );
p->pPars->nBddMax = ABC_INFINITY;
nIters--;
continue;
}
else
p->pPars->nBddMax = Limit;
Cudd_Ref( bNext );
nBddSize = Cudd_DagSize( bNext );
p->timeImage += clock() - clk3;
// transfer to the state manager
clk3 = clock();
Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
// p->ddG->bFunc2 = Extra_TransferPermuteTime( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo), p->pPars->TimeTarget );
p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) );
if ( p->ddG->bFunc2 == NULL )
{
@ -555,12 +535,24 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->dd, bNext );
Llb_NonlinImageQuit();
return -1;
}
Cudd_Ref( p->ddG->bFunc2 );
Cudd_RecursiveDeref( p->dd, bNext );
p->timeTran1 += clock() - clk3;
// save permutation
NumCmp = Llb_NonlinCompPerms( p->dd, p->pOrderL2 );
// save order before image computation
memcpy( p->pOrderL2, p->dd->perm, sizeof(int) * p->dd->size );
// update the image computation manager
p->timeReo += Cudd_ReadReorderingTime(p->dd);
p->ddLocReos += Cudd_ReadReorderings(p->dd);
p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd);
Llb_NonlinImageQuit();
p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 0 );
// derive new states
clk3 = clock();
p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) );
@ -570,6 +562,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->ddG, bTemp );
Llb_NonlinImageQuit();
return -1;
}
Cudd_Ref( p->ddG->bFunc2 );
@ -584,6 +577,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->ddG, bTemp );
Llb_NonlinImageQuit();
return -1;
}
Cudd_Ref( p->ddG->bFunc );
@ -593,20 +587,20 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
// reset permutation
// RetValue = Cudd_CheckZeroRef( dd );
// assert( RetValue == 0 );
// Cudd_ShuffleHeap( dd, pOrder );
// Cudd_ShuffleHeap( dd, pOrderG );
// move new states to the working manager
clk3 = clock();
// bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs), p->pPars->TimeTarget );
bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) );
if ( bCurrent == NULL )
p->dd->bFunc = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) );
if ( p->dd->bFunc == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Llb_NonlinImageQuit();
return -1;
}
Cudd_Ref( bCurrent );
Cudd_Ref( p->dd->bFunc );
p->timeTran2 += clock() - clk3;
// report the results
@ -615,11 +609,14 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
printf( "I =%3d : ", nIters );
printf( "Fr =%7d ", nBddSize0 );
printf( "Im =%7d ", nBddSize );
printf( "(%4d %4d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
printf( "(%4d %4d) ", p->ddLocReos, p->ddLocGrbs );
printf( "Rea =%6d ", Cudd_DagSize(p->ddG->bFunc) );
printf( "(%4d %4d) ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
printf( "S =%4d ", nSuppMax );
printf( "cL =%5d ", NumCmp );
printf( "cG =%5d ", Llb_NonlinCompPerms( p->ddG, p->pOrderG ) );
Abc_PrintTime( 1, "T", clock() - clk2 );
memcpy( p->pOrderG, p->ddG->perm, sizeof(int) * p->ddG->size );
}
/*
if ( pPars->fVerbose )
@ -630,18 +627,16 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
fflush( stdout );
}
*/
if ( nIters == p->pPars->nIterMax - 1 )
{
if ( !p->pPars->fSilent )
printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax );
p->pPars->iFrame = nIters;
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
Llb_NonlinImageQuit();
return -1;
}
// Llb_NonlinReorder( p->ddG, 1 );
// Llb_NonlinFindBestVar( p->ddG, bReached, NULL );
}
Llb_NonlinImageQuit();
// report the stats
if ( p->pPars->fVerbose )
@ -704,10 +699,14 @@ Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * p
Saig_ManForEachLi( pAig, pObj, i )
Vec_PtrPush( p->vRoots, pObj );
// variables to quantify
p->pOrder = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
p->pOrderL = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
p->pOrderL2= ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
p->pOrderG = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
p->pVars2Q = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
Aig_ManForEachPi( pAig, pObj, i )
p->pVars2Q[Aig_ObjId(pObj)] = 1;
for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
p->pOrderL[i] = p->pOrderL2[i] = p->pOrderG[i] = i;
Llb_NonlinPrepareVarMap( p );
return p;
}
@ -730,7 +729,6 @@ void Llb_MnnStop( Llb_Mnn_t * p )
if ( p->pPars->fVerbose )
{
p->timeOther = p->timeTotal - p->timeImage - p->timeTran1 - p->timeTran2 - p->timeGloba;
p->timeReo = Cudd_ReadReorderingTime(p->dd);
p->timeReoG = Cudd_ReadReorderingTime(p->ddG);
ABC_PRTP( "Image ", p->timeImage, p->timeTotal );
ABC_PRTP( " build ", timeBuild, p->timeTotal );
@ -744,7 +742,6 @@ void Llb_MnnStop( Llb_Mnn_t * p )
ABC_PRTP( " reo ", p->timeReo, p->timeTotal );
ABC_PRTP( " reoG ", p->timeReoG, p->timeTotal );
}
p->dd->bFunc = NULL;
if ( p->ddR->bFunc )
Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
@ -755,7 +752,7 @@ void Llb_MnnStop( Llb_Mnn_t * p )
if ( p->ddG->bFunc2 )
Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
// printf( "manager1\n" );
Extra_StopManager( p->dd );
// Extra_StopManager( p->dd );
// printf( "manager2\n" );
Extra_StopManager( p->ddG );
// printf( "manager3\n" );
@ -767,7 +764,9 @@ void Llb_MnnStop( Llb_Mnn_t * p )
Vec_PtrFree( p->vLeaves );
Vec_PtrFree( p->vRoots );
ABC_FREE( p->pVars2Q );
ABC_FREE( p->pOrder );
ABC_FREE( p->pOrderL );
ABC_FREE( p->pOrderL2 );
ABC_FREE( p->pOrderG );
ABC_FREE( p );
}

6
src/aig/llb/llbInt.h
View File

@ -172,9 +172,15 @@ extern DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMan
Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs,
int TimeTarget, int fBackward, int fReorder, int fVerbose );
extern DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst );
extern DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder );
extern void Llb_NonlinImageQuit();
/*=== llb3Image.c ======================================================*/
extern DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q,
DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeTarget );
/*=== llb3Nonlin.c ======================================================*/
extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd );
ABC_NAMESPACE_HEADER_END

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

@ -27937,7 +27937,7 @@ usage:
Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" );
Abc_Print( -2, "\t-r : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" );
Abc_Print( -2, "\t-b : perform backward reachability analysis [default = %s]\n", pPars->fBackward? "yes": "no" );
Abc_Print( -2, "\t-y : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );
Abc_Print( -2, "\t-z : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );
@ -28069,7 +28069,7 @@ usage:
Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" );
Abc_Print( -2, "\t-r : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" );
Abc_Print( -2, "\t-y : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );
Abc_Print( -2, "\t-z : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );
Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );