/**CFile**************************************************************** FileName [giaSim.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Scalable AIG package.] Synopsis [Fast sequential simulator.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: giaSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "gia.h" #include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// typedef struct Gia_SimRsbMan_t_ Gia_SimRsbMan_t; struct Gia_SimRsbMan_t_ { Gia_Man_t * pGia; Vec_Int_t * vTfo; Vec_Int_t * vCands; Vec_Int_t * vFanins; Vec_Int_t * vFanins2; Vec_Wrd_t * vSimsObj; Vec_Wrd_t * vSimsObj2; int nWords; word * pFunc[3]; }; typedef struct Gia_SimAbsMan_t_ Gia_SimAbsMan_t; struct Gia_SimAbsMan_t_ { // problem formulation Gia_Man_t * pGia; // AIG manager word * pSet[2]; // offset/onset truth tables int nCands; // candidate count int nWords; // word count Vec_Wrd_t * vSims; // candidate simulation info Vec_Int_t * vResub; // the result // intermediate result Vec_Int_t * vValues; // function values in each pattern Vec_Int_t * vPatPairs; // used minterms int nWordsTable; // words of table data word * pTableTemp; // temporary table pattern Vec_Wrd_t * vCoverTable; // columns = minterms; rows = classes Vec_Int_t * vTtMints; // truth table minterms }; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSimPatAssignInputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsIn ) { int i, Id; assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) ); assert( Vec_WrdSize(vSimsIn) == nWords * Gia_ManCiNum(p) ); Gia_ManForEachCiId( p, Id, i ) memcpy( Vec_WrdEntryP(vSims, Id*nWords), Vec_WrdEntryP(vSimsIn, i*nWords), sizeof(word)*nWords ); } static inline void Gia_ManSimPatSimAnd( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims ) { word pComps[2] = { 0, ~(word)0 }; word Diff0 = pComps[Gia_ObjFaninC0(pObj)]; word Diff1 = pComps[Gia_ObjFaninC1(pObj)]; word * pSims = Vec_WrdArray(vSims); word * pSims0 = pSims + nWords*Gia_ObjFaninId0(pObj, i); word * pSims1 = pSims + nWords*Gia_ObjFaninId1(pObj, i); word * pSims2 = pSims + nWords*i; int w; if ( Gia_ObjIsXor(pObj) ) for ( w = 0; w < nWords; w++ ) pSims2[w] = (pSims0[w] ^ Diff0) ^ (pSims1[w] ^ Diff1); else for ( w = 0; w < nWords; w++ ) pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1); } static inline void Gia_ManSimPatSimPo( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims ) { word pComps[2] = { 0, ~(word)0 }; word Diff0 = pComps[Gia_ObjFaninC0(pObj)]; word * pSims = Vec_WrdArray(vSims); word * pSims0 = pSims + nWords*Gia_ObjFaninId0(pObj, i); word * pSims2 = pSims + nWords*i; int w; for ( w = 0; w < nWords; w++ ) pSims2[w] = (pSims0[w] ^ Diff0); } Vec_Wrd_t * Gia_ManSimPatSim( Gia_Man_t * pGia ) { Gia_Obj_t * pObj; int i, nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia); Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords ); assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 ); Gia_ManSimPatAssignInputs( pGia, nWords, vSims, pGia->vSimsPi ); Gia_ManForEachAnd( pGia, pObj, i ) Gia_ManSimPatSimAnd( pGia, i, pObj, nWords, vSims ); Gia_ManForEachCo( pGia, pObj, i ) Gia_ManSimPatSimPo( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims ); return vSims; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSimPatValuesDerive( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vValues ) { int i, Id; assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) ); assert( Vec_WrdSize(vValues) == nWords * Gia_ManCoNum(p) ); Gia_ManForEachCoId( p, Id, i ) memcpy( Vec_WrdEntryP(vValues, nWords * i), Vec_WrdEntryP(vSims, nWords * Id), sizeof(word)* nWords ); } Vec_Wrd_t * Gia_ManSimPatValues( Gia_Man_t * p ) { int i, Id, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); Vec_Wrd_t * vSims = Gia_ManSimPatSim( p ); Vec_Wrd_t * vValues = Vec_WrdStart( Gia_ManCoNum(p) * nWords ); assert( Vec_WrdSize(p->vSimsPi) == nWords * Gia_ManCiNum(p) ); assert( Vec_WrdSize(vValues) == nWords * Gia_ManCoNum(p) ); assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) ); Gia_ManForEachCoId( p, Id, i ) memcpy( Vec_WrdEntryP(vValues, nWords * i), Vec_WrdEntryP(vSims, nWords * Id), sizeof(word)* nWords ); Vec_WrdFree( vSims ); return vValues; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Wrd_t * Gia_ManSimCombine( int nInputs, Vec_Wrd_t * vBase, Vec_Wrd_t * vAddOn, int nWordsUse ) { int nWordsBase = Vec_WrdSize(vBase) / nInputs; int nWordsAddOn = Vec_WrdSize(vAddOn) / nInputs; int i, w; Vec_Wrd_t * vSimsIn = Vec_WrdAlloc( nInputs * (nWordsBase + nWordsUse) ); assert( Vec_WrdSize(vBase) % nInputs == 0 ); assert( Vec_WrdSize(vAddOn) % nInputs == 0 ); assert( nWordsUse <= nWordsAddOn ); for ( i = 0; i < nInputs; i++ ) { word * pSimsB = Vec_WrdEntryP( vBase, i * nWordsBase ); word * pSimsA = Vec_WrdEntryP( vAddOn, i * nWordsAddOn ); for ( w = 0; w < nWordsBase; w++ ) Vec_WrdPush( vSimsIn, pSimsB[w] ); for ( w = 0; w < nWordsUse; w++ ) Vec_WrdPush( vSimsIn, pSimsA[w] ); } assert( Vec_WrdSize(vSimsIn) == Vec_WrdCap(vSimsIn) ); return vSimsIn; } int Gia_ManSimBitPackOne( int nWords, Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsCare, int iPat, int * pLits, int nLits ) { word * pSimsI, * pSimsC; int i, k; for ( i = 0; i < iPat; i++ ) { for ( k = 0; k < nLits; k++ ) { int iVar = Abc_Lit2Var( pLits[k] ); pSimsI = Vec_WrdEntryP( vSimsIn, nWords * iVar ); pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar ); if ( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k])) ) break; } if ( k == nLits ) break; } for ( k = 0; k < nLits; k++ ) { int iVar = Abc_Lit2Var( pLits[k] ); pSimsI = Vec_WrdEntryP( vSimsIn, nWords * iVar ); pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar ); if ( !Abc_TtGetBit(pSimsC, i) && Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k]) ) Abc_TtXorBit( pSimsI, i ); Abc_TtSetBit( pSimsC, i ); assert( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) != Abc_LitIsCompl(pLits[k])) ); } return (int)(i == iPat); } Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCexes ) { int c, iCur = 0, iPat = 0; int nWordsMax = Abc_Bit6WordNum( nCexes ); Vec_Wrd_t * vSimsIn = Vec_WrdStartRandom( Gia_ManCiNum(p) * nWordsMax ); Vec_Wrd_t * vSimsCare = Vec_WrdStart( Gia_ManCiNum(p) * nWordsMax ); Vec_Wrd_t * vSimsRes = NULL; for ( c = 0; c < nCexes; c++ ) { int Out = Vec_IntEntry( vCexStore, iCur++ ); int Size = Vec_IntEntry( vCexStore, iCur++ ); iPat += Gia_ManSimBitPackOne( nWordsMax, vSimsIn, vSimsCare, iPat, Vec_IntEntryP(vCexStore, iCur), Size ); iCur += Size; assert( iPat <= nCexes ); Out = 0; } printf( "Compressed %d CEXes into %d test patterns.\n", nCexes, iPat ); assert( iCur == Vec_IntSize(vCexStore) ); vSimsRes = Gia_ManSimCombine( Gia_ManCiNum(p), p->vSimsPi, vSimsIn, Abc_Bit6WordNum(iPat+1) ); printf( "Combined %d words of the original info with %d words of additional info.\n", Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p), Abc_Bit6WordNum(iPat+1) ); Vec_WrdFree( vSimsIn ); Vec_WrdFree( vSimsCare ); return vSimsRes; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManSimPatHashPatterns( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int * pnC0, int * pnC1 ) { Gia_Obj_t * pObj; int i, nUnique; Vec_Mem_t * vStore; vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page Vec_MemHashAlloc( vStore, 1 << 12 ); Gia_ManForEachCand( p, pObj, i ) { word * pSim = Vec_WrdEntryP(vSims, i*nWords); if ( pnC0 && Abc_TtIsConst0(pSim, nWords) ) (*pnC0)++; if ( pnC1 && Abc_TtIsConst1(pSim, nWords) ) (*pnC1)++; Vec_MemHashInsert( vStore, pSim ); } nUnique = Vec_MemEntryNum( vStore ); Vec_MemHashFree( vStore ); Vec_MemFree( vStore ); return nUnique; } Gia_Man_t * Gia_ManSimPatGenMiter( Gia_Man_t * p, Vec_Wrd_t * vSims ) { Gia_Man_t * pNew; Gia_Obj_t * pObj; int i, nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(p); pNew = Gia_ManStart( Gia_ManObjNum(p) + Gia_ManCoNum(p) ); Gia_ManHashStart( pNew ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi( pNew ); Gia_ManForEachAnd( p, pObj, i ) pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); Gia_ManForEachAnd( p, pObj, i ) { word * pSim = Vec_WrdEntryP(vSims, i*nWords); if ( Abc_TtIsConst0(pSim, nWords) ) Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 0) ); if ( Abc_TtIsConst1(pSim, nWords) ) Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 1) ); } Gia_ManHashStop( pNew ); return pNew; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSimPatWriteOne( FILE * pFile, word * pSim, int nWords ) { int k, Digit, nDigits = nWords*16; for ( k = 0; k < nDigits; k++ ) { Digit = (int)((pSim[k/16] >> ((k%16) * 4)) & 15); if ( Digit < 10 ) fprintf( pFile, "%d", Digit ); else fprintf( pFile, "%c", 'A' + Digit-10 ); } fprintf( pFile, "\n" ); } void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords ) { int i, nNodes = Vec_WrdSize(vSimsIn) / nWords; FILE * pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; } assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); for ( i = 0; i < nNodes; i++ ) Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords ); fclose( pFile ); printf( "Written %d words of simulation data.\n", nWords ); } int Gia_ManSimPatReadOne( char c ) { int Digit = 0; if ( c >= '0' && c <= '9' ) Digit = c - '0'; else if ( c >= 'A' && c <= 'F' ) Digit = c - 'A' + 10; else if ( c >= 'a' && c <= 'f' ) Digit = c - 'a' + 10; else assert( 0 ); assert( Digit >= 0 && Digit < 16 ); return Digit; } Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName ) { Vec_Wrd_t * vSimsIn = NULL; int c, nWords = -1, nChars = 0; word Num = 0; FILE * pFile = fopen( pFileName, "rb" ); if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for reading.\n", pFileName ); return NULL; } vSimsIn = Vec_WrdAlloc( 1000 ); while ( (c = fgetc(pFile)) != EOF ) { if ( c == '\n' && nWords == -1 ) nWords = Vec_WrdSize(vSimsIn); if ( c == '\n' || c == '\r' || c == '\t' || c == ' ' ) continue; Num |= (word)Gia_ManSimPatReadOne((char)c) << (nChars * 4); if ( ++nChars < 16 ) continue; Vec_WrdPush( vSimsIn, Num ); nChars = 0; Num = 0; } assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); fclose( pFile ); printf( "Read %d words of simulation data.\n", nWords ); return vSimsIn; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSimProfile( Gia_Man_t * pGia ) { Vec_Wrd_t * vSims = Gia_ManSimPatSim( pGia ); int nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia); int nC0s = 0, nC1s = 0, nUnique = Gia_ManSimPatHashPatterns( pGia, nWords, vSims, &nC0s, &nC1s ); printf( "Simulating %d words leads to %d unique objects (%.2f %% out of %d), Const0 = %d. Const1 = %d.\n", nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s ); Vec_WrdFree( vSims ); } void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose ) { extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); int i, Status, Counts[3] = {0}; Gia_Man_t * pGia; Vec_Wrd_t * vSimsIn = NULL; Vec_Str_t * vStatus = NULL; Vec_Int_t * vCexStore = NULL; Vec_Wrd_t * vSims = Gia_ManSimPatSim( p ); Gia_ManSimProfile( p ); pGia = Gia_ManSimPatGenMiter( p, vSims ); vCexStore = Cbs2_ManSolveMiterNc( pGia, 1000, &vStatus, 0 ); Gia_ManStop( pGia ); Vec_StrForEachEntry( vStatus, Status, i ) { assert( Status >= -1 && Status <= 1 ); Counts[Status+1]++; } printf( "Total = %d : SAT = %d. UNSAT = %d. UNDEC = %d.\n", Counts[1]+Counts[2]+Counts[0], Counts[1], Counts[2], Counts[0] ); if ( Counts[1] == 0 ) printf( "There are no counter-examples. No need for more simulation.\n" ); else { vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1] ); Vec_WrdFreeP( &p->vSimsPi ); p->vSimsPi = vSimsIn; Gia_ManSimProfile( p ); } Vec_StrFree( vStatus ); Vec_IntFree( vCexStore ); Vec_WrdFree( vSims ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_SimRsbMan_t * Gia_SimRsbAlloc( Gia_Man_t * pGia ) { Gia_SimRsbMan_t * p = ABC_CALLOC( Gia_SimRsbMan_t, 1 ); p->pGia = pGia; p->nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia); assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 ); p->pFunc[0] = ABC_CALLOC( word, p->nWords ); p->pFunc[1] = ABC_CALLOC( word, p->nWords ); p->pFunc[2] = ABC_CALLOC( word, p->nWords ); p->vTfo = Vec_IntAlloc( 1000 ); p->vCands = Vec_IntAlloc( 1000 ); p->vFanins = Vec_IntAlloc( 10 ); p->vFanins2 = Vec_IntAlloc( 10 ); p->vSimsObj = Gia_ManSimPatSim( pGia ); p->vSimsObj2 = Vec_WrdStart( Vec_WrdSize(p->vSimsObj) ); assert( p->nWords == Vec_WrdSize(p->vSimsObj) / Gia_ManObjNum(pGia) ); Gia_ManStaticFanoutStart( pGia ); return p; } void Gia_SimRsbFree( Gia_SimRsbMan_t * p ) { Gia_ManStaticFanoutStop( p->pGia ); Vec_IntFree( p->vTfo ); Vec_IntFree( p->vCands ); Vec_IntFree( p->vFanins ); Vec_IntFree( p->vFanins2 ); Vec_WrdFree( p->vSimsObj ); Vec_WrdFree( p->vSimsObj2 ); ABC_FREE( p->pFunc[0] ); ABC_FREE( p->pFunc[1] ); ABC_FREE( p->pFunc[2] ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_SimRsbTfo_rec( Gia_Man_t * p, int iObj, int iFanout, Vec_Int_t * vTfo ) { int i, iFan; if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) return; Gia_ObjSetTravIdCurrentId(p, iObj); Gia_ObjForEachFanoutStaticId( p, iObj, iFan, i ) if ( iFanout == -1 || iFan == iFanout ) Gia_SimRsbTfo_rec( p, iFan, -1, vTfo ); Vec_IntPush( vTfo, iObj ); } Vec_Int_t * Gia_SimRsbTfo( Gia_SimRsbMan_t * p, int iObj, int iFanout ) { assert( iObj > 0 ); Vec_IntClear( p->vTfo ); Gia_ManIncrementTravId( p->pGia ); Gia_SimRsbTfo_rec( p->pGia, iObj, iFanout, p->vTfo ); assert( Vec_IntEntryLast(p->vTfo) == iObj ); Vec_IntPop( p->vTfo ); Vec_IntReverseOrder( p->vTfo ); Vec_IntSort( p->vTfo, 0 ); return p->vTfo; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ word * Gia_SimRsbFunc( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins, int fOnSet ) { int nTruthWords = Abc_Truth6WordNum( Vec_IntSize(vFanins) ); word * pTruth = ABC_CALLOC( word, nTruthWords ); word * pFunc = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj ); word * pFanins[16] = {NULL}; int s, b, iMint, i, iFanin; assert( Vec_IntSize(vFanins) <= 16 ); Vec_IntForEachEntry( vFanins, iFanin, i ) pFanins[i] = Vec_WrdEntryP( p->vSimsObj, p->nWords*iFanin ); for ( s = 0; s < 64*p->nWords; s++ ) { if ( !Abc_TtGetBit(p->pFunc[2], s) || Abc_TtGetBit(pFunc, s) != fOnSet ) continue; iMint = 0; for ( b = 0; b < Vec_IntSize(vFanins); b++ ) if ( Abc_TtGetBit(pFanins[b], s) ) iMint |= 1 << b; Abc_TtSetBit( pTruth, iMint ); } return pTruth; } int Gia_SimRsbResubVerify( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins ) { word * pTruth0 = Gia_SimRsbFunc( p, iObj, p->vFanins, 0 ); word * pTruth1 = Gia_SimRsbFunc( p, iObj, p->vFanins, 1 ); int Res = !Abc_TtIntersect( pTruth0, pTruth1, p->nWords, 0 ); ABC_FREE( pTruth0 ); ABC_FREE( pTruth1 ); return Res; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline void Gia_SimRsbSimAndCareSet( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSims2 ) { word pComps[2] = { 0, ~(word)0 }; word Diff0 = pComps[Gia_ObjFaninC0(pObj)]; word Diff1 = pComps[Gia_ObjFaninC1(pObj)]; Vec_Wrd_t * vSims0 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) ? vSims2 : vSims; Vec_Wrd_t * vSims1 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) ? vSims2 : vSims; word * pSims0 = Vec_WrdEntryP( vSims0, nWords*Gia_ObjFaninId0(pObj, i) ); word * pSims1 = Vec_WrdEntryP( vSims1, nWords*Gia_ObjFaninId1(pObj, i) ); word * pSims2 = Vec_WrdEntryP( vSims2, nWords*i ); int w; if ( Gia_ObjIsXor(pObj) ) for ( w = 0; w < nWords; w++ ) pSims2[w] = (pSims0[w] ^ Diff0) ^ (pSims1[w] ^ Diff1); else for ( w = 0; w < nWords; w++ ) pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1); } word * Gia_SimRsbCareSet( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vTfo ) { word * pSims = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj ); word * pSims2 = Vec_WrdEntryP( p->vSimsObj2, p->nWords*iObj ); int iNode, i; Abc_TtCopy( pSims2, pSims, p->nWords, 1 ); Abc_TtClear( p->pFunc[2], p->nWords ); Vec_IntForEachEntry( vTfo, iNode, i ) { Gia_Obj_t * pNode = Gia_ManObj(p->pGia, iNode); if ( Gia_ObjIsAnd(pNode) ) Gia_SimRsbSimAndCareSet( p->pGia, iNode, pNode, p->nWords, p->vSimsObj, p->vSimsObj2 ); else if ( Gia_ObjIsCo(pNode) ) { word * pSimsA = Vec_WrdEntryP( p->vSimsObj, p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) ); word * pSimsB = Vec_WrdEntryP( p->vSimsObj2, p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) ); Abc_TtOrXor( p->pFunc[2], pSimsA, pSimsB, p->nWords ); } else assert( 0 ); } return p->pFunc[2]; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ObjSimCollect( Gia_SimRsbMan_t * p ) { int i, k, iTemp, iFanout; Vec_IntClear( p->vFanins2 ); assert( Vec_IntSize(p->vFanins) > 0 ); Vec_IntForEachEntry( p->vFanins, iTemp, i ) { Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iTemp ); if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId0(pObj, iTemp) ) ) Vec_IntPush( p->vFanins2, Gia_ObjFaninId0(pObj, iTemp) ); if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId1(pObj, iTemp) ) ) Vec_IntPush( p->vFanins2, Gia_ObjFaninId1(pObj, iTemp) ); Gia_ObjForEachFanoutStaticId( p->pGia, iTemp, iFanout, k ) if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanout)) && !Gia_ObjIsTravIdCurrentId( p->pGia, iFanout ) ) Vec_IntPush( p->vFanins2, iFanout ); } } Vec_Int_t * Gia_ObjSimCands( Gia_SimRsbMan_t * p, int iObj, int nCands ) { assert( iObj > 0 ); assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iObj)) ); Vec_IntClear( p->vCands ); Vec_IntFill( p->vFanins, 1, iObj ); while ( Vec_IntSize(p->vFanins) > 0 && Vec_IntSize(p->vCands) < nCands ) { int i, iTemp; Vec_IntForEachEntry( p->vFanins, iTemp, i ) Gia_ObjSetTravIdCurrentId( p->pGia, iTemp ); Gia_ObjSimCollect( p ); // p->vFanins -> p->vFanins2 Vec_IntAppend( p->vCands, p->vFanins2 ); ABC_SWAP( Vec_Int_t *, p->vFanins, p->vFanins2 ); } assert( Vec_IntSize(p->vFanins) == 0 || Vec_IntSize(p->vCands) >= nCands ); if ( Vec_IntSize(p->vCands) > nCands ) Vec_IntShrink( p->vCands, nCands ); return p->vCands; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ObjSimRsb( Gia_SimRsbMan_t * p, int iObj, int nCands, int fVerbose, int * pnBufs, int * pnInvs ) { int i, iCand, RetValue = 0; Vec_Int_t * vTfo = Gia_SimRsbTfo( p, iObj, -1 ); word * pCareSet = Gia_SimRsbCareSet( p, iObj, vTfo ); word * pFunc = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj ); Vec_Int_t * vCands = Gia_ObjSimCands( p, iObj, nCands ); Abc_TtAndSharp( p->pFunc[0], pCareSet, pFunc, p->nWords, 1 ); Abc_TtAndSharp( p->pFunc[1], pCareSet, pFunc, p->nWords, 0 ); /* printf( "Considering node %d with %d candidates:\n", iObj, Vec_IntSize(vCands) ); Vec_IntPrint( vTfo ); Vec_IntPrint( vCands ); Extra_PrintBinary( stdout, (unsigned *)pCareSet, 64 ); printf( "\n" ); Extra_PrintBinary( stdout, (unsigned *)pFunc, 64 ); printf( "\n" ); Extra_PrintBinary( stdout, (unsigned *)p->pFunc[0], 64 ); printf( "\n" ); Extra_PrintBinary( stdout, (unsigned *)p->pFunc[1], 64 ); printf( "\n" ); */ Vec_IntForEachEntry( vCands, iCand, i ) { word * pDiv = Vec_WrdEntryP( p->vSimsObj, p->nWords*iCand ); if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 0) && !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 1) ) { (*pnBufs)++; if ( fVerbose ) printf( "Level %3d : %d = buf(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; } if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 1) && !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 0) ) { (*pnInvs)++; if ( fVerbose ) printf( "Level %3d : %d = inv(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; } } return RetValue; } int Gia_ManSimRsb( Gia_Man_t * pGia, int nCands, int fVerbose ) { abctime clk = Abc_Clock(); Gia_Obj_t * pObj; int iObj, nCount = 0, nBufs = 0, nInvs = 0; Gia_SimRsbMan_t * p = Gia_SimRsbAlloc( pGia ); assert( pGia->vSimsPi != NULL ); Gia_ManLevelNum( pGia ); Gia_ManForEachAnd( pGia, pObj, iObj ) //if ( iObj == 6 ) nCount += Gia_ObjSimRsb( p, iObj, nCands, fVerbose, &nBufs, &nInvs ); printf( "Can resubstitute %d nodes (%.2f %% out of %d) (Bufs = %d Invs = %d) ", nCount, 100.0*nCount/Gia_ManAndNum(pGia), Gia_ManAndNum(pGia), nBufs, nInvs ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Gia_SimRsbFree( p ); return nCount; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSimRelAssignInputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int nWordsIn, Vec_Wrd_t * vSimsIn ) { int i, m, Id, nMints = nWords / nWordsIn; assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) ); assert( Vec_WrdSize(vSimsIn) == nWordsIn * Gia_ManCiNum(p) ); Gia_ManForEachCiId( p, Id, i ) for ( m = 0; m < nMints; m++ ) memcpy( Vec_WrdEntryP(vSims, Id * nWords + nWordsIn * m), Vec_WrdEntryP(vSimsIn, i * nWordsIn), sizeof(word) * nWordsIn ); } int Gia_ManSimRelCompare( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int nWordsOut, Vec_Wrd_t * vSimsOut, int iPat, int iMint ) { int i, Id; Gia_ManForEachCoId( p, Id, i ) { word * pSim = Vec_WrdEntryP( vSims, nWords * Id + iMint * nWordsOut ); word * pSimOut = Vec_WrdEntryP( vSimsOut, nWordsOut * i ); /* int k; for ( k = 0; k < 64*nWordsOut; k++ ) printf( "%d", Abc_TtGetBit( pSim, k ) ); printf( "\n" ); for ( k = 0; k < 64*nWordsOut; k++ ) printf( "%d", Abc_TtGetBit( pSimOut, k ) ); printf( "\n\n" ); */ if ( Abc_TtGetBit(pSim, iPat) != Abc_TtGetBit(pSimOut, iPat) ) return 0; } return 1; } void Gia_ManSimRelCollectOutputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int nWordsOut, Vec_Wrd_t * vSimsOut, Vec_Wrd_t * vRel ) { int i, m, nMints = nWords / nWordsOut; assert( Vec_WrdSize(vSims) == nWords * Gia_ManObjNum(p) ); assert( Vec_WrdSize(vSimsOut) == nWordsOut * Gia_ManCoNum(p) ); assert( Vec_WrdSize(vRel) == nWordsOut * nMints ); for ( i = 0; i < 64 * nWordsOut; i++ ) for ( m = 0; m < nMints; m++ ) if ( Gia_ManSimRelCompare(p, nWords, vSims, nWordsOut, vSimsOut, i, m) ) Abc_TtSetBit( Vec_WrdArray(vRel), i*nMints+m ); } Vec_Wrd_t * Gia_ManSimRel( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vVals ) { int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); int nMints = 1 << Vec_IntSize(vObjs), i, m, iObj; Gia_Obj_t * pObj; Vec_Wrd_t * vRel = Vec_WrdStart( nWords * nMints ); Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords * nMints ); Gia_ManSimRelAssignInputs( p, nWords * nMints, vSims, nWords, p->vSimsPi ); Vec_IntForEachEntry( vObjs, iObj, i ) for ( m = 0; m < nMints; m++ ) if ( (m >> i) & 1 ) memset( Vec_WrdEntryP(vSims, iObj*nMints*nWords + nWords*m), 0xFF, sizeof(word)*nWords ); else memset( Vec_WrdEntryP(vSims, iObj*nMints*nWords + nWords*m), 0x00, sizeof(word)*nWords ); Gia_ManCleanPhase( p ); Gia_ManForEachObjVec( vObjs, p, pObj, i ) pObj->fPhase = 1; Gia_ManForEachAnd( p, pObj, i ) if ( !pObj->fPhase ) Gia_ManSimPatSimAnd( p, i, pObj, nWords * nMints, vSims ); Gia_ManForEachCo( p, pObj, i ) if ( !pObj->fPhase ) Gia_ManSimPatSimPo( p, Gia_ObjId(p, pObj), pObj, nWords * nMints, vSims ); Gia_ManForEachObjVec( vObjs, p, pObj, i ) pObj->fPhase = 0; Gia_ManSimRelCollectOutputs( p, nWords * nMints, vSims, nWords, vVals, vRel ); Vec_WrdFree( vSims ); return vRel; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSimRelPrint( Gia_Man_t * p, Vec_Wrd_t * vRel, Vec_Int_t * vOutMints ) { int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); int nMints = Vec_WrdSize(vRel) / nWords; int i, k, m, Count; for ( i = 0; i < 64 * nWords; i++ ) { for ( k = 0; k < Gia_ManCiNum(p); k++ ) printf( "%d", Abc_TtGetBit( Vec_WrdEntryP(p->vSimsPi, k), i ) ); printf( " " ); Count = 0; for ( m = 0; m < nMints; m++ ) { printf( "%d", Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ) ); Count += Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ); } printf( " Count = %2d ", Count ); if ( vOutMints ) { printf( " %3d ", Vec_IntEntry(vOutMints, i) ); if ( Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+Vec_IntEntry(vOutMints, i) ) ) printf( "yes" ); else printf( "no" ); } printf( "\n" ); } } Vec_Int_t * Gia_ManSimPatStart( int nItems ) { Vec_Int_t * vValues = Vec_IntAlloc( nItems ); Vec_IntPush( vValues, 17 ); Vec_IntPush( vValues, 39 ); Vec_IntPush( vValues, 56 ); Vec_IntPush( vValues, 221 ); return vValues; } void Gia_ManSimRelTest( Gia_Man_t * p ) { //int nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); Vec_Int_t * vObjs = Gia_ManSimPatStart( 4 ); // can be CI/AND/CO Vec_Wrd_t * vVals = Gia_ManSimPatValues( p ); Vec_Wrd_t * vRel = Gia_ManSimRel( p, vObjs, vVals ); assert( p->vSimsPi != NULL ); Gia_ManSimRelPrint( p, vRel, NULL ); Vec_IntFree( vObjs ); Vec_WrdFree( vVals ); Vec_WrdFree( vRel ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Gia_Sim5CollectValues( word * pOffSet, word * pOnSet, int nWords ) { Vec_Int_t * vBits = Vec_IntAlloc( 64*nWords ); int i, Count[2] = {0}; for ( i = 0; i < 64*nWords; i++ ) if ( Abc_TtGetBit( pOffSet, i ) ) Vec_IntPush( vBits, 0 ), Count[0]++; else if ( Abc_TtGetBit( pOnSet, i ) ) Vec_IntPush( vBits, 1 ), Count[1]++; else Vec_IntPush( vBits, -1 ); //printf( "Offset = %d. Onset = %d. Dcset = %d.\n", Count[0], Count[1], 64*nWords - Count[0] - Count[1] ); return vBits; } Gia_SimAbsMan_t * Gia_SimAbsAlloc( Gia_Man_t * pGia, word * pOffSet, word * pOnSet, Vec_Wrd_t * vSims, int nWords, Vec_Int_t * vResub ) { Gia_SimAbsMan_t * p = ABC_CALLOC( Gia_SimAbsMan_t, 1 ); p->pGia = pGia; p->pSet[0] = pOffSet; p->pSet[1] = pOnSet; p->nCands = Vec_WrdSize(vSims)/nWords; p->nWords = nWords; p->vSims = vSims; p->vResub = vResub; p->vValues = Gia_Sim5CollectValues( pOffSet, pOnSet, nWords ); p->vPatPairs = Vec_IntAlloc( 100 ); p->vCoverTable = Vec_WrdAlloc( 10000 ); p->vTtMints = Vec_IntAlloc( 100 ); assert( Vec_WrdSize(vSims) % nWords == 0 ); return p; } void Gia_SimAbsFree( Gia_SimAbsMan_t * p ) { Vec_IntFree( p->vValues ); Vec_IntFree( p->vPatPairs ); Vec_WrdFree( p->vCoverTable ); Vec_IntFree( p->vTtMints ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_SimAbsCheckSolution( Gia_SimAbsMan_t * p ) { int x, y, z, w, fFound = 0; assert( Vec_WrdSize(p->vCoverTable) == p->nWordsTable * (p->nCands+1) ); Abc_TtClear( p->pTableTemp, p->nWordsTable ); for ( x = 0; x < Vec_IntSize(p->vPatPairs)/2; x++ ) Abc_TtXorBit( p->pTableTemp, x ); for ( x = 0; x < p->nCands; x++ ) { word * pSimTableX = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * x ); for ( w = 0; w < p->nWordsTable; w++ ) if ( p->pTableTemp[w] != pSimTableX[w] ) break; if ( w == p->nWordsTable ) { printf( "Found solution { %d }\n", x ); fFound = 1; } } if ( fFound ) return; for ( x = 0; x < p->nCands; x++ ) for ( y = 0; y < x; y++ ) { word * pSimTableX = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * x ); word * pSimTableY = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * y ); for ( w = 0; w < p->nWordsTable; w++ ) if ( p->pTableTemp[w] != (pSimTableX[w] | pSimTableY[w]) ) break; if ( w == p->nWordsTable ) { printf( "Found solution { %d %d }\n", y, x ); fFound = 1; } } if ( fFound ) return; for ( x = 0; x < p->nCands; x++ ) for ( y = 0; y < x; y++ ) for ( z = 0; z < y; z++ ) { word * pSimTableX = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * x ); word * pSimTableY = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * y ); word * pSimTableZ = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * z ); for ( w = 0; w < p->nWordsTable; w++ ) if ( p->pTableTemp[w] != (pSimTableX[w] | pSimTableY[w] | pSimTableZ[w]) ) break; if ( w == p->nWordsTable ) printf( "Found solution { %d %d %d }\n", z, y, x ); } } void Gia_SimAbsSolve( Gia_SimAbsMan_t * p ) { abctime clk = Abc_Clock(); int i, k, iPat, iPat2; /* Vec_Int_t * vSimPats = Vec_IntDup( p->vPatPairs ); Vec_IntUniqify( vSimPats ); printf( "Selected %d pattern pairs contain %d unique patterns.\n", Vec_IntSize(p->vPatPairs)/2, Vec_IntSize(vSimPats) ); Vec_IntFree( vSimPats ); */ // set up the covering problem p->nWordsTable = Abc_Bit6WordNum( Vec_IntSize(p->vPatPairs)/2 ); Vec_WrdFill( p->vCoverTable, p->nWordsTable * (p->nCands + 1), 0 ); p->pTableTemp = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * p->nCands ); for ( i = 0; i < p->nCands; i++ ) { word * pSimCand = Vec_WrdEntryP( p->vSims, p->nWords * i ); word * pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * i ); //printf( "%4d : ", i ); //Extra_PrintBinary( stdout, (word *)pSimCand, p->nCands ); printf( "\n" ); Vec_IntForEachEntryDouble( p->vPatPairs, iPat, iPat2, k ) { assert( Vec_IntEntry(p->vValues, iPat) == 0 ); assert( Vec_IntEntry(p->vValues, iPat2) == 1 ); if ( Abc_TtGetBit(pSimCand, iPat) != Abc_TtGetBit(pSimCand, iPat2) ) Abc_TtXorBit(pSimTable, k/2); } assert( k == Vec_IntSize(p->vPatPairs) ); } if ( 0 ) { printf( " " ); for ( i = 0; i < p->nCands; i++ ) printf( "%d", i % 10 ); printf( "\n" ); Vec_IntForEachEntryDouble( p->vPatPairs, iPat, iPat2, i ) { printf( "%4d ", i/2 ); printf( "%4d ", iPat ); printf( "%4d ", iPat2 ); for ( k = 0; k < p->nCands; k++ ) { word * pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * k ); printf( "%c", Abc_TtGetBit(pSimTable, i/2) ? '*' : ' ' ); } printf( "\n" ); } } //Gia_SimAbsCheckSolution(p); Vec_IntClear( p->vResub ); Abc_TtClear( p->pTableTemp, p->nWordsTable ); for ( i = 0; i < Vec_IntSize(p->vPatPairs)/2; i++ ) Abc_TtXorBit( p->pTableTemp, i ); while ( !Abc_TtIsConst0(p->pTableTemp, p->nWordsTable) ) { word * pSimTable; int iArgMax = -1, CostThis, CostMax = -1; // compute the cost of each column for ( i = 0; i < p->nCands; i++ ) { pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * i ); CostThis = Abc_TtCountOnesVecMask( pSimTable, p->pTableTemp, p->nWordsTable, 0 ); if ( CostMax >= CostThis ) continue; CostMax = CostThis; iArgMax = i; } // find the best column Vec_IntPush( p->vResub, iArgMax ); // delete values of this column pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * iArgMax ); Abc_TtSharp( p->pTableTemp, p->pTableTemp, pSimTable, p->nWordsTable ); } printf( "Solution %2d for covering problem [%5d x %5d]: ", Vec_IntSize(p->vResub), Vec_IntSize(p->vPatPairs)/2, p->nCands ); Vec_IntForEachEntry( p->vResub, iPat, i ) printf( "%4d ", iPat ); for ( ; i < 16; i++ ) printf( " " ); printf( " " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } int Gia_SimAbsRefine( Gia_SimAbsMan_t * p ) { int i, b, Value, iPat, iMint, iObj, Count = 0; word ** pFanins = ABC_ALLOC( word *, Vec_IntSize(p->vResub) ); assert( Vec_IntSize(p->vResub) > 0 ); Vec_IntForEachEntry( p->vResub, iObj, b ) pFanins[b] = Vec_WrdEntryP( p->vSims, p->nWords * iObj ); Vec_IntFill( p->vTtMints, 1 << Vec_IntSize(p->vResub), -1 ); Vec_IntForEachEntry( p->vValues, Value, i ) { if ( Value == -1 ) continue; iMint = 0; for ( b = 0; b < Vec_IntSize(p->vResub); b++ ) if ( Abc_TtGetBit(pFanins[b], i) ) iMint |= 1 << b; iPat = Vec_IntEntry( p->vTtMints, iMint ); if ( iPat == -1 ) { Vec_IntWriteEntry( p->vTtMints, iMint, i ); continue; } assert( Abc_TtGetBit(p->pSet[Value], i) ); if ( Abc_TtGetBit(p->pSet[Value], iPat) ) continue; assert( Abc_TtGetBit(p->pSet[!Value], iPat) ); Vec_IntPushTwo( p->vPatPairs, Value ? iPat : i, Value ? i : iPat ); //printf( "iPat1 = %d iPat2 = %d Mint = %d\n", Value ? iPat : i, Value ? i : iPat, iMint ); Count++; if ( Count == 64 ) return 1; } //printf( "Refinement added %d minterm pairs.\n", Count ); ABC_FREE( pFanins ); return Count != 0; } Vec_Int_t * Gia_SimAbsFind( Vec_Int_t * vValues, int Value ) { Vec_Int_t * vSubset = Vec_IntAlloc( 100 ); int i, Entry; Vec_IntForEachEntry( vValues, Entry, i ) if ( Entry == Value ) Vec_IntPush( vSubset, i ); return vSubset; } void Gia_SimAbsInit( Gia_SimAbsMan_t * p ) { int n, nPairsInit = 64; Vec_Int_t * vValue0 = Gia_SimAbsFind( p->vValues, 0 ); Vec_Int_t * vValue1 = Gia_SimAbsFind( p->vValues, 1 ); Vec_IntClear( p->vPatPairs ); printf( "There %d offset and %d onset minterms (%d pairs).\n", Vec_IntSize(vValue0), Vec_IntSize(vValue1), Vec_IntSize(vValue0)*Vec_IntSize(vValue1) ); Gia_ManRandom( 1 ); assert( Vec_IntSize(vValue0) > 0 ); assert( Vec_IntSize(vValue1) > 0 ); for ( n = 0; n < nPairsInit; n++ ) Vec_IntPushTwo( p->vPatPairs, Vec_IntEntry(vValue0, Gia_ManRandom(0) % Vec_IntSize(vValue0)), Vec_IntEntry(vValue1, Gia_ManRandom(0) % Vec_IntSize(vValue1)) ); Vec_IntFree( vValue0 ); Vec_IntFree( vValue1 ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Int_t * Gia_SimAbsPerformOne( Gia_Man_t * pGia, word * pOffSet, word * pOnSet, Vec_Wrd_t * vSimsCands, int nWords ) { Vec_Int_t * vResub = Vec_IntAlloc( 10 ); Gia_SimAbsMan_t * p = Gia_SimAbsAlloc( pGia, pOffSet, pOnSet, vSimsCands, nWords, vResub ); Gia_SimAbsInit( p ); while ( 1 ) { Gia_SimAbsSolve( p ); if ( !Gia_SimAbsRefine( p ) ) break; } Gia_SimAbsFree( p ); return vResub; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END