diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-11-06 16:43:32 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-11-06 16:43:32 -0800 |
commit | 716969190a4d6d944cfa24a085c9e7069d868dab (patch) | |
tree | 1a0a95bd9dfc505341c367752658c732900e55de /src/aig | |
parent | 94a575a5b3113d714b96ba3711124c5780151bee (diff) | |
download | abc-716969190a4d6d944cfa24a085c9e7069d868dab.tar.gz abc-716969190a4d6d944cfa24a085c9e7069d868dab.tar.bz2 abc-716969190a4d6d944cfa24a085c9e7069d868dab.zip |
Profiling quantification and other changes.
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/gia.h | 11 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaSim.c | 148 | ||||
-rw-r--r-- | src/aig/gia/giaUtil.c | 52 |
4 files changed, 212 insertions, 1 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 9acbbe48..920ebb06 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -198,6 +198,7 @@ struct Gia_Man_t_ int MappedArea; // area after mapping int MappedDelay; // delay after mapping // bit-parallel simulation + int fBuiltInSim; int iPatsPi; int nSimWords; Vec_Wrd_t * vSims; @@ -673,6 +674,11 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 ) if ( pFan1->fMark0 ) pFan1->fMark1 = 1; else pFan1->fMark0 = 1; pObj->fPhase = (Gia_ObjPhase(pFan0) ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjPhase(pFan1) ^ Gia_ObjFaninC1(pObj)); } + if ( p->fBuiltInSim ) + { + extern void Gia_ManBuiltInSimPerform( Gia_Man_t * p, int iObj ); + Gia_ManBuiltInSimPerform( p, Gia_ObjId( p, pObj ) ); + } return Gia_ObjId( p, pObj ) << 1; } static inline int Gia_ManAppendXorReal( Gia_Man_t * p, int iLit0, int iLit1 ) @@ -1469,6 +1475,10 @@ extern unsigned * Gia_SimDataCoExt( Gia_ManSim_t * p, int i ); extern void Gia_ManSimInfoInit( Gia_ManSim_t * p ); 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 ); /*=== giaSpeedup.c ============================================================*/ extern float Gia_ManDelayTraceLut( Gia_Man_t * p ); extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose ); @@ -1612,6 +1622,7 @@ extern void Gia_ManSwapPos( Gia_Man_t * p, int i ); extern Vec_Int_t * Gia_ManSaveValue( Gia_Man_t * p ); extern void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues ); extern Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p ); +extern int Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, int iNode2 ); /*=== giaCTas.c ===========================================================*/ typedef struct Tas_Man_t_ Tas_Man_t; diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 1d4f7a22..977ef42c 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1909,7 +1909,7 @@ Gia_Man_t * Gia_ManDupConeSupp( Gia_Man_t * p, int iLit, Vec_Int_t * vCiIds ) Gia_Man_t * pNew; int i, iLit0; Gia_Obj_t * pObj, * pRoot = Gia_ManObj( p, Abc_Lit2Var(iLit) ); Vec_Int_t * vObjs = Vec_IntAlloc( 1000 ); - assert( Gia_ObjIsAnd(pRoot) ); + //assert( Gia_ObjIsAnd(pRoot) ); if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) ) Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 90224062..aba7f712 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -748,6 +748,154 @@ void Gia_ManSimSimulatePattern( Gia_Man_t * p, char * pFileIn, char * pFileOut ) Vec_IntFree( vPatOut ); } + +/**Function************************************************************* + + Synopsis [Bit-parallel simulation during AIG construction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline word * Gia_ManBuiltInData( Gia_Man_t * p, int iObj ) +{ + return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj ); +} +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->nSimWords = nWords; + 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 ) +{ + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + word * pInfo0 = Gia_ManBuiltInData( p, Gia_ObjFaninId0(pObj, iObj) ); + word * pInfo1 = Gia_ManBuiltInData( p, Gia_ObjFaninId1(pObj, iObj) ); int w; + 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]) ); + else + for ( w = 0; w < p->nSimWords; w++ ) + Vec_WrdPush( p->vSims, ~pInfo0[w] & pInfo1[w] ); + } + else + { + if ( Gia_ObjFaninC1(pObj) ) + for ( w = 0; w < p->nSimWords; w++ ) + Vec_WrdPush( p->vSims, pInfo0[w] & ~pInfo1[w] ); + else + for ( w = 0; w < p->nSimWords; w++ ) + Vec_WrdPush( p->vSims, 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 ) +{ + 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 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; +} + + +/**Function************************************************************* + + Synopsis [Finds a satisfying assignment.] + + Description [Returns 1 if a sat assignment is found; 0 otherwise.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManObjCheckSat_rec( Gia_Man_t * p, int iLit, Vec_Int_t * vObjs ) +{ + int iObj = Abc_Lit2Var(iLit); + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + if ( pObj->fMark0 ) + return pObj->fMark1 == (unsigned)Abc_LitIsCompl(iLit); + pObj->fMark0 = 1; + pObj->fMark1 = Abc_LitIsCompl(iLit); + Vec_IntPush( vObjs, iObj ); + if ( Gia_ObjIsAnd(pObj) ) + { + if ( pObj->fMark1 == 0 ) // node value is 1 + { + if ( !Gia_ManObjCheckSat_rec( p, Gia_ObjFaninLit0(pObj, iObj), vObjs ) ) return 0; + if ( !Gia_ManObjCheckSat_rec( p, Gia_ObjFaninLit1(pObj, iObj), vObjs ) ) return 0; + } + else + { + if ( !Gia_ManObjCheckSat_rec( p, Abc_LitNot(Gia_ObjFaninLit0(pObj, iObj)), vObjs ) ) return 0; + } + } + return 1; +} +int Gia_ManObjCheckOverlap1( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs ) +{ + Gia_Obj_t * pObj; + int i, Res0, Res1 = 0; +// Gia_ManForEachObj( p, pObj, i ) +// assert( pObj->fMark0 == 0 && pObj->fMark1 == 0 ); + Vec_IntClear( vObjs ); + Res0 = Gia_ManObjCheckSat_rec( p, iLit0, vObjs ); + if ( Res0 ) + Res1 = Gia_ManObjCheckSat_rec( p, iLit1, vObjs ); + Gia_ManForEachObjVec( vObjs, p, pObj, i ) + pObj->fMark0 = pObj->fMark1 = 0; + return Res0 && Res1; +} +int Gia_ManObjCheckOverlap( Gia_Man_t * p, int iLit0, int iLit1, Vec_Int_t * vObjs ) +{ + if ( Gia_ManObjCheckOverlap1( p, iLit0, iLit1, vObjs ) ) + return 1; + return Gia_ManObjCheckOverlap1( p, iLit1, iLit0, vObjs ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 1c1edda7..204d3033 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -2075,6 +2075,58 @@ void Gia_DumpLutSizeDistrib( Gia_Man_t * p, char * pFileName ) fclose( pTable ); } +/**Function************************************************************* + + Synopsis [Check if two logic cones have overlap.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCheckSuppMark_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( pObj->fMark0 ) + return; + pObj->fMark0 = 1; + if ( Gia_ObjIsCi(pObj) ) + return; + Gia_ManCheckSuppMark_rec( p, Gia_ObjFanin0(pObj) ); + Gia_ManCheckSuppMark_rec( p, Gia_ObjFanin1(pObj) ); +} +void Gia_ManCheckSuppUnmark_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( !pObj->fMark0 ) + return; + pObj->fMark0 = 0; + if ( Gia_ObjIsCi(pObj) ) + return; + Gia_ManCheckSuppUnmark_rec( p, Gia_ObjFanin0(pObj) ); + Gia_ManCheckSuppUnmark_rec( p, Gia_ObjFanin1(pObj) ); +} +int Gia_ManCheckSupp_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( pObj->fMark0 ) + return 1; + if ( Gia_ObjIsCi(pObj) ) + return 0; + if ( Gia_ManCheckSupp_rec( p, Gia_ObjFanin0(pObj) ) ) + return 1; + return Gia_ManCheckSupp_rec( p, Gia_ObjFanin1(pObj) ); +} +int Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, int iNode2 ) +{ + int Result; + if ( iNode1 == 0 || iNode2 == 0 ) + return 0; + Gia_ManCheckSuppMark_rec( p, Gia_ManObj(p, iNode1) ); + Result = Gia_ManCheckSupp_rec( p, Gia_ManObj(p, iNode2) ); + Gia_ManCheckSuppUnmark_rec( p, Gia_ManObj(p, iNode1) ); + return Result; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |