diff options
Diffstat (limited to 'src/proof/llb/llb3Nonlin.c')
| -rw-r--r-- | src/proof/llb/llb3Nonlin.c | 871 |
1 files changed, 871 insertions, 0 deletions
diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c new file mode 100644 index 00000000..45f6f11e --- /dev/null +++ b/src/proof/llb/llb3Nonlin.c @@ -0,0 +1,871 @@ +/**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; + + int timeImage; + int timeTran1; + int timeTran2; + int timeGloba; + int timeOther; + int timeTotal; + int timeReo; + int timeReoG; + +}; + +extern int 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; + int clk = 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", 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, 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, * 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, ABC_INFINITY, ABC_INFINITY ); // 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, NumCmp, Limit = p->pPars->nBddMax; + int clk2, clk3, clk = clock(); + assert( Aig_ManRegNum(p->pAig) > 0 ); + + // compute time to stop + p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 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 = clock(); + if ( p->pPars->TimeLimit && time(NULL) > 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 ) + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pInit->pSeqModel->iPo, nIters ); + else + printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); + Abc_PrintTime( 1, "Time", clock() - clk ); + } + p->pPars->iFrame = nIters - 1; + Llb_NonlinImageQuit(); + return 0; + } + + // compute the next states + clk3 = 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 += clock() - clk3; + + + // transfer to the state manager + clk3 = 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 += 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 = 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 += clock() - clk3; + + if ( Cudd_IsConstant(p->ddG->bFunc2) ) + break; + // add to the reached set + clk3 = 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 += clock() - clk3; + + // reset permutation +// RetValue = Cudd_CheckZeroRef( dd ); +// assert( RetValue == 0 ); +// Cudd_ShuffleHeap( dd, pOrderG ); + + // move new states to the working manager + clk3 = 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 += 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", 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", 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_ManPiNum(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_ManPiNum(pAig) ); + Aig_ManForEachPi( pAig, pObj, i ) + Vec_PtrPush( p->vLeaves, pObj ); + // create roots + p->vRoots = Vec_PtrAlloc( Aig_ManPoNum(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_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; +} + +/**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; + int clk = 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 = 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 ) + { + int clk = clock(); + pMnn = Llb_MnnStart( pAig, p, pPars ); + RetValue = Llb_NonlinReachability( pMnn ); + pMnn->timeTotal = clock() - clk; + Llb_MnnStop( pMnn ); + } + + Aig_ManStop( p ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |