fraBmc.c File Reference

#include "fra.h"

Go to the source code of this file.

Data Structures
struct	Fra_Bmc_t_
	DECLARATIONS ///. More...

Functions
static Aig_Obj_t *	Bmc_ObjFrames (Aig_Obj_t *pObj, int i)
static void	Bmc_ObjSetFrames (Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
static Aig_Obj_t *	Bmc_ObjFraig (Aig_Obj_t *pObj)
static void	Bmc_ObjSetFraig (Aig_Obj_t *pObj, Aig_Obj_t *pNode)
static Aig_Obj_t *	Bmc_ObjChild0Frames (Aig_Obj_t *pObj, int i)
static Aig_Obj_t *	Bmc_ObjChild1Frames (Aig_Obj_t *pObj, int i)
int	Fra_BmcNodesAreEqual (Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
	FUNCTION DEFINITIONS ///. More...
int	Fra_BmcNodeIsConst (Aig_Obj_t *pObj)
void	Fra_BmcFilterImplications (Fra_Man_t *p, Fra_Bmc_t *pBmc)
Fra_Bmc_t *	Fra_BmcStart (Aig_Man_t *pAig, int nPref, int nDepth)
void	Fra_BmcStop (Fra_Bmc_t *p)
Aig_Man_t *	Fra_BmcFrames (Fra_Bmc_t *p, int fKeepPos)
void	Fra_BmcPerform (Fra_Man_t *p, int nPref, int nDepth)
void	Fra_BmcPerformSimple (Aig_Man_t *pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose)

Function Documentation

static Aig_Obj_t* Bmc_ObjChild0Frames ( Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 54 of file fraBmc.c.

{ assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }

static Aig_Obj_t* Bmc_ObjChild1Frames ( Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 55 of file fraBmc.c.

{ assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }

static Aig_Obj_t* Bmc_ObjFraig ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 51 of file fraBmc.c.

{ return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id];  }

static Aig_Obj_t* Bmc_ObjFrames ( Aig_Obj_t *  pObj, int  i  )

inlinestatic

Definition at line 48 of file fraBmc.c.

{ return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i];  }

static void Bmc_ObjSetFraig ( Aig_Obj_t *  pObj, Aig_Obj_t *  pNode  )

inlinestatic

Definition at line 52 of file fraBmc.c.

{ ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id] = pNode; }

static void Bmc_ObjSetFrames ( Aig_Obj_t *  pObj, int  i, Aig_Obj_t *  pNode  )

inlinestatic

Definition at line 49 of file fraBmc.c.

{ ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i] = pNode; }

void Fra_BmcFilterImplications	(	Fra_Man_t *	p,
		Fra_Bmc_t *	pBmc
	)

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

Synopsis [Refines implications using BMC.]

Description [The input is the combinational FRAIG manager, which is used to FRAIG the timeframes. ]

SideEffects []

SeeAlso []

Definition at line 121 of file fraBmc.c.

{
    Aig_Obj_t * pLeft, * pRight;
    Aig_Obj_t * pLeftT, * pRightT;
    Aig_Obj_t * pLeftF, * pRightF;
    int i, f, Imp, Left, Right;
    int fComplL, fComplR;
    assert( p->nFramesAll == 1 );
    assert( p->pManAig == pBmc->pAigFrames );
    Vec_IntForEachEntry( pBmc->vImps, Imp, i )
    {
        if ( Imp == 0 )
            continue;
        Left  = Fra_ImpLeft(Imp);
        Right = Fra_ImpRight(Imp);
        // get the corresponding nodes
        pLeft  = Aig_ManObj( pBmc->pAig, Left );
        pRight = Aig_ManObj( pBmc->pAig, Right );
        // iterate through the timeframes
        for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ )
        {
            // get timeframe nodes
            pLeftT  = Bmc_ObjFrames( pLeft, f );
            pRightT = Bmc_ObjFrames( pRight, f );
            // get the corresponding FRAIG nodes
            pLeftF  = Fra_ObjFraig( Aig_Regular(pLeftT), 0 );
            pRightF = Fra_ObjFraig( Aig_Regular(pRightT), 0 );
            // get the complemented attributes
            fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF) ^ Aig_IsComplement(pLeftT);
            fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF) ^ Aig_IsComplement(pRightT);
            // check equality
            if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
            {
                if ( fComplL == fComplR ) // x => x  - always true
                    continue;
                assert( fComplL != fComplR );
                // consider 4 possibilities:
                // NOT(1) => 1    or   0 => 1  - always true
                // 1 => NOT(1)    or   1 => 0  - never true
                // NOT(x) => x    or   x       - not always true
                // x => NOT(x)    or   NOT(x)  - not always true
                if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
                    continue;
                // disproved implication
                Vec_IntWriteEntry( pBmc->vImps, i, 0 ); 
                break;
            }
            // check the implication 
            if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 )
            {
                Vec_IntWriteEntry( pBmc->vImps, i, 0 );
                break;
            }
        }
    }
    Fra_ImpCompactArray( pBmc->vImps );
}

