diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
-rw-r--r-- | src/aig/gia/giaMan.c | 1 | ||||
-rw-r--r-- | src/proof/abs/absRpm.c | 340 |
3 files changed, 314 insertions, 28 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 0c98e94d..446f3e4f 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -135,6 +135,7 @@ struct Gia_Man_t_ Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc Vec_Int_t * vGateClasses; // classes of gates for abstraction Vec_Int_t * vObjClasses; // classes of objects for abstraction + Vec_Int_t * vDoms; // dominators unsigned char* pSwitching; // switching activity for each object Gia_Plc_t * pPlacement; // placement of the objects int * pTravIds; // separate traversal ID representation diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 6b57e292..e7b831bd 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -85,6 +85,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vFlopClasses ); Vec_IntFreeP( &p->vGateClasses ); Vec_IntFreeP( &p->vObjClasses ); + Vec_IntFreeP( &p->vDoms ); Vec_IntFreeP( &p->vLevels ); Vec_IntFreeP( &p->vTruths ); Vec_StrFreeP( &p->vTtNums ); diff --git a/src/proof/abs/absRpm.c b/src/proof/abs/absRpm.c index dbd3b628..7ef314ea 100644 --- a/src/proof/abs/absRpm.c +++ b/src/proof/abs/absRpm.c @@ -26,12 +26,190 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static inline int Gia_ObjDom( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vDoms, Gia_ObjId(p, pObj)); } +static inline void Gia_ObjSetDom( Gia_Man_t * p, Gia_Obj_t * pObj, int d ) { Vec_IntWriteEntry(p->vDoms, Gia_ObjId(p, pObj), d); } + +static int Abs_ManSupport( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ); +static int Abs_GiaObjDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode ); +static int Abs_GiaObjRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [Collects non-trivial internal dominators of the PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManCollectDoms( Gia_Man_t * p ) +{ + Vec_Int_t * vNodes; + Gia_Obj_t * pObj; + int Level, LevelMax = 2; + int i, iDom, iDomNext; + vNodes = Vec_IntAlloc( 100 ); + Gia_ManForEachObj( p, pObj, i ) + { + if ( !pObj->fMark0 ) + continue; + iDom = Gia_ObjDom(p, pObj); + if ( iDom == Gia_ObjId(p, pObj) ) + continue; + for ( Level = 0; Level < LevelMax && Gia_ObjIsAnd( Gia_ManObj(p, iDom) ); Level++ ) + { + Vec_IntPush( vNodes, iDom ); + iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom) ); + if ( iDomNext == iDom ) + break; + iDom = iDomNext; + } + } + Vec_IntUniqify( vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Computes one-node dominators.] + + Description [For each node, computes the closest one-node dominator, + which can be the node itself if the node has no other dominators.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAddDom( Gia_Man_t * p, Gia_Obj_t * pObj, int iDom0 ) +{ + int iDom1, iDomNext; + if ( Gia_ObjDom(p, pObj) == -1 ) + { + Gia_ObjSetDom( p, pObj, iDom0 ); + return; + } + iDom1 = Gia_ObjDom( p, pObj ); + while ( 1 ) + { + if ( iDom0 > iDom1 ) + { + iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom1) ); + if ( iDomNext == iDom1 ) + break; + iDom1 = iDomNext; + continue; + } + if ( iDom1 > iDom0 ) + { + iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom0) ); + if ( iDomNext == iDom0 ) + break; + iDom0 = iDomNext; + continue; + } + assert( iDom0 == iDom1 ); + Gia_ObjSetDom( p, pObj, iDom0 ); + return; + } + Gia_ObjSetDom( p, pObj, Gia_ObjId(p, pObj) ); +} +void Gia_ManComputeDoms( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i; + if ( p->vDoms == NULL ) + p->vDoms = Vec_IntAlloc( 0 ); + Vec_IntFill( p->vDoms, Gia_ManObjNum(p), -1 ); + Gia_ManForEachObjReverse( p, pObj, i ) + { + if ( i == 0 || Gia_ObjIsCi(pObj) ) + continue; + if ( pObj->fMark0 || (p->pRefs && Gia_ObjRefs(p, pObj) == 0) ) + continue; + if ( Gia_ObjIsCo(pObj) ) + { + Gia_ObjSetDom( p, pObj, i ); + Gia_ManAddDom( p, Gia_ObjFanin0(pObj), i ); + continue; + } + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManAddDom( p, Gia_ObjFanin0(pObj), i ); + Gia_ManAddDom( p, Gia_ObjFanin1(pObj), i ); + } +} +void Gia_ManTestDoms2( Gia_Man_t * p ) +{ + Vec_Int_t * vNodes; + Gia_Obj_t * pObj, * pDom; + clock_t clk = clock(); + int i; + assert( p->vDoms == NULL ); + Gia_ManComputeDoms( p ); +/* + Gia_ManForEachPi( p, pObj, i ) + if ( Gia_ObjId(p, pObj) != Gia_ObjDom(p, pObj) ) + printf( "PI =%6d Id =%8d. Dom =%8d.\n", i, Gia_ObjId(p, pObj), Gia_ObjDom(p, pObj) ); +*/ + Abc_PrintTime( 1, "Time", clock() - clk ); + // for each dominated PI, when if the PIs is in a leaf of the MFFC of the dominator + Gia_ManCleanMark0( p ); + Gia_ManForEachPi( p, pObj, i ) + pObj->fMark0 = 1; + vNodes = Vec_IntAlloc( 100 ); + Gia_ManCreateRefs( p ); + Gia_ManForEachPi( p, pObj, i ) + { + if ( Gia_ObjId(p, pObj) == Gia_ObjDom(p, pObj) ) + continue; + + pDom = Gia_ManObj(p, Gia_ObjDom(p, pObj)); + if ( Gia_ObjIsCo(pDom) ) + { + assert( Gia_ObjFanin0(pDom) == pObj ); + continue; + } + assert( Gia_ObjIsAnd(pDom) ); + Abs_GiaObjDeref_rec( p, pDom ); + Abs_ManSupport( p, pDom, vNodes ); + Abs_GiaObjRef_rec( p, pDom ); + + if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) == -1 ) + printf( "FAILURE.\n" ); +// else +// printf( "Success.\n" ); + } + Vec_IntFree( vNodes ); + Gia_ManCleanMark0( p ); +} + +void Gia_ManTestDoms( Gia_Man_t * p ) +{ + Vec_Int_t * vNodes; + Gia_Obj_t * pObj; + int i; + assert( p->vDoms == NULL ); + Gia_ManComputeDoms( p ); + // for each dominated PI, when if the PIs is in a leaf of the MFFC of the dominator + Gia_ManCleanMark0( p ); + Gia_ManForEachPi( p, pObj, i ) + pObj->fMark0 = 1; + vNodes = Gia_ManCollectDoms( p ); +// Vec_IntPrint( vNodes ); + printf( "Nodes = %d. Doms = %d.\n", Gia_ManAndNum(p), Vec_IntSize(vNodes) ); + Vec_IntFree( vNodes ); + Gia_ManCleanMark0( p ); +} + + +/**Function************************************************************* + Synopsis [] Description [] @@ -41,22 +219,22 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -void Gia_ManCountPisNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnPis, int * pnNodes ) +void Gia_ManCountPisNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPis, Vec_Int_t * vAnds ) { if ( Gia_ObjIsTravIdCurrent(p, pObj) ) return; Gia_ObjSetTravIdCurrent(p, pObj); if ( pObj->fMark0 ) { - (*pnPis)++; + Vec_IntPush( vPis, Gia_ObjId(p, pObj) ); return; } assert( Gia_ObjIsAnd(pObj) ); - Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), pnPis, pnNodes ); - Gia_ManCountPisNodes_rec( p, Gia_ObjFanin1(pObj), pnPis, pnNodes ); - (*pnNodes)++; + Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), vPis, vAnds ); + Gia_ManCountPisNodes_rec( p, Gia_ObjFanin1(pObj), vPis, vAnds ); + Vec_IntPush( vAnds, Gia_ObjId(p, pObj) ); } -void Gia_ManCountPisNodes( Gia_Man_t * p, int * pnPis, int * pnNodes ) +void Gia_ManCountPisNodes( Gia_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vAnds ) { Gia_Obj_t * pObj; int i; @@ -66,9 +244,10 @@ void Gia_ManCountPisNodes( Gia_Man_t * p, int * pnPis, int * pnNodes ) Gia_ManForEachRo( p, pObj, i ) Gia_ObjSetTravIdCurrent( p, pObj ); // count PIs and internal nodes reachable from COs - *pnPis = *pnNodes = 0; + Vec_IntClear( vPis ); + Vec_IntClear( vAnds ); Gia_ManForEachCo( p, pObj, i ) - Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), pnPis, pnNodes ); + Gia_ManCountPisNodes_rec( p, Gia_ObjFanin0(pObj), vPis, vAnds ); } /**Function************************************************************* @@ -82,7 +261,7 @@ void Gia_ManCountPisNodes( Gia_Man_t * p, int * pnPis, int * pnNodes ) SeeAlso [] ***********************************************************************/ -void Abs_ManSupport_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ) +void Abs_ManSupport2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ) { if ( Gia_ObjIsTravIdCurrent(p, pObj) ) return; @@ -93,6 +272,40 @@ void Abs_ManSupport_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ) return; } assert( Gia_ObjIsAnd(pObj) ); + Abs_ManSupport2_rec( p, Gia_ObjFanin0(pObj), vSupp ); + Abs_ManSupport2_rec( p, Gia_ObjFanin1(pObj), vSupp ); +} +int Abs_ManSupport2( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ) +{ + assert( Gia_ObjIsAnd(pObj) ); + Vec_IntClear( vSupp ); + Gia_ManIncrementTravId( p ); + Abs_ManSupport2_rec( p, pObj, vSupp ); + return Vec_IntSize(vSupp); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abs_ManSupport_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( pObj->fMark0 || Gia_ObjIsRo(p, pObj) || Gia_ObjRefs(p, pObj) > 0 ) + { + Vec_IntPush( vSupp, Gia_ObjId(p, pObj) ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); Abs_ManSupport_rec( p, Gia_ObjFanin0(pObj), vSupp ); Abs_ManSupport_rec( p, Gia_ObjFanin1(pObj), vSupp ); } @@ -101,7 +314,8 @@ int Abs_ManSupport( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ) assert( Gia_ObjIsAnd(pObj) ); Vec_IntClear( vSupp ); Gia_ManIncrementTravId( p ); - Abs_ManSupport_rec( p, pObj, vSupp ); + Abs_ManSupport_rec( p, Gia_ObjFanin0(pObj), vSupp ); + Abs_ManSupport_rec( p, Gia_ObjFanin1(pObj), vSupp ); return Vec_IntSize(vSupp); } @@ -167,7 +381,10 @@ int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp ) int i, RetValue; Gia_ManForEachObjVec( vSupp, p, pObj, i ) if ( i < nSize && Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj) ) // add removable leaves + { + assert( pObj->fMark0 ); Vec_IntPush( vSupp, Gia_ObjId(p, pObj) ); + } RetValue = Vec_IntSize(vSupp) - nSize; Gia_ManForEachObjVec( vSupp, p, pObj, i ) if ( i < nSize && !(Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj)) ) // add non-removable leaves @@ -296,16 +513,18 @@ word Abs_GiaComputeTruth( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Ve ***********************************************************************/ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose ) { - Vec_Int_t * vSupp; + Vec_Int_t * vSupp, * vPis, * vAnds; Vec_Wrd_t * vTruths; Gia_Obj_t * pObj; word uTruth; - int Iter, i, nPis, nNodes, nSize0; + int Iter, i, nSize0; int fChanges = 1; Gia_ManCreateRefs( p ); Gia_ManCleanMark0( p ); Gia_ManForEachPi( p, pObj, i ) pObj->fMark0 = 1; + vPis = Vec_IntAlloc( 100 ); + vAnds = Vec_IntAlloc( 100 ); vSupp = Vec_IntAlloc( 100 ); vTruths = Vec_WrdAlloc( 100 ); for ( Iter = 0; fChanges; Iter++ ) @@ -313,16 +532,16 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose ) // count the number of PIs and internal nodes if ( fVerbose ) { - Gia_ManCountPisNodes( p, &nPis, &nNodes ); + Gia_ManCountPisNodes( p, vPis, vAnds ); printf( "Iter %3d : ", Iter ); - printf( "PI = %5d ", nPis ); - printf( "And = %6d ", nNodes ); + printf( "PI = %5d ", Vec_IntSize(vPis) ); + printf( "And = %6d ", Vec_IntSize(vAnds) ); printf( "\n" ); } fChanges = 0; Gia_ManCleanMark1( p ); -// pObj = Gia_ObjFanin0( Gia_ManPo(p, 0) ); +// pObj = Gia_ObjFanin0( Gia_ManPo(p, 1) ); Gia_ManForEachAnd( p, pObj, i ) { if ( pObj->fMark0 ) @@ -334,18 +553,22 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose ) pObj->fMark1 = 1; continue; } - if ( Abs_ManSupport(p, pObj, vSupp) > nCutMax ) + + // dereference nodes + Abs_GiaObjDeref_rec( p, pObj ); + // compute support + Abs_ManSupport( p, pObj, vSupp ); + // check support size + if ( Vec_IntSize(vSupp) > nCutMax ) { + Abs_GiaObjRef_rec( p, pObj ); pObj->fMark1 = 1; continue; } - - // pObj has structural support no more than nCutMax - Abs_GiaObjDeref_rec( p, pObj ); - // sort support nodes by ref count + // order nodes by their ref counts nSize0 = Abs_GiaSortNodes( p, vSupp ); - // check how many support nodes have ref count 0 - if ( nSize0 == 0 ) + // quit if there is no removable or too many + if ( nSize0 == 0 || nSize0 > nCutMax ) { Abs_GiaObjRef_rec( p, pObj ); continue; @@ -358,30 +581,91 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose ) if ( !Abs_GiaCheckTruth( &uTruth, Vec_IntSize(vSupp), nSize0 ) ) // has const { Abs_GiaObjRef_rec( p, pObj ); -// printf( " no\n" ); +/* + if ( Iter == 1 ) + { + printf( "Node = %8d Supp = %2d Supp0 = %2d ", Gia_ObjId(p, pObj), Vec_IntSize(vSupp), nSize0 ); + Extra_PrintHex( stdout, &uTruth, Vec_IntSize(vSupp) ); + printf( " no\n" ); + } +*/ continue; } +/* printf( "Node = %8d Supp = %2d Supp0 = %2d ", Gia_ObjId(p, pObj), Vec_IntSize(vSupp), nSize0 ); Extra_PrintHex( stdout, &uTruth, Vec_IntSize(vSupp) ); printf( " yes\n" ); - +*/ // pObj can be reparamed pObj->fMark0 = 1; fChanges = 1; } } + Vec_IntFree( vPis ); + Vec_IntFree( vAnds ); Vec_IntFree( vSupp ); Vec_WrdFree( vTruths ); ABC_FREE( p->pRefs ); - Gia_ManCleanMark0( p ); // temp +// Gia_ManCleanMark0( p ); // temp Gia_ManCleanMark1( p ); } +/**Function************************************************************* + + Synopsis [Assumed that fMark0 marks the internal PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupRpm( Gia_Man_t * p ) +{ + Vec_Int_t * vPis, * vAnds; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + vPis = Vec_IntAlloc( 100 ); + vAnds = Vec_IntAlloc( 100 ); + Gia_ManCountPisNodes( p, vPis, vAnds ); + + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + // create PIs + Gia_ManForEachObjVec( vPis, p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + // create flops + Gia_ManForEachRo( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + // create internal nodes + Gia_ManForEachObjVec( vAnds, p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // create COs + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + + Vec_IntFree( vPis ); + Vec_IntFree( vAnds ); + return pNew; +} + Gia_Man_t * Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose ) { -// Abs_GiaTest( p, nCutMax, fVerbose ); - Abs_RpmPerformMark( p, nCutMax, 1 ); + Gia_Man_t * pNew; + + Gia_ManTestDoms( p ); return NULL; + + Abs_RpmPerformMark( p, nCutMax, 1 ); + pNew = Gia_ManDupRpm( p ); + Gia_ManCleanMark0( p ); + return pNew; } //////////////////////////////////////////////////////////////////////// |