cecPat.c File Reference

#include "cecInt.h"

Go to the source code of this file.

Functions
static ABC_NAMESPACE_IMPL_START void	Cec_ManPatStoreNum (Cec_ManPat_t *p, int Num)
	DECLARATIONS ///. More...
static int	Cec_ManPatRestoreNum (Cec_ManPat_t *p)
static void	Cec_ManPatStore (Cec_ManPat_t *p, Vec_Int_t *vPat)
static void	Cec_ManPatRestore (Cec_ManPat_t *p, Vec_Int_t *vPat)
int	Cec_ManPatComputePattern_rec (Cec_ManSat_t *pSat, Gia_Man_t *p, Gia_Obj_t *pObj)
void	Cec_ManPatComputePattern1_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPat)
void	Cec_ManPatComputePattern2_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPat)
int	Cec_ManPatComputePattern3_rec (Gia_Man_t *p, Gia_Obj_t *pObj)
void	Cec_ManPatVerifyPattern (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPat)
void	Cec_ManPatComputePattern4_rec (Gia_Man_t *p, Gia_Obj_t *pObj)
void	Cec_ManPatCleanMark0 (Gia_Man_t *p, Gia_Obj_t *pObj)
void	Cec_ManPatSavePattern (Cec_ManPat_t *pMan, Cec_ManSat_t *p, Gia_Obj_t *pObj)
void	Cec_ManPatSavePatternCSat (Cec_ManPat_t *pMan, Vec_Int_t *vPat)
int	Cec_ManPatCollectTry (Vec_Ptr_t *vInfo, Vec_Ptr_t *vPres, int iBit, int *pLits, int nLits)
Vec_Ptr_t *	Cec_ManPatCollectPatterns (Cec_ManPat_t *pMan, int nInputs, int nWordsInit)
Vec_Ptr_t *	Cec_ManPatPackPatterns (Vec_Int_t *vCexStore, int nInputs, int nRegs, int nWordsInit)

Function Documentation

void Cec_ManPatCleanMark0	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 341 of file cecPat.c.

{
    assert( Gia_ObjIsCo(pObj) );
    Gia_ManIncrementTravId( p );
    Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin0(pObj) );
}

Vec_Ptr_t* Cec_ManPatCollectPatterns	(	Cec_ManPat_t *	pMan,
		int	nInputs,
		int	nWordsInit
	)

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

Synopsis [Packs patterns into array of simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 455 of file cecPat.c.

{
    Vec_Int_t * vPat = pMan->vPattern1;
    Vec_Ptr_t * vInfo, * vPres;
    int k, kMax = -1, nPatterns = 0;
    int iStartOld = pMan->iStart;
    int nWords = nWordsInit;
    int nBits = 32 * nWords;
    abctime clk = Abc_Clock();
    vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
    Gia_ManRandomInfo( vInfo, 0, 0, nWords );
    vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
    Vec_PtrCleanSimInfo( vPres, 0, nWords );
    while ( pMan->iStart < Vec_StrSize(pMan->vStorage) )
    {
        nPatterns++;
        Cec_ManPatRestore( pMan, vPat );
        for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) )
            if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
                break;
        kMax = Abc_MaxInt( kMax, k );
        if ( k == nBits-1 )
        {
            Vec_PtrReallocSimInfo( vInfo );
            Gia_ManRandomInfo( vInfo, 0, nWords, 2*nWords );
            Vec_PtrReallocSimInfo( vPres );
            Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
            nWords *= 2;
            nBits *= 2;
        }
    }
    Vec_PtrFree( vPres );
    pMan->nSeries = Vec_PtrReadWordsSimInfo(vInfo) / nWordsInit;
    pMan->timePack += Abc_Clock() - clk;
    pMan->timeTotal += Abc_Clock() - clk;
    pMan->iStart = iStartOld;
    if ( pMan->fVerbose )
    {
        Abc_Print( 1, "Total = %5d. Max used = %5d. Full = %5d. Series = %d. ", 
            nPatterns, kMax, nWordsInit*32, pMan->nSeries );
        ABC_PRT( "Time", Abc_Clock() - clk );
        Cec_ManPatPrintStats( pMan );
    }
    return vInfo;
}