Aig_Man_t* Fra_BmcFrames	(	Fra_Bmc_t *	p,
		int	fKeepPos
	)

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

Synopsis [Constructs initialized timeframes of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file fraBmc.c.

{
    Aig_Man_t * pAigFrames;
    Aig_Obj_t * pObj, * pObjNew;
    Aig_Obj_t ** pLatches;
    int i, k, f;

    // start the fraig package
    pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll );
    pAigFrames->pName = Abc_UtilStrsav( p->pAig->pName );
    pAigFrames->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
    // create PI nodes for the frames
    for ( f = 0; f < p->nFramesAll; f++ )
        Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) );
    for ( f = 0; f < p->nFramesAll; f++ )
        Aig_ManForEachPiSeq( p->pAig, pObj, i )
            Bmc_ObjSetFrames( pObj, f, Aig_ObjCreateCi(pAigFrames) );
    // set initial state for the latches
    Aig_ManForEachLoSeq( p->pAig, pObj, i )
        Bmc_ObjSetFrames( pObj, 0, Aig_ManConst0(pAigFrames) );

    // add timeframes
    pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
    for ( f = 0; f < p->nFramesAll; f++ )
    {
        // add internal nodes of this frame
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            pObjNew = Aig_And( pAigFrames, Bmc_ObjChild0Frames(pObj,f), Bmc_ObjChild1Frames(pObj,f) );
            Bmc_ObjSetFrames( pObj, f, pObjNew );
        }
        if ( f == p->nFramesAll - 1 )
            break;
        // save the latch input values
        k = 0;
        Aig_ManForEachLiSeq( p->pAig, pObj, i )
            pLatches[k++] = Bmc_ObjChild0Frames(pObj,f);
        assert( k == Aig_ManRegNum(p->pAig) );
        // insert them to the latch output values
        k = 0;
        Aig_ManForEachLoSeq( p->pAig, pObj, i )
            Bmc_ObjSetFrames( pObj, f+1, pLatches[k++] );
        assert( k == Aig_ManRegNum(p->pAig) );
    }
    ABC_FREE( pLatches );
    if ( fKeepPos )
    {
        for ( f = 0; f < p->nFramesAll; f++ )
            Aig_ManForEachPoSeq( p->pAig, pObj, i )
                Aig_ObjCreateCo( pAigFrames, Bmc_ObjChild0Frames(pObj,f) );
        Aig_ManCleanup( pAigFrames );
    }
    else
    {
        // add POs to all the dangling nodes
        Aig_ManForEachObj( pAigFrames, pObjNew, i )
            if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 )
                Aig_ObjCreateCo( pAigFrames, pObjNew );
    }
    // return the new manager
    return pAigFrames;
}

int Fra_BmcNodeIsConst

(

Aig_Obj_t *

pObj

)

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

Synopsis [Returns 1 if the node is costant.]

Description []

SideEffects []

SeeAlso []

Definition at line 103 of file fraBmc.c.

{
    Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
    return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) );
}

int Fra_BmcNodesAreEqual	(	Aig_Obj_t *	pObj0,
		Aig_Obj_t *	pObj1
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Returns 1 if the nodes are equivalent.]

Description []

SideEffects []

SeeAlso []

Definition at line 72 of file fraBmc.c.

{
    Fra_Man_t * p = (Fra_Man_t *)pObj0->pData;
    Aig_Obj_t * pObjFrames0, * pObjFrames1;
    Aig_Obj_t * pObjFraig0, * pObjFraig1;
    int i;
    for ( i = p->pBmc->nPref; i < p->pBmc->nFramesAll; i++ )
    {
        pObjFrames0 = Aig_Regular( Bmc_ObjFrames(pObj0, i) );
        pObjFrames1 = Aig_Regular( Bmc_ObjFrames(pObj1, i) );
        if ( pObjFrames0 == pObjFrames1 )
            continue;
        pObjFraig0 = Aig_Regular( Bmc_ObjFraig(pObjFrames0) );
        pObjFraig1 = Aig_Regular( Bmc_ObjFraig(pObjFrames1) );
        if ( pObjFraig0 != pObjFraig1 )
            return 0;
    }
    return 1;
}

void Fra_BmcPerform	(	Fra_Man_t *	p,
		int	nPref,
		int	nDepth
	)

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

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file fraBmc.c.

{
    Aig_Obj_t * pObj;
    int i, nImpsOld = 0;
    abctime clk = Abc_Clock();
    assert( p->pBmc == NULL );
    // derive and fraig the frames
    p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
    p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc, 0 );
    // if implications are present, configure the AIG manager to check them
    if ( p->pCla->vImps )
    {
        p->pBmc->pAigFrames->pImpFunc = (void (*) (void*, void*))Fra_BmcFilterImplications;
        p->pBmc->pAigFrames->pImpData = p->pBmc;
        p->pBmc->vImps = p->pCla->vImps;
        nImpsOld = Vec_IntSize(p->pCla->vImps);
    } 
    p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000, 0 );
    p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
    p->pBmc->pAigFrames->pObjCopies = NULL;
    // annotate frames nodes with pointers to the manager
    Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i )
        pObj->pData = p;
    // report the results
    if ( p->pPars->fVerbose )
    {
        printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d.  ", 
            Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, 
            Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
        ABC_PRT( "Time", Abc_Clock() - clk );
        printf( "Before BMC: " );  
//        Fra_ClassesPrint( p->pCla, 0 );
        printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
            Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
        if ( p->pCla->vImps )
            printf( "Imp = %5d. ", nImpsOld );
        printf( "\n" );
    }
    // refine the classes
    p->pCla->pFuncNodeIsConst   = Fra_BmcNodeIsConst;
    p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual;
    Fra_ClassesRefine( p->pCla );
    Fra_ClassesRefine1( p->pCla, 1, NULL );
    p->pCla->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
    p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
    // report the results
    if ( p->pPars->fVerbose )
    {
        printf( "After  BMC: " );  
//        Fra_ClassesPrint( p->pCla, 0 );
        printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
            Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
        if ( p->pCla->vImps )
            printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
        printf( "\n" );
    }
    // free the BMC manager
    Fra_BmcStop( p->pBmc );  
    p->pBmc = NULL;
}

void Fra_BmcPerformSimple	(	Aig_Man_t *	pAig,
		int	nFrames,
		int	nBTLimit,
		int	fRewrite,
		int	fVerbose
	)

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

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 383 of file fraBmc.c.

{
    extern Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig );
    Fra_Man_t * pTemp;
    Fra_Bmc_t * pBmc;
    Aig_Man_t * pAigTemp;
    abctime clk;
    int iOutput;
    // derive and fraig the frames
    clk = Abc_Clock();
    pBmc = Fra_BmcStart( pAig, 0, nFrames );
    pTemp = Fra_LcrAigPrepare( pAig );
    pTemp->pBmc = pBmc;
    pBmc->pAigFrames = Fra_BmcFrames( pBmc, 1 );
    if ( fVerbose )
    {
        printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
            Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), Aig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
        printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
            nFrames, Aig_ManCiNum(pBmc->pAigFrames), Aig_ManCoNum(pBmc->pAigFrames), 
            Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    if ( fRewrite )
    {
        clk = Abc_Clock();
        pBmc->pAigFrames = Dar_ManRwsat( pAigTemp = pBmc->pAigFrames, 1, 0 );
        Aig_ManStop( pAigTemp );
        if ( fVerbose )
        {
            printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
                Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
            ABC_PRT( "Time", Abc_Clock() - clk );
        }
    }
    clk = Abc_Clock();
    iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
    if ( iOutput >= 0 )
        pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
    else
    {
        pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 );
        iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFraig );
        if ( pBmc->pAigFraig->pData )
        {
            pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, (int *)pBmc->pAigFraig->pData );
            ABC_FREE( pBmc->pAigFraig->pData );
        }
        else if ( iOutput >= 0 )
            pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
    }
    if ( fVerbose )
    {
        printf( "Fraiged init frames: Node = %6d. Lev = %5d.  ", 
            pBmc->pAigFraig? Aig_ManNodeNum(pBmc->pAigFraig) : -1,
            pBmc->pAigFraig? Aig_ManLevelNum(pBmc->pAigFraig) : -1 );
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    Fra_BmcStop( pBmc );  
    ABC_FREE( pTemp );
}

Fra_Bmc_t* Fra_BmcStart	(	Aig_Man_t *	pAig,
		int	nPref,
		int	nDepth
	)

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

Synopsis [Starts the BMC manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 191 of file fraBmc.c.

{
    Fra_Bmc_t * p;
    p = ABC_ALLOC( Fra_Bmc_t, 1 );
    memset( p, 0, sizeof(Fra_Bmc_t) );
    p->pAig = pAig;
    p->nPref = nPref;
    p->nDepth = nDepth;
    p->nFramesAll = nPref + nDepth;
    p->pObjToFrames  = ABC_ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) );
    memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * Aig_ManObjNumMax(pAig) );
    return p;
}

void Fra_BmcStop

(

Fra_Bmc_t *

p

)

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

Synopsis [Stops the BMC manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 216 of file fraBmc.c.

{
    Aig_ManStop( p->pAigFrames );
    if ( p->pAigFraig )
        Aig_ManStop( p->pAigFraig );
    ABC_FREE( p->pObjToFrames );
    ABC_FREE( p->pObjToFraig );
    ABC_FREE( p );
}