diff options
Diffstat (limited to 'src/proof/bbr/bbrReach.c')
| -rw-r--r-- | src/proof/bbr/bbrReach.c | 606 |
1 files changed, 606 insertions, 0 deletions
diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c new file mode 100644 index 00000000..1b5c3984 --- /dev/null +++ b/src/proof/bbr/bbrReach.c @@ -0,0 +1,606 @@ +/**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, clk = clock(); + Vec_Ptr_t * vOnionRings; + + 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 && ((float)pPars->TimeLimit <= (float)(clock()-clk)/(float)(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 ) ) + 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 ) + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", i, 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 ); + if ( nIters > pPars->nIterMax || nBddSize > pPars->nBddMax ) + { + if ( !pPars->fSilent ) + printf( "Verified only for states reachable in %d frames. ", nIters ); + return -1; // undecided + } + if ( !pPars->fSilent ) + printf( "The miter is proved unreachable after %d iterations. ", nIters ); + pPars->iFrame = nIters - 1; + return 1; // unreachable +} + +/**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, clk = 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 && ((float)pPars->TimeLimit <= (float)(clock()-clk)/(float)(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 ) + printf( "The miter output %d is proved REACHABLE in the initial state (use \"write_counter\" to dump a witness). ", i ); + 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", 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_ManPiNum(p) < Aig_ManPiNum(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_ObjPioNum((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 + |