diff options
Diffstat (limited to 'src/proof/llb/llb4Nonlin.c')
| -rw-r--r-- | src/proof/llb/llb4Nonlin.c | 1080 |
1 files changed, 1080 insertions, 0 deletions
diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c new file mode 100644 index 00000000..33c6b3f7 --- /dev/null +++ b/src/proof/llb/llb4Nonlin.c @@ -0,0 +1,1080 @@ +/**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; +}; + +//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, * bCube; + 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_ObjBddVar(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 ) + { + bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube ); + Saig_ManForEachPi( pAig, pObj, i ) + { + bCube = Cudd_bddAnd( dd, bTemp = bCube, (DdNode *)pObj->pData ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + } + bResult = Cudd_bddExistAbstract( dd, bTemp = bResult, bCube ); Cudd_Ref( bResult ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bCube ); + 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_ObjBddVar(vOrder, pObj) ); + Aig_ManForEachNode( pAig, pObj, i ) + if ( Llb_ObjBddVar(vOrder, pObj) >= 0 ) + { + pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); + Cudd_Ref( (DdNode *)pObj->pData ); + } + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(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_Nonlin4CreateOrder_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_ObjBddVar(vOrder, pObj) < 0 ); + if ( Aig_ObjIsPi(pObj) ) + { +// if ( Saig_ObjIsLo(pAig, pObj) ) +// Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), (*pCounter)++ ); + 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_Nonlin4CreateOrder_rec( pAig, pFanin0, vOrder, pCounter ); + Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter ); + } + else + { + Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter ); + Llb_Nonlin4CreateOrder_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_Nonlin4CreateOrder( 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_ManForEachObjVec( vNodes, pAig, 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 ) + { + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); + Llb_Nonlin4CreateOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter ); + } + Aig_ManForEachPi( pAig, pObj, i ) + if ( Llb_ObjBddVar(vOrder, pObj) < 0 ) + { +// if ( Saig_ObjIsLo(pAig, pObj) ) +// Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), Counter++ ); + 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 fBackward ) +{ + Vec_Int_t * vVars2Q; + Aig_Obj_t * pObjLi, * pObjLo; + int i; + vVars2Q = Vec_IntAlloc( 0 ); + Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 ); + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, fBackward ? pObjLo : pObjLi), 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 ) + { + assert( Llb_ObjBddVar(vOrder, pObjLo) >= 0 ); + assert( Llb_ObjBddVar(vOrder, pObjLi) >= 0 ); + pVarsX[i] = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObjLo) ); + pVarsY[i] = Cudd_bddIthVar( dd, Llb_ObjBddVar(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, int fBackward ) +{ + Aig_Obj_t * pObjLi, * pObjLo; + DdNode * bRes, * bVar, * bTemp; + int i, TimeStop; + TimeStop = dd->TimeStop; dd->TimeStop = 0; + bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + { + bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, fBackward? pObjLi : pObjLo) ); + 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, int Flag ) +{ + Aig_Obj_t * pObjLo, * pObjLi, * pObjTemp; + DdNode * bRes, * bVar, * bTemp; + int i, TimeStop; + TimeStop = dd->TimeStop; dd->TimeStop = 0; + bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + { + if ( Flag ) + pObjTemp = pObjLo, pObjLo = pObjLi, pObjLi = pObjTemp; + // get the correspoding flop input variable + bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObjLi) ); + if ( pValues[Llb_ObjBddVar(vOrder, pObjLo)] != 1 ) + 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 [Compute initial state in terms of current state variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4RecordState( Aig_Man_t * pAig, Vec_Int_t * vOrder, unsigned * pState, char * pValues, int fBackward ) +{ + Aig_Obj_t * pObjLo, * pObjLi; + int i; + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + if ( pValues[Llb_ObjBddVar(vOrder, fBackward? pObjLi : pObjLo)] == 1 ) + Abc_InfoSetBit( pState, i ); +} + +/**Function************************************************************* + + Synopsis [Multiply every partition by the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_Nonlin4Multiply( DdManager * dd, DdNode * bCube, Vec_Ptr_t * vParts ) +{ + Vec_Ptr_t * vNew; + DdNode * bTemp, * bFunc; + int i; + vNew = Vec_PtrAlloc( Vec_PtrSize(vParts) ); + Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i ) + { + bTemp = Cudd_bddAnd( dd, bFunc, bCube ); Cudd_Ref( bTemp ); + Vec_PtrPush( vNew, bTemp ); + } + return vNew; +} + +/**Function************************************************************* + + Synopsis [Multiply every partition by the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4Deref( DdManager * dd, Vec_Ptr_t * vParts ) +{ + DdNode * bFunc; + int i; + Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i ) + Cudd_RecursiveDeref( dd, bFunc ); + Vec_PtrFree( vParts ); +} + +/**Function************************************************************* + + Synopsis [Derives counter-example by backward reachability.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p, int fBackward, int fVerbose ) +{ + Vec_Int_t * vVars2Q; + Vec_Ptr_t * vStates, * vRootsNew; + Aig_Obj_t * pObj; + DdNode * bState, * bImage, * bOneCube, * bRing; + int i, v, RetValue, clk = clock(); + char * pValues; + assert( Vec_PtrSize(p->vRings) > 0 ); + // disable the timeout + p->dd->TimeStop = 0; + + // start the state set + vStates = Vec_PtrAllocSimInfo( Vec_PtrSize(p->vRings), Abc_BitWordNum(Aig_ManRegNum(p->pAig)) ); + Vec_PtrCleanSimInfo( vStates, 0, Abc_BitWordNum(Aig_ManRegNum(p->pAig)) ); + if ( fBackward ) + Vec_PtrReverseOrder( vStates ); + + // get the last cube + pValues = ABC_ALLOC( char, Cudd_ReadSize(p->dd) ); + 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 ); + + // record the cube + Llb_Nonlin4RecordState( p->pAig, p->vOrder, (unsigned *)Vec_PtrEntryLast(vStates), pValues, fBackward ); + + // write state in terms of NS variables + if ( Vec_PtrSize(p->vRings) > 1 ) + { + bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues, fBackward ); Cudd_Ref( bState ); + } + // perform backward analysis + vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, p->pAig, p->vOrder, !fBackward ); + Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v ) + { + if ( v == Vec_PtrSize(p->vRings) - 1 ) + continue; + + // preprocess partitions + vRootsNew = Llb_Nonlin4Multiply( p->dd, bState, p->vRoots ); + Cudd_RecursiveDeref( p->dd, bState ); + + // compute the next states + bImage = Llb_Nonlin4Image( p->dd, vRootsNew, NULL, vVars2Q ); Cudd_Ref( bImage ); + Llb_Nonlin4Deref( p->dd, vRootsNew ); + + // 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 ); + + // record the cube + Llb_Nonlin4RecordState( p->pAig, p->vOrder, (unsigned *)Vec_PtrEntry(vStates, v), pValues, fBackward ); + + // check that we get the init state + if ( v == 0 ) + { + Saig_ManForEachLo( p->pAig, pObj, i ) + assert( fBackward || pValues[Llb_ObjBddVar(p->vOrder, pObj)] == 0 ); + break; + } + + // write state in terms of NS variables + bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues, fBackward ); Cudd_Ref( bState ); + } + Vec_IntFree( vVars2Q ); + ABC_FREE( pValues ); + if ( fBackward ) + Vec_PtrReverseOrder( vStates ); +// if ( fVerbose ) +// Abc_PrintTime( 1, "BDD-based cex generation time", clock() - clk ); + return vStates; +} + + +/**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 ); + + if ( p->pPars->fBackward ) + { + // create bad state in the ring manager + if ( !p->pPars->fSkipOutCheck ) + { + p->bBad = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward ); Cudd_Ref( p->bBad ); + } + // create init state + if ( p->pPars->fCluster ) + p->bCurrent = p->dd->bFunc, p->dd->bFunc = NULL; + else + { + p->bCurrent = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder ); + if ( p->bCurrent == 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->bCurrent ); + } + // remap into the next states + p->bCurrent = Cudd_bddVarMap( p->dd, bAux = p->bCurrent ); + if ( p->bCurrent == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during remapping bad states.\n", p->pPars->TimeLimit ); + Cudd_RecursiveDeref( p->dd, bAux ); + p->pPars->iFrame = -1; + return -1; + } + Cudd_Ref( p->bCurrent ); + Cudd_RecursiveDeref( p->dd, bAux ); + } + else + { + // create bad state in the ring manager + if ( !p->pPars->fSkipOutCheck ) + { + if ( p->pPars->fCluster ) + p->bBad = p->dd->bFunc, p->dd->bFunc = NULL; + else + { + 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 ); + } + } + else if ( p->dd->bFunc ) + Cudd_RecursiveDeref( p->dd, p->dd->bFunc ), p->dd->bFunc = NULL; + // compute the starting set of states + p->bCurrent = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward ); Cudd_Ref( p->bCurrent ); + } + // perform iterations + p->bReached = p->bCurrent; Cudd_Ref( p->bReached ); + for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ ) + { + clkIter = clock(); + // check the runtime limit + 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; + 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) ) ) + { + Vec_Ptr_t * vStates; + assert( p->pAig->pSeqModel == NULL ); + vStates = Llb_Nonlin4DeriveCex( p, p->pPars->fBackward, p->pPars->fVerbose ); + p->pAig->pSeqModel = Llb4_Nonlin4TransformCex( p->pAig, vStates, -1, p->pPars->fVerbose ); + Vec_PtrFreeP( &vStates ); + if ( !p->pPars->fSilent ) + { + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pAig->pSeqModel->iPo, 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; +/* + // reduce BDD size using constrain // Cudd_bddRestrict + p->bCurrent = Cudd_bddRestrict( p->dd, bAux = p->bCurrent, Cudd_Not(p->bReached) ); + Cudd_Ref( p->bCurrent ); +printf( "Before = %d. After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurrent) ); + Cudd_RecursiveDeref( p->dd, bAux ); +*/ + + // 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; + + // compute time to stop + p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0; + + if ( pPars->fCluster ) + { +// Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose ); +// Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); + Llb4_Nonlin4Sweep( p->pAig, pPars->nBddMax, pPars->nClusterMax, &p->dd, &p->vOrder, &p->vRoots, pPars->fVerbose ); + // set the stop time parameter + p->dd->TimeStop = p->pPars->TimeTarget; + } + else + { +// p->vOrder = Llb_Nonlin4CreateOrderSimple( pAig ); + p->vOrder = Llb_Nonlin4CreateOrder( pAig ); + p->dd = Cudd_Init( Vec_IntCountPositive(p->vOrder) + 1, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); + Cudd_SetMaxGrowth( p->dd, 1.05 ); + // set the stop time parameter + p->dd->TimeStop = p->pPars->TimeTarget; + p->vRoots = Llb_Nonlin4DerivePartitions( p->dd, pAig, p->vOrder ); + } + + Llb_Nonlin4SetupVarMap( p->dd, pAig, p->vOrder ); + p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, pAig, p->vOrder, p->pPars->fBackward ); + 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 ); + if ( p->vRings ) + Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i ) + Cudd_RecursiveDeref( p->dd, bTemp ); + if ( p->vRoots ) + Vec_PtrForEachEntry( DdNode *, p->vRoots, bTemp, i ) + Cudd_RecursiveDeref( p->dd, bTemp ); + // remove arrays + Vec_PtrFreeP( &p->vRings ); + Vec_PtrFreeP( &p->vRoots ); +//Cudd_PrintInfo( p->dd, stdout ); + Extra_StopManager( p->dd ); + Vec_IntFreeP( &p->vOrder ); + Vec_IntFreeP( &p->vVars2Q ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MnxCheckNextStateVars( Llb_Mnx_t * p ) +{ + Aig_Obj_t * pObj; + int i, Counter0 = 0, Counter1 = 0; + Saig_ManForEachLi( p->pAig, pObj, i ) + if ( Saig_ObjIsLo(p->pAig, Aig_ObjFanin0(pObj)) ) + { + if ( Aig_ObjFaninC0(pObj) ) + Counter0++; + else + Counter1++; + } + printf( "Total = %d. Direct LO = %d. Compl LO = %d.\n", Aig_ManRegNum(p->pAig), Counter1, Counter0 ); +} + +/**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->fCluster && Aig_ManObjNum(pAig) >= (1 << 15) ) + { + printf( "The number of objects is more than 2^15. Clustering cannot be used.\n" ); + return RetValue; + } + { + int clk = clock(); + pMnn = Llb_MnxStart( pAig, pPars ); +//Llb_MnxCheckNextStateVars( pMnn ); + if ( !pPars->fSkipReach ) + RetValue = Llb_Nonlin4Reachability( pMnn ); + pMnn->timeTotal = clock() - clk; + Llb_MnxStop( pMnn ); + } + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |