diff options
| -rw-r--r-- | src/aig/cec/cecCec.c | 1 | ||||
| -rw-r--r-- | src/aig/cec/cecClass.c | 5 | ||||
| -rw-r--r-- | src/aig/cec/cecCore.c | 14 | ||||
| -rw-r--r-- | src/aig/cec/cecSeq.c | 2 | ||||
| -rw-r--r-- | src/aig/cec/cecSolve.c | 3 | ||||
| -rw-r--r-- | src/aig/gia/gia.h | 28 | ||||
| -rw-r--r-- | src/aig/gia/giaAig.c | 23 | ||||
| -rw-r--r-- | src/aig/gia/giaAiger.c | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaCof.c | 226 | ||||
| -rw-r--r-- | src/aig/gia/giaDup.c | 195 | ||||
| -rw-r--r-- | src/aig/gia/giaEnable.c | 229 | ||||
| -rw-r--r-- | src/aig/gia/giaEquiv.c | 239 | ||||
| -rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
| -rw-r--r-- | src/aig/saig/saigBmc2.c | 12 | ||||
| -rw-r--r-- | src/aig/ssw/sswCore.c | 24 | ||||
| -rw-r--r-- | src/base/abc/abc.h | 1 | ||||
| -rw-r--r-- | src/base/abc/abcHie.c | 259 | ||||
| -rw-r--r-- | src/base/abc/abcNames.c | 26 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 125 | ||||
| -rw-r--r-- | src/base/abci/abcDar.c | 6 | ||||
| -rw-r--r-- | src/base/main/mainMC.c | 4 |
21 files changed, 1196 insertions, 229 deletions
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c index 96bddbcb..f3d3dea9 100644 --- a/src/aig/cec/cecCec.c +++ b/src/aig/cec/cecCec.c @@ -129,6 +129,7 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ) double clkTotal = clock(); // sweep for equivalences Cec_ManFraSetDefaultParams( pParsFra ); + pParsFra->nItersMax = 1000; pParsFra->nBTLimit = pPars->nBTLimit; pParsFra->TimeLimit = pPars->TimeLimit; pParsFra->fVerbose = pPars->fVerbose; diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c index 0cac88af..26ff543a 100644 --- a/src/aig/cec/cecClass.c +++ b/src/aig/cec/cecClass.c @@ -242,6 +242,7 @@ void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass ) } else { + assert( Repr < Ent ); Gia_ObjSetRepr( p, Ent, Repr ); Gia_ObjSetNext( p, EntPrev, Ent ); EntPrev = Ent; @@ -500,7 +501,7 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat ) ***********************************************************************/ void Cec_ManSimFindBestPattern( Cec_ManSim_t * p ) -{ +{ unsigned * pInfo; int i, ScoreBest = 0, iPatBest = 1; // find the best pattern @@ -838,7 +839,7 @@ int Cec_ManSimClassesRefine( Cec_ManSim_t * p ) p->nWords = p->pPars->nWords; for ( i = 0; i < p->pPars->nRounds; i++ ) { - if ( (i % 4) == 0 && p->pPars->fVerbose ) + if ( (i % (p->pPars->nRounds / 5)) == 0 && p->pPars->fVerbose ) Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) ); Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo ); if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index 061c3a7d..8e66179f 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -90,10 +90,10 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p ) void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p ) { memset( p, 0, sizeof(Cec_ParSmf_t) ); - p->nWords = 15; // the number of simulation words - p->nRounds = 15; // the number of simulation rounds + p->nWords = 31; // the number of simulation words + p->nRounds = 1; // the number of simulation rounds p->nFrames = 2; // the number of time frames - p->nBTLimit = 1000; // conflict limit at a node + p->nBTLimit = 100; // conflict limit at a node p->TimeLimit = 0; // the runtime limit in seconds p->fDualOut = 0; // miter with separate outputs p->fCheckMiter = 0; // the circuit is the miter @@ -118,8 +118,8 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ) p->nWords = 15; // the number of simulation words p->nRounds = 15; // the number of simulation rounds p->TimeLimit = 0; // the runtime limit in seconds - p->nItersMax = 1000; // the maximum number of iterations of SAT sweeping - p->nBTLimit = 1000; // conflict limit at a node + p->nItersMax = 10; // the maximum number of iterations of SAT sweeping + p->nBTLimit = 100; // conflict limit at a node p->nLevelMax = 0; // restriction on the level of nodes to be swept p->nDepthMax = 1; // the depth in terms of steps of speculative reduction p->fRewriting = 0; // enables AIG rewriting @@ -322,6 +322,8 @@ p->timeSat += clock() - clk; // update the manager pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut ); Gia_ManStop( pTemp ); + if ( p->pAig == NULL ) + break; if ( p->pPars->fVerbose ) { printf( "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ", @@ -381,7 +383,7 @@ finalize: } pTemp = p->pAig; p->pAig = NULL; - if ( pTemp == NULL ) + if ( pTemp == NULL && pSim->iOut >= 0 ) printf( "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut ); else if ( pSim->pCexes ) printf( "Disproved %d outputs of the miter.\n", pSim->nOuts ); diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index 6cb229ae..1a398e2e 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -255,7 +255,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) Gia_Man_t * pSrm; int r, nPats, RetValue = -1; if ( pAig->pReprs == NULL ) - { + { printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" ); return -1; } diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c index 2b6997e1..24d5c3ed 100644 --- a/src/aig/cec/cecSolve.c +++ b/src/aig/cec/cecSolve.c @@ -703,7 +703,8 @@ void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pP } p->timeTotal = clock() - clk; Bar_ProgressStop( pProgress ); -// Cec_ManSatPrintStats( p ); + if ( pPars->fVerbose ) + Cec_ManSatPrintStats( p ); Cec_ManSatStop( p ); if ( pnPats ) *pnPats = iPat-1; diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index c5d55565..1c3529ba 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -67,6 +67,11 @@ struct Gia_Obj_t_ unsigned Value; // application-specific value }; +// Value is currently use to store several types of information +// - pointer to the next node in the hash table during structural hashing +// - pointer to the node copy during duplication +// - traversal ID of the node during traversal +// - reference counter of the node (will not be used in the future) // sequential counter-example typedef struct Gia_Cex_t_ Gia_Cex_t; @@ -177,6 +182,7 @@ static inline int Gia_ManPoNum( Gia_Man_t * p ) { return Vec_IntS static inline int Gia_ManRegNum( Gia_Man_t * p ) { return p->nRegs; } static inline int Gia_ManObjNum( Gia_Man_t * p ) { return p->nObjs; } static inline int Gia_ManAndNum( Gia_Man_t * p ) { return p->nObjs - Vec_IntSize(p->vCis) - Vec_IntSize(p->vCos) - 1; } +static inline int Gia_ManCandNum( Gia_Man_t * p ) { return Gia_ManCiNum(p) + Gia_ManAndNum(p); } static inline Gia_Obj_t * Gia_ManConst0( Gia_Man_t * p ) { return p->pObjs; } static inline Gia_Obj_t * Gia_ManConst1( Gia_Man_t * p ) { return Gia_Not(Gia_ManConst0(p)); } @@ -193,6 +199,7 @@ static inline int Gia_ObjIsAndOrConst0( Gia_Obj_t * pObj ) { static inline int Gia_ObjIsCi( Gia_Obj_t * pObj ) { return pObj->fTerm && pObj->iDiff0 == GIA_NONE; } static inline int Gia_ObjIsCo( Gia_Obj_t * pObj ) { return pObj->fTerm && pObj->iDiff0 != GIA_NONE; } static inline int Gia_ObjIsAnd( Gia_Obj_t * pObj ) { return!pObj->fTerm && pObj->iDiff0 != GIA_NONE; } +static inline int Gia_ObjIsCand( Gia_Obj_t * pObj ) { return Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj); } static inline int Gia_ObjIsConst0( Gia_Obj_t * pObj ) { return pObj->iDiff0 == GIA_NONE && pObj->iDiff1 == GIA_NONE; } static inline int Gia_ManObjIsConst0( Gia_Man_t * p, Gia_Obj_t * pObj){ return pObj == p->pObjs; } @@ -232,6 +239,12 @@ static inline int Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFani static inline int Gia_ObjFanin0Copy( Gia_Obj_t * pObj ) { return Gia_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); } static inline int Gia_ObjFanin1Copy( Gia_Obj_t * pObj ) { return Gia_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); } +static inline int Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)]; } +static inline void Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit; } + +static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } +static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } + static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Gia_Lit2Var(iLit)), Gia_LitIsCompl(iLit) ); } static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_Var2Lit( Gia_ObjId(p, pObj), Gia_IsComplement(pObj) ); } static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); } @@ -397,6 +410,8 @@ static inline int * Gia_ObjGateFanins( Gia_Man_t * p, int Id ) { re for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Vec_IntEntry(vVec,i))); i++ ) #define Gia_ManForEachObjVecLit( vVec, p, pObj, fCompl, i ) \ for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Gia_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Gia_LitIsCompl(Vec_IntEntry(vVec,i))),1); i++ ) +#define Gia_ManForEachObjReverse( p, pObj, i ) \ + for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) #define Gia_ManForEachAnd( p, pObj, i ) \ for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else #define Gia_ManForEachCi( p, pObj, i ) \ @@ -429,6 +444,9 @@ extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ); extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact ); /*=== giaCof.c ============================================================*/ extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ); +extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar ); +extern Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose ); +extern Gia_Man_t * Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose ); /*=== giaDfs.c ============================================================*/ extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp ); extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes ); @@ -436,6 +454,7 @@ extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNo extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes ); /*=== giaDup.c ============================================================*/ extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes ); extern Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ); @@ -444,22 +463,23 @@ extern Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj ); extern Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits ); extern Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos ); -extern Gia_Man_t * Gia_ManDupCofactored( Gia_Man_t * p, int iVar, int nLimFan ); extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits ); extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fDualOut, int fSeq, int fVerbose ); extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ); /*=== giaEnable.c ==========================================================*/ -extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset ); +extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); +extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose ); /*=== giaEquiv.c ==========================================================*/ +extern int Gia_ManCheckTopoOrder( Gia_Man_t * p ); extern int * Gia_ManDeriveNexts( Gia_Man_t * p ); extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter ); extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ); -extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll ); +extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose ); extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ); extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); -extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ); +extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose ); extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut ); extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ); /*=== giaFanout.c =========================================================*/ diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 544cfe0d..3f707e1c 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -205,6 +205,29 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit ) +{ + Aig_Man_t * pMan; + Gia_Man_t * pGia, * pTemp; + pGia = Gia_ManFromAig( p ); + pGia = Gia_ManUnrollAndCofactor( pTemp = pGia, nFrames, nCofFanLit, 1 ); + Gia_ManStop( pTemp ); + pMan = Gia_ManToAig( pGia ); + Gia_ManStop( pGia ); + return pMan; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index cfd2dc73..da1a8c9f 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -230,6 +230,7 @@ Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize ) iNode += Item; pReprs[iNode].fProved = fProved; pReprs[iNode].iRepr = iRepr; + assert( iRepr < iNode ); //printf( "Node = %d ", iNode ); } return pReprs; diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c index 735aca72..c5efa839 100644 --- a/src/aig/gia/giaCof.c +++ b/src/aig/gia/giaCof.c @@ -685,6 +685,232 @@ ABC_PRT( "Time", clock() - clk ); } +/**Function************************************************************* + + Synopsis [Duplicates AIG in the DFS order while putting CIs first.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj, * pPivot; + int i, iCofVar = -1; + if ( !(iVar > 0 && iVar < Gia_ManObjNum(p)) ) + { + printf( "Gia_ManDupCof(): Variable %d is out of range (%d; %d).\n", iVar, 0, Gia_ManObjNum(p) ); + return NULL; + } + // find the cofactoring variable + pPivot = Gia_ManObj( p, iVar ); + if ( !Gia_ObjIsCand(pPivot) ) + { + printf( "Gia_ManDupCof(): Variable %d should be a CI or an AND node.\n", iVar ); + return NULL; + } + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + // compute negative cofactor + Gia_ManForEachCi( p, pObj, i ) + { + pObj->Value = Gia_ManAppendCi(pNew); + if ( pObj == pPivot ) + { + iCofVar = pObj->Value; + pObj->Value = Gia_Var2Lit( 0, 0 ); + } + } + Gia_ManForEachAnd( p, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( pObj == pPivot ) + { + iCofVar = pObj->Value; + pObj->Value = Gia_Var2Lit( 0, 0 ); + } + } + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + // compute the positive cofactor + Gia_ManForEachCi( p, pObj, i ) + { + pObj->Value = Gia_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 ); + if ( pObj == pPivot ) + pObj->Value = Gia_Var2Lit( 0, 1 ); + } + Gia_ManForEachAnd( p, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( pObj == pPivot ) + pObj->Value = Gia_Var2Lit( 0, 1 ); + } + // create MUXes + assert( iCofVar > 0 ); + Gia_ManForEachCo( p, pObj, i ) + { + if ( pObj->Value == (unsigned)Gia_ObjFanin0Copy(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + else + pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashMux(pNew, iCofVar, Gia_ObjFanin0Copy(pObj), pObj->Value) ); + } + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG in the DFS order while putting CIs first.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar ) +{ + Gia_Man_t * pNew, * pTemp; + pNew = Gia_ManDupCofInt( p, iVar ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [Determines variables whose fanout count is higher than this.] + + Description [Variables are returned in a reverse topological order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManCofVars( Gia_Man_t * p, int nFanLim ) +{ + Vec_Int_t * vVars; + Gia_Obj_t * pObj; + int i; + ABC_FREE( p->pRefs ); + Gia_ManCreateRefs( p ); + vVars = Vec_IntAlloc( 100 ); + Gia_ManForEachObj( p, pObj, i ) + if ( Gia_ObjIsCand(pObj) && Gia_ObjRefs(p, pObj) >= nFanLim ) + Vec_IntPush( vVars, i ); + ABC_FREE( p->pRefs ); + return vVars; +} + +/**Function************************************************************* + + Synopsis [Transfers attributes from the original one to the final one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManTransfer( Gia_Man_t * pAig, Gia_Man_t * pCof, Gia_Man_t * pNew, Vec_Int_t * vSigs ) +{ + Vec_Int_t * vSigsNew; + Gia_Obj_t * pObj, * pObjF; + int i; + vSigsNew = Vec_IntAlloc( 100 ); + Gia_ManForEachObjVec( vSigs, pAig, pObj, i ) + { + assert( Gia_ObjIsCand(pObj) ); + pObjF = Gia_ManObj( pCof, Gia_Lit2Var(pObj->Value) ); + if ( pObjF->Value && ~pObjF->Value ) + Vec_IntPushUnique( vSigsNew, Gia_Lit2Var(pObjF->Value) ); + } + return vSigsNew; +} + +/**Function************************************************************* + + Synopsis [Cofactors selected variables (should be in reverse topo order).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose ) +{ + Vec_Int_t * vSigsNew, * vTemp; + Gia_Man_t * pAig, * pCof, * pNew; + int iVar; + if ( fVerbose ) + { + printf( "Cofactoring %d signals.\n", Vec_IntSize(vSigs) ); + Gia_ManPrintStats( p ); + } + if ( Vec_IntSize( vSigs ) > 200 ) + { + printf( "Too many signals to cofactor.\n" ); + return NULL; + } + pAig = Gia_ManDup( p ); + vSigsNew = Vec_IntDup( vSigs ); + while ( Vec_IntSize(vSigsNew) > 0 ) + { + Vec_IntSort( vSigsNew, 0 ); + iVar = Vec_IntPop( vSigsNew ); +// Gia_ManCreateRefs( pAig ); +// printf( "ref count = %d\n", Gia_ObjRefs( pAig, Gia_ManObj(pAig, iVar) ) ); +// ABC_FREE( pAig->pRefs ); + pCof = Gia_ManDupCofInt( pAig, iVar ); + pNew = Gia_ManCleanup( pCof ); + vSigsNew = Gia_ManTransfer( pAig, pCof, pNew, vTemp = vSigsNew ); + Vec_IntFree( vTemp ); + Gia_ManStop( pAig ); + Gia_ManStop( pCof ); + pAig = pNew; + if ( fVerbose ) + printf( "Cofactored variable %d.\n", iVar ); + if ( fVerbose ) + Gia_ManPrintStats( pAig ); + } + Vec_IntFree( vSigsNew ); + return pAig; +} + +/**Function************************************************************* + + Synopsis [Cofactors all variables whose fanout is higher than this.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose ) +{ + Gia_Man_t * pNew; + Vec_Int_t * vSigs = Gia_ManCofVars( p, nFanLim ); + pNew = Gia_ManDupCofAllInt( p, vSigs, fVerbose ); + Vec_IntFree( vSigs ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 1d940b78..5fb801a7 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -62,6 +62,45 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p ) /**Function************************************************************* + Synopsis [Duplicates while adding self-loops to the registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, iCtrl; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + iCtrl = Gia_ManAppendCi( pNew ); + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = Gia_ManHashMux( pNew, iCtrl, Gia_ObjFanin0Copy(pObj), Gia_ObjRiToRo(p, pObj)->Value ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, pObj->Value ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Duplicates AIG without any changes.] Description [] @@ -192,22 +231,22 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes ) SeeAlso [] ***********************************************************************/ -int Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +int Gia_ManDupDfs2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) { if ( ~pObj->Value ) return pObj->Value; if ( p->pReprsOld && ~p->pReprsOld[Gia_ObjId(p, pObj)] ) { Gia_Obj_t * pRepr = Gia_ManObj( p, p->pReprsOld[Gia_ObjId(p, pObj)] ); - pRepr->Value = Gia_ManDupDfs_rec( pNew, p, pRepr ); + pRepr->Value = Gia_ManDupDfs2_rec( pNew, p, pRepr ); return pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); } if ( Gia_ObjIsCi(pObj) ) return pObj->Value = Gia_ManAppendCi(pNew); - Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManDupDfs2_rec( pNew, p, Gia_ObjFanin0(pObj) ); if ( Gia_ObjIsCo(pObj) ) return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin1(pObj) ); + Gia_ManDupDfs2_rec( pNew, p, Gia_ObjFanin1(pObj) ); if ( pNew->pHTable ) return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); @@ -224,7 +263,7 @@ int Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) +Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p ) { Gia_Man_t * pNew; Gia_Obj_t * pObj, * pObjNew; @@ -234,7 +273,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) pNew->pName = Aig_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCo( p, pObj, i ) - Gia_ManDupDfs_rec( pNew, p, pObj ); + Gia_ManDupDfs2_rec( pNew, p, pObj ); Gia_ManForEachCi( p, pObj, i ) if ( ~pObj->Value == 0 ) pObj->Value = Gia_ManAppendCi(pNew); @@ -253,6 +292,57 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) /**Function************************************************************* + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin1(pObj) ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Duplicates AIG in the DFS order while putting CIs first.] Description [] @@ -332,7 +422,7 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits ) pObj->Value = Gia_ManAppendCi(pNew); Vec_IntForEachEntry( vLits, iLit, i ) { - iLitRes = Gia_ManDupDfs_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) ); + iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) ); Gia_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) ); } Gia_ManSetRegNum( pNew, 0 ); @@ -404,95 +494,6 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos ) /**Function************************************************************* - Synopsis [Duplicates AIG in the DFS order while putting CIs first.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManDupCofactored( Gia_Man_t * p, int iVar, int nLimFan ) -{ - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pPivot; - int i, iCofVar = -1; - if ( nLimFan > 0 ) - { - printf( "This feature is not implemented.\n" ); - return NULL; - } - if ( !(iVar > 0 && iVar < Gia_ManObjNum(p)) ) - { - printf( "Gia_ManDupCofactored(): Variable %d is out of range (%d; %d).\n", iVar, 0, Gia_ManObjNum(p) ); - return NULL; - } - // find the cofactoring variable - pPivot = Gia_ManObj( p, iVar ); - if ( !(Gia_ObjIsCi(pPivot) || Gia_ObjIsAnd(pPivot)) ) - { - printf( "Gia_ManDupCofactored(): Variable %d should be a CI or an AND node.\n", iVar ); - return NULL; - } -// assert( Gia_ManRegNum(p) == 0 ); - pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); - Gia_ManHashAlloc( pNew ); - Gia_ManConst0(p)->Value = 0; - // compute negative cofactor - Gia_ManForEachCi( p, pObj, i ) - { - pObj->Value = Gia_ManAppendCi(pNew); - if ( pObj == pPivot ) - { - iCofVar = pObj->Value; - pObj->Value = Gia_Var2Lit( 0, 0 ); - } - } - Gia_ManForEachAnd( p, pObj, i ) - { - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - if ( pObj == pPivot ) - { - iCofVar = pObj->Value; - pObj->Value = Gia_Var2Lit( 0, 0 ); - } - } - Gia_ManForEachCo( p, pObj, i ) - pObj->Value = Gia_ObjFanin0Copy(pObj); - // compute the positive cofactor - Gia_ManForEachCi( p, pObj, i ) - { - pObj->Value = Gia_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 ); - if ( pObj == pPivot ) - pObj->Value = Gia_Var2Lit( 0, 1 ); - } - Gia_ManForEachAnd( p, pObj, i ) - { - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - if ( pObj == pPivot ) - pObj->Value = Gia_Var2Lit( 0, 1 ); - } - // create MUXes - assert( iCofVar > 0 ); - Gia_ManForEachCo( p, pObj, i ) - { - if ( pObj->Value == (unsigned)Gia_ObjFanin0Copy(pObj) ) - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - else - pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashMux(pNew, iCofVar, Gia_ObjFanin0Copy(pObj), pObj->Value) ); - } - Gia_ManHashStop( pNew ); - Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); - // rehash the result - pNew = Gia_ManCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - return pNew; -} - -/**Function************************************************************* - Synopsis [Print representatives.] Description [] @@ -544,7 +545,7 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits int iLit, iLitRes; Vec_IntForEachEntry( vLits, iLit, i ) { - iLitRes = Gia_ManDupDfs_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) ); + iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) ); Gia_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) ); } } diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c index d05dc5a9..f80bc885 100644 --- a/src/aig/gia/giaEnable.c +++ b/src/aig/gia/giaEnable.c @@ -104,7 +104,7 @@ void Gia_ManPrintSignals( Gia_Man_t * p, int * pFreq, char * pStr ) printf( "%s (total = %d driven = %d)\n", pStr, Counter, nTotal ); Counter = 0; for ( i = 0; i < Gia_ManObjNum(p); i++ ) - if ( pFreq[i] > 1 ) + if ( pFreq[i] > 10 ) { printf( "%3d : Obj = %6d Refs = %6d Freq = %6d\n", ++Counter, i, Gia_ObjRefs(p, Gia_ManObj(p,i)), pFreq[i] ); @@ -124,7 +124,7 @@ void Gia_ManPrintSignals( Gia_Man_t * p, int * pFreq, char * pStr ) SeeAlso [] ***********************************************************************/ -void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset ) +void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ) { Vec_Int_t * vSuper; Gia_Obj_t * pFlop, * pObjC, * pObj0, * pObj1, * pNode, * pTemp; @@ -189,20 +189,235 @@ void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset ) } } Vec_IntFree( vSuper ); + ABC_FREE( p->pRefs ); Gia_ManCreateRefs( p ); - printf( "Flops with set/reset = %6d. Flops with enable = %6d.\n", nHaveSetReset, nHaveEnable ); - if ( fSetReset ) + if ( fVerbose ) { - Gia_ManPrintSignals( p, pSets, "Set signals" ); - Gia_ManPrintSignals( p, pResets, "Reset signals" ); + printf( "Flops with set/reset = %6d. Flops with enable = %6d.\n", nHaveSetReset, nHaveEnable ); + if ( fSetReset ) + { + Gia_ManPrintSignals( p, pSets, "Set signals" ); + Gia_ManPrintSignals( p, pResets, "Reset signals" ); + } + Gia_ManPrintSignals( p, pEnables, "Enable signals" ); } - Gia_ManPrintSignals( p, pEnables, "Enable signals" ); ABC_FREE( p->pRefs ); ABC_FREE( pSets ); ABC_FREE( pResets ); ABC_FREE( pEnables ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManDetectSeqSignalsWithFanout( Gia_Man_t * p, int nFanMax, int fVerbose ) +{ + Vec_Int_t * vResult; + Vec_Int_t * vSuper; + Gia_Obj_t * pFlop, * pObjC, * pObj0, * pObj1, * pNode, * pTemp; + int i, k, Ent, * pSets, * pResets, * pEnables; + int nHaveSetReset = 0, nHaveEnable = 0; + assert( Gia_ManRegNum(p) > 0 ); + pSets = ABC_CALLOC( int, Gia_ManObjNum(p) ); + pResets = ABC_CALLOC( int, Gia_ManObjNum(p) ); + pEnables = ABC_CALLOC( int, Gia_ManObjNum(p) ); + vSuper = Vec_IntAlloc( 100 ); + Gia_ManForEachRi( p, pFlop, i ) + { + pNode = Gia_ObjFanin0(pFlop); + if ( !Gia_ObjIsAnd(pNode) ) + continue; + // detect sets/resets + Gia_CollectSuper( p, pNode, vSuper ); + if ( Gia_ObjFaninC0(pFlop) ) + Vec_IntForEachEntry( vSuper, Ent, k ) + pSets[Ent]++; + else + Vec_IntForEachEntry( vSuper, Ent, k ) + pResets[Ent]++; + // detect enables + if ( !Gia_ObjIsMuxType(pNode) ) + continue; + pObjC = Gia_ObjRecognizeMux( pNode, &pObj0, &pObj1 ); + pTemp = Gia_ObjRiToRo( p, pFlop ); + if ( Gia_Regular(pObj0) != pTemp && Gia_Regular(pObj1) != pTemp ) + continue; + if ( !Gia_ObjFaninC0(pFlop) ) + { + pObj0 = Gia_Not(pObj0); + pObj1 = Gia_Not(pObj1); + } + if ( Gia_IsComplement(pObjC) ) + { + pObjC = Gia_Not(pObjC); + pTemp = pObj0; + pObj0 = pObj1; + pObj1 = pTemp; + } + // detect controls +// Gia_CollectSuper( p, pObjC, vSuper ); +// Vec_IntForEachEntry( vSuper, Ent, k ) +// pEnables[Ent]++; + pEnables[Gia_ObjId(p, pObjC)]++; + nHaveEnable++; + } + Gia_ManForEachRi( p, pFlop, i ) + { + pNode = Gia_ObjFanin0(pFlop); + if ( !Gia_ObjIsAnd(pNode) ) + continue; + // detect sets/resets + Gia_CollectSuper( p, pNode, vSuper ); + Vec_IntForEachEntry( vSuper, Ent, k ) + if ( pSets[Ent] > 1 || pResets[Ent] > 1 ) + { + nHaveSetReset++; + break; + } + } + Vec_IntFree( vSuper ); + vResult = Vec_IntAlloc( 100 ); + for ( i = 1; i < Gia_ManObjNum(p); i++ ) + if ( pSets[i] > nFanMax ) + { + if ( fVerbose ) + printf( "Adding set signal %d related to %d flops.\n", i, pSets[i] ); + Vec_IntPushUnique( vResult, i ); + } + for ( i = 1; i < Gia_ManObjNum(p); i++ ) + if ( pResets[i] > nFanMax ) + { + if ( fVerbose ) + printf( "Adding reset signal %d related to %d flops.\n", i, pResets[i] ); + Vec_IntPushUnique( vResult, i ); + } + for ( i = 1; i < Gia_ManObjNum(p); i++ ) + if ( pEnables[i] > nFanMax ) + { + if ( fVerbose ) + printf( "Adding enable signal %d related to %d flops.\n", i, pEnables[i] ); + Vec_IntPushUnique( vResult, i ); + } + ABC_FREE( pSets ); + ABC_FREE( pResets ); + ABC_FREE( pEnables ); + return vResult; +} + + +/**Function************************************************************* + + Synopsis [Transfers attributes from the original one to the final one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManTransferFrames( Gia_Man_t * pAig, Gia_Man_t * pFrames, int nFrames, Gia_Man_t * pNew, Vec_Int_t * vSigs ) +{ + Vec_Int_t * vSigsNew; + Gia_Obj_t * pObj, * pObjF; + int k, f; + vSigsNew = Vec_IntAlloc( 100 ); + Gia_ManForEachObjVec( vSigs, pAig, pObj, k ) + { + assert( Gia_ObjIsCand(pObj) ); + for ( f = 0; f < nFrames; f++ ) + { + pObjF = Gia_ManObj( pFrames, Gia_Lit2Var(Gia_ObjCopyF( pAig, f, pObj )) ); + if ( pObjF->Value && ~pObjF->Value ) + Vec_IntPushUnique( vSigsNew, Gia_Lit2Var(pObjF->Value) ); + } + } + return vSigsNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int f, i; + ABC_FREE( p->pCopies ); + p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) ); + pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachRo( p, pObj, i ) + Gia_ObjSetCopyF( p, 0, pObj, 0 ); + 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_ManForEachAnd( p, pObj, i ) + Gia_ObjSetCopyF( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj)) ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ObjSetCopyF( p, f, pObj, Gia_ObjFanin0CopyF(p, f, pObj) ); + Gia_ManForEachPo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjCopyF(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) ); + } + Gia_ManHashStop( pNew ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Unrolls initialized timeframes while cofactoring some vars.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose ) +{ + Vec_Int_t * vCofSigs, * vTemp; + Gia_Man_t * pAig, * pFrames, * pNew; + // compute initialized timeframes + pFrames = Gia_ManUnrollInit( p, nFrames ); + pAig = Gia_ManCleanup( pFrames ); + // compute and remap set/reset/enable signals + vCofSigs = Gia_ManDetectSeqSignalsWithFanout( p, nFanMax, fVerbose ); + vCofSigs = Gia_ManTransferFrames( p, pFrames, nFrames, pAig, vTemp = vCofSigs ); + Vec_IntFree( vTemp ); + Gia_ManStop( pFrames ); + ABC_FREE( p->pCopies ); + // cofactor all these variables + pNew = Gia_ManDupCofAllInt( pAig, vCofSigs, fVerbose ); + Vec_IntFree( vCofSigs ); + Gia_ManStop( pAig ); + return pNew; + +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index acdd3c13..b87c77e5 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -30,6 +30,57 @@ /**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 = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); + 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 [] @@ -192,18 +243,21 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) SeeAlso [] ***********************************************************************/ -static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll ) +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)) ); } @@ -218,20 +272,20 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int SeeAlso [] ***********************************************************************/ -void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll ) +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 ( ~pObj->Value ) return; assert( Gia_ObjIsAnd(pObj) ); - if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) ) + if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) ) { - Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll ); + Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut ); pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } - Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll ); - Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll ); + 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) ); } @@ -246,12 +300,24 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll ) +Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose ) { Gia_Man_t * pNew; Gia_Obj_t * pObj, * pRepr; int i; + if ( fDualOut && (Gia_ManPoNum(p) & 1) ) + { + printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" ); + return NULL; + } + if ( !Gia_ManCheckTopoOrder( p ) ) + { + printf( "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" ); + return NULL; + } Gia_ManSetPhase( p ); + if ( fDualOut ) + Gia_ManEquivSetColors( p, fVerbose ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); Gia_ManFillValue( p ); @@ -259,12 +325,12 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll ) Gia_ManForEachCi( p, pObj, i ) { pObj->Value = Gia_ManAppendCi(pNew); - if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) ) + if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) ) pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); } Gia_ManHashAlloc( pNew ); Gia_ManForEachCo( p, pObj, i ) - Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll ); + Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut ); Gia_ManForEachCo( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManHashStop( pNew ); @@ -386,6 +452,52 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina /**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, Gia_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, Gia_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.] @@ -398,7 +510,9 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ) { Gia_Man_t * pNew, * pFinal; - pNew = Gia_ManEquivReduce( p, 0 ); + pNew = Gia_ManEquivReduce( p, 0, 0, 0 ); + if ( pNew == NULL ) + return NULL; if ( fMiterPairs ) Gia_ManEquivFixOutputPairs( pNew ); if ( fSeq ) @@ -409,6 +523,8 @@ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs pFinal = Gia_ManDupMarked( pNew ); Gia_ManEquivDeriveReprs( p, pNew, pFinal ); Gia_ManStop( pNew ); + pFinal = Gia_ManEquivRemapDfs( pNew = pFinal ); + Gia_ManStop( pNew ); return pFinal; } @@ -448,25 +564,24 @@ int Gia_ManEquivSetColor_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fOdds ) int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ) { Gia_Obj_t * pObj; - int i, nNodes[2] = {0,0}, nDiffs[2]; + 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_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[0]); - nDiffs[1] = Gia_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[1]); + nDiffs[0] = Gia_ManCandNum(p) - nNodes[0]; + nDiffs[1] = Gia_ManCandNum(p) - nNodes[1]; if ( fVerbose ) { printf( "CI+AND = %7d A = %7d B = %7d Ad = %7d Bd = %7d AB = %7d.\n", - Gia_ManCiNum(p) + Gia_ManAndNum(p), - Gia_ManPiNum(p) + nNodes[0], Gia_ManPiNum(p) + nNodes[1], - nDiffs[0], nDiffs[1], - Gia_ManCiNum(p) + Gia_ManAndNum(p) - nDiffs[0] - nDiffs[1] ); + Gia_ManCandNum(p), nNodes[0], nNodes[1], nDiffs[0], nDiffs[1], + Gia_ManCandNum(p) - nDiffs[0] - nDiffs[1] ); } return (nDiffs[0] + nDiffs[1]) / 2; } @@ -482,13 +597,16 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ -static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits ) +static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut ) { 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 = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); @@ -506,15 +624,15 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t SeeAlso [] ***********************************************************************/ -void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits ) +void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut ) { if ( ~pObj->Value ) return; assert( Gia_ObjIsAnd(pObj) ); - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits ); - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManSpecBuild( pNew, p, pObj, vXorLits ); + Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut ); } /**Function************************************************************* @@ -528,7 +646,7 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ) +Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; @@ -539,9 +657,21 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ) printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" ); return NULL; } + if ( fDualOut && (Gia_ManPoNum(p) & 1) ) + { + printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" ); + return NULL; + } + if ( !Gia_ManCheckTopoOrder( p ) ) + { + printf( "Gia_ManSpecReduce(): AIG is not in a correct topological order.\n" ); + return NULL; + } vXorLits = Vec_IntAlloc( 1000 ); Gia_ManSetPhase( p ); Gia_ManFillValue( p ); + if ( fDualOut ) + Gia_ManEquivSetColors( p, fVerbose ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); @@ -549,9 +679,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ) Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); Gia_ManForEachRo( p, pObj, i ) - Gia_ManSpecBuild( pNew, p, pObj, vXorLits ); + Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut ); Gia_ManForEachCo( p, pObj, i ) - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut ); Vec_IntForEachEntry( vXorLits, iLitNew, i ) Gia_ManAppendCo( pNew, iLitNew ); if ( Vec_IntSize(vXorLits) == 0 ) @@ -570,12 +700,6 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ) } -static inline int Gia_ObjSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)]; } -static inline void Gia_ObjSetSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit; } - -static inline int Gia_ObjChild0Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } -static inline int Gia_ObjChild1Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } - /**Function************************************************************* Synopsis [Duplicates the AIG in the DFS order.] @@ -587,17 +711,20 @@ static inline int Gia_ObjChild1Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f ) +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; - iLitNew = Gia_LitNotCond( Gia_ObjSpec(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); - if ( Gia_ObjSpec(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) - Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjSpec(p, f, pObj), iLitNew) ); - Gia_ObjSetSpec( p, f, pObj, iLitNew ); +// 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 = Gia_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************************************************************* @@ -611,15 +738,15 @@ void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Ve SeeAlso [] ***********************************************************************/ -void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f ) +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_ObjSpec(p, f, pObj) ) + if ( ~Gia_ObjCopyF(p, f, pObj) ) return; assert( Gia_ObjIsAnd(pObj) ); - Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f ); - Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f ); - Gia_ObjSetSpec( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjChild0Spec(p, f, pObj), Gia_ObjChild1Spec(p, f, pObj)) ); - Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f ); + 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************************************************************* @@ -654,31 +781,43 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames printf( "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" ); return NULL; } + if ( fDualOut && (Gia_ManPoNum(p) & 1) ) + { + printf( "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" ); + return NULL; + } + if ( !Gia_ManCheckTopoOrder( p ) ) + { + printf( "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" ); + return NULL; + } assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 ); p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) ); vXorLits = Vec_IntAlloc( 1000 ); Gia_ManSetPhase( p ); + if ( fDualOut ) + Gia_ManEquivSetColors( p, 0 ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManForEachRo( p, pObj, i ) - Gia_ObjSetSpec( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) ); + Gia_ObjSetCopyF( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) ); for ( f = 0; f < nFrames; f++ ) { - Gia_ObjSetSpec( p, f, Gia_ManConst0(p), 0 ); + Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); Gia_ManForEachPi( p, pObj, i ) - Gia_ObjSetSpec( p, f, pObj, Gia_ManAppendCi(pNew) ); + Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); Gia_ManForEachRo( p, pObj, i ) - Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f ); + Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut ); Gia_ManForEachCo( p, pObj, i ) { - Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f ); - Gia_ObjSetSpec( p, f, pObj, Gia_ObjChild0Spec(p, f, pObj) ); + 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_ObjSetSpec( p, f+1, pObjRo, Gia_ObjSpec(p, f, pObjRi) ); + Gia_ObjSetCopyF( p, f+1, pObjRo, Gia_ObjCopyF(p, f, pObjRi) ); } Vec_IntForEachEntry( vXorLits, iLitNew, i ) Gia_ManAppendCo( pNew, iLitNew ); diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 3db3e396..f11345eb 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -92,7 +92,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { /*=== sswAbs.c ==========================================================*/ extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose ); /*=== saigBmc.c ==========================================================*/ -extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame ); +extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ); /*=== saigCone.c ==========================================================*/ extern void Saig_ManPrintCones( Aig_Man_t * p ); diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index 8ba02528..f8799e38 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -173,16 +173,24 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax SeeAlso [] ***********************************************************************/ -int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame ) +int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ) { + extern Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit ); sat_solver * pSat; Cnf_Dat_t * pCnf; Aig_Man_t * pFrames, * pAigTemp; Aig_Obj_t * pObj; int status, clk, Lit, i, RetValue = 1; + // derive the timeframes clk = clock(); - if ( nSizeMax > 0 ) + if ( nCofFanLit ) + { + pFrames = Gia_ManCofactorAig( pAig, nFrames, nCofFanLit ); + if ( pFrames == NULL ) + return -1; + } + else if ( nSizeMax > 0 ) { pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax ); nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0); diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 9d09d4e7..03df38e1 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -146,6 +146,18 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0; for ( nIter = 0; ; nIter++ ) { + if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter ) + { + Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p ); + Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); + Aig_ManStop( pSRed ); + printf( "Iterative refinement is stopped before iteration %d.\n", nIter ); + printf( "The network is reduced using candidate equivalences.\n" ); + printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" ); + printf( "If the miter is SAT, the reduced result is incorrect.\n" ); + break; + } + clk = clock(); p->pMSat = Ssw_SatStart( 0 ); if ( p->pPars->fLatchCorrOpt ) @@ -199,18 +211,6 @@ clk = clock(); Ssw_ManCleanup( p ); if ( !RetValue ) break; - - if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter ) - { - Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p ); - Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); - Aig_ManStop( pSRed ); - printf( "Iterative refinement is stopped after iteration %d.\n", nIter ); - printf( "The network is reduced using candidate equivalences.\n" ); - printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" ); - printf( "If the miter is SAT, the reduced result is incorrect.\n" ); - break; - } } p->pPars->nIters = nIter + 1; p->timeTotal = clock() - clkTotal; diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index b7fe6316..2869352c 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -661,6 +661,7 @@ extern ABC_DLL Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, /*=== abcNames.c ====================================================*/ extern ABC_DLL char * Abc_ObjName( Abc_Obj_t * pNode ); extern ABC_DLL char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix ); +extern ABC_DLL char * Abc_ObjNamePrefix( Abc_Obj_t * pObj, char * pPrefix ); extern ABC_DLL char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix ); extern ABC_DLL char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits ); extern ABC_DLL void Abc_NtkTrasferNames( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c index 19bdc47e..2addf289 100644 --- a/src/base/abc/abcHie.c +++ b/src/base/abc/abcHie.c @@ -40,9 +40,9 @@ SeeAlso [] ***********************************************************************/ -void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int * pCounter ) +void Abc_NtkFlattenLogicHierarchy2_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int * pCounter ) { - char Suffix[1000] = {0}; + char Suffix[2000] = {0}; Abc_Ntk_t * pNtkModel; Abc_Obj_t * pObj, * pTerm, * pNet, * pFanin; int i, k; @@ -70,7 +70,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in (*pCounter)++; - // create the prefix, which will be appended to the internal names + // create the suffix, which will be appended to the internal names if ( *pCounter ) sprintf( Suffix, "_%s_%d", Abc_NtkName(pNtk), *pCounter ); @@ -98,7 +98,18 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in Abc_NtkForEachPi( pNtk, pTerm, i ) Abc_NodeSetTravIdCurrent( pTerm ); Abc_NtkForEachPo( pNtk, pTerm, i ) + { Abc_NodeSetTravIdCurrent( pTerm ); + // if the netlist has net names beginning with "abc_property_" + // these names will be addes as primary outputs of the network + pNet = Abc_ObjFanin0(pTerm); + if ( strncmp( Abc_ObjName(pNet), "abc_property", 12 ) ) + continue; + Abc_ObjAddFanin( Abc_NtkCreatePo(pNet->pCopy->pNtk), pNet->pCopy ); + if ( Nm_ManFindNameById(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id) ) + Nm_ManDeleteIdName(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id); + Abc_ObjAssignName( pNet->pCopy, Abc_ObjName(pNet), Suffix ); + } Abc_NtkForEachBox( pNtk, pObj, i ) { if ( Abc_ObjIsLatch(pObj) ) @@ -144,7 +155,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in Abc_ObjForEachFanout( pObj, pTerm, k ) Abc_ObjFanin0( Abc_NtkPo(pNtkModel, k) )->pCopy = Abc_ObjFanout0(pTerm)->pCopy; // call recursively - Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtkModel, pCounter ); + Abc_NtkFlattenLogicHierarchy2_rec( pNtkNew, pNtkModel, pCounter ); } // if it is a BLIF-MV netlist transfer the values of all nets @@ -168,7 +179,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ) +Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy2( Abc_Ntk_t * pNtk ) { Abc_Ntk_t * pNtkNew; Abc_Obj_t * pTerm, * pNet; @@ -203,7 +214,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ) // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes Counter = -1; - Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtk, &Counter ); + Abc_NtkFlattenLogicHierarchy2_rec( pNtkNew, pNtk, &Counter ); printf( "Hierarchy reader flattened %d instances of logic boxes and left %d black boxes.\n", Counter, Abc_NtkBlackboxNum(pNtkNew) ); @@ -217,6 +228,241 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ) pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy; } + // we may have added property outputs + Abc_NtkOrderCisCos( pNtkNew ); + + // copy the timing information +// Abc_ManTimeDup( pNtk, pNtkNew ); + // duplicate EXDC + if ( pNtk->pExdc ) + printf( "EXDC is not transformed.\n" ); + if ( !Abc_NtkCheck( pNtkNew ) ) + { + fprintf( stdout, "Abc_NtkFlattenLogicHierarchy2(): Network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + + + +/**Function************************************************************* + + Synopsis [Recursively flattens logic hierarchy of the netlist.] + + Description [When this procedure is called, the PI/PO nets of the old + netlist point to the corresponding nets of the flattened netlist.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int * pCounter, Vec_Str_t * vPref ) +{ + Abc_Ntk_t * pNtkModel; + Abc_Obj_t * pObj, * pTerm, * pNet, * pFanin; + int i, k, Length; + + // process the blackbox + if ( Abc_NtkHasBlackbox(pNtk) ) + { + // duplicate the blackbox + assert( Abc_NtkBoxNum(pNtk) == 1 ); + pObj = Abc_NtkBox( pNtk, 0 ); + Abc_NtkDupBox( pNtkNew, pObj, 1 ); + pObj->pCopy->pData = pNtk; + + // connect blackbox fanins to the PI nets + assert( Abc_ObjFaninNum(pObj->pCopy) == Abc_NtkPiNum(pNtk) ); + Abc_NtkForEachPi( pNtk, pTerm, i ) + Abc_ObjAddFanin( Abc_ObjFanin(pObj->pCopy,i), Abc_ObjFanout0(pTerm)->pCopy ); + + // connect blackbox fanouts to the PO nets + assert( Abc_ObjFanoutNum(pObj->pCopy) == Abc_NtkPoNum(pNtk) ); + Abc_NtkForEachPo( pNtk, pTerm, i ) + Abc_ObjAddFanin( Abc_ObjFanin0(pTerm)->pCopy, Abc_ObjFanout(pObj->pCopy,i) ); + return; + } + + (*pCounter)++; + + // create the suffix, which will be appended to the internal names + if ( *pCounter ) + { + char Buffer[20]; + sprintf( Buffer, "(%d)", *pCounter ); + Vec_StrAppend( vPref, Buffer ); + } + Vec_StrPush( vPref, '|' ); + Vec_StrPush( vPref, 0 ); + + // duplicate nets of all boxes, including latches + Abc_NtkForEachBox( pNtk, pObj, i ) + { + Abc_ObjForEachFanin( pObj, pTerm, k ) + { + pNet = Abc_ObjFanin0(pTerm); + if ( pNet->pCopy ) + continue; + pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjNamePrefix(pNet, Vec_StrArray(vPref)) ); + } + Abc_ObjForEachFanout( pObj, pTerm, k ) + { + pNet = Abc_ObjFanout0(pTerm); + if ( pNet->pCopy ) + continue; + pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjNamePrefix(pNet, Vec_StrArray(vPref)) ); + } + } + + // mark objects that will not be used + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkForEachPi( pNtk, pTerm, i ) + Abc_NodeSetTravIdCurrent( pTerm ); + Abc_NtkForEachPo( pNtk, pTerm, i ) + { + Abc_NodeSetTravIdCurrent( pTerm ); + // if the netlist has net names beginning with "abc_property_" + // these names will be addes as primary outputs of the network + pNet = Abc_ObjFanin0(pTerm); + if ( strncmp( Abc_ObjName(pNet), "abc_property", 12 ) ) + continue; + Abc_ObjAddFanin( Abc_NtkCreatePo(pNet->pCopy->pNtk), pNet->pCopy ); + if ( Nm_ManFindNameById(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id) ) + Nm_ManDeleteIdName(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id); + Abc_ObjAssignName( pNet->pCopy, Vec_StrArray(vPref), Abc_ObjName(pNet) ); + } + Abc_NtkForEachBox( pNtk, pObj, i ) + { + if ( Abc_ObjIsLatch(pObj) ) + continue; + Abc_NodeSetTravIdCurrent( pObj ); + Abc_ObjForEachFanin( pObj, pTerm, k ) + Abc_NodeSetTravIdCurrent( pTerm ); + Abc_ObjForEachFanout( pObj, pTerm, k ) + Abc_NodeSetTravIdCurrent( pTerm ); + } + + // duplicate objects that do not have prototypes yet + Abc_NtkForEachObj( pNtk, pObj, i ) + { + if ( Abc_NodeIsTravIdCurrent(pObj) ) + continue; + if ( pObj->pCopy ) + continue; + Abc_NtkDupObj( pNtkNew, pObj, 0 ); + } + + // connect objects + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( !Abc_NodeIsTravIdCurrent(pObj) ) + Abc_ObjForEachFanin( pObj, pFanin, k ) + if ( !Abc_NodeIsTravIdCurrent(pFanin) ) + Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); + + // call recursively + Vec_StrPop( vPref ); + Length = Vec_StrSize( vPref ); + Abc_NtkForEachBox( pNtk, pObj, i ) + { + if ( Abc_ObjIsLatch(pObj) ) + continue; + pNtkModel = pObj->pData; + // check the match between the number of actual and formal parameters + assert( Abc_ObjFaninNum(pObj) == Abc_NtkPiNum(pNtkModel) ); + assert( Abc_ObjFanoutNum(pObj) == Abc_NtkPoNum(pNtkModel) ); + // clean the node copy fields + Abc_NtkCleanCopy( pNtkModel ); + // map PIs/POs + Abc_ObjForEachFanin( pObj, pTerm, k ) + Abc_ObjFanout0( Abc_NtkPi(pNtkModel, k) )->pCopy = Abc_ObjFanin0(pTerm)->pCopy; + Abc_ObjForEachFanout( pObj, pTerm, k ) + Abc_ObjFanin0( Abc_NtkPo(pNtkModel, k) )->pCopy = Abc_ObjFanout0(pTerm)->pCopy; + // create name + Vec_StrShrink( vPref, Length ); + Vec_StrAppend( vPref, Abc_NtkName(pNtkModel) ); + // call recursively + Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtkModel, pCounter, vPref ); + } + + // if it is a BLIF-MV netlist transfer the values of all nets + if ( Abc_NtkHasBlifMv(pNtk) && Abc_NtkMvVar(pNtk) ) + { + if ( Abc_NtkMvVar( pNtkNew ) == NULL ) + Abc_NtkStartMvVars( pNtkNew ); + Abc_NtkForEachNet( pNtk, pObj, i ) + Abc_NtkSetMvVarValues( pObj->pCopy, Abc_ObjMvVarNum(pObj) ); + } +} + +/**Function************************************************************* + + Synopsis [Flattens the logic hierarchy of the netlist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ) +{ + extern Abc_Lib_t * Abc_LibDupBlackboxes( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave ); + Vec_Str_t * vPref; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pTerm, * pNet; + int i, Counter = -1; + + assert( Abc_NtkIsNetlist(pNtk) ); + // start the network + pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); + // duplicate the name and the spec + pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); + pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec); + + // clean the node copy fields + Abc_NtkCleanCopy( pNtk ); + + // duplicate PIs/POs and their nets + Abc_NtkForEachPi( pNtk, pTerm, i ) + { + Abc_NtkDupObj( pNtkNew, pTerm, 0 ); + pNet = Abc_ObjFanout0( pTerm ); + pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) ); + Abc_ObjAddFanin( pNet->pCopy, pTerm->pCopy ); + } + Abc_NtkForEachPo( pNtk, pTerm, i ) + { + Abc_NtkDupObj( pNtkNew, pTerm, 0 ); + pNet = Abc_ObjFanin0( pTerm ); + pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) ); + Abc_ObjAddFanin( pTerm->pCopy, pNet->pCopy ); + } + + // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes + vPref = Vec_StrAlloc( 1000 ); + Vec_StrAppend( vPref, Abc_NtkName(pNtk) ); + Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtk, &Counter, vPref ); + printf( "Hierarchy reader flattened %d instances of logic boxes and left %d black boxes.\n", + Counter, Abc_NtkBlackboxNum(pNtkNew) ); + Vec_StrFree( vPref ); + + if ( pNtk->pDesign ) + { + // pass on the design + assert( Vec_PtrEntry(pNtk->pDesign->vTops, 0) == pNtk ); + pNtkNew->pDesign = Abc_LibDupBlackboxes( pNtk->pDesign, pNtkNew ); + // update the pointers + Abc_NtkForEachBlackbox( pNtkNew, pTerm, i ) + pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy; + } + + // we may have added property outputs + Abc_NtkOrderCisCos( pNtkNew ); + // copy the timing information // Abc_ManTimeDup( pNtk, pNtkNew ); // duplicate EXDC @@ -231,6 +477,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ) return pNtkNew; } + /**Function************************************************************* Synopsis [Extracts blackboxes by making them into additional PIs/POs.] diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c index 90fcd191..e07b47c1 100644 --- a/src/base/abc/abcNames.c +++ b/src/base/abc/abcNames.c @@ -70,9 +70,27 @@ char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix ) /**Function************************************************************* - Synopsis [Gets the long name of the node.] + Synopsis [Appends name to the prefix] - Description [This name is the output net's name.] + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_ObjNamePrefix( Abc_Obj_t * pObj, char * pPrefix ) +{ + static char Buffer[2000]; + sprintf( Buffer, "%s%s", pPrefix, Abc_ObjName(pObj) ); + return Buffer; +} + +/**Function************************************************************* + + Synopsis [Appends suffic to the name.] + + Description [] SideEffects [] @@ -81,7 +99,7 @@ char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix ) ***********************************************************************/ char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix ) { - static char Buffer[500]; + static char Buffer[2000]; sprintf( Buffer, "%s%s", Abc_ObjName(pObj), pSuffix ); return Buffer; } @@ -99,7 +117,7 @@ char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix ) ***********************************************************************/ char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits ) { - static char Buffer[100]; + static char Buffer[2000]; sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num ); return Buffer; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3045eb93..b5e23856 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17580,9 +17580,10 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) int nNodeDelta; int fRewrite; int fNewAlgo; + int nCofFanLit; int fVerbose; - extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose ); + extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -17596,9 +17597,10 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) nNodeDelta = 1000; fRewrite = 0; fNewAlgo = 1; + nCofFanLit = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDrvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDLrvh" ) ) != EOF ) { switch ( c ) { @@ -17657,6 +17659,17 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nNodeDelta < 0 ) goto usage; break; + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + nCofFanLit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCofFanLit < 0 ) + goto usage; + break; case 'r': fRewrite ^= 1; break; @@ -17687,19 +17700,20 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Does not work for combinational networks.\n" ); return 0; } - Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fVerbose ); + Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, nCofFanLit, fVerbose ); pAbc->pCex = pNtk->pSeqModel; // temporary ??? return 0; usage: // fprintf( pErr, "usage: bmc [-FNCGD num] [-ravh]\n" ); - fprintf( pErr, "usage: bmc [-FNC num] [-rvh]\n" ); + fprintf( pErr, "usage: bmc [-FNCL num] [-rcvh]\n" ); fprintf( pErr, "\t performs bounded model checking with static unrolling\n" ); fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames ); fprintf( pErr, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); // fprintf( pErr, "\t-G num : the max number of conflicts globally [default = %d]\n", nBTLimitAll ); // fprintf( pErr, "\t-D num : the delta in the number of nodes [default = %d]\n", nNodeDelta ); + fprintf( pErr, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit? "yes": "no" ); fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); // fprintf( pErr, "\t-a : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); @@ -17732,7 +17746,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) int fNewAlgo; int fVerbose; - extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose ); + extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -17837,7 +17851,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Does not work for combinational networks.\n" ); return 0; } - Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fVerbose ); + Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, 0, fVerbose ); pAbc->pCex = pNtk->pSeqModel; // temporary ??? return 0; @@ -22007,7 +22021,7 @@ usage: int Abc_CommandAbc9PSig( Abc_Frame_t * pAbc, int argc, char ** argv ) { int c; - int fSetReset = 0; + int fSetReset = 1; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF ) { @@ -22032,7 +22046,7 @@ int Abc_CommandAbc9PSig( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9PSigs(): Works only for sequential circuits.\n" ); return 1; } - Gia_ManDetectSeqSignals( pAbc->pAig, fSetReset ); + Gia_ManDetectSeqSignals( pAbc->pAig, fSetReset, 1 ); return 0; usage: @@ -22233,9 +22247,10 @@ usage: int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp; - int c, iVar = 0, nLimFan = 0; + int c, fVerbose = 0; + int iVar = 0, nLimFan = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "VLh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "VLvh" ) ) != EOF ) { switch ( c ) { @@ -22255,12 +22270,15 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv ) { fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" ); goto usage; - } + } nLimFan = atoi(argv[globalUtilOptind]); globalUtilOptind++; if ( nLimFan < 0 ) goto usage; break; + case 'v': + fVerbose ^= 1; + break; case 'h': goto usage; default: @@ -22272,7 +22290,21 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9Cof(): There is no AIG.\n" ); return 1; } - pAbc->pAig = Gia_ManDupCofactored( pTemp = pAbc->pAig, iVar, nLimFan ); + if ( nLimFan ) + { + printf( "Cofactoring all variables whose fanout count is higher than %d.\n", nLimFan ); + pAbc->pAig = Gia_ManDupCofAll( pTemp = pAbc->pAig, nLimFan, fVerbose ); + } + else if ( iVar ) + { + printf( "Cofactoring one variable with object ID %d.\n", iVar ); + pAbc->pAig = Gia_ManDupCof( pTemp = pAbc->pAig, iVar ); + } + else + { + printf( "One of the paramters, -V <num> or -L <num>, should be set on the command line.\n" ); + goto usage; + } if ( pAbc->pAig == NULL ) { pAbc->pAig = pTemp; @@ -22283,10 +22315,11 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &cof [-VL num] [-h]\n" ); - fprintf( stdout, "\t performs cofactoring w.r.t. a variable\n" ); - fprintf( stdout, "\t-V num : the zero-based ID of the variable to cofactor [default = %d]\n", iVar ); - fprintf( stdout, "\t-L num : cofactor w.r.t. variables whose fanout is higher [default = %d]\n", nLimFan ); + fprintf( stdout, "usage: &cof [-VL num] [-vh]\n" ); + fprintf( stdout, "\t performs cofactoring w.r.t. variable(s)\n" ); + fprintf( stdout, "\t-V num : the zero-based ID of one variable to cofactor [default = %d]\n", iVar ); + fprintf( stdout, "\t-L num : cofactor vars with fanout count higher than this [default = %d]\n", nLimFan ); + fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; } @@ -22825,9 +22858,10 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_Man_t * pTemp; Gia_ParFra_t Pars, * pPars = &Pars; int c; + int nCofFanLit = 0; Gia_ManFraSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FLivh" ) ) != EOF ) { switch ( c ) { @@ -22842,6 +22876,17 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nFrames < 0 ) goto usage; break; + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + nCofFanLit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCofFanLit < 0 ) + goto usage; + break; case 'i': pPars->fInit ^= 1; break; @@ -22859,14 +22904,18 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9Times(): There is no AIG.\n" ); return 1; } - pAbc->pAig = Gia_ManFrames( pTemp = pAbc->pAig, pPars ); + if ( nCofFanLit ) + pAbc->pAig = Gia_ManUnrollAndCofactor( pTemp = pAbc->pAig, pPars->nFrames, nCofFanLit, pPars->fVerbose ); + else + pAbc->pAig = Gia_ManFrames( pTemp = pAbc->pAig, pPars ); Gia_ManStop( pTemp ); return 0; usage: - fprintf( stdout, "usage: &frames [-F <num>] [-ivh]\n" ); + fprintf( stdout, "usage: &frames [-FL <num>] [-ivh]\n" ); fprintf( stdout, "\t unrolls the design for several timeframes\n" ); fprintf( stdout, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames ); + fprintf( stdout, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit? "yes": "no" ); fprintf( stdout, "\t-i : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); @@ -22929,7 +22978,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv ) } pAbc->pAig = Gia_ManTransformMiter( pAux = pAbc->pAig ); Gia_ManStop( pAux ); - printf( "Abc_CommandAbc9Miter(): Miter is transformed by merging POs pair-wise.\n" ); + printf( "The miter (current AIG) is transformed by XORing POs pair-wise.\n" ); return 0; } @@ -23286,7 +23335,7 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) { - char * pFileName = "gia_srm.aig"; + char * pFileName = "gsrm.aig"; Gia_Man_t * pTemp; int c, fVerbose = 0; int fDualOut = 0; @@ -23314,11 +23363,14 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) } // pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig, fDualOut ); // Gia_ManStop( pTemp ); - pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut ); - Gia_WriteAiger( pTemp, "gia_srm.aig", 0, 0 ); - printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName ); - Gia_ManPrintStatsShort( pTemp ); - Gia_ManStop( pTemp ); + pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut, fVerbose ); + if ( pTemp ) + { + Gia_WriteAiger( pTemp, pFileName, 0, 0 ); + printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName ); + Gia_ManPrintStatsShort( pTemp ); + Gia_ManStop( pTemp ); + } return 0; usage: @@ -23346,14 +23398,18 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_Man_t * pTemp; int c, fVerbose = 0; int fUseAll = 0; + int fDualOut = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "avh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "advh" ) ) != EOF ) { switch ( c ) { case 'a': fUseAll ^= 1; break; + case 'd': + fDualOut ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -23368,14 +23424,18 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9Reduce(): There is no AIG.\n" ); return 1; } - pAbc->pAig = Gia_ManEquivReduce( pTemp = pAbc->pAig, fUseAll ); - Gia_ManStop( pTemp ); + pAbc->pAig = Gia_ManEquivReduce( pTemp = pAbc->pAig, fUseAll, fDualOut, fVerbose ); + if ( pAbc->pAig == NULL ) + pAbc->pAig = pTemp; + else + Gia_ManStop( pTemp ); return 0; usage: - fprintf( stdout, "usage: &reduce [-avh]\n" ); + fprintf( stdout, "usage: &reduce [-advh]\n" ); fprintf( stdout, "\t reduces the circuit using equivalence classes\n" ); - fprintf( stdout, "\t-a : toggle creating dual output miter [default = %s]\n", fUseAll? "yes": "no" ); + fprintf( stdout, "\t-a : toggle merging all equivalences [default = %s]\n", fUseAll? "yes": "no" ); + fprintf( stdout, "\t-d : toggle using dual-output merging [default = %s]\n", fDualOut? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; @@ -23922,6 +23982,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_ManTestDistance( pAbc->pAig ); // Gia_SatSolveTest( pAbc->pAig ); // For_ManExperiment( pAbc->pAig, 20, 1, 1 ); +// Gia_ManUnrollSpecial( pAbc->pAig, 5, 100, 1 ); + pAbc->pAig = Gia_ManDupSelf( pTemp = pAbc->pAig ); + Gia_ManStop( pTemp ); return 0; usage: diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index ca33667f..91046340 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1538,7 +1538,7 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose ) +int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose ) { Aig_Man_t * pMan; int status, RetValue = -1, clk = clock(); @@ -1554,7 +1554,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, if ( fNewAlgo ) { int iFrame; - RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame ); + RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit ); ABC_FREE( pNtk->pModel ); ABC_FREE( pNtk->pSeqModel ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; @@ -1751,7 +1751,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) } if ( pSecPar->fTryBmc ) { - RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, -1, 2000, -1, 0, 1, 0 ); + RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, -1, 2000, -1, 0, 1, 0, 0 ); if ( RetValue == 0 ) { printf( "Networks are not equivalent.\n" ); diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c index dcabaf36..7761d428 100644 --- a/src/base/main/mainMC.c +++ b/src/base/main/mainMC.c @@ -91,7 +91,7 @@ int main( int argc, char * argv[] ) { // perform BMC if ( pAig->nRegs != 0 ) - RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL ); + RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL, 0 ); // perform full-blown SEC if ( RetValue != 0 ) @@ -120,7 +120,7 @@ int main( int argc, char * argv[] ) int nSizeMax = 500000; int nBTLimit = 10000000; int fRewrite = 0; - RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth ); + RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth, 0 ); if ( RetValue != 0 ) RetValue = -1; } |