diff options
Diffstat (limited to 'src/proof/bbr/bbrReach.c')
| -rw-r--r-- | src/proof/bbr/bbrReach.c | 615 |
1 files changed, 0 insertions, 615 deletions
diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c deleted file mode 100644 index b5125ec7..00000000 --- a/src/proof/bbr/bbrReach.c +++ /dev/null @@ -1,615 +0,0 @@ -/**CFile**************************************************************** - - FileName [bbrReach.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [BDD-based reachability analysis.] - - Synopsis [Procedures to perform reachability analysis.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: bbrReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "bbr.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -extern Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, - DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst, - int iOutput, int fVerbose, int fSilent ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [This procedure sets default resynthesis parameters.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bbr_ManSetDefaultParams( Saig_ParBbr_t * p ) -{ - memset( p, 0, sizeof(Saig_ParBbr_t) ); - p->TimeLimit = 0; - p->nBddMax = 50000; - p->nIterMax = 1000; - p->fPartition = 1; - p->fReorder = 1; - p->fReorderImage = 1; - p->fVerbose = 0; - p->fSilent = 0; - p->iFrame = -1; -} - -/**Function******************************************************************** - - Synopsis [Performs the reordering-sensitive step of Extra_bddMove().] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ) -{ - DdNode * bTemp, * bProd; - int i; - assert( iStart <= iStop ); - assert( iStart >= 0 && iStart <= dd->size ); - assert( iStop >= 0 && iStop <= dd->size ); - bProd = (dd)->one; Cudd_Ref( bProd ); - for ( i = iStart; i < iStop; i++ ) - { - bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] ); Cudd_Ref( bProd ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_Deref( bProd ); - return bProd; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bbr_StopManager( DdManager * dd ) -{ - int RetValue; - // check for remaining references in the package - RetValue = Cudd_CheckZeroRef( dd ); - if ( RetValue > 0 ) - printf( "\nThe number of referenced nodes = %d\n\n", RetValue ); -// Cudd_PrintInfo( dd, stdout ); - Cudd_Quit( dd ); -} - -/**Function************************************************************* - - Synopsis [Computes the initial state and sets up the variable map.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Aig_ManInitStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose ) -{ - DdNode ** pbVarsX, ** pbVarsY; - DdNode * bTemp, * bProd; - Aig_Obj_t * pLatch; - int i; - - // set the variable mapping for Cudd_bddVarMap() - pbVarsX = ABC_ALLOC( DdNode *, dd->size ); - pbVarsY = ABC_ALLOC( DdNode *, dd->size ); - bProd = (dd)->one; Cudd_Ref( bProd ); - Saig_ManForEachLo( p, pLatch, i ) - { - pbVarsX[i] = dd->vars[ Saig_ManPiNum(p) + i ]; - pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ]; - // get the initial value of the latch - bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_Not(pbVarsX[i]) ); Cudd_Ref( bProd ); - Cudd_RecursiveDeref( dd, bTemp ); - } - Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) ); - ABC_FREE( pbVarsX ); - ABC_FREE( pbVarsY ); - - Cudd_Deref( bProd ); - return bProd; -} - -/**Function************************************************************* - - Synopsis [Collects the array of output BDDs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode ** Aig_ManCreateOutputs( DdManager * dd, Aig_Man_t * p ) -{ - DdNode ** pbOutputs; - Aig_Obj_t * pNode; - int i; - // compute the transition relation - pbOutputs = ABC_ALLOC( DdNode *, Saig_ManPoNum(p) ); - Saig_ManForEachPo( p, pNode, i ) - { - pbOutputs[i] = Aig_ObjGlobalBdd(pNode); Cudd_Ref( pbOutputs[i] ); - } - return pbOutputs; -} - -/**Function************************************************************* - - Synopsis [Collects the array of partition BDDs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder, int fVerbose ) -{ - DdNode ** pbParts; - DdNode * bVar; - Aig_Obj_t * pNode; - int i; - - // extand the BDD manager to represent NS variables - assert( dd->size == Saig_ManCiNum(p) ); - Cudd_bddIthVar( dd, Saig_ManCiNum(p) + Saig_ManRegNum(p) - 1 ); - - // enable reordering - if ( fReorder ) - Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); - else - Cudd_AutodynDisable( dd ); - - // compute the transition relation - pbParts = ABC_ALLOC( DdNode *, Saig_ManRegNum(p) ); - Saig_ManForEachLi( p, pNode, i ) - { - bVar = Cudd_bddIthVar( dd, Saig_ManCiNum(p) + i ); - pbParts[i] = Cudd_bddXnor( dd, bVar, Aig_ObjGlobalBdd(pNode) ); Cudd_Ref( pbParts[i] ); - } - // free global BDDs - Aig_ManFreeGlobalBdds( p, dd ); - - // reorder and disable reordering - if ( fReorder ) - { - if ( fVerbose ) - fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) ); - Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); - Cudd_AutodynDisable( dd ); - if ( fVerbose ) - fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) ); - } - return pbParts; -} - -/**Function************************************************************* - - Synopsis [Computes the set of unreachable states.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, Saig_ParBbr_t * pPars, int fCheckOutputs ) -{ - int fInternalReorder = 0; - Bbr_ImageTree_t * pTree = NULL; // Suppress "might be used uninitialized" - Bbr_ImageTree2_t * pTree2 = NULL; // Supprses "might be used uninitialized" - DdNode * bReached, * bCubeCs; - DdNode * bCurrent; - DdNode * bNext = NULL; // Suppress "might be used uninitialized" - DdNode * bTemp; - Cudd_ReorderingType method; - int i, nIters, nBddSize = 0, status; - int nThreshold = 10000; - abctime clk = Abc_Clock(); - Vec_Ptr_t * vOnionRings; - int fixedPoint = 0; - - status = Cudd_ReorderingStatus( dd, &method ); - if ( status ) - Cudd_AutodynDisable( dd ); - - // start the image computation - bCubeCs = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs ); - if ( pPars->fPartition ) - pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->nBddMax, pPars->fVerbose ); - else - pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->fVerbose ); - Cudd_RecursiveDeref( dd, bCubeCs ); - if ( pTree == NULL ) - { - if ( !pPars->fSilent ) - printf( "BDDs blew up during qualitification scheduling. " ); - return -1; - } - - if ( status ) - Cudd_AutodynEnable( dd, method ); - - // start the onion rings - vOnionRings = Vec_PtrAlloc( 1000 ); - - // perform reachability analysis - bCurrent = bInitial; Cudd_Ref( bCurrent ); - bReached = bInitial; Cudd_Ref( bReached ); - Vec_PtrPush( vOnionRings, bCurrent ); Cudd_Ref( bCurrent ); - for ( nIters = 0; nIters < pPars->nIterMax; nIters++ ) - { - // check the runtime limit - if ( pPars->TimeLimit && pPars->TimeLimit <= (Abc_Clock()-clk)/CLOCKS_PER_SEC ) - { - printf( "Reached timeout after image computation (%d seconds).\n", pPars->TimeLimit ); - Vec_PtrFree( vOnionRings ); - // undo the image tree - if ( pPars->fPartition ) - Bbr_bddImageTreeDelete( pTree ); - else - Bbr_bddImageTreeDelete2( pTree2 ); - pPars->iFrame = nIters - 1; - return -1; - } - - // compute the next states - if ( pPars->fPartition ) - bNext = Bbr_bddImageCompute( pTree, bCurrent ); - else - bNext = Bbr_bddImageCompute2( pTree2, bCurrent ); - if ( bNext == NULL ) - { - if ( !pPars->fSilent ) - printf( "BDDs blew up during image computation. " ); - if ( pPars->fPartition ) - Bbr_bddImageTreeDelete( pTree ); - else - Bbr_bddImageTreeDelete2( pTree2 ); - Vec_PtrFree( vOnionRings ); - pPars->iFrame = nIters - 1; - return -1; - } - Cudd_Ref( bNext ); - Cudd_RecursiveDeref( dd, bCurrent ); - - // remap these states into the current state vars - bNext = Cudd_bddVarMap( dd, bTemp = bNext ); Cudd_Ref( bNext ); - Cudd_RecursiveDeref( dd, bTemp ); - // check if there are any new states - if ( Cudd_bddLeq( dd, bNext, bReached ) ) { - fixedPoint = 1; - break; - } - // check the BDD size - nBddSize = Cudd_DagSize(bNext); - if ( nBddSize > pPars->nBddMax ) - break; - // check the result - for ( i = 0; i < Saig_ManPoNum(p); i++ ) - { - if ( fCheckOutputs && !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) ) - { - DdNode * bIntersect; - bIntersect = Cudd_bddIntersect( dd, bNext, pbOutputs[i] ); Cudd_Ref( bIntersect ); - assert( p->pSeqModel == NULL ); - p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, - vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); - Cudd_RecursiveDeref( dd, bIntersect ); - if ( !pPars->fSilent ) - Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", i, p->pName, Vec_PtrSize(vOnionRings) ); - Cudd_RecursiveDeref( dd, bReached ); - bReached = NULL; - pPars->iFrame = nIters; - break; - } - } - if ( i < Saig_ManPoNum(p) ) - break; - // get the new states - bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); - Vec_PtrPush( vOnionRings, bCurrent ); Cudd_Ref( bCurrent ); - // minimize the new states with the reached states -// bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); -// Cudd_RecursiveDeref( dd, bTemp ); - // add to the reached states - bReached = Cudd_bddOr( dd, bTemp = bReached, bNext ); Cudd_Ref( bReached ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bNext ); - if ( pPars->fVerbose ) - fprintf( stdout, "Frame = %3d. BDD = %5d. ", nIters, nBddSize ); - if ( fInternalReorder && pPars->fReorder && nBddSize > nThreshold ) - { - if ( pPars->fVerbose ) - fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) ); - Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); - Cudd_AutodynDisable( dd ); - if ( pPars->fVerbose ) - fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) ); - nThreshold *= 2; - } - if ( pPars->fVerbose ) -// fprintf( stdout, "\r" ); - fprintf( stdout, "\n" ); - - if ( pPars->fVerbose ) - { - double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) ); -// Extra_bddPrint( dd, bReached );printf( "\n" ); - fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) ); - fflush( stdout ); - } - - } - Cudd_RecursiveDeref( dd, bNext ); - // free the onion rings - Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i ) - Cudd_RecursiveDeref( dd, bTemp ); - Vec_PtrFree( vOnionRings ); - // undo the image tree - if ( pPars->fPartition ) - Bbr_bddImageTreeDelete( pTree ); - else - Bbr_bddImageTreeDelete2( pTree2 ); - if ( bReached == NULL ) - return 0; // proved reachable - // report the stats - if ( pPars->fVerbose ) - { - double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) ); - if ( nIters > pPars->nIterMax || nBddSize > 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)) ); - fflush( stdout ); - } -//ABC_PRB( dd, bReached ); - Cudd_RecursiveDeref( dd, bReached ); - // SPG - // - if ( fixedPoint ) { - if ( !pPars->fSilent ) { - printf( "The miter is proved unreachable after %d iterations. ", nIters ); - } - pPars->iFrame = nIters - 1; - return 1; - } - assert(nIters >= pPars->nIterMax || nBddSize >= pPars->nBddMax); - if ( !pPars->fSilent ) - printf( "Verified only for states reachable in %d frames. ", nIters ); - pPars->iFrame = nIters - 1; - return -1; // undecided -} - -/**Function************************************************************* - - Synopsis [Performs reachability to see if any PO can be asserted.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars ) -{ - int fCheckOutputs = !pPars->fSkipOutCheck; - DdManager * dd; - DdNode ** pbParts, ** pbOutputs; - DdNode * bInitial, * bTemp; - int RetValue, i; - abctime clk = Abc_Clock(); - Vec_Ptr_t * vOnionRings; - - assert( Saig_ManRegNum(p) > 0 ); - - // compute the global BDDs of the latches - dd = Aig_ManComputeGlobalBdds( p, pPars->nBddMax, 1, pPars->fReorder, pPars->fVerbose ); - if ( dd == NULL ) - { - if ( !pPars->fSilent ) - printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", pPars->nBddMax ); - return -1; - } - if ( pPars->fVerbose ) - printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); - - // check the runtime limit - if ( pPars->TimeLimit && pPars->TimeLimit <= (Abc_Clock()-clk)/CLOCKS_PER_SEC ) - { - printf( "Reached timeout after constructing global BDDs (%d seconds).\n", pPars->TimeLimit ); - Cudd_Quit( dd ); - return -1; - } - - // start the onion rings - vOnionRings = Vec_PtrAlloc( 1000 ); - - // save outputs - pbOutputs = Aig_ManCreateOutputs( dd, p ); - - // create partitions - pbParts = Aig_ManCreatePartitions( dd, p, pPars->fReorder, pPars->fVerbose ); - - // create the initial state and the variable map - bInitial = Aig_ManInitStateVarMap( dd, p, pPars->fVerbose ); Cudd_Ref( bInitial ); - - // set reordering - if ( pPars->fReorderImage ) - Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); - - // check the result - RetValue = -1; - for ( i = 0; i < Saig_ManPoNum(p); i++ ) - { - if ( fCheckOutputs && !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) ) - { - DdNode * bIntersect; - bIntersect = Cudd_bddIntersect( dd, bInitial, pbOutputs[i] ); Cudd_Ref( bIntersect ); - assert( p->pSeqModel == NULL ); - p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, - vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); - Cudd_RecursiveDeref( dd, bIntersect ); - if ( !pPars->fSilent ) - Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", i, p->pName, -1 ); - RetValue = 0; - break; - } - } - // free the onion rings - Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i ) - Cudd_RecursiveDeref( dd, bTemp ); - Vec_PtrFree( vOnionRings ); - // explore reachable states - if ( RetValue == -1 ) - RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, pPars, fCheckOutputs ); - - // cleanup - Cudd_RecursiveDeref( dd, bInitial ); - for ( i = 0; i < Saig_ManRegNum(p); i++ ) - Cudd_RecursiveDeref( dd, pbParts[i] ); - ABC_FREE( pbParts ); - for ( i = 0; i < Saig_ManPoNum(p); i++ ) - Cudd_RecursiveDeref( dd, pbOutputs[i] ); - ABC_FREE( pbOutputs ); -// if ( RetValue == -1 ) - Cudd_Quit( dd ); -// else -// Bbr_StopManager( dd ); - - // report the runtime - if ( !pPars->fSilent ) - { - ABC_PRT( "Time", Abc_Clock() - clk ); - fflush( stdout ); - } - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Performs reachability to see if any PO can be asserted.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars ) -{ - Abc_Cex_t * pCexOld, * pCexNew; - Aig_Man_t * p; - Aig_Obj_t * pObj; - Vec_Int_t * vInputMap; - int i, k, Entry, iBitOld, iBitNew, RetValue; -// pPars->fVerbose = 1; - // check if there are PIs without fanout - Saig_ManForEachPi( pInit, pObj, i ) - if ( Aig_ObjRefs(pObj) == 0 ) - break; - if ( i == Saig_ManPiNum(pInit) ) - return Aig_ManVerifyUsingBdds_int( pInit, pPars ); - // create new AIG - p = Aig_ManDupTrim( pInit ); - assert( Aig_ManCiNum(p) < Aig_ManCiNum(pInit) ); - assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) ); - RetValue = Aig_ManVerifyUsingBdds_int( p, pPars ); - if ( RetValue != 0 ) - { - Aig_ManStop( p ); - return RetValue; - } - // the problem is satisfiable - remap the pattern - pCexOld = p->pSeqModel; - assert( pCexOld != NULL ); - // create input map - vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) ); - Saig_ManForEachPi( pInit, pObj, i ) - if ( pObj->pData != NULL ) - Vec_IntPush( vInputMap, Aig_ObjCioId((Aig_Obj_t *)pObj->pData) ); - else - Vec_IntPush( vInputMap, -1 ); - // create new pattern - pCexNew = Abc_CexAlloc( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 ); - pCexNew->iFrame = pCexOld->iFrame; - pCexNew->iPo = pCexOld->iPo; - // copy the bit-data - for ( iBitOld = 0; iBitOld < pCexOld->nRegs; iBitOld++ ) - if ( Abc_InfoHasBit( pCexOld->pData, iBitOld ) ) - Abc_InfoSetBit( pCexNew->pData, iBitOld ); - // copy the primary input data - iBitNew = iBitOld; - for ( i = 0; i <= pCexNew->iFrame; i++ ) - { - Vec_IntForEachEntry( vInputMap, Entry, k ) - { - if ( Entry == -1 ) - continue; - if ( Abc_InfoHasBit( pCexOld->pData, iBitOld + Entry ) ) - Abc_InfoSetBit( pCexNew->pData, iBitNew + k ); - } - iBitOld += Saig_ManPiNum(p); - iBitNew += Saig_ManPiNum(pInit); - } - assert( iBitOld < iBitNew ); - assert( iBitOld == pCexOld->nBits ); - assert( iBitNew == pCexNew->nBits ); - Vec_IntFree( vInputMap ); - pInit->pSeqModel = pCexNew; - Aig_ManStop( p ); - return 0; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |