summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aig.h7
-rw-r--r--src/aig/aig/aigDup.c2
-rw-r--r--src/aig/aig/aigRepr.c28
-rw-r--r--src/aig/aig/aigScl.c54
-rw-r--r--src/aig/fra/fraInd.c4
-rw-r--r--src/aig/ntl/ntl.h1
-rw-r--r--src/aig/ntl/ntlExtract.c30
-rw-r--r--src/aig/ntl/ntlFraig.c122
-rw-r--r--src/aig/nwk/module.make4
-rw-r--r--src/aig/nwk/nwk.h29
-rw-r--r--src/aig/nwk/nwkAig.c107
-rw-r--r--src/aig/nwk/nwkFlow.c593
-rw-r--r--src/aig/nwk/nwkUtil.c18
-rw-r--r--src/aig/nwk/nwkUtil_old.c615
-rw-r--r--src/aig/saig/module.make3
-rw-r--r--src/aig/saig/saigRetMin.c262
16 files changed, 1874 insertions, 5 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 8593fd76..74e3de31 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -66,7 +66,10 @@ typedef enum {
// the AIG node
struct Aig_Obj_t_ // 8 words
{
- Aig_Obj_t * pNext; // strashing table
+ union {
+ Aig_Obj_t * pNext; // strashing table
+ int PioNum; // the number of PI/PO
+ };
Aig_Obj_t * pFanin0; // fanin
Aig_Obj_t * pFanin1; // fanin
Aig_Obj_t * pHaig; // pointer to the HAIG node
@@ -551,6 +554,7 @@ extern void Aig_ManReprStop( Aig_Man_t * p );
extern void Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
extern void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered );
+extern Aig_Man_t * Aig_ManDupReprBasic( Aig_Man_t * p );
extern int Aig_ManCountReprs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p );
extern int Aig_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld );
@@ -563,6 +567,7 @@ extern Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax );
/*=== aigScl.c ==========================================================*/
extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
extern int Aig_ManSeqCleanup( Aig_Man_t * p );
+extern int Aig_ManSeqCleanupBasic( Aig_Man_t * p );
extern int Aig_ManCountMergeRegs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
extern void Aig_ManComputeSccs( Aig_Man_t * p );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 3829ee22..e7623739 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -50,6 +50,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = p->nRegs;
+ pNew->nTruePis = p->nTruePis;
+ pNew->nTruePos = p->nTruePos;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 88cdbf17..54ab0a33 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -302,6 +302,34 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
/**Function*************************************************************
+ Synopsis [Duplicates AIG with representatives without removing registers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupReprBasic( Aig_Man_t * p )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj;
+ int i;
+ assert( p->pReprs != NULL );
+ // reconstruct AIG with representatives
+ pNew = Aig_ManDupRepr( p, 0 );
+ // perfrom sequential cleanup but do not remove registers
+ Aig_ManSeqCleanupBasic( pNew );
+ // remove pointers to the dead nodes
+ Aig_ManForEachObj( p, pObj, i )
+ if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
+ pObj->pData = NULL;
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Transfer representatives and return the number of critical fanouts.]
Description []
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 34b3482d..00a8159e 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -240,6 +240,60 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
Synopsis [Returns the number of dangling nodes removed.]
+ Description [This cleanup procedure is different in that
+ it removes logic but does not remove the dangling latches.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManSeqCleanupBasic( Aig_Man_t * p )
+{
+ Vec_Ptr_t * vNodes;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i;
+// assert( Aig_ManBufNum(p) == 0 );
+
+ // mark the PIs
+ Aig_ManIncrementTravId( p );
+ Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+ Aig_ManForEachPiSeq( p, pObj, i )
+ Aig_ObjSetTravIdCurrent( p, pObj );
+
+ // prepare to collect nodes reachable from POs
+ vNodes = Vec_PtrAlloc( 100 );
+ Aig_ManForEachPoSeq( p, pObj, i )
+ Vec_PtrPush( vNodes, pObj );
+
+ // remember latch inputs in latch outputs
+ Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+ pObjLo->pNext = pObjLi;
+ // mark the nodes reachable from these nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Aig_ManSeqCleanup_rec( p, pObj, vNodes );
+ assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) );
+ // clean latch output pointers
+ Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+ pObjLo->pNext = NULL;
+
+ // if some latches are removed, update PIs/POs
+ if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) )
+ {
+ // add constant drivers to the dangling latches
+ Aig_ManForEachPo( p, pObj, i )
+ if ( !Aig_ObjIsTravIdCurrent(p, pObj) )
+ Aig_ObjPatchFanin0( p, pObj, Aig_ManConst0(p) );
+ }
+ Vec_PtrFree( vNodes );
+ // remove dangling nodes
+ return Aig_ManCleanup( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of dangling nodes removed.]
+
Description []
SideEffects []
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 2dde907c..b29fa946 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -580,6 +580,10 @@ clk2 = clock();
// Fra_ImpRecordInManager( p, pManAigNew );
// cleanup the new manager
Aig_ManSeqCleanup( pManAigNew );
+ // remove pointers to the dead nodes
+// Aig_ManForEachObj( pManAig, pObj, i )
+// if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
+// pObj->pData = NULL;
// Aig_ManCountMergeRegs( pManAigNew );
p->timeTrav += clock() - clk2;
p->timeTotal = clock() - clk;
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 4f00cbda..fc9d21bc 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -120,6 +120,7 @@ struct Ntl_Net_t_
{
Ntl_Net_t * pNext; // next net in the hash table
void * pCopy; // the copy of this object
+ void * pCopy2; // the copy of this object
Ntl_Obj_t * pDriver; // driver of the net
char nVisits; // the number of times the net is visited
char fMark; // temporary mark
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 18ca1a53..5a681a7e 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -233,7 +233,10 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
pRoot = Ntl_ManRootModel( p );
// clear net visited flags
Ntl_ModelForEachNet( pRoot, pNet, i )
+ {
pNet->nVisits = 0;
+ pNet->pCopy = NULL;
+ }
// collect primary inputs
Ntl_ModelForEachPi( pRoot, pObj, i )
{
@@ -417,7 +420,10 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
pRoot = Ntl_ManRootModel( p );
// clear net visited flags
Ntl_ModelForEachNet( pRoot, pNet, i )
+ {
pNet->nVisits = 0;
+ pNet->pCopy = NULL;
+ }
// collect primary inputs
Ntl_ModelForEachPi( pRoot, pObj, i )
{
@@ -486,9 +492,17 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p )
{
Aig_Man_t * pAig;
+ Ntl_Mod_t * pRoot;
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
int i;
+ // clear net visited flags
+ pRoot = Ntl_ManRootModel(p);
+ Ntl_ModelForEachNet( pRoot, pNet, i )
+ {
+ pNet->nVisits = 0;
+ pNet->pCopy = NULL;
+ }
// create the manager
p->pAig = Aig_ManStart( 10000 );
p->pAig->pName = Aig_UtilStrsav( p->pName );
@@ -557,6 +571,13 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
Aig_ObjCreatePo( pAig, Aig_ManConst1(pAig) );
/////////////////////////////////////////////////////
+ // clear net visited flags
+ pRoot1 = Ntl_ManRootModel(p1);
+ Ntl_ModelForEachNet( pRoot1, pNet, i )
+ {
+ pNet->nVisits = 0;
+ pNet->pCopy = NULL;
+ }
// primary inputs
Ntl_ManForEachCiNet( p1, pObj, i )
{
@@ -571,7 +592,6 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
pNet->nVisits = 2;
}
// latch outputs
- pRoot1 = Ntl_ManRootModel(p1);
Ntl_ModelForEachLatch( pRoot1, pObj, i )
{
assert( Ntl_ObjFanoutNum(pObj) == 1 );
@@ -614,6 +634,13 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
}
/////////////////////////////////////////////////////
+ // clear net visited flags
+ pRoot2 = Ntl_ManRootModel(p2);
+ Ntl_ModelForEachNet( pRoot2, pNet, i )
+ {
+ pNet->nVisits = 0;
+ pNet->pCopy = NULL;
+ }
// primary inputs
Ntl_ManForEachCiNet( p2, pObj, i )
{
@@ -628,7 +655,6 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
pNet->nVisits = 2;
}
// latch outputs
- pRoot2 = Ntl_ManRootModel(p2);
Ntl_ModelForEachLatch( pRoot2, pObj, i )
{
assert( Ntl_ObjFanoutNum(pObj) == 1 );
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 63725558..86d92b3c 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -369,6 +369,128 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
}
+
+
+/**Function*************************************************************
+
+ Synopsis [Transfers the copy field into the second copy field.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManTransferCopy( Ntl_Man_t * p )
+{
+ Ntl_Net_t * pNet;
+ Ntl_Mod_t * pRoot;
+ int i;
+ pRoot = Ntl_ManRootModel( p );
+ Ntl_ModelForEachNet( pRoot, pNet, i )
+ {
+ pNet->pCopy2 = pNet->pCopy;
+ pNet->pCopy = NULL;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reattaches one white-box.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManAttachWhiteBox( Ntl_Man_t * p, Aig_Man_t * pAigCol, Aig_Man_t * pAigRed, Ntl_Man_t * pNew, Ntl_Obj_t * pBox )
+{
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reattaches white-boxes after reducing the netlist.]
+
+ Description [The following parameters are given:
+ Original netlist (p) whose nets point to the nodes of collapsed AIG.
+ Collapsed AIG (pAigCol) whose objects point to those of reduced AIG.
+ Reduced AIG (pAigRed) whose objects point to the nets of the new netlist.
+ The new netlist is changed by this procedure to have those white-boxes
+ from the original AIG (p) those outputs are preserved after reduction.
+ Note that if outputs are preserved, the inputs are also preserved.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManAttachWhiteBoxes( Ntl_Man_t * p, Aig_Man_t * pAigCol, Aig_Man_t * pAigRed, Ntl_Man_t * pNew, int fVerbose )
+{
+ Ntl_Mod_t * pRoot;
+ Ntl_Obj_t * pBox;
+ Ntl_Net_t * pNet;
+ int i, k, Counter = 0;
+ // go through the white-boxes and check if they are preserved
+ pRoot = Ntl_ManRootModel( p );
+ Ntl_ModelForEachBox( pRoot, pBox, i )
+ {
+ Ntl_ObjForEachFanout( pBox, pNet, k )
+ {
+ // skip dangling outputs of the box
+ if ( pNet->pCopy == NULL )
+ continue;
+ // skip the outputs that are not preserved after merging equivalence
+ if ( Aig_Regular(pNet->pCopy2)->pData == NULL )
+ continue;
+ break;
+ }
+ if ( k == Ntl_ObjFanoutNum(pBox) )
+ continue;
+ // the box is preserved
+ Ntl_ManAttachWhiteBox( p, pAigCol, pAigRed, pNew, pBox );
+ Counter++;
+ }
+ if ( fVerbose )
+ printf( "Attached %d boxed (out of %d).\n", Counter, Ntl_ModelBoxNum(pRoot) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns AIG with WB after sequential SAT sweeping.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars )
+{
+ Ntl_Man_t * pNew;
+ Aig_Man_t * pAigRed, * pAigCol;
+ // collapse the AIG
+ pAigCol = Ntl_ManCollapse( p );
+ pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+ // transform the collapsed AIG
+ pAigRed = Fra_FraigInduction( pAigCol, pPars );
+ Aig_ManStop( pAigRed );
+ pAigRed = Aig_ManDupReprBasic( pAigCol );
+ // insert the result back
+ Ntl_ManTransferCopy( p );
+ pNew = Ntl_ManInsertAig( p, pAigRed );
+ // attach the white-boxes
+ Ntl_ManAttachWhiteBoxes( p, pAigCol, pAigRed, pNew, pPars->fVerbose );
+ Ntl_ManSweep( pNew, pPars->fVerbose );
+ // cleanup
+ Aig_ManStop( pAigRed );
+ Aig_ManStop( pAigCol );
+ return pNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/nwk/module.make b/src/aig/nwk/module.make
index 3cf2acc6..c0447823 100644
--- a/src/aig/nwk/module.make
+++ b/src/aig/nwk/module.make
@@ -1,7 +1,9 @@
-SRC += src/aig/nwk/nwkCheck.c \
+SRC += src/aig/nwk/nwkAig.c \
+ src/aig/nwk/nwkCheck.c \
src/aig/nwk/nwkBidec.c \
src/aig/nwk/nwkDfs.c \
src/aig/nwk/nwkFanio.c \
+ src/aig/nwk/nwkFlow.c \
src/aig/nwk/nwkMan.c \
src/aig/nwk/nwkMap.c \
src/aig/nwk/nwkObj.c \
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index c087cde8..d0a871cf 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -75,6 +75,10 @@ struct Nwk_Man_t_
Vec_Ptr_t * vTemp; // array used for incremental updates
int nTravIds; // the counter of traversal IDs
int nRealloced; // the number of realloced nodes
+ // sequential information
+ int nLatches; // the total number of latches
+ int nTruePis; // the number of true primary inputs
+ int nTruePos; // the number of true primary outputs
};
struct Nwk_Obj_t_
@@ -88,7 +92,8 @@ struct Nwk_Obj_t_
unsigned fInvert : 1; // complemented attribute
unsigned MarkA : 1; // temporary mark
unsigned MarkB : 1; // temporary mark
- unsigned PioId : 26; // number of this node in the PI/PO list
+ unsigned MarkC : 1; // temporary mark
+ unsigned PioId : 25; // number of this node in the PI/PO list
int Id; // unique ID
int TravId; // traversal ID
// timing information
@@ -140,6 +145,8 @@ static inline int Nwk_ObjIsNode( Nwk_Obj_t * p ) { return p->Ty
static inline int Nwk_ObjIsLatch( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_LATCH; }
static inline int Nwk_ObjIsPi( Nwk_Obj_t * p ) { return Nwk_ObjIsCi(p) && (p->pMan->pManTime == NULL || Tim_ManBoxForCi(p->pMan->pManTime, p->PioId) == -1); }
static inline int Nwk_ObjIsPo( Nwk_Obj_t * p ) { return Nwk_ObjIsCo(p) && (p->pMan->pManTime == NULL || Tim_ManBoxForCo(p->pMan->pManTime, p->PioId) == -1); }
+static inline int Nwk_ObjIsLi( Nwk_Obj_t * p ) { return p->pMan->nTruePos && Nwk_ObjIsCo(p) && (int)p->PioId >= p->pMan->nTruePos; }
+static inline int Nwk_ObjIsLo( Nwk_Obj_t * p ) { return p->pMan->nTruePis && Nwk_ObjIsCi(p) && (int)p->PioId >= p->pMan->nTruePis; }
static inline float Nwk_ObjArrival( Nwk_Obj_t * pObj ) { return pObj->tArrival; }
static inline float Nwk_ObjRequired( Nwk_Obj_t * pObj ) { return pObj->tRequired; }
@@ -190,10 +197,26 @@ static inline int Nwk_ManTimeMore( float f1, float f2, float Eps ) { r
#define Nwk_ObjForEachFanout( pObj, pFanout, i ) \
for ( i = 0; (i < (int)(pObj)->nFanouts) && ((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]); i++ )
+// sequential iterators
+#define Nwk_ManForEachPiSeq( p, pObj, i ) \
+ Vec_PtrForEachEntryStop( p->vCis, pObj, i, (p)->nTruePis )
+#define Nwk_ManForEachPoSeq( p, pObj, i ) \
+ Vec_PtrForEachEntryStop( p->vCos, pObj, i, (p)->nTruePos )
+#define Nwk_ManForEachLoSeq( p, pObj, i ) \
+ for ( i = 0; (i < (p)->nLatches) && (((pObj) = Vec_PtrEntry(p->vCis, i+(p)->nTruePis)), 1); i++ )
+#define Nwk_ManForEachLiSeq( p, pObj, i ) \
+ for ( i = 0; (i < (p)->nLatches) && (((pObj) = Vec_PtrEntry(p->vCos, i+(p)->nTruePos)), 1); i++ )
+#define Nwk_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) \
+ for ( i = 0; (i < (p)->nLatches) && (((pObjLi) = Nwk_ManCo(p, i+(p)->nTruePos)), 1) \
+ && (((pObjLo) = Nwk_ManCi(p, i+(p)->nTruePis)), 1); i++ )
+
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+/*=== nwkAig.c ==========================================================*/
+extern Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose );
/*=== nwkBidec.c ==========================================================*/
extern void Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose );
extern Hop_Obj_t * Nwk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
@@ -221,6 +244,9 @@ extern void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin
extern void Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew );
extern void Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo );
extern void Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew );
+/*=== nwkFlow.c ============================================================*/
+extern Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
+extern Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
/*=== nwkMan.c ============================================================*/
extern Nwk_Man_t * Nwk_ManAlloc();
extern void Nwk_ManFree( Nwk_Man_t * p );
@@ -258,6 +284,7 @@ extern int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_
extern void Nwk_ObjPrint( Nwk_Obj_t * pObj );
extern void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
extern void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk );
+extern void Nwk_ManCleanMarks( Nwk_Man_t * pNtk );
#ifdef __cplusplus
}
diff --git a/src/aig/nwk/nwkAig.c b/src/aig/nwk/nwkAig.c
new file mode 100644
index 00000000..7421348a
--- /dev/null
+++ b/src/aig/nwk/nwkAig.c
@@ -0,0 +1,107 @@
+/**CFile****************************************************************
+
+ FileName [nwkAig.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Translating of AIG into the network.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: nwkAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Converts AIG into the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Nwk_Man_t * Nwk_ManDeriveFromAig( Aig_Man_t * p )
+{
+ Nwk_Man_t * pNtk;
+ Aig_Obj_t * pObj;
+ int i;
+ pNtk = Nwk_ManAlloc();
+ pNtk->nFanioPlus = 0;
+ Hop_ManStop( pNtk->pManHop );
+ pNtk->pManHop = NULL;
+ pNtk->pName = Aig_UtilStrsav( p->pName );
+ pNtk->pSpec = Aig_UtilStrsav( p->pSpec );
+ pObj = Aig_ManConst1(p);
+ pObj->pData = Nwk_ManCreateNode( pNtk, 0, pObj->nRefs );
+ Aig_ManForEachPi( p, pObj, i )
+ pObj->pData = Nwk_ManCreateCi( pNtk, pObj->nRefs );
+ Aig_ManForEachNode( p, pObj, i )
+ {
+ pObj->pData = Nwk_ManCreateNode( pNtk, 2, pObj->nRefs );
+ Nwk_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData );
+ Nwk_ObjAddFanin( pObj->pData, Aig_ObjFanin1(pObj)->pData );
+ }
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ pObj->pData = Nwk_ManCreateCo( pNtk );
+ Nwk_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData );
+ }
+ return pNtk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts AIG into the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose )
+{
+ Vec_Ptr_t * vNodes;
+ Nwk_Man_t * pNtk;
+ Nwk_Obj_t * pNode;
+ Aig_Obj_t * pObj;
+ int i;
+ pNtk = Nwk_ManDeriveFromAig( p );
+ if ( fForward )
+ vNodes = Nwk_ManRetimeCutForward( pNtk, Aig_ManRegNum(p), fVerbose );
+ else
+ vNodes = Nwk_ManRetimeCutBackward( pNtk, Aig_ManRegNum(p), fVerbose );
+ Aig_ManForEachObj( p, pObj, i )
+ ((Nwk_Obj_t *)pObj->pData)->pCopy = pObj;
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrWriteEntry( vNodes, i, pNode->pCopy );
+ Nwk_ManFree( pNtk );
+ assert( Vec_PtrSize(vNodes) <= Aig_ManRegNum(p) );
+ return vNodes;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/nwk/nwkFlow.c b/src/aig/nwk/nwkFlow.c
new file mode 100644
index 00000000..b245628a
--- /dev/null
+++ b/src/aig/nwk/nwkFlow.c
@@ -0,0 +1,593 @@
+/**CFile****************************************************************
+
+ FileName [nwkFlow.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Max-flow/min-cut computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: nwkFlow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// predecessors
+static inline Nwk_Obj_t * Nwk_ObjPred( Nwk_Obj_t * pObj ) { return pObj->pCopy; }
+static inline int Nwk_ObjSetPred( Nwk_Obj_t * pObj, Nwk_Obj_t * p ) { pObj->pCopy = p; return 1; }
+// sink
+static inline int Nwk_ObjIsSink( Nwk_Obj_t * pObj ) { return pObj->MarkA; }
+static inline void Nwk_ObjSetSink( Nwk_Obj_t * pObj ) { pObj->MarkA = 1; }
+// flow
+static inline int Nwk_ObjHasFlow( Nwk_Obj_t * pObj ) { return pObj->MarkB; }
+static inline void Nwk_ObjSetFlow( Nwk_Obj_t * pObj ) { pObj->MarkB = 1; }
+static inline void Nwk_ObjClearFlow( Nwk_Obj_t * pObj ) { pObj->MarkB = 0; }
+
+// representation of visited nodes
+// pObj->TravId < pNtk->nTravIds-2 --- not visited
+// pObj->TravId == pNtk->nTravIds-2 --- visited bot only
+// pObj->TravId == pNtk->nTravIds-1 --- visited top only
+// pObj->TravId == pNtk->nTravIds --- visited bot and top
+static inline int Nwk_ObjVisitedBotOnly( Nwk_Obj_t * pObj )
+{
+ return pObj->TravId == pObj->pMan->nTravIds - 2;
+}
+static inline int Nwk_ObjVisitedBot( Nwk_Obj_t * pObj )
+{
+ return pObj->TravId == pObj->pMan->nTravIds - 2 || pObj->TravId == pObj->pMan->nTravIds;
+}
+static inline int Nwk_ObjVisitedTop( Nwk_Obj_t * pObj )
+{
+ return pObj->TravId == pObj->pMan->nTravIds - 1 || pObj->TravId == pObj->pMan->nTravIds;
+}
+static inline void Nwk_ObjSetVisitedBot( Nwk_Obj_t * pObj )
+{
+ if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
+ pObj->TravId = pObj->pMan->nTravIds - 2;
+ else if ( pObj->TravId == pObj->pMan->nTravIds - 1 )
+ pObj->TravId = pObj->pMan->nTravIds;
+ else
+ assert( 0 );
+}
+static inline void Nwk_ObjSetVisitedTop( Nwk_Obj_t * pObj )
+{
+ if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
+ pObj->TravId = pObj->pMan->nTravIds - 1;
+ else if ( pObj->TravId == pObj->pMan->nTravIds - 2 )
+ pObj->TravId = pObj->pMan->nTravIds;
+ else
+ assert( 0 );
+}
+static inline Nwk_ManIncrementTravIdFlow( Nwk_Man_t * pMan )
+{
+ Nwk_ManIncrementTravId( pMan );
+ Nwk_ManIncrementTravId( pMan );
+ Nwk_ManIncrementTravId( pMan );
+}
+
+static int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+static int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+
+static int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+static int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Marks TFI of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ManMarkTfiCone_rec( Nwk_Obj_t * pObj )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( pObj->MarkA )
+ return;
+ pObj->MarkA = 1;
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ Nwk_ManMarkTfiCone_rec( pNext );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks TFO of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ManMarkTfoCone_rec( Nwk_Obj_t * pObj )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( pObj->MarkA )
+ return;
+ pObj->MarkA = 1;
+ Nwk_ObjForEachFanout( pObj, pNext, i )
+ Nwk_ManMarkTfoCone_rec( pNext );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Fast forward flow pushing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushForwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+ return 0;
+ Nwk_ObjSetTravIdCurrent( pObj );
+ if ( Nwk_ObjHasFlow(pObj) )
+ return 0;
+ if ( Nwk_ObjIsSink(pObj) )
+ {
+ Nwk_ObjSetFlow(pObj);
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ Nwk_ObjForEachFanout( pObj, pNext, i )
+ if ( Nwk_ManPushForwardFast_rec( pNext, pObj ) )
+ {
+ Nwk_ObjSetFlow(pObj);
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Fast backward flow pushing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushBackwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+ return 0;
+ Nwk_ObjSetTravIdCurrent( pObj );
+ if ( Nwk_ObjHasFlow(pObj) )
+ return 0;
+ if ( Nwk_ObjIsSink(pObj) )
+ {
+ Nwk_ObjSetFlow(pObj);
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ if ( Nwk_ManPushBackwardFast_rec( pNext, pObj ) )
+ {
+ Nwk_ObjSetFlow(pObj);
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Pushing the flow through the bottom part of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( Nwk_ObjVisitedBot(pObj) )
+ return 0;
+ Nwk_ObjSetVisitedBot(pObj);
+ // propagate through the internal edge
+ if ( Nwk_ObjHasFlow(pObj) )
+ {
+ if ( Nwk_ObjPred(pObj) )
+ if ( Nwk_ManPushForwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ else if ( Nwk_ManPushForwardTop_rec(pObj, pObj) )
+ {
+ Nwk_ObjSetFlow( pObj );
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ // try to push through the fanins
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Pushing the flow through the top part of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( Nwk_ObjVisitedTop(pObj) )
+ return 0;
+ Nwk_ObjSetVisitedTop(pObj);
+ // check if this is the sink
+ if ( Nwk_ObjIsSink(pObj) )
+ return 1;
+ // try to push through the fanouts
+ Nwk_ObjForEachFanout( pObj, pNext, i )
+ if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
+ return 1;
+ // redirect the flow
+ if ( Nwk_ObjHasFlow(pObj) && !Nwk_ObjIsCi(pObj) )
+ if ( Nwk_ManPushForwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
+ {
+ Nwk_ObjClearFlow( pObj );
+ return Nwk_ObjSetPred( pObj, NULL );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Pushing the flow through the bottom part of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ if ( Nwk_ObjVisitedBot(pObj) )
+ return 0;
+ Nwk_ObjSetVisitedBot(pObj);
+ // propagate through the internal edge
+ if ( Nwk_ObjHasFlow(pObj) )
+ {
+ if ( Nwk_ObjPred(pObj) )
+ if ( Nwk_ManPushBackwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ else if ( Nwk_ManPushBackwardTop_rec(pObj, pObj) )
+ {
+ Nwk_ObjSetFlow( pObj );
+ return Nwk_ObjSetPred( pObj, pPred );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Pushing the flow through the top part of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( Nwk_ObjVisitedTop(pObj) )
+ return 0;
+ Nwk_ObjSetVisitedTop(pObj);
+ // check if this is the sink
+ if ( Nwk_ObjIsSink(pObj) )
+ return 1;
+ // try to push through the fanins
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ if ( Nwk_ManPushBackwardBot_rec( pNext, pPred ) )
+ return 1;
+ // try to push through the fanouts
+ Nwk_ObjForEachFanout( pObj, pNext, i )
+ if ( !Nwk_ObjIsCo(pObj) && Nwk_ManPushBackwardTop_rec( pNext, pPred ) )
+ return 1;
+ // redirect the flow
+ if ( Nwk_ObjHasFlow(pObj) )
+ if ( Nwk_ObjPred(pObj) && Nwk_ManPushBackwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
+ {
+ Nwk_ObjClearFlow( pObj );
+ return Nwk_ObjSetPred( pObj, NULL );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 0 if there is an unmarked path to a CI.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManVerifyCut_rec( Nwk_Obj_t * pObj )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( pObj->MarkA )
+ return 1;
+ if ( Nwk_ObjIsLo(pObj) )
+ return 0;
+ if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+ return 1;
+ Nwk_ObjSetTravIdCurrent( pObj );
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ if ( !Nwk_ManVerifyCut_rec( pNext ) )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verifies the forward cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManRetimeVerifyCutForward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes )
+{
+ Nwk_Obj_t * pObj;
+ int i;
+ // mark the nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ assert( pObj->MarkA == 0 );
+ pObj->MarkA = 1;
+ }
+ // traverse from the COs
+ Nwk_ManIncrementTravId( pMan );
+ Nwk_ManForEachCo( pMan, pObj, i )
+ if ( !Nwk_ManVerifyCut_rec( pObj ) )
+ printf( "Nwk_ManRetimeVerifyCutForward(): Internal cut verification failed.\n" );
+ // unmark the nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ pObj->MarkA = 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verifies the forward cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManRetimeVerifyCutBackward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes )
+{
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes minimum cut for forward retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
+{
+ Vec_Ptr_t * vNodes;
+ Nwk_Obj_t * pObj;
+ int i, RetValue, Counter = 0, Counter2 = 0;
+ int clk = clock();
+ // set the sequential parameters
+ pMan->nLatches = nLatches;
+ pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
+ pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
+ // mark the COs and the TFO of PIs
+ Nwk_ManForEachCo( pMan, pObj, i )
+ pObj->MarkA = 1;
+ Nwk_ManForEachPiSeq( pMan, pObj, i )
+ Nwk_ManMarkTfoCone_rec( pObj );
+ // start flow computation from each LO
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLoSeq( pMan, pObj, i )
+ {
+ if ( !Nwk_ManPushForwardFast_rec( pObj, NULL ) )
+ continue;
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Counter++;
+ }
+ if ( fVerbose )
+ printf( "Forward: Max-flow1 = %5d. ", Counter );
+ // continue flow computation from each LO
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLoSeq( pMan, pObj, i )
+ {
+ if ( !Nwk_ManPushForwardBot_rec( pObj, NULL ) )
+ continue;
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Counter2++;
+ }
+ if ( fVerbose )
+ printf( "Max-flow2 = %5d. ", Counter+Counter2 );
+ // repeat flow computation from each LO
+ if ( Counter2 > 0 )
+ {
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLoSeq( pMan, pObj, i )
+ {
+ RetValue = Nwk_ManPushForwardBot_rec( pObj, NULL );
+ assert( !RetValue );
+ }
+ }
+ // cut is a set of nodes whose bottom is visited but top is not visited
+ vNodes = Vec_PtrAlloc( Counter+Counter2 );
+ Counter = 0;
+ Nwk_ManForEachObj( pMan, pObj, i )
+ {
+ if ( Nwk_ObjVisitedBotOnly(pObj) )
+ {
+ assert( Nwk_ObjHasFlow(pObj) );
+ assert( !Nwk_ObjIsCo(pObj) );
+ Vec_PtrPush( vNodes, pObj );
+ Counter += Nwk_ObjIsCi(pObj);
+ }
+ }
+ Nwk_ManCleanMarks( pMan );
+ assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) );
+ if ( fVerbose )
+ {
+ printf( "Min-cut = %5d. Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter );
+ PRT( "Time", clock() - clk );
+ }
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes minimum cut for backward retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
+{
+ Vec_Ptr_t * vNodes;
+ Nwk_Obj_t * pObj;
+ int i, RetValue, Counter = 0, Counter2 = 0;
+ int clk = clock();
+ // set the sequential parameters
+ pMan->nLatches = nLatches;
+ pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
+ pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
+ // mark the CIs, the TFI of POs, and the constant nodes
+ Nwk_ManForEachCi( pMan, pObj, i )
+ pObj->MarkA = 1;
+ Nwk_ManForEachPoSeq( pMan, pObj, i )
+ Nwk_ManMarkTfiCone_rec( pObj );
+ Nwk_ManForEachObj( pMan, pObj, i )
+ if ( Nwk_ObjFaninNum(pObj) == 0 )
+ pObj->MarkA = 1;
+ // start flow computation from each LI driver
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLiSeq( pMan, pObj, i )
+ {
+ if ( !Nwk_ManPushBackwardFast_rec( Nwk_ObjFanin0(pObj), NULL ) )
+ continue;
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Counter++;
+ }
+ if ( fVerbose )
+ printf( "Backward: Max-flow1 = %5d. ", Counter );
+ // continue flow computation from each LI driver
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLiSeq( pMan, pObj, i )
+ {
+ if ( !Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL ) )
+ continue;
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Counter2++;
+ }
+ if ( fVerbose )
+ printf( "Max-flow2 = %5d. ", Counter+Counter2 );
+ // repeat flow computation from each LI driver
+ if ( Counter2 > 0 )
+ {
+ Nwk_ManIncrementTravIdFlow( pMan );
+ Nwk_ManForEachLiSeq( pMan, pObj, i )
+ {
+ RetValue = Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL );
+ assert( !RetValue );
+ }
+ }
+ // cut is a set of nodes whose bottom is visited but top is not visited
+ vNodes = Vec_PtrAlloc( Counter+Counter2 );
+ Nwk_ManForEachObj( pMan, pObj, i )
+ {
+ if ( Nwk_ObjVisitedBotOnly(pObj) )
+ {
+ assert( Nwk_ObjHasFlow(pObj) );
+ assert( !Nwk_ObjIsCo(pObj) );
+ Vec_PtrPush( vNodes, pObj );
+ }
+ }
+ // count CO drivers
+ Counter = 0;
+ Nwk_ManForEachLiSeq( pMan, pObj, i )
+ if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) )
+ Counter++;
+ Nwk_ManCleanMarks( pMan );
+ assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) );
+ if ( fVerbose )
+ {
+ printf( "Min-cut = %5d. Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter );
+ PRT( "Time", clock() - clk );
+ }
+ return vNodes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index f30f7251..1ef0af67 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -447,6 +447,24 @@ void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
nFanoutsMax, 1.0*nFanoutsAll/Nwk_ManNodeNum(pNtk) );
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ManCleanMarks( Nwk_Man_t * pMan )
+{
+ Nwk_Obj_t * pObj;
+ int i;
+ Nwk_ManForEachObj( pMan, pObj, i )
+ pObj->MarkA = pObj->MarkB = 0;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/nwk/nwkUtil_old.c b/src/aig/nwk/nwkUtil_old.c
new file mode 100644
index 00000000..c6f5c136
--- /dev/null
+++ b/src/aig/nwk/nwkUtil_old.c
@@ -0,0 +1,615 @@
+/**CFile****************************************************************
+
+ FileName [nwkUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Logic network representation.]
+
+ Synopsis [Various utilities.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: nwkUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+#include "kit.h"
+#include <math.h>
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Increments the current traversal ID of the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk )
+{
+ Nwk_Obj_t * pObj;
+ int i;
+ if ( pNtk->nTravIds >= (1<<26)-1 )
+ {
+ pNtk->nTravIds = 0;
+ Nwk_ManForEachObj( pNtk, pObj, i )
+ pObj->TravId = 0;
+ }
+ pNtk->nTravIds++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the maximum number of fanins.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManGetFaninMax( Nwk_Man_t * pNtk )
+{
+ Nwk_Obj_t * pNode;
+ int i, nFaninsMax = 0;
+ Nwk_ManForEachNode( pNtk, pNode, i )
+ {
+ if ( nFaninsMax < Nwk_ObjFaninNum(pNode) )
+ nFaninsMax = Nwk_ObjFaninNum(pNode);
+ }
+ return nFaninsMax;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the total number of all fanins.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk )
+{
+ Nwk_Obj_t * pNode;
+ int i, nFanins = 0;
+ Nwk_ManForEachNode( pNtk, pNode, i )
+ nFanins += Nwk_ObjFaninNum(pNode);
+ return nFanins;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPiNum( Nwk_Man_t * pNtk )
+{
+ Nwk_Obj_t * pNode;
+ int i, Counter = 0;
+ Nwk_ManForEachCi( pNtk, pNode, i )
+ Counter += Nwk_ObjIsPi( pNode );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPoNum( Nwk_Man_t * pNtk )
+{
+ Nwk_Obj_t * pNode;
+ int i, Counter = 0;
+ Nwk_ManForEachCo( pNtk, pNode, i )
+ Counter += Nwk_ObjIsPo( pNode );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the number of BDD nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk )
+{
+ Nwk_Obj_t * pNode;
+ int i, nNodes = 0;
+ Nwk_ManForEachNode( pNtk, pNode, i )
+ {
+ if ( pNode->pFunc == NULL )
+ {
+ printf( "Nwk_ManGetAigNodeNum(): Local AIG of node %d is not assigned.\n", pNode->Id );
+ continue;
+ }
+ if ( Nwk_ObjFaninNum(pNode) < 2 )
+ continue;
+ nNodes += Hop_DagSize( pNode->pFunc );
+ }
+ return nNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Procedure used for sorting the nodes in increasing order of levels.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 )
+{
+ int Diff = (*pp1)->Level - (*pp2)->Level;
+ if ( Diff < 0 )
+ return -1;
+ if ( Diff > 0 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 )
+{
+ int Diff = (*pp1)->Level - (*pp2)->Level;
+ if ( Diff > 0 )
+ return -1;
+ if ( Diff < 0 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deletes the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ObjPrint( Nwk_Obj_t * pObj )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ printf( "ObjId = %5d. ", pObj->Id );
+ if ( Nwk_ObjIsPi(pObj) )
+ printf( "PI" );
+ if ( Nwk_ObjIsPo(pObj) )
+ printf( "PO" );
+ if ( Nwk_ObjIsNode(pObj) )
+ printf( "Node" );
+ printf( " Fanins = " );
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ printf( "%d ", pNext->Id );
+ printf( " Fanouts = " );
+ Nwk_ObjForEachFanout( pObj, pNext, i )
+ printf( "%d ", pNext->Id );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deletes the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames )
+{
+ FILE * pFile;
+ Vec_Ptr_t * vNodes;
+ Vec_Int_t * vTruth;
+ Vec_Int_t * vCover;
+ Nwk_Obj_t * pObj, * pFanin;
+ Aig_MmFlex_t * pMem;
+ char * pSop = NULL;
+ unsigned * pTruth;
+ int i, k, nDigits, Counter = 0;
+ if ( Nwk_ManPoNum(pNtk) == 0 )
+ {
+ printf( "Nwk_ManDumpBlif(): Network does not have POs.\n" );
+ return;
+ }
+ // collect nodes in the DFS order
+ nDigits = Aig_Base10Log( Nwk_ManObjNumMax(pNtk) );
+ // write the file
+ pFile = fopen( pFileName, "w" );
+ fprintf( pFile, "# BLIF file written by procedure Nwk_ManDumpBlif()\n" );
+// fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
+ fprintf( pFile, ".model %s\n", pNtk->pName );
+ // write PIs
+ fprintf( pFile, ".inputs" );
+ Nwk_ManForEachCi( pNtk, pObj, i )
+ if ( vPiNames )
+ fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, i) );
+ else
+ fprintf( pFile, " n%0*d", nDigits, pObj->Id );
+ fprintf( pFile, "\n" );
+ // write POs
+ fprintf( pFile, ".outputs" );
+ Nwk_ManForEachCo( pNtk, pObj, i )
+ if ( vPoNames )
+ fprintf( pFile, " %s", Vec_PtrEntry(vPoNames, i) );
+ else
+ fprintf( pFile, " n%0*d", nDigits, pObj->Id );
+ fprintf( pFile, "\n" );
+ // write nodes
+ pMem = Aig_MmFlexStart();
+ vTruth = Vec_IntAlloc( 1 << 16 );
+ vCover = Vec_IntAlloc( 1 << 16 );
+ vNodes = Nwk_ManDfs( pNtk );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ if ( !Nwk_ObjIsNode(pObj) )
+ continue;
+ // derive SOP for the AIG
+ pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
+ if ( Hop_IsComplement(pObj->pFunc) )
+ Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) );
+ pSop = Kit_PlaFromTruth( pMem, pTruth, Nwk_ObjFaninNum(pObj), vCover );
+ // write the node
+ fprintf( pFile, ".names" );
+ if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
+ {
+ Nwk_ObjForEachFanin( pObj, pFanin, k )
+ if ( vPiNames && Nwk_ObjIsPi(pFanin) )
+ fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(pFanin)) );
+ else
+ fprintf( pFile, " n%0*d", nDigits, pFanin->Id );
+ }
+ fprintf( pFile, " n%0*d\n", nDigits, pObj->Id );
+ // write the function
+ fprintf( pFile, "%s", pSop );
+ }
+ Vec_IntFree( vCover );
+ Vec_IntFree( vTruth );
+ Vec_PtrFree( vNodes );
+ Aig_MmFlexStop( pMem, 0 );
+ // write POs
+ Nwk_ManForEachCo( pNtk, pObj, i )
+ {
+ fprintf( pFile, ".names" );
+ if ( vPiNames && Nwk_ObjIsPi(Nwk_ObjFanin0(pObj)) )
+ fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(Nwk_ObjFanin0(pObj))) );
+ else
+ fprintf( pFile, " n%0*d", nDigits, Nwk_ObjFanin0(pObj)->Id );
+ if ( vPoNames )
+ fprintf( pFile, " %s\n", Vec_PtrEntry(vPoNames, Nwk_ObjPioNum(pObj)) );
+ else
+ fprintf( pFile, " n%0*d\n", nDigits, pObj->Id );
+ fprintf( pFile, "%d 1\n", !pObj->fInvert );
+ }
+ fprintf( pFile, ".end\n\n" );
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the distribution of fanins/fanouts in the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
+{
+ char Buffer[100];
+ Nwk_Obj_t * pNode;
+ Vec_Int_t * vFanins, * vFanouts;
+ int nFanins, nFanouts, nFaninsMax, nFanoutsMax, nFaninsAll, nFanoutsAll;
+ int i, k, nSizeMax;
+
+ // determine the largest fanin and fanout
+ nFaninsMax = nFanoutsMax = 0;
+ nFaninsAll = nFanoutsAll = 0;
+ Nwk_ManForEachNode( pNtk, pNode, i )
+ {
+ nFanins = Nwk_ObjFaninNum(pNode);
+ nFanouts = Nwk_ObjFanoutNum(pNode);
+ nFaninsAll += nFanins;
+ nFanoutsAll += nFanouts;
+ nFaninsMax = AIG_MAX( nFaninsMax, nFanins );
+ nFanoutsMax = AIG_MAX( nFanoutsMax, nFanouts );
+ }
+
+ // allocate storage for fanin/fanout numbers
+ nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
+ vFanins = Vec_IntStart( nSizeMax );
+ vFanouts = Vec_IntStart( nSizeMax );
+
+ // count the number of fanins and fanouts
+ Nwk_ManForEachNode( pNtk, pNode, i )
+ {
+ nFanins = Nwk_ObjFaninNum(pNode);
+ nFanouts = Nwk_ObjFanoutNum(pNode);
+// nFanouts = Nwk_NodeMffcSize(pNode);
+
+ if ( nFanins < 10 )
+ Vec_IntAddToEntry( vFanins, nFanins, 1 );
+ else if ( nFanins < 100 )
+ Vec_IntAddToEntry( vFanins, 10 + nFanins/10, 1 );
+ else if ( nFanins < 1000 )
+ Vec_IntAddToEntry( vFanins, 20 + nFanins/100, 1 );
+ else if ( nFanins < 10000 )
+ Vec_IntAddToEntry( vFanins, 30 + nFanins/1000, 1 );
+ else if ( nFanins < 100000 )
+ Vec_IntAddToEntry( vFanins, 40 + nFanins/10000, 1 );
+ else if ( nFanins < 1000000 )
+ Vec_IntAddToEntry( vFanins, 50 + nFanins/100000, 1 );
+ else if ( nFanins < 10000000 )
+ Vec_IntAddToEntry( vFanins, 60 + nFanins/1000000, 1 );
+
+ if ( nFanouts < 10 )
+ Vec_IntAddToEntry( vFanouts, nFanouts, 1 );
+ else if ( nFanouts < 100 )
+ Vec_IntAddToEntry( vFanouts, 10 + nFanouts/10, 1 );
+ else if ( nFanouts < 1000 )
+ Vec_IntAddToEntry( vFanouts, 20 + nFanouts/100, 1 );
+ else if ( nFanouts < 10000 )
+ Vec_IntAddToEntry( vFanouts, 30 + nFanouts/1000, 1 );
+ else if ( nFanouts < 100000 )
+ Vec_IntAddToEntry( vFanouts, 40 + nFanouts/10000, 1 );
+ else if ( nFanouts < 1000000 )
+ Vec_IntAddToEntry( vFanouts, 50 + nFanouts/100000, 1 );
+ else if ( nFanouts < 10000000 )
+ Vec_IntAddToEntry( vFanouts, 60 + nFanouts/1000000, 1 );
+ }
+
+ printf( "The distribution of fanins and fanouts in the network:\n" );
+ printf( " Number Nodes with fanin Nodes with fanout\n" );
+ for ( k = 0; k < nSizeMax; k++ )
+ {
+ if ( vFanins->pArray[k] == 0 && vFanouts->pArray[k] == 0 )
+ continue;
+ if ( k < 10 )
+ printf( "%15d : ", k );
+ else
+ {
+ sprintf( Buffer, "%d - %d", (int)pow(10, k/10) * (k%10), (int)pow(10, k/10) * (k%10+1) - 1 );
+ printf( "%15s : ", Buffer );
+ }
+ if ( vFanins->pArray[k] == 0 )
+ printf( " " );
+ else
+ printf( "%12d ", vFanins->pArray[k] );
+ printf( " " );
+ if ( vFanouts->pArray[k] == 0 )
+ printf( " " );
+ else
+ printf( "%12d ", vFanouts->pArray[k] );
+ printf( "\n" );
+ }
+ Vec_IntFree( vFanins );
+ Vec_IntFree( vFanouts );
+
+ printf( "Fanins: Max = %d. Ave = %.2f. Fanouts: Max = %d. Ave = %.2f.\n",
+ nFaninsMax, 1.0*nFaninsAll/Nwk_ManNodeNum(pNtk),
+ nFanoutsMax, 1.0*nFanoutsAll/Nwk_ManNodeNum(pNtk) );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ManCleanMarks( Nwk_Man_t * pMan )
+{
+ Nwk_Obj_t * pObj;
+ int i;
+ Nwk_ManForEachObj( pMan, pObj, i )
+ pObj->MarkA = pObj->MarkB = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ManMarkCone_rec( Nwk_Obj_t * pObj )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( pObj->MarkA )
+ return;
+ pObj->MarkA = 1;
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ Nwk_ManMarkCone_rec( pNext );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the flow can be pushed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManPushFlow_rec( Nwk_Obj_t * pObj )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+ return 0;
+ Nwk_ObjSetTravIdCurrent( pObj );
+ // check the case when there is no flow
+ if ( !pObj->MarkB )
+ {
+ if ( pObj->MarkA )
+ return pObj->MarkB = 1;
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ if ( Nwk_ManPushFlow_rec( pNext ) )
+ return pObj->MarkB = 1;
+ }
+ // check the case when there is no flow or we could not push the flow
+ Nwk_ObjForEachFanout( pObj, pNext, i )
+ if ( Nwk_ManPushFlow_rec( pNext ) )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes min-cut using max-flow.]
+
+ Description [MarkA means the sink. MarkB means the flow is present.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ManComputeCut( Nwk_Man_t * pMan, int nLatches )
+{
+ Vec_Ptr_t * vNodes;
+ Nwk_Obj_t * pObj, * pNext;
+ int i, k, RetValue, Counter = 0;
+ // set the sequential parameters
+ pMan->nLatches = nLatches;
+ pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
+ pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
+ // mark the CIs
+ Nwk_ManForEachCi( pMan, pObj, i )
+ pObj->MarkA = 1;
+ // mark the TFI of the POs
+ Nwk_ManForEachPoSeq( pMan, pObj, i )
+ Nwk_ManMarkCone_rec( pObj );
+ // start flow computation from each LI
+// Nwk_ManIncrementTravId( pMan );
+ Nwk_ManForEachLiSeq( pMan, pObj, i )
+ {
+ Nwk_ManIncrementTravId( pMan );
+ if ( !Nwk_ManPushFlow_rec( pObj ) )
+ continue;
+// Nwk_ManIncrementTravId( pMan );
+ Counter++;
+ }
+ // mark the nodes reachable from the LIs
+ Nwk_ManIncrementTravId( pMan );
+ Nwk_ManForEachLiSeq( pMan, pObj, i )
+ {
+ RetValue = Nwk_ManPushFlow_rec( pObj );
+ assert( RetValue == 0 );
+ }
+ // collect labeled nodes whose all fanins are labeled
+ vNodes = Vec_PtrAlloc( Counter );
+ Nwk_ManForEachObj( pMan, pObj, i )
+ {
+ // skip unlabeled
+ if ( !Nwk_ObjIsTravIdCurrent(pObj) )
+ continue;
+ // visit the fanins
+ Nwk_ObjForEachFanin( pObj, pNext, k )
+ if ( !Nwk_ObjIsTravIdCurrent(pNext) )
+ break;
+ if ( k == Nwk_ObjFaninNum(pObj) )
+ Vec_PtrPush( vNodes, pObj );
+ }
+ // unlabel these nodes
+ Nwk_ManIncrementTravId( pMan );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Nwk_ObjSetTravIdCurrent( pObj );
+ // collect labeled nodes having unlabeled fanouts
+ Vec_PtrClear( vNodes );
+ Nwk_ManForEachObj( pMan, pObj, i )
+ {
+ // skip unreachable nodes
+ if ( !Nwk_ObjIsTravIdPrevious(pObj) )
+ continue;
+ if ( Nwk_ObjIsCo(pObj) )
+ {
+ Vec_PtrPush( vNodes, pObj );
+ continue;
+ }
+ Nwk_ObjForEachFanout( pObj, pNext, k )
+ if ( Nwk_ObjIsTravIdCurrent(pNext) )
+ break;
+ if ( k < Nwk_ObjFanoutNum(pObj) )
+ Vec_PtrPush( vNodes, pObj );
+ }
+
+ // clean the marks
+ Nwk_ManCleanMarks( pMan );
+ printf( "Flow = %5d. Cut = %5d. \n", Counter, Vec_PtrSize(vNodes) );
+ Vec_PtrFree( vNodes );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
new file mode 100644
index 00000000..3902ce70
--- /dev/null
+++ b/src/aig/saig/module.make
@@ -0,0 +1,3 @@
+SRC += src/aig/saig/saig_.c \
+ src/aig/saig/saigPhase.c \
+ src/aig/saig/saigRetMin.c
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
new file mode 100644
index 00000000..92d39ab6
--- /dev/null
+++ b/src/aig/saig/saigRetMin.c
@@ -0,0 +1,262 @@
+/**CFile****************************************************************
+
+ FileName [saigRetMin.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Min-area retiming for the AIG.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigRetMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+extern Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Marks the TFI cone with the current traversal ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ if ( pObj == NULL )
+ return;
+ if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+ return;
+ Aig_ObjSetTravIdCurrent( p, pObj );
+ Saig_ManMarkCone_rec( p, Aig_ObjFanin0(pObj) );
+ Saig_ManMarkCone_rec( p, Aig_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the TFI cones with the current traversal ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManMarkCones( Aig_Man_t * p, Vec_Ptr_t * vNodes )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Aig_ManIncrementTravId( p );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Saig_ManMarkCone_rec( p, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of nodes to get registers after retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )
+{
+ Vec_Ptr_t * vNodes;
+ Aig_Obj_t * pObj, * pFanin;
+ int i, RetValue;
+ Saig_ManMarkCones( p, vCut );
+ vNodes = Vec_PtrAlloc( 1000 );
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ continue;
+ pFanin = Aig_ObjFanin0( pObj );
+ if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )
+ {
+ Vec_PtrPush( vNodes, pFanin );
+ pFanin->fMarkA = 1;
+ }
+ pFanin = Aig_ObjFanin1( pObj );
+ if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )
+ {
+ Vec_PtrPush( vNodes, pFanin );
+ pFanin->fMarkA = 1;
+ }
+ }
+ RetValue = Vec_PtrSize( vNodes );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ pObj->fMarkA = 0;
+ Vec_PtrFree( vNodes );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG while retiming the registers to the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManRetimeDupForward_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
+{
+ if ( pObj->pData )
+ return;
+ assert( Aig_ObjIsNode(pObj) );
+ Saig_ManRetimeDupForward_rec( pNew, Aig_ObjFanin0(pObj) );
+ Saig_ManRetimeDupForward_rec( pNew, Aig_ObjFanin1(pObj) );
+ pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG while retiming the registers to the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i;
+ // mark the cones under the cut
+// assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+ pNew->nRegs = Vec_PtrSize(vCut);
+ pNew->nTruePis = p->nTruePis;
+ pNew->nTruePos = p->nTruePos;
+ // create the true PIs
+ Aig_ManCleanData( p );
+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+ Saig_ManForEachPi( p, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pNew );
+ // create the registers
+ Vec_PtrForEachEntry( vCut, pObj, i )
+ pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), pObj->fPhase );
+ // duplicate the logic above the cut
+ Aig_ManForEachPo( p, pObj, i )
+ Saig_ManRetimeDupForward_rec( pNew, Aig_ObjFanin0(pObj) );
+ // create the true POs
+ Saig_ManForEachPo( p, pObj, i )
+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ // remember value in LI
+ Saig_ManForEachLi( p, pObj, i )
+ pObj->pData = Aig_ObjChild0Copy(pObj);
+ // transfer values from the LIs to the LOs
+ Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+ pObjLo->pData = pObjLi->pData;
+ // erase the data values on the internal nodes of the cut
+ Vec_PtrForEachEntry( vCut, pObj, i )
+ if ( !Aig_ObjIsPi(pObj) )
+ pObj->pData = NULL;
+ // duplicate the logic below the cut
+ Vec_PtrForEachEntry( vCut, pObj, i )
+ {
+ Saig_ManRetimeDupForward_rec( pNew, pObj );
+ Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, pObj->fPhase) );
+ }
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG while retiming the registers to the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCut )
+{
+ Aig_Man_t * pNew;
+ pNew = Aig_ManDup( p );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs min-area retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fVerbose )
+{
+ Vec_Ptr_t * vCut;
+ Aig_Man_t * pNew, * pTemp;
+ pNew = Aig_ManDup( p );
+ // perform several iterations of forward retiming
+ if ( !fBackwardOnly )
+ while ( 1 )
+ {
+ vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
+ if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
+ {
+ Vec_PtrFree( vCut );
+ break;
+ }
+ pNew = Saig_ManRetimeDupForward( pTemp = pNew, vCut );
+ Aig_ManStop( pTemp );
+ Vec_PtrFree( vCut );
+ }
+ // perform one iteration of backward retiming
+ if ( !fForwardOnly )
+ {
+ vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
+ if ( Vec_PtrSize(vCut) < Aig_ManRegNum(pNew) )
+ {
+ pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut );
+ Aig_ManStop( pTemp );
+ }
+ Vec_PtrFree( vCut );
+ }
+ return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 09:38:52 +0000