diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-10-02 16:30:14 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-10-02 16:30:14 -0700 |
commit | 4aa33e7d0f8853443a2d33aa264ad27e60aa5ee8 (patch) | |
tree | 72f3f8a8cd80aa82386659db3a1cab56852b2751 /src/proof | |
parent | b71d4425d06fceb35c3888d2656ba39e046c6a02 (diff) | |
download | abc-4aa33e7d0f8853443a2d33aa264ad27e60aa5ee8.tar.gz abc-4aa33e7d0f8853443a2d33aa264ad27e60aa5ee8.tar.bz2 abc-4aa33e7d0f8853443a2d33aa264ad27e60aa5ee8.zip |
Structural reparametrization.
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/abs/absRpm.c | 245 |
1 files changed, 120 insertions, 125 deletions
diff --git a/src/proof/abs/absRpm.c b/src/proof/abs/absRpm.c index 5c44c152..13cb7952 100644 --- a/src/proof/abs/absRpm.c +++ b/src/proof/abs/absRpm.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "abs.h" +#include "misc/extra/extra.h" ABC_NAMESPACE_IMPL_START @@ -39,44 +40,6 @@ static int Abs_GiaObjRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode ); /**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 Lev, LevMax = 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 == i ) - continue; - for ( Lev = 0; Lev < LevMax && Gia_ObjIsAnd( Gia_ManObj(p, iDom) ); Lev++ ) - { - 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, @@ -131,7 +94,7 @@ void Gia_ManComputeDoms( Gia_Man_t * p ) { if ( i == 0 || Gia_ObjIsCi(pObj) ) continue; - if ( pObj->fMark0 || (p->pRefs && Gia_ObjRefs(p, pObj) == 0) ) + if ( pObj->fMark1 || (p->pRefs && Gia_ObjIsAnd(pObj) && Gia_ObjRefs(p, pObj) == 0) ) continue; if ( Gia_ObjIsCo(pObj) ) { @@ -159,9 +122,9 @@ void Gia_ManTestDoms2( Gia_Man_t * p ) */ 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_ManCleanMark1( p ); Gia_ManForEachPi( p, pObj, i ) - pObj->fMark0 = 1; + pObj->fMark1 = 1; vNodes = Vec_IntAlloc( 100 ); Gia_ManCreateRefs( p ); Gia_ManForEachPi( p, pObj, i ) @@ -186,47 +149,76 @@ void Gia_ManTestDoms2( Gia_Man_t * p ) // printf( "Success.\n" ); } Vec_IntFree( vNodes ); - Gia_ManCleanMark0( p ); + Gia_ManCleanMark1( p ); } /**Function************************************************************* Synopsis [Collect PI doms.] - Description [Assumes that some PIs and ANDs are marked with fMark0.] + Description [Assumes that some PIs and ANDs are marked with fMark1.] SideEffects [] SeeAlso [] ***********************************************************************/ +Vec_Int_t * Gia_ManCollectDoms( Gia_Man_t * p ) +{ + Vec_Int_t * vNodes; + Gia_Obj_t * pObj; + int Lev, LevMax = ABC_INFINITY; + int i, iDom, iDomNext; + vNodes = Vec_IntAlloc( 100 ); + Gia_ManForEachObj( p, pObj, i ) + { + if ( !pObj->fMark1 ) + continue; + iDom = Gia_ObjDom(p, pObj); + if ( iDom == -1 ) + continue; + if ( iDom == i ) + continue; + for ( Lev = 0; Lev < LevMax && Gia_ObjIsAnd( Gia_ManObj(p, iDom) ); Lev++ ) + { + Vec_IntPush( vNodes, iDom ); + iDomNext = Gia_ObjDom( p, Gia_ManObj(p, iDom) ); + if ( iDomNext == iDom ) + break; + iDom = iDomNext; + } + } + Vec_IntUniqify( vNodes ); + return vNodes; +} Vec_Int_t * Gia_ManComputePiDoms( Gia_Man_t * p ) { Vec_Int_t * vNodes; Gia_ManComputeDoms( p ); vNodes = Gia_ManCollectDoms( p ); // Vec_IntPrint( vNodes ); - printf( "Nodes = %d. Doms = %d.\n", Gia_ManAndNum(p), Vec_IntSize(vNodes) ); return vNodes; } - void Gia_ManTestDoms( Gia_Man_t * p ) { Vec_Int_t * vNodes; Gia_Obj_t * pObj; int i; - assert( p->vDoms == NULL ); // mark PIs - Gia_ManCleanMark0( p ); +// Gia_ManCreateRefs( p ); + Gia_ManCleanMark1( p ); Gia_ManForEachPi( p, pObj, i ) - pObj->fMark0 = 1; + pObj->fMark1 = 1; // compute dominators + assert( p->vDoms == NULL ); vNodes = Gia_ManComputePiDoms( p ); +// printf( "Nodes = %d. Doms = %d.\n", Gia_ManAndNum(p), Vec_IntSize(vNodes) ); Vec_IntFree( vNodes ); // unmark PIs - Gia_ManCleanMark0( p ); + Gia_ManCleanMark1( p ); } + /**Function************************************************************* Synopsis [] @@ -243,7 +235,7 @@ void Gia_ManCountPisNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPis if ( Gia_ObjIsTravIdCurrent(p, pObj) ) return; Gia_ObjSetTravIdCurrent(p, pObj); - if ( pObj->fMark0 ) + if ( pObj->fMark1 ) { Vec_IntPush( vPis, Gia_ObjId(p, pObj) ); return; @@ -271,7 +263,7 @@ void Gia_ManCountPisNodes( Gia_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vAnds ) /**Function************************************************************* - Synopsis [] + Synopsis [Computes support in terms of PIs and flops.] Description [] @@ -285,7 +277,7 @@ void Abs_ManSupport2_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) ) + if ( pObj->fMark1 || Gia_ObjIsRo(p, pObj) ) { Vec_IntPush( vSupp, Gia_ObjId(p, pObj) ); return; @@ -305,9 +297,9 @@ int Abs_ManSupport2( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ) /**Function************************************************************* - Synopsis [] + Synopsis [Computes support of the MFFC.] - Description [] + Description [Should be called when pObj's cone is dereferenced.] SideEffects [] @@ -319,7 +311,7 @@ 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 ) + if ( pObj->fMark1 || Gia_ObjIsRo(p, pObj) || Gia_ObjRefs(p, pObj) > 0 ) { Vec_IntPush( vSupp, Gia_ObjId(p, pObj) ); return; @@ -335,6 +327,7 @@ int Abs_ManSupport( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ) Gia_ManIncrementTravId( p ); Abs_ManSupport_rec( p, Gia_ObjFanin0(pObj), vSupp ); Abs_ManSupport_rec( p, Gia_ObjFanin1(pObj), vSupp ); + Gia_ObjSetTravIdCurrent(p, pObj); return Vec_IntSize(vSupp); } @@ -353,7 +346,7 @@ int Abs_GiaObjDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode ) { Gia_Obj_t * pFanin; int Counter = 0; - if ( pNode->fMark0 || Gia_ObjIsRo(p, pNode) ) + if ( pNode->fMark1 || Gia_ObjIsRo(p, pNode) ) return 0; assert( Gia_ObjIsAnd(pNode) ); pFanin = Gia_ObjFanin0(pNode); @@ -370,7 +363,7 @@ int Abs_GiaObjRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode ) { Gia_Obj_t * pFanin; int Counter = 0; - if ( pNode->fMark0 || Gia_ObjIsRo(p, pNode) ) + if ( pNode->fMark1 || Gia_ObjIsRo(p, pNode) ) return 0; assert( Gia_ObjIsAnd(pNode) ); pFanin = Gia_ObjFanin0(pNode); @@ -401,7 +394,7 @@ int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp ) Gia_ManForEachObjVec( vSupp, p, pObj, i ) if ( i < nSize && Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj) ) // add removable leaves { - assert( pObj->fMark0 ); + assert( pObj->fMark1 ); Vec_IntPush( vSupp, Gia_ObjId(p, pObj) ); } RetValue = Vec_IntSize(vSupp) - nSize; @@ -418,7 +411,8 @@ int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp ) Synopsis [Returns 1 if truth table has no const cofactors.] - Description [] + Description [The cofactoring variables are the (nSize-nSize0) + most significant vars. Each factors depends on nSize0 vars.] SideEffects [] @@ -428,7 +422,8 @@ int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp ) int Abs_GiaCheckTruth( word * pTruth, int nSize, int nSize0 ) { char * pStr = (char *)pTruth; - int i, k, nSteps, nStr = (nSize >= 3 ? (1 << (nSize - 3)) : 1); + int nStr = (nSize >= 3 ? (1 << (nSize - 3)) : 1); + int i, k, nSteps; assert( nSize0 > 0 && nSize0 <= nSize ); if ( nSize0 == 1 ) { @@ -440,8 +435,8 @@ int Abs_GiaCheckTruth( word * pTruth, int nSize, int nSize0 ) if ( nSize0 == 2 ) { for ( i = 0; i < nStr; i++ ) - if ( ((unsigned)pStr[i] & 0xF) == 0xF || (((unsigned)pStr[i] >> 4) & 0xF) == 0xF || - ((unsigned)pStr[i] & 0xF) == 0x0 || (((unsigned)pStr[i] >> 4) & 0xF) == 0x0 ) + if ( ((unsigned)pStr[i] & 0xF) == 0x0 || (((unsigned)pStr[i] >> 4) & 0xF) == 0x0 || + ((unsigned)pStr[i] & 0xF) == 0xF || (((unsigned)pStr[i] >> 4) & 0xF) == 0xF ) return 0; return 1; } @@ -460,6 +455,7 @@ int Abs_GiaCheckTruth( word * pTruth, int nSize, int nSize0 ) if ( k == nSteps ) break; } + assert( i <= nStr ); return (int)( i == nStr ); } @@ -474,108 +470,90 @@ int Abs_GiaCheckTruth( word * pTruth, int nSize, int nSize0 ) SeeAlso [] ***********************************************************************/ -void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose ) +void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose ) { - Vec_Int_t * vSupp, * vPis, * vAnds; - Vec_Wrd_t * vTruths; + Vec_Int_t * vSupp, * vPis, * vAnds, * vDoms; Gia_Obj_t * pObj; - word uTruth; + word * pTruth; int Iter, i, nSize0; - int fChanges = 1; + int fHasConst, fChanges = 1; Gia_ManCreateRefs( p ); - Gia_ManCleanMark0( p ); + Gia_ManCleanMark1( p ); Gia_ManForEachPi( p, pObj, i ) - pObj->fMark0 = 1; + pObj->fMark1 = 1; vPis = Vec_IntAlloc( 100 ); vAnds = Vec_IntAlloc( 100 ); vSupp = Vec_IntAlloc( 100 ); - vTruths = Vec_WrdAlloc( 100 ); for ( Iter = 0; fChanges; Iter++ ) { + fChanges = 0; + vDoms = Gia_ManComputePiDoms( p ); // count the number of PIs and internal nodes - if ( fVerbose ) + if ( fVerbose || fVeryVerbose ) { Gia_ManCountPisNodes( p, vPis, vAnds ); - printf( "Iter %3d : ", Iter ); - printf( "PI = %5d ", Vec_IntSize(vPis) ); - printf( "And = %6d ", Vec_IntSize(vAnds) ); + printf( "Iter %3d : ", Iter ); + printf( "Dom = %5d (%6.2f %%) ", Vec_IntSize(vDoms), 100.0 * Vec_IntSize(vDoms) / Gia_ManAndNum(p) ); + printf( "PI = %5d (%6.2f %%) ", Vec_IntSize(vPis), 100.0 * Vec_IntSize(vPis) / Gia_ManPiNum(p) ); + printf( "And = %6d (%6.2f %%) ", Vec_IntSize(vAnds), 100.0 * Vec_IntSize(vAnds) / Gia_ManAndNum(p) ); printf( "\n" ); } - - fChanges = 0; - Gia_ManCleanMark1( p ); // pObj = Gia_ObjFanin0( Gia_ManPo(p, 1) ); - Gia_ManForEachAnd( p, pObj, i ) + Gia_ManForEachObjVec( vDoms, p, pObj, i ) { - if ( pObj->fMark0 ) - continue; - if ( Gia_ObjRefs( p, pObj ) == 0 ) - continue; - if ( Gia_ObjFanin0(pObj)->fMark1 || Gia_ObjFanin1(pObj)->fMark1 ) - { - pObj->fMark1 = 1; - continue; - } - - // dereference nodes + assert( !pObj->fMark1 ); + assert( Gia_ObjRefs( p, pObj ) > 0 ); + // dereference root node Abs_GiaObjDeref_rec( p, pObj ); - // compute support - Abs_ManSupport( p, pObj, vSupp ); // check support size - if ( Vec_IntSize(vSupp) > nCutMax ) + if ( Abs_ManSupport(p, pObj, vSupp) > nCutMax ) { Abs_GiaObjRef_rec( p, pObj ); - pObj->fMark1 = 1; continue; } // order nodes by their ref counts nSize0 = Abs_GiaSortNodes( p, vSupp ); - // quit if there is no removable or too many - if ( nSize0 == 0 || nSize0 > nCutMax ) + assert( nSize0 > 0 && nSize0 <= nCutMax ); + // check if truth table has const cofs + pTruth = (word *)Gia_ObjComputeTruthTableCut( p, pObj, vSupp ); + fHasConst = !Abs_GiaCheckTruth( pTruth, Vec_IntSize(vSupp), nSize0 ); + if ( fVeryVerbose ) { - Abs_GiaObjRef_rec( p, pObj ); - continue; + printf( "Node = %8d Supp = %2d Supp0 = %2d Res = %4s ", Gia_ObjId(p, pObj), Vec_IntSize(vSupp), nSize0, fHasConst? "no":"yes" ); + Extra_PrintHex( stdout, (unsigned *)pTruth, Vec_IntSize(vSupp) ); printf( "\n" ); } - - // compute truth table - uTruth = Gia_ObjComputeTruthTable6( p, pObj, vSupp, vTruths ); - - // check if truth table has const cofs - if ( !Abs_GiaCheckTruth( &uTruth, Vec_IntSize(vSupp), nSize0 ) ) // has const + if ( fHasConst ) { Abs_GiaObjRef_rec( p, pObj ); -/* - 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; + pObj->fMark1 = 1; fChanges = 1; } + Vec_IntFree( vDoms ); +// break; + } + // count the number of PIs and internal nodes + if ( fVeryVerbose ) + { + Gia_ManCountPisNodes( p, vPis, vAnds ); + printf( "Iter %3d : ", Iter ); + printf( "Dom = %5d (%6.2f %%) ", Vec_IntSize(vDoms), 100.0 * Vec_IntSize(vDoms) / Gia_ManAndNum(p) ); + printf( "PI = %5d (%6.2f %%) ", Vec_IntSize(vPis), 100.0 * Vec_IntSize(vPis) / Gia_ManPiNum(p) ); + printf( "And = %6d (%6.2f %%) ", Vec_IntSize(vAnds), 100.0 * Vec_IntSize(vAnds) / Gia_ManAndNum(p) ); + printf( "\n" ); } Vec_IntFree( vPis ); Vec_IntFree( vAnds ); Vec_IntFree( vSupp ); - Vec_WrdFree( vTruths ); ABC_FREE( p->pRefs ); -// Gia_ManCleanMark0( p ); // temp - Gia_ManCleanMark1( p ); +// Gia_ManCleanMark1( p ); // temp } /**Function************************************************************* - Synopsis [Assumed that fMark0 marks the internal PIs.] + Synopsis [Assumed that fMark1 marks the internal PIs.] Description [] @@ -590,10 +568,12 @@ Gia_Man_t * Gia_ManDupRpm( Gia_Man_t * p ) Gia_Man_t * pNew; Gia_Obj_t * pObj; int i; + // derive PIs and internal nodes vPis = Vec_IntAlloc( 100 ); vAnds = Vec_IntAlloc( 100 ); Gia_ManCountPisNodes( p, vPis, vAnds ); + // duplicate AIG Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); @@ -613,20 +593,35 @@ Gia_Man_t * Gia_ManDupRpm( Gia_Man_t * p ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + // cleanup Vec_IntFree( vPis ); Vec_IntFree( vAnds ); return pNew; } -Gia_Man_t * Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose ) +/**Function************************************************************* + + Synopsis [Performs structural reparametrization.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose ) { Gia_Man_t * pNew; - Gia_ObjComputeTruthTableStart( p, nCutMax ); // Gia_ManTestDoms( p ); // return NULL; - Abs_RpmPerformMark( p, nCutMax, 1 ); + // perform structural analysis + Gia_ObjComputeTruthTableStart( p, nCutMax ); + Abs_RpmPerformMark( p, nCutMax, fVerbose, fVeryVerbose ); + Gia_ObjComputeTruthTableStop( p ); + // derive new AIG pNew = Gia_ManDupRpm( p ); - Gia_ManCleanMark0( p ); + Gia_ManCleanMark1( p ); return pNew; } |