bmcInse.c File Reference

#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "aig/gia/giaAig.h"

Include dependency graph for bmcInse.c:

Go to the source code of this file.

Functions
void	Gia_ManInseInit (Gia_Man_t *p, Vec_Int_t *vInit)
	FUNCTION DEFINITIONS ///.
void	Gia_ManInseSimulateObj (Gia_Man_t *p, int Id)
int	Gia_ManInseHighestScore (Gia_Man_t *p, int *pCost)
void	Gia_ManInseFindStarting (Gia_Man_t *p, int iPat, Vec_Int_t *vInit, Vec_Int_t *vInputs)
Vec_Int_t *	Gia_ManInseSimulate (Gia_Man_t *p, Vec_Int_t *vInit0, Vec_Int_t *vInputs, Vec_Int_t *vInit)
Vec_Int_t *	Gia_ManInsePerform (Gia_Man_t *p, Vec_Int_t *vInit0, int nFrames, int nWords, int fVerbose)
Vec_Int_t *	Gia_ManInseTest (Gia_Man_t *p, Vec_Int_t *vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose)

Function Documentation

Gia_ManInseFindStarting()

void Gia_ManInseFindStarting	(	Gia_Man_t *	p,
		int	iPat,
		Vec_Int_t *	vInit,
		Vec_Int_t *	vInputs )

Definition at line 198 of file bmcInse.c.

{
    Gia_Obj_t * pObj;
    word * pData0, * pData1;
    int i, k;
    Vec_IntClear( vInit );
    Gia_ManForEachRi( p, pObj, k )
    {
        pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
        pData1 = pData0 + p->iData;
        for ( i = 0; i < p->iData; i++ )
            assert( (pData0[i] & pData1[i]) == 0 );
        if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) )
            Vec_IntPush( vInit, 0 );
        else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) )
            Vec_IntPush( vInit, 1 );
        else 
            Vec_IntPush( vInit, 2 );
    }
    Gia_ManForEachPi( p, pObj, k )
    {
        pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
        pData1 = pData0 + p->iData;
        for ( i = 0; i < p->iData; i++ )
            assert( (pData0[i] & pData1[i]) == 0 );
        if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) )
            Vec_IntPush( vInputs, 0 );
        else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) )
            Vec_IntPush( vInputs, 1 );
        else 
            Vec_IntPush( vInputs, 2 );
    }
}

Here is the caller graph for this function:

Gia_ManInseHighestScore()

int Gia_ManInseHighestScore	(	Gia_Man_t *	p,
		int *	pCost )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file bmcInse.c.

{
    Gia_Obj_t * pObj;
    word * pData0, * pData1;
    int * pCounts, CountBest;
    int i, k, b, nPats, iPat;
    nPats = 64 * p->iData;
    pCounts = ABC_CALLOC( int, nPats );
    Gia_ManForEachRi( p, pObj, k )
    {
        pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
        pData1 = pData0 + p->iData;
        for ( i = 0; i < p->iData; i++ )
            for ( b = 0; b < 64; b++ )
                pCounts[64*i+b] += (((pData0[i] >> b) & 1) || ((pData1[i] >> b) & 1)); // binary
    }
    iPat = 0;
    CountBest = pCounts[0]; 
    for ( k = 1; k < nPats; k++ )
        if ( CountBest < pCounts[k] )
            CountBest = pCounts[k], iPat = k;
    *pCost = Gia_ManRegNum(p) - CountBest; // ternary
    ABC_FREE( pCounts );
    return iPat;
}

Here is the caller graph for this function:

Gia_ManInseInit()

void Gia_ManInseInit	(	Gia_Man_t *	p,
		Vec_Int_t *	vInit )

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file bmcInse.c.

{
    Gia_Obj_t * pObj;
    word * pData1, * pData0;
    int i, k;
    Gia_ManForEachRi( p, pObj, k )
    {
        pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
        pData1 = pData0 + p->iData;
        if ( Vec_IntEntry(vInit, k) == 0 ) // 0
            for ( i = 0; i < p->iData; i++ )
                pData0[i] = ~(word)0, pData1[i] = 0;
        else if ( Vec_IntEntry(vInit, k) == 1 ) // 1
            for ( i = 0; i < p->iData; i++ )
                pData0[i] = 0, pData1[i] = ~(word)0;
        else // if ( Vec_IntEntry(vInit, k) > 1 ) // X
            for ( i = 0; i < p->iData; i++ )
                pData0[i] = pData1[i] = 0;
    }
}

Here is the caller graph for this function:

Gia_ManInsePerform()

Vec_Int_t * Gia_ManInsePerform	(	Gia_Man_t *	p,
		Vec_Int_t *	vInit0,
		int	nFrames,
		int	nWords,
		int	fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 277 of file bmcInse.c.

{
    Vec_Int_t * vRes, * vInit, * vInputs;
    Gia_Obj_t * pObj;
    int i, f, iPat, Cost, Cost0;
    abctime clk, clkTotal = Abc_Clock();
    Gia_ManRandomW( 1 );
    if ( fVerbose )
        printf( "Running with %d frames, %d words, and %sgiven init state.\n", nFrames, nWords, vInit0 ? "":"no " );
    vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 );
    vInputs = Vec_IntStart( Gia_ManPiNum(p) * nFrames );
    Gia_ParTestAlloc( p, nWords );
    Gia_ManInseInit( p, vInit );
    Cost0 = 0;
    Vec_IntForEachEntry( vInit, iPat, i )
        Cost0 += ((iPat >> 1) & 1);
    if ( fVerbose )
        printf( "Frame =%6d : Values =%6d (out of %6d)\n", 0, Cost0, Cost0 );
    for ( f = 0; f < nFrames; f++ )
    {
        clk = Abc_Clock();
        Gia_ManForEachObj( p, pObj, i )
            Gia_ManInseSimulateObj( p, i );
        iPat = Gia_ManInseHighestScore( p, &Cost );
        Gia_ManInseFindStarting( p, iPat, vInit, vInputs );
        Gia_ManInseInit( p, vInit );
        if ( fVerbose )
            printf( "Frame =%6d : Values =%6d (out of %6d)   ", f+1, Cost, Cost0 );
        if ( fVerbose )
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    Gia_ParTestFree( p );
    vRes = Gia_ManInseSimulate( p, vInit0, vInputs, vInit );
    Vec_IntFreeP( &vInit );
    Vec_IntFreeP( &vInputs );
    printf( "After %d frames, found a sequence to produce %d x-values (out of %d).  ", f, Cost, Gia_ManRegNum(p) );
    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
    return vRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManInseSimulate()

Vec_Int_t * Gia_ManInseSimulate	(	Gia_Man_t *	p,
		Vec_Int_t *	vInit0,
		Vec_Int_t *	vInputs,
		Vec_Int_t *	vInit )

Definition at line 231 of file bmcInse.c.

{
    Vec_Int_t * vRes;
    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
    int nFrames = Vec_IntSize(vInputs) / Gia_ManPiNum(p);
    int i, f, iBit = 0;
    assert( Vec_IntSize(vInputs) % Gia_ManPiNum(p) == 0 );
    assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) );
    assert( Vec_IntSize(vInit) == Gia_ManRegNum(p) );
    Gia_ManConst0(p)->fMark0 = 0;
    Gia_ManForEachRi( p, pObj, i )
        pObj->fMark0 = Vec_IntEntry(vInit0, i);
    for ( f = 0; f < nFrames; f++ )
    {
        Gia_ManForEachPi( p, pObj, i )
            pObj->fMark0 = Vec_IntEntry(vInputs, iBit++);
        Gia_ManForEachAnd( p, pObj, i )
            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
        Gia_ManForEachRi( p, pObj, i )
            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
        Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
            pObjRo->fMark0 = pObjRi->fMark0;
    }
    assert( iBit == Vec_IntSize(vInputs) );
    vRes = Vec_IntAlloc( Gia_ManRegNum(p) );
    Gia_ManForEachRo( p, pObj, i )
        assert( Vec_IntEntry(vInit, i) == 2 || Vec_IntEntry(vInit, i) == (int)pObj->fMark0 );
    Gia_ManForEachRo( p, pObj, i )
        Vec_IntPush( vRes, pObj->fMark0 | (Vec_IntEntry(vInit, i) != 2 ? 4 : 0) );
    Gia_ManForEachObj( p, pObj, i )
        pObj->fMark0 = 0;
    return vRes;
}

Here is the caller graph for this function:

Gia_ManInseSimulateObj()

void Gia_ManInseSimulateObj	(	Gia_Man_t *	p,
		int	Id )

Definition at line 72 of file bmcInse.c.

{
    Gia_Obj_t * pObj = Gia_ManObj( p, Id );
    word * pData0, * pDataA0, * pDataB0;
    word * pData1, * pDataA1, * pDataB1;
    int i;
    if ( Gia_ObjIsAnd(pObj) )
    {
        pData0  = Gia_ParTestObj( p, Id );
        pData1  = pData0 + p->iData;
        if ( Gia_ObjFaninC0(pObj) )
        {
            pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
            pDataA0 = pDataA1 + p->iData;
            if ( Gia_ObjFaninC1(pObj) )
            {
                pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
                pDataB0 = pDataB1 + p->iData;
            }
            else 
            {
                pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
                pDataB1 = pDataB0 + p->iData;
            }
        }
        else 
        {
            pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
            pDataA1 = pDataA0 + p->iData;
            if ( Gia_ObjFaninC1(pObj) )
            {
                pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
                pDataB0 = pDataB1 + p->iData;
            }
            else 
            {
                pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
                pDataB1 = pDataB0 + p->iData;
            }
        }
        for ( i = 0; i < p->iData; i++ )
            pData0[i] = pDataA0[i] | pDataB0[i], pData1[i] = pDataA1[i] & pDataB1[i];
    }
    else if ( Gia_ObjIsCo(pObj) )
    {
        pData0  = Gia_ParTestObj( p, Id );
        pData1  = pData0 + p->iData;
        if ( Gia_ObjFaninC0(pObj) )
        {
            pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
            pDataA0 = pDataA1 + p->iData;
        }
        else 
        {
            pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
            pDataA1 = pDataA0 + p->iData;
        }
        for ( i = 0; i < p->iData; i++ )
            pData0[i] = pDataA0[i], pData1[i] = pDataA1[i];
    }
    else if ( Gia_ObjIsCi(pObj) )
    {
        if ( Gia_ObjIsPi(p, pObj) )
        {
            pData0  = Gia_ParTestObj( p, Id );
            pData1  = pData0 + p->iData;
            for ( i = 0; i < p->iData; i++ )
                pData0[i] = Gia_ManRandomW(0), pData1[i] = ~pData0[i];
        }
        else
        {
            int Id2 = Gia_ObjId(p, Gia_ObjRoToRi(p, pObj));
            pData0  = Gia_ParTestObj( p, Id );
            pData1  = pData0 + p->iData;
            pDataA0 = Gia_ParTestObj( p, Id2 );
            pDataA1 = pDataA0 + p->iData;
            for ( i = 0; i < p->iData; i++ )
                pData0[i] = pDataA0[i], pData1[i] = pDataA1[i];
        }
    }
    else if ( Gia_ObjIsConst0(pObj) )
    {
        pData0  = Gia_ParTestObj( p, Id );
        pData1  = pData0 + p->iData;
        for ( i = 0; i < p->iData; i++ )
            pData0[i] = ~(word)0, pData1[i] = 0;
    }
    else assert( 0 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManInseTest()

Vec_Int_t * Gia_ManInseTest	(	Gia_Man_t *	p,
		Vec_Int_t *	vInit0,
		int	nFrames,
		int	nWords,
		int	nTimeOut,
		int	fSim,
		int	fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file bmcInse.c.

{
    Vec_Int_t * vRes, * vInit;
    vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 0 );
    vRes = Gia_ManInsePerform( p, vInit, nFrames, nWords, fVerbose );
    if ( vInit != vInit0 )
        Vec_IntFree( vInit );
    return vRes;
}

Here is the call graph for this function: