diff options
Diffstat (limited to 'src/aig/bbr/bbrCex.c')
| -rw-r--r-- | src/aig/bbr/bbrCex.c | 172 |
1 files changed, 0 insertions, 172 deletions
diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c deleted file mode 100644 index 4a1a1d67..00000000 --- a/src/aig/bbr/bbrCex.c +++ /dev/null @@ -1,172 +0,0 @@ -/**CFile**************************************************************** - - FileName [bbrCex.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [BDD-based reachability analysis.] - - Synopsis [Procedures to derive a satisfiable counter-example.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: bbrCex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "bbr.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -extern DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Derives the counter-example using the set of reached states.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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 ) -{ - Abc_Cex_t * pCex; - Aig_Obj_t * pObj; - Bbr_ImageTree_t * pTree; - DdNode * bCubeNs, * bState, * bImage; - DdNode * bTemp, * bVar, * bRing; - int i, v, RetValue, nPiOffset; - char * pValues; - int clk = clock(); -//printf( "\nDeriving counter-example.\n" ); - - // allocate room for the counter-example - pCex = Abc_CexAlloc( 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, 100000000, 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 = ABC_ALLOC( char, dd->size ); - - // get the last cube - RetValue = Cudd_bddPickOneCube( dd, bCubeFirst, pValues ); - assert( RetValue ); - - // write PIs of counter-example - Saig_ManForEachPi( p, pObj, i ) - if ( pValues[i] == 1 ) - Aig_InfoSetBit( pCex->pData, nPiOffset + i ); - nPiOffset -= Saig_ManPiNum(p); - - // write state in terms of NS variables - bState = (dd)->one; Cudd_Ref( bState ); - Saig_ManForEachLo( p, pObj, i ) - { - 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 ); - } - - // perform backward analysis - Vec_PtrForEachEntryReverse( DdNode *, vOnionRings, bRing, v ) - { - // compute the next states - bImage = Bbr_bddImageCompute( pTree, bState ); - if ( bImage == NULL ) - { - Cudd_RecursiveDeref( dd, bState ); - if ( !fSilent ) - printf( "BDDs blew up during image computation. " ); - Bbr_bddImageTreeDelete( pTree ); - ABC_FREE( pValues ); - return NULL; - } - Cudd_Ref( bImage ); - Cudd_RecursiveDeref( dd, bState ); - - // intersect with the previous set - 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 ); - - // write PIs of counter-example - Saig_ManForEachPi( p, pObj, i ) - if ( pValues[i] == 1 ) - Aig_InfoSetBit( pCex->pData, nPiOffset + i ); - nPiOffset -= Saig_ManPiNum(p); - - // check that we get the init state - if ( v == 0 ) - { - Saig_ManForEachLo( p, pObj, i ) - assert( pValues[Saig_ManPiNum(p)+i] == 0 ); - break; - } - - // write state in terms of NS variables - bState = (dd)->one; Cudd_Ref( bState ); - Saig_ManForEachLo( p, pObj, i ) - { - 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 ); - } - } - // cleanup - Bbr_bddImageTreeDelete( pTree ); - ABC_FREE( pValues ); - // verify the counter example - if ( Vec_PtrSize(vOnionRings) < 1000 ) - { - RetValue = Saig_ManVerifyCex( p, pCex ); - if ( RetValue == 0 && !fSilent ) - printf( "Aig_ManVerifyUsingBdds(): Counter-example verification has FAILED.\n" ); - } - if ( fVerbose && !fSilent ) - { - ABC_PRT( "Counter-example generation time", clock() - clk ); - } - return pCex; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |