sswBmc.c File Reference

#include "sswInt.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Aig_Obj_t *	Ssw_BmcUnroll_rec (Ssw_Frm_t *pFrm, Aig_Obj_t *pObj, int f)
	DECLARATIONS ///. More...
Abc_Cex_t *	Ssw_BmcGetCounterExample (Ssw_Frm_t *pFrm, Ssw_Sat_t *pSat, int iPo, int iFrame)
int	Ssw_BmcDynamic (Aig_Man_t *pAig, int nFramesMax, int nConfLimit, int fVerbose, int *piFrame)
	MACRO DEFINITIONS ///. More...

Function Documentation

int Ssw_BmcDynamic	(	Aig_Man_t *	pAig,
		int	nFramesMax,
		int	nConfLimit,
		int	fVerbose,
		int *	piFrame
	)

MACRO DEFINITIONS ///.

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

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 126 of file sswBmc.c.

{
    Ssw_Frm_t * pFrm;
    Ssw_Sat_t * pSat;
    Aig_Obj_t * pObj, * pObjFrame;
    int status, Lit, i, f, RetValue;
    abctime clkPart;

    // start managers
    assert( Saig_ManRegNum(pAig) > 0 );
    Aig_ManSetCioIds( pAig );
    pSat = Ssw_SatStart( 0 );
    pFrm = Ssw_FrmStart( pAig );
    pFrm->pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * 3 );
    // report statistics
    if ( fVerbose )
    {
        Abc_Print( 1, "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n",
            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
        fflush( stdout );
    }
    // perform dynamic unrolling
    RetValue = -1;
    for ( f = 0; f < nFramesMax; f++ )
    {
        clkPart = Abc_Clock();
        Saig_ManForEachPo( pAig, pObj, i )
        {
            // unroll the circuit for this output
            Ssw_BmcUnroll_rec( pFrm, pObj, f );
            pObjFrame = Ssw_ObjFrame_( pFrm, pObj, f );
            Ssw_CnfNodeAddToSolver( pSat, Aig_Regular(pObjFrame) );
            status = sat_solver_simplify(pSat->pSat);
            assert( status );
            // solve
            Lit = toLitCond( Ssw_ObjSatNum(pSat,pObjFrame), Aig_IsComplement(pObjFrame) );
            if ( fVerbose )
            {
                Abc_Print( 1, "Solving output %2d of frame %3d ... \r",
                    i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
            }
            status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
            if ( status == l_False )
            {
/*
                Lit = lit_neg( Lit );
                RetValue = sat_solver_addclause( pSat->pSat, &Lit, &Lit + 1 );
                assert( RetValue );
                if ( pSat->pSat->qtail != pSat->pSat->qhead )
                {
                    RetValue = sat_solver_simplify(pSat->pSat);
                    assert( RetValue );
                }
*/
                RetValue = 1;
                continue;
            }
            else if ( status == l_True )
            {
                pAig->pSeqModel = Ssw_BmcGetCounterExample( pFrm, pSat, i, f );
                if ( piFrame )
                    *piFrame = f;
                RetValue = 0;
                break;
            }
            else
            {
                if ( piFrame )
                    *piFrame = f;
                RetValue = -1;
                break;
            }
        }
        if ( fVerbose )
        {
            Abc_Print( 1, "Solved %2d outputs of frame %3d.  ", Saig_ManPoNum(pAig), f );
            Abc_Print( 1, "Conf =%8.0f. Var =%8d. AIG=%9d. ",
                (double)pSat->pSat->stats.conflicts,
                pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) );
            ABC_PRT( "T", Abc_Clock() - clkPart );
            clkPart = Abc_Clock();
            fflush( stdout );
        }
        if ( RetValue != 1 )
            break;
    }

    Ssw_SatStop( pSat );
    Ssw_FrmStop( pFrm );
    return RetValue;
}

Abc_Cex_t* Ssw_BmcGetCounterExample	(	Ssw_Frm_t *	pFrm,
		Ssw_Sat_t *	pSat,
		int	iPo,
		int	iFrame
	)

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

Synopsis [Derives counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file sswBmc.c.

{
    Abc_Cex_t * pCex;
    Aig_Obj_t * pObj, * pObjFrames;
    int f, i, nShift;
    assert( Saig_ManRegNum(pFrm->pAig) > 0 );
    // allocate the counter example
    pCex = Abc_CexAlloc( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 );
    pCex->iPo    = iPo;
    pCex->iFrame = iFrame;
    // create data-bits
    nShift = Saig_ManRegNum(pFrm->pAig);
    for ( f = 0; f <= iFrame; f++, nShift += Saig_ManPiNum(pFrm->pAig) )
        Saig_ManForEachPi( pFrm->pAig, pObj, i )
        {
            pObjFrames = Ssw_ObjFrame_(pFrm, pObj, f);
            if ( pObjFrames == NULL )
                continue;
            if ( Ssw_CnfGetNodeValue( pSat, pObjFrames ) )
                Abc_InfoSetBit( pCex->pData, nShift + i );
        }
    return pCex;
}

ABC_NAMESPACE_IMPL_START Aig_Obj_t* Ssw_BmcUnroll_rec	(	Ssw_Frm_t *	pFrm,
		Aig_Obj_t *	pObj,
		int	f
	)

DECLARATIONS ///.

CFile****************************************************************

FileName [sswBmc.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Bounded model checker using dynamic unrolling.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswBmc.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Incrementally unroll the timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswBmc.c.

{
    Aig_Obj_t * pRes, * pRes0, * pRes1;
    if ( (pRes = Ssw_ObjFrame_(pFrm, pObj, f)) )
        return pRes;
    if ( Aig_ObjIsConst1(pObj) )
        pRes = Aig_ManConst1( pFrm->pFrames );
    else if ( Saig_ObjIsPi(pFrm->pAig, pObj) )
        pRes = Aig_ObjCreateCi( pFrm->pFrames );
    else if ( Aig_ObjIsCo(pObj) )
    {
        Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
        pRes = Ssw_ObjChild0Fra_( pFrm, pObj, f );
    }
    else if ( Saig_ObjIsLo(pFrm->pAig, pObj) )
    {
        if ( f == 0 )
            pRes = Aig_ManConst0( pFrm->pFrames );
        else
            pRes = Ssw_BmcUnroll_rec( pFrm, Saig_ObjLoToLi(pFrm->pAig, pObj), f-1 );
    }
    else
    {
        assert( Aig_ObjIsNode(pObj) );
        Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
        Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin1(pObj), f );
        pRes0 = Ssw_ObjChild0Fra_( pFrm, pObj, f );
        pRes1 = Ssw_ObjChild1Fra_( pFrm, pObj, f );
        pRes = Aig_And( pFrm->pFrames, pRes0, pRes1 );
    }
    Ssw_ObjSetFrame_( pFrm, pObj, f, pRes );
    return pRes;
}