bbrCex.c File Reference

#include "bbr.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START DdNode *	Bbr_bddComputeRangeCube (DdManager *dd, int iStart, int iStop)
	DECLARATIONS ///. More...
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 ///. More...

Function Documentation

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 ///.

DECLARATIONS ///.

Function*************************************************************

Synopsis [Derives the counter-example using the set of reached states.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file bbrCex.c.

{
    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;
    abctime clk = Abc_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 )
            Abc_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 )
                Abc_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", Abc_Clock() - clk );
    }
    return pCex;
}

ABC_NAMESPACE_IMPL_START DdNode* Bbr_bddComputeRangeCube	(	DdManager *	dd,
		int	iStart,
		int	iStop
	)

DECLARATIONS ///.

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

]

Function********************************************************************

Synopsis [Performs the reordering-sensitive step of Extra_bddMove().]

Description []

SideEffects []

SeeAlso []

Definition at line 74 of file bbrReach.c.

{
    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;
}