summaryrefslogtreecommitdiffstats
path: root/src/aig/gia
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia')
-rw-r--r--src/aig/gia/gia.h59
-rw-r--r--src/aig/gia/giaAig.c2
-rw-r--r--src/aig/gia/giaAig.h62
-rw-r--r--src/aig/gia/giaAiger.c6
-rw-r--r--src/aig/gia/giaCSat.c3
-rw-r--r--src/aig/gia/giaCof.c4
-rw-r--r--src/aig/gia/giaDup.c38
-rw-r--r--src/aig/gia/giaEmbed.c20
-rw-r--r--src/aig/gia/giaEnable.c6
-rw-r--r--src/aig/gia/giaEquiv.c68
-rw-r--r--src/aig/gia/giaFanout.c2
-rw-r--r--src/aig/gia/giaForce.c6
-rw-r--r--src/aig/gia/giaFrames.c4
-rw-r--r--src/aig/gia/giaFront.c2
-rw-r--r--src/aig/gia/giaGlitch.c18
-rw-r--r--src/aig/gia/giaHash.c33
-rw-r--r--src/aig/gia/giaMan.c1
-rw-r--r--src/aig/gia/giaRetime.c2
-rw-r--r--src/aig/gia/giaSat.c2
-rw-r--r--src/aig/gia/giaSim.c112
-rw-r--r--src/aig/gia/giaSwitch.c29
-rw-r--r--src/aig/gia/giaTsim.c22
-rw-r--r--src/aig/gia/giaUtil.c199
23 files changed, 570 insertions, 130 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 5395f361..feee5472 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -24,8 +24,14 @@
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
-
-#include "aig.h"
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@@ -124,6 +130,7 @@ struct Gia_Man_t_
int nFansAlloc; // the size of fanout representation
int * pMapping; // mapping for each node
Gia_Cex_t * pCexComb; // combinational counter-example
+ Gia_Cex_t * pCexSeq; // sequential counter-example
int * pCopies; // intermediate copies
Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc
unsigned char* pSwitching; // switching activity for each object
@@ -174,6 +181,36 @@ extern void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p );
extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
+static inline int Gia_IntAbs( int n ) { return (n < 0)? -n : n; }
+static inline int Gia_Float2Int( float Val ) { return *((int *)&Val); }
+static inline float Gia_Int2Float( int Num ) { return *((float *)&Num); }
+static inline int Gia_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
+static inline int Gia_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
+static inline char * Gia_UtilStrsav( char * s ) { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; }
+static inline int Gia_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
+static inline int Gia_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+static inline int Gia_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
+static inline void Gia_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
+static inline void Gia_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
+static inline unsigned Gia_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
+static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
+static inline int Gia_WordCountOnes( unsigned uWord )
+{
+ uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
+ uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
+ uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
+ uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
+ return (uWord & 0x0000FFFF) + (uWord>>16);
+}
+static inline int Gia_WordFindFirstBit( unsigned uWord )
+{
+ int i;
+ for ( i = 0; i < 32; i++ )
+ if ( uWord & (1 << i) )
+ return i;
+ return -1;
+}
+
static inline int Gia_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
static inline int Gia_Lit2Var( int Lit ) { return Lit >> 1; }
@@ -265,8 +302,8 @@ static inline int Gia_ObjValue( Gia_Obj_t * pObj ) {
static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(p->pLevels);return p->pLevels[Gia_ObjId(p, pObj)]; }
static inline int Gia_ObjRefs( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]; }
-static inline void Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); p->pRefs[Gia_ObjId(p, pObj)]++; }
-static inline void Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); p->pRefs[Gia_ObjId(p, pObj)]--; }
+static inline int Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]++; }
+static inline int Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return --p->pRefs[Gia_ObjId(p, pObj)]; }
static inline void Gia_ObjRefFanin0Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin0(pObj)); }
static inline void Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin1(pObj)); }
static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj)); }
@@ -368,6 +405,7 @@ static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { p
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 void Gia_ObjUnsetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 0; }
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; }
@@ -451,10 +489,6 @@ static inline int * Gia_ObjGateFanins( Gia_Man_t * p, int Id ) { re
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-/*=== giaAig.c =============================================================*/
-extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
-extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
-extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p );
/*=== giaAiger.c ===========================================================*/
extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck );
extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
@@ -509,6 +543,7 @@ extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
+extern void Gia_ManEquivImprove( Gia_Man_t * p );
/*=== 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 );
@@ -530,7 +565,7 @@ extern int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
extern int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 );
extern int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 );
extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 );
-extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash );
extern void Gia_ManHashProfile( Gia_Man_t * p );
/*=== giaLogic.c ===========================================================*/
extern void Gia_ManTestDistance( Gia_Man_t * p );
@@ -567,6 +602,10 @@ extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames,
/*=== giaTsim.c ============================================================*/
extern Gia_Man_t * Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose );
/*=== giaUtil.c ===========================================================*/
+extern unsigned Gia_ManRandom( int fReset );
+extern void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop );
+extern unsigned int Gia_PrimeCudd( unsigned int p );
+extern char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix );
extern void Gia_ManSetMark0( Gia_Man_t * p );
extern void Gia_ManCleanMark0( Gia_Man_t * p );
extern void Gia_ManCheckMark0( Gia_Man_t * p );
@@ -589,7 +628,7 @@ extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t **
extern Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut );
extern void Gia_ManPrintCounterExample( Gia_Cex_t * p );
-
+extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
#ifdef __cplusplus
}
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 1c341d6f..601b85af 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "gia.h"
+#include "giaAig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
new file mode 100644
index 00000000..07cf7bae
--- /dev/null
+++ b/src/aig/gia/giaAig.h
@@ -0,0 +1,62 @@
+/**CFile****************************************************************
+
+ FileName [giaAig.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaAig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __GIA_AIG_H__
+#define __GIA_AIG_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig.h"
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== giaAig.c =============================================================*/
+extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
+extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
+extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index adc58e6c..8dbc0cab 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -143,7 +143,7 @@ int Gia_FileSize( char * pFileName )
char * Gia_FileNameGeneric( char * FileName )
{
char * pDot, * pRes;
- pRes = Aig_UtilStrsav( FileName );
+ pRes = Gia_UtilStrsav( FileName );
if ( (pDot = strrchr( pRes, '.' )) )
*pDot = 0;
return pRes;
@@ -412,7 +412,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
// allocate the empty AIG
pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
pName = Gia_FileNameGeneric( pFileName );
- pNew->pName = Aig_UtilStrsav( pName );
+ pNew->pName = Gia_UtilStrsav( pName );
// pNew->pSpec = Aig_UtilStrsav( pFileName );
ABC_FREE( pName );
@@ -549,7 +549,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
pCur++;
// read model name
ABC_FREE( pNew->pName );
- pNew->pName = Aig_UtilStrsav( pCur );
+ pNew->pName = Gia_UtilStrsav( pCur );
}
}
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 15faea72..832eff26 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -20,6 +20,9 @@
#include "gia.h"
+//#define gia_assert(exp) ((void)0)
+//#define gia_assert(exp) (assert(exp))
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c
index b256100c..da48c1b0 100644
--- a/src/aig/gia/giaCof.c
+++ b/src/aig/gia/giaCof.c
@@ -580,7 +580,7 @@ void Cof_ManPrintFanio( Cof_Man_t * p )
}
// allocate storage for fanin/fanout numbers
- nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
+ nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );
@@ -714,7 +714,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
return NULL;
}
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 2510f572..bd5297e4 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -168,7 +168,7 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@@ -200,7 +200,7 @@ Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCoReverse( p, pObj, i )
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@@ -232,7 +232,7 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -265,7 +265,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
@@ -297,7 +297,7 @@ Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i, iCtrl;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
@@ -337,7 +337,7 @@ Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass )
int i, Counter1 = 0, Counter2 = 0;
assert( p->vFlopClasses != NULL );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
@@ -381,7 +381,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
int i, nRos = 0, nRis = 0;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
@@ -426,7 +426,7 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
int i, t, Entry;
assert( nTimes > 0 );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
vPis = Vec_IntAlloc( Gia_ManPiNum(p) * nTimes );
vPos = Vec_IntAlloc( Gia_ManPoNum(p) * nTimes );
@@ -536,7 +536,7 @@ Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupDfs2_rec( pNew, p, pObj );
@@ -594,7 +594,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@@ -625,7 +625,7 @@ Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -655,7 +655,7 @@ Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot )
assert( Gia_ObjIsCo(pRoot) );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -682,7 +682,7 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
int i, iLit, iLitRes;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -712,7 +712,7 @@ Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -743,7 +743,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManSetRefs( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@@ -797,7 +797,7 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
{
@@ -847,7 +847,7 @@ Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p )
assert( p->pReprsOld != NULL );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -1064,7 +1064,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq
}
// start the manager
pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) );
- pNew->pName = Aig_UtilStrsav( "miter" );
+ pNew->pName = Gia_UtilStrsav( "miter" );
// map combinational inputs
Gia_ManFillValue( p0 );
Gia_ManFillValue( p1 );
@@ -1161,7 +1161,7 @@ Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p )
int i, iLit;
assert( (Gia_ManPoNum(p) & 1) == 0 );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManHashAlloc( pNew );
Gia_ManForEachCi( p, pObj, i )
diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c
index fa172f70..bd14eea9 100644
--- a/src/aig/gia/giaEmbed.c
+++ b/src/aig/gia/giaEmbed.c
@@ -691,7 +691,7 @@ void Emb_ManPrintFanio( Emb_Man_t * p )
}
// allocate storage for fanin/fanout numbers
- nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
+ nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );
@@ -836,14 +836,14 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
int nAttempts = 20;
int i, iNode, Dist, clk;
Emb_Obj_t * pPivot, * pNext;
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
Emb_ManResetTravId( p );
// compute distances from several randomly selected PIs
clk = clock();
printf( "From inputs: " );
for ( i = 0; i < nAttempts; i++ )
{
- iNode = Aig_ManRandom( 0 ) % Emb_ManCiNum(p);
+ iNode = Gia_ManRandom( 0 ) % Emb_ManCiNum(p);
pPivot = Emb_ManCi( p, iNode );
if ( Emb_ObjFanoutNum(pPivot) == 0 )
{ i--; continue; }
@@ -859,7 +859,7 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
printf( "From outputs: " );
for ( i = 0; i < nAttempts; i++ )
{
- iNode = Aig_ManRandom( 0 ) % Emb_ManCoNum(p);
+ iNode = Gia_ManRandom( 0 ) % Emb_ManCoNum(p);
pPivot = Emb_ManCo( p, iNode );
pNext = Emb_ObjFanin( pPivot, 0 );
if ( !Emb_ObjIsNode(pNext) )
@@ -873,7 +873,7 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
printf( "From nodes: " );
for ( i = 0; i < nAttempts; i++ )
{
- iNode = Aig_ManRandom( 0 ) % Gia_ManObjNum(p->pGia);
+ iNode = Gia_ManRandom( 0 ) % Gia_ManObjNum(p->pGia);
if ( !~Gia_ManObj(p->pGia, iNode)->Value )
{ i--; continue; }
pPivot = Emb_ManObj( p, Gia_ManObj(p->pGia, iNode)->Value );
@@ -1043,7 +1043,7 @@ Emb_Obj_t * Emb_ManRandomVertex( Emb_Man_t * p )
{
Emb_Obj_t * pPivot;
do {
- int iNode = (911 * Aig_ManRandom(0)) % Gia_ManObjNum(p->pGia);
+ int iNode = (911 * Gia_ManRandom(0)) % Gia_ManObjNum(p->pGia);
if ( ~Gia_ManObj(p->pGia, iNode)->Value )
pPivot = Emb_ManObj( p, Gia_ManObj(p->pGia, iNode)->Value );
else
@@ -1240,7 +1240,7 @@ void Emb_ManVecRandom( float * pVec, int nDims )
{
int i;
for ( i = 0; i < nDims; i++ )
- pVec[i] = Aig_ManRandom( 0 );
+ pVec[i] = Gia_ManRandom( 0 );
}
/**Function*************************************************************
@@ -1702,7 +1702,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI
printf( "Emb_ManDumpGnuplot(): Placement is not available.\n" );
return;
}
- sprintf( Buffer, "%s%s", pDirectory, Aig_FileNameGenericAppend(pName, ".plt") );
+ sprintf( Buffer, "%s%s", pDirectory, Gia_FileNameGenericAppend(pName, ".plt") );
pFile = fopen( Buffer, "w" );
fprintf( pFile, "# This Gnuplot file was produced by ABC on %s\n", Ioa_TimeStamp() );
fprintf( pFile, "\n" );
@@ -1712,7 +1712,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI
{
// fprintf( pFile, "set terminal postscript\n" );
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, "set output \'%s\'\n", Gia_FileNameGenericAppend(pName, ".gif") );
fprintf( pFile, "\n" );
}
fprintf( pFile, "set title \"%s : PI = %d PO = %d FF = %d Node = %d Obj = %d HPWL = %.2e\\n",
@@ -1806,7 +1806,7 @@ clk = clock();
// Emb_ManPrintFanio( p );
// prepare data-structure
- Aig_ManRandom( 1 ); // reset random numbers for deterministic behavior
+ Gia_ManRandom( 1 ); // reset random numbers for deterministic behavior
Emb_ManResetTravId( p );
Emb_ManSetValue( p );
clkSetup = clock() - clk;
diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c
index 13d6145c..c768bb43 100644
--- a/src/aig/gia/giaEnable.c
+++ b/src/aig/gia/giaEnable.c
@@ -362,7 +362,7 @@ Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames )
ABC_FREE( p->pCopies );
p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
Gia_ObjSetCopyF( p, 0, pObj, 0 );
@@ -437,7 +437,7 @@ Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p )
Gia_Obj_t * pThis, * pNode;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
@@ -607,7 +607,7 @@ Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p )
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 79345fd0..f802e15d 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -330,7 +330,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@@ -682,7 +682,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@@ -809,10 +809,10 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
if ( fDualOut )
Gia_ManEquivSetColors( p, 0 );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
- Gia_ObjSetCopyF( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) );
+ Gia_ObjSetCopyF( p, 0, pObj, Gia_InfoHasBit(pInit->pData, i) );
for ( f = 0; f < nFrames; f++ )
{
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
@@ -906,6 +906,66 @@ void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose )
nRemovedClas, nTotalClas, nRemovedLits, nTotalLits );
}
+/**Function*************************************************************
+
+ Synopsis [Transforms equiv classes by setting a good representative.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManEquivImprove( Gia_Man_t * p )
+{
+ Vec_Int_t * vClass;
+ int i, k, iNode, iRepr;
+ int iReprBest, iLevelBest, iLevelCur, iMffcBest, iMffcCur;
+ assert( p->pReprs != NULL && p->pNexts != NULL );
+ Gia_ManLevelNum( p );
+ Gia_ManCreateRefs( p );
+ // iterate over class candidates
+ vClass = Vec_IntAlloc( 100 );
+ Gia_ManForEachClass( p, i )
+ {
+ Vec_IntClear( vClass );
+ iReprBest = -1;
+ iLevelBest = iMffcBest = ABC_INFINITY;
+ Gia_ClassForEachObj( p, i, k )
+ {
+ iLevelCur = Gia_ObjLevel( p,Gia_ManObj(p, k) );
+ iMffcCur = Gia_NodeMffcSize( p, Gia_ManObj(p, k) );
+ if ( iLevelBest > iLevelCur || (iLevelBest == iLevelCur && iMffcBest > iMffcCur) )
+ {
+ iReprBest = k;
+ iLevelBest = iLevelCur;
+ iMffcBest = iMffcCur;
+ }
+ Vec_IntPush( vClass, k );
+ }
+ assert( Vec_IntSize( vClass ) > 1 );
+ assert( iReprBest > 0 );
+ if ( i == iReprBest )
+ continue;
+/*
+ printf( "Repr/Best = %6d/%6d. Lev = %3d/%3d. Mffc = %3d/%3d.\n",
+ i, iReprBest, Gia_ObjLevel( p,Gia_ManObj(p, i) ), Gia_ObjLevel( p,Gia_ManObj(p, iReprBest) ),
+ Gia_NodeMffcSize( p, Gia_ManObj(p, i) ), Gia_NodeMffcSize( p, Gia_ManObj(p, iReprBest) ) );
+*/
+ iRepr = iReprBest;
+ Gia_ObjSetRepr( p, iRepr, GIA_VOID );
+ Gia_ObjSetProved( p, i );
+ Gia_ObjUnsetProved( p, iRepr );
+ Vec_IntForEachEntry( vClass, iNode, k )
+ if ( iNode != iRepr )
+ Gia_ObjSetRepr( p, iNode, iRepr );
+ }
+ Vec_IntFree( vClass );
+ ABC_FREE( p->pNexts );
+// p->pNexts = Gia_ManDeriveNexts( p );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaFanout.c b/src/aig/gia/giaFanout.c
index 42ccd7e7..b32484af 100644
--- a/src/aig/gia/giaFanout.c
+++ b/src/aig/gia/giaFanout.c
@@ -117,7 +117,7 @@ void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout )
assert( Gia_ObjId(p, pFanout) > 0 );
if ( Gia_ObjId(p, pObj) >= p->nFansAlloc || Gia_ObjId(p, pFanout) >= p->nFansAlloc )
{
- int nFansAlloc = 2 * AIG_MAX( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) );
+ int nFansAlloc = 2 * ABC_MAX( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) );
p->pFanData = ABC_REALLOC( int, p->pFanData, 5 * nFansAlloc );
memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) );
p->nFansAlloc = nFansAlloc;
diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c
index cf4c4aa5..04c8f2e7 100644
--- a/src/aig/gia/giaForce.c
+++ b/src/aig/gia/giaForce.c
@@ -747,7 +747,7 @@ void Frc_ManPlaceRandom( Frc_Man_t * p )
pPlacement[i] = i;
for ( i = 0; i < p->nObjs; i++ )
{
- iNext = Aig_ManRandom( 0 ) % p->nObjs;
+ iNext = Gia_ManRandom( 0 ) % p->nObjs;
Temp = pPlacement[i];
pPlacement[i] = pPlacement[iNext];
pPlacement[iNext] = Temp;
@@ -774,7 +774,7 @@ void Frc_ManArrayShuffle( Vec_Int_t * vArray )
int i, iNext, Temp;
for ( i = 0; i < vArray->nSize; i++ )
{
- iNext = Aig_ManRandom( 0 ) % vArray->nSize;
+ iNext = Gia_ManRandom( 0 ) % vArray->nSize;
Temp = vArray->pArray[i];
vArray->pArray[i] = vArray->pArray[iNext];
vArray->pArray[iNext] = Temp;
@@ -1036,7 +1036,7 @@ void Frc_DumpGraphIntoFile( Frc_Man_t * p )
void For_ManExperiment( Gia_Man_t * pGia, int nIters, int fClustered, int fVerbose )
{
Frc_Man_t * p;
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
if ( fClustered )
p = Frc_ManStart( pGia );
else
diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c
index e99ef514..c0ea6680 100644
--- a/src/aig/gia/giaFrames.c
+++ b/src/aig/gia/giaFrames.c
@@ -180,7 +180,7 @@ Gia_Man_t * Gia_ManFramesInit( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
Gia_ManFraSupports( p );
pFrames = Gia_ManStart( Vec_VecSizeSize((Vec_Vec_t*)p->vIns)+
Vec_VecSizeSize((Vec_Vec_t*)p->vAnds)+Vec_VecSizeSize((Vec_Vec_t*)p->vOuts) );
- pFrames->pName = Aig_UtilStrsav( pAig->pName );
+ pFrames->pName = Gia_UtilStrsav( pAig->pName );
Gia_ManHashAlloc( pFrames );
Gia_ManConst0(pAig)->Value = 0;
for ( f = 0; f < pPars->nFrames; f++ )
@@ -290,7 +290,7 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
if ( pPars->fInit )
return Gia_ManFramesInit( pAig, pPars );
pFrames = Gia_ManStart( pPars->nFrames * Gia_ManObjNum(pAig) );
- pFrames->pName = Aig_UtilStrsav( pAig->pName );
+ pFrames->pName = Gia_UtilStrsav( pAig->pName );
Gia_ManHashAlloc( pFrames );
Gia_ManConst0(pAig)->Value = 0;
for ( f = 0; f < pPars->nFrames; f++ )
diff --git a/src/aig/gia/giaFront.c b/src/aig/gia/giaFront.c
index ee9e5b5f..b3a3c2d0 100644
--- a/src/aig/gia/giaFront.c
+++ b/src/aig/gia/giaFront.c
@@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
Gia_ManSetRefs( p );
// start the new manager
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit);
// start the frontier
pFront = ABC_CALLOC( char, pNew->nFront );
diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c
index 443a1ae8..ed636540 100644
--- a/src/aig/gia/giaGlitch.c
+++ b/src/aig/gia/giaGlitch.c
@@ -330,7 +330,7 @@ static inline int Gli_NodeComputeValue( Gli_Obj_t * pNode )
int i, Phase = 0;
for ( i = 0; i < (int)pNode->nFanins; i++ )
Phase |= (Gli_ObjFanin(pNode, i)->fPhase << i);
- return Aig_InfoHasBit( pNode->uTruth, Phase );
+ return Gia_InfoHasBit( pNode->uTruth, Phase );
}
/**Function*************************************************************
@@ -349,7 +349,7 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode )
int i, Phase = 0;
for ( i = 0; i < (int)pNode->nFanins; i++ )
Phase |= (Gli_ObjFanin(pNode, i)->fPhase2 << i);
- return Aig_InfoHasBit( pNode->uTruth, Phase );
+ return Gia_InfoHasBit( pNode->uTruth, Phase );
}
/**Function*************************************************************
@@ -429,7 +429,7 @@ void Gli_ManSetPiRandom( Gli_Man_t * p, float PiTransProb )
assert( 0.0 < PiTransProb && PiTransProb < 1.0 );
Vec_IntClear( p->vCisChanged );
Gli_ManForEachCi( p, pObj, i )
- if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb )
+ if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb )
{
Vec_IntPush( p->vCisChanged, pObj->Handle );
pObj->fPhase ^= 1;
@@ -590,7 +590,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode )
for ( k = 0; k < nFanins; k++ )
if ( (pSimInfos[k] >> i) & 1 )
Phase |= (1 << k);
- if ( Aig_InfoHasBit( pNode->uTruth, Phase ) )
+ if ( Gia_InfoHasBit( pNode->uTruth, Phase ) )
Result |= (1 << i);
}
return Result;
@@ -612,9 +612,9 @@ static inline unsigned Gli_ManUpdateRandomInput( unsigned uInfo, float PiTransPr
float Multi = 1.0 / (1 << 16);
int i;
if ( PiTransProb == 0.5 )
- return Aig_ManRandom(0);
+ return Gia_ManRandom(0);
for ( i = 0; i < 32; i++ )
- if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb )
+ if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb )
uInfo ^= (1 << i);
return uInfo;
}
@@ -703,7 +703,7 @@ void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb )
// set changed PIs
Vec_IntClear( p->vCisChanged );
Gli_ManForEachPi( p, pObj, i )
- if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb )
+ if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb )
{
Vec_IntPush( p->vCisChanged, pObj->Handle );
pObj->fPhase ^= 1;
@@ -738,7 +738,7 @@ void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb )
void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose )
{
int i, k, clk = clock();
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
Gli_ManFinalize( p );
if ( p->nRegs == 0 )
{
@@ -752,7 +752,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb
}
else
{
- int nIters = Aig_BitWordNum(nPatterns);
+ int nIters = Gia_BitWordNum(nPatterns);
Gli_ManSimulateSeqPref( p, 16 );
for ( i = 0; i < 32; i++ )
{
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index a7cae8fe..97326c92 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -86,7 +86,7 @@ static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1 )
void Gia_ManHashAlloc( Gia_Man_t * p )
{
assert( p->pHTable == NULL );
- p->nHTable = Aig_PrimeCudd( p->nObjsAlloc );
+ p->nHTable = Gia_PrimeCudd( p->nObjsAlloc );
p->pHTable = ABC_CALLOC( int, p->nHTable );
}
@@ -152,7 +152,7 @@ void Gia_ManHashResize( Gia_Man_t * p )
// replace the table
pHTableOld = p->pHTable;
nHTableOld = p->nHTable;
- p->nHTable = Aig_PrimeCudd( 2 * Gia_ManAndNum(p) );
+ p->nHTable = Gia_PrimeCudd( 2 * Gia_ManAndNum(p) );
p->pHTable = ABC_CALLOC( int, p->nHTable );
// rehash the entries from the old table
Counter = 0;
@@ -322,14 +322,14 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O
{
Gia_Obj_t * pNode0, * pNode1, * pFanA, * pFanB, * pFanC, * pFanD;
assert( p->fAddStrash );
- if ( !Gia_ObjIsAnd(Gia_Regular(p0)) && !Gia_ObjIsAnd(Gia_Regular(p1)) )
- return NULL;
pNode0 = Gia_Regular(p0);
pNode1 = Gia_Regular(p1);
- pFanA = Gia_ObjChild0(pNode0);
- pFanB = Gia_ObjChild1(pNode0);
- pFanC = Gia_ObjChild0(pNode1);
- pFanD = Gia_ObjChild1(pNode1);
+ if ( !Gia_ObjIsAnd(pNode0) && !Gia_ObjIsAnd(pNode1) )
+ return NULL;
+ pFanA = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild0(pNode0) : NULL;
+ pFanB = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild1(pNode0) : NULL;
+ pFanC = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild0(pNode1) : NULL;
+ pFanD = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild1(pNode1) : NULL;
if ( Gia_IsComplement(p0) )
{
if ( pFanA == Gia_Not(p1) || pFanB == Gia_Not(p1) )
@@ -404,6 +404,7 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O
if ( pFanB == pFanD && pFanA == Gia_Not(pFanC) )
return Gia_Not(pFanB);
}
+/*
if ( !Gia_IsComplement(p0) || !Gia_IsComplement(p1) )
return NULL;
if ( !Gia_ObjIsAnd(pNode0) || !Gia_ObjIsAnd(pNode1) )
@@ -424,8 +425,12 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O
}
pNode0 = Gia_ManHashAndP( p, Gia_Not(pNodeC), pNodeE );
pNode1 = Gia_ManHashAndP( p, pNodeC, pNodeT );
- return Gia_NotCond( Gia_ManHashAndP( p, pNode0, pNode1 ), !fCompl );
+ p->fAddStrash = 0;
+ pNodeC = Gia_NotCond( Gia_ManHashAndP( p, Gia_Not(pNode0), Gia_Not(pNode1) ), !fCompl );
+ p->fAddStrash = 1;
+ return pNodeC;
}
+*/
return NULL;
}
@@ -555,13 +560,14 @@ int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManRehash( Gia_Man_t * p )
+Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash )
{
- Gia_Man_t * pNew;
+ Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
+ pNew->fAddStrash = fAddStrash;
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj( p, pObj, i )
@@ -574,8 +580,11 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
Gia_ManHashStop( pNew );
+ pNew->fAddStrash = 0;
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
// printf( "Top gate is %s\n", Gia_ObjFaninC0(Gia_ManCo(pNew, 0))? "OR" : "AND" );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
return pNew;
}
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index dba90507..f69ac266 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -72,6 +72,7 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_IntFree( p->vCos );
ABC_FREE( p->pPlacement );
ABC_FREE( p->pSwitching );
+ ABC_FREE( p->pCexSeq );
ABC_FREE( p->pCexComb );
ABC_FREE( p->pIso );
ABC_FREE( p->pMapping );
diff --git a/src/aig/gia/giaRetime.c b/src/aig/gia/giaRetime.c
index 965b5981..69dea59d 100644
--- a/src/aig/gia/giaRetime.c
+++ b/src/aig/gia/giaRetime.c
@@ -122,7 +122,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut )
int i;
// create the new manager
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
// create the true PIs
Gia_ManFillValue( p );
diff --git a/src/aig/gia/giaSat.c b/src/aig/gia/giaSat.c
index 6d127223..29ade5c6 100644
--- a/src/aig/gia/giaSat.c
+++ b/src/aig/gia/giaSat.c
@@ -262,7 +262,7 @@ int Gia_ManSatPartCount( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnLeaves, int *
(*pnLeaves)++;
else
Level1 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC1(pObj);
- return AIG_MAX( Level0, Level1 );
+ return ABC_MAX( Level0, Level1 );
}
/**Function*************************************************************
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 020683ad..ae9e304c 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -64,7 +64,7 @@ void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p )
p->nIters = 32; // the number of timeframes
p->TimeLimit = 60; // time limit in seconds
p->fCheckMiter = 0; // check if miter outputs are non-zero
- p->fVerbose = 1; // enables verbose output
+ p->fVerbose = 0; // enables verbose output
}
/**Function*************************************************************
@@ -92,7 +92,7 @@ Gia_ManSim_t * Gia_ManSimCreate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * Gia_ManCoNum(p->pAig) );
p->vCis2Ids = Vec_IntAlloc( Gia_ManCiNum(p->pAig) );
Vec_IntForEachEntry( pAig->vCis, Entry, i )
- Vec_IntPush( p->vCis2Ids, Entry );
+ Vec_IntPush( p->vCis2Ids, i ); // do we need p->vCis2Ids?
printf( "AIG = %7.2f Mb. Front mem = %7.2f Mb. Other mem = %7.2f Mb.\n",
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
4.0*p->nWords*p->pAig->nFront/(1<<20),
@@ -136,7 +136,7 @@ static inline void Gia_ManSimInfoRandom( Gia_ManSim_t * p, unsigned * pInfo )
{
int w;
for ( w = p->nWords-1; w >= 0; w-- )
- pInfo[w] = Aig_ManRandom( 0 );
+ pInfo[w] = Gia_ManRandom( 0 );
}
/**Function*************************************************************
@@ -173,7 +173,7 @@ static inline int Gia_ManSimInfoIsZero( Gia_ManSim_t * p, unsigned * pInfo )
int w;
for ( w = p->nWords-1; w >= 0; w-- )
if ( pInfo[w] )
- return 32*(w-1) + Aig_WordFindFirstBit( pInfo[w] );
+ return 32*(w-1) + Gia_WordFindFirstBit( pInfo[w] );
return -1;
}
@@ -382,6 +382,71 @@ static inline void Gia_ManSimulateRound( Gia_ManSim_t * p )
/**Function*************************************************************
+ Synopsis [Returns index of the PO and pattern that failed it.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Gia_ManCheckPos( Gia_ManSim_t * p, int * piPo, int * piPat )
+{
+ int i, iPat;
+ for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
+ {
+ iPat = Gia_ManSimInfoIsZero( p, Gia_SimDataCo(p, i) );
+ if ( iPat >= 0 )
+ {
+ *piPo = i;
+ *piPat = iPat;
+ return 1;
+ }
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids )
+{
+ Gia_Cex_t * p;
+ unsigned * pData;
+ int f, i, w, iPioId, Counter;
+ p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
+ p->iFrame = iFrame;
+ p->iPo = iOut;
+ // fill in the binary data
+ Gia_ManRandom( 1 );
+ Counter = p->nRegs;
+ pData = ABC_ALLOC( unsigned, nWords );
+ for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
+ for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
+ {
+ iPioId = Vec_IntEntry( vCis2Ids, i );
+ if ( iPioId >= p->nPis )
+ continue;
+ for ( w = nWords-1; w >= 0; w-- )
+ pData[w] = Gia_ManRandom( 0 );
+ if ( Gia_InfoHasBit( pData, iPat ) )
+ Gia_InfoSetBit( p->pData, Counter + iPioId );
+ }
+ ABC_FREE( pData );
+ return p;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -394,40 +459,53 @@ static inline void Gia_ManSimulateRound( Gia_ManSim_t * p )
int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
{
Gia_ManSim_t * p;
- int i, clk = clock();
+ int i, clkTotal = clock();
+ int iOut, iPat, RetValue = 0;
+ ABC_FREE( pAig->pCexSeq );
p = Gia_ManSimCreate( pAig, pPars );
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
Gia_ManSimInfoInit( p );
for ( i = 0; i < pPars->nIters; i++ )
{
Gia_ManSimulateRound( p );
-/*
+
if ( pPars->fVerbose )
{
printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
- printf( "Time = %7.2f sec\r", (1.0*clock()-clk)/CLOCKS_PER_SEC );
+ printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
}
if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
{
- assert( pAig->pSeqModel == NULL );
- pAig->pSeqModel = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
- if ( pPars->fVerbose )
- printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
+ pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", iOut, i );
+ if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
+ {
+ printf( "\n" );
+ printf( "Generated counter-example is INVALID \n" );
+ printf( "\n" );
+ }
+ else
+ {
+ printf( "\n" );
+ printf( "Generated counter-example is fine \n" );
+ printf( "\n" );
+ }
+ RetValue = 1;
break;
}
if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
{
- printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, pPars->TimeLimit );
+ printf( "No bug detected after %d frames with time limit %d seconds. \n", i+1, pPars->TimeLimit );
break;
}
-*/
+
if ( i < pPars->nIters - 1 )
Gia_ManSimInfoTransfer( p );
}
Gia_ManSimDelete( p );
- printf( "Simulated %d frames with %d words. ", pPars->nIters, pPars->nWords );
- ABC_PRT( "Time", clock() - clk );
- return 0;
+ printf( "Simulated %d frames with %d words. ", i, pPars->nWords );
+ ABC_PRT( "Time", clock() - clkTotal );
+ return RetValue;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c
index 713f224b..5dac1fbc 100644
--- a/src/aig/gia/giaSwitch.c
+++ b/src/aig/gia/giaSwitch.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "gia.h"
+#include "giaAig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -146,23 +146,23 @@ static inline void Gia_ManSwiSimInfoRandom( Gia_ManSwi_t * p, unsigned * pInfo,
int w, i;
if ( nProbNum == -1 )
{ // 3/8 = 1/4 + 1/8
- Mask = (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 )) |
- (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ));
+ Mask = (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 )) |
+ (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ));
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] ^= Mask;
}
else if ( nProbNum > 0 )
{
- Mask = Aig_ManRandom( 0 );
+ Mask = Gia_ManRandom( 0 );
for ( i = 0; i < nProbNum; i++ )
- Mask &= Aig_ManRandom( 0 );
+ Mask &= Gia_ManRandom( 0 );
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] ^= Mask;
}
else if ( nProbNum == 0 )
{
for ( w = p->nWords-1; w >= 0; w-- )
- pInfo[w] = Aig_ManRandom( 0 );
+ pInfo[w] = Gia_ManRandom( 0 );
}
else
assert( 0 );
@@ -185,14 +185,14 @@ static inline void Gia_ManSwiSimInfoRandomShift( Gia_ManSwi_t * p, unsigned * pI
int w, i;
if ( nProbNum == -1 )
{ // 3/8 = 1/4 + 1/8
- Mask = (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 )) |
- (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ));
+ Mask = (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 )) |
+ (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ));
}
else if ( nProbNum >= 0 )
{
- Mask = Aig_ManRandom( 0 );
+ Mask = Gia_ManRandom( 0 );
for ( i = 0; i < nProbNum; i++ )
- Mask &= Aig_ManRandom( 0 );
+ Mask &= Gia_ManRandom( 0 );
}
else
assert( 0 );
@@ -430,7 +430,7 @@ static inline int Gia_ManSwiSimInfoCountOnes( Gia_ManSwi_t * p, int iPlace )
int w, Counter = 0;
pInfo = Gia_SwiData( p, iPlace );
for ( w = p->nWords-1; w >= 0; w-- )
- Counter += Aig_WordCountOnes( pInfo[w] );
+ Counter += Gia_WordCountOnes( pInfo[w] );
return Counter;
}
@@ -451,7 +451,7 @@ static inline int Gia_ManSwiSimInfoCountTrans( Gia_ManSwi_t * p, int iPlace )
int w, Counter = 0;
pInfo = Gia_SwiData( p, iPlace );
for ( w = p->nWords-1; w >= 0; w-- )
- Counter += 2*Aig_WordCountOnes( (pInfo[w] ^ (pInfo[w] >> 16)) & 0xffff );
+ Counter += 2*Gia_WordCountOnes( (pInfo[w] ^ (pInfo[w] >> 16)) & 0xffff );
return Counter;
}
@@ -565,7 +565,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
{
printf( "Obj = %8d (%8d). F = %6d. ",
pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront,
- 4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
+ 4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ",
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
4.0*p->nWords*p->pAig->nFront/(1<<20),
@@ -573,7 +573,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
ABC_PRT( "Time", clock() - clk );
}
// perform simulation
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
Gia_ManSwiSimInfoInit( p );
for ( i = 0; i < pPars->nIters; i++ )
{
@@ -612,7 +612,6 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
return vSwitching;
}
-
/**Function*************************************************************
Synopsis [Computes probability of switching (or of being 1).]
diff --git a/src/aig/gia/giaTsim.c b/src/aig/gia/giaTsim.c
index 8cfe5959..a4cdf88a 100644
--- a/src/aig/gia/giaTsim.c
+++ b/src/aig/gia/giaTsim.c
@@ -81,15 +81,15 @@ Gia_ManTer_t * Gia_ManTerCreate( Gia_Man_t * pAig )
p = ABC_CALLOC( Gia_ManTer_t, 1 );
p->pAig = Gia_ManFront( pAig );
p->nIters = 300;
- p->pDataSim = ABC_ALLOC( unsigned, Aig_BitWordNum(2*p->pAig->nFront) );
- p->pDataSimCis = ABC_ALLOC( unsigned, Aig_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
- p->pDataSimCos = ABC_ALLOC( unsigned, Aig_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
+ p->pDataSim = ABC_ALLOC( unsigned, Gia_BitWordNum(2*p->pAig->nFront) );
+ p->pDataSimCis = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
+ p->pDataSimCos = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
// allocate storage for terminary states
- p->nStateWords = Aig_BitWordNum( 2*Gia_ManRegNum(pAig) );
+ p->nStateWords = Gia_BitWordNum( 2*Gia_ManRegNum(pAig) );
p->vStates = Vec_PtrAlloc( 1000 );
p->pCount0 = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
p->pCountX = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
- p->nBins = Aig_PrimeCudd( 500 );
+ p->nBins = Gia_PrimeCudd( 500 );
p->pBins = ABC_CALLOC( unsigned *, p->nBins );
p->vRetired = Vec_IntAlloc( 100 );
p->pRetired = ABC_CALLOC( char, Gia_ManRegNum(pAig) );
@@ -508,7 +508,7 @@ void Gia_ManTerAnalyze2( Vec_Ptr_t * vStates, int nRegs )
unsigned * pTemp, * pStates = Vec_PtrPop( vStates );
int i, w, nZeros, nConsts, nStateWords;
// detect constant zero registers
- nStateWords = Aig_BitWordNum( 2*nRegs );
+ nStateWords = Gia_BitWordNum( 2*nRegs );
memset( pStates, 0, sizeof(int) * nStateWords );
Vec_PtrForEachEntry( vStates, pTemp, i )
for ( w = 0; w < nStateWords; w++ )
@@ -576,7 +576,7 @@ Vec_Ptr_t * Gia_ManTerTranspose( Gia_ManTer_t * p )
unsigned * pState, * pFlop;
int i, k, nFlopWords;
vFlops = Vec_PtrAlloc( 100 );
- nFlopWords = Aig_BitWordNum( 2*Vec_PtrSize(p->vStates) );
+ nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) );
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
if ( p->pCount0[i] == Vec_PtrSize(p->vStates) )
@@ -631,7 +631,7 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p, int fVerbose )
Gia_Obj_t * pObj;
Vec_Int_t * vMapKtoI;
int i, iRepr, nFlopWords, Counter0 = 0, CounterE = 0;
- nFlopWords = Aig_BitWordNum( 2*Vec_PtrSize(p->vStates) );
+ nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) );
p->vFlops = Gia_ManTerTranspose( p );
pCi2Lit = ABC_FALLOC( unsigned, Gia_ManCiNum(p->pAig) );
vMapKtoI = Vec_IntAlloc( 100 );
@@ -679,11 +679,11 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
{
printf( "Obj = %8d (%8d). F = %6d. ",
pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront,
- 4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
+ 4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ",
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
- 4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20),
- 4.0*Aig_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) );
+ 4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20),
+ 4.0*Gia_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) );
ABC_PRT( "Time", clock() - clk );
}
// perform simulation
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 822f1e64..5716c1a0 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -23,6 +23,9 @@
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+
+#define NUMBER1 3716960521u
+#define NUMBER2 2174103536u
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -30,6 +33,113 @@
/**Function*************************************************************
+ Synopsis [Creates a sequence or random numbers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
+
+***********************************************************************/
+unsigned Gia_ManRandom( int fReset )
+{
+ static unsigned int m_z = NUMBER1;
+ static unsigned int m_w = NUMBER2;
+ if ( fReset )
+ {
+ m_z = NUMBER1;
+ m_w = NUMBER2;
+ }
+ m_z = 36969 * (m_z & 65535) + (m_z >> 16);
+ m_w = 18000 * (m_w & 65535) + (m_w >> 16);
+ return (m_z << 16) + m_w;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Creates random info for the primary inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop )
+{
+ unsigned * pInfo;
+ int i, w;
+ Vec_PtrForEachEntryStart( vInfo, pInfo, i, iInputStart )
+ for ( w = iWordStart; w < iWordStop; w++ )
+ pInfo[w] = Gia_ManRandom(0);
+}
+
+/**Function********************************************************************
+
+ Synopsis [Returns the next prime >= p.]
+
+ Description [Copied from CUDD, for stand-aloneness.]
+
+ SideEffects [None]
+
+ SeeAlso []
+
+******************************************************************************/
+unsigned int Gia_PrimeCudd( unsigned int p )
+{
+ int i,pn;
+
+ p--;
+ do {
+ p++;
+ if (p&1) {
+ pn = 1;
+ i = 3;
+ while ((unsigned) (i * i) <= p) {
+ if (p % i == 0) {
+ pn = 0;
+ break;
+ }
+ i += 2;
+ }
+ } else {
+ pn = 0;
+ }
+ } while (!pn);
+ return(p);
+
+} /* end of Cudd_Prime */
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns the composite name of the file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix )
+{
+ static char Buffer[1000];
+ char * pDot;
+ strcpy( Buffer, pBase );
+ if ( (pDot = strrchr( Buffer, '.' )) )
+ *pDot = 0;
+ strcat( Buffer, pSuffix );
+ if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) )
+ return pDot+1;
+ return Buffer;
+}
+
+/**Function*************************************************************
+
Synopsis [Sets phases of the internal nodes.]
Description []
@@ -592,7 +702,7 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames )
{
Gia_Cex_t * pCex;
- int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
+ int nWords = Gia_BitWordNum( nRegs + nRealPis * nFrames );
pCex = (Gia_Cex_t *)ABC_ALLOC( char, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords );
memset( pCex, 0, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords );
pCex->nRegs = nRegs;
@@ -617,11 +727,11 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut )
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
Gia_ManForEachRo( pAig, pObj, i )
- pObj->fMark0 = Aig_InfoHasBit(p->pData, iBit++);
+ pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
- pObj->fMark0 = Aig_InfoHasBit(p->pData, iBit++);
+ pObj->fMark0 = Gia_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));
@@ -657,18 +767,97 @@ void Gia_ManPrintCounterExample( Gia_Cex_t * p )
p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits );
printf( "State : " );
for ( k = 0; k < p->nRegs; k++ )
- printf( "%d", Aig_InfoHasBit(p->pData, k) );
+ printf( "%d", Gia_InfoHasBit(p->pData, k) );
printf( "\n" );
for ( f = 0; f <= p->iFrame; f++ )
{
printf( "Frame %2d : ", f );
for ( i = 0; i < p->nPis; i++ )
- printf( "%d", Aig_InfoHasBit(p->pData, k++) );
+ printf( "%d", Gia_InfoHasBit(p->pData, k++) );
printf( "\n" );
}
assert( k == p->nBits );
}
+/**Function*************************************************************
+
+ Synopsis [Dereferences the node's MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_NodeDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
+{
+ Gia_Obj_t * pFanin;
+ int Counter = 0;
+ if ( Gia_ObjIsCi(pNode) )
+ return 0;
+ assert( Gia_ObjIsAnd(pNode) );
+ pFanin = Gia_ObjFanin0(pNode);
+ assert( Gia_ObjRefs(p, pFanin) > 0 );
+ if ( Gia_ObjRefDec(p, pFanin) == 0 )
+ Counter += Gia_NodeDeref_rec( p, pFanin );
+ pFanin = Gia_ObjFanin1(pNode);
+ assert( Gia_ObjRefs(p, pFanin) > 0 );
+ if ( Gia_ObjRefDec(p, pFanin) == 0 )
+ Counter += Gia_NodeDeref_rec( p, pFanin );
+ return Counter + 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [References the node's MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_NodeRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
+{
+ Gia_Obj_t * pFanin;
+ int Counter = 0;
+ if ( Gia_ObjIsCi(pNode) )
+ return 0;
+ assert( Gia_ObjIsAnd(pNode) );
+ pFanin = Gia_ObjFanin0(pNode);
+ if ( Gia_ObjRefInc(p, pFanin) == 0 )
+ Counter += Gia_NodeRef_rec( p, pFanin );
+ pFanin = Gia_ObjFanin1(pNode);
+ if ( Gia_ObjRefInc(p, pFanin) == 0 )
+ Counter += Gia_NodeRef_rec( p, pFanin );
+ return Counter + 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of internal nodes in the MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
+{
+ int ConeSize1, ConeSize2;
+ assert( !Gia_IsComplement(pNode) );
+ assert( Gia_ObjIsCand(pNode) );
+ ConeSize1 = Gia_NodeDeref_rec( p, pNode );
+ ConeSize2 = Gia_NodeRef_rec( p, pNode );
+ assert( ConeSize1 == ConeSize2 );
+ assert( ConeSize1 >= 0 );
+ return ConeSize1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 17:23:55 +0000