diff options
Diffstat (limited to 'src/aig/llb/llb4Nonlin.c')
| -rw-r--r-- | src/aig/llb/llb4Nonlin.c | 914 |
1 files changed, 914 insertions, 0 deletions
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c new file mode 100644 index 00000000..1a6f538c --- /dev/null +++ b/src/aig/llb/llb4Nonlin.c @@ -0,0 +1,914 @@ +/**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_Mnx_t_ Llb_Mnx_t; +struct Llb_Mnx_t_ +{ + // user info + Aig_Man_t * pAig; // AIG manager + Gia_ParLlb_t * pPars; // parameters + + // intermediate BDDs + DdManager * dd; // BDD manager + DdNode * bBad; // bad states in terms of CIs + DdNode * bReached; // reached states + DdNode * bCurrent; // from states + DdNode * bNext; // to states + Vec_Ptr_t * vRings; // onion rings in ddR + Vec_Ptr_t * vRoots; // BDDs for partitions + + // structural info + Vec_Int_t * vOrder; // for each object ID, its BDD variable number or -1 + Vec_Int_t * vVars2Q; // 1 if variable is quantifiable; 0 othervise + + int timeImage; + int timeRemap; + int timeReo; + int timeOther; + int timeTotal; +}; + +static inline int Llb_MnxBddVar( Vec_Int_t * vOrder, Aig_Obj_t * pObj ) { return Vec_IntEntry(vOrder, Aig_ObjId(pObj)); } + +//extern int timeBuild, timeAndEx, timeOther; +//extern int nSuppMax; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes bad in working manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder ) +{ + Vec_Ptr_t * vNodes; + DdNode * bBdd, * bBdd0, * bBdd1, * bTemp, * bResult; + Aig_Obj_t * pObj; + int i; + Aig_ManCleanData( pAig ); + // assign elementary variables + Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) ); + // compute internal nodes + vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vPos), Saig_ManPoNum(pAig) ); + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + { + if ( !Aig_ObjIsNode(pObj) ) + continue; + bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); + bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); + if ( bBdd == NULL ) + { + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL ) + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); + Vec_PtrFree( vNodes ); + return NULL; + } + Cudd_Ref( bBdd ); + pObj->pData = bBdd; + } + // quantify PIs of each PO + bResult = Cudd_ReadLogicZero( dd ); Cudd_Ref( bResult ); + Saig_ManForEachPo( pAig, pObj, i ) + { + bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + bResult = Cudd_bddOr( dd, bTemp = bResult, bBdd0 ); + if ( bResult == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp ); + break; + } + Cudd_Ref( bResult ); + Cudd_RecursiveDeref( dd, bTemp ); + } + // deref + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL ) + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); + Vec_PtrFree( vNodes ); + if ( bResult ) + Cudd_Deref( bResult ); +//if ( bResult ) +//printf( "Bad state = %d.\n", Cudd_DagSize(bResult) ); + return bResult; +} + +/**Function************************************************************* + + Synopsis [Derives BDDs for the partitions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_Nonlin4DerivePartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder ) +{ + Vec_Ptr_t * vRoots; + Aig_Obj_t * pObj; + DdNode * bBdd, * bBdd0, * bBdd1, * bPart; + int i; + Aig_ManCleanData( pAig ); + // assign elementary variables + Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) ); + Aig_ManForEachNode( pAig, pObj, i ) + if ( Llb_MnxBddVar(vOrder, pObj) >= 0 ) + { + pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) ); + Cudd_Ref( (DdNode *)pObj->pData ); + } + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) ); + // compute intermediate BDDs + vRoots = Vec_PtrAlloc( 100 ); + Aig_ManForEachNode( pAig, pObj, i ) + { + bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); + bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); + if ( bBdd == NULL ) + goto finish; + Cudd_Ref( bBdd ); + if ( pObj->pData == NULL ) + { + pObj->pData = bBdd; + continue; + } + // create new partition + bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd ); + if ( bPart == NULL ) + goto finish; + Cudd_Ref( bPart ); + Cudd_RecursiveDeref( dd, bBdd ); + Vec_PtrPush( vRoots, bPart ); +//printf( "%d ", Cudd_DagSize(bPart) ); + } + // compute register output BDDs + Saig_ManForEachLi( pAig, pObj, i ) + { + bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd0 ); + if ( bPart == NULL ) + goto finish; + Cudd_Ref( bPart ); + Vec_PtrPush( vRoots, bPart ); +//printf( "%d ", Cudd_DagSize(bPart) ); + } +//printf( "\n" ); + Aig_ManForEachNode( pAig, pObj, i ) + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); + return vRoots; + // early termination +finish: + Aig_ManForEachNode( pAig, pObj, i ) + if ( pObj->pData ) + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); + Vec_PtrForEachEntry( DdNode *, vRoots, bPart, i ) + Cudd_RecursiveDeref( dd, bPart ); + Vec_PtrFree( vRoots ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Find simple variable ordering.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_Nonlin4CreateOrderSimple( Aig_Man_t * pAig ) +{ + Vec_Int_t * vOrder; + Aig_Obj_t * pObj; + int i, Counter = 0; + vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) ); + Aig_ManForEachPi( pAig, pObj, i ) + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); + Saig_ManForEachLi( pAig, pObj, i ) + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); + return vOrder; +} + +/**Function************************************************************* + + Synopsis [Find good static variable ordering.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4CreateOrderSmart_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter ) +{ + Aig_Obj_t * pFanin0, * pFanin1; + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent( pAig, pObj ); + assert( Llb_MnxBddVar(vOrder, pObj) < 0 ); + if ( Aig_ObjIsPi(pObj) ) + { + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ ); + return; + } + // try fanins with higher level first + pFanin0 = Aig_ObjFanin0(pObj); + pFanin1 = Aig_ObjFanin1(pObj); +// if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) ) + if ( pFanin0->Level > pFanin1->Level ) + { + Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin0, vOrder, pCounter ); + Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin1, vOrder, pCounter ); + } + else + { + Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin1, vOrder, pCounter ); + Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin0, vOrder, pCounter ); + } + if ( pObj->fMarkA ) + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ ); +} + +/**Function************************************************************* + + Synopsis [Collect nodes with the given fanout count.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_Nonlin4CollectHighRefNodes( Aig_Man_t * pAig, int nFans ) +{ + Vec_Int_t * vNodes; + Aig_Obj_t * pObj; + int i; + Aig_ManCleanMarkA( pAig ); + Aig_ManForEachNode( pAig, pObj, i ) + if ( Aig_ObjRefs(pObj) >= nFans ) + pObj->fMarkA = 1; + // unmark flop drivers + Saig_ManForEachLi( pAig, pObj, i ) + Aig_ObjFanin0(pObj)->fMarkA = 0; + // collect mapping + vNodes = Vec_IntAlloc( 100 ); + Aig_ManForEachNode( pAig, pObj, i ) + if ( pObj->fMarkA ) + Vec_IntPush( vNodes, Aig_ObjId(pObj) ); + Aig_ManCleanMarkA( pAig ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Find good static variable ordering.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_Nonlin4CreateOrderSmart( Aig_Man_t * pAig ) +{ + Vec_Int_t * vNodes = NULL; + Vec_Int_t * vOrder; + Aig_Obj_t * pObj; + int i, Counter = 0; +/* + // mark internal nodes to be used + Aig_ManCleanMarkA( pAig ); + vNodes = Llb_Nonlin4CollectHighRefNodes( pAig, 4 ); + Aig_ManForEachNodeVec( pAig, vNodes, pObj, i ) + pObj->fMarkA = 1; +printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) ); +*/ + + // collect nodes in the order + vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) ); + Aig_ManIncrementTravId( pAig ); + Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) ); + Saig_ManForEachLi( pAig, pObj, i ) + { + Llb_Nonlin4CreateOrderSmart_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter ); + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); + } + Aig_ManForEachPi( pAig, pObj, i ) + if ( Llb_MnxBddVar(vOrder, pObj) < 0 ) + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); + assert( Counter <= Aig_ManPiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) ); + Aig_ManCleanMarkA( pAig ); + Vec_IntFreeP( &vNodes ); + return vOrder; +} + + +/**Function************************************************************* + + Synopsis [Creates quantifiable varaibles for both types of traversal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_Nonlin4CreateVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fForward ) +{ + Vec_Int_t * vVars2Q; + Aig_Obj_t * pObj; + int i; + vVars2Q = Vec_IntAlloc( 0 ); + Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 ); + if ( fForward ) + { + Saig_ManForEachLi( pAig, pObj, i ) + Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 ); + } + else + { + Aig_ManForEachPi( pAig, pObj, i ) + Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 ); + } + return vVars2Q; +} + +/**Function************************************************************* + + Synopsis [Compute initial state in terms of current state variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4SetupVarMap( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder ) +{ + DdNode ** pVarsX, ** pVarsY; + Aig_Obj_t * pObjLo, * pObjLi; + int i; + pVarsX = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) ); + pVarsY = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) ); + Saig_ManForEachLiLo( pAig, pObjLo, pObjLi, i ) + { + pVarsX[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLo) ); + pVarsY[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLi) ); + } + Cudd_SetVarMap( dd, pVarsX, pVarsY, Aig_ManRegNum(pAig) ); + ABC_FREE( pVarsX ); + ABC_FREE( pVarsY ); +} + +/**Function************************************************************* + + Synopsis [Compute initial state in terms of current state variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_Nonlin4ComputeInitState( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder ) +{ + Aig_Obj_t * pObj; + DdNode * bRes, * bVar, * bTemp; + int i, TimeStop; + TimeStop = dd->TimeStop; dd->TimeStop = 0; + bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); + Saig_ManForEachLo( pAig, pObj, i ) + { + bVar = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) ); + 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 [Compute initial state in terms of current state variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_Nonlin4ComputeCube( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, char * pValues ) +{ + Aig_Obj_t * pObj, * pObjLi; + DdNode * bRes, * bVar, * bTemp; + int i, TimeStop; + TimeStop = dd->TimeStop; dd->TimeStop = 0; + bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); + Saig_ManForEachLo( pAig, pObj, i ) + { + if ( pValues[Llb_MnxBddVar(vOrder, pObj)] == 2 ) + continue; + // get the correspoding flop input variable + pObjLi = Saig_ObjLoToLi(pAig, pObj); + bVar = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLi) ); + if ( pValues[Llb_MnxBddVar(vOrder, pObj)] == 0 ) + bVar = Cudd_Not(bVar); + // create cube + bRes = Cudd_bddAnd( dd, bTemp = bRes, 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_Nonlin4DeriveCex( Llb_Mnx_t * p ) +{ + Abc_Cex_t * pCex; + Aig_Obj_t * pObj; + DdNode * bState, * bImage, * bOneCube, * bRing; + int i, v, RetValue, nPiOffset; + char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->dd) ); + assert( Vec_PtrSize(p->vRings) > 0 ); + // disable the timeout + p->dd->TimeStop = 0; + + // update quantifiable vars + Vec_IntFreeP( &p->vVars2Q ); + p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, p->pAig, p->vOrder, 0 ); + + // 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->dd, (DdNode *)Vec_PtrEntryLast(p->vRings), p->bBad ); Cudd_Ref( bOneCube ); + RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues ); + Cudd_RecursiveDeref( p->dd, 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[Llb_MnxBddVar(p->vOrder, pObj)] == 1 ) + Aig_InfoSetBit( pCex->pData, nPiOffset + i ); + + // write state in terms of NS variables + if ( Vec_PtrSize(p->vRings) > 1 ) + { + bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues ); Cudd_Ref( bState ); + } + // perform backward analysis + Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v ) + { + if ( v == Vec_PtrSize(p->vRings) - 1 ) + continue; + // compute the next states + bImage = Llb_Nonlin4Image( p->dd, p->vRoots, bState, p->vVars2Q ); + assert( bImage != NULL ); + Cudd_Ref( bImage ); + Cudd_RecursiveDeref( p->dd, bState ); + + // intersect with the previous set + bOneCube = Cudd_bddIntersect( p->dd, bImage, bRing ); Cudd_Ref( bOneCube ); + Cudd_RecursiveDeref( p->dd, bImage ); + + // find any assignment of the BDD + RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues ); + Cudd_RecursiveDeref( p->dd, bOneCube ); + assert( RetValue ); + + // write PIs of counter-example + nPiOffset -= Saig_ManPiNum(p->pAig); + Saig_ManForEachPi( p->pAig, pObj, i ) + if ( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 1 ) + Aig_InfoSetBit( pCex->pData, nPiOffset + i ); + + // check that we get the init state + if ( v == 0 ) + { + Saig_ManForEachLo( p->pAig, pObj, i ) + assert( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 0 ); + break; + } + + // write state in terms of NS variables + bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues ); Cudd_Ref( bState ); + } + assert( nPiOffset == Saig_ManRegNum(p->pAig) ); + // update the output number +//Abc_CexPrint( pCex ); + RetValue = Saig_ManFindFailedPoCex( p->pAig, pCex ); + assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pAig) ); // invalid CEX!!! + pCex->iPo = RetValue; + // cleanup + ABC_FREE( pValues ); + return pCex; +} + + +/**Function************************************************************* + + Synopsis [Perform reachability with hints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) +{ + DdNode * bAux; + int nIters, nBddSizeFr, nBddSizeTo, nBddSizeTo2; + int clkTemp, clkIter, clk = clock(); + assert( Aig_ManRegNum(p->pAig) > 0 ); + + // compute time to stop + if ( p->pPars->TimeLimit ) + p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC; + else + p->pPars->TimeTarget = 0; + // set the stop time parameter + p->dd->TimeStop = p->pPars->TimeTarget; + + // create bad state in the ring manager + if ( !p->pPars->fSkipOutCheck ) + { + p->bBad = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder ); + if ( p->bBad == 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->bBad ); + } + + // compute the starting set of states + p->bCurrent = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder ); Cudd_Ref( p->bCurrent ); + p->bReached = p->bCurrent; Cudd_Ref( p->bCurrent ); + for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ ) + { + clkIter = clock(); + // check the runtime limit + if ( p->pPars->TimeLimit && 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; + return -1; + } + + // save the onion ring + Vec_PtrPush( p->vRings, p->bCurrent ); Cudd_Ref( p->bCurrent ); + + // check it for bad states + if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->dd, p->bCurrent, Cudd_Not(p->bBad) ) ) + { + assert( p->pAig->pSeqModel == NULL ); + if ( !p->pPars->fBackward ) + p->pAig->pSeqModel = Llb_Nonlin4DeriveCex( 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->pAig->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; + return 0; + } + + // compute the next states + clkTemp = clock(); + p->bNext = Llb_Nonlin4Image( p->dd, p->vRoots, p->bCurrent, p->vVars2Q ); + if ( p->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; + return -1; + } + Cudd_Ref( p->bNext ); + p->timeImage += clock() - clkTemp; + + // remap into current states + clkTemp = clock(); + p->bNext = Cudd_bddVarMap( p->dd, bAux = p->bNext ); + if ( p->bNext == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during remapping next states.\n", p->pPars->TimeLimit ); + Cudd_RecursiveDeref( p->dd, bAux ); + p->pPars->iFrame = nIters - 1; + return -1; + } + Cudd_Ref( p->bNext ); + Cudd_RecursiveDeref( p->dd, bAux ); + p->timeRemap += clock() - clkTemp; + + // collect statistics + if ( p->pPars->fVerbose ) + { + nBddSizeFr = Cudd_DagSize( p->bCurrent ); + nBddSizeTo = Cudd_DagSize( bAux ); + nBddSizeTo2 = Cudd_DagSize( p->bNext ); + } + Cudd_RecursiveDeref( p->dd, p->bCurrent ); p->bCurrent = NULL; + + // derive new states + p->bCurrent = Cudd_bddAnd( p->dd, p->bNext, Cudd_Not(p->bReached) ); + if ( p->bCurrent == 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; + return -1; + } + Cudd_Ref( p->bCurrent ); + Cudd_RecursiveDeref( p->dd, p->bNext ); p->bNext = NULL; + if ( Cudd_IsConstant(p->bCurrent) ) + break; + + // add to the reached set + p->bReached = Cudd_bddOr( p->dd, bAux = p->bReached, p->bCurrent ); + if ( p->bReached == 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, bAux ); + return -1; + } + Cudd_Ref( p->bReached ); + Cudd_RecursiveDeref( p->dd, bAux ); + + // report the results + if ( p->pPars->fVerbose ) + { + printf( "I =%5d : ", nIters ); + printf( "Fr =%7d ", nBddSizeFr ); + printf( "ImNs =%7d ", nBddSizeTo ); + printf( "ImCs =%7d ", nBddSizeTo2 ); + printf( "Rea =%7d ", Cudd_DagSize(p->bReached) ); + printf( "(%4d %4d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) ); + Abc_PrintTime( 1, "T", clock() - clkIter ); + } +/* + if ( pPars->fVerbose ) + { + double nMints = Cudd_CountMinterm(p->dd, bReached, Saig_ManRegNum(p->pAig) ); +// Extra_bddPrint( p->dd, bReached );printf( "\n" ); + 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 - 1 ) + { + if ( !p->pPars->fSilent ) + printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax ); + p->pPars->iFrame = nIters; + return -1; + } + } + + // report the stats + if ( p->pPars->fVerbose ) + { + double nMints = Cudd_CountMinterm(p->dd, p->bReached, Saig_ManRegNum(p->pAig) ); + if ( p->bCurrent && Cudd_IsConstant(p->bCurrent) ) + printf( "Reachability analysis completed after %d frames.\n", nIters ); + else + printf( "Reachability analysis is stopped 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 ( p->bCurrent == NULL || !Cudd_IsConstant(p->bCurrent) ) + { + 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 [Reorders BDDs in the working manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4Reorder( DdManager * dd, int fTwice, int fVerbose ) +{ + int clk = clock(); + if ( fVerbose ) + Abc_Print( 1, "Reordering... Before =%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 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) +{ + Llb_Mnx_t * p; + p = ABC_CALLOC( Llb_Mnx_t, 1 ); + p->pAig = pAig; + p->pPars = pPars; +// p->vOrder = Llb_Nonlin4CreateOrderSimple( pAig ); + p->vOrder = Llb_Nonlin4CreateOrderSmart( pAig ); + p->dd = Cudd_Init( Vec_IntSize(p->vOrder), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Llb_Nonlin4SetupVarMap( p->dd, pAig, p->vOrder ); + Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); + p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, pAig, p->vOrder, 1 ); + p->vRoots = Llb_Nonlin4DerivePartitions( p->dd, pAig, p->vOrder ); + p->vRings = Vec_PtrAlloc( 100 ); + if ( pPars->fReorder ) + Llb_Nonlin4Reorder( p->dd, 0, 1 ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MnxStop( Llb_Mnx_t * p ) +{ + DdNode * bTemp; + int i; + if ( p->pPars->fVerbose ) + { + p->timeReo = Cudd_ReadReorderingTime(p->dd); + p->timeOther = p->timeTotal - p->timeImage - p->timeRemap; + ABC_PRTP( "Image ", p->timeImage, p->timeTotal ); + ABC_PRTP( "Remap ", p->timeRemap, p->timeTotal ); + ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); + ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + ABC_PRTP( " reo ", p->timeReo, p->timeTotal ); + } + // remove BDDs + if ( p->bBad ) + Cudd_RecursiveDeref( p->dd, p->bBad ); + if ( p->bReached ) + Cudd_RecursiveDeref( p->dd, p->bReached ); + if ( p->bCurrent ) + Cudd_RecursiveDeref( p->dd, p->bCurrent ); + if ( p->bNext ) + Cudd_RecursiveDeref( p->dd, p->bNext ); + Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i ) + Cudd_RecursiveDeref( p->dd, bTemp ); + Vec_PtrForEachEntry( DdNode *, p->vRoots, bTemp, i ) + Cudd_RecursiveDeref( p->dd, bTemp ); + // remove arrays + Vec_PtrFree( p->vRings ); + Vec_PtrFree( p->vRoots ); + Extra_StopManager( p->dd ); + Vec_IntFreeP( &p->vOrder ); + Vec_IntFreeP( &p->vVars2Q ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [Finds balanced cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) +{ + Llb_Mnx_t * pMnn; + int RetValue = -1; + if ( pPars->fVerbose ) + Aig_ManPrintStats( pAig ); + if ( !pPars->fSkipReach ) + { + int clk = clock(); + pMnn = Llb_MnxStart( pAig, pPars ); + RetValue = Llb_Nonlin4Reachability( pMnn ); + pMnn->timeTotal = clock() - clk; + Llb_MnxStop( pMnn ); + } + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |