Skip to content

A
abc
Commit 81b51657 by Alan Mishchenko
Options

Version abc90313

parent 243cb29e
Showing with 1196 additions and 229 deletions
src/aig/cec/cecCec.c
...@@ -129,6 +129,7 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars ) ...@@ -129,6 +129,7 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
double clkTotal = clock(); double clkTotal = clock();
// sweep for equivalences // sweep for equivalences
Cec_ManFraSetDefaultParams( pParsFra ); Cec_ManFraSetDefaultParams( pParsFra );
pParsFra->nItersMax = 1000;
pParsFra->nBTLimit = pPars->nBTLimit; pParsFra->nBTLimit = pPars->nBTLimit;
pParsFra->TimeLimit = pPars->TimeLimit; pParsFra->TimeLimit = pPars->TimeLimit;
pParsFra->fVerbose = pPars->fVerbose; pParsFra->fVerbose = pPars->fVerbose;
......
src/aig/cec/cecClass.c
...@@ -242,6 +242,7 @@ void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass ) ...@@ -242,6 +242,7 @@ void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
} }
else else
{ {
assert( Repr < Ent );
Gia_ObjSetRepr( p, Ent, Repr ); Gia_ObjSetRepr( p, Ent, Repr );
Gia_ObjSetNext( p, EntPrev, Ent ); Gia_ObjSetNext( p, EntPrev, Ent );
EntPrev = Ent; EntPrev = Ent;
...@@ -500,7 +501,7 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat ) ...@@ -500,7 +501,7 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
***********************************************************************/ ***********************************************************************/
void Cec_ManSimFindBestPattern( Cec_ManSim_t * p ) void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
{ {
unsigned * pInfo; unsigned * pInfo;
int i, ScoreBest = 0, iPatBest = 1; int i, ScoreBest = 0, iPatBest = 1;
// find the best pattern // find the best pattern
...@@ -838,7 +839,7 @@ int Cec_ManSimClassesRefine( Cec_ManSim_t * p ) ...@@ -838,7 +839,7 @@ int Cec_ManSimClassesRefine( Cec_ManSim_t * p )
p->nWords = p->pPars->nWords; p->nWords = p->pPars->nWords;
for ( i = 0; i < p->pPars->nRounds; i++ ) 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) ); Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo ); Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
......
src/aig/cec/cecCore.c
...@@ -90,10 +90,10 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p ) ...@@ -90,10 +90,10 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p ) void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p )
{ {
memset( p, 0, sizeof(Cec_ParSmf_t) ); memset( p, 0, sizeof(Cec_ParSmf_t) );
p->nWords = 15; // the number of simulation words p->nWords = 31; // the number of simulation words
p->nRounds = 15; // the number of simulation rounds p->nRounds = 1; // the number of simulation rounds
p->nFrames = 2; // the number of time frames 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->TimeLimit = 0; // the runtime limit in seconds
p->fDualOut = 0; // miter with separate outputs p->fDualOut = 0; // miter with separate outputs
p->fCheckMiter = 0; // the circuit is the miter p->fCheckMiter = 0; // the circuit is the miter
...@@ -118,8 +118,8 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ) ...@@ -118,8 +118,8 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
p->nWords = 15; // the number of simulation words p->nWords = 15; // the number of simulation words
p->nRounds = 15; // the number of simulation rounds p->nRounds = 15; // the number of simulation rounds
p->TimeLimit = 0; // the runtime limit in seconds p->TimeLimit = 0; // the runtime limit in seconds
p->nItersMax = 1000; // the maximum number of iterations of SAT sweeping p->nItersMax = 10; // the maximum number of iterations of SAT sweeping
p->nBTLimit = 1000; // conflict limit at a node p->nBTLimit = 100; // conflict limit at a node
p->nLevelMax = 0; // restriction on the level of nodes to be swept 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->nDepthMax = 1; // the depth in terms of steps of speculative reduction
p->fRewriting = 0; // enables AIG rewriting p->fRewriting = 0; // enables AIG rewriting
...@@ -322,6 +322,8 @@ p->timeSat += clock() - clk; ...@@ -322,6 +322,8 @@ p->timeSat += clock() - clk;
// update the manager // update the manager
pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut ); pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut );
Gia_ManStop( pTemp ); Gia_ManStop( pTemp );
if ( p->pAig == NULL )
break;
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
{ {
printf( "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ", printf( "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ",
...@@ -381,7 +383,7 @@ finalize: ...@@ -381,7 +383,7 @@ finalize:
} }
pTemp = p->pAig; p->pAig = NULL; 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 ); printf( "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut );
else if ( pSim->pCexes ) else if ( pSim->pCexes )
printf( "Disproved %d outputs of the miter.\n", pSim->nOuts ); printf( "Disproved %d outputs of the miter.\n", pSim->nOuts );
......
src/aig/cec/cecSeq.c
...@@ -255,7 +255,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) ...@@ -255,7 +255,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
Gia_Man_t * pSrm; Gia_Man_t * pSrm;
int r, nPats, RetValue = -1; int r, nPats, RetValue = -1;
if ( pAig->pReprs == NULL ) if ( pAig->pReprs == NULL )
{ {
printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" ); printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
return -1; return -1;
} }
......
src/aig/cec/cecSolve.c
...@@ -703,7 +703,8 @@ void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pP ...@@ -703,7 +703,8 @@ void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pP
} }
p->timeTotal = clock() - clk; p->timeTotal = clock() - clk;
Bar_ProgressStop( pProgress ); Bar_ProgressStop( pProgress );
// Cec_ManSatPrintStats( p ); if ( pPars->fVerbose )
Cec_ManSatPrintStats( p );
Cec_ManSatStop( p ); Cec_ManSatStop( p );
if ( pnPats ) if ( pnPats )
*pnPats = iPat-1; *pnPats = iPat-1;
......
src/aig/gia/gia.h
...@@ -67,6 +67,11 @@ struct Gia_Obj_t_ ...@@ -67,6 +67,11 @@ struct Gia_Obj_t_
unsigned Value; // application-specific value 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 // sequential counter-example
typedef struct Gia_Cex_t_ Gia_Cex_t; typedef struct Gia_Cex_t_ Gia_Cex_t;
...@@ -177,6 +182,7 @@ static inline int Gia_ManPoNum( Gia_Man_t * p ) { return Vec_IntS ...@@ -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_ManRegNum( Gia_Man_t * p ) { return p->nRegs; }
static inline int Gia_ManObjNum( Gia_Man_t * p ) { return p->nObjs; } 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_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_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)); } 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 ) { ...@@ -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_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_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_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_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; } 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 ...@@ -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_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_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 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_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) ); } 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 ...@@ -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++ ) for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
#define Gia_ManForEachObjVecLit( vVec, p, pObj, fCompl, 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++ ) 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 ) \ #define Gia_ManForEachAnd( p, pObj, i ) \
for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else
#define Gia_ManForEachCi( p, pObj, i ) \ #define Gia_ManForEachCi( p, pObj, i ) \
...@@ -429,6 +444,9 @@ extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ); ...@@ -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 ); extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
/*=== giaCof.c ============================================================*/ /*=== giaCof.c ============================================================*/
extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ); 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 ============================================================*/ /*=== giaDfs.c ============================================================*/
extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp ); 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 ); 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 ...@@ -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 ); extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
/*=== giaDup.c ============================================================*/ /*=== giaDup.c ============================================================*/
extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); 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_ManDupMarked( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes ); extern Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes );
extern Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ); 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 ); ...@@ -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_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
extern Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p ); 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_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_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_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose ); 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_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 ); extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
/*=== giaEnable.c ==========================================================*/ /*=== 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 ==========================================================*/ /*=== giaEquiv.c ==========================================================*/
extern int Gia_ManCheckTopoOrder( Gia_Man_t * p );
extern int * Gia_ManDeriveNexts( 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_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ); 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 Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); 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 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 ); extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
/*=== giaFanout.c =========================================================*/ /*=== giaFanout.c =========================================================*/
......
src/aig/gia/giaAig.c
...@@ -205,6 +205,29 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p ) ...@@ -205,6 +205,29 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p )
return pNew; 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 /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/gia/giaAiger.c
...@@ -230,6 +230,7 @@ Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize ) ...@@ -230,6 +230,7 @@ Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize )
iNode += Item; iNode += Item;
pReprs[iNode].fProved = fProved; pReprs[iNode].fProved = fProved;
pReprs[iNode].iRepr = iRepr; pReprs[iNode].iRepr = iRepr;
assert( iRepr < iNode );
//printf( "Node = %d ", iNode ); //printf( "Node = %d ", iNode );
} }
return pReprs; return pReprs;
......
src/aig/gia/giaCof.c
...@@ -685,6 +685,232 @@ ABC_PRT( "Time", clock() - clk ); ...@@ -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 /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/gia/giaDup.c
...@@ -62,6 +62,45 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p ) ...@@ -62,6 +62,45 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
/**Function************************************************************* /**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.] Synopsis [Duplicates AIG without any changes.]
Description [] Description []
...@@ -192,22 +231,22 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes ) ...@@ -192,22 +231,22 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
SeeAlso [] 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 ) if ( ~pObj->Value )
return pObj->Value; return pObj->Value;
if ( p->pReprsOld && ~p->pReprsOld[Gia_ObjId(p, pObj)] ) if ( p->pReprsOld && ~p->pReprsOld[Gia_ObjId(p, pObj)] )
{ {
Gia_Obj_t * pRepr = Gia_ManObj( p, 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) ); return pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
} }
if ( Gia_ObjIsCi(pObj) ) if ( Gia_ObjIsCi(pObj) )
return pObj->Value = Gia_ManAppendCi(pNew); 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) ) if ( Gia_ObjIsCo(pObj) )
return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(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 ) if ( pNew->pHTable )
return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
return pObj->Value = Gia_ManAppendAnd( 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 ) ...@@ -224,7 +263,7 @@ int Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p )
{ {
Gia_Man_t * pNew; Gia_Man_t * pNew;
Gia_Obj_t * pObj, * pObjNew; Gia_Obj_t * pObj, * pObjNew;
...@@ -234,7 +273,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) ...@@ -234,7 +273,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
pNew->pName = Aig_UtilStrsav( p->pName ); pNew->pName = Aig_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0; Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCo( p, pObj, i ) Gia_ManForEachCo( p, pObj, i )
Gia_ManDupDfs_rec( pNew, p, pObj ); Gia_ManDupDfs2_rec( pNew, p, pObj );
Gia_ManForEachCi( p, pObj, i ) Gia_ManForEachCi( p, pObj, i )
if ( ~pObj->Value == 0 ) if ( ~pObj->Value == 0 )
pObj->Value = Gia_ManAppendCi(pNew); pObj->Value = Gia_ManAppendCi(pNew);
...@@ -253,6 +292,57 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) ...@@ -253,6 +292,57 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
/**Function************************************************************* /**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.] Synopsis [Duplicates AIG in the DFS order while putting CIs first.]
Description [] Description []
...@@ -332,7 +422,7 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits ) ...@@ -332,7 +422,7 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
pObj->Value = Gia_ManAppendCi(pNew); pObj->Value = Gia_ManAppendCi(pNew);
Vec_IntForEachEntry( vLits, iLit, i ) 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_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) );
} }
Gia_ManSetRegNum( pNew, 0 ); Gia_ManSetRegNum( pNew, 0 );
...@@ -404,95 +494,6 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos ) ...@@ -404,95 +494,6 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos )
/**Function************************************************************* /**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.] Synopsis [Print representatives.]
Description [] Description []
...@@ -544,7 +545,7 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits ...@@ -544,7 +545,7 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
int iLit, iLitRes; int iLit, iLitRes;
Vec_IntForEachEntry( vLits, iLit, i ) 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_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) );
} }
} }
......
src/aig/gia/giaEnable.c
...@@ -104,7 +104,7 @@ void Gia_ManPrintSignals( Gia_Man_t * p, int * pFreq, char * pStr ) ...@@ -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 ); printf( "%s (total = %d driven = %d)\n", pStr, Counter, nTotal );
Counter = 0; Counter = 0;
for ( i = 0; i < Gia_ManObjNum(p); i++ ) 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", printf( "%3d : Obj = %6d Refs = %6d Freq = %6d\n",
++Counter, i, Gia_ObjRefs(p, Gia_ManObj(p,i)), pFreq[i] ); ++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 ) ...@@ -124,7 +124,7 @@ void Gia_ManPrintSignals( Gia_Man_t * p, int * pFreq, char * pStr )
SeeAlso [] 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; Vec_Int_t * vSuper;
Gia_Obj_t * pFlop, * pObjC, * pObj0, * pObj1, * pNode, * pTemp; Gia_Obj_t * pFlop, * pObjC, * pObj0, * pObj1, * pNode, * pTemp;
...@@ -189,20 +189,235 @@ void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset ) ...@@ -189,20 +189,235 @@ void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset )
} }
} }
Vec_IntFree( vSuper ); Vec_IntFree( vSuper );
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p ); Gia_ManCreateRefs( p );
printf( "Flops with set/reset = %6d. Flops with enable = %6d.\n", nHaveSetReset, nHaveEnable ); if ( fVerbose )
if ( fSetReset )
{ {
Gia_ManPrintSignals( p, pSets, "Set signals" ); printf( "Flops with set/reset = %6d. Flops with enable = %6d.\n", nHaveSetReset, nHaveEnable );
Gia_ManPrintSignals( p, pResets, "Reset signals" ); 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( p->pRefs );
ABC_FREE( pSets ); ABC_FREE( pSets );
ABC_FREE( pResets ); ABC_FREE( pResets );
ABC_FREE( pEnables ); 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 /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/gia/giaEquiv.c
...@@ -30,6 +30,57 @@ ...@@ -30,6 +30,57 @@
/**Function************************************************************* /**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.] Synopsis [Given representatives, derives pointers to the next objects.]
Description [] Description []
...@@ -192,18 +243,21 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) ...@@ -192,18 +243,21 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
SeeAlso [] 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 ( fUseAll )
{ {
if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID ) if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID )
return NULL; return NULL;
} }
else else
{ {
if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
return NULL; 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)) ); 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 ...@@ -218,20 +272,20 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int
SeeAlso [] 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; Gia_Obj_t * pRepr;
if ( ~pObj->Value ) if ( ~pObj->Value )
return; return;
assert( Gia_ObjIsAnd(pObj) ); 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) ); pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
return; return;
} }
Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll ); Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll ); Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll, fDualOut );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); 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, ...@@ -246,12 +300,24 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
SeeAlso [] 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_Man_t * pNew;
Gia_Obj_t * pObj, * pRepr; Gia_Obj_t * pObj, * pRepr;
int i; 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 ); Gia_ManSetPhase( p );
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName ); pNew->pName = Aig_UtilStrsav( p->pName );
Gia_ManFillValue( p ); Gia_ManFillValue( p );
...@@ -259,12 +325,12 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll ) ...@@ -259,12 +325,12 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll )
Gia_ManForEachCi( p, pObj, i ) Gia_ManForEachCi( p, pObj, i )
{ {
pObj->Value = Gia_ManAppendCi(pNew); 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) ); pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
} }
Gia_ManHashAlloc( pNew ); Gia_ManHashAlloc( pNew );
Gia_ManForEachCo( p, pObj, i ) 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_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManHashStop( pNew ); Gia_ManHashStop( pNew );
...@@ -386,6 +452,52 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina ...@@ -386,6 +452,52 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina
/**Function************************************************************* /**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.] Synopsis [Reduces AIG while remapping equivalence classes.]
Description [Drops the pairs of outputs if they are proved equivalent.] 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 ...@@ -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 * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs )
{ {
Gia_Man_t * pNew, * pFinal; Gia_Man_t * pNew, * pFinal;
pNew = Gia_ManEquivReduce( p, 0 ); pNew = Gia_ManEquivReduce( p, 0, 0, 0 );
if ( pNew == NULL )
return NULL;
if ( fMiterPairs ) if ( fMiterPairs )
Gia_ManEquivFixOutputPairs( pNew ); Gia_ManEquivFixOutputPairs( pNew );
if ( fSeq ) if ( fSeq )
...@@ -409,6 +523,8 @@ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ...@@ -409,6 +523,8 @@ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs
pFinal = Gia_ManDupMarked( pNew ); pFinal = Gia_ManDupMarked( pNew );
Gia_ManEquivDeriveReprs( p, pNew, pFinal ); Gia_ManEquivDeriveReprs( p, pNew, pFinal );
Gia_ManStop( pNew ); Gia_ManStop( pNew );
pFinal = Gia_ManEquivRemapDfs( pNew = pFinal );
Gia_ManStop( pNew );
return pFinal; return pFinal;
} }
...@@ -448,25 +564,24 @@ int Gia_ManEquivSetColor_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fOdds ) ...@@ -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 ) int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
{ {
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i, nNodes[2] = {0,0}, nDiffs[2]; int i, nNodes[2], nDiffs[2];
assert( (Gia_ManPoNum(p) & 1) == 0 ); assert( (Gia_ManPoNum(p) & 1) == 0 );
Gia_ObjSetColors( p, 0 ); Gia_ObjSetColors( p, 0 );
Gia_ManForEachPi( p, pObj, i ) Gia_ManForEachPi( p, pObj, i )
Gia_ObjSetColors( p, Gia_ObjId(p,pObj) ); Gia_ObjSetColors( p, Gia_ObjId(p,pObj) );
nNodes[0] = nNodes[1] = Gia_ManPiNum(p);
Gia_ManForEachPo( p, pObj, i ) Gia_ManForEachPo( p, pObj, i )
nNodes[i&1] += Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), i&1 ); nNodes[i&1] += Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), i&1 );
// Gia_ManForEachObj( p, pObj, i ) // Gia_ManForEachObj( p, pObj, i )
// if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ) // if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) )
// assert( Gia_ObjColors(p, i) ); // assert( Gia_ObjColors(p, i) );
nDiffs[0] = Gia_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[0]); nDiffs[0] = Gia_ManCandNum(p) - nNodes[0];
nDiffs[1] = Gia_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[1]); nDiffs[1] = Gia_ManCandNum(p) - nNodes[1];
if ( fVerbose ) if ( fVerbose )
{ {
printf( "CI+AND = %7d A = %7d B = %7d Ad = %7d Bd = %7d AB = %7d.\n", printf( "CI+AND = %7d A = %7d B = %7d Ad = %7d Bd = %7d AB = %7d.\n",
Gia_ManCiNum(p) + Gia_ManAndNum(p), Gia_ManCandNum(p), nNodes[0], nNodes[1], nDiffs[0], nDiffs[1],
Gia_ManPiNum(p) + nNodes[0], Gia_ManPiNum(p) + nNodes[1], Gia_ManCandNum(p) - nDiffs[0] - nDiffs[1] );
nDiffs[0], nDiffs[1],
Gia_ManCiNum(p) + Gia_ManAndNum(p) - nDiffs[0] - nDiffs[1] );
} }
return (nDiffs[0] + nDiffs[1]) / 2; return (nDiffs[0] + nDiffs[1]) / 2;
} }
...@@ -482,13 +597,16 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ) ...@@ -482,13 +597,16 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
SeeAlso [] 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; Gia_Obj_t * pRepr;
unsigned iLitNew; unsigned iLitNew;
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL ) if ( pRepr == NULL )
return; 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) ); iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); 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 ...@@ -506,15 +624,15 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
SeeAlso [] 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 ) if ( ~pObj->Value )
return; return;
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits ); Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits ); Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); 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************************************************************* /**Function*************************************************************
...@@ -528,7 +646,7 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V ...@@ -528,7 +646,7 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V
SeeAlso [] 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_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
...@@ -539,9 +657,21 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ) ...@@ -539,9 +657,21 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" ); printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
return NULL; 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 ); vXorLits = Vec_IntAlloc( 1000 );
Gia_ManSetPhase( p ); Gia_ManSetPhase( p );
Gia_ManFillValue( p ); Gia_ManFillValue( p );
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName ); pNew->pName = Aig_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew ); Gia_ManHashAlloc( pNew );
...@@ -549,9 +679,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ) ...@@ -549,9 +679,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
Gia_ManForEachCi( p, pObj, i ) Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew); pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachRo( p, pObj, i ) Gia_ManForEachRo( p, pObj, i )
Gia_ManSpecBuild( pNew, p, pObj, vXorLits ); Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut );
Gia_ManForEachCo( p, pObj, i ) 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 ) Vec_IntForEachEntry( vXorLits, iLitNew, i )
Gia_ManAppendCo( pNew, iLitNew ); Gia_ManAppendCo( pNew, iLitNew );
if ( Vec_IntSize(vXorLits) == 0 ) if ( Vec_IntSize(vXorLits) == 0 )
...@@ -570,12 +700,6 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut ) ...@@ -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************************************************************* /**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.] 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 ) ...@@ -587,17 +711,20 @@ static inline int Gia_ObjChild1Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj )
SeeAlso [] 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; Gia_Obj_t * pRepr;
int iLitNew; int iLitNew;
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL ) if ( pRepr == NULL )
return; return;
iLitNew = Gia_LitNotCond( Gia_ObjSpec(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
if ( Gia_ObjSpec(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjSpec(p, f, pObj), iLitNew) ); return;
Gia_ObjSetSpec( p, f, pObj, iLitNew ); 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************************************************************* /**Function*************************************************************
...@@ -611,15 +738,15 @@ void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Ve ...@@ -611,15 +738,15 @@ void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Ve
SeeAlso [] 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; return;
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f ); Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f ); Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f, fDualOut );
Gia_ObjSetSpec( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjChild0Spec(p, f, pObj), Gia_ObjChild1Spec(p, f, pObj)) ); 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 ); Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -654,31 +781,43 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames ...@@ -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" ); printf( "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" );
return NULL; 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 ); assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 );
p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) ); p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
vXorLits = Vec_IntAlloc( 1000 ); vXorLits = Vec_IntAlloc( 1000 );
Gia_ManSetPhase( p ); Gia_ManSetPhase( p );
if ( fDualOut )
Gia_ManEquivSetColors( p, 0 );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName ); pNew->pName = Aig_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew ); Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i ) 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++ ) 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_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_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_ManForEachCo( p, pObj, i )
{ {
Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f ); Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
Gia_ObjSetSpec( p, f, pObj, Gia_ObjChild0Spec(p, f, pObj) ); Gia_ObjSetCopyF( p, f, pObj, Gia_ObjFanin0CopyF(p, f, pObj) );
} }
if ( f == nFrames - 1 ) if ( f == nFrames - 1 )
break; break;
Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) 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 ) Vec_IntForEachEntry( vXorLits, iLitNew, i )
Gia_ManAppendCo( pNew, iLitNew ); Gia_ManAppendCo( pNew, iLitNew );
......
src/aig/saig/saig.h
...@@ -92,7 +92,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { ...@@ -92,7 +92,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) {
/*=== sswAbs.c ==========================================================*/ /*=== sswAbs.c ==========================================================*/
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose ); extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose );
/*=== saigBmc.c ==========================================================*/ /*=== 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 ); extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
/*=== saigCone.c ==========================================================*/ /*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p ); extern void Saig_ManPrintCones( Aig_Man_t * p );
......
src/aig/saig/saigBmc2.c
...@@ -173,16 +173,24 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax ...@@ -173,16 +173,24 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax
SeeAlso [] 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; sat_solver * pSat;
Cnf_Dat_t * pCnf; Cnf_Dat_t * pCnf;
Aig_Man_t * pFrames, * pAigTemp; Aig_Man_t * pFrames, * pAigTemp;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int status, clk, Lit, i, RetValue = 1; int status, clk, Lit, i, RetValue = 1;
// derive the timeframes // derive the timeframes
clk = clock(); 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 ); pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0); nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
......
src/aig/ssw/sswCore.c
...@@ -146,6 +146,18 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) ...@@ -146,6 +146,18 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0; nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
for ( nIter = 0; ; nIter++ ) 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(); clk = clock();
p->pMSat = Ssw_SatStart( 0 ); p->pMSat = Ssw_SatStart( 0 );
if ( p->pPars->fLatchCorrOpt ) if ( p->pPars->fLatchCorrOpt )
...@@ -199,18 +211,6 @@ clk = clock(); ...@@ -199,18 +211,6 @@ clk = clock();
Ssw_ManCleanup( p ); Ssw_ManCleanup( p );
if ( !RetValue ) if ( !RetValue )
break; 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->pPars->nIters = nIter + 1;
p->timeTotal = clock() - clkTotal; p->timeTotal = clock() - clkTotal;
......
src/base/abc/abc.h
...@@ -661,6 +661,7 @@ extern ABC_DLL Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, ...@@ -661,6 +661,7 @@ extern ABC_DLL Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames,
/*=== abcNames.c ====================================================*/ /*=== abcNames.c ====================================================*/
extern ABC_DLL char * Abc_ObjName( Abc_Obj_t * pNode ); 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_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_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix );
extern ABC_DLL char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits ); 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 ); extern ABC_DLL void Abc_NtkTrasferNames( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
......
src/base/abc/abcHie.c
...@@ -40,9 +40,9 @@ ...@@ -40,9 +40,9 @@
SeeAlso [] 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_Ntk_t * pNtkModel;
Abc_Obj_t * pObj, * pTerm, * pNet, * pFanin; Abc_Obj_t * pObj, * pTerm, * pNet, * pFanin;
int i, k; int i, k;
...@@ -70,7 +70,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in ...@@ -70,7 +70,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
(*pCounter)++; (*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 ) if ( *pCounter )
sprintf( Suffix, "_%s_%d", Abc_NtkName(pNtk), *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 ...@@ -98,7 +98,18 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
Abc_NtkForEachPi( pNtk, pTerm, i ) Abc_NtkForEachPi( pNtk, pTerm, i )
Abc_NodeSetTravIdCurrent( pTerm ); Abc_NodeSetTravIdCurrent( pTerm );
Abc_NtkForEachPo( pNtk, pTerm, i ) Abc_NtkForEachPo( pNtk, pTerm, i )
{
Abc_NodeSetTravIdCurrent( pTerm ); 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 ) Abc_NtkForEachBox( pNtk, pObj, i )
{ {
if ( Abc_ObjIsLatch(pObj) ) if ( Abc_ObjIsLatch(pObj) )
...@@ -144,7 +155,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in ...@@ -144,7 +155,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
Abc_ObjForEachFanout( pObj, pTerm, k ) Abc_ObjForEachFanout( pObj, pTerm, k )
Abc_ObjFanin0( Abc_NtkPo(pNtkModel, k) )->pCopy = Abc_ObjFanout0(pTerm)->pCopy; Abc_ObjFanin0( Abc_NtkPo(pNtkModel, k) )->pCopy = Abc_ObjFanout0(pTerm)->pCopy;
// call recursively // 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 // 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 ...@@ -168,7 +179,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ) Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy2( Abc_Ntk_t * pNtk )
{ {
Abc_Ntk_t * pNtkNew; Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pTerm, * pNet; Abc_Obj_t * pTerm, * pNet;
...@@ -203,7 +214,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ) ...@@ -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 // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes
Counter = -1; 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", printf( "Hierarchy reader flattened %d instances of logic boxes and left %d black boxes.\n",
Counter, Abc_NtkBlackboxNum(pNtkNew) ); Counter, Abc_NtkBlackboxNum(pNtkNew) );
...@@ -217,6 +228,241 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ) ...@@ -217,6 +228,241 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy; 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 // copy the timing information
// Abc_ManTimeDup( pNtk, pNtkNew ); // Abc_ManTimeDup( pNtk, pNtkNew );
// duplicate EXDC // duplicate EXDC
...@@ -231,6 +477,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk ) ...@@ -231,6 +477,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
return pNtkNew; return pNtkNew;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Extracts blackboxes by making them into additional PIs/POs.] Synopsis [Extracts blackboxes by making them into additional PIs/POs.]
......
src/base/abc/abcNames.c
...@@ -70,9 +70,27 @@ char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix ) ...@@ -70,9 +70,27 @@ char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix )
/**Function************************************************************* /**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 [] SideEffects []
...@@ -81,7 +99,7 @@ char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix ) ...@@ -81,7 +99,7 @@ char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix )
***********************************************************************/ ***********************************************************************/
char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, 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 ); sprintf( Buffer, "%s%s", Abc_ObjName(pObj), pSuffix );
return Buffer; return Buffer;
} }
...@@ -99,7 +117,7 @@ char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix ) ...@@ -99,7 +117,7 @@ char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix )
***********************************************************************/ ***********************************************************************/
char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits ) 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 ); sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num );
return Buffer; return Buffer;
} }
......
src/base/abci/abc.c
...@@ -17580,9 +17580,10 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -17580,9 +17580,10 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
int nNodeDelta; int nNodeDelta;
int fRewrite; int fRewrite;
int fNewAlgo; int fNewAlgo;
int nCofFanLit;
int fVerbose; 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); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
...@@ -17596,9 +17597,10 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -17596,9 +17597,10 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
nNodeDelta = 1000; nNodeDelta = 1000;
fRewrite = 0; fRewrite = 0;
fNewAlgo = 1; fNewAlgo = 1;
nCofFanLit = 0;
fVerbose = 0; fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDrvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDLrvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -17657,6 +17659,17 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -17657,6 +17659,17 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nNodeDelta < 0 ) if ( nNodeDelta < 0 )
goto usage; goto usage;
break; 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': case 'r':
fRewrite ^= 1; fRewrite ^= 1;
break; break;
...@@ -17687,19 +17700,20 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -17687,19 +17700,20 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Does not work for combinational networks.\n" ); fprintf( stdout, "Does not work for combinational networks.\n" );
return 0; 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 ??? pAbc->pCex = pNtk->pSeqModel; // temporary ???
return 0; return 0;
usage: usage:
// fprintf( pErr, "usage: bmc [-FNCGD num] [-ravh]\n" ); // 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 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-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-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-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-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-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-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-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" ); 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 ) ...@@ -17732,7 +17746,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
int fNewAlgo; int fNewAlgo;
int fVerbose; 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); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
...@@ -17837,7 +17851,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -17837,7 +17851,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Does not work for combinational networks.\n" ); fprintf( stdout, "Does not work for combinational networks.\n" );
return 0; 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 ??? pAbc->pCex = pNtk->pSeqModel; // temporary ???
return 0; return 0;
...@@ -22007,7 +22021,7 @@ usage: ...@@ -22007,7 +22021,7 @@ usage:
int Abc_CommandAbc9PSig( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9PSig( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
int c; int c;
int fSetReset = 0; int fSetReset = 1;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
{ {
...@@ -22032,7 +22046,7 @@ int Abc_CommandAbc9PSig( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22032,7 +22046,7 @@ int Abc_CommandAbc9PSig( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9PSigs(): Works only for sequential circuits.\n" ); printf( "Abc_CommandAbc9PSigs(): Works only for sequential circuits.\n" );
return 1; return 1;
} }
Gia_ManDetectSeqSignals( pAbc->pAig, fSetReset ); Gia_ManDetectSeqSignals( pAbc->pAig, fSetReset, 1 );
return 0; return 0;
usage: usage:
...@@ -22233,9 +22247,10 @@ usage: ...@@ -22233,9 +22247,10 @@ usage:
int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Gia_Man_t * pTemp; Gia_Man_t * pTemp;
int c, iVar = 0, nLimFan = 0; int c, fVerbose = 0;
int iVar = 0, nLimFan = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "VLh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "VLvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -22255,12 +22270,15 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -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" ); fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nLimFan = atoi(argv[globalUtilOptind]); nLimFan = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nLimFan < 0 ) if ( nLimFan < 0 )
goto usage; goto usage;
break; break;
case 'v':
fVerbose ^= 1;
break;
case 'h': case 'h':
goto usage; goto usage;
default: default:
...@@ -22272,7 +22290,21 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22272,7 +22290,21 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Cof(): There is no AIG.\n" ); printf( "Abc_CommandAbc9Cof(): There is no AIG.\n" );
return 1; 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 ) if ( pAbc->pAig == NULL )
{ {
pAbc->pAig = pTemp; pAbc->pAig = pTemp;
...@@ -22283,10 +22315,11 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22283,10 +22315,11 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( stdout, "usage: &cof [-VL num] [-h]\n" ); fprintf( stdout, "usage: &cof [-VL num] [-vh]\n" );
fprintf( stdout, "\t performs cofactoring w.r.t. a variable\n" ); fprintf( stdout, "\t performs cofactoring w.r.t. variable(s)\n" );
fprintf( stdout, "\t-V num : the zero-based ID of the variable to cofactor [default = %d]\n", iVar ); fprintf( stdout, "\t-V num : the zero-based ID of one 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, "\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"); fprintf( stdout, "\t-h : print the command usage\n");
return 1; return 1;
} }
...@@ -22825,9 +22858,10 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22825,9 +22858,10 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pTemp; Gia_Man_t * pTemp;
Gia_ParFra_t Pars, * pPars = &Pars; Gia_ParFra_t Pars, * pPars = &Pars;
int c; int c;
int nCofFanLit = 0;
Gia_ManFraSetDefaultParams( pPars ); Gia_ManFraSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FLivh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -22842,6 +22876,17 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22842,6 +22876,17 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nFrames < 0 ) if ( pPars->nFrames < 0 )
goto usage; goto usage;
break; 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': case 'i':
pPars->fInit ^= 1; pPars->fInit ^= 1;
break; break;
...@@ -22859,14 +22904,18 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22859,14 +22904,18 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Times(): There is no AIG.\n" ); printf( "Abc_CommandAbc9Times(): There is no AIG.\n" );
return 1; 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 ); Gia_ManStop( pTemp );
return 0; return 0;
usage: 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 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-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-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-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n"); fprintf( stdout, "\t-h : print the command usage\n");
...@@ -22929,7 +22978,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22929,7 +22978,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
pAbc->pAig = Gia_ManTransformMiter( pAux = pAbc->pAig ); pAbc->pAig = Gia_ManTransformMiter( pAux = pAbc->pAig );
Gia_ManStop( pAux ); 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; return 0;
} }
...@@ -23286,7 +23335,7 @@ usage: ...@@ -23286,7 +23335,7 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
char * pFileName = "gia_srm.aig"; char * pFileName = "gsrm.aig";
Gia_Man_t * pTemp; Gia_Man_t * pTemp;
int c, fVerbose = 0; int c, fVerbose = 0;
int fDualOut = 0; int fDualOut = 0;
...@@ -23314,11 +23363,14 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23314,11 +23363,14 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
// pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig, fDualOut ); // pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig, fDualOut );
// Gia_ManStop( pTemp ); // Gia_ManStop( pTemp );
pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut ); pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut, fVerbose );
Gia_WriteAiger( pTemp, "gia_srm.aig", 0, 0 ); if ( pTemp )
printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName ); {
Gia_ManPrintStatsShort( pTemp ); Gia_WriteAiger( pTemp, pFileName, 0, 0 );
Gia_ManStop( pTemp ); printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName );
Gia_ManPrintStatsShort( pTemp );
Gia_ManStop( pTemp );
}
return 0; return 0;
usage: usage:
...@@ -23346,14 +23398,18 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23346,14 +23398,18 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pTemp; Gia_Man_t * pTemp;
int c, fVerbose = 0; int c, fVerbose = 0;
int fUseAll = 0; int fUseAll = 0;
int fDualOut = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "avh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "advh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'a': case 'a':
fUseAll ^= 1; fUseAll ^= 1;
break; break;
case 'd':
fDualOut ^= 1;
break;
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;
break; break;
...@@ -23368,14 +23424,18 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23368,14 +23424,18 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Reduce(): There is no AIG.\n" ); printf( "Abc_CommandAbc9Reduce(): There is no AIG.\n" );
return 1; return 1;
} }
pAbc->pAig = Gia_ManEquivReduce( pTemp = pAbc->pAig, fUseAll ); pAbc->pAig = Gia_ManEquivReduce( pTemp = pAbc->pAig, fUseAll, fDualOut, fVerbose );
Gia_ManStop( pTemp ); if ( pAbc->pAig == NULL )
pAbc->pAig = pTemp;
else
Gia_ManStop( pTemp );
return 0; return 0;
usage: 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 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-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n"); fprintf( stdout, "\t-h : print the command usage\n");
return 1; return 1;
...@@ -23922,6 +23982,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -23922,6 +23982,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ManTestDistance( pAbc->pAig ); // Gia_ManTestDistance( pAbc->pAig );
// Gia_SatSolveTest( pAbc->pAig ); // Gia_SatSolveTest( pAbc->pAig );
// For_ManExperiment( pAbc->pAig, 20, 1, 1 ); // 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; return 0;
usage: usage:
......
src/base/abci/abcDar.c
...@@ -1538,7 +1538,7 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in ...@@ -1538,7 +1538,7 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
SeeAlso [] 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; Aig_Man_t * pMan;
int status, RetValue = -1, clk = clock(); int status, RetValue = -1, clk = clock();
...@@ -1554,7 +1554,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, ...@@ -1554,7 +1554,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
if ( fNewAlgo ) if ( fNewAlgo )
{ {
int iFrame; 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->pModel );
ABC_FREE( pNtk->pSeqModel ); ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
...@@ -1751,7 +1751,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) ...@@ -1751,7 +1751,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
} }
if ( pSecPar->fTryBmc ) 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 ) if ( RetValue == 0 )
{ {
printf( "Networks are not equivalent.\n" ); printf( "Networks are not equivalent.\n" );
......
src/base/main/mainMC.c
...@@ -91,7 +91,7 @@ int main( int argc, char * argv[] ) ...@@ -91,7 +91,7 @@ int main( int argc, char * argv[] )
{ {
// perform BMC // perform BMC
if ( pAig->nRegs != 0 ) 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 // perform full-blown SEC
if ( RetValue != 0 ) if ( RetValue != 0 )
...@@ -120,7 +120,7 @@ int main( int argc, char * argv[] ) ...@@ -120,7 +120,7 @@ int main( int argc, char * argv[] )
int nSizeMax = 500000; int nSizeMax = 500000;
int nBTLimit = 10000000; int nBTLimit = 10000000;
int fRewrite = 0; 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 ) if ( RetValue != 0 )
RetValue = -1; RetValue = -1;
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment