diff options
| -rw-r--r-- | src/aig/gia/giaSim.c | 297 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 71 |
2 files changed, 366 insertions, 2 deletions
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index cb10507e..564be76c 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -1361,6 +1361,7 @@ Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCex 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) ); @@ -1550,7 +1551,7 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose ) assert( Status >= -1 && Status <= 1 ); Counts[Status+1]++; } - printf( "Total = %d : SAT = %d. UNSAT = %d. UNDEC = %d.\n", Gia_ManCoNum(p), Counts[1], Counts[2], Counts[0] ); + 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 @@ -1562,6 +1563,300 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose ) } Vec_StrFree( vStatus ); Vec_IntFree( vCexStore ); + Vec_WrdFree( vSims ); +} + + + + + +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]; +}; + +/**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; + 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 ) +{ + 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( "Resubstitution is possible for %d nodes (%.2f %% out of %d) (Bufs = %d Invs = %d)\n", + nCount, 100.0*nCount/Gia_ManAndNum(pGia), Gia_ManAndNum(pGia), nBufs, nInvs ); + Gia_SimRsbFree( p ); + return nCount; } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f6fc7ea6..6a852bf7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -414,6 +414,7 @@ static int Abc_CommandAbc9Sim3 ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9ReadSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9WriteSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SimPat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9SimRsb ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Resim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SpecI ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Equiv ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1126,6 +1127,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&read_sim", Abc_CommandAbc9ReadSim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&write_sim", Abc_CommandAbc9WriteSim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&simpat", Abc_CommandAbc9SimPat, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&simrsb", Abc_CommandAbc9SimRsb, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&resim", Abc_CommandAbc9Resim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&speci", Abc_CommandAbc9SpecI, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&equiv", Abc_CommandAbc9Equiv, 0 ); @@ -32687,7 +32689,7 @@ int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia->vSimsPi == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9WriteSim(): Does not have simulation information available.\n" ); + Abc_Print( -1, "Abc_CommandAbc9SimPat(): Does not have simulation information available.\n" ); return 0; } Gia_ManSimPat( pAbc->pGia, nWords, fVerbose ); @@ -32713,6 +32715,73 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9SimRsb( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Gia_ManSimRsb( Gia_Man_t * p, int nCands, int fVerbose ); + int c, nCands = 32, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nCands = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCands < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9SimRsb(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pGia) > 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9SimRsb(): This command works only for combinational AIGs.\n" ); + return 0; + } + if ( pAbc->pGia->vSimsPi == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9SimRsb(): Does not have simulation information available.\n" ); + return 0; + } + Gia_ManSimRsb( pAbc->pGia, nCands, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: &simrsb [-N num] [-vh]\n" ); + Abc_Print( -2, "\t performs resubstitution\n" ); + Abc_Print( -2, "\t-C num : the number of candidates to try [default = %d]\n", nCands ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9Resim( Abc_Frame_t * pAbc, int argc, char ** argv ) { Cec_ParSim_t Pars, * pPars = &Pars; |