summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-08-22 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-08-22 08:01:00 -0700
commit28467823812f63a40f9a322b1fefc7decce4b766 (patch)
tree8e7d9849119d106ebafd58e02e640338ffddacf3
parentc8a25de8e411409b60f3677f70eab0860070b462 (diff)
downloadabc-28467823812f63a40f9a322b1fefc7decce4b766.tar.gz
abc-28467823812f63a40f9a322b1fefc7decce4b766.tar.bz2
abc-28467823812f63a40f9a322b1fefc7decce4b766.zip
Version abc70822
-rw-r--r--abc.dsp4
-rw-r--r--src/aig/aig/aig.h6
-rw-r--r--src/aig/aig/aigDfs.c48
-rw-r--r--src/aig/aig/aigRepr.c50
-rw-r--r--src/aig/aig/aigRet.c528
-rw-r--r--src/aig/aig/aigSeq.c219
-rw-r--r--src/aig/aig/aigTsim.c436
-rw-r--r--src/aig/aig/module.make1
-rw-r--r--src/aig/fra/fra.h6
-rw-r--r--src/aig/fra/fraClass.c172
-rw-r--r--src/aig/fra/fraCore.c104
-rw-r--r--src/aig/fra/fraImp.c16
-rw-r--r--src/aig/fra/fraInd.c55
-rw-r--r--src/aig/fra/fraMan.c1
-rw-r--r--src/aig/fra/fraPart.c86
-rw-r--r--src/aig/fra/fraSec.c5
-rw-r--r--src/aig/fra/fraSim.c13
-rw-r--r--src/aig/ivy/ivyMan.c2
-rw-r--r--src/base/abci/abc.c24
-rw-r--r--src/base/abci/abcDar.c11
-rw-r--r--src/base/abci/abcPrint.c5
-rw-r--r--todo.txt3
22 files changed, 1415 insertions, 380 deletions
diff --git a/abc.dsp b/abc.dsp
index 33e3d675..17c2006a 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -2814,6 +2814,10 @@ SOURCE=.\src\aig\aig\aigTruth.c
# End Source File
# Begin Source File
+SOURCE=.\src\aig\aig\aigTsim.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\aig\aig\aigUtil.c
# End Source File
# Begin Source File
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 953d98ac..1ee62ad6 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -359,6 +359,7 @@ extern Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p );
extern int Aig_ManCountLevels( Aig_Man_t * p );
extern int Aig_DagSize( Aig_Obj_t * pObj );
+extern int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
@@ -434,10 +435,9 @@ extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p );
extern void Aig_ManCreateChoices( Aig_Man_t * p );
/*=== aigRet.c ========================================================*/
-extern Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose );
+extern Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
/*=== aigSeq.c ========================================================*/
extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
-extern Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose );
/*=== aigShow.c ========================================================*/
extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
/*=== aigTable.c ========================================================*/
@@ -458,6 +458,8 @@ extern void Aig_ManVerifyLevel( Aig_Man_t * p );
extern void Aig_ManVerifyReverseLevel( Aig_Man_t * p );
/*=== aigTruth.c ========================================================*/
extern unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore );
+/*=== aigTsim.c ========================================================*/
+extern Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose );
/*=== aigUtil.c =========================================================*/
extern unsigned Aig_PrimeCudd( unsigned p );
extern void Aig_ManIncrementTravId( Aig_Man_t * p );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 5a18c4ac..86509322 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -380,6 +380,54 @@ int Aig_DagSize( Aig_Obj_t * pObj )
/**Function*************************************************************
+ Synopsis [Counts the support size of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_SupportSize_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pCounter )
+{
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ (*pCounter)++;
+ return;
+ }
+ assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
+ Aig_SupportSize_rec( p, Aig_ObjFanin0(pObj), pCounter );
+ if ( Aig_ObjFanin1(pObj) )
+ Aig_SupportSize_rec( p, Aig_ObjFanin1(pObj), pCounter );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the support size of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ int Counter = 0;
+ assert( !Aig_IsComplement(pObj) );
+ assert( !Aig_ObjIsPo(pObj) );
+ Aig_ManIncrementTravId( p );
+ Aig_SupportSize_rec( p, pObj, &Counter );
+ return Counter;
+}
+
+/**Function*************************************************************
+
Synopsis [Transfers the AIG from one manager into another.]
Description []
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index a862bf97..3e588979 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -130,7 +130,7 @@ static inline Aig_Obj_t * Aig_ObjFindRepr( Aig_Man_t * p, Aig_Obj_t * pNode )
assert( p->pReprs != NULL );
assert( !Aig_IsComplement(pNode) );
assert( pNode->Id < p->nReprsAlloc );
- assert( !p->pReprs[pNode->Id] || p->pReprs[pNode->Id]->Id < pNode->Id );
+// assert( !p->pReprs[pNode->Id] || p->pReprs[pNode->Id]->Id < pNode->Id );
return p->pReprs[pNode->Id];
}
@@ -210,12 +210,38 @@ void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p )
assert( pNew->pReprs != NULL );
// go through the nodes which have representatives
Aig_ManForEachObj( p, pObj, k )
- if ( pRepr = Aig_ObjFindRepr(p, pObj) )
+ if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) );
}
/**Function*************************************************************
+ Synopsis [Duplicates the AIG manager recursively.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pRepr;
+ if ( pObj->pData )
+ return pObj->pData;
+ if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
+ {
+ Aig_ManDupRepr_rec( pNew, p, pRepr );
+ return pObj->pData = Aig_NotCond( pRepr->pData, pRepr->fPhase ^ pObj->fPhase );
+ }
+ Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
+ Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin1(pObj) );
+ return pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
+}
+
+/**Function*************************************************************
+
Synopsis [Duplicates AIG while substituting representatives.]
Description []
@@ -227,27 +253,29 @@ void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p )
***********************************************************************/
Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p )
{
+ int fOrdered = 1;
Aig_Man_t * pNew;
- Aig_Obj_t * pObj, * pRepr;
+ Aig_Obj_t * pObj;
int i;
// start the HOP package
pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
pNew->nRegs = p->nRegs;
Aig_ManReprStart( pNew, Aig_ManObjIdMax(p)+1 );
// map the const and primary inputs
+ Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
// map the internal nodes
-//printf( "\n" );
- Aig_ManForEachNode( p, pObj, i )
+ if ( fOrdered )
{
- pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
- if ( pRepr = Aig_ObjFindRepr(p, pObj) ) // member of the class
- {
-//printf( "Using node %d for node %d.\n", pRepr->Id, pObj->Id );
- Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) );
- }
+ Aig_ManForEachNode( p, pObj, i )
+ pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
+ }
+ else
+ {
+ Aig_ManForEachPo( p, pObj, i )
+ Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
}
// transfer the POs
Aig_ManForEachPo( p, pObj, i )
diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c
index eacf756b..38fcc719 100644
--- a/src/aig/aig/aigRet.c
+++ b/src/aig/aig/aigRet.c
@@ -40,9 +40,11 @@ struct Rtm_Man_t_
Vec_Ptr_t * vPis; // PIs only
Vec_Ptr_t * vPos; // POs only
Aig_MmFlex_t * pMem; // the memory manager
+ // autonomous components after cutting off
// storage for overflow latches
- unsigned * pExtra;
- unsigned * pExtraFree;
+ unsigned * pExtra;
+ int nExtraCur;
+ int nExtraAlloc;
};
typedef struct Rtm_Edg_t_ Rtm_Edg_t;
@@ -58,32 +60,59 @@ struct Rtm_Obj_t_
void * pCopy; // the copy of this object
unsigned long Type : 3; // object type
unsigned long fMark : 1; // multipurpose mark
+ unsigned long fAuto : 1; // this object belongs to an autonomous component
unsigned long fCompl0 : 1; // complemented attribute of the first edge
unsigned long fCompl1 : 1; // complemented attribute of the second edge
unsigned long nFanins : 8; // the number of fanins
- unsigned Num : 18; // the retiming number of this node
+ unsigned Num : 17; // the retiming number of this node
int Id; // ID of this object
int Temp; // temporary usage
int nFanouts; // the number of fanouts
void * pFanio[0]; // fanins and their edges (followed by fanouts and pointers to their edges)
};
-static Rtm_Init_t Rtm_InitNot( Rtm_Init_t Val ) { if ( Val == RTM_VAL_ZERO ) return RTM_VAL_ONE; if ( Val == RTM_VAL_ONE ) return RTM_VAL_ZERO; assert( 0 ); return -1; }
-static Rtm_Init_t Rtm_InitNotCond( Rtm_Init_t Val, int c ) { return c ? Rtm_InitNot(Val) : Val; }
-static Rtm_Init_t Rtm_InitAnd(Rtm_Init_t ValA, Rtm_Init_t ValB) { if ( ValA == RTM_VAL_ONE && ValB == RTM_VAL_ONE ) return RTM_VAL_ONE; if ( ValA == RTM_VAL_ZERO || ValB == RTM_VAL_ZERO ) return RTM_VAL_ZERO; assert( 0 ); return -1; }
+static inline Rtm_Obj_t * Rtm_ObjFanin( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*i]; }
+static inline Rtm_Obj_t * Rtm_ObjFanout( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*(pObj->nFanins+i)]; }
+static inline Rtm_Edg_t * Rtm_ObjEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)(pObj->pFanio + 2*i + 1); }
+static inline Rtm_Edg_t * Rtm_ObjFanoutEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)pObj->pFanio[2*(pObj->nFanins+i) + 1]; }
+
+static inline Rtm_Init_t Rtm_InitNot( Rtm_Init_t Val ) { if ( Val == RTM_VAL_ZERO ) return RTM_VAL_ONE; if ( Val == RTM_VAL_ONE ) return RTM_VAL_ZERO; assert( 0 ); return -1; }
+static inline Rtm_Init_t Rtm_InitNotCond( Rtm_Init_t Val, int c ) { return c ? Rtm_InitNot(Val) : Val; }
+static inline Rtm_Init_t Rtm_InitAnd(Rtm_Init_t ValA, Rtm_Init_t ValB ) { if ( ValA == RTM_VAL_ONE && ValB == RTM_VAL_ONE ) return RTM_VAL_ONE; if ( ValA == RTM_VAL_ZERO || ValB == RTM_VAL_ZERO ) return RTM_VAL_ZERO; assert( 0 ); return -1; }
+
+static inline int Rtm_InitWordsNum( int nLats ) { return (nLats >> 4) + ((nLats & 15) > 0); }
+static inline int Rtm_InitGetTwo( unsigned * p, int i ) { return (p[i>>4] >> ((i & 15)<<1)) & 3; }
+static inline void Rtm_InitSetTwo( unsigned * p, int i, int val ) { p[i>>4] |= (val << ((i & 15)<<1)); }
+static inline void Rtm_InitXorTwo( unsigned * p, int i, int val ) { p[i>>4] ^= (val << ((i & 15)<<1)); }
+
+static inline Rtm_Init_t Rtm_ObjGetFirst1( Rtm_Edg_t * pEdge ) { return pEdge->LData & 3; }
+static inline Rtm_Init_t Rtm_ObjGetLast1( Rtm_Edg_t * pEdge ) { return (pEdge->LData >> ((pEdge->nLats-1)<<1)) & 3; }
+static inline Rtm_Init_t Rtm_ObjGetOne1( Rtm_Edg_t * pEdge, int i ) { assert( i < (int)pEdge->nLats ); return (pEdge->LData >> (i << 1)) & 3; }
+static inline Rtm_Init_t Rtm_ObjRemFirst1( Rtm_Edg_t * pEdge ) { int Val = pEdge->LData & 3; pEdge->LData >>= 2; assert(pEdge->nLats > 0); pEdge->nLats--; return Val; }
+static inline Rtm_Init_t Rtm_ObjRemLast1( Rtm_Edg_t * pEdge ) { int Val = (pEdge->LData >> ((pEdge->nLats-1)<<1)) & 3; pEdge->LData ^= Val << ((pEdge->nLats-1)<<1); assert(pEdge->nLats > 0); pEdge->nLats--; return Val; }
+static inline void Rtm_ObjAddFirst1( Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { assert( Val > 0 && Val < 4 ); pEdge->LData = (pEdge->LData << 2) | Val; pEdge->nLats++; }
+static inline void Rtm_ObjAddLast1( Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { assert( Val > 0 && Val < 4 ); pEdge->LData |= Val << (pEdge->nLats<<1); pEdge->nLats++; }
+
+static inline Rtm_Init_t Rtm_ObjGetFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, 0 ); }
+static inline Rtm_Init_t Rtm_ObjGetLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, pEdge->nLats - 1 ); }
+static inline Rtm_Init_t Rtm_ObjGetOne2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, int i ) { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, i ); }
+static Rtm_Init_t Rtm_ObjRemFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge );
+static inline Rtm_Init_t Rtm_ObjRemLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { Rtm_Init_t Val = Rtm_ObjGetLast2( p, pEdge ); Rtm_InitXorTwo( p->pExtra + pEdge->LData, pEdge->nLats - 1, Val ); pEdge->nLats--; return Val; }
+static void Rtm_ObjAddFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val );
+static inline void Rtm_ObjAddLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { Rtm_InitSetTwo( p->pExtra + pEdge->LData, pEdge->nLats, Val ); pEdge->nLats++; }
+
+static void Rtm_ObjTransferToSmall( Rtm_Man_t * p, Rtm_Edg_t * pEdge );
+static void Rtm_ObjTransferToBig( Rtm_Man_t * p, Rtm_Edg_t * pEdge );
+static void Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge );
+
+static inline Rtm_Init_t Rtm_ObjGetFirst( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { return pEdge->nLats > 10? Rtm_ObjGetFirst2(p, pEdge) : Rtm_ObjGetFirst1(pEdge); }
+static inline Rtm_Init_t Rtm_ObjGetLast( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { return pEdge->nLats > 10? Rtm_ObjGetLast2(p, pEdge) : Rtm_ObjGetLast1(pEdge); }
+static inline Rtm_Init_t Rtm_ObjGetOne( Rtm_Man_t * p, Rtm_Edg_t * pEdge, int i ) { return pEdge->nLats > 10? Rtm_ObjGetOne2(p, pEdge, i) : Rtm_ObjGetOne1(pEdge, i); }
+static Rtm_Init_t Rtm_ObjRemFirst( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { Rtm_Init_t Res = pEdge->nLats > 10 ? Rtm_ObjRemFirst2(p, pEdge) : Rtm_ObjRemFirst1(pEdge); if ( pEdge->nLats == 10 ) Rtm_ObjTransferToSmall(p, pEdge); return Res; }
+static Rtm_Init_t Rtm_ObjRemLast( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { Rtm_Init_t Res = pEdge->nLats > 10 ? Rtm_ObjRemLast2(p, pEdge) : Rtm_ObjRemLast1(pEdge); if ( pEdge->nLats == 10 ) Rtm_ObjTransferToSmall(p, pEdge); return Res; }
+static void Rtm_ObjAddFirst( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { if ( pEdge->nLats == 10 ) Rtm_ObjTransferToBig(p, pEdge); else if ( (pEdge->nLats & 15) == 15 ) Rtm_ObjTransferToBigger(p, pEdge); if ( pEdge->nLats >= 10 ) Rtm_ObjAddFirst2(p, pEdge, Val); else Rtm_ObjAddFirst1(pEdge, Val); }
+static void Rtm_ObjAddLast( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { if ( pEdge->nLats == 10 ) Rtm_ObjTransferToBig(p, pEdge); else if ( (pEdge->nLats & 15) == 15 ) Rtm_ObjTransferToBigger(p, pEdge); if ( pEdge->nLats >= 10 ) Rtm_ObjAddLast2(p, pEdge, Val); else Rtm_ObjAddLast1(pEdge, Val); }
-static Rtm_Obj_t * Rtm_ObjFanin( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*i]; }
-static Rtm_Obj_t * Rtm_ObjFanout( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*(pObj->nFanins+i)]; }
-static Rtm_Edg_t * Rtm_ObjEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)(pObj->pFanio + 2*i + 1); }
-static Rtm_Edg_t * Rtm_ObjFanoutEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)pObj->pFanio[2*(pObj->nFanins+i) + 1]; }
-
-static Rtm_Init_t Rtm_ObjGetFirst( Rtm_Edg_t * pEdge ) { return pEdge->LData & 3; }
-static Rtm_Init_t Rtm_ObjGetLast( Rtm_Edg_t * pEdge ) { return (pEdge->LData >> (2 *(pEdge->nLats-1))) & 3; }
-static Rtm_Init_t Rtm_ObjGetOne( Rtm_Edg_t * pEdge, int i ) { assert( i < (int)pEdge->nLats ); return (pEdge->LData >> (2 * i)) & 3; }
-static Rtm_Init_t Rtm_ObjRemFirst( Rtm_Edg_t * pEdge ) { int Val = pEdge->LData & 3; pEdge->LData >>= 2; assert(pEdge->nLats > 0); pEdge->nLats--; return Val; }
-static Rtm_Init_t Rtm_ObjRemLast( Rtm_Edg_t * pEdge ) { int Val = (pEdge->LData >> (2 *(pEdge->nLats-1))) & 3; pEdge->LData ^= Val << (2 *(pEdge->nLats-1)); assert(pEdge->nLats > 0); pEdge->nLats--; return Val; }
-static void Rtm_ObjAddFirst( Rtm_Edg_t * pEdge, Rtm_Init_t Lat ) { assert( Lat < 4 ); pEdge->LData = (pEdge->LData << 2) | Lat; pEdge->nLats++; }
-static void Rtm_ObjAddLast( Rtm_Edg_t * pEdge, Rtm_Init_t Lat ) { assert( Lat < 4 ); pEdge->LData |= Lat << (2*pEdge->nLats); pEdge->nLats++; }
// iterator over the primary inputs
#define Rtm_ManForEachPi( p, pObj, i ) \
@@ -113,6 +142,149 @@ static void Rtm_ObjAddLast( Rtm_Edg_t * pEdge, Rtm_Init_t Lat ) { assert
/**Function*************************************************************
+ Synopsis [Transfers from big to small storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rtm_ObjTransferToSmall( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
+{
+ assert( pEdge->nLats == 10 );
+ pEdge->LData = p->pExtra[pEdge->LData];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transfers from small to big storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rtm_ObjTransferToBig( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
+{
+ assert( pEdge->nLats == 10 );
+ if ( p->nExtraCur + 1 > p->nExtraAlloc )
+ {
+ int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 );
+ p->pExtra = REALLOC( unsigned, p->pExtra, nExtraAllocNew );
+ p->nExtraAlloc = nExtraAllocNew;
+ }
+ p->pExtra[p->nExtraCur] = pEdge->LData;
+ pEdge->LData = p->nExtraCur++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transfers to bigger storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
+{
+ int nWords;
+ assert( (pEdge->nLats & 15) == 15 );
+ nWords = (pEdge->nLats + 1) >> 4;
+ if ( p->nExtraCur + nWords + 1 > p->nExtraAlloc )
+ {
+ int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 );
+ p->pExtra = REALLOC( unsigned, p->pExtra, nExtraAllocNew );
+ p->nExtraAlloc = nExtraAllocNew;
+ }
+ memcpy( p->pExtra + p->nExtraCur, p->pExtra + pEdge->LData, sizeof(unsigned) * nWords );
+ p->pExtra[p->nExtraCur + nWords] = 0;
+ pEdge->LData = p->nExtraCur;
+ p->nExtraCur += nWords + 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Rtm_Init_t Rtm_ObjRemFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
+{
+ Rtm_Init_t Val = 0, Temp;
+ unsigned * pB = p->pExtra + pEdge->LData, * pE = pB + Rtm_InitWordsNum( pEdge->nLats-- ) - 1;
+ while ( pE >= pB )
+ {
+ Temp = *pE & 3;
+ *pE = (*pE >> 2) | (Val << 30);
+ Val = Temp;
+ pE--;
+ }
+ assert( Val != 0 );
+ return Val;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rtm_ObjAddFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val )
+{
+ unsigned * pB = p->pExtra + pEdge->LData, * pE = pB + Rtm_InitWordsNum( ++pEdge->nLats );
+ Rtm_Init_t Temp;
+ assert( Val != 0 );
+ while ( pB < pE )
+ {
+ Temp = *pB >> 30;
+ *pB = (*pB << 2) | Val;
+ Val = Temp;
+ pB++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rtm_PrintEdge( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
+{
+ unsigned LData = pEdge->LData;
+ printf( "%d : ", pEdge->nLats );
+ if ( pEdge->nLats > 10 )
+ Extra_PrintBinary( stdout, p->pExtra + pEdge->LData, 2*(pEdge->nLats+1) );
+ else
+ Extra_PrintBinary( stdout, &LData, 2*(pEdge->nLats+1) );
+ printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
Synopsis [Allocates the retiming manager.]
Description []
@@ -153,6 +325,7 @@ void Rtm_ManFree( Rtm_Man_t * p )
Vec_PtrFree( p->vPis );
Vec_PtrFree( p->vPos );
Aig_MmFlexStop( p->pMem, 0 );
+ FREE( p->pExtra );
free( p );
}
@@ -171,10 +344,19 @@ int Rtm_ManLatchMax( Rtm_Man_t * p )
{
Rtm_Obj_t * pObj;
Rtm_Edg_t * pEdge;
- int nLatchMax = 0, i, k;
+ int nLatchMax = 0, i, k;//, c, Val;
Rtm_ManForEachObj( p, pObj, i )
Rtm_ObjForEachFaninEdge( pObj, pEdge, k )
+ {
+/*
+ for ( c = 0; c < (int)pEdge->nLats; c++ )
+ {
+ Val = Rtm_ObjGetOne( p, pEdge, c );
+ assert( Val == 1 || Val == 2 );
+ }
+*/
nLatchMax = AIG_MAX( nLatchMax, (int)pEdge->nLats );
+ }
return nLatchMax;
}
@@ -264,6 +446,27 @@ int Rtm_ObjCheckRetimeFwd( Rtm_Obj_t * pObj )
SeeAlso []
***********************************************************************/
+int Rtm_ObjCheckRetimeBwd( Rtm_Obj_t * pObj )
+{
+ Rtm_Edg_t * pEdge;
+ int i;
+ Rtm_ObjForEachFanoutEdge( pObj, pEdge, i )
+ if ( pEdge->nLats == 0 )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check the possibility of forward retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj )
{
Rtm_Obj_t * pFanin;
@@ -275,6 +478,26 @@ int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj )
/**Function*************************************************************
+ Synopsis [Check the possibility of forward retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rtm_ObjGetDegreeBwd( Rtm_Obj_t * pObj )
+{
+ Rtm_Obj_t * pFanout;
+ int i, Degree = 0;
+ Rtm_ObjForEachFanout( pObj, pFanout, i )
+ Degree = AIG_MAX( Degree, (int)pFanout->Num );
+ return Degree + 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs forward retiming.]
Description []
@@ -284,7 +507,7 @@ int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Rtm_ObjRetimeFwd( Rtm_Obj_t * pObj )
+void Rtm_ObjRetimeFwd( Rtm_Man_t * pRtm, Rtm_Obj_t * pObj )
{
Rtm_Init_t ValTotal, ValCur;
Rtm_Edg_t * pEdge;
@@ -294,17 +517,143 @@ void Rtm_ObjRetimeFwd( Rtm_Obj_t * pObj )
ValTotal = RTM_VAL_ONE;
Rtm_ObjForEachFaninEdge( pObj, pEdge, i )
{
- ValCur = Rtm_ObjRemFirst( pEdge );
+ ValCur = Rtm_ObjRemFirst( pRtm, pEdge );
ValCur = Rtm_InitNotCond( ValCur, i? pObj->fCompl1 : pObj->fCompl0 );
ValTotal = Rtm_InitAnd( ValTotal, ValCur );
}
// insert the result in the fanout values
Rtm_ObjForEachFanoutEdge( pObj, pEdge, i )
+ Rtm_ObjAddLast( pRtm, pEdge, ValTotal );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs forward retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rtm_ObjRetimeBwd( Rtm_Man_t * pRtm, Rtm_Obj_t * pObj )
+{
+ Rtm_Edg_t * pEdge;
+ int i;
+ assert( Rtm_ObjCheckRetimeBwd(pObj) );
+ // extract values and compute the result
+ Rtm_ObjForEachFanoutEdge( pObj, pEdge, i )
+ Rtm_ObjRemLast( pRtm, pEdge );
+ // insert the result in the fanout values
+ Rtm_ObjForEachFaninEdge( pObj, pEdge, i )
+ Rtm_ObjAddFirst( pRtm, pEdge, RTM_VAL_VOID );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rtm_ObjMarkAutoFwd_rec( Rtm_Obj_t * pObj )
+{
+ Rtm_Obj_t * pFanout;
+ int i;
+ if ( pObj->fAuto )
+ return;
+ pObj->fAuto = 1;
+ Rtm_ObjForEachFanout( pObj, pFanout, i )
+ Rtm_ObjMarkAutoFwd_rec( pFanout );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the nodes unreachable from the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rtm_ManMarkAutoFwd( Rtm_Man_t * pRtm )
+{
+ Rtm_Obj_t * pObjRtm;
+ int i, Counter = 0;
+ // mark nodes reachable from the PIs
+ pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 );
+ Rtm_ObjMarkAutoFwd_rec( pObjRtm );
+ Rtm_ManForEachPi( pRtm, pObjRtm, i )
+ Rtm_ObjMarkAutoFwd_rec( pObjRtm );
+ // count the number of autonomous nodes
+ Rtm_ManForEachObj( pRtm, pObjRtm, i )
{
- if ( pEdge->nLats >= 10 )
- printf( "Rtm_ObjRetimeFwd(); More than 10 latches on the edge!\n" );
- Rtm_ObjAddLast( pEdge, ValTotal );
+ pObjRtm->fAuto = !pObjRtm->fAuto;
+ Counter += pObjRtm->fAuto;
}
+ // mark the fanins of the autonomous nodes
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rtm_ObjMarkAutoBwd_rec( Rtm_Obj_t * pObj )
+{
+ Rtm_Obj_t * pFanin;
+ int i;
+ if ( pObj->fAuto )
+ return;
+ pObj->fAuto = 1;
+ Rtm_ObjForEachFanin( pObj, pFanin, i )
+ Rtm_ObjMarkAutoBwd_rec( pFanin );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the nodes unreachable from the POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rtm_ManMarkAutoBwd( Rtm_Man_t * pRtm )
+{
+ Rtm_Obj_t * pObjRtm;
+ int i, Counter = 0;
+ // mark nodes reachable from the PIs
+ pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 );
+ pObjRtm->fAuto = 1;
+ Rtm_ManForEachPi( pRtm, pObjRtm, i )
+ pObjRtm->fAuto = 1;
+ Rtm_ManForEachPo( pRtm, pObjRtm, i )
+ Rtm_ObjMarkAutoBwd_rec( pObjRtm );
+ // count the number of autonomous nodes
+ Rtm_ManForEachObj( pRtm, pObjRtm, i )
+ {
+ pObjRtm->fAuto = !pObjRtm->fAuto;
+ Counter += pObjRtm->fAuto;
+ }
+ // mark the fanins of the autonomous nodes
+ return Counter;
}
/**Function*************************************************************
@@ -358,9 +707,6 @@ Rtm_Man_t * Rtm_ManFromAig( Aig_Man_t * p )
Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
}
- // set registers
- Aig_ManForEachLoSeq( p, pObj, i )
- Rtm_ObjAddFirst( Rtm_ObjEdge(pObj->pData, 0), RTM_VAL_ZERO );
return pRtm;
}
@@ -375,7 +721,7 @@ Rtm_Man_t * Rtm_ManFromAig( Aig_Man_t * p )
SeeAlso []
***********************************************************************/
-Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Obj_t * pObjRtm, int * pLatches )
+Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Man_t * pRtm, Rtm_Obj_t * pObjRtm, int * pLatches )
{
Rtm_Edg_t * pEdge;
Aig_Obj_t * pRes, * pFanin;
@@ -387,10 +733,10 @@ Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Obj_t * pObjRtm, int * pLatc
Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k )
{
if ( pEdge->nLats == 0 )
- pFanin = Rtm_ManToAig_rec( pNew, Rtm_ObjFanin(pObjRtm, k), pLatches );
+ pFanin = Rtm_ManToAig_rec( pNew, pRtm, Rtm_ObjFanin(pObjRtm, k), pLatches );
else
{
- Val = Rtm_ObjGetFirst( pEdge );
+ Val = Rtm_ObjGetFirst( pRtm, pEdge );
pFanin = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + pEdge->nLats - 1 );
pFanin = Aig_NotCond( pFanin, Val == RTM_VAL_ONE );
}
@@ -438,7 +784,7 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
Aig_ObjCreatePi(pNew);
// create internal nodes
Rtm_ManForEachObj( pRtm, pObjRtm, i )
- Rtm_ManToAig_rec( pNew, pObjRtm, pLatches );
+ Rtm_ManToAig_rec( pNew, pRtm, pObjRtm, pLatches );
// create POs
Rtm_ManForEachPo( pRtm, pObjRtm, i )
Aig_ObjCreatePo( pNew, pObjRtm->pCopy );
@@ -451,7 +797,8 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
pObjNew = Rtm_ObjFanin( pObjRtm, k )->pCopy;
for ( m = 0; m < (int)pEdge->nLats; m++ )
{
- Val = Rtm_ObjGetOne( pEdge, pEdge->nLats - 1 - m );
+ Val = Rtm_ObjGetOne( pRtm, pEdge, pEdge->nLats - 1 - m );
+ assert( Val == RTM_VAL_ZERO || Val == RTM_VAL_ONE || Val == RTM_VAL_VOID );
pObjNew = Aig_NotCond( pObjNew, Val == RTM_VAL_ONE );
Aig_ObjCreatePo( pNew, pObjNew );
pObjNew = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + m );
@@ -479,16 +826,33 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose )
+Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose )
{
Vec_Ptr_t * vQueue;
Aig_Man_t * pNew;
Rtm_Man_t * pRtm;
- Rtm_Obj_t * pObj, * pFanout;
+ Rtm_Obj_t * pObj, * pNext;
Aig_Obj_t * pObjAig;
- int i, k, Degree, DegreeMax = 0;
+ int i, k, nAutos, Degree, DegreeMax = 0;
+ int clk;
+
// create the retiming manager
+clk = clock();
pRtm = Rtm_ManFromAig( p );
+ // set registers
+ Aig_ManForEachLoSeq( p, pObjAig, i )
+ Rtm_ObjAddFirst( pRtm, Rtm_ObjEdge(pObjAig->pData, 0), fForward? RTM_VAL_ZERO : RTM_VAL_VOID );
+ // detect and mark the autonomous components
+ if ( fForward )
+ nAutos = Rtm_ManMarkAutoFwd( pRtm );
+ else
+ nAutos = Rtm_ManMarkAutoBwd( pRtm );
+ if ( fVerbose )
+ {
+ printf( "Detected %d autonomous objects. ", nAutos );
+ PRT( "Time", clock() - clk );
+ }
+
// set the current retiming number
Rtm_ManForEachObj( pRtm, pObj, i )
{
@@ -497,13 +861,30 @@ Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose )
pObj->Num = 0;
}
+clk = clock();
// put the LOs on the queue
vQueue = Vec_PtrAlloc( 1000 );
- Aig_ManForEachLoSeq( p, pObjAig, i )
+ if ( fForward )
+ {
+ Aig_ManForEachLoSeq( p, pObjAig, i )
+ {
+ pObj = pObjAig->pData;
+ if ( pObj->fAuto )
+ continue;
+ pObj->fMark = 1;
+ Vec_PtrPush( vQueue, pObj );
+ }
+ }
+ else
{
- pObj = pObjAig->pData;
- pObj->fMark = 1;
- Vec_PtrPush( vQueue, pObj );
+ Aig_ManForEachLiSeq( p, pObjAig, i )
+ {
+ pObj = pObjAig->pData;
+ if ( pObj->fAuto )
+ continue;
+ pObj->fMark = 1;
+ Vec_PtrPush( vQueue, pObj );
+ }
}
// perform retiming
DegreeMax = 0;
@@ -511,36 +892,69 @@ Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose )
{
pObj->fMark = 0;
// retime the node
- Rtm_ObjRetimeFwd( pObj );
- // check if its fanouts should be retimed
- Rtm_ObjForEachFanout( pObj, pFanout, k )
+ if ( fForward )
{
- if ( pFanout->fMark ) // skip aleady scheduled
- continue;
- if ( pFanout->Type ) // skip POs
- continue;
- if ( !Rtm_ObjCheckRetimeFwd( pFanout ) ) // skip non-retimable
- continue;
- Degree = Rtm_ObjGetDegreeFwd( pFanout );
- DegreeMax = AIG_MAX( DegreeMax, Degree );
- if ( Degree > nStepsMax ) // skip nodes with high degree
- continue;
- pFanout->fMark = 1;
- pFanout->Num = Degree;
- Vec_PtrPush( vQueue, pFanout );
+ Rtm_ObjRetimeFwd( pRtm, pObj );
+ // check if its fanouts should be retimed
+ Rtm_ObjForEachFanout( pObj, pNext, k )
+ {
+ if ( pNext->fMark ) // skip aleady scheduled
+ continue;
+ if ( pNext->Type ) // skip POs
+ continue;
+ if ( !Rtm_ObjCheckRetimeFwd( pNext ) ) // skip non-retimable
+ continue;
+ Degree = Rtm_ObjGetDegreeFwd( pNext );
+ DegreeMax = AIG_MAX( DegreeMax, Degree );
+ if ( Degree > nStepsMax ) // skip nodes with high degree
+ continue;
+ pNext->fMark = 1;
+ pNext->Num = Degree;
+ Vec_PtrPush( vQueue, pNext );
+ }
+ }
+ else
+ {
+ Rtm_ObjRetimeBwd( pRtm, pObj );
+ // check if its fanouts should be retimed
+ Rtm_ObjForEachFanin( pObj, pNext, k )
+ {
+ if ( pNext->fMark ) // skip aleady scheduled
+ continue;
+ if ( pNext->nFanins == 0 ) // skip PIs
+ continue;
+ if ( !Rtm_ObjCheckRetimeBwd( pNext ) ) // skip non-retimable
+ continue;
+ Degree = Rtm_ObjGetDegreeBwd( pNext );
+ DegreeMax = AIG_MAX( DegreeMax, Degree );
+ if ( Degree > nStepsMax ) // skip nodes with high degree
+ continue;
+ pNext->fMark = 1;
+ pNext->Num = Degree;
+ Vec_PtrPush( vQueue, pNext );
+ }
}
}
if ( fVerbose )
- printf( "Performed %d fwd latch moves of max depth %d and max latch count %d.\n",
- Vec_PtrSize(vQueue), DegreeMax, Rtm_ManLatchMax(pRtm) );
+ {
+ printf( "Performed %d %s latch moves of max depth %d and max latch count %d.\n",
+ Vec_PtrSize(vQueue), fForward? "fwd":"bwd", DegreeMax, Rtm_ManLatchMax(pRtm) );
+ printf( "Memory usage = %d. ", pRtm->nExtraCur );
+ PRT( "Time", clock() - clk );
+ }
Vec_PtrFree( vQueue );
// get the new manager
pNew = Rtm_ManToAig( pRtm );
Rtm_ManFree( pRtm );
// group the registers
+clk = clock();
pNew = Aig_ManReduceLaches( pNew, fVerbose );
+ if ( fVerbose )
+ {
+ PRT( "Register sharing time", clock() - clk );
+ }
return pNew;
}
diff --git a/src/aig/aig/aigSeq.c b/src/aig/aig/aigSeq.c
index 5bd5aaa5..d296d339 100644
--- a/src/aig/aig/aigSeq.c
+++ b/src/aig/aig/aigSeq.c
@@ -24,70 +24,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-#define AIG_XVS0 1
-#define AIG_XVS1 2
-#define AIG_XVSX 3
-
-static inline void Aig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; }
-static inline int Aig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; }
-static inline int Aig_XsimInv( int Value )
-{
- if ( Value == AIG_XVS0 )
- return AIG_XVS1;
- if ( Value == AIG_XVS1 )
- return AIG_XVS0;
- assert( Value == AIG_XVSX );
- return AIG_XVSX;
-}
-static inline int Aig_XsimAnd( int Value0, int Value1 )
-{
- if ( Value0 == AIG_XVS0 || Value1 == AIG_XVS0 )
- return AIG_XVS0;
- if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX )
- return AIG_XVSX;
- assert( Value0 == AIG_XVS1 && Value1 == AIG_XVS1 );
- return AIG_XVS1;
-}
-static inline int Aig_XsimRand2()
-{
- return (rand() & 1) ? AIG_XVS1 : AIG_XVS0;
-}
-static inline int Aig_XsimRand3()
-{
- int RetValue;
- do {
- RetValue = rand() & 3;
- } while ( RetValue == 0 );
- return RetValue;
-}
-static inline int Aig_ObjGetXsimFanin0( Aig_Obj_t * pObj )
-{
- int RetValue;
- RetValue = Aig_ObjGetXsim(Aig_ObjFanin0(pObj));
- return Aig_ObjFaninC0(pObj)? Aig_XsimInv(RetValue) : RetValue;
-}
-static inline int Aig_ObjGetXsimFanin1( Aig_Obj_t * pObj )
-{
- int RetValue;
- RetValue = Aig_ObjGetXsim(Aig_ObjFanin1(pObj));
- return Aig_ObjFaninC1(pObj)? Aig_XsimInv(RetValue) : RetValue;
-}
-static inline void Aig_XsimPrint( FILE * pFile, int Value )
-{
- if ( Value == AIG_XVS0 )
- {
- fprintf( pFile, "0" );
- return;
- }
- if ( Value == AIG_XVS1 )
- {
- fprintf( pFile, "1" );
- return;
- }
- assert( Value == AIG_XVSX );
- fprintf( pFile, "x" );
-}
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -559,161 +495,6 @@ int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits )
-/**Function*************************************************************
-
- Synopsis [Cycles the circuit to create a new initial state.]
-
- Description [Simulates the circuit with random input for the given
- number of timeframes to get a better initial state.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
-{
- int nRounds = 1000; // limit on the number of ternary simulation rounds
- Vec_Ptr_t * vMap;
- Vec_Ptr_t * vStates;
- Aig_Obj_t * pObj, * pObjLi, * pObjLo;
- unsigned * pState, * pPrev;
- int i, k, f, fConstants, Value, nWords, nCounter;
- // allocate storage for states
- nWords = Aig_BitWordNum( 2*Aig_ManRegNum(p) );
- vStates = Vec_PtrAllocSimInfo( nRounds, nWords );
- // initialize the values
- Aig_ObjSetXsim( Aig_ManConst1(p), AIG_XVS1 );
- Aig_ManForEachPiSeq( p, pObj, i )
- Aig_ObjSetXsim( pObj, AIG_XVSX );
- Aig_ManForEachLoSeq( p, pObj, i )
- Aig_ObjSetXsim( pObj, AIG_XVS0 );
- // simulate for the given number of timeframes
- for ( f = 0; f < nRounds; f++ )
- {
- // collect this state
- pState = Vec_PtrEntry( vStates, f );
- memset( pState, 0, sizeof(unsigned) * nWords );
- Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
- {
- Value = Aig_ObjGetXsim(pObjLo);
- if ( Value & 1 )
- Aig_InfoSetBit( pState, 2 * i );
- if ( Value & 2 )
- Aig_InfoSetBit( pState, 2 * i + 1 );
-// Aig_XsimPrint( stdout, Value );
- }
-// printf( "\n" );
- // check if this state exists
- for ( i = f - 1; i >= 0; i-- )
- {
- pPrev = Vec_PtrEntry( vStates, i );
- if ( !memcmp( pPrev, pState, sizeof(unsigned) * nWords ) )
- break;
- }
- if ( i >= 0 )
- break;
- // simulate internal nodes
- Aig_ManForEachNode( p, pObj, i )
- Aig_ObjSetXsim( pObj, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) );
- // transfer the latch values
- Aig_ManForEachLiSeq( p, pObj, i )
- Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) );
- Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
- Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
- }
- if ( f == nRounds )
- {
- printf( "Aig_ManTernarySimulate(): Did not reach a fixed point.\n" );
- Vec_PtrFree( vStates );
- return NULL;
- }
- // OR all the states
- pState = Vec_PtrEntry( vStates, 0 );
- for ( i = 1; i <= f; i++ )
- {
- pPrev = Vec_PtrEntry( vStates, i );
- for ( k = 0; k < nWords; k++ )
- pState[k] |= pPrev[k];
- }
- // check if there are constants
- fConstants = 0;
- if ( 2*Aig_ManRegNum(p) == 32*nWords )
- {
- for ( i = 0; i < nWords; i++ )
- if ( pState[i] != ~0 )
- fConstants = 1;
- }
- else
- {
- for ( i = 0; i < nWords - 1; i++ )
- if ( pState[i] != ~0 )
- fConstants = 1;
- if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(nWords-1) ) )
- fConstants = 1;
- }
- if ( fConstants == 0 )
- {
- Vec_PtrFree( vStates );
- return NULL;
- }
-
- // start mapping by adding the true PIs
- vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
- Aig_ManForEachPiSeq( p, pObj, i )
- Vec_PtrPush( vMap, pObj );
- // find constant registers
- nCounter = 0;
- Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
- {
- Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
- nCounter += (Value == 1 || Value == 2);
- if ( Value == 1 )
- Vec_PtrPush( vMap, Aig_ManConst0(p) );
- else if ( Value == 2 )
- Vec_PtrPush( vMap, Aig_ManConst1(p) );
- else if ( Value == 3 )
- Vec_PtrPush( vMap, pObjLo );
- else
- assert( 0 );
-// Aig_XsimPrint( stdout, Value );
- }
-// printf( "\n" );
- Vec_PtrFree( vStates );
- if ( fVerbose )
- printf( "Detected %d constants after %d iterations.\n", nCounter, f );
- return vMap;
-}
-
-/**Function*************************************************************
-
- Synopsis [Reduces the circuit using ternary simulation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose )
-{
- Aig_Man_t * pTemp;
- Vec_Ptr_t * vMap;
- while ( vMap = Aig_ManTernarySimulate( p, fVerbose ) )
- {
- if ( fVerbose )
- printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
- p = Aig_ManRemap( pTemp = p, vMap );
- Aig_ManStop( pTemp );
- Vec_PtrFree( vMap );
- Aig_ManSeqCleanup( p );
- if ( fVerbose )
- printf( "REnd = %5d. NEnd = %6d. \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
- }
- return p;
-}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
new file mode 100644
index 00000000..b8296cb2
--- /dev/null
+++ b/src/aig/aig/aigTsim.c
@@ -0,0 +1,436 @@
+/**CFile****************************************************************
+
+ FileName [aigTsim.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG package.]
+
+ Synopsis [Ternary simulation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: aigTsim.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define TSI_MAX_ROUNDS 10000
+
+#define AIG_XVS0 1
+#define AIG_XVS1 2
+#define AIG_XVSX 3
+
+static inline void Aig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; }
+static inline int Aig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; }
+static inline int Aig_XsimInv( int Value )
+{
+ if ( Value == AIG_XVS0 )
+ return AIG_XVS1;
+ if ( Value == AIG_XVS1 )
+ return AIG_XVS0;
+ assert( Value == AIG_XVSX );
+ return AIG_XVSX;
+}
+static inline int Aig_XsimAnd( int Value0, int Value1 )
+{
+ if ( Value0 == AIG_XVS0 || Value1 == AIG_XVS0 )
+ return AIG_XVS0;
+ if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX )
+ return AIG_XVSX;
+ assert( Value0 == AIG_XVS1 && Value1 == AIG_XVS1 );
+ return AIG_XVS1;
+}
+static inline int Aig_XsimRand2()
+{
+ return (rand() & 1) ? AIG_XVS1 : AIG_XVS0;
+}
+static inline int Aig_XsimRand3()
+{
+ int RetValue;
+ do {
+ RetValue = rand() & 3;
+ } while ( RetValue == 0 );
+ return RetValue;
+}
+static inline int Aig_ObjGetXsimFanin0( Aig_Obj_t * pObj )
+{
+ int RetValue;
+ RetValue = Aig_ObjGetXsim(Aig_ObjFanin0(pObj));
+ return Aig_ObjFaninC0(pObj)? Aig_XsimInv(RetValue) : RetValue;
+}
+static inline int Aig_ObjGetXsimFanin1( Aig_Obj_t * pObj )
+{
+ int RetValue;
+ RetValue = Aig_ObjGetXsim(Aig_ObjFanin1(pObj));
+ return Aig_ObjFaninC1(pObj)? Aig_XsimInv(RetValue) : RetValue;
+}
+static inline void Aig_XsimPrint( FILE * pFile, int Value )
+{
+ if ( Value == AIG_XVS0 )
+ {
+ fprintf( pFile, "0" );
+ return;
+ }
+ if ( Value == AIG_XVS1 )
+ {
+ fprintf( pFile, "1" );
+ return;
+ }
+ assert( Value == AIG_XVSX );
+ fprintf( pFile, "x" );
+}
+
+// simulation manager
+typedef struct Aig_Tsi_t_ Aig_Tsi_t;
+struct Aig_Tsi_t_
+{
+ Aig_Man_t * pAig; // the original AIG manager
+ // ternary state representation
+ int nWords; // the number of words in the states
+ Vec_Ptr_t * vStates; // the collection of ternary states
+ Aig_MmFixed_t * pMem; // memory for ternary states
+ // hash table for terminary states
+ unsigned ** pBins;
+ int nBins;
+};
+
+static inline unsigned * Aig_TsiNext( unsigned * pState, int nWords ) { return *((unsigned **)(pState + nWords)); }
+static inline void Aig_TsiSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocates simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Tsi_t * Aig_TsiStart( Aig_Man_t * pAig )
+{
+ Aig_Tsi_t * p;
+ p = (Aig_Tsi_t *)malloc( sizeof(Aig_Tsi_t) );
+ memset( p, 0, sizeof(Aig_Tsi_t) );
+ p->pAig = pAig;
+ p->nWords = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) );
+ p->vStates = Vec_PtrAlloc( 1000 );
+ p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 );
+ p->nBins = Aig_PrimeCudd(TSI_MAX_ROUNDS/2);
+ p->pBins = ALLOC( unsigned *, p->nBins );
+ memset( p->pBins, 0, sizeof(unsigned *) * p->nBins );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TsiStop( Aig_Tsi_t * p )
+{
+ Aig_MmFixedStop( p->pMem, 0 );
+ Vec_PtrFree( p->vStates );
+ free( p->pBins );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes hash value of the node using its simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_TsiStateHash( unsigned * pState, int nWords, int nTableSize )
+{
+ static int s_FPrimes[128] = {
+ 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
+ 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
+ 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
+ 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
+ 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
+ 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
+ 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
+ 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
+ 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
+ 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
+ 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
+ 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
+ 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+ };
+ unsigned uHash;
+ int i;
+ uHash = 0;
+ for ( i = 0; i < nWords; i++ )
+ uHash ^= pState[i] * s_FPrimes[i & 0x7F];
+ return uHash % nTableSize;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts value into the table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_TsiStateLookup( Aig_Tsi_t * p, unsigned * pState, int nWords )
+{
+ unsigned * pEntry;
+ int Hash;
+ Hash = Aig_TsiStateHash( pState, nWords, p->nBins );
+ for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Aig_TsiNext(pEntry, nWords) )
+ if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts value into the table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TsiStateInsert( Aig_Tsi_t * p, unsigned * pState, int nWords )
+{
+ int Hash = Aig_TsiStateHash( pState, nWords, p->nBins );
+ assert( !Aig_TsiStateLookup( p, pState, nWords ) );
+ Aig_TsiSetNext( pState, nWords, p->pBins[Hash] );
+ p->pBins[Hash] = pState;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts value into the table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Aig_TsiStateNew( Aig_Tsi_t * p )
+{
+ unsigned * pState;
+ pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMem );
+ memset( pState, 0, sizeof(unsigned) * p->nWords );
+ Vec_PtrPush( p->vStates, pState );
+ return pState;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts value into the table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TsiStatePrint( Aig_Tsi_t * p, unsigned * pState )
+{
+ int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
+ for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
+ {
+ Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+ if ( Value == 1 )
+ printf( "0" ), nZeros++;
+ else if ( Value == 2 )
+ printf( "1" ), nOnes++;
+ else if ( Value == 3 )
+ printf( "x" ), nDcs++;
+ else
+ assert( 0 );
+ }
+ printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Cycles the circuit to create a new initial state.]
+
+ Description [Simulates the circuit with random input for the given
+ number of timeframes to get a better initial state.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
+{
+ Aig_Tsi_t * pTsi;
+ Vec_Ptr_t * vMap;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ unsigned * pState, * pPrev;
+ int i, k, f, fConstants, Value, nCounter;
+ // allocate the simulation manager
+ pTsi = Aig_TsiStart( p );
+ // initialize the values
+ Aig_ObjSetXsim( Aig_ManConst1(p), AIG_XVS1 );
+ Aig_ManForEachPiSeq( p, pObj, i )
+ Aig_ObjSetXsim( pObj, AIG_XVSX );
+ Aig_ManForEachLoSeq( p, pObj, i )
+ Aig_ObjSetXsim( pObj, AIG_XVS0 );
+ // simulate for the given number of timeframes
+ for ( f = 0; f < TSI_MAX_ROUNDS; f++ )
+ {
+ // collect this state
+ pState = Aig_TsiStateNew( pTsi );
+ Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+ {
+ Value = Aig_ObjGetXsim(pObjLo);
+ if ( Value & 1 )
+ Aig_InfoSetBit( pState, 2 * i );
+ if ( Value & 2 )
+ Aig_InfoSetBit( pState, 2 * i + 1 );
+ }
+// Aig_TsiStatePrint( pTsi, pState );
+ // check if this state exists
+ if ( Aig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
+ break;
+ // insert this state
+ Aig_TsiStateInsert( pTsi, pState, pTsi->nWords );
+ // simulate internal nodes
+ Aig_ManForEachNode( p, pObj, i )
+ Aig_ObjSetXsim( pObj, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) );
+ // transfer the latch values
+ Aig_ManForEachLiSeq( p, pObj, i )
+ Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) );
+ Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+ Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
+ }
+ if ( f == TSI_MAX_ROUNDS )
+ {
+ printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations.\n", TSI_MAX_ROUNDS );
+ Aig_TsiStop( pTsi );
+ return NULL;
+ }
+ // OR all the states
+ pState = Vec_PtrEntry( pTsi->vStates, 0 );
+ Vec_PtrForEachEntry( pTsi->vStates, pPrev, i )
+ {
+ for ( k = 0; k < pTsi->nWords; k++ )
+ pState[k] |= pPrev[k];
+ }
+ // check if there are constants
+ fConstants = 0;
+ if ( 2*Aig_ManRegNum(p) == 32*pTsi->nWords )
+ {
+ for ( i = 0; i < pTsi->nWords; i++ )
+ if ( pState[i] != ~0 )
+ fConstants = 1;
+ }
+ else
+ {
+ for ( i = 0; i < pTsi->nWords - 1; i++ )
+ if ( pState[i] != ~0 )
+ fConstants = 1;
+ if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(pTsi->nWords-1) ) )
+ fConstants = 1;
+ }
+ if ( fConstants == 0 )
+ {
+ Aig_TsiStop( pTsi );
+ return NULL;
+ }
+
+ // start mapping by adding the true PIs
+ vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
+ Aig_ManForEachPiSeq( p, pObj, i )
+ Vec_PtrPush( vMap, pObj );
+ // find constant registers
+ nCounter = 0;
+ Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+ {
+ Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+ nCounter += (Value == 1 || Value == 2);
+ if ( Value == 1 )
+ Vec_PtrPush( vMap, Aig_ManConst0(p) );
+ else if ( Value == 2 )
+ Vec_PtrPush( vMap, Aig_ManConst1(p) );
+ else if ( Value == 3 )
+ Vec_PtrPush( vMap, pObjLo );
+ else
+ assert( 0 );
+// Aig_XsimPrint( stdout, Value );
+ }
+// printf( "\n" );
+ Aig_TsiStop( pTsi );
+ if ( fVerbose )
+ printf( "Detected %d constants after %d iterations of ternary simulation.\n", nCounter, f );
+ return vMap;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reduces the circuit using ternary simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose )
+{
+ Aig_Man_t * pTemp;
+ Vec_Ptr_t * vMap;
+ while ( vMap = Aig_ManTernarySimulate( p, fVerbose ) )
+ {
+ if ( fVerbose )
+ printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+ p = Aig_ManRemap( pTemp = p, vMap );
+ Aig_ManStop( pTemp );
+ Vec_PtrFree( vMap );
+ Aig_ManSeqCleanup( p );
+ if ( fVerbose )
+ printf( "REnd = %5d. NEnd = %6d. \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+ }
+ return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 93b25e4a..45ed62ee 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -13,5 +13,6 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigTable.c \
src/aig/aig/aigTiming.c \
src/aig/aig/aigTruth.c \
+ src/aig/aig/aigTsim.c \
src/aig/aig/aigUtil.c \
src/aig/aig/aigWin.c \ No newline at end of file
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index c8617d84..217d1fba 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -73,6 +73,7 @@ struct Fra_Par_t_
int nBTLimitMiter; // conflict limit at an output
int nFramesP; // the number of timeframes to in the prefix
int nFramesK; // the number of timeframes to unroll
+ int nMaxImps; // the maximum number of implications to consider
int fRewrite; // use rewriting for constraint reduction
int fLatchCorr; // computes latch correspondence only
int fUseImps; // use implications
@@ -133,6 +134,7 @@ struct Fra_Man_t_
// counter example storage
int nPatWords; // the number of words in the counter example
unsigned * pPatWords; // the counter example
+ Vec_Int_t * vCex;
// satisfiability solving
sat_solver * pSat; // SAT solver
int nSatVars; // the number of variables currently used
@@ -226,6 +228,8 @@ extern int Fra_ClassesCountPairs( Fra_Cla_t * p );
extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
extern void Fra_ClassesLatchCorr( Fra_Man_t * p );
extern void Fra_ClassesPostprocess( Fra_Cla_t * p );
+extern void Fra_ClassesSelectRepr( Fra_Cla_t * p );
+extern Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
/*=== fraCnf.c ========================================================*/
extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== fraCore.c ========================================================*/
@@ -240,7 +244,7 @@ extern int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps
extern int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
extern void Fra_ImpCompactArray( Vec_Int_t * vImps );
/*=== fraInd.c ========================================================*/
-extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
+extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
/*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( Fra_Par_t * pParams );
extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index a9d727da..d6db125b 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -114,9 +114,18 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
int i;
Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 );
memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) );
+ if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
+ {
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ {
+ if ( p->pAig->pReprs[i] != NULL )
+ printf( "Classes are not cleared!\n" );
+ assert( p->pAig->pReprs[i] == NULL );
+ }
+ }
if ( vFailed )
- Vec_PtrForEachEntry( vFailed, pObj, i )
- p->pAig->pReprs[pObj->Id] = NULL;
+ Vec_PtrForEachEntry( vFailed, pObj, i )
+ p->pAig->pReprs[pObj->Id] = NULL;
}
/**Function*************************************************************
@@ -206,7 +215,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass )
assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
printf( "{ " );
for ( i = 0; pTemp = pClass[i]; i++ )
- printf( "%d ", pTemp->Id, Fra_ClassObjRepr(pTemp)? Fra_ClassObjRepr(pTemp)->Id : -1 );
+ printf( "%d(%d) ", pTemp->Id, pTemp->Level );
printf( "}\n" );
}
@@ -227,8 +236,11 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
Aig_Obj_t * pObj;
int i;
- printf( "Const = %5d. Class = %5d. Lit = %5d.\n",
+ printf( "Const = %5d. Class = %5d. Lit = %5d. ",
Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
+ if ( p->vImps && Vec_IntSize(p->vImps) > 0 )
+ printf( "Imp = %5d. ", Vec_IntSize(p->vImps) );
+ printf( "\n" );
if ( fVeryVerbose )
{
@@ -283,10 +295,10 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
{
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
+ // skip the node with more that the given number of levels
+// if ( pObj->Level > 3 )
+// continue;
}
-//printf( "%3d : ", pObj->Id );
-//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 );
-//printf( "\n" );
// hash the node by its simulation info
iEntry = p->pFuncNodeHash( pObj, nTableSize );
// check if the node belongs to the class of constant 1
@@ -494,7 +506,6 @@ int Fra_ClassesRefine( Fra_Cla_t * p )
vTemp = p->vClassesTemp;
p->vClassesTemp = p->vClasses;
p->vClasses = vTemp;
- p->fRefinement = (nRefis > 0);
return nRefis;
}
@@ -531,7 +542,6 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
Vec_PtrShrink( p->vClasses1, k );
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
- p->fRefinement = 1;
/*
printf( "Refined const-1 class: {" );
Vec_PtrForEachEntry( p->vClassNew, pObj, i )
@@ -677,6 +687,95 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
/**Function*************************************************************
+ Synopsis [Postprocesses the classes by selecting representative lowest in top order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ClassesSelectRepr( Fra_Cla_t * p )
+{
+ Aig_Obj_t ** pClass, * pNodeMin;
+ int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
+ // reassign representatives in each class
+ Vec_PtrForEachEntry( p->vClasses, pClass, i )
+ {
+ // collect support sizes and find the min-support node
+ pNodeMin = NULL;
+ nSuppSizeMin = AIG_INFINITY;
+ for ( c = 0; pClass[c]; c++ )
+ {
+ nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
+// nSuppSizeCur = 1;
+ if ( nSuppSizeMin > nSuppSizeCur ||
+ (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) )
+ {
+ nSuppSizeMin = nSuppSizeCur;
+ pNodeMin = pClass[c];
+ cMinSupp = c;
+ }
+ }
+ // skip the case when the repr did not change
+ if ( cMinSupp == 0 )
+ continue;
+ // make the new node the representative of the class
+ pClass[cMinSupp] = pClass[0];
+ pClass[0] = pNodeMin;
+ // set the representative
+ for ( c = 0; pClass[c]; c++ )
+ Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL );
+ }
+}
+
+
+
+static inline Aig_Obj_t * Fra_ObjEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return ppEquivs[pObj->Id]; }
+static inline void Fra_ObjSetEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ppEquivs[pObj->Id] = pNode; }
+
+static inline Aig_Obj_t * Fra_ObjChild0Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)); }
+static inline Aig_Obj_t * Fra_ObjChild1Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)); }
+
+/**Function*************************************************************
+
+ Synopsis [Add the node and its constraints to the new AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, Aig_Obj_t ** ppEquivs )
+{
+ Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2;
+ // skip nodes without representative
+ if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
+ return;
+ assert( pObjRepr->Id < pObj->Id );
+ // get the new node
+ pObjNew = Fra_ObjEqu( ppEquivs, pObj );
+ // get the new node of the representative
+ pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr );
+ // if this is the same node, no need to add constraints
+ if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
+ return;
+ // these are different nodes - perform speculative reduction
+// pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
+ // set the new node
+// Fra_ObjSetEqu( ppEquivs, pObj, pObjNew2 );
+ // add the constraint
+ pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
+ pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
+ pMiter = Aig_Not( pMiter );
+ Aig_ObjCreatePo( pManFraig, pMiter );
+}
+
+/**Function*************************************************************
+
Synopsis [Derives AIG for the partitioned problem.]
Description []
@@ -688,7 +787,60 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
***********************************************************************/
Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
{
-
+ Aig_Man_t * pManFraig;
+ Aig_Obj_t * pObj, * pObjNew;
+ Aig_Obj_t ** pLatches, ** ppEquivs;
+ int i, k, f, nFramesAll = nFramesK + 1;
+ assert( Aig_ManRegNum(p->pAig) > 0 );
+ assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+ assert( nFramesK > 0 );
+ // start the fraig package
+ pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * nFramesAll );
+ // allocate place for the node mapping
+ ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p->pAig) + 1 );
+ Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
+ // create latches for the first frame
+ Aig_ManForEachLoSeq( p->pAig, pObj, i )
+ Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
+ // add timeframes
+ pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
+ for ( f = 0; f < nFramesAll; f++ )
+ {
+ // create PIs for this frame
+ Aig_ManForEachPiSeq( p->pAig, pObj, i )
+ Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
+ // set the constraints on the latch outputs
+ Aig_ManForEachLoSeq( p->pAig, pObj, i )
+ Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
+ // add internal nodes of this frame
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ {
+ pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) );
+ Fra_ObjSetEqu( ppEquivs, pObj, pObjNew );
+ Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
+ }
+ if ( f == nFramesAll - 1 )
+ break;
+ if ( f == nFramesAll - 2 )
+ pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
+ // save the latch input values
+ k = 0;
+ Aig_ManForEachLiSeq( p->pAig, pObj, i )
+ pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj );
+ // insert them to the latch output values
+ k = 0;
+ Aig_ManForEachLoSeq( p->pAig, pObj, i )
+ Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
+ }
+ free( pLatches );
+ free( ppEquivs );
+ // mark the asserts
+ assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
+printf( "Assert miters = %6d. Output miters = %6d.\n",
+ pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts );
+ // remove dangling nodes
+ Aig_ManCleanup( pManFraig );
+ return pManFraig;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 3c76af03..9adbb7a9 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -24,6 +24,23 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+/*
+ Speculating reduction in the sequential case leads to an interesting
+ situation when a counter-ex may not refine any classes. This happens
+ for non-constant equivalence classes. In such cases the representative
+ of the class (proved by simulation to be non-constant) may be reduced
+ to a constant during the speculative reduction. The fraig-representative
+ of this representative node is a constant node, even though this is a
+ non-constant class. Experiments have shown that this situation happens
+ very often at the beginning of the refinement iteration when there are
+ many spurious candidate equivalence classes (especially if heavy-duty
+ simulatation of BMC was node used at the beginning). As a result, the
+ SAT solver run may return a counter-ex that distinguishes the given
+ representative node from the constant-1 node but this counter-ex
+ does not distinguish the nodes in the non-costant class... This is why
+ there is no check of refinment after a counter-ex in the sequential case.
+*/
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -117,6 +134,54 @@ static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_
/**Function*************************************************************
+ Synopsis [Verifies the generated counter-ex.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex )
+{
+ Aig_Obj_t * pObj, ** ppClass;
+ int i, c;
+ assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) );
+ // make sure the input pattern is not used
+ Aig_ManForEachObj( p->pManAig, pObj, i )
+ assert( !pObj->fMarkB );
+ // simulate the cex through the AIG
+ Aig_ManConst1(p->pManAig)->fMarkB = 1;
+ Aig_ManForEachPi( p->pManAig, pObj, i )
+ pObj->fMarkB = Vec_IntEntry(vCex, i);
+ Aig_ManForEachNode( p->pManAig, pObj, i )
+ pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
+ (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+ Aig_ManForEachPo( p->pManAig, pObj, i )
+ pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+ // check if the classes hold
+ Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
+ {
+ if ( pObj->fPhase != pObj->fMarkB )
+ printf( "The node %d is not constant under cex!\n", pObj->Id );
+ }
+ Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
+ {
+ for ( c = 1; ppClass[c]; c++ )
+ if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) )
+ printf( "The nodes %d and %d are not equal under cex!\n", ppClass[0]->Id, ppClass[c]->Id );
+// for ( c = 0; ppClass[c]; c++ )
+// if ( Fra_ObjFraig(ppClass[c],p->pPars->nFramesK) == Aig_ManConst1(p->pManFraig) )
+// printf( "A member of non-constant class has a constant repr!\n" );
+ }
+ // clean the simulation pattern
+ Aig_ManForEachObj( p->pManAig, pObj, i )
+ pObj->fMarkB = 0;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
@@ -173,47 +238,20 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
return;
}
-//printf( "Disproved %d and %d.\n", pObj->Id, pObjRepr->Id );
// disprove the nodes
+ p->pCla->fRefinement = 1;
// if we do not include the node into those disproved, we may end up
// merging this node with another representative, for which proof has timed out
if ( p->vTimeouts )
Vec_PtrPush( p->vTimeouts, pObj );
+ // verify that the counter-example satisfies all the constraints
+// if ( p->vCex )
+// Fra_FraigVerifyCounterEx( p, p->vCex );
// simulate the counter-example and return the Fraig node
Fra_SmlResimulate( p );
-/*
-printf( "%d -> %d.\n", pObj->Id, pObjRepr->Id );
-Fra_ClassesPrint( p->pCla, 1 );
-printf( "%3d : ", 19 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 19), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", 27 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 27), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", 30 );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 30), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "\n\n" );
-*/
- if ( Fra_ClassObjRepr(pObj) == pObjRepr )
- {
-/*
-//Fra_ClassesPrint( p->pCla, 1 );
-//printf( "\n\n" );
-printf( "%3d : ", pObj->Id );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObj->Id), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-printf( "%3d : ", pObjRepr->Id );
-Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObjRepr->Id), 32 * p->pSml->nWordsTotal );
-printf( "\n" );
-*/
- if ( Aig_ObjIsPi(pObj) )
- printf( "primary input\n" );
- else
- printf( "NOT primary input\n" );
+ if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
printf( "Fra_FraigNode(): Error in class refinement!\n" );
- }
- assert( Fra_ClassObjRepr(pObj) != pObjRepr );
+ assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr );
}
/**Function*************************************************************
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index 25b34e03..8af11b78 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -205,7 +205,7 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit )
+Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange )
{
Vec_Int_t * vImpsNew;
int * pCostCount, nImpCount, Imp, i, c;
@@ -239,6 +239,8 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax,
break;
}
free( pCostCount );
+ if ( pCostRange )
+ *pCostRange = c;
return vImpsNew;
}
@@ -290,7 +292,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
int * pImpCosts, * pNodesI, * pNodesK;
int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
int CostMin = AIG_INFINITY, CostMax = 0;
- int i, k, Imp, clk = clock();
+ int i, k, Imp, CostRange, clk = clock();
assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
// normalize both managers
pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
@@ -350,9 +352,10 @@ finish:
Fra_SmlStop( pSeq );
// select implications with the highest cost
+ CostRange = CostMin;
if ( Vec_IntSize(vImps) > nImpUseLimit )
{
- vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit );
+ vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
Vec_IntFree( vTemp );
}
@@ -365,8 +368,8 @@ finish:
(int (*)(const void *, const void *)) Sml_CompareMaxId );
if ( p->pPars->fVerbose )
{
-printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d. Cost = [%d - %d] ",
- nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostMax );
+printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d. Cost = [%d < %d < %d] ",
+ nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostRange, CostMax );
PRT( "Time", clock() - clk );
}
return vImps;
@@ -381,7 +384,7 @@ PRT( "Time", clock() - clk );
Synopsis [Add implication clauses to the SAT solver.]
- Description []
+ Description [Note that implications should be checked in the first frame!]
SideEffects []
@@ -540,7 +543,6 @@ int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
{
Vec_IntWriteEntry( vImps, i, 0 );
RetValue = 1;
- p->pCla->fRefinement = 1;
}
}
return RetValue;
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index d754f3ae..6d8305c0 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -50,11 +50,9 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p )
pTemp = Aig_ManDup( p->pManFraig, 0 );
// pTemp = Dar_ManRwsat( pTemp, 1, 0 );
pTemp = Dar_ManRewriteDefault( pTemp );
-
// printf( "Before = %6d. After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) );
//Aig_ManDumpBlif( p->pManFraig, "1.blif" );
//Aig_ManDumpBlif( pTemp, "2.blif" );
-
// Fra_FramesWriteCone( pTemp );
// Aig_ManStop( pTemp );
// transfer PI/register pointers
@@ -128,8 +126,7 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p
Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
{
Aig_Man_t * pManFraig;
- Aig_Obj_t * pObj, * pObjNew;
- Aig_Obj_t ** pLatches;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
int i, k, f;
assert( p->pManFraig == NULL );
assert( Aig_ManRegNum(p->pManAig) > 0 );
@@ -149,7 +146,6 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
// add timeframes
- pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pManAig) );
for ( f = 0; f < p->nFramesAll - 1; f++ )
{
// set the constraints on the latch outputs
@@ -162,23 +158,15 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
Fra_ObjSetFraig( pObj, f, pObjNew );
Fra_FramesConstrainNode( pManFraig, pObj, f );
}
- // save the latch input values
- k = 0;
- Aig_ManForEachLiSeq( p->pManAig, pObj, i )
- pLatches[k++] = Fra_ObjChild0Fra(pObj,f);
- assert( k == Aig_ManRegNum(p->pManAig) );
- // insert them to the latch output values
- k = 0;
- Aig_ManForEachLoSeq( p->pManAig, pObj, i )
- Fra_ObjSetFraig( pObj, f+1, pLatches[k++] );
- assert( k == Aig_ManRegNum(p->pManAig) );
+ // transfer latch input to the latch outputs
+ Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k )
+ Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) );
}
- free( pLatches );
// mark the asserts
pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
- // add the POs for the latch inputs
- Aig_ManForEachLiSeq( p->pManAig, pObj, i )
- Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) );
+ // add the POs for the latch outputs of the last frame
+ Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+ Aig_ObjCreatePo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
// remove dangling nodes
Aig_ManCleanup( pManFraig );
@@ -198,7 +186,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
{
int fUseSimpleCnf = 0;
int fUseOldSimulation = 0;
@@ -229,6 +217,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
Fra_ParamsDefaultSeq( pPars );
pPars->nFramesP = nFramesP;
pPars->nFramesK = nFramesK;
+ pPars->nMaxImps = nMaxImps;
pPars->fVerbose = fVerbose;
pPars->fRewrite = fRewrite;
pPars->fLatchCorr = fLatchCorr;
@@ -249,9 +238,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
}
else
{
+ // bug: r iscas/blif/s5378.blif ; st; ssw -v
// bug: r iscas/blif/s1238.blif ; st; ssw -v
// refine the classes with more simulation rounds
- p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 2 ); //pPars->nFramesK + 1, 6 ); // 32, 2 );
+if ( fVerbose )
+printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
+ p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );
+if ( fVerbose )
+{
+PRT( "Time", clock() - clk );
+}
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
// Fra_ClassesPostprocess( p->pCla );
// allocate new simulation manager for simulating counter-examples
@@ -259,19 +255,26 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
}
- // perform BMC
- Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK + 1 );
+ // perform BMC (for the min number of frames)
+ Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK );
//Fra_ClassesPrint( p->pCla, 1 );
+// p->vCex = Vec_IntAlloc( 1000 );
// select the most expressive implications
if ( pPars->fUseImps )
- p->pCla->vImps = Fra_ImpDerive( p, 5000000, 5000, pPars->fLatchCorr );
+ p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
p->nNodesBeg = Aig_ManNodeNum(pManAig);
p->nRegsBeg = Aig_ManRegNum(pManAig);
+ // dump AIG of the timeframes
+// pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
+// Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" );
+// Fra_ManPartitionTest2( pManAigNew );
+// Aig_ManStop( pManAigNew );
+
// iterate the inductive case
p->pCla->fRefinement = 1;
for ( nIter = 0; p->pCla->fRefinement; nIter++ )
@@ -341,7 +344,11 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
// cleanup
Fra_ManClean( p );
+// if ( nIter == 3 )
+// break;
}
+// Fra_ClassesPrint( p->pCla, 1 );
+// Fra_ClassesSelectRepr( p->pCla );
// move the classes into representatives and reduce AIG
clk2 = clock();
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 2b8e0a68..0116bbc4 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -248,6 +248,7 @@ void Fra_ManStop( Fra_Man_t * p )
if ( p->pSat ) sat_solver_delete( p->pSat );
if ( p->pCla ) Fra_ClassesStop( p->pCla );
if ( p->pSml ) Fra_SmlStop( p->pSml );
+ if ( p->vCex ) Vec_IntFree( p->vCex );
FREE( p->pMemFraig );
FREE( p->pMemFanins );
FREE( p->pMemSatNums );
diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c
index d3fdbcfd..6e593694 100644
--- a/src/aig/fra/fraPart.c
+++ b/src/aig/fra/fraPart.c
@@ -170,6 +170,92 @@ PRT( "Scanning", clock() - clk );
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ManPartitionTest2( Aig_Man_t * p )
+{
+ Vec_Vec_t * vSupps, * vSuppsIn;
+ Vec_Int_t * vSup, * vSup2, * vSup3;
+ Aig_Obj_t * pObj;
+ int Entry, Entry2, Entry3, Counter;
+ int i, k, m, n, clk;
+ char * pSupp;
+
+ // compute supports
+clk = clock();
+ vSupps = Aig_ManSupports( p );
+PRT( "Supports", clock() - clk );
+ // remove last entry
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ vSup = Vec_VecEntry( vSupps, i );
+ Vec_IntPop( vSup );
+ // remember support
+// pObj->pNext = (Aig_Obj_t *)vSup;
+ }
+
+ // create reverse supports
+clk = clock();
+ vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ if ( i == p->nAsserts )
+ break;
+ vSup = Vec_VecEntry( vSupps, i );
+ Vec_IntForEachEntry( vSup, Entry, k )
+ Vec_VecPush( vSuppsIn, Entry, (void *)i );
+ }
+PRT( "Inverse ", clock() - clk );
+
+ // create affective supports
+clk = clock();
+ pSupp = ALLOC( char, Aig_ManPiNum(p) );
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ if ( i % 50 != 0 )
+ continue;
+ vSup = Vec_VecEntry( vSupps, i );
+ memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) );
+ // go through each input of this output
+ Vec_IntForEachEntry( vSup, Entry, k )
+ {
+ pSupp[Entry] = 1;
+ vSup2 = Vec_VecEntry( vSuppsIn, Entry );
+ // go though each assert of this input
+ Vec_IntForEachEntry( vSup2, Entry2, m )
+ {
+ vSup3 = Vec_VecEntry( vSupps, Entry2 );
+ // go through each input of this assert
+ Vec_IntForEachEntry( vSup3, Entry3, n )
+ {
+ pSupp[Entry3] = 1;
+ }
+ }
+ }
+ // count the entries
+ Counter = 0;
+ for ( m = 0; m < Aig_ManPiNum(p); m++ )
+ Counter += pSupp[m];
+ printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
+ }
+ printf( "\n" );
+PRT( "Extension ", clock() - clk );
+
+ free( pSupp );
+ Vec_VecFree( vSupps );
+ Vec_VecFree( vSuppsIn );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 2a0d06b5..8b9258cb 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -43,11 +43,12 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
{
Aig_Man_t * pNew;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
+ int fLatchCorr = 0;
if ( nFramesFix )
{
nFrames = nFramesFix;
// perform seq sweeping for one frame number
- pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+ pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
}
else
{
@@ -55,7 +56,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
for ( nFrames = 1; ; nFrames++ )
{
clk = clock();
- pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+ pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
{
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index b31fcb7f..3463ee0d 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -200,6 +200,17 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
Aig_InfoSetBit( p->pPatWords, i );
/*
+ if ( p->vCex )
+ {
+ Vec_IntClear( p->vCex );
+ for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
+ Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
+ for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ )
+ Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
+ }
+*/
+
+/*
printf( "Pattern: " );
Aig_ManForEachPi( p->pManFraig, pObj, i )
printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) );
@@ -601,7 +612,7 @@ clk = clock();
if ( p->pCla->vImps )
nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
p->timeRef += clock() - clk;
- if ( nChanges < 1 )
+ if ( !p->pPars->nFramesK && nChanges < 1 )
printf( "Error: A counter-example did not refine classes!\n" );
// assert( nChanges >= 1 );
//printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
diff --git a/src/aig/ivy/ivyMan.c b/src/aig/ivy/ivyMan.c
index 2d99c4f1..07faef85 100644
--- a/src/aig/ivy/ivyMan.c
+++ b/src/aig/ivy/ivyMan.c
@@ -411,7 +411,7 @@ int Ivy_ManLatchIsSelfFeed( Ivy_Obj_t * pLatch )
int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
{
Ivy_Obj_t * pNode;
- int LimitFactor = 10;
+ int LimitFactor = 100;
int NodeBeg = Ivy_ManNodeNum(p);
int nSteps;
for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c2eead14..78519d40 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6293,7 +6293,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// pNtkRes = Abc_NtkDar( pNtk );
- pNtkRes = Abc_NtkDarRetime( pNtk, 100, 1 );
+ pNtkRes = Abc_NtkDarRetime( pNtk, 1000, 1 );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -10974,12 +10974,13 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int nFramesP;
int nFramesK;
+ int nMaxImps;
int fExdc;
int fUseImps;
int fRewrite;
int fLatchCorr;
int fVerbose;
- extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -10988,13 +10989,14 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nFramesP = 0;
nFramesK = 1;
+ nMaxImps = 5000;
fExdc = 1;
fUseImps = 0;
fRewrite = 0;
fLatchCorr = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "PFeirlvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "PFIeirlvh" ) ) != EOF )
{
switch ( c )
{
@@ -11020,6 +11022,17 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nFramesK <= 0 )
goto usage;
break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nMaxImps = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nMaxImps <= 0 )
+ goto usage;
+ break;
case 'e':
fExdc ^= 1;
break;
@@ -11061,7 +11074,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
- pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose );
+ pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -11072,10 +11085,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: ssweep [-P num] [-F num] [-ilrvh]\n" );
+ fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrvh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
+ fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", nMaxImps );
// fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", fUseImps? "yes": "no" );
fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 99217030..ce783c95 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -892,11 +892,12 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
{
Fraig_Params_t Params;
Abc_Ntk_t * pNtkAig, * pNtkFraig;
Aig_Man_t * pMan, * pTemp;
+ int clk = clock();
// preprocess the miter by fraiging it
// (note that for each functional class, fraiging leaves one representative;
@@ -905,13 +906,17 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in
Params.nBTLimit = 100000;
pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
// pNtkFraig = Abc_NtkDup( pNtk );
+if ( fVerbose )
+{
+PRT( "Initial fraiging time", clock() - clk );
+}
pMan = Abc_NtkToDar( pNtkFraig, 1 );
Abc_NtkDelete( pNtkFraig );
if ( pMan == NULL )
return NULL;
- pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
+ pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
Aig_ManStop( pTemp );
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
@@ -1033,7 +1038,7 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
- pMan = Rtm_ManRetimeFwd( pTemp = pMan, nStepsMax, fVerbose );
+ pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
Aig_ManStop( pTemp );
// pMan = Aig_ManReduceLaches( pMan, 1 );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 4c061637..004d1f39 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -127,13 +127,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
/*
{
FILE * pTable;
- pTable = fopen( "iscas/seqmap__stats.txt", "a+" );
+ pTable = fopen( "xs/reg_stats.txt", "a+" );
fprintf( pTable, "%s ", pNtk->pName );
- fprintf( pTable, "%d ", Abc_NtkPiNum(pNtk) );
- fprintf( pTable, "%d ", Abc_NtkPoNum(pNtk) );
fprintf( pTable, "%d ", Abc_NtkLatchNum(pNtk) );
fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
- fprintf( pTable, "%d ", Abc_NtkLevel(pNtk) );
fprintf( pTable, "\n" );
fclose( pTable );
}
diff --git a/todo.txt b/todo.txt
index 348930d3..3ab59b8c 100644
--- a/todo.txt
+++ b/todo.txt
@@ -21,3 +21,6 @@
- comparing tts of differently derived the same cut
- area flow based AIG rewriting
- cut frontier adjustment
+
+
+