summaryrefslogtreecommitdiffstats
path: root/src/aig/gia
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2009-03-10 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2009-03-10 08:01:00 -0700
commit32314347bae6ddcd841a268e797ec4da45726abb (patch)
treee2e5fd1711f04a06d0da2b8003bc02cb9a5dd446 /src/aig/gia
parentc03f9b516bed2c06ec2bfc78617eba5fc9a11c32 (diff)
downloadabc-32314347bae6ddcd841a268e797ec4da45726abb.tar.gz
abc-32314347bae6ddcd841a268e797ec4da45726abb.tar.bz2
abc-32314347bae6ddcd841a268e797ec4da45726abb.zip
Version abc90310
Diffstat (limited to 'src/aig/gia')
-rw-r--r--src/aig/gia/gia.h165
-rw-r--r--src/aig/gia/giaAig.c6
-rw-r--r--src/aig/gia/giaAiger.c309
-rw-r--r--src/aig/gia/giaCof.c8
-rw-r--r--src/aig/gia/giaDup.c214
-rw-r--r--src/aig/gia/giaEmbed.c460
-rw-r--r--src/aig/gia/giaEnable.c210
-rw-r--r--src/aig/gia/giaEquiv.c618
-rw-r--r--src/aig/gia/giaForce.c1117
-rw-r--r--src/aig/gia/giaMan.c11
-rw-r--r--src/aig/gia/giaMap.c305
-rw-r--r--src/aig/gia/giaScl.c52
-rw-r--r--src/aig/gia/giaSort.c13
-rw-r--r--src/aig/gia/giaUtil.c67
-rw-r--r--src/aig/gia/module.make3
15 files changed, 3130 insertions, 428 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index b77dd76f..91507947 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -36,27 +36,50 @@ extern "C" {
#endif
#define GIA_NONE 0x1FFFFFFF
+#define GIA_VOID 0x0FFFFFFF
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
+typedef struct Gia_Rpr_t_ Gia_Rpr_t;
+struct Gia_Rpr_t_
+{
+ unsigned iRepr : 28; // representative node
+ unsigned fProved : 1; // marks the proved equivalence
+ unsigned fFailed : 1; // marks the failed equivalence
+ unsigned fColorA : 1; // marks cone of A
+ unsigned fColorB : 1; // marks cone of B
+};
+
typedef struct Gia_Obj_t_ Gia_Obj_t;
struct Gia_Obj_t_
{
- unsigned iDiff0 : 29; // the diff of the first fanin
- unsigned fCompl0: 1; // the complemented attribute
- unsigned fMark0 : 1; // first user-controlled mark
- unsigned fTerm : 1; // terminal node (CI/CO)
+ unsigned iDiff0 : 29; // the diff of the first fanin
+ unsigned fCompl0: 1; // the complemented attribute
+ unsigned fMark0 : 1; // first user-controlled mark
+ unsigned fTerm : 1; // terminal node (CI/CO)
- unsigned iDiff1 : 29; // the diff of the second fanin
- unsigned fCompl1: 1; // the complemented attribute
- unsigned fMark1 : 1; // second user-controlled mark
- unsigned fPhase : 1; // value under 000 pattern
+ unsigned iDiff1 : 29; // the diff of the second fanin
+ unsigned fCompl1: 1; // the complemented attribute
+ unsigned fMark1 : 1; // second user-controlled mark
+ unsigned fPhase : 1; // value under 000 pattern
unsigned Value; // application-specific value
};
+// sequential counter-example
+typedef struct Gia_Cex_t_ Gia_Cex_t;
+struct Gia_Cex_t_
+{
+ int iPo; // the zero-based number of PO, for which verification failed
+ int iFrame; // the zero-based number of the time-frame, for which verificaiton failed
+ int nRegs; // the number of registers in the miter
+ int nPis; // the number of primary inputs in the miter
+ int nBits; // the number of words of bit data used
+ unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
+};
+
typedef struct Gia_Man_t_ Gia_Man_t;
struct Gia_Man_t_
{
@@ -76,23 +99,42 @@ struct Gia_Man_t_
int nLevels; // the mamixum level
int nTravIds; // the current traversal ID
int nFront; // frontier size
- int * pReprs; // representatives (for CIs and ANDs)
+ int * pReprsOld; // representatives (for CIs and ANDs)
+ Gia_Rpr_t * pReprs; // representatives (for CIs and ANDs)
+ int * pNexts; // next nodes in the equivalence classes
+ int * pIso; // pairs of structurally isomorphic nodes
int nTerLoop; // the state where loop begins
int nTerStates; // the total number of ternary states
int * pFanData; // the database to store fanout information
int nFansAlloc; // the size of fanout representation
+ int * pMapping; // mapping for each node
+ Gia_Cex_t * pCexComb; // combinational counter-example
};
+typedef struct Emb_Par_t_ Emb_Par_t;
+struct Emb_Par_t_
+{
+ int nDims; // the number of dimension
+ int nSols; // the number of solutions (typically, 2)
+ int nIters; // the number of iterations of FORCE
+ int fRefine; // use refinement by FORCE
+ int fCluster; // use clustered representation
+ int fDump; // dump Gnuplot file
+ int fDumpLarge; // dump Gnuplot file for large benchmarks
+ int fShowImage; // shows image if Gnuplot is installed
+ int fVerbose; // verbose flag
+};
+
// frames parameters
typedef struct Gia_ParFra_t_ Gia_ParFra_t;
struct Gia_ParFra_t_
{
- int nFrames; // the number of frames to unroll
- int fInit; // initialize the timeframes
- int fVerbose; // enables verbose output
+ int nFrames; // the number of frames to unroll
+ int fInit; // initialize the timeframes
+ int fVerbose; // enables verbose output
};
@@ -180,17 +222,17 @@ static inline int Gia_ObjFaninId0p( Gia_Man_t * p, Gia_Obj_t * pObj ) {
static inline int Gia_ObjFaninId1p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId1( pObj, Gia_ObjId(p, pObj) ); }
static inline int Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId ) { return Gia_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); }
static inline int Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId ) { return Gia_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); }
-static inline int Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) ); }
-static inline int Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) ); }
+static inline int Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) ); }
+static inline int Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) ); }
static inline void Gia_ObjFlipFaninC0( Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1; }
static inline int Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) { return Gia_ObjFanin0(pObj) == pFanin ? 0 : (Gia_ObjFanin1(pObj) == pFanin ? 1 : -1); }
-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_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 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_LitNotCond( 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_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_ObjValue( Gia_Obj_t * pObj ) { return pObj->Value; }
static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(p->pLevels);return p->pLevels[Gia_ObjId(p, pObj)]; }
@@ -204,12 +246,12 @@ static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){
static inline void Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin1(pObj)); }
static inline void Gia_ManResetTravId( Gia_Man_t * p ) { extern void Gia_ManCleanValue( Gia_Man_t * p ); Gia_ManCleanValue( p ); p->nTravIds = 1; }
-static inline void Gia_ManIncrementTravId( Gia_Man_t * p ) { p->nTravIds++; }
-static inline void Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId ) { pObj->Value = TravId; }
-static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds; }
-static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds - 1; }
-static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds); }
-static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds - 1); }
+static inline void Gia_ManIncrementTravId( Gia_Man_t * p ) { p->nTravIds++; }
+static inline void Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId ) { pObj->Value = TravId; }
+static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds; }
+static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds - 1; }
+static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds); }
+static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds - 1); }
// AIG construction
extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
@@ -293,6 +335,54 @@ static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCom
return GIA_ONE;
}
+static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr ); }
+static inline int Gia_ObjRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr; }
+static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { p->pReprs[Id].iRepr = Num; }
+
+static inline int Gia_ObjProved( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fProved; }
+static inline void Gia_ObjSetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 1; }
+
+static inline int Gia_ObjFailed( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fFailed; }
+static inline void Gia_ObjSetFailed( Gia_Man_t * p, int Id ) { p->pReprs[Id].fFailed = 1; }
+
+static inline int Gia_ObjColor( Gia_Man_t * p, int Id, int c ) { return c? p->pReprs[Id].fColorB : p->pReprs[Id].fColorA; }
+static inline int Gia_ObjColors( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fColorB * 2 + p->pReprs[Id].fColorA; }
+static inline void Gia_ObjSetColor( Gia_Man_t * p, int Id, int c ) { if (c) p->pReprs[Id].fColorB = 1; else p->pReprs[Id].fColorA = 1; }
+static inline void Gia_ObjSetColors( Gia_Man_t * p, int Id ) { p->pReprs[Id].fColorB = p->pReprs[Id].fColorA = 1; }
+static inline int Gia_ObjVisitColor( Gia_Man_t * p, int Id, int c ) { int x; if (c) { x = p->pReprs[Id].fColorB; p->pReprs[Id].fColorB = 1; } else { x = p->pReprs[Id].fColorA; p->pReprs[Id].fColorA = 1; } return x; }
+static inline int Gia_ObjDiffColors( Gia_Man_t * p, int i, int j ) { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) && (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); }
+static inline int Gia_ObjDiffColors2( Gia_Man_t * p, int i, int j ) { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) || (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); }
+
+static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { return p->pNexts[Id]; }
+static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; }
+
+static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; }
+static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; }
+static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; }
+static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; }
+static inline int Gia_ObjIsClass( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0; }
+
+#define Gia_ManForEachConst( p, i ) \
+ for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else
+#define Gia_ManForEachClass( p, i ) \
+ for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsHead(p, i) ) {} else
+#define Gia_ManForEachClassReverse( p, i ) \
+ for ( i = Gia_ManObjNum(p) - 1; i > 0; i-- ) if ( !Gia_ObjIsHead(p, i) ) {} else
+#define Gia_ClassForEachObj( p, i, iObj ) \
+ for ( assert(Gia_ObjIsHead(p, i)), iObj = i; iObj; iObj = Gia_ObjNext(p, iObj) )
+#define Gia_ClassForEachObj1( p, i, iObj ) \
+ for ( assert(Gia_ObjIsHead(p, i)), iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iObj) )
+
+
+static inline int Gia_ObjIsGate( Gia_Man_t * p, int Id ) { return p->pMapping[Id] != 0; }
+static inline int Gia_ObjGateSize( Gia_Man_t * p, int Id ) { return p->pMapping[p->pMapping[Id]]; }
+static inline int * Gia_ObjGateFanins( Gia_Man_t * p, int Id ) { return p->pMapping + p->pMapping[Id] + 1; }
+
+#define Gia_ManForEachGate( p, i ) \
+ for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsGate(p, i) ) {} else
+#define Gia_GateForEachFanin( p, i, iFan, k ) \
+ for ( k = 0; k < Gia_ObjGateSize(p,i) && ((iFan = Gia_ObjGateFanins(p,i)[k]),1); k++ )
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -351,18 +441,30 @@ extern Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
extern Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
extern Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p );
-extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p );
-extern Gia_Man_t * Gia_ManDupCofactored( Gia_Man_t * p, int iVar );
+extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos );
+extern Gia_Man_t * Gia_ManDupCofactored( Gia_Man_t * p, int iVar, int nLimFan );
extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
+extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fXorOuts, int fComb, int fVerbose );
+extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
+/*=== giaEnable.c ==========================================================*/
+extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset );
+/*=== giaEquiv.c ==========================================================*/
+extern int * Gia_ManDeriveNexts( Gia_Man_t * p );
+extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
+extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
+extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
+extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
+extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p );
+extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
/*=== giaFanout.c =========================================================*/
extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
extern void Gia_ObjRemoveFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
extern void Gia_ManFanoutStart( Gia_Man_t * p );
extern void Gia_ManFanoutStop( Gia_Man_t * p );
/*=== giaForce.c =========================================================*/
-extern void For_ManExperiment( Gia_Man_t * pGia );
+extern void For_ManExperiment( Gia_Man_t * pGia, int nIters, int fClustered, int fVerbose );
/*=== giaFrames.c =========================================================*/
extern void Gia_ManFraSetDefaultParams( Gia_ParFra_t * p );
extern Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars );
@@ -380,7 +482,7 @@ extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit
extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p );
/*=== giaLogic.c ===========================================================*/
extern void Gia_ManTestDistance( Gia_Man_t * p );
-extern void Gia_ManSolveProblem( Gia_Man_t * pGia, int nDims, int nSols, int fCluster, int fDump, int fVerbose );
+extern void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars );
/*=== giaMan.c ===========================================================*/
extern Gia_Man_t * Gia_ManStart( int nObjsMax );
extern void Gia_ManStop( Gia_Man_t * p );
@@ -388,13 +490,18 @@ extern void Gia_ManPrintStats( Gia_Man_t * p );
extern void Gia_ManPrintStatsShort( Gia_Man_t * p );
extern void Gia_ManPrintMiterStatus( Gia_Man_t * p );
extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
+/*=== giaMap.c ===========================================================*/
+extern void Gia_ManPrintMappingStats( Gia_Man_t * p );
/*=== giaSat.c ============================================================*/
extern int Sat_ManTest( Gia_Man_t * pGia, Gia_Obj_t * pObj, int nConfsMax );
/*=== giaScl.c ============================================================*/
+extern int Gia_ManSeqMarkUsed( Gia_Man_t * p );
extern int Gia_ManCombMarkUsed( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose );
+/*=== giaSort.c ============================================================*/
+extern int * Gia_SortFloats( float * pArray, int * pPerm, int nSize );
/*=== giaSim.c ============================================================*/
extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
/*=== giaTsim.c ============================================================*/
@@ -411,6 +518,7 @@ extern void Gia_ManFillValue( Gia_Man_t * p );
extern void Gia_ManSetPhase( Gia_Man_t * p );
extern int Gia_ManLevelNum( Gia_Man_t * p );
extern void Gia_ManSetRefs( Gia_Man_t * p );
+extern int * Gia_ManCreateMuxRefs( Gia_Man_t * p );
extern void Gia_ManCreateRefs( Gia_Man_t * p );
extern int Gia_ManCrossCut( Gia_Man_t * p );
extern int Gia_ManIsNormalized( Gia_Man_t * p );
@@ -418,6 +526,7 @@ extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p );
extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode );
extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 );
extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
+extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOuts );
#ifdef __cplusplus
}
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 8b59341a..544cfe0d 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -92,10 +92,9 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
}
// add logic for the POs
Aig_ManForEachPo( p, pObj, i )
- {
Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) );
+ Aig_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
- }
Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
return pNew;
}
@@ -133,10 +132,9 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
}
// add logic for the POs
Aig_ManForEachPo( p, pObj, i )
- {
Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) );
+ Aig_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
- }
Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
return pNew;
}
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 40c5329d..cfd2dc73 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -175,6 +175,120 @@ char * Gia_TimeStamp()
/**Function*************************************************************
+ Synopsis [Read integer from the string.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ReadInt( unsigned char * pPos )
+{
+ int i, Value = 0;
+ for ( i = 0; i < 4; i++ )
+ Value = (Value << 8) | *pPos++;
+ return Value;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Read equivalence classes from the string.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize )
+{
+ Gia_Rpr_t * pReprs;
+ unsigned char * pStop;
+ int i, Item, fProved, iRepr, iNode;
+ pStop = *ppPos;
+ pStop += Gia_ReadInt( *ppPos ); *ppPos += 4;
+ pReprs = ABC_CALLOC( Gia_Rpr_t, nSize );
+ for ( i = 0; i < nSize; i++ )
+ pReprs[i].iRepr = GIA_VOID;
+ iRepr = iNode = 0;
+ while ( *ppPos < pStop )
+ {
+ Item = Gia_ReadAigerDecode( ppPos );
+ if ( Item & 1 )
+ {
+ iRepr += (Item >> 1);
+ iNode = iRepr;
+//printf( "\nRepr = %d ", iRepr );
+ continue;
+ }
+ Item >>= 1;
+ fProved = (Item & 1);
+ Item >>= 1;
+ iNode += Item;
+ pReprs[iNode].fProved = fProved;
+ pReprs[iNode].iRepr = iRepr;
+//printf( "Node = %d ", iNode );
+ }
+ return pReprs;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads decoded value.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Gia_ReadDiffValue( char ** ppPos, int iPrev )
+{
+ int Item = Gia_ReadAigerDecode( ppPos );
+ if ( Item & 1 )
+ return iPrev + (Item >> 1);
+ return iPrev - (Item >> 1);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Read equivalence classes from the string.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Gia_ReadMapping( unsigned char ** ppPos, int nSize )
+{
+ int * pMapping;
+ unsigned char * pStop;
+ int k, j, nFanins, nAlloc, iNode = 0, iOffset = nSize;
+ pStop = *ppPos;
+ pStop += Gia_ReadInt( *ppPos ); *ppPos += 4;
+ nAlloc = nSize + pStop - *ppPos;
+ pMapping = ABC_CALLOC( int, nAlloc );
+ while ( *ppPos < pStop )
+ {
+ k = iOffset;
+ pMapping[k++] = nFanins = Gia_ReadAigerDecode( ppPos );
+ for ( j = 0; j <= nFanins; j++ )
+ pMapping[k++] = iNode = Gia_ReadDiffValue( ppPos, iNode );
+ pMapping[iNode] = iOffset;
+ iOffset = k;
+ }
+ assert( iOffset <= nAlloc );
+ return pMapping;
+}
+
+/**Function*************************************************************
+
Synopsis [Reads the AIG in the binary AIGER format.]
Description []
@@ -328,6 +442,38 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
// create the latches
Gia_ManSetRegNum( pNew, nLatches );
+ // check if there are other types of information to read
+ pCur = pSymbols;
+ if ( pCur + 1 < pContents + nFileSize && *pCur == 'c' )
+ {
+ pCur++;
+ if ( *pCur == 'e' )
+ {
+ pCur++;
+ // read equivalence classes
+ pNew->pReprs = Gia_ReadEquivClasses( &pCur, Gia_ManObjNum(pNew) );
+ pNew->pNexts = Gia_ManDeriveNexts( pNew );
+ }
+ if ( *pCur == 'm' )
+ {
+ pCur++;
+ // read mapping
+ pNew->pMapping = Gia_ReadMapping( &pCur, Gia_ManObjNum(pNew) );
+ }
+ if ( *pCur == 'p' )
+ {
+ pCur++;
+ // read placement
+ }
+ if ( *pCur == 'n' )
+ {
+ pCur++;
+ // read model name
+ ABC_FREE( pNew->pName );
+ pNew->pName = Aig_UtilStrsav( pCur );
+ }
+ }
+
// skipping the comments
ABC_FREE( pContents );
Vec_IntFree( vNodes );
@@ -443,6 +589,144 @@ Vec_Str_t * Gia_WriteEncodeLiterals( Vec_Int_t * vLits )
/**Function*************************************************************
+ Synopsis [Write integer into the string.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_WriteInt( unsigned char * pPos, int Value )
+{
+ int i;
+ for ( i = 3; i >= 0; i-- )
+ *pPos++ = (Value >> (8*i)) & 255;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Read equivalence classes from the string.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned char * Gia_WriteEquivClasses( Gia_Man_t * p, int * pEquivSize )
+{
+ unsigned char * pBuffer;
+ int iRepr, iNode, iPrevRepr, iPrevNode, iLit, nItems, iPos;
+ assert( p->pReprs && p->pNexts );
+ // count the number of entries to be written
+ nItems = 0;
+ for ( iRepr = 1; iRepr < Gia_ManObjNum(p); iRepr++ )
+ {
+ nItems += Gia_ObjIsConst( p, iRepr );
+ if ( !Gia_ObjIsHead(p, iRepr) )
+ continue;
+ Gia_ClassForEachObj( p, iRepr, iNode )
+ nItems++;
+ }
+ pBuffer = ABC_ALLOC( char, sizeof(int) * (nItems + 1) );
+ // write constant class
+ iPos = Gia_WriteAigerEncode( pBuffer, 4, Gia_Var2Lit(0, 1) );
+//printf( "\nRepr = %d ", 0 );
+ iPrevNode = 0;
+ for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ )
+ if ( Gia_ObjIsConst(p, iNode) )
+ {
+//printf( "Node = %d ", iNode );
+ iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
+ iPrevNode = iNode;
+ iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) );
+ }
+ // write non-constant classes
+ iPrevRepr = 0;
+ Gia_ManForEachClass( p, iRepr )
+ {
+//printf( "\nRepr = %d ", iRepr );
+ iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iRepr - iPrevRepr, 1) );
+ iPrevRepr = iPrevNode = iRepr;
+ Gia_ClassForEachObj1( p, iRepr, iNode )
+ {
+//printf( "Node = %d ", iNode );
+ iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
+ iPrevNode = iNode;
+ iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) );
+ }
+ }
+ Gia_WriteInt( pBuffer, iPos );
+ *pEquivSize = iPos;
+ return pBuffer;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads decoded value.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_WriteDiffValue( char * pPos, int iPos, int iPrev, int iThis )
+{
+ if ( iPrev < iThis )
+ return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iThis - iPrev, 1) );
+ return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iPrev - iThis, 0) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Read equivalence classes from the string.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned char * Gia_WriteMapping( Gia_Man_t * p, int * pMapSize )
+{
+ unsigned char * pBuffer;
+ int i, k, iPrev, iFan, nItems, iPos = 4;
+ assert( p->pMapping );
+ // count the number of entries to be written
+ nItems = 0;
+ Gia_ManForEachGate( p, i )
+ nItems += 2 + Gia_ObjGateSize( p, i );
+ pBuffer = ABC_ALLOC( char, sizeof(int) * (nItems + 1) );
+ // write non-constant classes
+ iPrev = 0;
+ Gia_ManForEachGate( p, i )
+ {
+//printf( "\nSize = %d ", Gia_ObjGateSize(p, i) );
+ iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_ObjGateSize(p, i) );
+ Gia_GateForEachFanin( p, i, iFan, k )
+ {
+//printf( "Fan = %d ", iFan );
+ iPos = Gia_WriteDiffValue( pBuffer, iPos, iPrev, iFan );
+ iPrev = iFan;
+ }
+ iPos = Gia_WriteDiffValue( pBuffer, iPos, iPrev, i );
+ iPrev = i;
+//printf( "Node = %d ", i );
+ }
+//printf( "\n" );
+ Gia_WriteInt( pBuffer, iPos );
+ *pMapSize = iPos;
+ return pBuffer;
+}
+
+/**Function*************************************************************
+
Synopsis [Writes the AIG in the binary AIGER format.]
Description []
@@ -536,10 +820,29 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
ABC_FREE( pBuffer );
// write the comment
- fprintf( pFile, "c\n" );
+ fprintf( pFile, "c" );
+ // write equivalences
+ if ( p->pReprs && p->pNexts )
+ {
+ int nEquivSize;
+ unsigned char * pEquivs = Gia_WriteEquivClasses( p, &nEquivSize );
+ fprintf( pFile, "e" );
+ fwrite( pEquivs, 1, nEquivSize, pFile );
+ ABC_FREE( pEquivs );
+ }
+ // write mapping
+ if ( p->pMapping )
+ {
+ int nMapSize;
+ unsigned char * pMaps = Gia_WriteMapping( p, &nMapSize );
+ fprintf( pFile, "m" );
+ fwrite( pMaps, 1, nMapSize, pFile );
+ ABC_FREE( pMaps );
+ }
+ // write placement
if ( p->pName )
- fprintf( pFile, ".model %s\n", p->pName );
- fprintf( pFile, "This file was produced by the AIG package on %s\n", Gia_TimeStamp() );
+ fprintf( pFile, "n%s%c", p->pName, '\0' );
+ fprintf( pFile, "\nThis file was produced by the GIA package in ABC on %s\n", Gia_TimeStamp() );
fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
fclose( pFile );
if ( p != pInit )
diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c
index d58429cd..735aca72 100644
--- a/src/aig/gia/giaCof.c
+++ b/src/aig/gia/giaCof.c
@@ -41,6 +41,7 @@ struct Cof_Obj_t_
unsigned fMark1 : 1; // second user-controlled mark
unsigned nFanins : 4; // the number of fanins
unsigned nFanouts : 24; // total number of fanouts
+ unsigned nFanoutsM; // total number of MUX ctrl fanouts
unsigned Value; // application specific data
int Id; // ID of the node
int iNext; // next one in the linked list
@@ -124,6 +125,7 @@ Cof_Man_t * Cof_ManCreateLogicSimple( Gia_Man_t * pGia )
Cof_Man_t * p;
Cof_Obj_t * pObjLog, * pFanLog;
Gia_Obj_t * pObj;
+ int * pMuxRefs;
int i, iHandle = 0;
p = ABC_CALLOC( Cof_Man_t, 1 );
p->pGia = pGia;
@@ -173,11 +175,14 @@ Cof_Man_t * Cof_ManCreateLogicSimple( Gia_Man_t * pGia )
p->nObjs++;
}
assert( iHandle == p->nObjData );
+ pMuxRefs = Gia_ManCreateMuxRefs( pGia );
Gia_ManForEachObj( pGia, pObj, i )
{
pObjLog = Cof_ManObj( p, Gia_ObjHandle(pObj) );
assert( pObjLog->nFanouts == pObjLog->Value );
+ pObjLog->nFanoutsM = pMuxRefs[i];
}
+ ABC_FREE( pMuxRefs );
return p;
}
@@ -509,8 +514,7 @@ int Cof_ManCountRemoved( Cof_Man_t * p, Cof_Obj_t * pRoot, int fConst1 )
void Cof_ManPrintHighFanoutOne( Cof_Man_t * p, Cof_Obj_t * pObj )
{
printf( "%7d : ", pObj->Id );
- printf( "fi =%2d ", Cof_ObjFaninNum(pObj) );
- printf( "fo =%5d ", Cof_ObjFanoutNum(pObj) );
+ printf( "i/o/c =%2d %5d %5d ", Cof_ObjFaninNum(pObj), Cof_ObjFanoutNum(pObj), 2*pObj->nFanoutsM );
printf( "l =%4d ", Cof_ObjLevel(p, pObj) );
printf( "s =%5d ", Cof_ManSuppSize(p, &pObj, 1) );
printf( "TFI =%7d ", Cof_ManTfiSize(p, &pObj, 1) );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index d5c0862f..4821dba9 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -196,11 +196,11 @@ int Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return pObj->Value;
- if ( p->pReprs && ~p->pReprs[Gia_ObjId(p, pObj)] )
+ if ( p->pReprsOld && ~p->pReprsOld[Gia_ObjId(p, pObj)] )
{
- Gia_Obj_t * pRepr = Gia_ManObj( p, p->pReprs[Gia_ObjId(p, pObj)] );
- pObj->Value = Gia_ManDupDfs_rec( pNew, p, pRepr );
- return pObj->Value = Gia_LitNotCond( pObj->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+ Gia_Obj_t * pRepr = Gia_ManObj( p, p->pReprsOld[Gia_ObjId(p, pObj)] );
+ pRepr->Value = Gia_ManDupDfs_rec( pNew, p, pRepr );
+ return pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
}
if ( Gia_ObjIsCi(pObj) )
return pObj->Value = Gia_ManAppendCi(pNew);
@@ -380,7 +380,7 @@ Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p )
+Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
@@ -391,12 +391,12 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p )
Gia_ManSetRefs( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
- if ( pObj->Value > 0 || Gia_ObjIsRo(p, pObj) )
+ if ( !fTrimCis || pObj->Value > 0 || Gia_ObjIsRo(p, pObj) )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachCo( p, pObj, i )
- if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) || Gia_ObjIsRi(p, pObj) )
+ if ( !fTrimCos || !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) || Gia_ObjIsRi(p, pObj) )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
@@ -413,11 +413,16 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManDupCofactored( Gia_Man_t * p, int iVar )
+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) );
@@ -502,7 +507,7 @@ void Gia_ManPrintRepr( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
Gia_ManForEachObj( p, pObj, i )
- if ( ~p->pReprs[i] )
+ if ( ~p->pReprsOld[i] )
printf( "%d->%d ", i, p->pReprs[i] );
printf( "\n" );
}
@@ -569,7 +574,7 @@ Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p )
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;
- assert( p->pReprs != NULL );
+ assert( p->pReprsOld != NULL );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
@@ -719,6 +724,195 @@ Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose )
}
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( ~pObj->Value )
+ return pObj->Value;
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
+ return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates miter of two designs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fXorOuts, int fComb, int fVerbose )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj;
+ int i, iLit;
+ if ( fComb )
+ {
+ if ( Gia_ManCiNum(p0) != Gia_ManCiNum(p1) )
+ {
+ printf( "Gia_ManMiter(): Designs have different number of CIs.\n" );
+ return NULL;
+ }
+ if ( Gia_ManCoNum(p0) != Gia_ManCoNum(p1) )
+ {
+ printf( "Gia_ManMiter(): Designs have different number of COs.\n" );
+ return NULL;
+ }
+ }
+ else
+ {
+ if ( Gia_ManPiNum(p0) != Gia_ManPiNum(p1) )
+ {
+ printf( "Gia_ManMiter(): Designs have different number of PIs.\n" );
+ return NULL;
+ }
+ if ( Gia_ManPoNum(p0) != Gia_ManPoNum(p1) )
+ {
+ printf( "Gia_ManMiter(): Designs have different number of POs.\n" );
+ return NULL;
+ }
+ if ( Gia_ManRegNum(p0) == 0 || Gia_ManRegNum(p1) == 0 )
+ {
+ printf( "Gia_ManMiter(): At least one of the designs has no registers.\n" );
+ return NULL;
+ }
+ }
+ // start the manager
+ pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) );
+ pNew->pName = Aig_UtilStrsav( "miter" );
+ // map combinational inputs
+ Gia_ManFillValue( p0 );
+ Gia_ManFillValue( p1 );
+ Gia_ManConst0(p0)->Value = 0;
+ Gia_ManConst0(p1)->Value = 0;
+ // map internal nodes and outputs
+ Gia_ManHashAlloc( pNew );
+ if ( fComb )
+ {
+ // create combinational inputs
+ Gia_ManForEachCi( p0, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ Gia_ManForEachCi( p1, pObj, i )
+ pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) );
+ // create combinational outputs
+ Gia_ManForEachCo( p0, pObj, i )
+ {
+ Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
+ Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManCo(p1,i)) );
+ if ( fXorOuts )
+ {
+ iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
+ Gia_ManAppendCo( pNew, iLit );
+ }
+ else
+ {
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
+ }
+ }
+ }
+ else
+ {
+ // create primary inputs
+ Gia_ManForEachPi( p0, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ Gia_ManForEachPi( p1, pObj, i )
+ pObj->Value = Gia_ObjToLit( pNew, Gia_ManPi(pNew, i) );
+ // create latch outputs
+ Gia_ManForEachRo( p0, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ Gia_ManForEachRo( p1, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ // create primary outputs
+ Gia_ManForEachPo( p0, pObj, i )
+ {
+ Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
+ Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(Gia_ManPo(p1,i)) );
+ if ( fXorOuts )
+ {
+ iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
+ Gia_ManAppendCo( pNew, iLit );
+ }
+ else
+ {
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
+ }
+ }
+ // create register inputs
+ Gia_ManForEachRi( p0, pObj, i )
+ {
+ Gia_ManMiter_rec( pNew, p0, Gia_ObjFanin0(pObj) );
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ Gia_ManForEachRi( p1, pObj, i )
+ {
+ Gia_ManMiter_rec( pNew, p1, Gia_ObjFanin0(pObj) );
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p0) + Gia_ManRegNum(p1) );
+ }
+ Gia_ManHashStop( pNew );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the circuit into a regular miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj, * pObj2;
+ int i, iLit;
+ assert( (Gia_ManPoNum(p) & 1) == 0 );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManHashAlloc( 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 )
+ {
+ pObj2 = Gia_ManPo( p, ++i );
+ iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(pObj2) );
+ Gia_ManAppendCo( pNew, iLit );
+ }
+ Gia_ManForEachRi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManHashStop( pNew );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c
index 0469d1a4..6c2f00df 100644
--- a/src/aig/gia/giaEmbed.c
+++ b/src/aig/gia/giaEmbed.c
@@ -25,12 +25,18 @@
The code is based on the paper by D. Harel and Y. Koren,
"Graph drawing by high-dimensional embedding",
J. Graph Algs & Apps, Vol 8(2), pp. 195-217 (2004).
+ http://www.emis.de/journals/JGAA/accepted/2004/HarelKoren2004.8.2.pdf
+
+ Iterative refinement is described in the paper: F. A. Aloul, I. L. Markov, and K. A. Sakallah.
+ "FORCE: A Fast and Easy-To-Implement Variable-Ordering Heuristic", Proc. GLSVLSI’03.
+ http://www.eecs.umich.edu/~imarkov/pubs/conf/glsvlsi03-force.pdf
*/
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+
typedef float Emb_Dat_t;
typedef struct Emb_Obj_t_ Emb_Obj_t;
@@ -90,10 +96,10 @@ static inline Emb_Obj_t * Emb_ManCo( Emb_Man_t * p, int i )
static inline int Emb_ObjIsTerm( Emb_Obj_t * pObj ) { return pObj->fCi || pObj->fCo; }
static inline int Emb_ObjIsCi( Emb_Obj_t * pObj ) { return pObj->fCi; }
static inline int Emb_ObjIsCo( Emb_Obj_t * pObj ) { return pObj->fCo; }
-static inline int Emb_ObjIsPi( Emb_Obj_t * pObj ) { return pObj->fCi && pObj->nFanins == 0; }
-static inline int Emb_ObjIsPo( Emb_Obj_t * pObj ) { return pObj->fCo && pObj->nFanouts == 0; }
+//static inline int Emb_ObjIsPi( Emb_Obj_t * pObj ) { return pObj->fCi && pObj->nFanins == 0; }
+//static inline int Emb_ObjIsPo( Emb_Obj_t * pObj ) { return pObj->fCo && pObj->nFanouts == 0; }
static inline int Emb_ObjIsNode( Emb_Obj_t * pObj ) { return!Emb_ObjIsTerm(pObj) && pObj->nFanins > 0; }
-static inline int Emb_ObjIsConst0( Emb_Obj_t * pObj ) { return!Emb_ObjIsTerm(pObj) && pObj->nFanins == 0; }
+//static inline int Emb_ObjIsConst0( Emb_Obj_t * pObj ) { return!Emb_ObjIsTerm(pObj) && pObj->nFanins == 0; }
static inline int Emb_ObjSize( Emb_Obj_t * pObj ) { return sizeof(Emb_Obj_t) / 4 + pObj->nFanins + pObj->nFanouts; }
static inline int Emb_ObjFaninNum( Emb_Obj_t * pObj ) { return pObj->nFanins; }
@@ -109,8 +115,8 @@ static inline void Emb_ObjSetTravIdPrevious( Emb_Man_t * p, Emb_Obj_t * p
static inline int Emb_ObjIsTravIdCurrent( Emb_Man_t * p, Emb_Obj_t * pObj ) { return ((int)pObj->TravId == p->nTravIds); }
static inline int Emb_ObjIsTravIdPrevious( Emb_Man_t * p, Emb_Obj_t * pObj ) { return ((int)pObj->TravId == p->nTravIds - 1); }
-static inline Emb_Dat_t * Emb_ManVec( Emb_Man_t * p, int v ) { return p->pVecs + v * p->nObjs; }
-static inline float * Emb_ManSol( Emb_Man_t * p, int v ) { return p->pSols + v * p->nObjs; }
+static inline Emb_Dat_t * Emb_ManVec( Emb_Man_t * p, int v ) { return p->pVecs + v * p->nObjs; }
+static inline float * Emb_ManSol( Emb_Man_t * p, int v ) { return p->pSols + v * p->nObjs; }
#define Emb_ManForEachObj( p, pObj, i ) \
for ( i = 0; (i < p->nObjData) && (pObj = Emb_ManObj(p,i)); i += Emb_ObjSize(pObj) )
@@ -171,13 +177,13 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
p->nRegs = Gia_ManRegNum(pGia);
p->vCis = Vec_IntAlloc( Gia_ManCiNum(pGia) );
p->vCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );
- p->nObjData = (sizeof(Emb_Obj_t) / 4) * Gia_ManObjNum(pGia) + 2 * (2 * Gia_ManAndNum(pGia) + Gia_ManCoNum(pGia) + Gia_ManRegNum(pGia));
+ p->nObjData = (sizeof(Emb_Obj_t) / 4) * Gia_ManObjNum(pGia) + 2 * (2 * Gia_ManAndNum(pGia) + Gia_ManCoNum(pGia) + Gia_ManRegNum(pGia) + Gia_ManCoNum(pGia));
p->pObjData = ABC_CALLOC( int, p->nObjData );
// create constant node
Gia_ManConst0(pGia)->Value = hHandle;
pObjLog = Emb_ManObj( p, hHandle );
pObjLog->hHandle = hHandle;
- pObjLog->nFanins = 0;
+ pObjLog->nFanins = Gia_ManCoNum(pGia); //0;
pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) );
// count objects
hHandle += Emb_ObjSize( pObjLog );
@@ -227,7 +233,7 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
pObjLog = Emb_ManObj( p, hHandle );
pObjLog->hHandle = hHandle;
pObjLog->nFanins = 1;
- pObjLog->nFanouts = Gia_ObjIsRi( pGia, pObj );
+ pObjLog->nFanouts = 1 + Gia_ObjIsRi( pGia, pObj );
pObjLog->fCo = 1;
// add fanins
pFanLog = Emb_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
@@ -249,8 +255,8 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
if ( !~Gia_ObjValue(pObj) )
continue;
pObjLog = Emb_ManObj( p, Gia_ObjValue(pObj) );
- assert( pObjLog->nFanins == pObjLog->iFanin );
- assert( pObjLog->nFanouts == pObjLog->iFanout );
+ assert( pObjLog->nFanins == pObjLog->iFanin || Gia_ObjIsConst0(pObj) );
+ assert( pObjLog->nFanouts == pObjLog->iFanout || Gia_ObjIsCo(pObj) );
pObjLog->iFanin = pObjLog->iFanout = 0;
}
ABC_FREE( pGia->pRefs );
@@ -496,13 +502,13 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia )
p->nRegs = Gia_ManRegNum(pGia);
p->vCis = Vec_IntAlloc( Gia_ManCiNum(pGia) );
p->vCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );
- p->nObjData = (sizeof(Emb_Obj_t) / 4) * nObjs + 2 * (nFanios + Gia_ManRegNum(pGia));
+ p->nObjData = (sizeof(Emb_Obj_t) / 4) * nObjs + 2 * (nFanios + Gia_ManRegNum(pGia) + Gia_ManCoNum(pGia));
p->pObjData = ABC_CALLOC( int, p->nObjData );
// create constant node
Gia_ManConst0(pGia)->Value = hHandle;
pObjLog = Emb_ManObj( p, hHandle );
pObjLog->hHandle = hHandle;
- pObjLog->nFanins = 0;
+ pObjLog->nFanins = Gia_ManCoNum(pGia); //0;
pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) );
// count objects
hHandle += Emb_ObjSize( pObjLog );
@@ -563,7 +569,7 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia )
pObjLog = Emb_ManObj( p, hHandle );
pObjLog->hHandle = hHandle;
pObjLog->nFanins = 1;
- pObjLog->nFanouts = Gia_ObjIsRi( pGia, pObj );
+ pObjLog->nFanouts = 1 + Gia_ObjIsRi( pGia, pObj );
pObjLog->fCo = 1;
// add fanins
pFanLog = Emb_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
@@ -587,8 +593,8 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia )
if ( !~Gia_ObjValue(pObj) )
continue;
pObjLog = Emb_ManObj( p, Gia_ObjValue(pObj) );
- assert( pObjLog->nFanins == pObjLog->iFanin );
- assert( pObjLog->nFanouts == pObjLog->iFanout );
+ assert( pObjLog->nFanins == pObjLog->iFanin || Gia_ObjIsConst0(pObj) );
+ assert( pObjLog->nFanouts == pObjLog->iFanout || Gia_ObjIsCo(pObj) );
pObjLog->iFanin = pObjLog->iFanout = 0;
}
ABC_FREE( pGia->pRefs );
@@ -904,7 +910,7 @@ ABC_PRT( "Time", clock() - clk );
/**Function*************************************************************
- Synopsis [Computes the distances from the given set of objects.]
+ Synopsis [Perform BFS from the set of nodes.]
Description [Returns one of the most distant objects.]
@@ -913,20 +919,11 @@ ABC_PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
-Emb_Obj_t * Emb_ManFindDistances( Emb_Man_t * p, Vec_Int_t * vStart, Emb_Dat_t * pDist )
+Emb_Obj_t * Emb_ManPerformBfs( Emb_Man_t * p, Vec_Int_t * vThis, Vec_Int_t * vNext, Emb_Dat_t * pDist )
{
- Vec_Int_t * vThis, * vNext, * vTemp;
+ Vec_Int_t * vTemp;
Emb_Obj_t * pThis, * pNext, * pResult;
int i, k;
- p->nReached = p->nDistMax = 0;
- vThis = Vec_IntAlloc( 1000 );
- vNext = Vec_IntAlloc( 1000 );
- Emb_ManIncrementTravId( p );
- Emb_ManForEachObjVec( vStart, p, pThis, i )
- {
- Emb_ObjSetTravIdCurrent( p, pThis );
- Vec_IntPush( vThis, pThis->hHandle );
- }
assert( Vec_IntSize(vThis) > 0 );
for ( p->nDistMax = 0; Vec_IntSize(vThis) > 0; p->nDistMax++ )
{
@@ -955,6 +952,74 @@ Emb_Obj_t * Emb_ManFindDistances( Emb_Man_t * p, Vec_Int_t * vStart, Emb_Dat_t *
assert( Vec_IntSize(vNext) > 0 );
pResult = Emb_ManObj( p, Vec_IntEntry(vNext, 0) );
assert( pDist == NULL || pDist[pResult->Value] == p->nDistMax - 1 );
+ return pResult;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the distances from the given set of objects.]
+
+ Description [Returns one of the most distant objects.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Emb_ManConnectedComponents( Emb_Man_t * p )
+{
+ Gia_Obj_t * pObj;
+ Vec_Int_t * vThis, * vNext, * vResult;
+ Emb_Obj_t * pThis;
+ int i;
+ vResult = Vec_IntAlloc( 1000 );
+ vThis = Vec_IntAlloc( 1000 );
+ vNext = Vec_IntAlloc( 1000 );
+ p->nReached = 0;
+ Emb_ManIncrementTravId( p );
+ Gia_ManForEachCo( p->pGia, pObj, i )
+ {
+ pThis = Emb_ManObj( p, Gia_ObjValue(pObj) );
+ if ( Emb_ObjIsTravIdCurrent(p, pThis) )
+ continue;
+ Emb_ObjSetTravIdCurrent( p, pThis );
+ Vec_IntPush( vResult, pThis->hHandle );
+ // perform BFS from this node
+ Vec_IntClear( vThis );
+ Vec_IntPush( vThis, pThis->hHandle );
+ Emb_ManPerformBfs( p, vThis, vNext, NULL );
+ }
+ Vec_IntFree( vThis );
+ Vec_IntFree( vNext );
+ return vResult;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the distances from the given set of objects.]
+
+ Description [Returns one of the most distant objects.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Emb_Obj_t * Emb_ManFindDistances( Emb_Man_t * p, Vec_Int_t * vStart, Emb_Dat_t * pDist )
+{
+ Vec_Int_t * vThis, * vNext;
+ Emb_Obj_t * pThis, * pResult;
+ int i;
+ p->nReached = p->nDistMax = 0;
+ vThis = Vec_IntAlloc( 1000 );
+ vNext = Vec_IntAlloc( 1000 );
+ Emb_ManIncrementTravId( p );
+ Emb_ManForEachObjVec( vStart, p, pThis, i )
+ {
+ Emb_ObjSetTravIdCurrent( p, pThis );
+ Vec_IntPush( vThis, pThis->hHandle );
+ }
+ pResult = Emb_ManPerformBfs( p, vThis, vNext, pDist );
Vec_IntFree( vThis );
Vec_IntFree( vNext );
return pResult;
@@ -1029,13 +1094,28 @@ void Emb_DumpGraphIntoFile( Emb_Man_t * p )
void Emb_ManComputeDimensions( Emb_Man_t * p, int nDims )
{
Emb_Obj_t * pRandom, * pPivot;
- Vec_Int_t * vStart;
+ Vec_Int_t * vStart, * vComps;
int d, nReached;
- int i, Counter;
+ int i;//, Counter;
+ // connect unconnected components
+ vComps = Emb_ManConnectedComponents( p );
+// printf( "Components = %d. Considered %d objects (out of %d).\n", Vec_IntSize(vComps), p->nReached, Emb_ManObjNum(p) );
+ if ( Vec_IntSize(vComps) > 1 )
+ {
+ Emb_Obj_t * pFanin, * pObj = Emb_ManObj( p, 0 );
+ Emb_ManForEachObjVec( vComps, p, pFanin, i )
+ {
+ assert( Emb_ObjIsCo(pFanin) );
+ pFanin->Fanios[pFanin->nFanins + pFanin->nFanouts-1] =
+ pObj->Fanios[i] = pObj->hHandle - pFanin->hHandle;
+ }
+ }
+ Vec_IntFree( vComps );
+ // allocate memory for vectors
assert( p->pVecs == NULL );
- p->pVecs = ABC_ALLOC( Emb_Dat_t, p->nObjs * nDims );
- for ( i = 0; i < p->nObjs * nDims; i++ )
- p->pVecs[i] = ABC_INFINITY;
+ p->pVecs = ABC_CALLOC( Emb_Dat_t, p->nObjs * nDims );
+// for ( i = 0; i < p->nObjs * nDims; i++ )
+// p->pVecs[i] = ABC_INFINITY;
vStart = Vec_IntAlloc( nDims );
// get the pivot vertex
pRandom = Emb_ManRandomVertex( p );
@@ -1046,7 +1126,7 @@ void Emb_ManComputeDimensions( Emb_Man_t * p, int nDims )
nReached = p->nReached;
if ( nReached < Emb_ManObjNum(p) )
{
- printf( "Considering a connected component with %d objects (out of %d).\n", p->nReached, Emb_ManObjNum(p) );
+// printf( "Considering a connected component with %d objects (out of %d).\n", p->nReached, Emb_ManObjNum(p) );
}
// start dimensions with this vertex
Vec_IntClear( vStart );
@@ -1061,11 +1141,11 @@ void Emb_ManComputeDimensions( Emb_Man_t * p, int nDims )
}
Vec_IntFree( vStart );
// make sure the number of reached objects is correct
- Counter = 0;
- for ( i = 0; i < p->nObjs; i++ )
- if ( p->pVecs[i] < ABC_INFINITY )
- Counter++;
- assert( Counter == nReached );
+// Counter = 0;
+// for ( i = 0; i < p->nObjs; i++ )
+// if ( p->pVecs[i] < ABC_INFINITY )
+// Counter++;
+// assert( Counter == nReached );
}
/**Function*************************************************************
@@ -1338,7 +1418,6 @@ void Emb_ManComputeSolutions( Emb_Man_t * p, int nDims, int nSols )
***********************************************************************/
void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
{
- extern int * Gia_SortFloats( float * pArray, int nSize );
float * pY0, * pY1, Max0, Max1, Min0, Min1, Str0, Str1;
int * pPerm0, * pPerm1;
int k;
@@ -1373,10 +1452,10 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
pY1[k] = (pY1[k] != 0.0) ? ((pY1[k] - Min1) * Str1) : 0.0;
// derive the order of these numbers
- pPerm0 = Gia_SortFloats( pY0, p->nObjs );
- pPerm1 = Gia_SortFloats( pY1, p->nObjs );
+ pPerm0 = Gia_SortFloats( pY0, NULL, p->nObjs );
+ pPerm1 = Gia_SortFloats( pY1, NULL, p->nObjs );
- // average solutions and project them into 32K by 32K square
+ // average solutions and project them into square [0;0xffff] x [0;0xffff]
p->pPlacement = ABC_ALLOC( unsigned short, 2 * p->nObjs );
for ( k = 0; k < p->nObjs; k++ )
{
@@ -1387,6 +1466,127 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
ABC_FREE( pPerm1 );
}
+
+/**Function*************************************************************
+
+ Synopsis [Computes wire-length.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+double Emb_ManComputeHPWL( Emb_Man_t * p )
+{
+ double Result = 0.0;
+ Emb_Obj_t * pThis, * pNext;
+ int i, k, iMinX, iMaxX, iMinY, iMaxY;
+ if ( p->pPlacement == NULL )
+ return 0.0;
+ Emb_ManForEachObj( p, pThis, i )
+ {
+ iMinX = iMaxX = p->pPlacement[2*pThis->Value+0];
+ iMinY = iMaxY = p->pPlacement[2*pThis->Value+1];
+ Emb_ObjForEachFanout( pThis, pNext, k )
+ {
+ iMinX = ABC_MIN( iMinX, p->pPlacement[2*pNext->Value+0] );
+ iMaxX = ABC_MAX( iMaxX, p->pPlacement[2*pNext->Value+0] );
+ iMinY = ABC_MIN( iMinY, p->pPlacement[2*pNext->Value+1] );
+ iMaxY = ABC_MAX( iMaxY, p->pPlacement[2*pNext->Value+1] );
+ }
+ Result += (iMaxX - iMinX) + (iMaxY - iMinY);
+ }
+ return Result;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs iterative refinement of the given placement.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Emb_ManPlacementRefine( Emb_Man_t * p, int nIters, int fVerbose )
+{
+ Emb_Obj_t * pThis, * pNext;
+ double CostThis, CostPrev;
+ float * pEdgeX, * pEdgeY;
+ float * pVertX, * pVertY;
+ float VertX, VertY;
+ int * pPermX, * pPermY;
+ int i, k, Iter, iMinX, iMaxX, iMinY, iMaxY;
+ int clk = clock();
+ if ( p->pPlacement == NULL )
+ return;
+ pEdgeX = ABC_ALLOC( float, p->nObjs );
+ pEdgeY = ABC_ALLOC( float, p->nObjs );
+ pVertX = ABC_ALLOC( float, p->nObjs );
+ pVertY = ABC_ALLOC( float, p->nObjs );
+ // refine placement
+ CostPrev = 0.0;
+ for ( Iter = 0; Iter < nIters; Iter++ )
+ {
+ // compute centers of hyperedges
+ CostThis = 0.0;
+ Emb_ManForEachObj( p, pThis, i )
+ {
+ iMinX = iMaxX = p->pPlacement[2*pThis->Value+0];
+ iMinY = iMaxY = p->pPlacement[2*pThis->Value+1];
+ Emb_ObjForEachFanout( pThis, pNext, k )
+ {
+ iMinX = ABC_MIN( iMinX, p->pPlacement[2*pNext->Value+0] );
+ iMaxX = ABC_MAX( iMaxX, p->pPlacement[2*pNext->Value+0] );
+ iMinY = ABC_MIN( iMinY, p->pPlacement[2*pNext->Value+1] );
+ iMaxY = ABC_MAX( iMaxY, p->pPlacement[2*pNext->Value+1] );
+ }
+ pEdgeX[pThis->Value] = 0.5 * (iMaxX + iMinX);
+ pEdgeY[pThis->Value] = 0.5 * (iMaxY + iMinY);
+ CostThis += (iMaxX - iMinX) + (iMaxY - iMinY);
+ }
+ // compute new centers of objects
+ Emb_ManForEachObj( p, pThis, i )
+ {
+ VertX = pEdgeX[pThis->Value];
+ VertY = pEdgeY[pThis->Value];
+ Emb_ObjForEachFanin( pThis, pNext, k )
+ {
+ VertX += pEdgeX[pNext->Value];
+ VertY += pEdgeY[pNext->Value];
+ }
+ pVertX[pThis->Value] = VertX / (Emb_ObjFaninNum(pThis) + 1);
+ pVertY[pThis->Value] = VertY / (Emb_ObjFaninNum(pThis) + 1);
+ }
+ // sort these numbers
+ pPermX = Gia_SortFloats( pVertX, NULL, p->nObjs );
+ pPermY = Gia_SortFloats( pVertY, NULL, p->nObjs );
+ for ( k = 0; k < p->nObjs; k++ )
+ {
+ p->pPlacement[2*pPermX[k]+0] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
+ p->pPlacement[2*pPermY[k]+1] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
+ }
+ ABC_FREE( pPermX );
+ ABC_FREE( pPermY );
+ // evaluate cost
+ if ( fVerbose )
+ {
+ printf( "%2d : HPWL = %e ", Iter+1, CostThis );
+ ABC_PRT( "Time", clock() - clk );
+ }
+ }
+ ABC_FREE( pEdgeX );
+ ABC_FREE( pEdgeY );
+ ABC_FREE( pVertX );
+ ABC_FREE( pVertY );
+}
+
+
/**Function*************************************************************
Synopsis [Derives solutions from original vectors and eigenvectors.]
@@ -1413,6 +1613,68 @@ void Emb_ManPrintSolutions( Emb_Man_t * p, int nSols )
/**Function*************************************************************
+ Synopsis [Prepares image for dumping.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Emb_ManDumpGnuplotPrepare( Emb_Man_t * p )
+{
+// int nRows = 496;
+// int nCols = 710;
+ int nRows = 500;
+ int nCols = 700;
+ Vec_Int_t * vLines;
+ Emb_Obj_t * pThis;
+ char * pBuffer, ** ppRows;
+ int i, k, placeX, placeY;
+ int fStart;
+ // alloc memory
+ pBuffer = ABC_CALLOC( char, nRows * (nCols+1) );
+ ppRows = ABC_ALLOC( char *, nRows );
+ for ( i = 0; i < nRows; i++ )
+ ppRows[i] = pBuffer + i*(nCols+1);
+ // put data into them
+ Emb_ManForEachObj( p, pThis, i )
+ {
+ placeX = p->pPlacement[2*pThis->Value+0] * nCols / (1<<16);
+ placeY = p->pPlacement[2*pThis->Value+1] * nRows / (1<<16);
+ assert( placeX < nCols && placeY < nRows );
+ ppRows[placeY][placeX] = 1;
+ }
+ // select lines
+ vLines = Vec_IntAlloc( 1000 );
+ for ( i = 0; i < nRows; i++ )
+ {
+ fStart = 0;
+ for ( k = 0; k <= nCols; k++ )
+ {
+ if ( ppRows[i][k] && !fStart )
+ {
+ Vec_IntPush( vLines, k );
+ Vec_IntPush( vLines, i );
+ fStart = 1;
+ }
+ if ( !ppRows[i][k] && fStart )
+ {
+ Vec_IntPush( vLines, k-1 );
+ Vec_IntPush( vLines, i );
+ fStart = 0;
+ }
+ }
+ assert( fStart == 0 );
+ }
+ ABC_FREE( pBuffer );
+ ABC_FREE( ppRows );
+ return vLines;
+}
+
+/**Function*************************************************************
+
Synopsis [Derives solutions from original vectors and eigenvectors.]
Description []
@@ -1422,71 +1684,89 @@ void Emb_ManPrintSolutions( Emb_Man_t * p, int nSols )
SeeAlso []
***********************************************************************/
-void Emb_ManDumpGnuplot( Emb_Man_t * p, int nSols, char * pName )
+void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowImage )
{
- int fDumpImage = 1;
+ extern void Gia_ManGnuplotShow( char * pPlotFileName );
// char * pDirectory = "place\\";
char * pDirectory = "";
extern char * Ioa_TimeStamp();
FILE * pFile;
char Buffer[1000];
Emb_Obj_t * pThis, * pNext;
- float * pSol0, * pSol1;
int i, k;
- if ( nSols < 2 )
- return;
if ( p->pPlacement == NULL )
{
printf( "Emb_ManDumpGnuplot(): Placement is not available.\n" );
return;
}
- pSol0 = Emb_ManSol( p, 0 );
- pSol1 = Emb_ManSol( p, 1 );
sprintf( Buffer, "%s%s", pDirectory, Aig_FileNameGenericAppend(pName, ".plt") );
pFile = fopen( Buffer, "w" );
fprintf( pFile, "# This Gnuplot file was produced by ABC on %s\n", Ioa_TimeStamp() );
fprintf( pFile, "\n" );
- if ( fDumpImage )
- {
fprintf( pFile, "set nokey\n" );
+ fprintf( pFile, "\n" );
+ if ( !fShowImage )
+ {
// fprintf( pFile, "set terminal postscript\n" );
-// fprintf( pFile, "set output \'%s\'\n", Aig_FileNameGenericAppend(pName, ".ps") );
fprintf( pFile, "set terminal gif font \'arial\' 10 size 800,600 xffffff x000000 x000000 x000000\n" );
fprintf( pFile, "set output \'%s\'\n", Aig_FileNameGenericAppend(pName, ".gif") );
fprintf( pFile, "\n" );
}
- fprintf( pFile, "set title \"%s : PI = %d PO = %d FF = %d Node = %d Obj = %d\\n",
- pName, Emb_ManPiNum(p), Emb_ManPoNum(p), Emb_ManRegNum(p), Emb_ManNodeNum(p), Emb_ManObjNum(p) );
+ fprintf( pFile, "set title \"%s : PI = %d PO = %d FF = %d Node = %d Obj = %d HPWL = %.2e\\n",
+ pName, Emb_ManPiNum(p), Emb_ManPoNum(p), Emb_ManRegNum(p), Emb_ManNodeNum(p), Emb_ManObjNum(p), Emb_ManComputeHPWL(p) );
fprintf( pFile, "(image generated by ABC and Gnuplot on %s)\"", Ioa_TimeStamp() );
fprintf( pFile, "font \"Times, 12\"\n" );
fprintf( pFile, "\n" );
fprintf( pFile, "plot [:] '-' w l\n" );
fprintf( pFile, "\n" );
- Emb_ManForEachObj( p, pThis, i )
+ if ( fDumpLarge )
{
- if ( !Emb_ObjIsTravIdCurrent(p, pThis) )
- continue;
- Emb_ObjForEachFanout( pThis, pNext, k )
+ int begX, begY, endX, endY;
+ Vec_Int_t * vLines = Emb_ManDumpGnuplotPrepare( p );
+ Vec_IntForEachEntry( vLines, begX, i )
{
- assert( Emb_ObjIsTravIdCurrent(p, pNext) );
-// fprintf( pFile, "%d %d\n", (int)pSol0[pThis->Value], (int)pSol1[pThis->Value] );
-// fprintf( pFile, "%d %d\n", (int)pSol0[pNext->Value], (int)pSol1[pNext->Value] );
-// fprintf( pFile, "%5.2f %5.2f\n", pSol0[pThis->Value], pSol1[pThis->Value] );
-// fprintf( pFile, "%5.2f %5.2f\n", pSol0[pNext->Value], pSol1[pNext->Value] );
- fprintf( pFile, "%5d %5d\n", p->pPlacement[2*pThis->Value+0], p->pPlacement[2*pThis->Value+1] );
- fprintf( pFile, "%5d %5d\n", p->pPlacement[2*pNext->Value+0], p->pPlacement[2*pNext->Value+1] );
+ begY = Vec_IntEntry( vLines, i+1 );
+ endX = Vec_IntEntry( vLines, i+2 );
+ endY = Vec_IntEntry( vLines, i+3 );
+ i += 3;
+ fprintf( pFile, "%5d %5d\n", begX, begY );
+ fprintf( pFile, "%5d %5d\n", endX, endY );
fprintf( pFile, "\n" );
}
+ Vec_IntFree( vLines );
+ }
+ else
+ {
+ Emb_ManForEachObj( p, pThis, i )
+ {
+ if ( !Emb_ObjIsTravIdCurrent(p, pThis) )
+ continue;
+ Emb_ObjForEachFanout( pThis, pNext, k )
+ {
+ assert( Emb_ObjIsTravIdCurrent(p, pNext) );
+ fprintf( pFile, "%5d %5d\n", p->pPlacement[2*pThis->Value+0], p->pPlacement[2*pThis->Value+1] );
+ fprintf( pFile, "%5d %5d\n", p->pPlacement[2*pNext->Value+0], p->pPlacement[2*pNext->Value+1] );
+ fprintf( pFile, "\n" );
+ }
+ }
}
fprintf( pFile, "EOF\n" );
fprintf( pFile, "\n" );
- if ( !fDumpImage )
+ if ( fShowImage )
{
- fprintf( pFile, "pause -1 \"Hit return to continue\"\n" );
+ fprintf( pFile, "pause -1 \"Close window\"\n" ); // Hit return to continue
fprintf( pFile, "reset\n" );
fprintf( pFile, "\n" );
}
+ else
+ {
+ fprintf( pFile, "# pause -1 \"Close window\"\n" ); // Hit return to continue
+ fprintf( pFile, "# reset\n" );
+ fprintf( pFile, "\n" );
+ }
fclose( pFile );
+ if ( fShowImage )
+ Gia_ManGnuplotShow( Buffer );
}
/**Function*************************************************************
@@ -1500,7 +1780,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, int nSols, char * pName )
SeeAlso []
***********************************************************************/
-void Gia_ManSolveProblem( Gia_Man_t * pGia, int nDims, int nSols, int fCluster, int fDump, int fVerbose )
+void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars )
{
Emb_Man_t * p;
int clk, clkSetup;
@@ -1508,18 +1788,18 @@ void Gia_ManSolveProblem( Gia_Man_t * pGia, int nDims, int nSols, int fCluster,
// transform AIG into internal data-structure
clk = clock();
- if ( fCluster )
+ if ( pPars->fCluster )
{
p = Emb_ManStart( pGia );
- if ( fVerbose )
+ if ( pPars->fVerbose )
{
- printf( "After clustering: " );
+ printf( "Clustered: " );
Emb_ManPrintStats( p );
}
}
else
p = Emb_ManStartSimple( pGia );
- p->fVerbose = fVerbose;
+ p->fVerbose = pPars->fVerbose;
// Emb_ManPrintFanio( p );
// prepare data-structure
@@ -1529,26 +1809,40 @@ clk = clock();
clkSetup = clock() - clk;
clk = clock();
- Emb_ManComputeDimensions( p, nDims );
-if ( fVerbose )
+ Emb_ManComputeDimensions( p, pPars->nDims );
+if ( pPars->fVerbose )
ABC_PRT( "Setup ", clkSetup );
-if ( fVerbose )
+if ( pPars->fVerbose )
ABC_PRT( "Dimensions", clock() - clk );
clk = clock();
- Emb_ManComputeCovariance( p, nDims );
-if ( fVerbose )
+ Emb_ManComputeCovariance( p, pPars->nDims );
+if ( pPars->fVerbose )
ABC_PRT( "Matrix ", clock() - clk );
clk = clock();
- Emb_ManComputeEigenvectors( p, nDims, nSols );
- Emb_ManComputeSolutions( p, nDims, nSols );
- Emb_ManDerivePlacement( p, nSols );
-if ( fVerbose )
+ Emb_ManComputeEigenvectors( p, pPars->nDims, pPars->nSols );
+ Emb_ManComputeSolutions( p, pPars->nDims, pPars->nSols );
+ Emb_ManDerivePlacement( p, pPars->nSols );
+if ( pPars->fVerbose )
ABC_PRT( "Eigenvecs ", clock() - clk );
- if ( fDump )
- Emb_ManDumpGnuplot( p, nSols, pGia->pName );
+ if ( pPars->fRefine )
+ {
+clk = clock();
+ Emb_ManPlacementRefine( p, pPars->nIters, pPars->fVerbose );
+if ( pPars->fVerbose )
+ABC_PRT( "Refinement", clock() - clk );
+ }
+
+ if ( (pPars->fDump || pPars->fDumpLarge) && pPars->nSols == 2 )
+ {
+clk = clock();
+ Emb_ManDumpGnuplot( p, pGia->pName, pPars->fDumpLarge, pPars->fShowImage );
+if ( pPars->fVerbose )
+ABC_PRT( "Image dump", clock() - clk );
+ }
+
Emb_ManStop( p );
}
diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c
new file mode 100644
index 00000000..d05dc5a9
--- /dev/null
+++ b/src/aig/gia/giaEnable.c
@@ -0,0 +1,210 @@
+/**CFile****************************************************************
+
+ FileName [gia.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [Structural detection of enables, sets and resets.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Collects the supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_CollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
+{
+ // if the new node is complemented or a PI, another gate begins
+ if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) )
+ {
+ Vec_IntPushUnique( vSuper, Gia_ObjId(p, Gia_Regular(pObj)) );
+ return;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
+ // go through the branches
+ Gia_CollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
+ Gia_CollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_CollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
+{
+ assert( !Gia_IsComplement(pObj) );
+ Vec_IntClear( vSuper );
+// Gia_CollectSuper_rec( p, pObj, vSuper );
+ if ( Gia_ObjIsAnd(pObj) )
+ {
+ Vec_IntPushUnique( vSuper, Gia_ObjId(p, Gia_ObjFanin0(pObj)) );
+ Vec_IntPushUnique( vSuper, Gia_ObjId(p, Gia_ObjFanin1(pObj)) );
+ }
+ else
+ Vec_IntPushUnique( vSuper, Gia_ObjId(p, Gia_Regular(pObj)) );
+
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManPrintSignals( Gia_Man_t * p, int * pFreq, char * pStr )
+{
+ Vec_Int_t * vObjs;
+ int i, Counter = 0, nTotal = 0;
+ vObjs = Vec_IntAlloc( 100 );
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ if ( pFreq[i] > 1 )
+ {
+ nTotal += pFreq[i];
+ Counter++;
+ }
+ printf( "%s (total = %d driven = %d)\n", pStr, Counter, nTotal );
+ Counter = 0;
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ if ( pFreq[i] > 1 )
+ {
+ printf( "%3d : Obj = %6d Refs = %6d Freq = %6d\n",
+ ++Counter, i, Gia_ObjRefs(p, Gia_ManObj(p,i)), pFreq[i] );
+ Vec_IntPush( vObjs, i );
+ }
+ Vec_IntFree( vObjs );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset )
+{
+ 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 );
+ Gia_ManCreateRefs( p );
+ printf( "Flops with set/reset = %6d. Flops with enable = %6d.\n", nHaveSetReset, nHaveEnable );
+ if ( fSetReset )
+ {
+ Gia_ManPrintSignals( p, pSets, "Set signals" );
+ Gia_ManPrintSignals( p, pResets, "Reset signals" );
+ }
+ Gia_ManPrintSignals( p, pEnables, "Enable signals" );
+ ABC_FREE( p->pRefs );
+ ABC_FREE( pSets );
+ ABC_FREE( pResets );
+ ABC_FREE( pEnables );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
new file mode 100644
index 00000000..9e190da3
--- /dev/null
+++ b/src/aig/gia/giaEquiv.c
@@ -0,0 +1,618 @@
+/**CFile****************************************************************
+
+ FileName [giaEquiv.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [Manipulation of equivalence classes.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaEquiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Given representatives, derives pointers to the next objects.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Gia_ManDeriveNexts( Gia_Man_t * p )
+{
+ unsigned * pNexts, * pTails;
+ int i;
+ assert( p->pReprs );
+ pNexts = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
+ pTails = ABC_ALLOC( unsigned, Gia_ManObjNum(p) );
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ pTails[i] = i;
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ {
+ if ( !p->pReprs[i].iRepr || p->pReprs[i].iRepr == GIA_VOID )
+ continue;
+ pNexts[ pTails[p->pReprs[i].iRepr] ] = i;
+ pTails[p->pReprs[i].iRepr] = i;
+ }
+ ABC_FREE( pTails );
+ return (int *)pNexts;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManEquivCountOne( Gia_Man_t * p, int i )
+{
+ int Ent, nLits = 1;
+ Gia_ClassForEachObj1( p, i, Ent )
+ {
+ assert( Gia_ObjRepr(p, Ent) == i );
+ nLits++;
+ }
+ return nLits;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter )
+{
+ int Ent;
+ printf( "Class %4d : Num = %2d {", Counter, Gia_ManEquivCountOne(p, i) );
+ Gia_ClassForEachObj( p, i, Ent )
+ {
+ printf(" %d", Ent );
+ if ( p->pReprs[Ent].fColorA || p->pReprs[Ent].fColorB )
+ printf(" <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB );
+ }
+ printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManEquivCountLitsAll( Gia_Man_t * p )
+{
+ int i, nLits = 0;
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ nLits += (Gia_ObjRepr(p, i) != GIA_VOID);
+ return nLits;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
+{
+ int nLitsReal = Gia_ManEquivCountLitsAll( p );
+ if ( nLitsReal != nLits )
+ printf( "Detected a mismatch in counting equivalence classes (%d).\n", nLitsReal - nLits );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
+{
+ int i, Counter = 0, Counter1 = 0, CounterX = 0, Proved = 0, nLits;
+ for ( i = 1; i < Gia_ManObjNum(p); i++ )
+ {
+ if ( Gia_ObjIsHead(p, i) )
+ Counter++;
+ else if ( Gia_ObjIsConst(p, i) )
+ Counter1++;
+ else if ( Gia_ObjIsNone(p, i) )
+ CounterX++;
+ if ( Gia_ObjProved(p, i) )
+ Proved++;
+ }
+ CounterX -= Gia_ManCoNum(p);
+ nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
+ printf( "cls =%7d cst =%8d lit =%8d unused =%8d proof =%6d mem =%5.2f Mb\n",
+ Counter, Counter1, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
+ assert( Gia_ManEquivCheckLits( p, nLits ) );
+ if ( fVerbose )
+ {
+ Counter = 0;
+ Gia_ManForEachClass( p, i )
+ Gia_ManEquivPrintOne( p, i, ++Counter );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns representative node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
+ return NULL;
+ return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ Gia_Obj_t * pRepr;
+ if ( ~pObj->Value )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ if ( (pRepr = Gia_ManEquivRepr(p, pObj)) )
+ {
+ Gia_ManEquivReduce_rec( pNew, p, pRepr );
+ pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+ return;
+ }
+ Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reduces AIG using equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj, * pRepr;
+ int i;
+ Gia_ManSetPhase( p );
+ 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);
+ if ( (pRepr = Gia_ManEquivRepr(p, pObj)) )
+ pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+ }
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachCo( p, pObj, i )
+ Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManForEachCo( p, pObj, i )
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManHashStop( pNew );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reduces AIG using equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManEquivFixOutputPairs( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj0, * pObj1;
+ int i;
+ assert( (Gia_ManPoNum(p) & 1) == 0 );
+ Gia_ManForEachPo( p, pObj0, i )
+ {
+ pObj1 = Gia_ManPo( p, ++i );
+ if ( Gia_ObjChild0(pObj0) != Gia_ObjChild0(pObj1) )
+ continue;
+ pObj0->iDiff0 = Gia_ObjId(p, pObj0);
+ pObj0->fCompl0 = 0;
+ pObj1->iDiff0 = Gia_ObjId(p, pObj1);
+ pObj1->fCompl0 = 0;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes pointers to the unmarked nodes..]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManEquivUpdatePointers( Gia_Man_t * p, Gia_Man_t * pNew )
+{
+ Gia_Obj_t * pObj, * pObjNew;
+ int i;
+ Gia_ManForEachObj( p, pObj, i )
+ {
+ if ( !~pObj->Value )
+ continue;
+ pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
+ if ( pObjNew->fMark0 )
+ pObj->Value = ~0;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes pointers to the unmarked nodes..]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFinal )
+{
+ Vec_Int_t * vClass;
+ Gia_Obj_t * pObj, * pObjNew;
+ int i, k, iNode, iRepr, iPrev;
+ // start representatives
+ pFinal->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pFinal) );
+ for ( i = 0; i < Gia_ManObjNum(pFinal); i++ )
+ Gia_ObjSetRepr( pFinal, i, GIA_VOID );
+ // iterate over constant candidates
+ Gia_ManForEachConst( p, i )
+ {
+ pObj = Gia_ManObj( p, i );
+ if ( !~pObj->Value )
+ continue;
+ pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
+ if ( Gia_Lit2Var(pObjNew->Value) == 0 )
+ continue;
+ Gia_ObjSetRepr( pFinal, Gia_Lit2Var(pObjNew->Value), 0 );
+ }
+ // iterate over class candidates
+ vClass = Vec_IntAlloc( 100 );
+ Gia_ManForEachClass( p, i )
+ {
+ Vec_IntClear( vClass );
+ Gia_ClassForEachObj( p, i, k )
+ {
+ pObj = Gia_ManObj( p, k );
+ if ( !~pObj->Value )
+ continue;
+ pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
+ Vec_IntPushUnique( vClass, Gia_Lit2Var(pObjNew->Value) );
+ }
+ if ( Vec_IntSize( vClass ) < 2 )
+ continue;
+ Vec_IntSort( vClass, 0 );
+ iRepr = iPrev = Vec_IntEntry( vClass, 0 );
+ Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
+ {
+ Gia_ObjSetRepr( pFinal, iNode, iRepr );
+ assert( iPrev < iNode );
+ iPrev = iNode;
+ }
+ }
+ Vec_IntFree( vClass );
+ pFinal->pNexts = Gia_ManDeriveNexts( pFinal );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reduces AIG while remapping equivalence classes.]
+
+ Description [Drops the pairs of outputs if they are proved equivalent.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs )
+{
+ Gia_Man_t * pNew, * pFinal;
+ pNew = Gia_ManEquivReduce( p );
+ if ( fMiterPairs )
+ Gia_ManEquivFixOutputPairs( pNew );
+ if ( fSeq )
+ Gia_ManSeqMarkUsed( pNew );
+ else
+ Gia_ManCombMarkUsed( pNew );
+ Gia_ManEquivUpdatePointers( p, pNew );
+ pFinal = Gia_ManDupMarked( pNew );
+ Gia_ManEquivDeriveReprs( p, pNew, pFinal );
+ Gia_ManStop( pNew );
+ return pFinal;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks CIs/COs/ANDs unreachable from POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManEquivSetColor_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fOdds )
+{
+ if ( Gia_ObjVisitColor( p, Gia_ObjId(p,pObj), fOdds ) )
+ return 0;
+ if ( Gia_ObjIsRo(p, pObj) )
+ return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p, pObj)), fOdds );
+ assert( Gia_ObjIsAnd(pObj) );
+ return 1 + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), fOdds )
+ + Gia_ManEquivSetColor_rec( p, Gia_ObjFanin1(pObj), fOdds );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks CIs/COs/ANDs unreachable from POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
+{
+ Gia_Obj_t * pObj;
+ int i, nNodes[2] = {0,0}, nDiffs[2];
+ assert( (Gia_ManPoNum(p) & 1) == 0 );
+ Gia_ObjSetColors( p, 0 );
+ Gia_ManForEachPi( p, pObj, i )
+ Gia_ObjSetColors( p, Gia_ObjId(p,pObj) );
+ Gia_ManForEachPo( p, pObj, i )
+ nNodes[i&1] += Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), i&1 );
+// Gia_ManForEachObj( p, pObj, i )
+// if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) )
+// assert( Gia_ObjColors(p, i) );
+ nDiffs[0] = Gia_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[0]);
+ nDiffs[1] = Gia_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[1]);
+ if ( fVerbose )
+ {
+ printf( "CI+AND = %7d A = %7d B = %7d Ad = %7d Bd = %7d AB = %7d.\n",
+ Gia_ManCiNum(p) + Gia_ManAndNum(p),
+ Gia_ManPiNum(p) + nNodes[0], Gia_ManPiNum(p) + nNodes[1],
+ nDiffs[0], nDiffs[1],
+ Gia_ManCiNum(p) + Gia_ManAndNum(p) - nDiffs[0] - nDiffs[1] );
+ }
+ return (nDiffs[0] + nDiffs[1]) / 2;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits )
+{
+ Gia_Obj_t * pRepr;
+ int iLitNew;
+ if ( ~pObj->Value )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits );
+ Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits );
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+ if ( pRepr == NULL )
+ return;
+ iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+ if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
+ Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
+ pObj->Value = iLitNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reduces AIG using equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj, * pRepr;
+ Vec_Int_t * vXorLits;
+ int i, iLitNew;
+ if ( !p->pReprs )
+ return NULL;
+ vXorLits = Vec_IntAlloc( 1000 );
+ Gia_ManSetPhase( p );
+ 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_ManHashAlloc( pNew );
+ Gia_ManForEachCi( p, pObj, i )
+ {
+ pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+ if ( pRepr == NULL )
+ continue;
+ iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+ if ( pObj->Value != (unsigned)iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
+ Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
+ pObj->Value = iLitNew;
+ }
+ Gia_ManForEachCo( p, pObj, i )
+ Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits );
+ Vec_IntForEachEntry( vXorLits, iLitNew, i )
+ Gia_ManAppendCo( pNew, iLitNew );
+ if ( Vec_IntSize(vXorLits) == 0 )
+ {
+ printf( "Speculatively reduced model has no primary outputs.\n" );
+ Gia_ManAppendCo( pNew, 0 );
+ }
+ Gia_ManForEachRi( p, pObj, i )
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Vec_IntFree( vXorLits );
+ Gia_ManHashStop( pNew );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms equiv classes by removing the AB nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose )
+{
+ extern void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass );
+ Vec_Int_t * vClass, * vClassNew;
+ int iRepr, iNode, Ent, k;
+ int nRemovedLits = 0, nRemovedClas = 0;
+ int nTotalLits = 0, nTotalClas = 0;
+ Gia_Obj_t * pObj;
+ int i;
+ assert( p->pReprs && p->pNexts );
+ vClass = Vec_IntAlloc( 100 );
+ vClassNew = Vec_IntAlloc( 100 );
+ Gia_ManForEachObj( p, pObj, i )
+ if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) )
+ assert( Gia_ObjColors(p, i) );
+ Gia_ManForEachClassReverse( p, iRepr )
+ {
+ nTotalClas++;
+ Vec_IntClear( vClass );
+ Vec_IntClear( vClassNew );
+ Gia_ClassForEachObj( p, iRepr, iNode )
+ {
+ nTotalLits++;
+ Vec_IntPush( vClass, iNode );
+ assert( Gia_ObjColors(p, iNode) );
+ if ( Gia_ObjColors(p, iNode) != 3 )
+ Vec_IntPush( vClassNew, iNode );
+ else
+ nRemovedLits++;
+ }
+ Vec_IntForEachEntry( vClass, Ent, k )
+ {
+ p->pReprs[Ent].fFailed = p->pReprs[Ent].fProved = 0;
+ p->pReprs[Ent].iRepr = GIA_VOID;
+ p->pNexts[Ent] = 0;
+ }
+ if ( Vec_IntSize(vClassNew) < 2 )
+ {
+ nRemovedClas++;
+ continue;
+ }
+ Cec_ManSimClassCreate( p, vClassNew );
+ }
+ Vec_IntFree( vClass );
+ Vec_IntFree( vClassNew );
+ if ( fVerbose )
+ printf( "Removed classes = %6d (out of %6d). Removed literals = %6d (out of %6d).\n",
+ nRemovedClas, nTotalClas, nRemovedLits, nTotalLits );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c
index c2d2d33f..cf4c4aa5 100644
--- a/src/aig/gia/giaForce.c
+++ b/src/aig/gia/giaForce.c
@@ -23,47 +23,100 @@
/*
The code is based on the paper by F. A. Aloul, I. L. Markov, and K. A. Sakallah.
"FORCE: A Fast and Easy-To-Implement Variable-Ordering Heuristic", Proc. GLSVLSI’03.
+ http://www.eecs.umich.edu/~imarkov/pubs/conf/glsvlsi03-force.pdf
*/
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-typedef struct For_Obj_t_ For_Obj_t;
-struct For_Obj_t_
+typedef struct Frc_Obj_t_ Frc_Obj_t;
+struct Frc_Obj_t_
{
- int iObj;
- float lNode;
+ unsigned fCi : 1; // terminal node CI
+ unsigned fCo : 1; // terminal node CO
+ unsigned fMark0 : 1; // first user-controlled mark
+ unsigned fMark1 : 1; // second user-controlled mark
+ unsigned nFanins : 28; // the number of fanins
+ unsigned nFanouts; // the number of fanouts
+ unsigned iFanout; // the current number of fanouts
+ int hHandle; // the handle of the node
+ int pPlace; // the placement of each node
+ union {
+ float fEdgeCenter; // center-of-gravity of the edge
+ unsigned iFanin;
+ };
+ int Fanios[0]; // the array of fanins/fanouts
};
-typedef struct For_Man_t_ For_Man_t;
-struct For_Man_t_
+typedef struct Frc_Man_t_ Frc_Man_t;
+struct Frc_Man_t_
{
Gia_Man_t * pGia; // the original AIG manager
+ Vec_Int_t * vCis; // the vector of CIs (PIs + LOs)
+ Vec_Int_t * vCos; // the vector of COs (POs + LIs)
int nObjs; // the number of objects
- int iObj; // the last added object
- int * pPlace; // coordinates of objects
- int * piNext; // array of next pointers
- int * piRoot; // array of root pointers
- float * plEdge; // edge coordinates
- For_Obj_t * pNodes; // the array of nodes
+ int nRegs; // the number of registers
+ int * pObjData; // the array containing data for objects
+ int nObjData; // the size of array to store the logic network
+ int fVerbose; // verbose output flag
+ int nCutCur; // current cut
+ int nCutMax; // max cut seen
};
-static inline int Gia_ObjPlace( For_Man_t * p, Gia_Obj_t * pObj ) { return p->pPlace[Gia_ObjId(p->pGia, pObj)]; }
-static inline int Gia_ObjPlaceFanin0( For_Man_t * p, Gia_Obj_t * pObj ) { return p->pPlace[Gia_ObjFaninId0p(p->pGia, pObj)]; }
-static inline int Gia_ObjPlaceFanin1( For_Man_t * p, Gia_Obj_t * pObj ) { return p->pPlace[Gia_ObjFaninId1p(p->pGia, pObj)]; }
-
-static inline int Gia_ObjEdge( For_Man_t * p, Gia_Obj_t * pObj ) { return p->plEdge[Gia_ObjId(p->pGia, pObj)]; }
-static inline int Gia_ObjEdgeFanin0( For_Man_t * p, Gia_Obj_t * pObj ) { return p->plEdge[Gia_ObjFaninId0p(p->pGia, pObj)]; }
-static inline int Gia_ObjEdgeFanin1( For_Man_t * p, Gia_Obj_t * pObj ) { return p->plEdge[Gia_ObjFaninId1p(p->pGia, pObj)]; }
+static inline int Frc_ManRegNum( Frc_Man_t * p ) { return p->nRegs; }
+static inline int Frc_ManCiNum( Frc_Man_t * p ) { return Vec_IntSize(p->vCis); }
+static inline int Frc_ManCoNum( Frc_Man_t * p ) { return Vec_IntSize(p->vCos); }
+static inline int Frc_ManPiNum( Frc_Man_t * p ) { return Vec_IntSize(p->vCis) - p->nRegs; }
+static inline int Frc_ManPoNum( Frc_Man_t * p ) { return Vec_IntSize(p->vCos) - p->nRegs; }
+static inline int Frc_ManObjNum( Frc_Man_t * p ) { return p->nObjs; }
+static inline int Frc_ManNodeNum( Frc_Man_t * p ) { return p->nObjs - Vec_IntSize(p->vCis) - Vec_IntSize(p->vCos); }
+
+static inline Frc_Obj_t * Frc_ManObj( Frc_Man_t * p, int hHandle ) { return (Frc_Obj_t *)(p->pObjData + hHandle); }
+static inline Frc_Obj_t * Frc_ManCi( Frc_Man_t * p, int i ) { return Frc_ManObj( p, Vec_IntEntry(p->vCis,i) ); }
+static inline Frc_Obj_t * Frc_ManCo( Frc_Man_t * p, int i ) { return Frc_ManObj( p, Vec_IntEntry(p->vCos,i) ); }
+
+static inline int Frc_ObjIsTerm( Frc_Obj_t * pObj ) { return pObj->fCi || pObj->fCo; }
+static inline int Frc_ObjIsCi( Frc_Obj_t * pObj ) { return pObj->fCi; }
+static inline int Frc_ObjIsCo( Frc_Obj_t * pObj ) { return pObj->fCo; }
+static inline int Frc_ObjIsPi( Frc_Obj_t * pObj ) { return pObj->fCi && pObj->nFanins == 0; }
+static inline int Frc_ObjIsPo( Frc_Obj_t * pObj ) { return pObj->fCo && pObj->nFanouts == 0; }
+static inline int Frc_ObjIsNode( Frc_Obj_t * pObj ) { return!Frc_ObjIsTerm(pObj) && pObj->nFanins > 0; }
+static inline int Frc_ObjIsConst0( Frc_Obj_t * pObj ) { return!Frc_ObjIsTerm(pObj) && pObj->nFanins == 0; }
+
+static inline int Frc_ObjSize( Frc_Obj_t * pObj ) { return sizeof(Frc_Obj_t) / 4 + pObj->nFanins + pObj->nFanouts; }
+static inline int Frc_ObjFaninNum( Frc_Obj_t * pObj ) { return pObj->nFanins; }
+static inline int Frc_ObjFanoutNum( Frc_Obj_t * pObj ) { return pObj->nFanouts; }
+static inline Frc_Obj_t * Frc_ObjFanin( Frc_Obj_t * pObj, int i ) { return (Frc_Obj_t *)(((int *)pObj) - pObj->Fanios[i]); }
+static inline Frc_Obj_t * Frc_ObjFanout( Frc_Obj_t * pObj, int i ) { return (Frc_Obj_t *)(((int *)pObj) + pObj->Fanios[pObj->nFanins+i]); }
+
+#define Frc_ManForEachObj( p, pObj, i ) \
+ for ( i = 0; (i < p->nObjData) && (pObj = Frc_ManObj(p,i)); i += Frc_ObjSize(pObj) )
+#define Frc_ManForEachObjVec( vVec, p, pObj, i ) \
+ for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Frc_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
+
+#define Frc_ManForEachNode( p, pObj, i ) \
+ for ( i = 0; (i < p->nObjData) && (pObj = Frc_ManObj(p,i)); i += Frc_ObjSize(pObj) ) if ( Frc_ObjIsTerm(pObj) ) {} else
+#define Frc_ManForEachCi( p, pObj, i ) \
+ for ( i = 0; (i < Vec_IntSize(p->vCis)) && (pObj = Frc_ManObj(p,Vec_IntEntry(p->vCis,i))); i++ )
+#define Frc_ManForEachCo( p, pObj, i ) \
+ for ( i = 0; (i < Vec_IntSize(p->vCos)) && (pObj = Frc_ManObj(p,Vec_IntEntry(p->vCos,i))); i++ )
+
+#define Frc_ObjForEachFanin( pObj, pNext, i ) \
+ for ( i = 0; (i < (int)pObj->nFanins) && (pNext = Frc_ObjFanin(pObj,i)); i++ )
+#define Frc_ObjForEachFaninReverse( pObj, pNext, i ) \
+ for ( i = (int)pObj->nFanins - 1; (i >= 0) && (pNext = Frc_ObjFanin(pObj,i)); i-- )
+#define Frc_ObjForEachFanout( pObj, pNext, i ) \
+ for ( i = 0; (i < (int)pObj->nFanouts) && (pNext = Frc_ObjFanout(pObj,i)); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+
/**Function*************************************************************
- Synopsis []
+ Synopsis [Creates fanin/fanout pair.]
Description []
@@ -72,23 +125,128 @@ static inline int Gia_ObjEdgeFanin1( For_Man_t * p, Gia_Obj_t * pObj ) { retu
SeeAlso []
***********************************************************************/
-For_Man_t * For_ManStart( Gia_Man_t * pGia )
+void Frc_ObjAddFanin( Frc_Obj_t * pObj, Frc_Obj_t * pFanin )
+{
+ assert( pObj->iFanin < pObj->nFanins );
+ assert( pFanin->iFanout < pFanin->nFanouts );
+ pFanin->Fanios[pFanin->nFanins + pFanin->iFanout++] =
+ pObj->Fanios[pObj->iFanin++] = pObj->hHandle - pFanin->hHandle;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates logic network isomorphic to the given AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Frc_Man_t * Frc_ManStartSimple( Gia_Man_t * pGia )
{
- For_Man_t * p;
- p = ABC_CALLOC( For_Man_t, 1 );
- p->pGia = pGia;
- p->nObjs = Gia_ManObjNum(pGia);
- p->pPlace = ABC_ALLOC( int, p->nObjs );
- p->piNext = ABC_ALLOC( int, p->nObjs );
- p->piRoot = ABC_ALLOC( int, p->nObjs );
- p->plEdge = ABC_ALLOC( float, p->nObjs );
- p->pNodes = ABC_ALLOC( For_Obj_t, p->nObjs );
+ Frc_Man_t * p;
+ Frc_Obj_t * pObjLog, * pFanLog;
+ Gia_Obj_t * pObj;//, * pObjRi, * pObjRo;
+ int i, nNodes, hHandle = 0;
+ // prepare the AIG
+ Gia_ManCreateRefs( pGia );
+ // create logic network
+ p = ABC_CALLOC( Frc_Man_t, 1 );
+ p->pGia = pGia;
+ p->nRegs = Gia_ManRegNum(pGia);
+ p->vCis = Vec_IntAlloc( Gia_ManCiNum(pGia) );
+ p->vCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );
+ p->nObjData = (sizeof(Frc_Obj_t) / 4) * Gia_ManObjNum(pGia) + 2 * (2 * Gia_ManAndNum(pGia) + Gia_ManCoNum(pGia));
+ p->pObjData = ABC_CALLOC( int, p->nObjData );
+ // create constant node
+ Gia_ManConst0(pGia)->Value = hHandle;
+ pObjLog = Frc_ManObj( p, hHandle );
+ pObjLog->hHandle = hHandle;
+ pObjLog->nFanins = 0;
+ pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) );
+ // count objects
+ hHandle += Frc_ObjSize( pObjLog );
+ nNodes = 1;
+ p->nObjs++;
+ // create the PIs
+ Gia_ManForEachCi( pGia, pObj, i )
+ {
+ // create PI object
+ pObj->Value = hHandle;
+ Vec_IntPush( p->vCis, hHandle );
+ pObjLog = Frc_ManObj( p, hHandle );
+ pObjLog->hHandle = hHandle;
+ pObjLog->nFanins = 0;
+ pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+ pObjLog->fCi = 0;
+ // count objects
+ hHandle += Frc_ObjSize( pObjLog );
+ p->nObjs++;
+ }
+ // create internal nodes
+ Gia_ManForEachAnd( pGia, pObj, i )
+ {
+ assert( Gia_ObjRefs( pGia, pObj ) > 0 );
+ // create node object
+ pObj->Value = hHandle;
+ pObjLog = Frc_ManObj( p, hHandle );
+ pObjLog->hHandle = hHandle;
+ pObjLog->nFanins = 2;
+ pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+ // add fanins
+ pFanLog = Frc_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
+ Frc_ObjAddFanin( pObjLog, pFanLog );
+ pFanLog = Frc_ManObj( p, Gia_ObjValue(Gia_ObjFanin1(pObj)) );
+ Frc_ObjAddFanin( pObjLog, pFanLog );
+ // count objects
+ hHandle += Frc_ObjSize( pObjLog );
+ nNodes++;
+ p->nObjs++;
+ }
+ // create the POs
+ Gia_ManForEachCo( pGia, pObj, i )
+ {
+ // create PO object
+ pObj->Value = hHandle;
+ Vec_IntPush( p->vCos, hHandle );
+ pObjLog = Frc_ManObj( p, hHandle );
+ pObjLog->hHandle = hHandle;
+ pObjLog->nFanins = 1;
+ pObjLog->nFanouts = 0;
+ pObjLog->fCo = 1;
+ // add fanins
+ pFanLog = Frc_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
+ Frc_ObjAddFanin( pObjLog, pFanLog );
+ // count objects
+ hHandle += Frc_ObjSize( pObjLog );
+ p->nObjs++;
+ }
+ // connect registers
+// Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, i )
+// Frc_ObjAddFanin( Frc_ManObj(p,Gia_ObjValue(pObjRo)), Frc_ManObj(p,Gia_ObjValue(pObjRi)) );
+ assert( nNodes == Frc_ManNodeNum(p) );
+ assert( hHandle == p->nObjData );
+ if ( hHandle != p->nObjData )
+ printf( "Frc_ManStartSimple(): Fatal error in internal representation.\n" );
+ // make sure the fanin/fanout counters are correct
+ Gia_ManForEachObj( pGia, pObj, i )
+ {
+ if ( !~Gia_ObjValue(pObj) )
+ continue;
+ pObjLog = Frc_ManObj( p, Gia_ObjValue(pObj) );
+ assert( pObjLog->nFanins == pObjLog->iFanin );
+ assert( pObjLog->nFanouts == pObjLog->iFanout );
+ pObjLog->iFanin = pObjLog->iFanout = 0;
+ }
+ ABC_FREE( pGia->pRefs );
return p;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Collect the fanin IDs.]
Description []
@@ -97,19 +255,50 @@ For_Man_t * For_ManStart( Gia_Man_t * pGia )
SeeAlso []
***********************************************************************/
-void For_ManStop( For_Man_t * p )
+void Frc_ManCollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper, Vec_Int_t * vVisit )
{
- ABC_FREE( p->pPlace );
- ABC_FREE( p->piNext );
- ABC_FREE( p->piRoot );
- ABC_FREE( p->plEdge );
- ABC_FREE( p->pNodes );
- ABC_FREE( p );
+ if ( pObj->fMark1 )
+ return;
+ pObj->fMark1 = 1;
+ Vec_IntPush( vVisit, Gia_ObjId(p, pObj) );
+ if ( pObj->fMark0 )
+ {
+ Vec_IntPush( vSuper, Gia_ObjId(p, pObj) );
+ return;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
+ Frc_ManCollectSuper_rec( p, Gia_ObjFanin0(pObj), vSuper, vVisit );
+ Frc_ManCollectSuper_rec( p, Gia_ObjFanin1(pObj), vSuper, vVisit );
+
}
/**Function*************************************************************
- Synopsis [Derives random ordering of nodes.]
+ Synopsis [Collect the fanin IDs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Frc_ManCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper, Vec_Int_t * vVisit )
+{
+ int Entry, i;
+ Vec_IntClear( vSuper );
+ Vec_IntClear( vVisit );
+ assert( pObj->fMark0 == 1 );
+ pObj->fMark0 = 0;
+ Frc_ManCollectSuper_rec( p, pObj, vSuper, vVisit );
+ pObj->fMark0 = 1;
+ Vec_IntForEachEntry( vVisit, Entry, i )
+ Gia_ManObj(p, Entry)->fMark1 = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assigns references while removing the MUX/XOR ones.]
Description []
@@ -118,24 +307,44 @@ void For_ManStop( For_Man_t * p )
SeeAlso []
***********************************************************************/
-void For_ManSetInitPlaceRandom( For_Man_t * p )
+void Frc_ManCreateRefsSpecial( Gia_Man_t * p )
{
- int i, Temp, iNext;
- Aig_ManRandom( 1 );
- for ( i = 0; i < p->nObjs; i++ )
- p->pPlace[i] = i;
- for ( i = 0; i < p->nObjs; i++ )
+ Gia_Obj_t * pObj, * pFan0, * pFan1;
+ Gia_Obj_t * pObjC, * pObjD0, * pObjD1;
+ int i;
+ assert( p->pRefs == NULL );
+ Gia_ManCleanMark0( p );
+ Gia_ManCreateRefs( p );
+ Gia_ManForEachAnd( p, pObj, i )
{
- iNext = Aig_ManRandom( 0 ) % p->nObjs;
- Temp = p->pPlace[i];
- p->pPlace[i] = p->pPlace[iNext];
- p->pPlace[iNext] = Temp;
+ assert( pObj->fMark0 == 0 );
+ pFan0 = Gia_ObjFanin0(pObj);
+ pFan1 = Gia_ObjFanin1(pObj);
+ // skip nodes whose fanins are PIs or are already marked
+ if ( Gia_ObjIsCi(pFan0) || pFan0->fMark0 ||
+ Gia_ObjIsCi(pFan1) || pFan1->fMark0 )
+ continue;
+ // skip nodes that are not MUX type
+ if ( !Gia_ObjIsMuxType(pObj) )
+ continue;
+ // the node is MUX type, mark it and its fanins
+ pObj->fMark0 = 1;
+ pFan0->fMark0 = 1;
+ pFan1->fMark0 = 1;
+ // deref the control
+ pObjC = Gia_ObjRecognizeMux( pObj, &pObjD1, &pObjD0 );
+ Gia_ObjRefDec( p, Gia_Regular(pObjC) );
+ if ( Gia_Regular(pObjD0) == Gia_Regular(pObjD1) )
+ Gia_ObjRefDec( p, Gia_Regular(pObjD0) );
}
+ Gia_ManForEachAnd( p, pObj, i )
+ assert( Gia_ObjRefs(p, pObj) > 0 );
+ Gia_ManCleanMark0( p );
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Assigns references while removing the MUX/XOR ones.]
Description []
@@ -144,39 +353,196 @@ void For_ManSetInitPlaceRandom( For_Man_t * p )
SeeAlso []
***********************************************************************/
-void For_ManSetInitPlaceDfs_rec( For_Man_t * p, Gia_Obj_t * pObj, int fRev )
+void Frc_ManTransformRefs( Gia_Man_t * p, int * pnObjs, int * pnFanios )
{
- if ( pObj->fMark0 )
- return;
- pObj->fMark0 = 1;
- if ( Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj) )
+ Vec_Int_t * vSuper, * vVisit;
+ Gia_Obj_t * pObj, * pFanin;
+ int i, k, Counter;
+ assert( p->pRefs != NULL );
+
+ // mark nodes to be used in the logic network
+ Gia_ManCleanMark0( p );
+ Gia_ManConst0(p)->fMark0 = 1;
+ // mark the inputs
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->fMark0 = 1;
+ // mark those nodes that have ref count more than 1
+ Gia_ManForEachAnd( p, pObj, i )
+ pObj->fMark0 = (Gia_ObjRefs(p, pObj) > 1);
+ // mark the output drivers
+ Gia_ManForEachCoDriver( p, pObj, i )
+ pObj->fMark0 = 1;
+
+ // count the number of nodes
+ Counter = 0;
+ Gia_ManForEachObj( p, pObj, i )
+ Counter += pObj->fMark0;
+ *pnObjs = Counter + Gia_ManCoNum(p);
+
+ // reset the references
+ ABC_FREE( p->pRefs );
+ p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
+ // reference from internal nodes
+ Counter = 0;
+ vSuper = Vec_IntAlloc( 100 );
+ vVisit = Vec_IntAlloc( 100 );
+ Gia_ManCleanMark1( p );
+ Gia_ManForEachAnd( p, pObj, i )
{
- p->pPlace[ Gia_ObjId(p->pGia, pObj) ] = p->iObj++;
- return;
+ if ( pObj->fMark0 == 0 )
+ continue;
+ Frc_ManCollectSuper( p, pObj, vSuper, vVisit );
+ Gia_ManForEachObjVec( vSuper, p, pFanin, k )
+ {
+ assert( pFanin->fMark0 );
+ Gia_ObjRefInc( p, pFanin );
+ }
+ Counter += Vec_IntSize( vSuper );
}
- if ( Gia_ObjIsCo(pObj) )
+ Gia_ManCheckMark1( p );
+ Vec_IntFree( vSuper );
+ Vec_IntFree( vVisit );
+ // reference from outputs
+ Gia_ManForEachCoDriver( p, pObj, i )
{
- For_ManSetInitPlaceDfs_rec( p, Gia_ObjFanin0(pObj), fRev );
- p->pPlace[ Gia_ObjId(p->pGia, pObj) ] = p->iObj++;
- return;
+ assert( pObj->fMark0 );
+ Gia_ObjRefInc( p, pObj );
}
- assert( Gia_ObjIsAnd(pObj) );
- if ( fRev )
+ *pnFanios = Counter + Gia_ManCoNum(p);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates logic network isomorphic to the given AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Frc_Man_t * Frc_ManStart( Gia_Man_t * pGia )
+{
+ Frc_Man_t * p;
+ Frc_Obj_t * pObjLog, * pFanLog;
+ Gia_Obj_t * pObj, * pFanin;//, * pObjRi, * pObjRo;
+ Vec_Int_t * vSuper, * vVisit;
+ int nObjs, nFanios, nNodes = 0;
+ int i, k, hHandle = 0;
+ // prepare the AIG
+// Gia_ManCreateRefs( pGia );
+ Frc_ManCreateRefsSpecial( pGia );
+ Frc_ManTransformRefs( pGia, &nObjs, &nFanios );
+ Gia_ManFillValue( pGia );
+ // create logic network
+ p = ABC_CALLOC( Frc_Man_t, 1 );
+ p->pGia = pGia;
+ p->nRegs = Gia_ManRegNum(pGia);
+ p->vCis = Vec_IntAlloc( Gia_ManCiNum(pGia) );
+ p->vCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );
+ p->nObjData = (sizeof(Frc_Obj_t) / 4) * nObjs + 2 * nFanios;
+ p->pObjData = ABC_CALLOC( int, p->nObjData );
+ // create constant node
+ Gia_ManConst0(pGia)->Value = hHandle;
+ pObjLog = Frc_ManObj( p, hHandle );
+ pObjLog->hHandle = hHandle;
+ pObjLog->nFanins = 0;
+ pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) );
+ // count objects
+ hHandle += Frc_ObjSize( pObjLog );
+ nNodes++;
+ p->nObjs++;
+ // create the PIs
+ Gia_ManForEachCi( pGia, pObj, i )
{
- For_ManSetInitPlaceDfs_rec( p, Gia_ObjFanin1(pObj), fRev );
- For_ManSetInitPlaceDfs_rec( p, Gia_ObjFanin0(pObj), fRev );
+ // create PI object
+ pObj->Value = hHandle;
+ Vec_IntPush( p->vCis, hHandle );
+ pObjLog = Frc_ManObj( p, hHandle );
+ pObjLog->hHandle = hHandle;
+ pObjLog->nFanins = 0;
+ pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+ pObjLog->fCi = 1;
+ // count objects
+ hHandle += Frc_ObjSize( pObjLog );
+ p->nObjs++;
}
- else
+ // create internal nodes
+ vSuper = Vec_IntAlloc( 100 );
+ vVisit = Vec_IntAlloc( 100 );
+ Gia_ManForEachAnd( pGia, pObj, i )
{
- For_ManSetInitPlaceDfs_rec( p, Gia_ObjFanin0(pObj), fRev );
- For_ManSetInitPlaceDfs_rec( p, Gia_ObjFanin1(pObj), fRev );
+ if ( pObj->fMark0 == 0 )
+ {
+ assert( Gia_ObjRefs( pGia, pObj ) == 0 );
+ continue;
+ }
+ assert( Gia_ObjRefs( pGia, pObj ) > 0 );
+ Frc_ManCollectSuper( pGia, pObj, vSuper, vVisit );
+ // create node object
+ pObj->Value = hHandle;
+ pObjLog = Frc_ManObj( p, hHandle );
+ pObjLog->hHandle = hHandle;
+ pObjLog->nFanins = Vec_IntSize( vSuper );
+ pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+ // add fanins
+ Gia_ManForEachObjVec( vSuper, pGia, pFanin, k )
+ {
+ pFanLog = Frc_ManObj( p, Gia_ObjValue(pFanin) );
+ Frc_ObjAddFanin( pObjLog, pFanLog );
+ }
+ // count objects
+ hHandle += Frc_ObjSize( pObjLog );
+ nNodes++;
+ p->nObjs++;
+ }
+ Vec_IntFree( vSuper );
+ Vec_IntFree( vVisit );
+ // create the POs
+ Gia_ManForEachCo( pGia, pObj, i )
+ {
+ // create PO object
+ pObj->Value = hHandle;
+ Vec_IntPush( p->vCos, hHandle );
+ pObjLog = Frc_ManObj( p, hHandle );
+ pObjLog->hHandle = hHandle;
+ pObjLog->nFanins = 1;
+ pObjLog->nFanouts = 0;
+ pObjLog->fCo = 1;
+ // add fanins
+ pFanLog = Frc_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
+ Frc_ObjAddFanin( pObjLog, pFanLog );
+ // count objects
+ hHandle += Frc_ObjSize( pObjLog );
+ p->nObjs++;
}
- p->pPlace[ Gia_ObjId(p->pGia, pObj) ] = p->iObj++;
+ // connect registers
+// Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, i )
+// Frc_ObjAddFanin( Frc_ManObj(p,Gia_ObjValue(pObjRo)), Frc_ManObj(p,Gia_ObjValue(pObjRi)) );
+ Gia_ManCleanMark0( pGia );
+ assert( nNodes == Frc_ManNodeNum(p) );
+ assert( nObjs == p->nObjs );
+ assert( hHandle == p->nObjData );
+ if ( hHandle != p->nObjData )
+ printf( "Frc_ManStart(): Fatal error in internal representation.\n" );
+ // make sure the fanin/fanout counters are correct
+ Gia_ManForEachObj( pGia, pObj, i )
+ {
+ if ( !~Gia_ObjValue(pObj) )
+ continue;
+ pObjLog = Frc_ManObj( p, Gia_ObjValue(pObj) );
+ assert( pObjLog->nFanins == pObjLog->iFanin );
+ assert( pObjLog->nFanouts == pObjLog->iFanout );
+ pObjLog->iFanin = pObjLog->iFanout = 0;
+ }
+ ABC_FREE( pGia->pRefs );
+ return p;
}
/**Function*************************************************************
- Synopsis [Derives DFS ordering of nodes.]
+ Synopsis [Creates logic network isomorphic to the given AIG.]
Description []
@@ -185,25 +551,25 @@ void For_ManSetInitPlaceDfs_rec( For_Man_t * p, Gia_Obj_t * pObj, int fRev )
SeeAlso []
***********************************************************************/
-void For_ManSetInitPlaceDfs( For_Man_t * p, int fRev )
+void Frc_ManPrintStats( Frc_Man_t * p )
{
- Gia_Obj_t * pObj;
- int i;
- p->iObj = 0;
- Gia_ManCleanMark0( p->pGia );
- For_ManSetInitPlaceDfs_rec( p, Gia_ManConst0(p->pGia), fRev );
- Gia_ManForEachCo( p->pGia, pObj, i )
- For_ManSetInitPlaceDfs_rec( p, pObj, fRev );
- Gia_ManForEachCi( p->pGia, pObj, i )
- if ( pObj->fMark0 == 0 )
- For_ManSetInitPlaceDfs_rec( p, pObj, fRev );
- assert( p->iObj == p->nObjs );
- Gia_ManCleanMark0( p->pGia );
+// if ( p->pName )
+// printf( "%8s : ", p->pName );
+ printf( "i/o =%7d/%7d ", Frc_ManPiNum(p), Frc_ManPoNum(p) );
+ if ( Frc_ManRegNum(p) )
+ printf( "ff =%7d ", Frc_ManRegNum(p) );
+ printf( "node =%8d ", Frc_ManNodeNum(p) );
+ printf( "obj =%8d ", Frc_ManObjNum(p) );
+// printf( "lev =%5d ", Frc_ManLevelNum(p) );
+// printf( "cut =%5d ", Frc_ManCrossCut(p) );
+ printf( "mem =%5.2f Mb", 4.0*p->nObjData/(1<<20) );
+// printf( "obj =%5d ", Frc_ManObjNum(p) );
+ printf( "\n" );
}
/**Function*************************************************************
- Synopsis [Computes span for the given placement.]
+ Synopsis [Creates logic network isomorphic to the given AIG.]
Description []
@@ -212,29 +578,72 @@ void For_ManSetInitPlaceDfs( For_Man_t * p, int fRev )
SeeAlso []
***********************************************************************/
-double For_ManGetEdgeSpan( For_Man_t * p )
+void Frc_ManStop( Frc_Man_t * p )
{
- double Result = 0.0;
- Gia_Obj_t * pObj;
- int i, Diff;
- Gia_ManForEachAnd( p->pGia, pObj, i )
+ Vec_IntFree( p->vCis );
+ Vec_IntFree( p->vCos );
+ ABC_FREE( p->pObjData );
+ ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes cross cut size for the given order of POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Frc_ManCrossCut_rec( Frc_Man_t * p, Frc_Obj_t * pObj )
+{
+ assert( pObj->iFanout > 0 );
+ if ( pObj->iFanout-- == pObj->nFanouts )
{
- Diff = Gia_ObjPlace(p, pObj) - Gia_ObjPlaceFanin0(p, pObj);
- Result += (double)ABC_ABS(Diff);
- Diff = Gia_ObjPlace(p, pObj) - Gia_ObjPlaceFanin1(p, pObj);
- Result += (double)ABC_ABS(Diff);
+ Frc_Obj_t * pFanin;
+ int i;
+ p->nCutCur++;
+ p->nCutMax = ABC_MAX( p->nCutMax, p->nCutCur );
+ if ( !Frc_ObjIsCi(pObj) )
+ Frc_ObjForEachFanin( pObj, pFanin, i )
+ p->nCutCur -= Frc_ManCrossCut_rec( p, pFanin );
}
- Gia_ManForEachCo( p->pGia, pObj, i )
+ return pObj->iFanout == 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes cross cut size for the given order of POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Frc_ManCrossCut2_rec( Frc_Man_t * p, Frc_Obj_t * pObj )
+{
+ assert( pObj->iFanout > 0 );
+ if ( pObj->iFanout-- == pObj->nFanouts )
{
- Diff = Gia_ObjPlace(p, pObj) - Gia_ObjPlaceFanin0(p, pObj);
- Result += (double)ABC_ABS(Diff);
+ Frc_Obj_t * pFanin;
+ int i;
+ p->nCutCur++;
+ p->nCutMax = ABC_MAX( p->nCutMax, p->nCutCur );
+ if ( !Frc_ObjIsCi(pObj) )
+ Frc_ObjForEachFaninReverse( pObj, pFanin, i )
+ p->nCutCur -= Frc_ManCrossCut2_rec( p, pFanin );
}
- return Result;
+ return pObj->iFanout == 0;
}
/**Function*************************************************************
- Synopsis [Computes max cut of the given placement.]
+ Synopsis [Computes cross cut size for the given order of POs.]
Description []
@@ -243,68 +652,138 @@ double For_ManGetEdgeSpan( For_Man_t * p )
SeeAlso []
***********************************************************************/
-int For_ManGetMaxCut( For_Man_t * p )
+int Frc_ManCrossCut( Frc_Man_t * p, Vec_Int_t * vOrder, int fReverse )
{
- Gia_Obj_t * pObj;
- int i, iObj, iFan, * pTemp;
- int nCutCut, nCutMax;
- pTemp = ABC_CALLOC( int, p->nObjs );
- Gia_ManForEachAnd( p->pGia, pObj, i )
+ Frc_Obj_t * pObj;
+ int i;
+ assert( Vec_IntSize(vOrder) == Frc_ManCoNum(p) );
+ p->nCutCur = 0;
+ p->nCutMax = 0;
+ Frc_ManForEachObj( p, pObj, i )
+ pObj->iFanout = pObj->nFanouts;
+ Frc_ManForEachObjVec( vOrder, p, pObj, i )
{
- iObj = Gia_ObjPlace(p, pObj);
- iFan = Gia_ObjPlaceFanin0(p, pObj);
- if ( iObj < iFan )
- {
- pTemp[iObj]++;
- pTemp[iFan]--;
- }
- else
- {
- pTemp[iObj]--;
- pTemp[iFan]++;
- }
- iObj = Gia_ObjPlace(p, pObj);
- iFan = Gia_ObjPlaceFanin1(p, pObj);
- if ( iObj < iFan )
- {
- pTemp[iObj]++;
- pTemp[iFan]--;
- }
+ assert( Frc_ObjIsCo(pObj) );
+ if ( fReverse )
+ p->nCutCur -= Frc_ManCrossCut2_rec( p, Frc_ObjFanin(pObj,0) );
else
- {
- pTemp[iObj]--;
- pTemp[iFan]++;
- }
+ p->nCutCur -= Frc_ManCrossCut_rec( p, Frc_ObjFanin(pObj,0) );
}
- Gia_ManForEachCo( p->pGia, pObj, i )
+ assert( p->nCutCur == 0 );
+// Frc_ManForEachObj( p, pObj, i )
+// assert( pObj->iFanout == 0 );
+ return p->nCutMax;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects CO handles.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Frc_ManCollectCos( Frc_Man_t * p )
+{
+ Vec_Int_t * vCoOrder;
+ Frc_Obj_t * pObj;
+ int i;
+ vCoOrder = Vec_IntAlloc( Frc_ManCoNum(p) );
+ Frc_ManForEachCo( p, pObj, i )
+ Vec_IntPush( vCoOrder, pObj->hHandle );
+ return vCoOrder;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes cross cut size for the given order of POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Frc_ManCrossCutTest( Frc_Man_t * p, Vec_Int_t * vOrderInit )
+{
+ Vec_Int_t * vOrder;
+ int clk = clock();
+ vOrder = vOrderInit? vOrderInit : Frc_ManCollectCos( p );
+ printf( "CrossCut = %6d\n", Frc_ManCrossCut( p, vOrder, 0 ) );
+ printf( "CrossCut = %6d\n", Frc_ManCrossCut( p, vOrder, 1 ) );
+ Vec_IntReverseOrder( vOrder );
+ printf( "CrossCut = %6d\n", Frc_ManCrossCut( p, vOrder, 0 ) );
+ printf( "CrossCut = %6d\n", Frc_ManCrossCut( p, vOrder, 1 ) );
+ Vec_IntReverseOrder( vOrder );
+ if ( vOrder != vOrderInit )
+ Vec_IntFree( vOrder );
+// ABC_PRT( "Time", clock() - clk );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Generates random placement.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Frc_ManPlaceRandom( Frc_Man_t * p )
+{
+ Frc_Obj_t * pThis;
+ int * pPlacement;
+ int i, h, Temp, iNext, Counter;
+ pPlacement = ABC_ALLOC( int, p->nObjs );
+ for ( i = 0; i < p->nObjs; i++ )
+ pPlacement[i] = i;
+ for ( i = 0; i < p->nObjs; i++ )
{
- iObj = Gia_ObjPlace(p, pObj);
- iFan = Gia_ObjPlaceFanin0(p, pObj);
- if ( iObj < iFan )
- {
- pTemp[iObj]++;
- pTemp[iFan]--;
- }
- else
- {
- pTemp[iObj]--;
- pTemp[iFan]++;
- }
+ iNext = Aig_ManRandom( 0 ) % p->nObjs;
+ Temp = pPlacement[i];
+ pPlacement[i] = pPlacement[iNext];
+ pPlacement[iNext] = Temp;
}
- nCutCut = nCutMax = 0;
- for ( i = 0; i < p->nObjs; i++ )
+ Counter = 0;
+ Frc_ManForEachObj( p, pThis, h )
+ pThis->pPlace = pPlacement[Counter++];
+ ABC_FREE( pPlacement );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Shuffles array of random integers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Frc_ManArrayShuffle( Vec_Int_t * vArray )
+{
+ int i, iNext, Temp;
+ for ( i = 0; i < vArray->nSize; i++ )
{
- nCutCut += pTemp[i];
- nCutMax = ABC_MAX( nCutCut, nCutMax );
+ iNext = Aig_ManRandom( 0 ) % vArray->nSize;
+ Temp = vArray->pArray[i];
+ vArray->pArray[i] = vArray->pArray[iNext];
+ vArray->pArray[iNext] = Temp;
}
- ABC_FREE( pTemp );
- assert( nCutCut == 0 );
- return nCutMax;
}
/**Function*************************************************************
- Synopsis [Computes hyper-edge centers.]
+ Synopsis [Computes cross cut size for the given order of POs.]
Description []
@@ -313,31 +792,23 @@ int For_ManGetMaxCut( For_Man_t * p )
SeeAlso []
***********************************************************************/
-void For_ManEdgeCenters( For_Man_t * p )
+void Frc_ManPlaceDfs_rec( Frc_Man_t * p, Frc_Obj_t * pObj, int * piPlace )
{
- Gia_Obj_t * pObj;
- int i;
- memset( p->plEdge, 0, sizeof(float) * p->nObjs );
- Gia_ManForEachObj( p->pGia, pObj, i )
+ assert( pObj->iFanout > 0 );
+ if ( pObj->iFanout-- == pObj->nFanouts )
{
- p->plEdge[i] = Gia_ObjPlace(p, pObj);
- if ( Gia_ObjIsAnd(pObj) )
- {
- p->plEdge[Gia_ObjFaninId0p(p->pGia, pObj)] += Gia_ObjPlace(p, pObj);
- p->plEdge[Gia_ObjFaninId1p(p->pGia, pObj)] += Gia_ObjPlace(p, pObj);
- }
- else if ( Gia_ObjIsCo(pObj) )
- {
- p->plEdge[Gia_ObjFaninId0p(p->pGia, pObj)] += Gia_ObjPlace(p, pObj);
- }
+ Frc_Obj_t * pFanin;
+ int i;
+ if ( !Frc_ObjIsCi(pObj) )
+ Frc_ObjForEachFanin( pObj, pFanin, i )
+ Frc_ManPlaceDfs_rec( p, pFanin, piPlace );
+ pObj->pPlace = (*piPlace)++;
}
- Gia_ManForEachObj( p->pGia, pObj, i )
- p->plEdge[i] /= 1.0 + Gia_ObjRefs( p->pGia, pObj );
}
/**Function*************************************************************
- Synopsis [Computes object centers.]
+ Synopsis [Generates DFS placement.]
Description []
@@ -346,30 +817,156 @@ void For_ManEdgeCenters( For_Man_t * p )
SeeAlso []
***********************************************************************/
-void For_ManObjCenters( For_Man_t * p )
+void Frc_ManPlaceDfs( Frc_Man_t * p, Vec_Int_t * vCoOrder )
{
- Gia_Obj_t * pObj;
- int i;
- Gia_ManForEachObj( p->pGia, pObj, i )
+ Frc_Obj_t * pObj;
+ int i, nPlaces = 0;
+ Frc_ManForEachObj( p, pObj, i )
{
- p->pNodes[i].lNode = Gia_ObjEdge(p, pObj);
- if ( Gia_ObjIsAnd(pObj) )
+ pObj->iFanout = pObj->nFanouts;
+ if ( pObj->nFanouts == 0 && !Frc_ObjIsCo(pObj) )
+ pObj->pPlace = nPlaces++;
+ }
+ Frc_ManForEachObjVec( vCoOrder, p, pObj, i )
+ {
+ assert( Frc_ObjIsCo(pObj) );
+ Frc_ManPlaceDfs_rec( p, Frc_ObjFanin(pObj,0), &nPlaces );
+ pObj->pPlace = nPlaces++;
+ }
+ assert( nPlaces == p->nObjs );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Generates DFS placement by trying both orders.]
+
+ Description [Returns the cross cut size of the best order. ]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Frc_ManPlaceDfsBoth( Frc_Man_t * p, Vec_Int_t * vCoOrder, int * piCutSize2 )
+{
+ int nCutStart1, nCutStart2;
+ nCutStart1 = Frc_ManCrossCut( p, vCoOrder, 0 );
+ Vec_IntReverseOrder( vCoOrder );
+ nCutStart2 = Frc_ManCrossCut( p, vCoOrder, 0 );
+ if ( nCutStart1 <= nCutStart2 )
+ {
+ Vec_IntReverseOrder( vCoOrder ); // undo
+ Frc_ManPlaceDfs( p, vCoOrder );
+ *piCutSize2 = nCutStart2;
+ return nCutStart1;
+ }
+ else
+ {
+ Frc_ManPlaceDfs( p, vCoOrder );
+ Vec_IntReverseOrder( vCoOrder ); // undo
+ *piCutSize2 = nCutStart1;
+ return nCutStart2;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs iterative refinement of the given placement.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Frc_ManPlacementRefine( Frc_Man_t * p, int nIters, int fVerbose )
+{
+ int fRandomize = 0;
+ Vec_Int_t * vCoOrder;
+ Frc_Obj_t * pThis, * pNext;
+ double CostThis, CostPrev;
+ float * pVertX, VertX;
+ int * pPermX, * pHandles;
+ int k, h, Iter, iMinX, iMaxX, Counter, nCutStart, nCutCur, nCutCur2, nCutPrev;
+ int clk = clock(), clk2, clk2Total = 0;
+ // create starting one-dimensional placement
+ vCoOrder = Frc_ManCollectCos( p );
+ if ( fRandomize )
+ Frc_ManArrayShuffle( vCoOrder );
+ nCutStart = Frc_ManPlaceDfsBoth( p, vCoOrder, &nCutCur2 );
+ // refine placement
+ CostPrev = 0.0;
+ nCutPrev = nCutStart;
+ pHandles = ABC_ALLOC( int, p->nObjs );
+ pVertX = ABC_ALLOC( float, p->nObjs );
+ for ( Iter = 0; Iter < nIters; Iter++ )
+ {
+ // compute centers of hyperedges
+ CostThis = 0.0;
+ Frc_ManForEachObj( p, pThis, h )
+ {
+ iMinX = iMaxX = pThis->pPlace;
+ Frc_ObjForEachFanout( pThis, pNext, k )
+ {
+ iMinX = ABC_MIN( iMinX, pNext->pPlace );
+ iMaxX = ABC_MAX( iMaxX, pNext->pPlace );
+ }
+ pThis->fEdgeCenter = 0.5 * (iMaxX + iMinX);
+ CostThis += (iMaxX - iMinX);
+ }
+ // compute new centers of objects
+ Counter = 0;
+ Frc_ManForEachObj( p, pThis, h )
{
- p->pNodes[i].lNode += Gia_ObjEdgeFanin0(p, pObj);
- p->pNodes[i].lNode += Gia_ObjEdgeFanin1(p, pObj);
- p->pNodes[i].lNode /= 3.0;
+ VertX = pThis->fEdgeCenter;
+ Frc_ObjForEachFanin( pThis, pNext, k )
+ VertX += pNext->fEdgeCenter;
+ pVertX[Counter] = VertX / (Frc_ObjFaninNum(pThis) + 1);
+ pHandles[Counter++] = h;
}
- else if ( Gia_ObjIsCo(pObj) )
+ assert( Counter == Frc_ManObjNum(p) );
+ // sort these numbers
+ clk2 = clock();
+ pPermX = Gia_SortFloats( pVertX, pHandles, p->nObjs );
+ clk2Total += clock() - clk2;
+ assert( pPermX == pHandles );
+ Vec_IntClear( vCoOrder );
+ for ( k = 0; k < p->nObjs; k++ )
{
- p->pNodes[i].lNode += Gia_ObjEdgeFanin0(p, pObj);
- p->pNodes[i].lNode /= 2.0;
+ pThis = Frc_ManObj( p, pPermX[k] );
+ pThis->pPlace = k;
+ if ( Frc_ObjIsCo(pThis) )
+ Vec_IntPush( vCoOrder, pThis->hHandle );
}
+/*
+ printf( "Ordering of PIs:\n" );
+ Frc_ManForEachCi( p, pThis, k )
+ printf( "PI number = %7d. Object handle = %7d, Coordinate = %7d.\n",
+ k, pThis->hHandle, pThis->pPlace );
+*/
+ nCutCur = Frc_ManPlaceDfsBoth( p, vCoOrder, &nCutCur2 );
+ // evaluate cost
+ if ( fVerbose )
+ {
+ printf( "%2d : Span = %e ", Iter+1, CostThis );
+ printf( "Cut = %6d (%5.2f %%) CutR = %6d ", nCutCur, 100.0*(nCutStart-nCutCur)/nCutStart, nCutCur2 );
+ ABC_PRTn( "Total", clock() - clk );
+ ABC_PRT( "Sort", clk2Total );
+// Frc_ManCrossCutTest( p, vCoOrder );
+ }
+// if ( 1.0 * nCutPrev / nCutCur < 1.001 )
+// break;
+ nCutPrev = nCutCur;
}
+ ABC_FREE( pHandles );
+ ABC_FREE( pVertX );
+ Vec_IntFree( vCoOrder );
}
/**Function*************************************************************
- Synopsis [Sorts objects by their new centers.]
+ Synopsis [Returns 1 if all fanouts are COsw.]
Description []
@@ -378,65 +975,56 @@ void For_ManObjCenters( For_Man_t * p )
SeeAlso []
***********************************************************************/
-int For_ObjCompare( For_Obj_t ** pp0, For_Obj_t ** pp1 )
+int Frc_ObjFanoutsAreCos( Frc_Obj_t * pThis )
{
- if ( (*pp0)->lNode < (*pp1)->lNode )
- return -1;
- if ( (*pp0)->lNode > (*pp1)->lNode )
- return 1;
- return 0;
+ Frc_Obj_t * pNext;
+ int i;
+ Frc_ObjForEachFanout( pThis, pNext, i )
+ if ( !Frc_ObjIsCo(pNext) )
+ return 0;
+ return 1;
}
/**Function*************************************************************
- Synopsis [Sorts objects by their new centers.]
+ Synopsis [Computes the distances from the given set of objects.]
- Description []
+ Description [Returns one of the most distant objects.]
SideEffects []
SeeAlso []
-
+
***********************************************************************/
-void For_ManSortObjects( For_Man_t * p )
+void Frc_DumpGraphIntoFile( Frc_Man_t * p )
{
- For_Obj_t * pNode, * pPrev;
- Vec_Ptr_t * vArray;
- int i, k, iPlace;
- // link the nodes into lists by cost
- memset( p->piRoot, 0xff, sizeof(int) * p->nObjs );
- for ( i = 0; i < p->nObjs; i++ )
+ FILE * pFile;
+ Frc_Obj_t * pThis, * pNext;
+ int i, k, Counter = 0;
+ // assign numbers to CIs and internal nodes
+ Frc_ManForEachObj( p, pThis, i )
{
- p->pNodes[i].iObj = i;
- iPlace = (int)p->pNodes[i].lNode;
- assert( iPlace >= 0 && iPlace < p->nObjs );
- p->piNext[i] = p->piRoot[iPlace];
- p->piRoot[iPlace] = i;
+ if ( i && ((Frc_ObjIsCi(pThis) && !Frc_ObjFanoutsAreCos(pThis)) || Frc_ObjIsNode(pThis)) )
+ pThis->iFanin = Counter++;
+ else
+ pThis->iFanin = ~0;
}
- // reconstruct the order
- p->iObj = 0;
- pPrev = NULL;
- vArray = Vec_PtrAlloc( 100 );
- for ( i = 0; i < p->nObjs; i++ )
+ // assign numbers to all other nodes
+ pFile = fopen( "x\\large\\aig\\dg1.g", "w" );
+ Frc_ManForEachObj( p, pThis, i )
{
- Vec_PtrClear( vArray );
- for ( k = p->piRoot[i]; ~((unsigned)k); k = p->piNext[k] )
- Vec_PtrPush( vArray, p->pNodes + k );
- Vec_PtrSort( vArray, (int (*)())For_ObjCompare );
- Vec_PtrForEachEntry( vArray, pNode, k )
+ Frc_ObjForEachFanout( pThis, pNext, k )
{
- p->pPlace[ pNode->iObj ] = p->iObj++;
- assert( !pPrev || pPrev->lNode <= pNode->lNode );
- pPrev = pNode;
+ if ( ~pThis->iFanin && ~pNext->iFanin )
+ fprintf( pFile, "%d %d\n", pThis->iFanin, pNext->iFanin );
}
}
- Vec_PtrFree( vArray );
- assert( p->iObj == p->nObjs );
+ fclose( pFile );
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Experiment with the FORCE algorithm.]
Description []
@@ -445,33 +1033,25 @@ void For_ManSortObjects( For_Man_t * p )
SeeAlso []
***********************************************************************/
-void For_ManPlaceByForce( For_Man_t * p )
+void For_ManExperiment( Gia_Man_t * pGia, int nIters, int fClustered, int fVerbose )
{
- int clk, Iter, fUseCut = 1;
- double iCostThis, iCostPrev;
- iCostThis = fUseCut? For_ManGetMaxCut(p) : For_ManGetEdgeSpan(p);
- printf( "Init = %12.0f. \n", iCostThis );
- Iter = 0;
- do {
- Iter++;
- iCostPrev = iCostThis;
-clk = clock();
- For_ManEdgeCenters( p );
-//ABC_PRT( "Time", clock() - clk );
-clk = clock();
- For_ManObjCenters( p );
-//ABC_PRT( "Time", clock() - clk );
-clk = clock();
- For_ManSortObjects( p );
-//ABC_PRT( "Time", clock() - clk );
- iCostThis = fUseCut? For_ManGetMaxCut(p) : For_ManGetEdgeSpan(p);
- printf( "%4d = %12.0f. \n", Iter, iCostThis );
- } while ( iCostPrev > iCostThis );
+ Frc_Man_t * p;
+ Aig_ManRandom( 1 );
+ if ( fClustered )
+ p = Frc_ManStart( pGia );
+ else
+ p = Frc_ManStartSimple( pGia );
+// Frc_DumpGraphIntoFile( p );
+ if ( fVerbose )
+ Frc_ManPrintStats( p );
+// Frc_ManCrossCutTest( p, NULL );
+ Frc_ManPlacementRefine( p, nIters, fVerbose );
+ Frc_ManStop( p );
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Experiment with the FORCE algorithm.]
Description []
@@ -480,51 +1060,40 @@ clk = clock();
SeeAlso []
***********************************************************************/
-void For_ManExperiment( Gia_Man_t * pGia )
+void For_ManFileExperiment()
{
- For_Man_t * p;
+ FILE * pFile;
+ int * pBuffer;
+ int i, Size, Exp = 25;
int clk = clock();
- p = For_ManStart( pGia );
- Gia_ManCreateRefs( pGia );
-
- // use DSF order
-clk = clock();
- For_ManSetInitPlaceDfs( p, 0 );
- printf( "Tot span = %12.0f ", For_ManGetEdgeSpan(p) );
- printf( "Max span = %8d ", For_ManGetMaxCut(p) );
-ABC_PRT( "Time", clock() - clk );
-
-clk = clock();
- For_ManPlaceByForce( p );
-ABC_PRT( "Time", clock() - clk );
- // use modified DFS order
-clk = clock();
- For_ManSetInitPlaceDfs( p, 1 );
- printf( "Tot span = %12.0f ", For_ManGetEdgeSpan(p) );
- printf( "Max span = %8d ", For_ManGetMaxCut(p) );
-ABC_PRT( "Time", clock() - clk );
+ Size = (1 << Exp);
+ printf( "2^%d machine words (%d bytes).\n", Exp, sizeof(int) * Size );
-clk = clock();
- For_ManPlaceByForce( p );
-ABC_PRT( "Time", clock() - clk );
+ pBuffer = ABC_ALLOC( int, Size );
+ for ( i = 0; i < Size; i++ )
+ pBuffer[i] = i;
+ABC_PRT( "Fillup", clock() - clk );
- // use random order
clk = clock();
- For_ManSetInitPlaceRandom( p );
- printf( "Tot span = %12.0f ", For_ManGetEdgeSpan(p) );
- printf( "Max span = %8d ", For_ManGetMaxCut(p) );
-ABC_PRT( "Time", clock() - clk );
+ pFile = fopen( "test.txt", "rb" );
+ fread( pBuffer, 1, sizeof(int) * Size, pFile );
+ fclose( pFile );
+ABC_PRT( "Read ", clock() - clk );
clk = clock();
- For_ManPlaceByForce( p );
-ABC_PRT( "Time", clock() - clk );
-
- For_ManStop( p );
+ pFile = fopen( "test.txt", "wb" );
+ fwrite( pBuffer, 1, sizeof(int) * Size, pFile );
+ fclose( pFile );
+ABC_PRT( "Write ", clock() - clk );
+/*
+2^25 machine words (134217728 bytes).
+Fillup = 0.06 sec
+Read = 0.08 sec
+Write = 1.81 sec
+*/
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
+//////////////////////////////////////////////////////////////////////// \ No newline at end of file
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index e6e45cb5..95bffee8 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -68,8 +68,13 @@ void Gia_ManStop( Gia_Man_t * p )
{
Vec_IntFree( p->vCis );
Vec_IntFree( p->vCos );
+ ABC_FREE( p->pCexComb );
+ ABC_FREE( p->pIso );
+ ABC_FREE( p->pMapping );
ABC_FREE( p->pFanData );
+ ABC_FREE( p->pReprsOld );
ABC_FREE( p->pReprs );
+ ABC_FREE( p->pNexts );
ABC_FREE( p->pName );
ABC_FREE( p->pRefs );
ABC_FREE( p->pLevels );
@@ -98,12 +103,16 @@ void Gia_ManPrintStats( Gia_Man_t * p )
printf( "ff =%7d ", Gia_ManRegNum(p) );
printf( "and =%8d ", Gia_ManAndNum(p) );
printf( "lev =%5d ", Gia_ManLevelNum(p) );
-// printf( "cut =%5d ", Gia_ManCrossCut(p) );
+ printf( "cut =%5d ", Gia_ManCrossCut(p) );
printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
// printf( "obj =%5d ", Gia_ManObjNum(p) );
printf( "\n" );
// Gia_ManSatExperiment( p );
+ if ( p->pReprs && p->pNexts )
+ Gia_ManEquivPrintClasses( p, 0, 0.0 );
+ if ( p->pMapping )
+ Gia_ManPrintMappingStats( p );
}
/**Function*************************************************************
diff --git a/src/aig/gia/giaMap.c b/src/aig/gia/giaMap.c
new file mode 100644
index 00000000..72bdb001
--- /dev/null
+++ b/src/aig/gia/giaMap.c
@@ -0,0 +1,305 @@
+/**CFile****************************************************************
+
+ FileName [giaMap.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [Manipulation of mapping associated with the AIG.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaMap.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "if.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Load the network into FPGA manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManSetIfParsDefault( If_Par_t * pPars )
+{
+// extern void * Abc_FrameReadLibLut();
+ // set defaults
+ memset( pPars, 0, sizeof(If_Par_t) );
+ // user-controlable paramters
+// pPars->nLutSize = -1;
+ pPars->nLutSize = 6;
+ pPars->nCutsMax = 8;
+ pPars->nFlowIters = 1;
+ pPars->nAreaIters = 2;
+ pPars->DelayTarget = -1;
+ pPars->Epsilon = (float)0.005;
+ pPars->fPreprocess = 1;
+ pPars->fArea = 0;
+ pPars->fFancy = 0;
+ pPars->fExpRed = 1; ////
+ pPars->fLatchPaths = 0;
+ pPars->fEdge = 1;
+ pPars->fPower = 0;
+ pPars->fCutMin = 0;
+ pPars->fSeqMap = 0;
+ pPars->fVerbose = 0;
+ // internal parameters
+ pPars->fTruth = 0;
+ pPars->nLatches = 0;
+ pPars->fLiftLeaves = 0;
+// pPars->pLutLib = Abc_FrameReadLibLut();
+ pPars->pLutLib = NULL;
+ pPars->pTimesArr = NULL;
+ pPars->pTimesArr = NULL;
+ pPars->pFuncCost = NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Load the network into FPGA manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
+{
+// extern Vec_Int_t * SGia_ManComputeSwitchProbs( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
+// Vec_Int_t * vSwitching = NULL, * vSwitching2 = NULL;
+// float * pSwitching, * pSwitching2;
+ If_Man_t * pIfMan;
+ If_Obj_t * pIfObj;
+ Gia_Obj_t * pNode;
+ int i, clk = clock();
+ Gia_ManLevelNum( p );
+/*
+ // set the number of registers (switch activity will be combinational)
+ Gia_ManSetRegNum( p, 0 );
+ if ( pPars->fPower )
+ {
+ vSwitching = SGia_ManComputeSwitchProbs( p, 48, 16, 0 );
+ if ( pPars->fVerbose )
+ {
+ ABC_PRT( "Computing switching activity", clock() - clk );
+ }
+ pSwitching = (float *)vSwitching->pArray;
+ vSwitching2 = Vec_IntStart( Gia_ManObjNumMax(p) );
+ pSwitching2 = (float *)vSwitching2->pArray;
+ }
+*/
+ // start the mapping manager and set its parameters
+ pIfMan = If_ManStart( pPars );
+// pIfMan->vSwitching = vSwitching2;
+ // load the AIG into the mapper
+ Gia_ManForEachObj( p, pNode, i )
+ {
+ if ( Gia_ObjIsAnd(pNode) )
+ pIfObj = If_ManCreateAnd( pIfMan,
+ If_NotCond( Vec_PtrEntry(vAigToIf, Gia_ObjFaninId0(pNode, i)), Gia_ObjFaninC0(pNode) ),
+ If_NotCond( Vec_PtrEntry(vAigToIf, Gia_ObjFaninId1(pNode, i)), Gia_ObjFaninC1(pNode) ) );
+ else if ( Gia_ObjIsCi(pNode) )
+ {
+ pIfObj = If_ManCreateCi( pIfMan );
+ If_ObjSetLevel( pIfObj, Gia_ObjLevel(p,pNode) );
+// printf( "pi=%d ", pIfObj->Level );
+ if ( pIfMan->nLevelMax < (int)pIfObj->Level )
+ pIfMan->nLevelMax = (int)pIfObj->Level;
+ }
+ else if ( Gia_ObjIsCo(pNode) )
+ {
+ pIfObj = If_ManCreateCo( pIfMan, If_NotCond( Vec_PtrEntry(vAigToIf, Gia_ObjFaninId0(pNode, i)), Gia_ObjFaninC0(pNode) ) );
+// printf( "po=%d ", pIfObj->Level );
+ }
+ else if ( Gia_ObjIsConst0(pNode) )
+ pIfObj = If_Not(If_ManConst1( pIfMan ));
+ else // add the node to the mapper
+ assert( 0 );
+ // save the result
+ assert( Vec_PtrEntry(vAigToIf, i) == NULL );
+ Vec_PtrWriteEntry( vAigToIf, i, pIfObj );
+// if ( vSwitching2 )
+// pSwitching2[pIfObj->Id] = pSwitching[pNode->Id];
+/* // set up the choice node
+ if ( Gia_ObjIsChoice( p, pNode ) )
+ {
+ pIfMan->nChoices++;
+ for ( pPrev = pNode, pFanin = Gia_ObjEquiv(p, pNode); pFanin; pPrev = pFanin, pFanin = Gia_ObjEquiv(p, pFanin) )
+ If_ObjSetChoice( pPrev->pData, pFanin->pData );
+ If_ManCreateChoice( pIfMan, pNode->pData );
+ }
+// assert( If_ObjLevel(pIfObj) == Gia_ObjLevel(pNode) );
+*/
+ }
+// if ( vSwitching )
+// Vec_IntFree( vSwitching );
+ return pIfMan;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Gia_ManFromIf( If_Man_t * pIfMan, Gia_Man_t * p, Vec_Ptr_t * vAigToIf )
+{
+ int * pMapping, iOffset;
+ Vec_Ptr_t * vIfToAig;
+ Gia_Obj_t * pObj, * pObjRepr;
+ If_Obj_t * pIfObj;
+ If_Cut_t * pCutBest;
+ int i, k, j, nLeaves, * ppLeaves;
+ int nItems = 0;
+ assert( Gia_ManCiNum(p) == If_ManCiNum(pIfMan) );
+ assert( Gia_ManCoNum(p) == If_ManCoNum(pIfMan) );
+ assert( Gia_ManAndNum(p) == If_ManAndNum(pIfMan) );
+ // create mapping of IF to AIG
+ vIfToAig = Vec_PtrStart( If_ManObjNum(pIfMan) );
+ Gia_ManForEachObj( p, pObj, i )
+ {
+ pIfObj = Vec_PtrEntry( vAigToIf, i );
+ Vec_PtrWriteEntry( vIfToAig, pIfObj->Id, pObj );
+ if ( !Gia_ObjIsAnd(pObj) || pIfObj->nRefs == 0 )
+ continue;
+ nItems += 2 + If_CutLeaveNum( If_ObjCutBest(pIfObj) );
+ }
+ // construct the network
+ pMapping = ABC_CALLOC( int, Gia_ManObjNum(p) + nItems );
+ iOffset = Gia_ManObjNum(p);
+ Gia_ManForEachObj( p, pObj, i )
+ {
+ pIfObj = Vec_PtrEntry( vAigToIf, i );
+ if ( !Gia_ObjIsAnd(pObj) || pIfObj->nRefs == 0 )
+ continue;
+ pCutBest = If_ObjCutBest( pIfObj );
+ nLeaves = If_CutLeaveNum( pCutBest );
+ ppLeaves = If_CutLeaves( pCutBest );
+ // create node
+ k = iOffset;
+ pMapping[k++] = nLeaves;
+ for ( j = 0; j < nLeaves; j++ )
+ {
+ pObjRepr = Vec_PtrEntry( vIfToAig, ppLeaves[j] );
+ pMapping[k++] = Gia_ObjId( p, pObjRepr );
+ }
+ pMapping[k++] = i;
+ pMapping[i] = iOffset;
+ iOffset = k;
+ }
+ assert( iOffset <= Gia_ManObjNum(p) + nItems );
+ Vec_PtrFree( vIfToAig );
+// pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
+ return pMapping;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Interface with the FPGA mapping package.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars )
+{
+ If_Man_t * pIfMan;
+ Vec_Ptr_t * vAigToIf;
+ // set the arrival times
+ pPars->pTimesArr = ABC_ALLOC( float, Gia_ManCiNum(p) );
+ memset( pPars->pTimesArr, 0, sizeof(float) * Gia_ManCiNum(p) );
+ // translate into the mapper
+ vAigToIf = Vec_PtrStart( Gia_ManObjNum(p) );
+ pIfMan = Gia_ManToIf( p, pPars, vAigToIf );
+ if ( pIfMan == NULL )
+ return 0;
+// pIfMan->pManTim = Tim_ManDup( pManTime, 0 );
+ if ( !If_ManPerformMapping( pIfMan ) )
+ {
+ If_ManStop( pIfMan );
+ return 0;
+ }
+ // transform the result of mapping into the new network
+ ABC_FREE( p->pMapping );
+ p->pMapping = Gia_ManFromIf( pIfMan, p, vAigToIf );
+// if ( pPars->fBidec && pPars->nLutSize <= 8 )
+// Gia_ManBidecResyn( pNtk, 0 );
+ If_ManStop( pIfMan );
+ Vec_PtrFree( vAigToIf );
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Prints mapping statistics.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManPrintMappingStats( Gia_Man_t * p )
+{
+ int * pLevels;
+ int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0;
+ if ( !p->pMapping )
+ return;
+ pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
+ Gia_ManForEachGate( p, i )
+ {
+ nLuts++;
+ nFanins += Gia_ObjGateSize(p, i);
+ nLutSize = ABC_MAX( nLutSize, Gia_ObjGateSize(p, i) );
+ Gia_GateForEachFanin( p, i, iFan, k )
+ pLevels[i] = ABC_MAX( pLevels[i], pLevels[iFan] );
+ pLevels[i]++;
+ LevelMax = ABC_MAX( LevelMax, pLevels[i] );
+ }
+ ABC_FREE( pLevels );
+ printf( "mapping : " );
+ printf( "%d=lut =%7d ", nLutSize, nLuts );
+ printf( "edge =%8d ", nFanins );
+ printf( "lev =%5d ", LevelMax );
+ printf( "mem =%5.2f Mb", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) );
+ printf( "\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/gia/giaScl.c b/src/aig/gia/giaScl.c
index 3f72b0b9..9058af7d 100644
--- a/src/aig/gia/giaScl.c
+++ b/src/aig/gia/giaScl.c
@@ -30,7 +30,7 @@
/**Function*************************************************************
- Synopsis [Returns the number of unmarked nodes.]
+ Synopsis [Marks unreachable internal nodes and returned their number.]
Description []
@@ -45,13 +45,13 @@ int Gia_ManCombMarkUsed_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
return 0;
pObj->fMark0 = 0;
assert( Gia_ObjIsAnd(pObj) );
- return Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin0(pObj) ) +
- Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) ) + 1;
+ return 1 + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin0(pObj) )
+ + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) );
}
/**Function*************************************************************
- Synopsis [Returns the number of unused nodes.]
+ Synopsis [Marks unreachable internal nodes and returned their number.]
Description []
@@ -90,7 +90,7 @@ Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p )
/**Function*************************************************************
- Synopsis [Marks CIs/COs reachable from POs.]
+ Synopsis [Marks CIs/COs/ANDs unreachable from POs.]
Description []
@@ -99,29 +99,26 @@ Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-void Gia_ManSeqMarkUsed_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRoots )
+int Gia_ManSeqMarkUsed_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRoots )
{
if ( !pObj->fMark0 )
- return;
+ return 0;
pObj->fMark0 = 0;
if ( Gia_ObjIsCo(pObj) )
- {
- Gia_ManSeqMarkUsed_rec( p, Gia_ObjFanin0(pObj), vRoots );
- return;
- }
+ return Gia_ManSeqMarkUsed_rec( p, Gia_ObjFanin0(pObj), vRoots );
if ( Gia_ObjIsRo(p, pObj) )
{
Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
- return;
+ return 0;
}
assert( Gia_ObjIsAnd(pObj) );
- Gia_ManSeqMarkUsed_rec( p, Gia_ObjFanin0(pObj), vRoots );
- Gia_ManSeqMarkUsed_rec( p, Gia_ObjFanin1(pObj), vRoots );
+ return 1 + Gia_ManSeqMarkUsed_rec( p, Gia_ObjFanin0(pObj), vRoots )
+ + Gia_ManSeqMarkUsed_rec( p, Gia_ObjFanin1(pObj), vRoots );
}
/**Function*************************************************************
- Synopsis [Performs sequential cleanup.]
+ Synopsis [Marks CIs/COs/ANDs unreachable from POs.]
Description []
@@ -130,19 +127,38 @@ void Gia_ManSeqMarkUsed_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRoots
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p )
+int Gia_ManSeqMarkUsed( Gia_Man_t * p )
{
Vec_Int_t * vRoots;
Gia_Obj_t * pObj;
- int i;
+ int i, nNodes = 0;
Gia_ManSetMark0( p );
Gia_ManConst0(p)->fMark0 = 0;
Gia_ManForEachPi( p, pObj, i )
pObj->fMark0 = 0;
+ Gia_ManForEachPo( p, pObj, i )
+ pObj->fMark0 = 0;
vRoots = Gia_ManCollectPoIds( p );
Gia_ManForEachObjVec( vRoots, p, pObj, i )
- Gia_ManSeqMarkUsed_rec( p, pObj, vRoots );
+ nNodes += Gia_ManSeqMarkUsed_rec( p, pObj, vRoots );
Vec_IntFree( vRoots );
+ return nNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs sequential cleanup.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p )
+{
+ Gia_ManSeqMarkUsed( p );
return Gia_ManDupMarked( p );
}
diff --git a/src/aig/gia/giaSort.c b/src/aig/gia/giaSort.c
index aec98fd8..8574297d 100644
--- a/src/aig/gia/giaSort.c
+++ b/src/aig/gia/giaSort.c
@@ -245,12 +245,15 @@ void minisat_sort3(float* array, int* perm, int size)
SeeAlso []
***********************************************************************/
-int * Gia_SortFloats( float * pArray, int nSize )
+int * Gia_SortFloats( float * pArray, int * pPerm, int nSize )
{
- int i, * pPerm;
- pPerm = ABC_ALLOC( int, nSize );
- for ( i = 0; i < nSize; i++ )
- pPerm[i] = i;
+ int i;
+ if ( pPerm == NULL )
+ {
+ pPerm = ABC_ALLOC( int, nSize );
+ for ( i = 0; i < nSize; i++ )
+ pPerm[i] = i;
+ }
minisat_sort3( pArray, pPerm, nSize );
// for ( i = 1; i < nSize; i++ )
// assert( pArray[i-1] <= pArray[i] );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 64f191f1..cc1a3861 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -300,6 +300,34 @@ void Gia_ManCreateRefs( Gia_Man_t * p )
/**Function*************************************************************
+ Synopsis [Assigns references.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Gia_ManCreateMuxRefs( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj, * pCtrl, * pFan0, * pFan1;
+ int i, * pMuxRefs;
+ pMuxRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
+ Gia_ManForEachObj( p, pObj, i )
+ {
+ if ( Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) )
+ continue;
+ if ( !Gia_ObjIsMuxType(pObj) )
+ continue;
+ pCtrl = Gia_ObjRecognizeMux( pObj, &pFan0, &pFan1 );
+ pMuxRefs[ Gia_ObjId(p, Gia_Regular(pCtrl)) ]++;
+ }
+ return pMuxRefs;
+}
+
+/**Function*************************************************************
+
Synopsis [Computes the maximum frontier size.]
Description []
@@ -549,6 +577,45 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
return NULL;
}
+
+/**Function*************************************************************
+
+ Synopsis [Resimulates the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDoubleOuts )
+{
+ Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+ int RetValue, i, k, iBit = 0;
+ Gia_ManForEachRo( pAig, pObj, i )
+ pObj->fMark0 = Aig_InfoHasBit(p->pData, iBit++);
+ for ( i = 0; i <= p->iFrame; i++ )
+ {
+ Gia_ManForEachPi( pAig, pObj, k )
+ pObj->fMark0 = Aig_InfoHasBit(p->pData, iBit++);
+ Gia_ManForEachAnd( pAig, pObj, k )
+ pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
+ (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+ Gia_ManForEachCo( pAig, pObj, k )
+ pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+ Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
+ pObjRo->fMark0 = pObjRi->fMark0;
+ }
+ assert( iBit == p->nBits );
+ if ( fDoubleOuts )
+ RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
+ else
+ RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
+ Gia_ManCleanMark0(pAig);
+ return RetValue;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 7a68b554..4410b497 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -5,6 +5,8 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaDfs.c \
src/aig/gia/giaDup.c \
src/aig/gia/giaEmbed.c \
+ src/aig/gia/giaEnable.c \
+ src/aig/gia/giaEquiv.c \
src/aig/gia/giaFanout.c \
src/aig/gia/giaForce.c \
src/aig/gia/giaFrames.c \
@@ -12,6 +14,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaGlitch.c \
src/aig/gia/giaHash.c \
src/aig/gia/giaMan.c \
+ src/aig/gia/giaMap.c \
src/aig/gia/giaScl.c \
src/aig/gia/giaSim.c \
src/aig/gia/giaSort.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 19:18:34 +0000