| /**CFile**************************************************************** |
| |
| FileName [llb1Reach.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [BDD based reachability.] |
| |
| Synopsis [Reachability analysis.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: llb1Reach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "llbInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives global BDD for the node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager * dd ) |
| { |
| DdNode * bBdd0, * bBdd1, * bFunc; |
| Vec_Ptr_t * vNodes; |
| Aig_Obj_t * pObj = NULL; |
| int i; |
| abctime TimeStop; |
| if ( Aig_ObjFanin0(pNode) == Aig_ManConst1(pAig) ) |
| return Cudd_NotCond( Cudd_ReadOne(dd), Aig_ObjFaninC0(pNode) ); |
| TimeStop = dd->TimeStop; dd->TimeStop = 0; |
| vNodes = Aig_ManDfsNodes( pAig, &pNode, 1 ); |
| assert( Vec_PtrSize(vNodes) > 0 ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| { |
| if ( !Aig_ObjIsNode(pObj) ) |
| continue; |
| bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); |
| bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); |
| pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData ); |
| } |
| bFunc = (DdNode *)pObj->pData; Cudd_Ref( bFunc ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) |
| { |
| if ( !Aig_ObjIsNode(pObj) ) |
| continue; |
| Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); |
| } |
| Vec_PtrFree( vNodes ); |
| if ( Aig_ObjIsCo(pNode) ) |
| bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pNode) ); |
| Cudd_Deref( bFunc ); |
| dd->TimeStop = TimeStop; |
| return bFunc; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives BDD for the group.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup ) |
| { |
| Aig_Obj_t * pObj; |
| DdNode * bBdd0, * bBdd1, * bRes, * bXor, * bTemp; |
| int i, k; |
| Aig_ManConst1(p->pAig)->pData = Cudd_ReadOne( p->dd ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) |
| pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i ) |
| { |
| bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); |
| bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); |
| // pObj->pData = Extra_bddAndTime( p->dd, bBdd0, bBdd1, p->pPars->TimeTarget ); |
| pObj->pData = Cudd_bddAnd( p->dd, bBdd0, bBdd1 ); |
| if ( pObj->pData == NULL ) |
| { |
| Vec_PtrForEachEntryStop( Aig_Obj_t *, pGroup->vNodes, pObj, k, i ) |
| if ( pObj->pData ) |
| Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData ); |
| return NULL; |
| } |
| Cudd_Ref( (DdNode *)pObj->pData ); |
| } |
| bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i ) |
| { |
| if ( Aig_ObjIsCo(pObj) ) |
| bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); |
| else |
| bBdd0 = (DdNode *)pObj->pData; |
| bBdd1 = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); |
| bXor = Cudd_bddXor( p->dd, bBdd0, bBdd1 ); Cudd_Ref( bXor ); |
| // bRes = Extra_bddAndTime( p->dd, bTemp = bRes, Cudd_Not(bXor), p->pPars->TimeTarget ); |
| bRes = Cudd_bddAnd( p->dd, bTemp = bRes, Cudd_Not(bXor) ); |
| if ( bRes == NULL ) |
| { |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| Cudd_RecursiveDeref( p->dd, bXor ); |
| Vec_PtrForEachEntryStop( Aig_Obj_t *, pGroup->vNodes, pObj, k, i ) |
| if ( pObj->pData ) |
| Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData ); |
| return NULL; |
| } |
| Cudd_Ref( bRes ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| Cudd_RecursiveDeref( p->dd, bXor ); |
| } |
| Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i ) |
| Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData ); |
| Cudd_Deref( bRes ); |
| return bRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives quantification cube.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace, int fBackward ) |
| { |
| Aig_Obj_t * pObj; |
| DdNode * bRes, * bTemp, * bVar; |
| int i, iGroupFirst, iGroupLast; |
| abctime TimeStop; |
| TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; |
| bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) |
| { |
| if ( fBackward && Saig_ObjIsPi(p->pAig, pObj) ) |
| continue; |
| iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj)); |
| iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj)); |
| assert( iGroupFirst <= iGroupLast ); |
| if ( iGroupFirst < iGroupLast ) |
| continue; |
| bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); |
| bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| } |
| Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i ) |
| { |
| if ( fBackward && Saig_ObjIsPi(p->pAig, pObj) ) |
| continue; |
| iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj)); |
| iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj)); |
| assert( iGroupFirst <= iGroupLast ); |
| if ( iGroupFirst < iGroupLast ) |
| continue; |
| bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); |
| bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| } |
| Cudd_Deref( bRes ); |
| p->dd->TimeStop = TimeStop; |
| return bRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives quantification cube.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdNode * Llb_ManConstructQuantCubeFwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace ) |
| { |
| Aig_Obj_t * pObj; |
| DdNode * bRes, * bTemp, * bVar; |
| int i, iGroupLast; |
| abctime TimeStop; |
| TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; |
| bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) |
| { |
| iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj)); |
| assert( iGroupLast >= iGrpPlace ); |
| if ( iGroupLast > iGrpPlace ) |
| continue; |
| bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); |
| bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| } |
| Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i ) |
| { |
| iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj)); |
| assert( iGroupLast >= iGrpPlace ); |
| if ( iGroupLast > iGrpPlace ) |
| continue; |
| bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); |
| bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| } |
| Cudd_Deref( bRes ); |
| p->dd->TimeStop = TimeStop; |
| return bRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives quantification cube.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdNode * Llb_ManConstructQuantCubeBwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace ) |
| { |
| Aig_Obj_t * pObj; |
| DdNode * bRes, * bTemp, * bVar; |
| int i, iGroupFirst; |
| abctime TimeStop; |
| TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; |
| bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) |
| { |
| if ( Saig_ObjIsPi(p->pAig, pObj) ) |
| continue; |
| iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj)); |
| assert( iGroupFirst <= iGrpPlace ); |
| if ( iGroupFirst < iGrpPlace ) |
| continue; |
| bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); |
| bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| } |
| Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i ) |
| { |
| if ( Saig_ObjIsPi(p->pAig, pObj) ) |
| continue; |
| iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj)); |
| assert( iGroupFirst <= iGrpPlace ); |
| if ( iGroupFirst < iGrpPlace ) |
| continue; |
| bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); |
| bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| } |
| Cudd_Deref( bRes ); |
| p->dd->TimeStop = TimeStop; |
| return bRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdNode * Llb_ManComputeInitState( Llb_Man_t * p, 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( p->pAig, pObj, i ) |
| { |
| iVar = (dd == p->ddG) ? i : Vec_IntEntry(p->vObj2Var, 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 [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit, int fBackward ) |
| { |
| int fCheckSupport = 0; |
| Llb_Grp_t * pGroup; |
| DdNode * bImage, * bGroup, * bCube, * bTemp; |
| int k, Index; |
| bImage = bInit; Cudd_Ref( bImage ); |
| for ( k = 1; k < p->pMatrix->nCols-1; k++ ) |
| { |
| if ( fBackward ) |
| Index = p->pMatrix->nCols - 1 - k; |
| else |
| Index = k; |
| |
| // compute group BDD |
| pGroup = p->pMatrix->pColGrps[Index]; |
| bGroup = Llb_ManConstructGroupBdd( p, pGroup ); |
| if ( bGroup == NULL ) |
| { |
| Cudd_RecursiveDeref( p->dd, bImage ); |
| return NULL; |
| } |
| Cudd_Ref( bGroup ); |
| // quantify variables appearing only in this group |
| bCube = Llb_ManConstructQuantCubeIntern( p, pGroup, Index, fBackward ); Cudd_Ref( bCube ); |
| bGroup = Cudd_bddExistAbstract( p->dd, bTemp = bGroup, bCube ); |
| if ( bGroup == NULL ) |
| { |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| Cudd_RecursiveDeref( p->dd, bCube ); |
| return NULL; |
| } |
| Cudd_Ref( bGroup ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| Cudd_RecursiveDeref( p->dd, bCube ); |
| // perform partial product |
| if ( fBackward ) |
| bCube = Llb_ManConstructQuantCubeBwd( p, pGroup, Index ); |
| else |
| bCube = Llb_ManConstructQuantCubeFwd( p, pGroup, Index ); |
| Cudd_Ref( bCube ); |
| // bImage = Extra_bddAndAbstractTime( p->dd, bTemp = bImage, bGroup, bCube, p->pPars->TimeTarget ); |
| bImage = Cudd_bddAndAbstract( p->dd, bTemp = bImage, bGroup, bCube ); |
| if ( bImage == NULL ) |
| { |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| Cudd_RecursiveDeref( p->dd, bGroup ); |
| Cudd_RecursiveDeref( p->dd, bCube ); |
| return NULL; |
| } |
| Cudd_Ref( bImage ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| Cudd_RecursiveDeref( p->dd, bGroup ); |
| Cudd_RecursiveDeref( p->dd, bCube ); |
| } |
| |
| // make sure image depends on next state vars |
| if ( fCheckSupport ) |
| { |
| bCube = Cudd_Support( p->dd, bImage ); Cudd_Ref( bCube ); |
| for ( bTemp = bCube; bTemp != p->dd->one; bTemp = cuddT(bTemp) ) |
| { |
| int ObjId = Vec_IntEntry( p->vVar2Obj, bTemp->index ); |
| Aig_Obj_t * pObj = Aig_ManObj( p->pAig, ObjId ); |
| if ( !Saig_ObjIsLi(p->pAig, pObj) ) |
| printf( "Var %d assigned to obj %d that is not LI\n", bTemp->index, ObjId ); |
| } |
| Cudd_RecursiveDeref( p->dd, bCube ); |
| } |
| Cudd_Deref( bImage ); |
| return bImage; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNsVars ) |
| { |
| DdNode * bConstr, * bFunc, * bTemp; |
| Aig_Obj_t * pObj; |
| int i, Entry; |
| abctime TimeStop; |
| if ( vHints == NULL ) |
| return Cudd_ReadOne( p->dd ); |
| TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; |
| assert( Aig_ManCiNum(p->pAig) == Aig_ManCiNum(p->pAigGlo) ); |
| // assign const and PI nodes to the original AIG |
| Aig_ManCleanData( p->pAig ); |
| Aig_ManConst1( p->pAig )->pData = Cudd_ReadOne( p->dd ); |
| Saig_ManForEachPi( p->pAig, pObj, i ) |
| pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var,Aig_ObjId(pObj)) ); |
| Saig_ManForEachLo( p->pAig, pObj, i ) |
| { |
| if ( fUseNsVars ) |
| Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(Saig_ObjLoToLi(p->pAig, pObj)) ); |
| else |
| Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(pObj) ); |
| pObj->pData = Cudd_bddIthVar( p->dd, Entry ); |
| } |
| // transfer them to the global AIG |
| Aig_ManCleanData( p->pAigGlo ); |
| Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd ); |
| Aig_ManForEachCi( p->pAigGlo, pObj, i ) |
| pObj->pData = Aig_ManCi(p->pAig, i)->pData; |
| // derive consraints |
| bConstr = Cudd_ReadOne( p->dd ); Cudd_Ref( bConstr ); |
| Vec_IntForEachEntry( vHints, Entry, i ) |
| { |
| if ( Entry != 0 && Entry != 1 ) |
| continue; |
| bFunc = Llb_ManConstructOutBdd( p->pAigGlo, Aig_ManObj(p->pAigGlo, i), p->dd ); Cudd_Ref( bFunc ); |
| bFunc = Cudd_NotCond( bFunc, Entry ); // restrict to not constraint |
| // make the product |
| bConstr = Cudd_bddAnd( p->dd, bTemp = bConstr, bFunc ); Cudd_Ref( bConstr ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| Cudd_RecursiveDeref( p->dd, bFunc ); |
| } |
| Cudd_Deref( bConstr ); |
| p->dd->TimeStop = TimeStop; |
| return bConstr; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Perform reachability with hints and returns reached states in ppGlo.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Cex_t * Llb_ManReachDeriveCex( Llb_Man_t * p ) |
| { |
| Abc_Cex_t * pCex; |
| Aig_Obj_t * pObj; |
| 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; |
| |
| /* |
| 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, p->vGlo2Ns, 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_ManComputeImage( p, bState, 1 ); |
| assert( bImage != NULL ); |
| Cudd_Ref( bImage ); |
| Cudd_RecursiveDeref( p->dd, bState ); |
| //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 ); |
| //Extra_bddPrintSupport( p->ddR, bImage ); printf( "\n" ); |
| |
| // 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 ); |
| /* |
| for ( i = 0; i < p->ddR->size; i++ ) |
| printf( "%d ", pValues[i] ); |
| printf( "\n" ); |
| */ |
| // 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, p->vGlo2Ns, 1, pValues ); Cudd_Ref( bState ); |
| } |
| assert( nPiOffset == Saig_ManRegNum(p->pAig) ); |
| // update the output number |
| //Abc_CexPrint( pCex ); |
| RetValue = Saig_ManFindFailedPoCex( p->pAigGlo, pCex ); |
| assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pAigGlo) ); // invalid CEX!!! |
| pCex->iPo = RetValue; |
| // cleanup |
| ABC_FREE( pValues ); |
| return pCex; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Perform reachability with hints and returns reached states in ppGlo.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo ) |
| { |
| int * pNs2Glo = Vec_IntArray( p->vNs2Glo ); |
| int * pCs2Glo = Vec_IntArray( p->vCs2Glo ); |
| int * pGlo2Cs = Vec_IntArray( p->vGlo2Cs ); |
| DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube; |
| DdNode * bConstrCs, * bConstrNs; |
| abctime clk2, clk = Abc_Clock(); |
| int nIters, nBddSize = 0; |
| // int nThreshold = 10000; |
| |
| // compute time to stop |
| p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0; |
| |
| // define variable limits |
| Llb_ManPrepareVarLimits( p ); |
| |
| // start the managers |
| assert( p->dd == NULL ); |
| assert( p->ddG == NULL ); |
| assert( p->ddR == NULL ); |
| p->dd = Cudd_Init( Vec_IntSize(p->vVar2Obj), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); |
| p->ddR = Cudd_Init( Aig_ManCiNum(p->pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); |
| if ( pddGlo && *pddGlo ) |
| p->ddG = *pddGlo, *pddGlo = NULL; |
| else |
| p->ddG = Cudd_Init( Aig_ManRegNum(p->pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); |
| |
| if ( p->pPars->fReorder ) |
| { |
| Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); |
| Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT ); |
| Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT ); |
| } |
| else |
| { |
| Cudd_AutodynDisable( p->dd ); |
| Cudd_AutodynDisable( p->ddG ); |
| Cudd_AutodynDisable( p->ddR ); |
| } |
| |
| // set the stop time parameter |
| p->dd->TimeStop = p->pPars->TimeTarget; |
| p->ddG->TimeStop = p->pPars->TimeTarget; |
| p->ddR->TimeStop = p->pPars->TimeTarget; |
| |
| // create bad state in the ring manager |
| p->ddR->bFunc = Llb_BddComputeBad( p->pAigGlo, 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 ); |
| |
| // derive constraints |
| bConstrCs = Llb_ManCreateConstraints( p, vHints, 0 ); Cudd_Ref( bConstrCs ); |
| bConstrNs = Llb_ManCreateConstraints( p, vHints, 1 ); Cudd_Ref( bConstrNs ); |
| //Extra_bddPrint( p->dd, bConstrCs ); printf( "\n" ); |
| //Extra_bddPrint( p->dd, bConstrNs ); printf( "\n" ); |
| |
| // perform reachability analysis |
| // compute the starting set of states |
| if ( p->ddG->bFunc ) |
| { |
| bReached = p->ddG->bFunc; p->ddG->bFunc = NULL; |
| bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Cs ); Cudd_Ref( bCurrent ); |
| } |
| else |
| { |
| bReached = Llb_ManComputeInitState( p, p->ddG ); Cudd_Ref( bReached ); |
| bCurrent = Llb_ManComputeInitState( p, p->dd ); Cudd_Ref( bCurrent ); |
| } |
| //Extra_bddPrintSupport( p->ddG, bReached ); printf( "\n" ); |
| //Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" ); |
| |
| //Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" ); |
| for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ ) |
| { |
| clk2 = Abc_Clock(); |
| // check the runtime limit |
| if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget ) |
| { |
| if ( !p->pPars->fSilent ) |
| printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit ); |
| p->pPars->iFrame = nIters - 1; |
| Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; |
| Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; |
| Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; |
| Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; |
| return -1; |
| } |
| |
| // save the onion ring |
| bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pCs2Glo ); |
| 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; |
| Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; |
| Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; |
| Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; |
| 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->pAigGlo->pSeqModel == NULL ); |
| if ( !p->pPars->fBackward ) |
| p->pAigGlo->pSeqModel = Llb_ManReachDeriveCex( p ); |
| if ( !p->pPars->fSilent ) |
| { |
| if ( !p->pPars->fBackward ) |
| Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pAigGlo->pSeqModel->iPo, p->pAigGlo->pName, p->pAigGlo->pName, nIters ); |
| else |
| Abc_Print( 1, "Output ??? of miter \"%s\" was asserted in frame %d (counter-example is not produced). ", p->pAigGlo->pName, nIters ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| } |
| p->pPars->iFrame = nIters - 1; |
| Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; |
| Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; |
| Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; |
| Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; |
| return 0; |
| } |
| |
| // restrict reachable states using constraints |
| if ( vHints ) |
| { |
| bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, bConstrCs ); Cudd_Ref( bCurrent ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| } |
| |
| // quantify variables appearing only in the init state |
| bCube = Llb_ManConstructQuantCubeIntern( p, (Llb_Grp_t *)Vec_PtrEntry(p->vGroups,0), 0, 0 ); Cudd_Ref( bCube ); |
| bCurrent = Cudd_bddExistAbstract( p->dd, bTemp = bCurrent, bCube ); Cudd_Ref( bCurrent ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| Cudd_RecursiveDeref( p->dd, bCube ); |
| |
| // compute the next states |
| bNext = Llb_ManComputeImage( p, bCurrent, 0 ); |
| if ( bNext == NULL ) |
| { |
| 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; |
| Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; |
| Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; |
| Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; |
| return -1; |
| } |
| Cudd_Ref( bNext ); |
| Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; |
| |
| // restrict reachable states using constraints |
| if ( vHints ) |
| { |
| bNext = Cudd_bddAnd( p->dd, bTemp = bNext, bConstrNs ); Cudd_Ref( bNext ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| } |
| //Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" ); |
| |
| // remap these states into the current state vars |
| // bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo ); Cudd_Ref( bNext ); |
| // Cudd_RecursiveDeref( p->dd, bTemp ); |
| // bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pNs2Glo, p->pPars->TimeTarget ); |
| bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo ); |
| if ( bNext == 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, bTemp ); |
| Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; |
| Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; |
| Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; |
| return -1; |
| } |
| Cudd_Ref( bNext ); |
| Cudd_RecursiveDeref( p->dd, bTemp ); |
| |
| |
| // check if there are any new states |
| if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states |
| { |
| Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL; |
| break; |
| } |
| |
| // check the BDD size |
| nBddSize = Cudd_DagSize(bNext); |
| if ( nBddSize > p->pPars->nBddMax ) |
| { |
| Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL; |
| break; |
| } |
| |
| // get the new states |
| bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) ); |
| if ( bCurrent == NULL ) |
| { |
| Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL; |
| Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; |
| break; |
| } |
| Cudd_Ref( bCurrent ); |
| // minimize the new states with the reached states |
| // bCurrent = Cudd_bddConstrain( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); |
| // bCurrent = Cudd_bddRestrict( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); |
| // Cudd_RecursiveDeref( p->ddG, bTemp ); |
| //printf( "Initial BDD =%7d. Constrained BDD =%7d.\n", Cudd_DagSize(bTemp), Cudd_DagSize(bCurrent) ); |
| |
| // remap these states into the current state vars |
| // bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs ); Cudd_Ref( bCurrent ); |
| // Cudd_RecursiveDeref( p->ddG, bTemp ); |
| // bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs, p->pPars->TimeTarget ); |
| bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs ); |
| if ( bCurrent == 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; |
| Cudd_RecursiveDeref( p->ddG, bTemp ); |
| Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; |
| Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; |
| Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; |
| return -1; |
| } |
| Cudd_Ref( bCurrent ); |
| Cudd_RecursiveDeref( p->ddG, bTemp ); |
| |
| |
| // add to the reached states |
| bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext ); |
| if ( bReached == NULL ) |
| { |
| Cudd_RecursiveDeref( p->ddG, bTemp ); bTemp = NULL; |
| Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL; |
| break; |
| } |
| Cudd_Ref( bReached ); |
| Cudd_RecursiveDeref( p->ddG, bTemp ); |
| Cudd_RecursiveDeref( p->ddG, bNext ); |
| bNext = NULL; |
| |
| if ( p->pPars->fVerbose ) |
| { |
| fprintf( stdout, "F =%5d : ", nIters ); |
| fprintf( stdout, "Im =%6d ", nBddSize ); |
| fprintf( stdout, "(%4d %3d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) ); |
| fprintf( stdout, "Rea =%6d ", Cudd_DagSize(bReached) ); |
| fprintf( stdout, "(%4d%4d) ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 ); |
| } |
| /* |
| if ( p->pPars->fVerbose ) |
| { |
| double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) ); |
| // Extra_bddPrint( p->ddG, bReached );printf( "\n" ); |
| fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) ); |
| fflush( stdout ); |
| } |
| */ |
| } |
| Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; |
| Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; |
| if ( bReached == NULL ) |
| { |
| p->pPars->iFrame = nIters - 1; |
| return 0; // reachable |
| } |
| // assert( bCurrent == NULL ); |
| if ( bCurrent ) |
| Cudd_RecursiveDeref( p->dd, bCurrent ); |
| // report the stats |
| if ( p->pPars->fVerbose ) |
| { |
| double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) ); |
| if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax ) |
| fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters ); |
| else |
| fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters ); |
| fprintf( stdout, "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; |
| Cudd_RecursiveDeref( p->ddG, bReached ); |
| return -1; // undecided |
| } |
| if ( pddGlo ) |
| { |
| assert( p->ddG->bFunc == NULL ); |
| p->ddG->bFunc = bReached; bReached = NULL; |
| assert( *pddGlo == NULL ); |
| *pddGlo = p->ddG; p->ddG = NULL; |
| } |
| else |
| Cudd_RecursiveDeref( p->ddG, bReached ); |
| if ( !p->pPars->fSilent ) |
| printf( "The miter is proved unreachable after %d iterations. ", nIters ); |
| p->pPars->iFrame = nIters - 1; |
| return 1; // unreachable |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
