/**CFile****************************************************************
FileName [llb2Nonlin.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Non-linear quantification scheduling.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb2Nonlin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Llb_Mnn_t_ Llb_Mnn_t;
struct Llb_Mnn_t_
{
Aig_Man_t * pInit; // AIG manager
Aig_Man_t * pAig; // AIG manager
Gia_ParLlb_t * pPars; // parameters
DdManager * dd; // BDD manager
DdManager * ddG; // BDD manager
DdManager * ddR; // BDD manager
Vec_Ptr_t * vRings; // onion rings in ddR
Vec_Ptr_t * vLeaves;
Vec_Ptr_t * vRoots;
int * pVars2Q;
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;
abctime timeImage;
abctime timeTran1;
abctime timeTran2;
abctime timeGloba;
abctime timeOther;
abctime timeTotal;
abctime timeReo;
abctime timeReoG;
};
extern abctime timeBuild, timeAndEx, timeOther;
extern int nSuppMax;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Finds variable whose 0-cofactor is the smallest.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinFindBestVar( DdManager * dd, DdNode * bFunc, Aig_Man_t * pAig )
{
int fVerbose = 0;
Aig_Obj_t * pObj;
DdNode * bCof, * bVar;
int i, iVar, iVarBest = -1, iValue, iValueBest = ABC_INFINITY, Size0Best = -1;
int Size, Size0, Size1;
abctime clk = Abc_Clock();
Size = Cudd_DagSize(bFunc);
// printf( "Original = %6d. SuppSize = %3d. Vars = %3d.\n",
// Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Aig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
{
iVar = Aig_ObjId(pObj);
if ( fVerbose )
printf( "Var =%3d : ", iVar );
bVar = Cudd_bddIthVar(dd, iVar);
bCof = Cudd_bddAnd( dd, bFunc, Cudd_Not(bVar) ); Cudd_Ref( bCof );
Size0 = Cudd_DagSize(bCof);
if ( fVerbose )
printf( "Supp0 =%3d ", Cudd_SupportSize(dd, bCof) );
if ( fVerbose )
printf( "Size0 =%6d ", Size0 );
Cudd_RecursiveDeref( dd, bCof );
bCof = Cudd_bddAnd( dd, bFunc, bVar ); Cudd_Ref( bCof );
Size1 = Cudd_DagSize(bCof);
if ( fVerbose )
printf( "Supp1 =%3d ", Cudd_SupportSize(dd, bCof) );
if ( fVerbose )
printf( "Size1 =%6d ", Size1 );
Cudd_RecursiveDeref( dd, bCof );
iValue = Abc_MaxInt(Size0, Size1) - Abc_MinInt(Size0, Size1) + Size0 + Size1 - Size;
if ( fVerbose )
printf( "D =%6d ", Size0 + Size1 - Size );
if ( fVerbose )
printf( "B =%6d ", Abc_MaxInt(Size0, Size1) - Abc_MinInt(Size0, Size1) );
if ( fVerbose )
printf( "S =%6d\n", iValue );
if ( Size0 > 1 && Size1 > 1 && iValueBest > iValue )
{
iValueBest = iValue;
iVarBest = i;
Size0Best = Size0;
}
}
printf( "BestVar = %4d/%4d. Value =%6d. Orig =%6d. Size0 =%6d. ",
iVarBest, Aig_ObjId(Saig_ManLo(pAig,iVarBest)), iValueBest, Size, Size0Best );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return iVarBest;
}
/**Function*************************************************************
Synopsis [Finds variable whose 0-cofactor is the smallest.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinTrySubsetting( DdManager * dd, DdNode * bFunc )
{
DdNode * bNew;
printf( "Original = %6d. SuppSize = %3d. ",
Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc) );
bNew = Cudd_SubsetHeavyBranch( dd, bFunc, Cudd_SupportSize(dd, bFunc), 1000 ); Cudd_Ref( bNew );
printf( "Result = %6d. SuppSize = %3d.\n",
Cudd_DagSize(bNew), Cudd_SupportSize(dd, bNew) );
Cudd_RecursiveDeref( dd, bNew );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinPrepareVarMap( Llb_Mnn_t * p )
{
Aig_Obj_t * pObjLi, * pObjLo, * pObj;
int i, iVarLi, iVarLo;
p->vCs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
p->vNs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
{
iVarLi = Aig_ObjId(pObjLi);
iVarLo = Aig_ObjId(pObjLo);
assert( iVarLi >= 0 && iVarLi < Aig_ManObjNumMax(p->pAig) );
assert( iVarLo >= 0 && iVarLo < Aig_ManObjNumMax(p->pAig) );
Vec_IntWriteEntry( p->vCs2Glo, iVarLo, i );
Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i );
Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo );
Vec_IntWriteEntry( p->vGlo2Ns, i, iVarLi );
}
// add mapping of the PIs
Saig_ManForEachPi( p->pAig, pObj, i )
{
Vec_IntWriteEntry( p->vCs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
Vec_IntWriteEntry( p->vNs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
{
Aig_Obj_t * pObj;
DdNode * bRes, * bVar, * bTemp;
int i, iVar;
abctime TimeStop;
TimeStop = dd->TimeStop; dd->TimeStop = 0;
bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
Saig_ManForEachLo( pAig, pObj, i )
{
iVar = (Cudd_ReadSize(dd) == Aig_ManRegNum(pAig)) ? i : Aig_ObjId(pObj);
bVar = Cudd_bddIthVar( dd, iVar );
bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_Deref( bRes );
dd->TimeStop = TimeStop;
return bRes;
}
/**Function*************************************************************
Synopsis [Derives counter-example by backward reachability.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
{
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
Vec_Int_t * vVarsNs;
DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
int i, v, RetValue, nPiOffset;
char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
assert( Vec_PtrSize(p->vRings) > 0 );
p->dd->TimeStop = 0;
p->ddR->TimeStop = 0;
// update quantifiable vars
memset( p->pVars2Q, 0, sizeof(int) * Cudd_ReadSize(p->dd) );
vVarsNs = Vec_IntAlloc( Aig_ManRegNum(p->pAig) );
Saig_ManForEachLi( p->pAig, pObj, i )
{
p->pVars2Q[Aig_ObjId(pObj)] = 1;
Vec_IntPush( vVarsNs, Aig_ObjId(pObj) );
}
/*
Saig_ManForEachLo( p->pAig, pObj, i )
printf( "%d ", pObj->Id );
printf( "\n" );
Saig_ManForEachLi( p->pAig, pObj, i )
printf( "%d(%d) ", pObj->Id, Aig_ObjFaninId0(pObj) );
printf( "\n" );
*/
// allocate room for the counter-example
pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
pCex->iPo = -1;
// get the last cube
bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube );
RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
Cudd_RecursiveDeref( p->ddR, bOneCube );
assert( RetValue );
// write PIs of counter-example
nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
Saig_ManForEachPi( p->pAig, pObj, i )
if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
Abc_InfoSetBit( pCex->pData, nPiOffset + i );
// write state in terms of NS variables
if ( Vec_PtrSize(p->vRings) > 1 )
{
bState = Llb_CoreComputeCube( p->dd, vVarsNs, 1, pValues ); Cudd_Ref( bState );
}
// perform backward analysis
Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
{
if ( v == Vec_PtrSize(p->vRings) - 1 )
continue;
//Extra_bddPrintSupport( p->dd, bState ); printf( "\n" );
//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, NULL ); // consumed reference
assert( bImage != NULL );
Cudd_Ref( bImage );
//Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
// move reached states into ring manager
bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bImage );
Cudd_RecursiveDeref( p->dd, bTemp );
// intersect with the previous set
bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing ); Cudd_Ref( bOneCube );
Cudd_RecursiveDeref( p->ddR, bImage );
// find any assignment of the BDD
RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
Cudd_RecursiveDeref( p->ddR, bOneCube );
assert( RetValue );
// write PIs of counter-example
nPiOffset -= Saig_ManPiNum(p->pAig);
Saig_ManForEachPi( p->pAig, pObj, i )
if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
Abc_InfoSetBit( pCex->pData, nPiOffset + i );
// check that we get the init state
if ( v == 0 )
{
Saig_ManForEachLo( p->pAig, pObj, i )
assert( pValues[i] == 0 );
break;
}
// write state in terms of NS variables
bState = Llb_CoreComputeCube( p->dd, vVarsNs, 1, pValues ); Cudd_Ref( bState );
}
assert( nPiOffset == Saig_ManRegNum(p->pAig) );
// update the output number
//Abc_CexPrint( pCex );
RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex );
assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
pCex->iPo = RetValue;
// cleanup
ABC_FREE( pValues );
Vec_IntFree( vVarsNs );
return pCex;
}
/**Function*************************************************************
Synopsis [Perform reachability with hints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinReoHook( DdManager * dd, char * Type, void * Method )
{
Aig_Man_t * pAig = (Aig_Man_t *)dd->bFunc;
Aig_Obj_t * pObj;
int i;
printf( "Order: " );
for ( i = 0; i < Cudd_ReadSize(dd); i++ )
{
pObj = Aig_ManObj( pAig, i );
if ( pObj == NULL )
continue;
if ( Saig_ObjIsPi(pAig, pObj) )
printf( "pi" );
else if ( Saig_ObjIsLo(pAig, pObj) )
printf( "lo" );
else if ( Saig_ObjIsPo(pAig, pObj) )
printf( "po" );
else if ( Saig_ObjIsLi(pAig, pObj) )
printf( "li" );
else continue;
printf( "%d=%d ", i, dd->perm[i] );
}
printf( "\n" );
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_MaxInt(dd->perm[i], pVar2Lev[i]) - Abc_MinInt(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.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinReachability( Llb_Mnn_t * p )
{
DdNode * bTemp, * bNext;
int nIters, nBddSize0, nBddSize = -1, NumCmp;//, Limit = p->pPars->nBddMax;
abctime clk2, clk3, clk = Abc_Clock();
assert( Aig_ManRegNum(p->pAig) > 0 );
// compute time to stop
p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
// set the stop time parameter
p->dd->TimeStop = p->pPars->TimeTarget;
p->ddG->TimeStop = p->pPars->TimeTarget;
p->ddR->TimeStop = p->pPars->TimeTarget;
// set reordering hooks
assert( p->dd->bFunc == NULL );
// p->dd->bFunc = (DdNode *)p->pAig;
// Cudd_AddHook( p->dd, Llb_NonlinReoHook, CUDD_POST_REORDERING_HOOK );
// create bad state in the ring manager
p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );
if ( p->ddR->bFunc == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
p->pPars->iFrame = -1;
return -1;
}
Cudd_Ref( p->ddR->bFunc );
// compute the starting set of states
Cudd_Quit( p->dd );
p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 1, p->pPars->TimeTarget );
if ( p->dd == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
p->pPars->iFrame = -1;
return -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++ )
{
// check the runtime limit
clk2 = Abc_Clock();
if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Llb_NonlinImageQuit();
return -1;
}
// save the onion ring
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;
Llb_NonlinImageQuit();
return -1;
}
Cudd_Ref( bTemp );
Vec_PtrPush( p->vRings, bTemp );
// check it for bad states
if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) )
{
assert( p->pInit->pSeqModel == NULL );
if ( !p->pPars->fBackward )
p->pInit->pSeqModel = Llb_NonlinDeriveCex( p );
if ( !p->pPars->fSilent )
{
if ( !p->pPars->fBackward )
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, nIters );
else
Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
p->pPars->iFrame = nIters - 1;
Llb_NonlinImageQuit();
return 0;
}
// compute the next states
clk3 = Abc_Clock();
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;
Llb_NonlinImageQuit();
return -1;
}
Cudd_Ref( bNext );
nBddSize = Cudd_DagSize( bNext );
p->timeImage += Abc_Clock() - clk3;
// transfer to the state manager
clk3 = Abc_Clock();
Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) );
// p->ddG->bFunc2 = Extra_bddAndPermute( p->ddG, Cudd_Not(p->ddG->bFunc), p->dd, bNext, Vec_IntArray(p->vNs2Glo) );
if ( p->ddG->bFunc2 == NULL )
{
if ( !p->pPars->fSilent )
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 += Abc_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, p->pPars->TimeTarget );
if ( p->dd == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
return -1;
}
//Extra_TestAndPerm( p->ddG, Cudd_Not(p->ddG->bFunc), p->ddG->bFunc2 );
// derive new states
clk3 = Abc_Clock();
p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) );
if ( p->ddG->bFunc2 == NULL )
{
if ( !p->pPars->fSilent )
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 );
Cudd_RecursiveDeref( p->ddG, bTemp );
p->timeGloba += Abc_Clock() - clk3;
if ( Cudd_IsConstant(p->ddG->bFunc2) )
break;
// add to the reached set
clk3 = Abc_Clock();
p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 );
if ( p->ddG->bFunc == NULL )
{
if ( !p->pPars->fSilent )
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 );
Cudd_RecursiveDeref( p->ddG, bTemp );
p->timeGloba += Abc_Clock() - clk3;
// reset permutation
// RetValue = Cudd_CheckZeroRef( dd );
// assert( RetValue == 0 );
// Cudd_ShuffleHeap( dd, pOrderG );
// move new states to the working manager
clk3 = Abc_Clock();
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( p->dd->bFunc );
p->timeTran2 += Abc_Clock() - clk3;
// report the results
if ( p->pPars->fVerbose )
{
printf( "I =%3d : ", nIters );
printf( "Fr =%7d ", nBddSize0 );
printf( "Im =%7d ", nBddSize );
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", Abc_Clock() - clk2 );
memcpy( p->pOrderG, p->ddG->perm, sizeof(int) * p->ddG->size );
}
/*
if ( pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(ddG, bReached, Saig_ManRegNum(pAig) );
// Extra_bddPrint( ddG, bReached );printf( "\n" );
printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(pAig)) );
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;
Llb_NonlinImageQuit();
return -1;
}
}
Llb_NonlinImageQuit();
// report the stats
if ( p->pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(p->ddG, p->ddG->bFunc, Saig_ManRegNum(p->pAig) );
if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
printf( "Reachability analysis is stopped after %d frames.\n", nIters );
else
printf( "Reachability analysis completed after %d frames.\n", nIters );
printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
fflush( stdout );
}
if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
{
if ( !p->pPars->fSilent )
printf( "Verified only for states reachable in %d frames. ", nIters );
p->pPars->iFrame = p->pPars->nIterMax;
return -1; // undecided
}
// report
if ( !p->pPars->fSilent )
printf( "The miter is proved unreachable after %d iterations. ", nIters );
p->pPars->iFrame = nIters - 1;
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return 1; // unreachable
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
Llb_Mnn_t * p;
Aig_Obj_t * pObj;
int i;
p = ABC_CALLOC( Llb_Mnn_t, 1 );
p->pInit = pInit;
p->pAig = pAig;
p->pPars = pPars;
p->dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
p->ddG = Cudd_Init( Aig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
p->ddR = Cudd_Init( Aig_ManCiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
p->vRings = Vec_PtrAlloc( 100 );
// create leaves
p->vLeaves = Vec_PtrAlloc( Aig_ManCiNum(pAig) );
Aig_ManForEachCi( pAig, pObj, i )
Vec_PtrPush( p->vLeaves, pObj );
// create roots
p->vRoots = Vec_PtrAlloc( Aig_ManCoNum(pAig) );
Saig_ManForEachLi( pAig, pObj, i )
Vec_PtrPush( p->vRoots, pObj );
// variables to quantify
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_ManForEachCi( 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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_MnnStop( Llb_Mnn_t * p )
{
DdNode * bTemp;
int i;
if ( p->pPars->fVerbose )
{
p->timeOther = p->timeTotal - p->timeImage - p->timeTran1 - p->timeTran2 - p->timeGloba;
p->timeReoG = Cudd_ReadReorderingTime(p->ddG);
ABC_PRTP( "Image ", p->timeImage, p->timeTotal );
ABC_PRTP( " build ", timeBuild, p->timeTotal );
ABC_PRTP( " and-ex ", timeAndEx, p->timeTotal );
ABC_PRTP( " other ", timeOther, p->timeTotal );
ABC_PRTP( "Transfer1", p->timeTran1, p->timeTotal );
ABC_PRTP( "Transfer2", p->timeTran2, p->timeTotal );
ABC_PRTP( "Global ", p->timeGloba, p->timeTotal );
ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
ABC_PRTP( " reo ", p->timeReo, p->timeTotal );
ABC_PRTP( " reoG ", p->timeReoG, p->timeTotal );
}
if ( p->ddR->bFunc )
Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
Cudd_RecursiveDeref( p->ddR, bTemp );
Vec_PtrFree( p->vRings );
if ( p->ddG->bFunc )
Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc );
if ( p->ddG->bFunc2 )
Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
// printf( "manager1\n" );
// Extra_StopManager( p->dd );
// printf( "manager2\n" );
Extra_StopManager( p->ddG );
// printf( "manager3\n" );
Extra_StopManager( p->ddR );
Vec_IntFreeP( &p->vCs2Glo );
Vec_IntFreeP( &p->vNs2Glo );
Vec_IntFreeP( &p->vGlo2Cs );
Vec_IntFreeP( &p->vGlo2Ns );
Vec_PtrFree( p->vLeaves );
Vec_PtrFree( p->vRoots );
ABC_FREE( p->pVars2Q );
ABC_FREE( p->pOrderL );
ABC_FREE( p->pOrderL2 );
ABC_FREE( p->pOrderG );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Finds balanced cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num )
{
Llb_Mnn_t * pMnn;
Gia_ParLlb_t Pars, * pPars = &Pars;
Aig_Man_t * p;
abctime clk = Abc_Clock();
Llb_ManSetDefaultParams( pPars );
pPars->fVerbose = 1;
p = Aig_ManDupFlopsOnly( pAig );
//Aig_ManShow( p, 0, NULL );
Aig_ManPrintStats( pAig );
Aig_ManPrintStats( p );
pMnn = Llb_MnnStart( pAig, p, pPars );
Llb_NonlinReachability( pMnn );
pMnn->timeTotal = Abc_Clock() - clk;
Llb_MnnStop( pMnn );
Aig_ManStop( p );
}
/**Function*************************************************************
Synopsis [Finds balanced cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
Llb_Mnn_t * pMnn;
Aig_Man_t * p;
int RetValue = -1;
p = Aig_ManDupFlopsOnly( pAig );
//Aig_ManShow( p, 0, NULL );
if ( pPars->fVerbose )
Aig_ManPrintStats( pAig );
if ( pPars->fVerbose )
Aig_ManPrintStats( p );
if ( !pPars->fSkipReach )
{
abctime clk = Abc_Clock();
pMnn = Llb_MnnStart( pAig, p, pPars );
RetValue = Llb_NonlinReachability( pMnn );
pMnn->timeTotal = Abc_Clock() - clk;
Llb_MnnStop( pMnn );
}
Aig_ManStop( p );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END