| /**CFile**************************************************************** |
| |
| FileName [giaEquiv.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Scalable AIG package.] |
| |
| Synopsis [Manipulation of equivalence classes.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: giaEquiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "gia.h" |
| #include "proof/cec/cec.h" |
| #include "sat/bmc/bmc.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Manipulating original IDs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManOrigIdsInit( Gia_Man_t * p ) |
| { |
| Vec_IntFreeP( &p->vIdsOrig ); |
| p->vIdsOrig = Vec_IntStartNatural( Gia_ManObjNum(p) ); |
| } |
| void Gia_ManOrigIdsStart( Gia_Man_t * p ) |
| { |
| Vec_IntFreeP( &p->vIdsOrig ); |
| p->vIdsOrig = Vec_IntStartFull( Gia_ManObjNum(p) ); |
| } |
| void Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew ) |
| { |
| Gia_Obj_t * pObj; int i; |
| if ( p->vIdsOrig == NULL ) |
| return; |
| Gia_ManOrigIdsStart( pNew ); |
| Vec_IntWriteEntry( pNew->vIdsOrig, 0, 0 ); |
| Gia_ManForEachObj1( p, pObj, i ) |
| if ( ~pObj->Value && Abc_Lit2Var(pObj->Value) && Vec_IntEntry(p->vIdsOrig, i) != -1 && Vec_IntEntry(pNew->vIdsOrig, Abc_Lit2Var(pObj->Value)) == -1 ) |
| Vec_IntWriteEntry( pNew->vIdsOrig, Abc_Lit2Var(pObj->Value), Vec_IntEntry(p->vIdsOrig, i) ); |
| Gia_ManForEachObj( pNew, pObj, i ) |
| assert( Vec_IntEntry(pNew->vIdsOrig, i) >= 0 ); |
| } |
| // input is a set of equivalent node pairs in any order |
| // output is the mapping of each node into the equiv node with the smallest ID |
| void Gia_ManOrigIdsRemapPairsInsert( Vec_Int_t * vMap, int One, int Two ) |
| { |
| int Smo = One < Two ? One : Two; |
| int Big = One < Two ? Two : One; |
| assert( Smo != Big ); |
| if ( Vec_IntEntry(vMap, Big) == -1 ) |
| Vec_IntWriteEntry( vMap, Big, Smo ); |
| else |
| Gia_ManOrigIdsRemapPairsInsert( vMap, Smo, Vec_IntEntry(vMap, Big) ); |
| } |
| int Gia_ManOrigIdsRemapPairsExtract( Vec_Int_t * vMap, int One ) |
| { |
| if ( Vec_IntEntry(vMap, One) == -1 ) |
| return One; |
| return Gia_ManOrigIdsRemapPairsExtract( vMap, Vec_IntEntry(vMap, One) ); |
| } |
| Vec_Int_t * Gia_ManOrigIdsRemapPairs( Vec_Int_t * vEquivPairs, int nObjs ) |
| { |
| Vec_Int_t * vMapResult; |
| Vec_Int_t * vMap2Smaller; |
| int i, One, Two; |
| // map bigger into smaller one |
| vMap2Smaller = Vec_IntStartFull( nObjs ); |
| Vec_IntForEachEntryDouble( vEquivPairs, One, Two, i ) |
| Gia_ManOrigIdsRemapPairsInsert( vMap2Smaller, One, Two ); |
| // collect results in the topo order |
| vMapResult = Vec_IntStartFull( nObjs ); |
| Vec_IntForEachEntry( vMap2Smaller, One, i ) |
| if ( One >= 0 ) |
| Vec_IntWriteEntry( vMapResult, i, Gia_ManOrigIdsRemapPairsExtract(vMap2Smaller, One) ); |
| Vec_IntFree( vMap2Smaller ); |
| return vMapResult; |
| } |
| // remap the AIG using the equivalent pairs proved |
| // returns the reduced AIG and the equivalence classes of the original AIG |
| Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs ) |
| { |
| Gia_Man_t * pNew = NULL; |
| Gia_Obj_t * pObj, * pRepr; int i; |
| Vec_Int_t * vMap = Gia_ManOrigIdsRemapPairs( vPairs, Gia_ManObjNum(p) ); |
| Gia_ManSetPhase( p ); |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| Gia_ManFillValue(p); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManForEachCi( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCi(pNew); |
| Gia_ManHashAlloc( pNew ); |
| Gia_ManForEachAnd( p, pObj, i ) |
| { |
| if ( Vec_IntEntry(vMap, i) == -1 ) |
| pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| else |
| { |
| pRepr = Gia_ManObj( p, Vec_IntEntry(vMap, i) ); |
| pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase ); |
| } |
| } |
| Gia_ManHashStop( pNew ); |
| Gia_ManForEachCo( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| Vec_IntFree( vMap ); |
| // compute equivalences |
| assert( !p->pReprs && !p->pNexts ); |
| p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); |
| for ( i = 0; i < Gia_ManObjNum(p); i++ ) |
| Gia_ObjSetRepr( p, i, GIA_VOID ); |
| Gia_ManFillValue(pNew); |
| Gia_ManForEachAnd( p, pObj, i ) |
| { |
| int iRepr = Abc_Lit2Var(pObj->Value); |
| if ( iRepr == 0 ) |
| { |
| Gia_ObjSetRepr( p, i, 0 ); |
| continue; |
| } |
| pRepr = Gia_ManObj( pNew, iRepr ); |
| if ( !~pRepr->Value ) // first time |
| { |
| pRepr->Value = i; |
| continue; |
| } |
| // add equivalence |
| Gia_ObjSetRepr( p, i, pRepr->Value ); |
| } |
| p->pNexts = Gia_ManDeriveNexts( p ); |
| return pNew; |
| } |
| Gia_Man_t * Gia_ManOrigIdsReduceTest( Gia_Man_t * p, Vec_Int_t * vPairs ) |
| { |
| Gia_Man_t * pTemp, * pNew = Gia_ManOrigIdsReduce( p, vPairs ); |
| Gia_ManPrintStats( p, NULL ); |
| Gia_ManPrintStats( pNew, NULL ); |
| //Gia_ManStop( pNew ); |
| // cleanup the resulting one |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| Gia_ManStop( pTemp ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Compute equivalence classes of nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose ) |
| { |
| Gia_Man_t * pTemp; |
| Cec_ParFra_t ParsFra, * pPars = &ParsFra; |
| Cec_ManFraSetDefaultParams( pPars ); |
| pPars->fUseOrigIds = 1; |
| pPars->fSatSweeping = 1; |
| pPars->nBTLimit = nConfs; |
| pPars->fVerbose = fVerbose; |
| pTemp = Cec_ManSatSweeping( pGia, pPars, 0 ); |
| Gia_ManStop( pTemp ); |
| return Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if AIG is not in the required topo order.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManCheckTopoOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) |
| { |
| Gia_Obj_t * pRepr; |
| if ( pObj->Value == 0 ) |
| return 1; |
| pObj->Value = 0; |
| assert( Gia_ObjIsAnd(pObj) ); |
| if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) ) ) |
| return 0; |
| if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin1(pObj) ) ) |
| return 0; |
| pRepr = p->pReprs ? Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ) : NULL; |
| return pRepr == NULL || pRepr->Value == 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 0 if AIG is not in the required topo order.] |
| |
| Description [AIG should be in such an order that the representative |
| is always traversed before the node.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManCheckTopoOrder( Gia_Man_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i, RetValue = 1; |
| Gia_ManFillValue( p ); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManForEachCi( p, pObj, i ) |
| pObj->Value = 0; |
| Gia_ManForEachCo( p, pObj, i ) |
| RetValue &= Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) ); |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Given representatives, derives pointers to the next objects.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int * Gia_ManDeriveNexts( Gia_Man_t * p ) |
| { |
| unsigned * pNexts, * pTails; |
| int i; |
| assert( p->pReprs != NULL ); |
| assert( p->pNexts == NULL ); |
| pNexts = ABC_CALLOC( unsigned, Gia_ManObjNum(p) ); |
| pTails = ABC_ALLOC( unsigned, Gia_ManObjNum(p) ); |
| for ( i = 0; i < Gia_ManObjNum(p); i++ ) |
| pTails[i] = i; |
| for ( i = 0; i < Gia_ManObjNum(p); i++ ) |
| { |
| if ( !p->pReprs[i].iRepr || p->pReprs[i].iRepr == GIA_VOID ) |
| continue; |
| pNexts[ pTails[p->pReprs[i].iRepr] ] = i; |
| pTails[p->pReprs[i].iRepr] = i; |
| } |
| ABC_FREE( pTails ); |
| return (int *)pNexts; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Given points to the next objects, derives representatives.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManDeriveReprs( Gia_Man_t * p ) |
| { |
| int i, iObj; |
| assert( p->pReprs == NULL ); |
| assert( p->pNexts != NULL ); |
| p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); |
| for ( i = 0; i < Gia_ManObjNum(p); i++ ) |
| Gia_ObjSetRepr( p, i, GIA_VOID ); |
| for ( i = 0; i < Gia_ManObjNum(p); i++ ) |
| { |
| if ( p->pNexts[i] == 0 ) |
| continue; |
| if ( p->pReprs[i].iRepr != GIA_VOID ) |
| continue; |
| // next is set, repr is not set |
| for ( iObj = p->pNexts[i]; iObj; iObj = p->pNexts[iObj] ) |
| p->pReprs[iObj].iRepr = i; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManEquivCountLitsAll( Gia_Man_t * p ) |
| { |
| int i, nLits = 0; |
| for ( i = 0; i < Gia_ManObjNum(p); i++ ) |
| nLits += (Gia_ObjRepr(p, i) != GIA_VOID); |
| return nLits; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManEquivCountClasses( Gia_Man_t * p ) |
| { |
| int i, Counter = 0; |
| if ( p->pReprs == NULL ) |
| return 0; |
| for ( i = 1; i < Gia_ManObjNum(p); i++ ) |
| Counter += Gia_ObjIsHead(p, i); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits ) |
| { |
| int nLitsReal = Gia_ManEquivCountLitsAll( p ); |
| if ( nLitsReal != nLits ) |
| Abc_Print( 1, "Detected a mismatch in counting equivalence classes (%d).\n", nLitsReal - nLits ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManPrintStatsClasses( Gia_Man_t * p ) |
| { |
| int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits; |
| for ( i = 1; i < Gia_ManObjNum(p); i++ ) |
| { |
| if ( Gia_ObjIsHead(p, i) ) |
| Counter++; |
| else if ( Gia_ObjIsConst(p, i) ) |
| Counter0++; |
| else if ( Gia_ObjIsNone(p, i) ) |
| CounterX++; |
| if ( Gia_ObjProved(p, i) ) |
| Proved++; |
| } |
| CounterX -= Gia_ManCoNum(p); |
| nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; |
| |
| // Abc_Print( 1, "i/o/ff =%5d/%5d/%5d ", Gia_ManPiNum(p), Gia_ManPoNum(p), Gia_ManRegNum(p) ); |
| // Abc_Print( 1, "and =%5d ", Gia_ManAndNum(p) ); |
| // Abc_Print( 1, "lev =%3d ", Gia_ManLevelNum(p) ); |
| Abc_Print( 1, "cst =%3d cls =%6d lit =%8d\n", Counter0, Counter, nLits ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManEquivCountLits( Gia_Man_t * p ) |
| { |
| int i, Counter = 0, Counter0 = 0, CounterX = 0; |
| if ( p->pReprs == NULL || p->pNexts == NULL ) |
| return 0; |
| for ( i = 1; i < Gia_ManObjNum(p); i++ ) |
| { |
| if ( Gia_ObjIsHead(p, i) ) |
| Counter++; |
| else if ( Gia_ObjIsConst(p, i) ) |
| Counter0++; |
| else if ( Gia_ObjIsNone(p, i) ) |
| CounterX++; |
| } |
| CounterX -= Gia_ManCoNum(p); |
| return Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManEquivCountOne( Gia_Man_t * p, int i ) |
| { |
| int Ent, nLits = 1; |
| Gia_ClassForEachObj1( p, i, Ent ) |
| { |
| assert( Gia_ObjRepr(p, Ent) == i ); |
| nLits++; |
| } |
| return nLits; |
| } |
| void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter ) |
| { |
| int Ent; |
| Abc_Print( 1, "Class %4d : Num = %2d {", Counter, Gia_ManEquivCountOne(p, i) ); |
| Gia_ClassForEachObj( p, i, Ent ) |
| { |
| Abc_Print( 1," %d", Ent ); |
| if ( p->pReprs[Ent].fColorA || p->pReprs[Ent].fColorB ) |
| Abc_Print( 1," <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB ); |
| } |
| Abc_Print( 1, " }\n" ); |
| } |
| void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) |
| { |
| int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits; |
| for ( i = 1; i < Gia_ManObjNum(p); i++ ) |
| { |
| if ( Gia_ObjIsHead(p, i) ) |
| Counter++; |
| else if ( Gia_ObjIsConst(p, i) ) |
| Counter0++; |
| else if ( Gia_ObjIsNone(p, i) ) |
| CounterX++; |
| if ( Gia_ObjProved(p, i) ) |
| Proved++; |
| } |
| CounterX -= Gia_ManCoNum(p); |
| nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; |
| Abc_Print( 1, "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f MB\n", |
| Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem ); |
| assert( Gia_ManEquivCheckLits( p, nLits ) ); |
| if ( fVerbose ) |
| { |
| // int Ent; |
| Abc_Print( 1, "Const0 (%d) = ", Counter0 ); |
| Gia_ManForEachConst( p, i ) |
| Abc_Print( 1, "%d ", i ); |
| Abc_Print( 1, "\n" ); |
| Counter = 0; |
| Gia_ManForEachClass( p, i ) |
| Gia_ManEquivPrintOne( p, i, ++Counter ); |
| /* |
| Gia_ManLevelNum( p ); |
| Gia_ManForEachClass( p, i ) |
| if ( i % 100 == 0 ) |
| { |
| // Abc_Print( 1, "%d ", Gia_ManEquivCountOne(p, i) ); |
| Gia_ClassForEachObj( p, i, Ent ) |
| { |
| Abc_Print( 1, "%d ", Gia_ObjLevel( p, Gia_ManObj(p, Ent) ) ); |
| } |
| Abc_Print( 1, "\n" ); |
| } |
| */ |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns representative node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut ) |
| { |
| if ( fUseAll ) |
| { |
| if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID ) |
| return NULL; |
| } |
| else |
| { |
| if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) |
| return NULL; |
| } |
| // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) ) |
| if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) ) |
| return NULL; |
| return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG in the DFS order.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut ) |
| { |
| Gia_Obj_t * pRepr; |
| if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) ) |
| { |
| Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut ); |
| pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); |
| return; |
| } |
| if ( ~pObj->Value ) |
| return; |
| assert( Gia_ObjIsAnd(pObj) ); |
| Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut ); |
| Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll, fDualOut ); |
| pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reduces AIG using equivalence classes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose ) |
| { |
| Gia_Man_t * pNew; |
| Gia_Obj_t * pObj; |
| int i; |
| if ( !p->pReprs ) |
| { |
| Abc_Print( 1, "Gia_ManEquivReduce(): Equivalence classes are not available.\n" ); |
| return NULL; |
| } |
| if ( fDualOut && (Gia_ManPoNum(p) & 1) ) |
| { |
| Abc_Print( 1, "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" ); |
| return NULL; |
| } |
| // check if there are any equivalences defined |
| Gia_ManForEachObj( p, pObj, i ) |
| if ( Gia_ObjReprObj(p, i) != NULL ) |
| break; |
| if ( i == Gia_ManObjNum(p) ) |
| { |
| // Abc_Print( 1, "Gia_ManEquivReduce(): There are no equivalences to reduce.\n" ); |
| return NULL; |
| } |
| /* |
| if ( !Gia_ManCheckTopoOrder( p ) ) |
| { |
| Abc_Print( 1, "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" ); |
| return NULL; |
| } |
| */ |
| if ( !fSkipPhase ) |
| Gia_ManSetPhase( p ); |
| if ( fDualOut ) |
| Gia_ManEquivSetColors( p, fVerbose ); |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| Gia_ManFillValue( p ); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManForEachCi( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCi(pNew); |
| Gia_ManHashAlloc( pNew ); |
| Gia_ManForEachCo( p, pObj, i ) |
| Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut ); |
| Gia_ManForEachCo( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| Gia_ManHashStop( pNew ); |
| Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reduces AIG using equivalence classes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEquivFixOutputPairs( Gia_Man_t * p ) |
| { |
| Gia_Obj_t * pObj0, * pObj1; |
| int i; |
| assert( (Gia_ManPoNum(p) & 1) == 0 ); |
| Gia_ManForEachPo( p, pObj0, i ) |
| { |
| pObj1 = Gia_ManPo( p, ++i ); |
| if ( Gia_ObjChild0(pObj0) != Gia_ObjChild0(pObj1) ) |
| continue; |
| pObj0->iDiff0 = Gia_ObjId(p, pObj0); |
| pObj0->fCompl0 = 0; |
| pObj1->iDiff0 = Gia_ObjId(p, pObj1); |
| pObj1->fCompl0 = 0; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Removes pointers to the unmarked nodes..] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEquivUpdatePointers( Gia_Man_t * p, Gia_Man_t * pNew ) |
| { |
| Gia_Obj_t * pObj, * pObjNew; |
| int i; |
| Gia_ManForEachObj( p, pObj, i ) |
| { |
| if ( !~pObj->Value ) |
| continue; |
| pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) ); |
| if ( pObjNew->fMark0 ) |
| pObj->Value = ~0; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Removes pointers to the unmarked nodes..] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFinal ) |
| { |
| Vec_Int_t * vClass; |
| Gia_Obj_t * pObj, * pObjNew; |
| int i, k, iNode, iRepr, iPrev; |
| // start representatives |
| pFinal->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pFinal) ); |
| for ( i = 0; i < Gia_ManObjNum(pFinal); i++ ) |
| Gia_ObjSetRepr( pFinal, i, GIA_VOID ); |
| // iterate over constant candidates |
| Gia_ManForEachConst( p, i ) |
| { |
| pObj = Gia_ManObj( p, i ); |
| if ( !~pObj->Value ) |
| continue; |
| pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) ); |
| if ( Abc_Lit2Var(pObjNew->Value) == 0 ) |
| continue; |
| Gia_ObjSetRepr( pFinal, Abc_Lit2Var(pObjNew->Value), 0 ); |
| } |
| // iterate over class candidates |
| vClass = Vec_IntAlloc( 100 ); |
| Gia_ManForEachClass( p, i ) |
| { |
| Vec_IntClear( vClass ); |
| Gia_ClassForEachObj( p, i, k ) |
| { |
| pObj = Gia_ManObj( p, k ); |
| if ( !~pObj->Value ) |
| continue; |
| pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) ); |
| Vec_IntPushUnique( vClass, Abc_Lit2Var(pObjNew->Value) ); |
| } |
| if ( Vec_IntSize( vClass ) < 2 ) |
| continue; |
| Vec_IntSort( vClass, 0 ); |
| iRepr = iPrev = Vec_IntEntry( vClass, 0 ); |
| Vec_IntForEachEntryStart( vClass, iNode, k, 1 ) |
| { |
| Gia_ObjSetRepr( pFinal, iNode, iRepr ); |
| assert( iPrev < iNode ); |
| iPrev = iNode; |
| } |
| } |
| Vec_IntFree( vClass ); |
| pFinal->pNexts = Gia_ManDeriveNexts( pFinal ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Removes pointers to the unmarked nodes..] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p ) |
| { |
| Gia_Man_t * pNew; |
| Vec_Int_t * vClass; |
| int i, k, iNode, iRepr, iPrev; |
| pNew = Gia_ManDupDfs( p ); |
| // start representatives |
| pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) ); |
| for ( i = 0; i < Gia_ManObjNum(pNew); i++ ) |
| Gia_ObjSetRepr( pNew, i, GIA_VOID ); |
| // iterate over constant candidates |
| Gia_ManForEachConst( p, i ) |
| Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 ); |
| // iterate over class candidates |
| vClass = Vec_IntAlloc( 100 ); |
| Gia_ManForEachClass( p, i ) |
| { |
| Vec_IntClear( vClass ); |
| Gia_ClassForEachObj( p, i, k ) |
| Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) ); |
| assert( Vec_IntSize( vClass ) > 1 ); |
| Vec_IntSort( vClass, 0 ); |
| iRepr = iPrev = Vec_IntEntry( vClass, 0 ); |
| Vec_IntForEachEntryStart( vClass, iNode, k, 1 ) |
| { |
| Gia_ObjSetRepr( pNew, iNode, iRepr ); |
| assert( iPrev < iNode ); |
| iPrev = iNode; |
| } |
| } |
| Vec_IntFree( vClass ); |
| pNew->pNexts = Gia_ManDeriveNexts( pNew ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reduces AIG while remapping equivalence classes.] |
| |
| Description [Drops the pairs of outputs if they are proved equivalent.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ) |
| { |
| Gia_Man_t * pNew, * pFinal; |
| pNew = Gia_ManEquivReduce( p, 0, 0, 0, 0 ); |
| if ( pNew == NULL ) |
| return NULL; |
| Gia_ManOrigIdsRemap( p, pNew ); |
| if ( fMiterPairs ) |
| Gia_ManEquivFixOutputPairs( pNew ); |
| if ( fSeq ) |
| Gia_ManSeqMarkUsed( pNew ); |
| else |
| Gia_ManCombMarkUsed( pNew ); |
| Gia_ManEquivUpdatePointers( p, pNew ); |
| pFinal = Gia_ManDupMarked( pNew ); |
| Gia_ManOrigIdsRemap( pNew, pFinal ); |
| Gia_ManEquivDeriveReprs( p, pNew, pFinal ); |
| Gia_ManStop( pNew ); |
| pFinal = Gia_ManEquivRemapDfs( pNew = pFinal ); |
| Gia_ManOrigIdsRemap( pNew, pFinal ); |
| Gia_ManStop( pNew ); |
| return pFinal; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Marks CIs/COs/ANDs unreachable from POs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManEquivSetColor_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fOdds ) |
| { |
| if ( Gia_ObjVisitColor( p, Gia_ObjId(p,pObj), fOdds ) ) |
| return 0; |
| if ( Gia_ObjIsRo(p, pObj) ) |
| return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p, pObj)), fOdds ); |
| assert( Gia_ObjIsAnd(pObj) ); |
| return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), fOdds ) |
| + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin1(pObj), fOdds ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Marks CIs/COs/ANDs unreachable from POs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ) |
| { |
| Gia_Obj_t * pObj; |
| int i, nNodes[2], nDiffs[2]; |
| assert( (Gia_ManPoNum(p) & 1) == 0 ); |
| Gia_ObjSetColors( p, 0 ); |
| Gia_ManForEachPi( p, pObj, i ) |
| Gia_ObjSetColors( p, Gia_ObjId(p,pObj) ); |
| nNodes[0] = nNodes[1] = Gia_ManPiNum(p); |
| Gia_ManForEachPo( p, pObj, i ) |
| nNodes[i&1] += Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), i&1 ); |
| // Gia_ManForEachObj( p, pObj, i ) |
| // if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ) |
| // assert( Gia_ObjColors(p, i) ); |
| nDiffs[0] = Gia_ManCandNum(p) - nNodes[0]; |
| nDiffs[1] = Gia_ManCandNum(p) - nNodes[1]; |
| if ( fVerbose ) |
| { |
| Abc_Print( 1, "CI+AND = %7d A = %7d B = %7d Ad = %7d Bd = %7d AB = %7d.\n", |
| Gia_ManCandNum(p), nNodes[0], nNodes[1], nDiffs[0], nDiffs[1], |
| Gia_ManCandNum(p) - nDiffs[0] - nDiffs[1] ); |
| } |
| return (nDiffs[0] + nDiffs[1]) / 2; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG in the DFS order.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap ) |
| { |
| Gia_Obj_t * pRepr; |
| unsigned iLitNew; |
| pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); |
| if ( pRepr == NULL ) |
| return; |
| // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) ) |
| if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) ) |
| return; |
| iLitNew = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); |
| if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) |
| { |
| if ( vTrace ) |
| Vec_IntPush( vTrace, 1 ); |
| if ( vGuide == NULL || Vec_IntEntry( vGuide, Vec_IntSize(vTrace)-1 ) ) |
| { |
| if ( vMap ) |
| Vec_IntPush( vMap, Gia_ObjId(p, pObj) ); |
| Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); |
| } |
| } |
| else |
| { |
| if ( vTrace ) |
| Vec_IntPush( vTrace, 0 ); |
| } |
| if ( fSpeculate ) |
| pObj->Value = iLitNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG in the DFS order.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate, Vec_Int_t * vTrace, Vec_Int_t * vGuide, Vec_Int_t * vMap ) |
| { |
| if ( ~pObj->Value ) |
| return; |
| assert( Gia_ObjIsAnd(pObj) ); |
| Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap ); |
| Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap ); |
| pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, vMap ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reduces AIG using equivalence classes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace, Vec_Int_t * vMap ) |
| { |
| Vec_Int_t * vXorLits; |
| Gia_Man_t * pNew, * pTemp; |
| Gia_Obj_t * pObj; |
| int i, iLitNew; |
| if ( !p->pReprs ) |
| { |
| Abc_Print( 1, "Gia_ManSpecReduce(): Equivalence classes are not available.\n" ); |
| return NULL; |
| } |
| Vec_IntClear( vTrace ); |
| vXorLits = Vec_IntAlloc( 1000 ); |
| Gia_ManSetPhase( p ); |
| Gia_ManFillValue( p ); |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| Gia_ManHashAlloc( pNew ); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManForEachCi( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCi(pNew); |
| Gia_ManForEachRo( p, pObj, i ) |
| Gia_ManSpecBuild( pNew, p, pObj, vXorLits, 0, 1, vTrace, NULL, vMap ); |
| Gia_ManForEachCo( p, pObj, i ) |
| Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, 0, 1, vTrace, NULL, vMap ); |
| Gia_ManForEachPo( p, pObj, i ) |
| Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| Vec_IntForEachEntry( vXorLits, iLitNew, i ) |
| Gia_ManAppendCo( pNew, iLitNew ); |
| if ( Vec_IntSize(vXorLits) == 0 ) |
| { |
| Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" ); |
| Gia_ManAppendCo( pNew, 0 ); |
| } |
| Gia_ManForEachRi( p, pObj, i ) |
| Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| Gia_ManHashStop( pNew ); |
| Vec_IntFree( vXorLits ); |
| Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| Gia_ManStop( pTemp ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reduces AIG using equivalence classes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fSpeculate, int fSkipSome, int fVerbose ) |
| { |
| Gia_Man_t * pNew, * pTemp; |
| Gia_Obj_t * pObj; |
| Vec_Int_t * vXorLits; |
| int i, iLitNew; |
| Vec_Int_t * vTrace = NULL, * vGuide = NULL; |
| if ( !p->pReprs ) |
| { |
| Abc_Print( 1, "Gia_ManSpecReduce(): Equivalence classes are not available.\n" ); |
| return NULL; |
| } |
| if ( fDualOut && (Gia_ManPoNum(p) & 1) ) |
| { |
| Abc_Print( 1, "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" ); |
| return NULL; |
| } |
| if ( fSkipSome ) |
| { |
| vGuide = Vec_IntAlloc( 100 ); |
| pTemp = Gia_ManSpecReduceTrace( p, vGuide, NULL ); |
| Gia_ManStop( pTemp ); |
| assert( Vec_IntSize(vGuide) == Gia_ManEquivCountLitsAll(p) ); |
| vTrace = Vec_IntAlloc( 100 ); |
| } |
| vXorLits = Vec_IntAlloc( 1000 ); |
| Gia_ManSetPhase( p ); |
| Gia_ManFillValue( p ); |
| if ( fDualOut ) |
| Gia_ManEquivSetColors( p, fVerbose ); |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| Gia_ManHashAlloc( pNew ); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManForEachCi( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCi(pNew); |
| Gia_ManForEachRo( p, pObj, i ) |
| Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL ); |
| Gia_ManForEachCo( p, pObj, i ) |
| Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate, vTrace, vGuide, NULL ); |
| if ( !fSynthesis ) |
| { |
| Gia_ManForEachPo( p, pObj, i ) |
| Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| } |
| Vec_IntForEachEntry( vXorLits, iLitNew, i ) |
| Gia_ManAppendCo( pNew, iLitNew ); |
| if ( Vec_IntSize(vXorLits) == 0 ) |
| { |
| Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" ); |
| Gia_ManAppendCo( pNew, 0 ); |
| } |
| Gia_ManForEachRi( p, pObj, i ) |
| Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| Gia_ManHashStop( pNew ); |
| Vec_IntFree( vXorLits ); |
| Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| Gia_ManStop( pTemp ); |
| |
| // update using trace |
| if ( fSkipSome ) |
| { |
| // count the number of non-zero entries |
| int iLit, nAddPos = 0; |
| Vec_IntForEachEntry( vGuide, iLit, i ) |
| if ( iLit ) |
| nAddPos++; |
| if ( nAddPos ) |
| assert( Gia_ManPoNum(pNew) == Gia_ManPoNum(p) + nAddPos ); |
| } |
| Vec_IntFreeP( &vTrace ); |
| Vec_IntFreeP( &vGuide ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG in the DFS order.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut ) |
| { |
| Gia_Obj_t * pRepr; |
| int iLitNew; |
| pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); |
| if ( pRepr == NULL ) |
| return; |
| // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) ) |
| if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) ) |
| return; |
| iLitNew = Abc_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); |
| if ( Gia_ObjCopyF(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) |
| Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjCopyF(p, f, pObj), iLitNew) ); |
| Gia_ObjSetCopyF( p, f, pObj, iLitNew ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG in the DFS order.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut ) |
| { |
| if ( ~Gia_ObjCopyF(p, f, pObj) ) |
| return; |
| assert( Gia_ObjIsAnd(pObj) ); |
| Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut ); |
| Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f, fDualOut ); |
| Gia_ObjSetCopyF( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj)) ); |
| Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates initialized SRM with the given number of frames.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut ) |
| { |
| Gia_Man_t * pNew, * pTemp; |
| Gia_Obj_t * pObj, * pObjRi, * pObjRo; |
| Vec_Int_t * vXorLits; |
| int f, i, iLitNew; |
| if ( !p->pReprs ) |
| { |
| Abc_Print( 1, "Gia_ManSpecReduceInit(): Equivalence classes are not available.\n" ); |
| return NULL; |
| } |
| if ( Gia_ManRegNum(p) == 0 ) |
| { |
| Abc_Print( 1, "Gia_ManSpecReduceInit(): Circuit is not sequential.\n" ); |
| return NULL; |
| } |
| if ( Gia_ManRegNum(p) != pInit->nRegs ) |
| { |
| Abc_Print( 1, "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" ); |
| return NULL; |
| } |
| if ( fDualOut && (Gia_ManPoNum(p) & 1) ) |
| { |
| Abc_Print( 1, "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" ); |
| return NULL; |
| } |
| |
| /* |
| if ( !Gia_ManCheckTopoOrder( p ) ) |
| { |
| Abc_Print( 1, "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" ); |
| return NULL; |
| } |
| */ |
| assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 ); |
| Vec_IntFill( &p->vCopies, nFrames * Gia_ManObjNum(p), -1 ); |
| vXorLits = Vec_IntAlloc( 1000 ); |
| Gia_ManSetPhase( p ); |
| if ( fDualOut ) |
| Gia_ManEquivSetColors( p, 0 ); |
| pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| Gia_ManHashAlloc( pNew ); |
| Gia_ManForEachRo( p, pObj, i ) |
| Gia_ObjSetCopyF( p, 0, pObj, Abc_InfoHasBit(pInit->pData, i) ); |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); |
| Gia_ManForEachPi( p, pObj, i ) |
| Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); |
| Gia_ManForEachRo( p, pObj, i ) |
| Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut ); |
| Gia_ManForEachCo( p, pObj, i ) |
| { |
| Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut ); |
| Gia_ObjSetCopyF( p, f, pObj, Gia_ObjFanin0CopyF(p, f, pObj) ); |
| } |
| if ( f == nFrames - 1 ) |
| break; |
| Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) |
| Gia_ObjSetCopyF( p, f+1, pObjRo, Gia_ObjCopyF(p, f, pObjRi) ); |
| } |
| Vec_IntForEachEntry( vXorLits, iLitNew, i ) |
| Gia_ManAppendCo( pNew, iLitNew ); |
| if ( Vec_IntSize(vXorLits) == 0 ) |
| { |
| // Abc_Print( 1, "Speculatively reduced model has no primary outputs.\n" ); |
| Gia_ManAppendCo( pNew, 0 ); |
| } |
| Vec_IntErase( &p->vCopies ); |
| Vec_IntFree( vXorLits ); |
| Gia_ManHashStop( pNew ); |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| Gia_ManStop( pTemp ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates initialized SRM with the given number of frames.] |
| |
| Description [Uses as many frames as needed to create the number of |
| output not less than the number of equivalence literals.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs ) |
| { |
| Gia_Man_t * pFrames; |
| int f, nLits; |
| nLits = Gia_ManEquivCountLits( p ); |
| for ( f = 1; ; f++ ) |
| { |
| pFrames = Gia_ManSpecReduceInit( p, pInit, f, fDualOut ); |
| if ( (nMinOutputs == 0 && Gia_ManPoNum(pFrames) >= nLits/2+1) || |
| (nMinOutputs != 0 && Gia_ManPoNum(pFrames) >= nMinOutputs) ) |
| break; |
| if ( f == nFramesMax ) |
| break; |
| if ( Gia_ManAndNum(pFrames) > 500000 ) |
| { |
| Gia_ManStop( pFrames ); |
| return NULL; |
| } |
| Gia_ManStop( pFrames ); |
| pFrames = NULL; |
| } |
| if ( f == nFramesMax ) |
| Abc_Print( 1, "Stopped unrolling after %d frames.\n", nFramesMax ); |
| if ( pnFrames ) |
| *pnFrames = f; |
| return pFrames; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Transforms equiv classes by removing the AB nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ) |
| { |
| extern void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass ); |
| Vec_Int_t * vClass, * vClassNew; |
| int iRepr, iNode, Ent, k; |
| int nRemovedLits = 0, nRemovedClas = 0; |
| int nTotalLits = 0, nTotalClas = 0; |
| Gia_Obj_t * pObj; |
| int i; |
| assert( p->pReprs && p->pNexts ); |
| vClass = Vec_IntAlloc( 100 ); |
| vClassNew = Vec_IntAlloc( 100 ); |
| Gia_ManForEachObj( p, pObj, i ) |
| if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ) |
| assert( Gia_ObjColors(p, i) ); |
| Gia_ManForEachClassReverse( p, iRepr ) |
| { |
| nTotalClas++; |
| Vec_IntClear( vClass ); |
| Vec_IntClear( vClassNew ); |
| Gia_ClassForEachObj( p, iRepr, iNode ) |
| { |
| nTotalLits++; |
| Vec_IntPush( vClass, iNode ); |
| assert( Gia_ObjColors(p, iNode) ); |
| if ( Gia_ObjColors(p, iNode) != 3 ) |
| Vec_IntPush( vClassNew, iNode ); |
| else |
| nRemovedLits++; |
| } |
| Vec_IntForEachEntry( vClass, Ent, k ) |
| { |
| p->pReprs[Ent].fFailed = p->pReprs[Ent].fProved = 0; |
| p->pReprs[Ent].iRepr = GIA_VOID; |
| p->pNexts[Ent] = 0; |
| } |
| if ( Vec_IntSize(vClassNew) < 2 ) |
| { |
| nRemovedClas++; |
| continue; |
| } |
| Cec_ManSimClassCreate( p, vClassNew ); |
| } |
| Vec_IntFree( vClass ); |
| Vec_IntFree( vClassNew ); |
| if ( fVerbose ) |
| Abc_Print( 1, "Removed classes = %6d (out of %6d). Removed literals = %6d (out of %6d).\n", |
| nRemovedClas, nTotalClas, nRemovedLits, nTotalLits ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Marks proved equivalences.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerbose ) |
| { |
| Gia_Man_t * pMiter, * pTemp; |
| Gia_Obj_t * pObj; |
| int i, iLit, nAddPos, nLits = 0; |
| int nLitsAll, Counter = 0; |
| nLitsAll = Gia_ManEquivCountLitsAll( p ); |
| if ( nLitsAll == 0 ) |
| { |
| Abc_Print( 1, "Gia_ManEquivMark(): Current AIG does not have equivalences.\n" ); |
| return; |
| } |
| // read AIGER file |
| pMiter = Gia_AigerRead( pFileName, 0, 0, 0 ); |
| if ( pMiter == NULL ) |
| { |
| Abc_Print( 1, "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName ); |
| return; |
| } |
| if ( fSkipSome ) |
| { |
| Vec_Int_t * vTrace = Vec_IntAlloc( 100 ); |
| pTemp = Gia_ManSpecReduceTrace( p, vTrace, NULL ); |
| Gia_ManStop( pTemp ); |
| assert( Vec_IntSize(vTrace) == nLitsAll ); |
| // count the number of non-zero entries |
| nAddPos = 0; |
| Vec_IntForEachEntry( vTrace, iLit, i ) |
| if ( iLit ) |
| nAddPos++; |
| // check the number |
| if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nAddPos ) |
| { |
| Abc_Print( 1, "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGFilteredEquivNum(%d).\n", |
| Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nAddPos ); |
| Gia_ManStop( pMiter ); |
| Vec_IntFreeP( &vTrace ); |
| return; |
| } |
| // mark corresponding POs as solved |
| nLits = iLit = Counter = 0; |
| for ( i = 0; i < Gia_ManObjNum(p); i++ ) |
| { |
| if ( Gia_ObjRepr(p, i) == GIA_VOID ) |
| continue; |
| if ( Vec_IntEntry( vTrace, nLits++ ) == 0 ) |
| continue; |
| pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + iLit++ ); |
| if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven |
| { |
| Gia_ObjSetProved(p, i); |
| Counter++; |
| } |
| } |
| assert( nLits == nLitsAll ); |
| assert( iLit == nAddPos ); |
| Vec_IntFreeP( &vTrace ); |
| } |
| else |
| { |
| if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nLitsAll ) |
| { |
| Abc_Print( 1, "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGEquivNum(%d).\n", |
| Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nLitsAll ); |
| Gia_ManStop( pMiter ); |
| return; |
| } |
| // mark corresponding POs as solved |
| nLits = 0; |
| for ( i = 0; i < Gia_ManObjNum(p); i++ ) |
| { |
| if ( Gia_ObjRepr(p, i) == GIA_VOID ) |
| continue; |
| pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + nLits++ ); |
| if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven |
| { |
| Gia_ObjSetProved(p, i); |
| Counter++; |
| } |
| } |
| assert( nLits == nLitsAll ); |
| } |
| if ( fVerbose ) |
| Abc_Print( 1, "Set %d equivalences as proved.\n", Counter ); |
| Gia_ManStop( pMiter ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Transforms equiv classes by filtering those that correspond to disproved outputs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEquivFilter( Gia_Man_t * p, Vec_Int_t * vPoIds, int fVerbose ) |
| { |
| Gia_Man_t * pSrm; |
| Vec_Int_t * vTrace, * vMap; |
| int i, iObjId, Entry, Prev = -1; |
| // check if there are equivalences |
| if ( p->pReprs == NULL || p->pNexts == NULL ) |
| { |
| Abc_Print( 1, "Gia_ManEquivFilter(): Equivalence classes are not defined.\n" ); |
| return; |
| } |
| // check if PO indexes are available |
| if ( vPoIds == NULL ) |
| { |
| Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs is not available.\n" ); |
| return; |
| } |
| if ( Vec_IntSize(vPoIds) == 0 ) |
| return; |
| // create SRM with mapping into POs |
| vMap = Vec_IntAlloc( 1000 ); |
| vTrace = Vec_IntAlloc( 1000 ); |
| pSrm = Gia_ManSpecReduceTrace( p, vTrace, vMap ); |
| Vec_IntFree( vTrace ); |
| // the resulting array (vMap) maps PO indexes of the SRM into object IDs |
| assert( Gia_ManPoNum(pSrm) == Gia_ManPoNum(p) + Vec_IntSize(vMap) ); |
| Gia_ManStop( pSrm ); |
| if ( fVerbose ) |
| printf( "Design POs = %d. SRM POs = %d. Spec POs = %d. Disproved POs = %d.\n", |
| Gia_ManPoNum(p), Gia_ManPoNum(p) + Vec_IntSize(vMap), Vec_IntSize(vMap), Vec_IntSize(vPoIds) ); |
| // check if disproved POs satisfy the range |
| Vec_IntSort( vPoIds, 0 ); |
| Vec_IntForEachEntry( vPoIds, Entry, i ) |
| { |
| if ( Entry < 0 || Entry >= Gia_ManPoNum(p) + Vec_IntSize(vMap) ) |
| { |
| Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains PO index (%d),\n", Entry ); |
| Abc_Print( 1, "which does not fit into the range of available PO indexes of the SRM: [%d; %d].\n", 0, Gia_ManPoNum(p) + Vec_IntSize(vMap)-1 ); |
| Vec_IntFree( vMap ); |
| return; |
| } |
| if ( Entry < Gia_ManPoNum(p) ) |
| Abc_Print( 0, "Gia_ManEquivFilter(): One of the original POs (%d) have failed.\n", Entry ); |
| if ( Prev == Entry ) |
| { |
| Abc_Print( 1, "Gia_ManEquivFilter(): Array of disproved POs contains at least one duplicate entry (%d),\n", Entry ); |
| Vec_IntFree( vMap ); |
| return; |
| } |
| Prev = Entry; |
| } |
| // perform the reduction of the equivalence classes |
| Vec_IntForEachEntry( vPoIds, Entry, i ) |
| { |
| if ( Entry < Gia_ManPoNum(p) ) |
| continue; |
| iObjId = Vec_IntEntry( vMap, Entry - Gia_ManPoNum(p) ); |
| Gia_ObjUnsetRepr( p, iObjId ); |
| // Gia_ObjSetNext( p, iObjId, 0 ); |
| } |
| Vec_IntFree( vMap ); |
| ABC_FREE( p->pNexts ); |
| p->pNexts = Gia_ManDeriveNexts( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Transforms equiv classes by filtering those that correspond to disproved outputs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEquivFilterTest( Gia_Man_t * p ) |
| { |
| Vec_Int_t * vPoIds; |
| int i; |
| vPoIds = Vec_IntAlloc( 1000 ); |
| for ( i = 0; i < 10; i++ ) |
| { |
| Vec_IntPush( vPoIds, Gia_ManPoNum(p) + 2 * i + 2 ); |
| printf( "%d ", Gia_ManPoNum(p) + 2*i + 2 ); |
| } |
| printf( "\n" ); |
| Gia_ManEquivFilter( p, vPoIds, 1 ); |
| Vec_IntFree( vPoIds ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Transforms equiv classes by setting a good representative.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEquivImprove( Gia_Man_t * p ) |
| { |
| Vec_Int_t * vClass; |
| int i, k, iNode, iRepr; |
| int iReprBest, iLevelBest, iLevelCur, iMffcBest, iMffcCur; |
| assert( p->pReprs != NULL && p->pNexts != NULL ); |
| Gia_ManLevelNum( p ); |
| Gia_ManCreateRefs( p ); |
| // iterate over class candidates |
| vClass = Vec_IntAlloc( 100 ); |
| Gia_ManForEachClass( p, i ) |
| { |
| Vec_IntClear( vClass ); |
| iReprBest = -1; |
| iLevelBest = iMffcBest = ABC_INFINITY; |
| Gia_ClassForEachObj( p, i, k ) |
| { |
| iLevelCur = Gia_ObjLevel( p,Gia_ManObj(p, k) ); |
| iMffcCur = Gia_NodeMffcSize( p, Gia_ManObj(p, k) ); |
| if ( iLevelBest > iLevelCur || (iLevelBest == iLevelCur && iMffcBest > iMffcCur) ) |
| { |
| iReprBest = k; |
| iLevelBest = iLevelCur; |
| iMffcBest = iMffcCur; |
| } |
| Vec_IntPush( vClass, k ); |
| } |
| assert( Vec_IntSize( vClass ) > 1 ); |
| assert( iReprBest > 0 ); |
| if ( i == iReprBest ) |
| continue; |
| /* |
| Abc_Print( 1, "Repr/Best = %6d/%6d. Lev = %3d/%3d. Mffc = %3d/%3d.\n", |
| i, iReprBest, Gia_ObjLevel( p,Gia_ManObj(p, i) ), Gia_ObjLevel( p,Gia_ManObj(p, iReprBest) ), |
| Gia_NodeMffcSize( p, Gia_ManObj(p, i) ), Gia_NodeMffcSize( p, Gia_ManObj(p, iReprBest) ) ); |
| */ |
| iRepr = iReprBest; |
| Gia_ObjSetRepr( p, iRepr, GIA_VOID ); |
| Gia_ObjSetProved( p, i ); |
| Gia_ObjUnsetProved( p, iRepr ); |
| Vec_IntForEachEntry( vClass, iNode, k ) |
| if ( iNode != iRepr ) |
| Gia_ObjSetRepr( p, iNode, iRepr ); |
| } |
| Vec_IntFree( vClass ); |
| ABC_FREE( p->pNexts ); |
| // p->pNexts = Gia_ManDeriveNexts( p ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if pOld is in the TFI of pNode.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ObjCheckTfi_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode, Vec_Ptr_t * vVisited ) |
| { |
| // check the trivial cases |
| if ( pNode == NULL ) |
| return 0; |
| if ( Gia_ObjIsCi(pNode) ) |
| return 0; |
| // if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode |
| // return 0; |
| if ( pNode == pOld ) |
| return 1; |
| // skip the visited node |
| if ( pNode->fMark0 ) |
| return 0; |
| pNode->fMark0 = 1; |
| Vec_PtrPush( vVisited, pNode ); |
| // check the children |
| if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) ) |
| return 1; |
| if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) ) |
| return 1; |
| // check equivalent nodes |
| return Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if pOld is in the TFI of pNode.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode ) |
| { |
| Vec_Ptr_t * vVisited; |
| Gia_Obj_t * pObj; |
| int RetValue, i; |
| assert( !Gia_IsComplement(pOld) ); |
| assert( !Gia_IsComplement(pNode) ); |
| vVisited = Vec_PtrAlloc( 100 ); |
| RetValue = Gia_ObjCheckTfi_rec( p, pOld, pNode, vVisited ); |
| Vec_PtrForEachEntry( Gia_Obj_t *, vVisited, pObj, i ) |
| pObj->fMark0 = 0; |
| Vec_PtrFree( vVisited ); |
| return RetValue; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Adds the next entry while making choices.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode ) |
| { |
| if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 ) |
| { |
| Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) ); |
| return; |
| } |
| Gia_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates the AIG in the DFS order.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) |
| { |
| Gia_Obj_t * pRepr, * pReprNew, * pObjNew; |
| if ( ~pObj->Value ) |
| return; |
| if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) |
| { |
| if ( Gia_ObjIsConst0(pRepr) ) |
| { |
| pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); |
| return; |
| } |
| Gia_ManEquivToChoices_rec( pNew, p, pRepr ); |
| assert( Gia_ObjIsAnd(pObj) ); |
| Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); |
| Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) ); |
| pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) ) |
| { |
| assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) ); |
| return; |
| } |
| if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit |
| return; |
| assert( pRepr->Value < pObj->Value ); |
| pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) ); |
| pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) ); |
| if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) ) |
| { |
| // assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew ); |
| if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) != pReprNew ) |
| return; |
| pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); |
| return; |
| } |
| if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) ) |
| { |
| assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 ); |
| Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) ); |
| Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew ); |
| } |
| pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); |
| return; |
| } |
| assert( Gia_ObjIsAnd(pObj) ); |
| Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); |
| Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) ); |
| pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Removes choices, which contain fanouts.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManRemoveBadChoices( Gia_Man_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i, iObj, iPrev, Counter = 0; |
| // mark nodes with fanout |
| Gia_ManForEachObj( p, pObj, i ) |
| { |
| pObj->fMark0 = 0; |
| if ( Gia_ObjIsAnd(pObj) ) |
| { |
| Gia_ObjFanin0(pObj)->fMark0 = 1; |
| Gia_ObjFanin1(pObj)->fMark0 = 1; |
| } |
| else if ( Gia_ObjIsCo(pObj) ) |
| Gia_ObjFanin0(pObj)->fMark0 = 1; |
| } |
| // go through the classes and remove |
| Gia_ManForEachClass( p, i ) |
| { |
| for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) ) |
| { |
| if ( !Gia_ManObj(p, iObj)->fMark0 ) |
| { |
| iPrev = iObj; |
| continue; |
| } |
| Gia_ObjSetRepr( p, iObj, GIA_VOID ); |
| Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) ); |
| Gia_ObjSetNext( p, iObj, 0 ); |
| Counter++; |
| } |
| } |
| // remove the marks |
| Gia_ManCleanMark0( p ); |
| // Abc_Print( 1, "Removed %d bad choices.\n", Counter ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reduces AIG using equivalence classes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots ) |
| { |
| Vec_Int_t * vNodes; |
| Gia_Man_t * pNew, * pTemp; |
| Gia_Obj_t * pObj, * pRepr; |
| int i; |
| //Gia_ManEquivPrintClasses( p, 0, 0 ); |
| assert( (Gia_ManCoNum(p) % nSnapshots) == 0 ); |
| Gia_ManSetPhase( p ); |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); |
| pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) ); |
| for ( i = 0; i < Gia_ManObjNum(p); i++ ) |
| Gia_ObjSetRepr( pNew, i, GIA_VOID ); |
| Gia_ManFillValue( p ); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManForEachCi( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCi(pNew); |
| Gia_ManForEachRo( p, pObj, i ) |
| if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) |
| { |
| assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) ); |
| pObj->Value = pRepr->Value; |
| } |
| Gia_ManHashAlloc( pNew ); |
| Gia_ManForEachCo( p, pObj, i ) |
| Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); |
| vNodes = Gia_ManGetDangling( p ); |
| Gia_ManForEachObjVec( vNodes, p, pObj, i ) |
| Gia_ManEquivToChoices_rec( pNew, p, pObj ); |
| Vec_IntFree( vNodes ); |
| Gia_ManForEachCo( p, pObj, i ) |
| if ( i % nSnapshots == 0 ) |
| Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| Gia_ManHashStop( pNew ); |
| Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); |
| Gia_ManRemoveBadChoices( pNew ); |
| //Gia_ManEquivPrintClasses( pNew, 0, 0 ); |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| Gia_ManStop( pTemp ); |
| //Gia_ManEquivPrintClasses( pNew, 0, 0 ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Counts the number of choice nodes] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManCountChoiceNodes( Gia_Man_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i, Counter = 0; |
| if ( p->pReprs == NULL || p->pNexts == NULL ) |
| return 0; |
| Gia_ManForEachObj( p, pObj, i ) |
| Counter += Gia_ObjIsHead( p, i ); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Counts the number of choices] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManCountChoices( Gia_Man_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i, Counter = 0; |
| if ( p->pReprs == NULL || p->pNexts == NULL ) |
| return 0; |
| Gia_ManForEachObj( p, pObj, i ) |
| Counter += (int)(Gia_ObjNext( p, i ) > 0); |
| return Counter; |
| } |
| |
| ABC_NAMESPACE_IMPL_END |
| |
| #include "aig/aig/aig.h" |
| #include "aig/saig/saig.h" |
| #include "proof/cec/cec.h" |
| #include "giaAig.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if AIG has dangling nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManHasNoEquivs( Gia_Man_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i; |
| if ( p->pReprs == NULL ) |
| return 1; |
| Gia_ManForEachObj( p, pObj, i ) |
| if ( Gia_ObjReprObj(p, i) != NULL ) |
| break; |
| return i == Gia_ManObjNum(p); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Implements iteration during speculation.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int fStart, int fCheckMiter, int fVerbose ) |
| { |
| // extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ); |
| Aig_Man_t * pTemp; |
| Gia_Man_t * pSrm, * pReduce, * pAux; |
| int nIter, nStart = 0; |
| if ( pGia->pReprs == NULL || pGia->pNexts == NULL ) |
| { |
| Abc_Print( 1, "Gia_CommandSpecI(): Equivalence classes are not defined.\n" ); |
| return 0; |
| } |
| // (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim |
| Gia_ManCleanMark0( pGia ); |
| Gia_ManPrintStats( pGia, NULL ); |
| for ( nIter = 0; ; nIter++ ) |
| { |
| if ( Gia_ManHasNoEquivs(pGia) ) |
| { |
| Abc_Print( 1, "Gia_CommandSpecI: No equivalences left.\n" ); |
| break; |
| } |
| Abc_Print( 1, "ITER %3d : ", nIter ); |
| // if ( fVerbose ) |
| // Abc_Print( 1, "Starting BMC from frame %d.\n", nStart ); |
| // if ( fVerbose ) |
| // Gia_ManPrintStats( pGia, 0 ); |
| Gia_ManPrintStatsClasses( pGia ); |
| // perform speculative reduction |
| // if ( Gia_ManPoNum(pSrm) <= Gia_ManPoNum(pGia) ) |
| if ( !Cec_ManCheckNonTrivialCands(pGia) ) |
| { |
| Abc_Print( 1, "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" ); |
| break; |
| } |
| pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 ); |
| // bmc2 -F 100 -C 25000 |
| { |
| Abc_Cex_t * pCex; |
| int nFrames = nFramesInit; // different from default |
| int nNodeDelta = 2000; |
| int nBTLimit = nBTLimitInit; // different from default |
| int nBTLimitAll = 2000000; |
| pTemp = Gia_ManToAig( pSrm, 0 ); |
| // Aig_ManPrintStats( pTemp ); |
| Gia_ManStop( pSrm ); |
| Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL, 0, 0 ); |
| pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL; |
| Aig_ManStop( pTemp ); |
| if ( pCex == NULL ) |
| { |
| Abc_Print( 1, "Gia_CommandSpecI(): Internal BMC could not find a counter-example.\n" ); |
| break; |
| } |
| if ( fStart ) |
| nStart = pCex->iFrame; |
| // perform simulation |
| { |
| Cec_ParSim_t Pars, * pPars = &Pars; |
| Cec_ManSimSetDefaultParams( pPars ); |
| pPars->fCheckMiter = fCheckMiter; |
| if ( Cec_ManSeqResimulateCounter( pGia, pPars, pCex ) ) |
| { |
| ABC_FREE( pCex ); |
| break; |
| } |
| ABC_FREE( pCex ); |
| } |
| } |
| // write equivalence classes |
| Gia_AigerWrite( pGia, "gore.aig", 0, 0 ); |
| // reduce the model |
| pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 ); |
| if ( pReduce ) |
| { |
| pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 ); |
| Gia_ManStop( pAux ); |
| Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 ); |
| // Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" ); |
| // Gia_ManPrintStatsShort( pReduce ); |
| Gia_ManStop( pReduce ); |
| } |
| } |
| return 1; |
| } |
| |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reduces AIG using equivalence classes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * pName2, int fLatchA, int fLatchB ) |
| { |
| Gia_Man_t * pGia1, * pGia2, * pMiter; |
| Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj; |
| int i, iObj, iNext, Counter = 0; |
| if ( pGia->pReprs == NULL || pGia->pNexts == NULL ) |
| { |
| Abc_Print( 1, "Equivalences are not defined.\n" ); |
| return 0; |
| } |
| pGia1 = Gia_AigerRead( pName1, 0, 0, 0 ); |
| if ( pGia1 == NULL ) |
| { |
| Abc_Print( 1, "Cannot read first file %s.\n", pName1 ); |
| return 0; |
| } |
| pGia2 = Gia_AigerRead( pName2, 0, 0, 0 ); |
| if ( pGia2 == NULL ) |
| { |
| Gia_ManStop( pGia2 ); |
| Abc_Print( 1, "Cannot read second file %s.\n", pName2 ); |
| return 0; |
| } |
| pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 ); |
| if ( pMiter == NULL ) |
| { |
| Gia_ManStop( pGia1 ); |
| Gia_ManStop( pGia2 ); |
| Abc_Print( 1, "Cannot create sequential miter.\n" ); |
| return 0; |
| } |
| // make sure the miter is isomorphic |
| if ( Gia_ManObjNum(pGia) != Gia_ManObjNum(pMiter) ) |
| { |
| Gia_ManStop( pGia1 ); |
| Gia_ManStop( pGia2 ); |
| Gia_ManStop( pMiter ); |
| Abc_Print( 1, "The number of objects in different.\n" ); |
| return 0; |
| } |
| if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) ) |
| { |
| Gia_ManStop( pGia1 ); |
| Gia_ManStop( pGia2 ); |
| Gia_ManStop( pMiter ); |
| Abc_Print( 1, "The AIG structure of the miter does not match.\n" ); |
| return 0; |
| } |
| // transfer copies |
| Gia_ManCleanMark0( pGia ); |
| Gia_ManForEachObj( pGia1, pObj1, i ) |
| { |
| if ( pObj1->Value == ~0 ) |
| continue; |
| pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) ); |
| pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) ); |
| pObj->fMark0 = 1; |
| } |
| Gia_ManCleanMark1( pGia ); |
| Gia_ManForEachObj( pGia2, pObj2, i ) |
| { |
| if ( pObj2->Value == ~0 ) |
| continue; |
| pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) ); |
| pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) ); |
| pObj->fMark1 = 1; |
| } |
| |
| // filter equivalences |
| Gia_ManForEachConst( pGia, i ) |
| { |
| Gia_ObjUnsetRepr( pGia, i ); |
| assert( pGia->pNexts[i] == 0 ); |
| } |
| Gia_ManForEachClass( pGia, i ) |
| { |
| // find the first colorA and colorB |
| int ClassA = -1, ClassB = -1; |
| Gia_ClassForEachObj( pGia, i, iObj ) |
| { |
| pObj = Gia_ManObj( pGia, iObj ); |
| if ( ClassA == -1 && pObj->fMark0 && !pObj->fMark1 ) |
| { |
| if ( fLatchA && !Gia_ObjIsRo(pGia, pObj) ) |
| continue; |
| ClassA = iObj; |
| } |
| if ( ClassB == -1 && pObj->fMark1 && !pObj->fMark0 ) |
| { |
| if ( fLatchB && !Gia_ObjIsRo(pGia, pObj) ) |
| continue; |
| ClassB = iObj; |
| } |
| } |
| // undo equivalence classes |
| for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj; |
| iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) ) |
| { |
| Gia_ObjUnsetRepr( pGia, iObj ); |
| Gia_ObjSetNext( pGia, iObj, 0 ); |
| } |
| assert( !Gia_ObjIsHead(pGia, i) ); |
| if ( ClassA > 0 && ClassB > 0 ) |
| { |
| if ( ClassA > ClassB ) |
| { |
| ClassA ^= ClassB; |
| ClassB ^= ClassA; |
| ClassA ^= ClassB; |
| } |
| assert( ClassA < ClassB ); |
| Gia_ObjSetNext( pGia, ClassA, ClassB ); |
| Gia_ObjSetRepr( pGia, ClassB, ClassA ); |
| Counter++; |
| assert( Gia_ObjIsHead(pGia, ClassA) ); |
| } |
| } |
| Abc_Print( 1, "The number of two-node classes after filtering = %d.\n", Counter ); |
| //Gia_ManEquivPrintClasses( pGia, 1, 0 ); |
| |
| Gia_ManCleanMark0( pGia ); |
| Gia_ManCleanMark1( pGia ); |
| return 1; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reduces AIG using equivalence classes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName2 ) |
| { |
| Vec_Int_t * vNodes; |
| Gia_Man_t * pGia1, * pGia2, * pMiter; |
| Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj = NULL; |
| int i, k, iObj, iNext, iPrev, iRepr; |
| int iLitsOld, iLitsNew; |
| if ( pGia->pReprs == NULL || pGia->pNexts == NULL ) |
| { |
| Abc_Print( 1, "Equivalences are not defined.\n" ); |
| return 0; |
| } |
| pGia1 = Gia_AigerRead( pName1, 0, 0, 0 ); |
| if ( pGia1 == NULL ) |
| { |
| Abc_Print( 1, "Cannot read first file %s.\n", pName1 ); |
| return 0; |
| } |
| pGia2 = Gia_AigerRead( pName2, 0, 0, 0 ); |
| if ( pGia2 == NULL ) |
| { |
| Gia_ManStop( pGia2 ); |
| Abc_Print( 1, "Cannot read second file %s.\n", pName2 ); |
| return 0; |
| } |
| pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 ); |
| if ( pMiter == NULL ) |
| { |
| Gia_ManStop( pGia1 ); |
| Gia_ManStop( pGia2 ); |
| Abc_Print( 1, "Cannot create sequential miter.\n" ); |
| return 0; |
| } |
| // make sure the miter is isomorphic |
| if ( Gia_ManObjNum(pGia) != Gia_ManObjNum(pMiter) ) |
| { |
| Gia_ManStop( pGia1 ); |
| Gia_ManStop( pGia2 ); |
| Gia_ManStop( pMiter ); |
| Abc_Print( 1, "The number of objects in different.\n" ); |
| return 0; |
| } |
| if ( memcmp( pGia->pObjs, pMiter->pObjs, sizeof(Gia_Obj_t) * Gia_ManObjNum(pGia) ) ) |
| { |
| Gia_ManStop( pGia1 ); |
| Gia_ManStop( pGia2 ); |
| Gia_ManStop( pMiter ); |
| Abc_Print( 1, "The AIG structure of the miter does not match.\n" ); |
| return 0; |
| } |
| // transfer copies |
| Gia_ManCleanMark0( pGia ); |
| Gia_ManForEachObj( pGia1, pObj1, i ) |
| { |
| if ( pObj1->Value == ~0 ) |
| continue; |
| pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) ); |
| pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) ); |
| pObj->fMark0 = 1; |
| } |
| Gia_ManCleanMark1( pGia ); |
| Gia_ManForEachObj( pGia2, pObj2, i ) |
| { |
| if ( pObj2->Value == ~0 ) |
| continue; |
| pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) ); |
| pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) ); |
| pObj->fMark1 = 1; |
| } |
| |
| // filter equivalences |
| iLitsOld = iLitsNew = 0; |
| Gia_ManForEachConst( pGia, i ) |
| { |
| iLitsOld++; |
| pObj = Gia_ManObj( pGia, i ); |
| assert( pGia->pNexts[i] == 0 ); |
| assert( pObj->fMark0 || pObj->fMark1 ); |
| if ( pObj->fMark0 && pObj->fMark1 ) // belongs to both A and B |
| Gia_ObjUnsetRepr( pGia, i ); |
| else |
| iLitsNew++; |
| } |
| // filter equivalences |
| vNodes = Vec_IntAlloc( 100 ); |
| Gia_ManForEachClass( pGia, i ) |
| { |
| int fSeenA = 0, fSeenB = 0; |
| assert( pObj->fMark0 || pObj->fMark1 ); |
| Vec_IntClear( vNodes ); |
| Gia_ClassForEachObj( pGia, i, iObj ) |
| { |
| pObj = Gia_ManObj( pGia, iObj ); |
| if ( pObj->fMark0 && !pObj->fMark1 ) |
| { |
| fSeenA = 1; |
| Vec_IntPush( vNodes, iObj ); |
| } |
| if ( !pObj->fMark0 && pObj->fMark1 ) |
| { |
| fSeenB = 1; |
| Vec_IntPush( vNodes, iObj ); |
| } |
| iLitsOld++; |
| } |
| iLitsOld--; |
| // undo equivalence classes |
| for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj; |
| iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) ) |
| { |
| Gia_ObjUnsetRepr( pGia, iObj ); |
| Gia_ObjSetNext( pGia, iObj, 0 ); |
| } |
| assert( !Gia_ObjIsHead(pGia, i) ); |
| if ( fSeenA && fSeenB && Vec_IntSize(vNodes) > 1 ) |
| { |
| // create new class |
| iPrev = iRepr = Vec_IntEntry( vNodes, 0 ); |
| Vec_IntForEachEntryStart( vNodes, iObj, k, 1 ) |
| { |
| Gia_ObjSetRepr( pGia, iObj, iRepr ); |
| Gia_ObjSetNext( pGia, iPrev, iObj ); |
| iPrev = iObj; |
| iLitsNew++; |
| } |
| assert( Gia_ObjNext(pGia, iPrev) == 0 ); |
| } |
| } |
| Vec_IntFree( vNodes ); |
| Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew ); |
| //Gia_ManEquivPrintClasses( pGia, 1, 0 ); |
| |
| Gia_ManCleanMark0( pGia ); |
| Gia_ManCleanMark1( pGia ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlopsWith, int fUseRiDrivers ) |
| { |
| Gia_Obj_t * pObjR; |
| Vec_Int_t * vNodes, * vFfIds; |
| int i, k, iObj, iNext, iPrev, iRepr; |
| int iLitsOld = 0, iLitsNew = 0; |
| assert( fFlopsOnly ^ fFlopsWith ); |
| vNodes = Vec_IntAlloc( 100 ); |
| // select nodes "flop" node IDs |
| vFfIds = Vec_IntStart( Gia_ManObjNum(pGia) ); |
| if ( fUseRiDrivers ) |
| { |
| Gia_ManForEachRi( pGia, pObjR, i ) |
| Vec_IntWriteEntry( vFfIds, Gia_ObjFaninId0p(pGia, pObjR), 1 ); |
| } |
| else |
| { |
| Gia_ManForEachRo( pGia, pObjR, i ) |
| Vec_IntWriteEntry( vFfIds, Gia_ObjId(pGia, pObjR), 1 ); |
| } |
| // remove all non-flop constants |
| Gia_ManForEachConst( pGia, i ) |
| { |
| iLitsOld++; |
| assert( pGia->pNexts[i] == 0 ); |
| if ( !Vec_IntEntry(vFfIds, i) ) |
| Gia_ObjUnsetRepr( pGia, i ); |
| else |
| iLitsNew++; |
| } |
| // clear the classes |
| if ( fFlopsOnly ) |
| { |
| Gia_ManForEachClass( pGia, i ) |
| { |
| Vec_IntClear( vNodes ); |
| Gia_ClassForEachObj( pGia, i, iObj ) |
| { |
| if ( Vec_IntEntry(vFfIds, iObj) ) |
| Vec_IntPush( vNodes, iObj ); |
| iLitsOld++; |
| } |
| iLitsOld--; |
| // undo equivalence classes |
| for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj; |
| iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) ) |
| { |
| Gia_ObjUnsetRepr( pGia, iObj ); |
| Gia_ObjSetNext( pGia, iObj, 0 ); |
| } |
| assert( !Gia_ObjIsHead(pGia, i) ); |
| if ( Vec_IntSize(vNodes) > 1 ) |
| { |
| // create new class |
| iPrev = iRepr = Vec_IntEntry( vNodes, 0 ); |
| Vec_IntForEachEntryStart( vNodes, iObj, k, 1 ) |
| { |
| Gia_ObjSetRepr( pGia, iObj, iRepr ); |
| Gia_ObjSetNext( pGia, iPrev, iObj ); |
| iPrev = iObj; |
| iLitsNew++; |
| } |
| assert( Gia_ObjNext(pGia, iPrev) == 0 ); |
| } |
| } |
| } |
| else |
| { |
| Gia_ManForEachClass( pGia, i ) |
| { |
| int fSeenFlop = 0; |
| Gia_ClassForEachObj( pGia, i, iObj ) |
| { |
| if ( Vec_IntEntry(vFfIds, iObj) ) |
| fSeenFlop = 1; |
| iLitsOld++; |
| iLitsNew++; |
| } |
| iLitsOld--; |
| iLitsNew--; |
| if ( fSeenFlop ) |
| continue; |
| // undo equivalence classes |
| for ( iObj = i, iNext = Gia_ObjNext(pGia, iObj); iObj; |
| iObj = iNext, iNext = Gia_ObjNext(pGia, iObj) ) |
| { |
| Gia_ObjUnsetRepr( pGia, iObj ); |
| Gia_ObjSetNext( pGia, iObj, 0 ); |
| iLitsNew--; |
| } |
| iLitsNew++; |
| assert( !Gia_ObjIsHead(pGia, i) ); |
| } |
| } |
| Vec_IntFree( vNodes ); |
| Vec_IntFree( vFfIds ); |
| Abc_Print( 1, "The number of literals: Before = %d. After = %d.\n", iLitsOld, iLitsNew ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
