diff options
Diffstat (limited to 'src/aig/bbr/bbrCex.c')
-rw-r--r-- | src/aig/bbr/bbrCex.c | 184 |
1 files changed, 87 insertions, 97 deletions
diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c index f5981439..be5377af 100644 --- a/src/aig/bbr/bbrCex.c +++ b/src/aig/bbr/bbrCex.c @@ -19,48 +19,21 @@ ***********************************************************************/ #include "bbr.h" +#include "ssw.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Computes the initial state and sets up the variable map.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_ManStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose ) -{ - DdNode ** pbVarsX, ** pbVarsY; - Aig_Obj_t * pLatch; - int i; - - // set the variable mapping for Cudd_bddVarMap() - pbVarsX = ALLOC( DdNode *, dd->size ); - pbVarsY = ALLOC( DdNode *, dd->size ); - Saig_ManForEachLo( p, pLatch, i ) - { - pbVarsY[i] = dd->vars[ Saig_ManPiNum(p) + i ]; - pbVarsX[i] = dd->vars[ Saig_ManCiNum(p) + i ]; - } - Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) ); - FREE( pbVarsX ); - FREE( pbVarsY ); -} - -/**Function************************************************************* - - Synopsis [] + Synopsis [Derives the counter-example using the set of reached states.] Description [] @@ -69,105 +42,122 @@ void Aig_ManStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ -int Aig_ManComputeCountExample( Aig_Man_t * p, DdManager * dd, DdNode ** pbParts, Vec_Ptr_t * vCareSets, int nBddMax, int fVerbose, int fSilent ) +Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, + DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst, + int iOutput, int fVerbose, int fSilent ) { -/* - Bbr_ImageTree_t * pTree = NULL; // Suppress "might be used uninitialized" - DdNode * bCubeCs; - DdNode * bCurrent; - DdNode * bNext = NULL; // Suppress "might be used uninitialized" - DdNode * bTemp; - DdNode ** pbVarsY; + Ssw_Cex_t * pCex; Aig_Obj_t * pObj; - int i, nIters, nBddSize; - int nThreshold = 10000; - int * pCex; + Bbr_ImageTree_t * pTree; + DdNode * bCubeNs, * bState, * bImage; + DdNode * bTemp, * bVar, * bRing; + int i, v, RetValue, nPiOffset; char * pValues; + int clk = clock(); // allocate room for the counter-example - pCex = ALLOC( int, Vec_PtrSize(vCareSets) ); + pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 ); + pCex->iFrame = Vec_PtrSize(vOnionRings); + pCex->iPo = iOutput; + nPiOffset = Saig_ManRegNum(p) + Saig_ManPiNum(p) * Vec_PtrSize(vOnionRings); + + // create the cube of NS variables + bCubeNs = Bbr_bddComputeRangeCube( dd, Saig_ManCiNum(p), Saig_ManCiNum(p)+Saig_ManRegNum(p) ); Cudd_Ref( bCubeNs ); + pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, fVerbose ); + Cudd_RecursiveDeref( dd, bCubeNs ); + if ( pTree == NULL ) + { + if ( !fSilent ) + printf( "BDDs blew up during qualitification scheduling. " ); + return NULL; + } // allocate room for the cube pValues = ALLOC( char, dd->size ); - // collect the NS variables - // set the variable mapping for Cudd_bddVarMap() - pbVarsY = ALLOC( DdNode *, dd->size ); - Aig_ManForEachPi( p, pObj, i ) - pbVarsY[i] = dd->vars[ i ]; + // get the last cube + RetValue = Cudd_bddPickOneCube( dd, bCubeFirst, pValues ); + assert( RetValue ); - // create the initial state and the variable map - Aig_ManStateVarMap( dd, p, fVerbose ); + // write PIs of counter-example + Saig_ManForEachPi( p, pObj, i ) + if ( pValues[i] == 1 ) + Aig_InfoSetBit( pCex->pData, nPiOffset + i ); + nPiOffset -= Saig_ManPiNum(p); - // start the image computation - bCubeCs = Bbr_bddComputeRangeCube( dd, Aig_ManPiNum(p), 2*Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs ); - pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose ); - Cudd_RecursiveDeref( dd, bCubeCs ); - free( pbVarsY ); - if ( pTree == NULL ) + // write state in terms of NS variables + bState = (dd)->one; Cudd_Ref( bState ); + Saig_ManForEachLo( p, pObj, i ) { - if ( !fSilent ) - printf( "BDDs blew up during qualitification scheduling. " ); - return -1; + bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 ); + bState = Cudd_bddAnd( dd, bTemp = bState, bVar ); Cudd_Ref( bState ); + Cudd_RecursiveDeref( dd, bTemp ); } - // create counter-example in terms of next state variables - // pNext = ... - - // perform reachability analisys - Vec_PtrForEachEntryReverse( vCareSets, pCurrent, i ) + // perform backward analysis + Vec_PtrForEachEntryReverse( vOnionRings, bRing, v ) { // compute the next states - bImage = Bbr_bddImageCompute( pTree, bCurrent ); + bImage = Bbr_bddImageCompute( pTree, bState ); if ( bImage == NULL ) { + Cudd_RecursiveDeref( dd, bState ); if ( !fSilent ) printf( "BDDs blew up during image computation. " ); Bbr_bddImageTreeDelete( pTree ); - return -1; + free( pValues ); + return NULL; } Cudd_Ref( bImage ); + Cudd_RecursiveDeref( dd, bState ); // intersect with the previous set - bImage = Cudd_bddAnd( dd, pTemp = bImage, pCurrent ); - Cudd_RecursiveDeref( dd, pTemp ); + bImage = Cudd_bddAnd( dd, bTemp = bImage, bRing ); Cudd_Ref( bImage ); + Cudd_RecursiveDeref( dd, bTemp ); // find any assignment of the BDD RetValue = Cudd_bddPickOneCube( dd, bImage, pValues ); + assert( RetValue ); + Cudd_RecursiveDeref( dd, bImage ); - // transform the assignment into the cube in terms of the next state vars + // write PIs of counter-example + Saig_ManForEachPi( p, pObj, i ) + if ( pValues[i] == 1 ) + Aig_InfoSetBit( pCex->pData, nPiOffset + i ); + nPiOffset -= Saig_ManPiNum(p); - - - // pCurrent = ... - - // save values of the PI variables - - - // check if there are any new states - if ( Cudd_bddLeq( dd, bNext, bReached ) ) - break; - // check the BDD size - nBddSize = Cudd_DagSize(bNext); - if ( nBddSize > nBddMax ) + // check that we get the init state + if ( v == 0 ) + { + Saig_ManForEachLo( p, pObj, i ) + assert( pValues[Saig_ManPiNum(p)+i] == 0 ); break; - // check the result - for ( i = 0; i < Saig_ManPoNum(p); i++ ) + } + + // write state in terms of NS variables + bState = (dd)->one; Cudd_Ref( bState ); + Saig_ManForEachLo( p, pObj, i ) { - if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) ) - { - if ( !fSilent ) - printf( "Output %d was asserted in frame %d. ", i, nIters ); - Cudd_RecursiveDeref( dd, bReached ); - bReached = NULL; - break; - } + bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 ); + bState = Cudd_bddAnd( dd, bTemp = bState, bVar ); Cudd_Ref( bState ); + Cudd_RecursiveDeref( dd, bTemp ); } - if ( i < Saig_ManPoNum(p) ) - break; - // get the new states - bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); -*/ + } + // cleanup + Bbr_bddImageTreeDelete( pTree ); + free( pValues ); + // verify the counter example + if ( Vec_PtrSize(vOnionRings) < 1000 ) + { + RetValue = Ssw_SmlRunCounterExample( p, pCex ); + if ( RetValue == 0 && !fSilent ) + printf( "Aig_ManVerifyUsingBdds(): Counter-example verification has FAILED.\n" ); + } + if ( fVerbose && !fSilent ) + { + PRT( "Counter-example generation time", clock() - clk ); + } + return pCex; } //////////////////////////////////////////////////////////////////////// |