From e5d8335268eddf7d1bade6bfc8f91da677294674 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 5 Dec 2017 09:49:02 -0800 Subject: Experiments with AIG-based simulation. --- src/aig/gia/gia.h | 16 +++- src/aig/gia/giaCSat.c | 4 + src/aig/gia/giaSim.c | 235 ++++++++++++++++++++++++++++++++++++++++++++++++-- 3 files changed, 244 insertions(+), 11 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 20d64dfe..039628bf 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -203,6 +203,8 @@ struct Gia_Man_t_ int fBuiltInSim; int iPatsPi; int nSimWords; + int iPastPiMax; + int nSimWordsMax; Vec_Wrd_t * vSims; Vec_Wrd_t * vSimsPi; Vec_Int_t * vClassOld; @@ -692,7 +694,12 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 ) pObj->fPhase = (Gia_ObjPhase(pFan0) ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjPhase(pFan1) ^ Gia_ObjFaninC1(pObj)); } if ( p->fBuiltInSim ) + { + Gia_Obj_t * pFan0 = Gia_ObjFanin0(pObj); + Gia_Obj_t * pFan1 = Gia_ObjFanin1(pObj); + pObj->fPhase = (Gia_ObjPhase(pFan0) ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjPhase(pFan1) ^ Gia_ObjFaninC1(pObj)); Gia_ManBuiltInSimPerform( p, Gia_ObjId( p, pObj ) ); + } if ( p->vSuppWords ) Gia_ManQuantSetSuppAnd( p, pObj ); return Gia_ObjId( p, pObj ) << 1; @@ -1208,6 +1215,8 @@ extern Cbs_Man_t * Cbs_ManAlloc( Gia_Man_t * pGia ); extern void Cbs_ManStop( Cbs_Man_t * p ); extern int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); +extern void Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num ); +extern Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p ); /*=== giaCTas.c ============================================================*/ extern Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCof.c =============================================================*/ @@ -1504,8 +1513,11 @@ extern void Gia_ManSimInfoTransfer( Gia_ManSim_t * p ); extern void Gia_ManSimulateRound( Gia_ManSim_t * p ); extern void Gia_ManBuiltInSimStart( Gia_Man_t * p, int nWords, int nObjs ); extern void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj ); -extern int Gia_ManBuiltInSimCheck( Gia_Man_t * p, int iLit0, int iLit1 ); -extern int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs ); +extern int Gia_ManBuiltInSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 ); +extern int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 ); +extern void Gia_ManBuiltInSimResimulateCone( Gia_Man_t * p, int iLit0, int iLit1 ); +extern void Gia_ManBuiltInSimResimulate( Gia_Man_t * p ); +extern int Gia_ManBuiltInSimAddPat( Gia_Man_t * p, Vec_Int_t * vPat ); /*=== giaSpeedup.c ============================================================*/ extern float Gia_ManDelayTraceLut( Gia_Man_t * p ); extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose ); diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index 5f516e21..31f32e30 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -134,6 +134,10 @@ void Cbs_SetDefaultParams( Cbs_Par_t * pPars ) pPars->fUseMaxFF = 0; // use node with the largest fanin fanout pPars->fVerbose = 1; // print detailed statistics } +void Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num ) +{ + p->Pars.nBTLimit = Num; +} /**Function************************************************************* diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index aba7f712..192184c8 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "gia.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -760,51 +761,102 @@ void Gia_ManSimSimulatePattern( Gia_Man_t * p, char * pFileIn, char * pFileOut ) SeeAlso [] ***********************************************************************/ +static inline word * Gia_ManBuiltInDataPi( Gia_Man_t * p, int iCiId ) +{ + return Vec_WrdEntryP( p->vSimsPi, p->nSimWords * iCiId ); +} static inline word * Gia_ManBuiltInData( Gia_Man_t * p, int iObj ) { return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj ); } +static inline void Gia_ManBuiltInDataPrint( Gia_Man_t * p, int iObj ) +{ +// printf( "Obj %6d : ", iObj ); Extra_PrintBinary( stdout, Gia_ManBuiltInData(p, iObj), p->nSimWords * 64 ); printf( "\n" ); +} void Gia_ManBuiltInSimStart( Gia_Man_t * p, int nWords, int nObjs ) { int i, k; assert( !p->fBuiltInSim ); assert( Gia_ManAndNum(p) == 0 ); p->fBuiltInSim = 1; + p->iPatsPi = 0; + p->iPastPiMax = 0; p->nSimWords = nWords; + p->nSimWordsMax = 8; + Gia_ManRandomW( 1 ); + // init PI care info + p->vSimsPi = Vec_WrdAlloc( p->nSimWords * Gia_ManCiNum(p) ); + Vec_WrdFill( p->vSimsPi, p->nSimWords * Gia_ManCiNum(p), 0 ); + // init object sim info p->vSims = Vec_WrdAlloc( p->nSimWords * nObjs ); Vec_WrdFill( p->vSims, p->nSimWords, 0 ); - Gia_ManRandomW( 1 ); for ( i = 0; i < Gia_ManCiNum(p); i++ ) for ( k = 0; k < p->nSimWords; k++ ) Vec_WrdPush( p->vSims, Gia_ManRandomW(0) ); } -void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj ) +void Gia_ManBuiltInSimPerformInt( Gia_Man_t * p, int iObj ) { - Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); int w; + word * pInfo = Gia_ManBuiltInData( p, iObj ); word * pInfo0 = Gia_ManBuiltInData( p, Gia_ObjFaninId0(pObj, iObj) ); - word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) ); int w; + word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) ); assert( p->fBuiltInSim ); if ( Gia_ObjFaninC0(pObj) ) { if ( Gia_ObjFaninC1(pObj) ) for ( w = 0; w < p->nSimWords; w++ ) - Vec_WrdPush( p->vSims, ~(pInfo0[w] | pInfo1[w]) ); + pInfo[w] = ~(pInfo0[w] | pInfo1[w]); else for ( w = 0; w < p->nSimWords; w++ ) - Vec_WrdPush( p->vSims, ~pInfo0[w] & pInfo1[w] ); + pInfo[w] = ~pInfo0[w] & pInfo1[w]; } else { if ( Gia_ObjFaninC1(pObj) ) for ( w = 0; w < p->nSimWords; w++ ) - Vec_WrdPush( p->vSims, pInfo0[w] & ~pInfo1[w] ); + pInfo[w] = pInfo0[w] & ~pInfo1[w]; else for ( w = 0; w < p->nSimWords; w++ ) - Vec_WrdPush( p->vSims, pInfo0[w] & pInfo1[w] ); + pInfo[w] = pInfo0[w] & pInfo1[w]; } assert( Vec_WrdSize(p->vSims) == Gia_ManObjNum(p) * p->nSimWords ); } -int Gia_ManBuiltInSimCheck( Gia_Man_t * p, int iLit0, int iLit1 ) +void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj ) +{ + int w; + for ( w = 0; w < p->nSimWords; w++ ) + Vec_WrdPush( p->vSims, 0 ); + Gia_ManBuiltInSimPerformInt( p, iObj ); +} + +void Gia_ManBuiltInSimResimulateCone_rec( Gia_Man_t * p, int iObj ) +{ + Gia_Obj_t * pObj; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return; + Gia_ObjSetTravIdCurrentId(p, iObj); + pObj = Gia_ManObj( p, iObj ); + if ( Gia_ObjIsCi(pObj) ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManBuiltInSimResimulateCone_rec( p, Gia_ObjFaninId0(pObj, iObj) ); + Gia_ManBuiltInSimResimulateCone_rec( p, Gia_ObjFaninId1(pObj, iObj) ); + Gia_ManBuiltInSimPerformInt( p, iObj ); +} +void Gia_ManBuiltInSimResimulateCone( Gia_Man_t * p, int iLit0, int iLit1 ) +{ + Gia_ManIncrementTravId( p ); + Gia_ManBuiltInSimResimulateCone_rec( p, Abc_Lit2Var(iLit0) ); + Gia_ManBuiltInSimResimulateCone_rec( p, Abc_Lit2Var(iLit1) ); +} +void Gia_ManBuiltInSimResimulate( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; int iObj; + Gia_ManForEachAnd( p, pObj, iObj ) + Gia_ManBuiltInSimPerformInt( p, iObj ); +} + +int Gia_ManBuiltInSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 ) { word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) ); word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w; @@ -818,28 +870,193 @@ int Gia_ManBuiltInSimCheck( Gia_Man_t * p, int iLit0, int iLit1 ) if ( Abc_LitIsCompl(iLit0) ) { if ( Abc_LitIsCompl(iLit1) ) + { for ( w = 0; w < p->nSimWords; w++ ) if ( ~pInfo0[w] & ~pInfo1[w] ) return 1; + } else + { for ( w = 0; w < p->nSimWords; w++ ) if ( ~pInfo0[w] & pInfo1[w] ) return 1; + } } else { if ( Abc_LitIsCompl(iLit1) ) + { for ( w = 0; w < p->nSimWords; w++ ) if ( pInfo0[w] & ~pInfo1[w] ) return 1; + } else + { for ( w = 0; w < p->nSimWords; w++ ) if ( pInfo0[w] & pInfo1[w] ) return 1; + } } return 0; } +int Gia_ManBuiltInSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 ) +{ + word * pInfo0 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit0) ); + word * pInfo1 = Gia_ManBuiltInData( p, Abc_Lit2Var(iLit1) ); int w; + assert( p->fBuiltInSim ); + +// printf( "%d %d\n", Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) ); +// Extra_PrintBinary( stdout, pInfo0, 64*p->nSimWords ); printf( "\n" ); +// Extra_PrintBinary( stdout, pInfo1, 64*p->nSimWords ); printf( "\n" ); +// printf( "\n" ); + + if ( Abc_LitIsCompl(iLit0) ) + { + if ( Abc_LitIsCompl(iLit1) ) + { + for ( w = 0; w < p->nSimWords; w++ ) + if ( ~pInfo0[w] != ~pInfo1[w] ) + return 0; + } + else + { + for ( w = 0; w < p->nSimWords; w++ ) + if ( ~pInfo0[w] != pInfo1[w] ) + return 0; + } + } + else + { + if ( Abc_LitIsCompl(iLit1) ) + { + for ( w = 0; w < p->nSimWords; w++ ) + if ( pInfo0[w] != ~pInfo1[w] ) + return 0; + } + else + { + for ( w = 0; w < p->nSimWords; w++ ) + if ( pInfo0[w] != pInfo1[w] ) + return 0; + } + } + return 1; +} +int Gia_ManBuiltInSimPack( Gia_Man_t * p, Vec_Int_t * vPat ) +{ + int i, k, iLit; + assert( Vec_IntSize(vPat) > 0 ); + //printf( "%d ", Vec_IntSize(vPat) ); + for ( i = 0; i < p->iPatsPi; i++ ) + { + Vec_IntForEachEntry( vPat, iLit, k ) + if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), i) && + Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), i) == Abc_LitIsCompl(iLit) ) + break; + if ( k == Vec_IntSize(vPat) ) + return i; // success + } + return -1; // failure +} +// adds PI pattern to storage; the pattern comes in terms of CiIds +int Gia_ManBuiltInSimAddPat( Gia_Man_t * p, Vec_Int_t * vPat ) +{ + int Period = 0xF; + int fOverflow = p->iPatsPi == 64 * p->nSimWords && p->nSimWords == p->nSimWordsMax; + int k, iLit, iPat = Gia_ManBuiltInSimPack( p, vPat ); + if ( iPat == -1 ) + { + if ( fOverflow ) + { + if ( (p->iPastPiMax & Period) == 0 ) + Gia_ManBuiltInSimResimulate( p ); + iPat = p->iPastPiMax; + //if ( p->iPastPiMax == 64 * p->nSimWordsMax - 1 ) + // printf( "Completed the cycle.\n" ); + p->iPastPiMax = p->iPastPiMax == 64 * p->nSimWordsMax - 1 ? 0 : p->iPastPiMax + 1; + } + else + { + if ( p->iPatsPi && (p->iPatsPi & Period) == 0 ) + Gia_ManBuiltInSimResimulate( p ); + if ( p->iPatsPi == 64 * p->nSimWords ) + { + Vec_Wrd_t * vTemp = Vec_WrdAlloc( 2 * Vec_WrdSize(p->vSims) ); + word Data; int w, Count = 0, iObj = 0; + Vec_WrdForEachEntry( p->vSims, Data, w ) + { + Vec_WrdPush( vTemp, Data ); + if ( ++Count == p->nSimWords ) + { + Gia_Obj_t * pObj = Gia_ManObj(p, iObj++); + if ( Gia_ObjIsCi(pObj) ) + Vec_WrdPush( vTemp, Gia_ManRandomW(0) ); // Vec_WrdPush( vTemp, 0 ); + else if ( Gia_ObjIsAnd(pObj) ) + Vec_WrdPush( vTemp, pObj->fPhase ? ~(word)0 : 0 ); + else + Vec_WrdPush( vTemp, 0 ); + Count = 0; + } + } + assert( iObj == Gia_ManObjNum(p) ); + Vec_WrdFree( p->vSims ); + p->vSims = vTemp; + + vTemp = Vec_WrdAlloc( 2 * Vec_WrdSize(p->vSimsPi) ); + Count = 0; + Vec_WrdForEachEntry( p->vSimsPi, Data, w ) + { + Vec_WrdPush( vTemp, Data ); + if ( ++Count == p->nSimWords ) + { + Vec_WrdPush( vTemp, 0 ); + Count = 0; + } + } + Vec_WrdFree( p->vSimsPi ); + p->vSimsPi = vTemp; + + // update the word count + p->nSimWords++; + assert( Vec_WrdSize(p->vSims) == p->nSimWords * Gia_ManObjNum(p) ); + assert( Vec_WrdSize(p->vSimsPi) == p->nSimWords * Gia_ManCiNum(p) ); + //printf( "Resizing to %d words.\n", p->nSimWords ); + } + iPat = p->iPatsPi++; + } + } + assert( iPat >= 0 && iPat < p->iPatsPi ); + // add literals + if ( fOverflow ) + { + int iVar; + Vec_IntForEachEntry( &p->vSuppVars, iVar, k ) + if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, iVar), iPat) ) + Abc_TtXorBit(Gia_ManBuiltInDataPi(p, iVar), iPat); + Vec_IntForEachEntry( vPat, iLit, k ) + { + if ( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) == Abc_LitIsCompl(iLit) ) + Abc_TtXorBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat); + Abc_TtXorBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat); + } + } + else + { + Vec_IntForEachEntry( vPat, iLit, k ) + { + if ( Abc_TtGetBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat) ) + assert( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) != Abc_LitIsCompl(iLit) ); + else + { + if ( Abc_TtGetBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat) == Abc_LitIsCompl(iLit) ) + Abc_TtXorBit(Gia_ManBuiltInData(p, 1+Abc_Lit2Var(iLit)), iPat); + Abc_TtXorBit(Gia_ManBuiltInDataPi(p, Abc_Lit2Var(iLit)), iPat); + } + } + } + return 1; +} /**Function************************************************************* -- cgit v1.2.3