abc/src/proof/cec/cecPat.c - third_party/vtr-verilog-to-routing - Git at Google


            
            /**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 $]


            ***********************************************************************/


            #include "cecInt.h"


            ABC_NAMESPACE_IMPL_START


            ////////////////////////////////////////////////////////////////////////

            
            ///                        DECLARATIONS                              ///

            
            ////////////////////////////////////////////////////////////////////////


            ////////////////////////////////////////////////////////////////////////

            
            ///                     FUNCTION DEFINITIONS                         ///

            
            ////////////////////////////////////////////////////////////////////////


            /**Function*************************************************************


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

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

            
            {

            
                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 );

            
            }


            /**Function*************************************************************


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            static inline int Cec_ManPatRestoreNum( Cec_ManPat_t * p )

            
            {

            
                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));

            
            }


            /**Function*************************************************************


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

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

            
            {

            
                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;

            
                }

            
            }


            /**Function*************************************************************


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

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

            
            {

            
                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 );

            
            }


            /**Function*************************************************************


              Synopsis    [Derives satisfying assignment.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

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

            
            {

            
                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;

            
            }


            /**Function*************************************************************


              Synopsis    [Derives satisfying assignment.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

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

            
            {

            
                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 );

            
                }

            
            }


            /**Function*************************************************************


              Synopsis    [Derives satisfying assignment.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

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

            
            {

            
                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 );

            
                }

            
            }


            /**Function*************************************************************


              Synopsis    [Derives satisfying assignment.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            int Cec_ManPatComputePattern3_rec( Gia_Man_t * p, Gia_Obj_t * pObj )

            
            {

            
                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;

            
            }


            /**Function*************************************************************


              Synopsis    [Derives satisfying assignment.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

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

            
            {

            
                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 );

            
            }


            /**Function*************************************************************


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            void Cec_ManPatComputePattern4_rec( Gia_Man_t * p, Gia_Obj_t * pObj )

            
            {

            
                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) );

            
            }


            /**Function*************************************************************


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

            
            void Cec_ManPatCleanMark0( Gia_Man_t * p, Gia_Obj_t * pObj )

            
            {

            
                assert( Gia_ObjIsCo(pObj) );

            
                Gia_ManIncrementTravId( p );

            
                Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin0(pObj) );

            
            }


            /**Function*************************************************************


              Synopsis    []


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

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

            
            {

            
                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 )

            
            {

            
                // sort pattern

            
                Vec_IntSort( vPat, 0 );

            
                // save pattern

            
                Cec_ManPatStore( pMan, vPat );

            
            }


            /**Function*************************************************************


              Synopsis    [Packs patterns into array of simulation info.]


              Description []


              SideEffects []


              SeeAlso     []


            *************************************`**********************************/

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

            
            {

            
                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;

            
            }


            /**Function*************************************************************


              Synopsis    [Packs patterns into array of simulation info.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

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

            
            {

            
                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;

            
            }


            /**Function*************************************************************


              Synopsis    [Packs patterns into array of simulation info.]


              Description []


              SideEffects []


              SeeAlso     []


            ***********************************************************************/

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

            
            {

            
                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;

            
            }


            ////////////////////////////////////////////////////////////////////////

            
            ///                       END OF FILE                                ///

            
            ////////////////////////////////////////////////////////////////////////


            ABC_NAMESPACE_IMPL_END
	/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 $]

	***********************************************************************/

	#include "cecInt.h"

	ABC_NAMESPACE_IMPL_START


	////////////////////////////////////////////////////////////////////////
	/// DECLARATIONS ///
	////////////////////////////////////////////////////////////////////////

	////////////////////////////////////////////////////////////////////////
	/// FUNCTION DEFINITIONS ///
	////////////////////////////////////////////////////////////////////////

	/Function***********************************************************

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	static inline void Cec_ManPatStoreNum( Cec_ManPat_t * p, int Num )
	{
	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 );
	}

	/Function***********************************************************

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	static inline int Cec_ManPatRestoreNum( Cec_ManPat_t * p )
	{
	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));
	}

	/Function***********************************************************

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	static inline void Cec_ManPatStore( Cec_ManPat_t * p, Vec_Int_t * vPat )
	{
	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;
	}
	}

	/Function***********************************************************

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	static inline void Cec_ManPatRestore( Cec_ManPat_t * p, Vec_Int_t * vPat )
	{
	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 );
	}


	/Function***********************************************************

	Synopsis [Derives satisfying assignment.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Cec_ManPatComputePattern_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj )
	{
	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;
	}

	/Function***********************************************************

	Synopsis [Derives satisfying assignment.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Cec_ManPatComputePattern1_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat )
	{
	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 );
	}
	}

	/Function***********************************************************

	Synopsis [Derives satisfying assignment.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Cec_ManPatComputePattern2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat )
	{
	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 );
	}
	}

	/Function***********************************************************

	Synopsis [Derives satisfying assignment.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	int Cec_ManPatComputePattern3_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
	{
	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;
	}

	/Function***********************************************************

	Synopsis [Derives satisfying assignment.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Cec_ManPatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat )
	{
	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 );
	}

	/Function***********************************************************

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Cec_ManPatComputePattern4_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
	{
	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) );
	}

	/Function***********************************************************

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Cec_ManPatCleanMark0( Gia_Man_t * p, Gia_Obj_t * pObj )
	{
	assert( Gia_ObjIsCo(pObj) );
	Gia_ManIncrementTravId( p );
	Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin0(pObj) );
	}

	/Function***********************************************************

	Synopsis []

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	void Cec_ManPatSavePattern( Cec_ManPat_t * pMan, Cec_ManSat_t * p, Gia_Obj_t * pObj )
	{
	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 )
	{
	// sort pattern
	Vec_IntSort( vPat, 0 );
	// save pattern
	Cec_ManPatStore( pMan, vPat );
	}

	/Function***********************************************************

	Synopsis [Packs patterns into array of simulation info.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************`********************************/
	int Cec_ManPatCollectTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
	{
	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;
	}

	/Function***********************************************************

	Synopsis [Packs patterns into array of simulation info.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nWordsInit )
	{
	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;
	}


	/Function***********************************************************

	Synopsis [Packs patterns into array of simulation info.]

	Description []

	SideEffects []

	SeeAlso []

	***********************************************************************/
	Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit )
	{
	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;
	}

	////////////////////////////////////////////////////////////////////////
	/// END OF FILE ///
	////////////////////////////////////////////////////////////////////////


	ABC_NAMESPACE_IMPL_END