int Cec_ManPatCollectTry	(	Vec_Ptr_t *	vInfo,
		Vec_Ptr_t *	vPres,
		int	iBit,
		int *	pLits,
		int	nLits
	)

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

Synopsis [Packs patterns into array of simulation info.]

Description []

SideEffects []

SeeAlso []

                               ` 

Definition at line 421 of file cecPat.c.

{
    unsigned * pInfo, * pPres;
    int i;
    for ( i = 0; i < nLits; i++ )
    {
        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
        pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
        if ( Abc_InfoHasBit( pPres, iBit ) && 
             Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
             return 0;
    }
    for ( i = 0; i < nLits; i++ )
    {
        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
        pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
        Abc_InfoSetBit( pPres, iBit );
        if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
            Abc_InfoXorBit( pInfo, iBit );
    }
    return 1;
}

void Cec_ManPatComputePattern1_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vPat
	)

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

Synopsis [Derives satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file cecPat.c.

{
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return;
    Gia_ObjSetTravIdCurrent(p, pObj);
    if ( Gia_ObjIsCi(pObj) )
    {
        Vec_IntPush( vPat, Abc_Var2Lit( Gia_ObjCioId(pObj), pObj->fMark1==0 ) );
        return;
    }
    assert( Gia_ObjIsAnd(pObj) );
    if ( pObj->fMark1 == 1 )
    {
        Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin0(pObj), vPat );
        Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin1(pObj), vPat );
    }
    else
    {
        assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 0 ||
                (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)) == 0 );
        if ( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 0 )
            Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin0(pObj), vPat );
        else
            Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin1(pObj), vPat );
    }
}

void Cec_ManPatComputePattern2_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vPat
	)

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

Synopsis [Derives satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file cecPat.c.

{
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return;
    Gia_ObjSetTravIdCurrent(p, pObj);
    if ( Gia_ObjIsCi(pObj) )
    {
        Vec_IntPush( vPat, Abc_Var2Lit( Gia_ObjCioId(pObj), pObj->fMark1==0 ) );
        return;
    }
    assert( Gia_ObjIsAnd(pObj) );
    if ( pObj->fMark1 == 1 )
    {
        Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin0(pObj), vPat );
        Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin1(pObj), vPat );
    }
    else
    {
        assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 0 ||
                (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)) == 0 );
        if ( (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)) == 0 )
            Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin1(pObj), vPat );
        else
            Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin0(pObj), vPat );
    }
}

int Cec_ManPatComputePattern3_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis [Derives satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file cecPat.c.

{
    int Value0, Value1, Value;
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return (pObj->fMark1 << 1) | pObj->fMark0;
    Gia_ObjSetTravIdCurrent(p, pObj);
    if ( Gia_ObjIsCi(pObj) )
    {
        pObj->fMark0 = 1;
        pObj->fMark1 = 1;
        return GIA_UND;
    }
    assert( Gia_ObjIsAnd(pObj) );
    Value0 = Cec_ManPatComputePattern3_rec( p, Gia_ObjFanin0(pObj) );
    Value1 = Cec_ManPatComputePattern3_rec( p, Gia_ObjFanin1(pObj) );
    Value = Gia_XsimAndCond( Value0, Gia_ObjFaninC0(pObj), Value1, Gia_ObjFaninC1(pObj) );
    pObj->fMark0 =  (Value & 1);
    pObj->fMark1 = ((Value >> 1) & 1);
    return Value;
}

void Cec_ManPatComputePattern4_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file cecPat.c.

{
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return;
    Gia_ObjSetTravIdCurrent(p, pObj);
    pObj->fMark0 = 0;
    if ( Gia_ObjIsCi(pObj) )
        return;
    assert( Gia_ObjIsAnd(pObj) );
    Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin0(pObj) );
    Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin1(pObj) );
}

int Cec_ManPatComputePattern_rec	(	Cec_ManSat_t *	pSat,
		Gia_Man_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis [Derives satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file cecPat.c.

{
    int Counter = 0;
    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
        return 0;
    Gia_ObjSetTravIdCurrent(p, pObj);
    if ( Gia_ObjIsCi(pObj) )
    {
        pObj->fMark1 = Cec_ObjSatVarValue( pSat, pObj );
        return 1;
    }
    assert( Gia_ObjIsAnd(pObj) );
    Counter += Cec_ManPatComputePattern_rec( pSat, p, Gia_ObjFanin0(pObj) );
    Counter += Cec_ManPatComputePattern_rec( pSat, p, Gia_ObjFanin1(pObj) );
    pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & 
                   (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
    return Counter;
}

Vec_Ptr_t* Cec_ManPatPackPatterns	(	Vec_Int_t *	vCexStore,
		int	nInputs,
		int	nRegs,
		int	nWordsInit
	)

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

Synopsis [Packs patterns into array of simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file cecPat.c.

{
    Vec_Int_t * vPat;
    Vec_Ptr_t * vInfo, * vPres;
    int k, nSize, iStart, kMax = 0, nPatterns = 0;
    int nWords = nWordsInit;
    int nBits = 32 * nWords;
//    int RetValue;
    assert( nRegs <= nInputs );
    vPat  = Vec_IntAlloc( 100 );

    vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
    Vec_PtrCleanSimInfo( vInfo, 0, nWords );
    Gia_ManRandomInfo( vInfo, nRegs, 0, nWords );

    vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
    Vec_PtrCleanSimInfo( vPres, 0, nWords );
    iStart = 0;
    while ( iStart < Vec_IntSize(vCexStore) )
    {
        nPatterns++;
        // skip the output number
        iStart++;
        // get the number of items
        nSize = Vec_IntEntry( vCexStore, iStart++ );
        if ( nSize <= 0 )
            continue;
        // extract pattern
        Vec_IntClear( vPat );
        for ( k = 0; k < nSize; k++ )
            Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
        // add pattern to storage
        for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) )
            if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
                break;

//        k = kMax + 1;
//        RetValue = Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) );
//        assert( RetValue == 1 );

        kMax = Abc_MaxInt( kMax, k );
        if ( k == nBits-1 )
        {
            Vec_PtrReallocSimInfo( vInfo );
            Vec_PtrCleanSimInfo( vInfo, nWords, 2*nWords );
            Gia_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords );

            Vec_PtrReallocSimInfo( vPres );
            Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
            nWords *= 2;
            nBits *= 2;
        }
    }
//    Abc_Print( 1, "packed %d patterns into %d vectors (out of %d)\n", nPatterns, kMax, nBits );
    Vec_PtrFree( vPres );
    Vec_IntFree( vPat );
    return vInfo;
}

static void Cec_ManPatRestore ( Cec_ManPat_t *  p, Vec_Int_t *  vPat  )

inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 113 of file cecPat.c.

{
    int i, Size, Number;
    Vec_IntClear( vPat );
    Size = Cec_ManPatRestoreNum( p );
    Number = Cec_ManPatRestoreNum( p );
    Vec_IntPush( vPat, Number );
    for ( i = 1; i < Size; i++ )
    {
        Number += Cec_ManPatRestoreNum( p );
        Vec_IntPush( vPat, Number );
    }
    assert( Vec_IntSize(vPat) == Size );
}

static int Cec_ManPatRestoreNum ( Cec_ManPat_t *  p )

inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file cecPat.c.

{
    int ch, i, x = 0;
    for ( i = 0; (ch = Vec_StrEntry(p->vStorage, p->iStart++)) & 0x80; i++ )
        x |= (ch & 0x7f) << (7 * i);
    return x | (ch << (7 * i));
}

void Cec_ManPatSavePattern	(	Cec_ManPat_t *	pMan,
		Cec_ManSat_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 359 of file cecPat.c.

{
    Vec_Int_t * vPat;
    int nPatLits;
    abctime clkTotal = Abc_Clock();
//    abctime clk;
    assert( Gia_ObjIsCo(pObj) );
    pMan->nPats++;
    pMan->nPatsAll++;
    // compute values in the cone of influence
//clk = Abc_Clock();
    Gia_ManIncrementTravId( p->pAig );
    nPatLits = Cec_ManPatComputePattern_rec( p, p->pAig, Gia_ObjFanin0(pObj) );
    assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 1 );
    pMan->nPatLits += nPatLits;
    pMan->nPatLitsAll += nPatLits;
//pMan->timeFind += Abc_Clock() - clk;
    // compute sensitizing path
//clk = Abc_Clock();
    Vec_IntClear( pMan->vPattern1 );
    Gia_ManIncrementTravId( p->pAig );
    Cec_ManPatComputePattern1_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern1 );
    // compute sensitizing path
    Vec_IntClear( pMan->vPattern2 );
    Gia_ManIncrementTravId( p->pAig );
    Cec_ManPatComputePattern2_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern2 );
    // compare patterns
    vPat = Vec_IntSize(pMan->vPattern1) < Vec_IntSize(pMan->vPattern2) ? pMan->vPattern1 : pMan->vPattern2;
    pMan->nPatLitsMin += Vec_IntSize(vPat);
    pMan->nPatLitsMinAll += Vec_IntSize(vPat);
//pMan->timeShrink += Abc_Clock() - clk;
    // verify pattern using ternary simulation
//clk = Abc_Clock();
//    Cec_ManPatVerifyPattern( p->pAig, pObj, vPat );
//pMan->timeVerify += Abc_Clock() - clk;
    // sort pattern
//clk = Abc_Clock();
    Vec_IntSort( vPat, 0 );
//pMan->timeSort += Abc_Clock() - clk;
    // save pattern
    Cec_ManPatStore( pMan, vPat );
    pMan->timeTotal += Abc_Clock() - clkTotal;
}

void Cec_ManPatSavePatternCSat	(	Cec_ManPat_t *	pMan,
		Vec_Int_t *	vPat
	)

Definition at line 402 of file cecPat.c.

{
    // sort pattern
    Vec_IntSort( vPat, 0 );
    // save pattern
    Cec_ManPatStore( pMan, vPat );
}

static void Cec_ManPatStore ( Cec_ManPat_t *  p, Vec_Int_t *  vPat  )

inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file cecPat.c.

{
    int i, Number, NumberPrev;
    assert( Vec_IntSize(vPat) > 0 );
    Cec_ManPatStoreNum( p, Vec_IntSize(vPat) );
    NumberPrev = Vec_IntEntry( vPat, 0 );
    Cec_ManPatStoreNum( p, NumberPrev );
    Vec_IntForEachEntryStart( vPat, Number, i, 1 )
    {
        assert( NumberPrev < Number );
        Cec_ManPatStoreNum( p, Number - NumberPrev );
        NumberPrev = Number;
    }
}

static ABC_NAMESPACE_IMPL_START void Cec_ManPatStoreNum ( Cec_ManPat_t *  p, int  Num  )

inlinestatic

DECLARATIONS ///.

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

FileName [cecPat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [Simulation pattern manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

cecPat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file cecPat.c.

{
    unsigned x = (unsigned)Num;
    assert( Num >= 0 );
    while ( x & ~0x7f )
    {
        Vec_StrPush( p->vStorage, (char)((x & 0x7f) | 0x80) );
        x >>= 7;
    }
    Vec_StrPush( p->vStorage, (char)x );
}

void Cec_ManPatVerifyPattern	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vPat
	)

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

Synopsis [Derives satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 278 of file cecPat.c.

{
    Gia_Obj_t * pTemp;
    int i, Value;
    Gia_ManIncrementTravId( p );
    Vec_IntForEachEntry( vPat, Value, i )
    {
        pTemp = Gia_ManCi( p, Abc_Lit2Var(Value) );
//        assert( Abc_LitIsCompl(Value) != (int)pTemp->fMark1 );
        if ( pTemp->fMark1 )
        {
            pTemp->fMark0 = 0;
            pTemp->fMark1 = 1;
        }
        else
        {
            pTemp->fMark0 = 1;
            pTemp->fMark1 = 0;
        }
        Gia_ObjSetTravIdCurrent( p, pTemp );
    }
    Value = Cec_ManPatComputePattern3_rec( p, Gia_ObjFanin0(pObj) );
    Value = Gia_XsimNotCond( Value, Gia_ObjFaninC0(pObj) );
    if ( Value != GIA_ONE )
        Abc_Print( 1, "Cec_ManPatVerifyPattern(): Verification failed.\n" );
    assert( Value == GIA_ONE );
}