summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/dar/dar.h38
-rw-r--r--src/aig/dar/darCheck.c13
-rw-r--r--src/aig/dar/darCore.c4
-rw-r--r--src/aig/dar/darDfs.c55
-rw-r--r--src/aig/dar/darMan.c26
-rw-r--r--src/aig/dar/darObj.c55
-rw-r--r--src/aig/dar/darOper.c64
-rw-r--r--src/aig/dar/darSeq.c471
-rw-r--r--src/aig/dar/darTable.c29
-rw-r--r--src/base/abc/abcDfs.c3
-rw-r--r--src/base/abc/abcNtk.c2
-rw-r--r--src/base/abci/abc.c56
-rw-r--r--src/base/abci/abcDar.c209
-rw-r--r--src/base/abci/abcFraig.c4
-rw-r--r--src/base/abci/abcPart.c55
-rw-r--r--src/base/io/ioReadAiger.c13
-rw-r--r--src/base/io/ioReadBench.c8
-rw-r--r--src/base/io/ioWriteVerilog.c10
-rw-r--r--src/base/io/ioWriteVerilog.zipbin0 -> 3662 bytes
-rw-r--r--src/base/ver/ver.h1
-rw-r--r--src/base/ver/verCore.c173
-rw-r--r--src/base/ver/verCore.zipbin14163 -> 14624 bytes
-rw-r--r--src/map/if/ifUtil.c20
23 files changed, 1099 insertions, 210 deletions
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 7c77bea5..9bb79262 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -65,7 +65,8 @@ typedef enum {
DAR_AIG_BUF, // 4: buffer node
DAR_AIG_AND, // 5: AND node
DAR_AIG_EXOR, // 6: EXOR node
- DAR_AIG_VOID // 7: unused object
+ DAR_AIG_LATCH, // 7: latch
+ DAR_AIG_VOID // 8: unused object
} Dar_Type_t;
// the parameters
@@ -179,11 +180,13 @@ static inline Dar_Obj_t * Dar_ManObj( Dar_Man_t * p, int i ) { return p->vO
static inline int Dar_ManPiNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_PI]; }
static inline int Dar_ManPoNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_PO]; }
+static inline int Dar_ManBufNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_BUF]; }
static inline int Dar_ManAndNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]; }
static inline int Dar_ManExorNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_EXOR]; }
-static inline int Dar_ManNodeNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+p->nObjs[DAR_AIG_EXOR];}
+static inline int Dar_ManLatchNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_LATCH]; }
+static inline int Dar_ManNodeNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+p->nObjs[DAR_AIG_EXOR]; }
static inline int Dar_ManGetCost( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+3*p->nObjs[DAR_AIG_EXOR]; }
-static inline int Dar_ManObjNum( Dar_Man_t * p ) { return p->nCreated - p->nDeleted; }
+static inline int Dar_ManObjNum( Dar_Man_t * p ) { return p->nCreated - p->nDeleted; }
static inline Dar_Type_t Dar_ObjType( Dar_Obj_t * pObj ) { return (Dar_Type_t)pObj->Type; }
static inline int Dar_ObjIsNone( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_NONE; }
@@ -193,19 +196,20 @@ static inline int Dar_ObjIsPo( Dar_Obj_t * pObj ) { return pObj-
static inline int Dar_ObjIsBuf( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_BUF; }
static inline int Dar_ObjIsAnd( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND; }
static inline int Dar_ObjIsExor( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_EXOR; }
+static inline int Dar_ObjIsLatch( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_LATCH; }
static inline int Dar_ObjIsNode( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR; }
-static inline int Dar_ObjIsTerm( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_PI || pObj->Type == DAR_AIG_PO || pObj->Type == DAR_AIG_CONST1; }
-static inline int Dar_ObjIsHash( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR; }
+static inline int Dar_ObjIsTerm( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_PI || pObj->Type == DAR_AIG_PO || pObj->Type == DAR_AIG_CONST1; }
+static inline int Dar_ObjIsHash( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR || pObj->Type == DAR_AIG_LATCH; }
static inline int Dar_ObjIsMarkA( Dar_Obj_t * pObj ) { return pObj->fMarkA; }
static inline void Dar_ObjSetMarkA( Dar_Obj_t * pObj ) { pObj->fMarkA = 1; }
static inline void Dar_ObjClearMarkA( Dar_Obj_t * pObj ) { pObj->fMarkA = 0; }
-static inline void Dar_ObjSetTravId( Dar_Obj_t * pObj, int TravId ) { pObj->pData = (void *)TravId; }
-static inline void Dar_ObjSetTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->pData = (void *)p->nTravIds; }
-static inline void Dar_ObjSetTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->pData = (void *)(p->nTravIds - 1); }
-static inline int Dar_ObjIsTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int )((int)pObj->pData == p->nTravIds); }
-static inline int Dar_ObjIsTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int )((int)pObj->pData == p->nTravIds - 1); }
+static inline void Dar_ObjSetTravId( Dar_Obj_t * pObj, int TravId ) { pObj->TravId = TravId; }
+static inline void Dar_ObjSetTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->TravId = p->nTravIds; }
+static inline void Dar_ObjSetTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1; }
+static inline int Dar_ObjIsTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int)(pObj->TravId == p->nTravIds); }
+static inline int Dar_ObjIsTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int)(pObj->TravId == p->nTravIds - 1); }
static inline int Dar_ObjTravId( Dar_Obj_t * pObj ) { return (int)pObj->pData; }
static inline int Dar_ObjPhase( Dar_Obj_t * pObj ) { return pObj->fPhase; }
@@ -247,7 +251,7 @@ static inline Dar_Obj_t * Dar_ObjCreateGhost( Dar_Man_t * p, Dar_Obj_t * p0, Da
assert( Type == DAR_AIG_PI || Dar_Regular(p0) != Dar_Regular(p1) );
pGhost = Dar_ManGhost(p);
pGhost->Type = Type;
- if ( Dar_Regular(p0)->Id < Dar_Regular(p1)->Id )
+ if ( p1 == NULL || Dar_Regular(p0)->Id < Dar_Regular(p1)->Id )
{
pGhost->pFanin0 = p0;
pGhost->pFanin1 = p1;
@@ -274,7 +278,8 @@ static inline Dar_Obj_t * Dar_ManFetchMemory( Dar_Man_t * p )
static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry )
{
extern void Dar_MmFixedEntryRecycle( Dar_MmFixed_t * p, char * pEntry );
- pEntry->Type = DAR_AIG_NONE; // distinquishes dead node from live node
+ p->nDeleted++;
+ pEntry->Type = DAR_AIG_NONE; // distinquishes a dead node from a live node
Dar_MmFixedEntryRecycle( p->pMemObjs, (char *)pEntry );
}
@@ -291,7 +296,7 @@ static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry )
Vec_PtrForEachEntry( p->vPos, pObj, i )
// iterator over all objects, including those currently not used
#define Dar_ManForEachObj( p, pObj, i ) \
- Vec_PtrForEachEntry( p->vObjs, pObj, i )
+ Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
@@ -313,7 +318,6 @@ extern Vec_Int_t * Dar_LibReadNodes();
extern Vec_Int_t * Dar_LibReadOuts();
/*=== darDfs.c ==========================================================*/
extern Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p );
-extern Vec_Ptr_t * Dar_ManDfsNode( Dar_Man_t * p, Dar_Obj_t * pNode );
extern int Dar_ManCountLevels( Dar_Man_t * p );
extern void Dar_ManCreateRefs( Dar_Man_t * p );
extern int Dar_DagSize( Dar_Obj_t * pObj );
@@ -342,11 +346,13 @@ extern void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_
extern void Dar_ObjDisconnect( Dar_Man_t * p, Dar_Obj_t * pObj );
extern void Dar_ObjDelete( Dar_Man_t * p, Dar_Obj_t * pObj );
extern void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop );
-extern void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew );
+extern void Dar_ObjPatchFanin0( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFaninNew );
+extern void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew, int fNodesOnly );
/*=== darOper.c =========================================================*/
extern Dar_Obj_t * Dar_IthVar( Dar_Man_t * p, int i );
extern Dar_Obj_t * Dar_Oper( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t Type );
extern Dar_Obj_t * Dar_And( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 );
+extern Dar_Obj_t * Dar_Latch( Dar_Man_t * p, Dar_Obj_t * pObj, int fInitOne );
extern Dar_Obj_t * Dar_Or( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 );
extern Dar_Obj_t * Dar_Exor( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 );
extern Dar_Obj_t * Dar_Mux( Dar_Man_t * p, Dar_Obj_t * pC, Dar_Obj_t * p1, Dar_Obj_t * p0 );
@@ -355,6 +361,8 @@ extern Dar_Obj_t * Dar_Miter( Dar_Man_t * p, Vec_Ptr_t * vPairs );
extern Dar_Obj_t * Dar_CreateAnd( Dar_Man_t * p, int nVars );
extern Dar_Obj_t * Dar_CreateOr( Dar_Man_t * p, int nVars );
extern Dar_Obj_t * Dar_CreateExor( Dar_Man_t * p, int nVars );
+/*=== darSeq.c ========================================================*/
+extern int Dar_ManSeqStrash( Dar_Man_t * p, int nLatches, int * pInits );
/*=== darTable.c ========================================================*/
extern Dar_Obj_t * Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost );
extern void Dar_TableInsert( Dar_Man_t * p, Dar_Obj_t * pObj );
diff --git a/src/aig/dar/darCheck.c b/src/aig/dar/darCheck.c
index 6cfba787..5c7a2390 100644
--- a/src/aig/dar/darCheck.c
+++ b/src/aig/dar/darCheck.c
@@ -89,15 +89,24 @@ int Dar_ManCheck( Dar_Man_t * p )
}
}
// count the total number of nodes
- if ( Dar_ManObjNum(p) != 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) )
+ if ( Dar_ManObjNum(p) != 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManBufNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) )
{
printf( "Dar_ManCheck: The number of created nodes is wrong.\n" );
+ printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n",
+ 1, Dar_ManPiNum(p), Dar_ManPoNum(p), Dar_ManBufNum(p), Dar_ManAndNum(p), Dar_ManExorNum(p), Dar_ManLatchNum(p),
+ 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManBufNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) );
+ printf( "Created = %d. Deleted = %d. Existing = %d.\n",
+ p->nCreated, p->nDeleted, p->nCreated - p->nDeleted );
return 0;
}
// count the number of nodes in the table
- if ( Dar_TableCountEntries(p) != Dar_ManAndNum(p) + Dar_ManExorNum(p) )
+ if ( Dar_TableCountEntries(p) != Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) )
{
printf( "Dar_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
+ printf( "Entries = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n",
+ Dar_TableCountEntries(p), Dar_ManAndNum(p), Dar_ManExorNum(p), Dar_ManLatchNum(p),
+ Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) );
+
return 0;
}
// if ( !Dar_ManIsAcyclic(p) )
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index 9f0f58f6..d56cca45 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -76,7 +76,7 @@ int Dar_ManRewrite( Dar_Man_t * p )
pObjNew = Dar_LibBuildBest( p );
pObjNew = Dar_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
// remove the old nodes
- Dar_ObjReplace( p, pObj, pObjNew );
+ Dar_ObjReplace( p, pObj, pObjNew, 1 );
// compare the gains
nNodeAfter = Dar_ManNodeNum( p );
assert( p->GainBest == nNodeBefore - nNodeAfter );
@@ -99,6 +99,8 @@ int Dar_ManRewrite( Dar_Man_t * p )
return 1;
}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/dar/darDfs.c b/src/aig/dar/darDfs.c
index 1c2ab057..bdb23c9d 100644
--- a/src/aig/dar/darDfs.c
+++ b/src/aig/dar/darDfs.c
@@ -39,15 +39,18 @@
SeeAlso []
***********************************************************************/
-void Dar_ManDfs_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vNodes )
+void Dar_ManDfs_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
assert( !Dar_IsComplement(pObj) );
- if ( !Dar_ObjIsNode(pObj) || Dar_ObjIsMarkA(pObj) )
+ if ( pObj == NULL )
return;
- Dar_ManDfs_rec( Dar_ObjFanin0(pObj), vNodes );
- Dar_ManDfs_rec( Dar_ObjFanin1(pObj), vNodes );
- assert( !Dar_ObjIsMarkA(pObj) ); // loop detection
- Dar_ObjSetMarkA(pObj);
+ if ( Dar_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ assert( Dar_ObjIsNode(pObj) || Dar_ObjIsBuf(pObj) );
+ Dar_ManDfs_rec( p, Dar_ObjFanin0(pObj), vNodes );
+ Dar_ManDfs_rec( p, Dar_ObjFanin1(pObj), vNodes );
+ assert( !Dar_ObjIsTravIdCurrent(p, pObj) ); // loop detection
+ Dar_ObjSetTravIdCurrent(p, pObj);
Vec_PtrPush( vNodes, pObj );
}
@@ -67,35 +70,21 @@ Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p )
Vec_Ptr_t * vNodes;
Dar_Obj_t * pObj;
int i;
+ Dar_ManIncrementTravId( p );
+ // mark constant and PIs
+ Dar_ObjSetTravIdCurrent( p, Dar_ManConst1(p) );
+ Dar_ManForEachPi( p, pObj, i )
+ Dar_ObjSetTravIdCurrent( p, pObj );
+ // if there are latches, mark them
+ if ( Dar_ManLatchNum(p) > 0 )
+ Dar_ManForEachObj( p, pObj, i )
+ if ( Dar_ObjIsLatch(pObj) )
+ Dar_ObjSetTravIdCurrent( p, pObj );
+ // go through the nodes
vNodes = Vec_PtrAlloc( Dar_ManNodeNum(p) );
Dar_ManForEachObj( p, pObj, i )
- Dar_ManDfs_rec( pObj, vNodes );
- Dar_ManForEachObj( p, pObj, i )
- Dar_ObjClearMarkA(pObj);
- return vNodes;
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects internal nodes in the DFS order.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Ptr_t * Dar_ManDfsNode( Dar_Man_t * p, Dar_Obj_t * pNode )
-{
- Vec_Ptr_t * vNodes;
- Dar_Obj_t * pObj;
- int i;
- assert( !Dar_IsComplement(pNode) );
- vNodes = Vec_PtrAlloc( 16 );
- Dar_ManDfs_rec( pNode, vNodes );
- Vec_PtrForEachEntry( vNodes, pObj, i )
- Dar_ObjClearMarkA(pObj);
+ if ( Dar_ObjIsNode(pObj) || Dar_ObjIsBuf(pObj) )
+ Dar_ManDfs_rec( p, pObj, vNodes );
return vNodes;
}
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index bbac1360..1b40bb39 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -55,6 +55,7 @@ Dar_Man_t * Dar_ManStart( int nNodesMax )
// allocate arrays for nodes
p->vPis = Vec_PtrAlloc( 100 );
p->vPos = Vec_PtrAlloc( 100 );
+ p->vObjs = Vec_PtrAlloc( 1000 );
// prepare the internal memory manager
p->pMemObjs = Dar_MmFixedStart( sizeof(Dar_Obj_t), nNodesMax );
p->pMemCuts = Dar_MmFlexStart();
@@ -66,7 +67,7 @@ Dar_Man_t * Dar_ManStart( int nNodesMax )
p->pConst1 = Dar_ManFetchMemory( p );
p->pConst1->Type = DAR_AIG_CONST1;
p->pConst1->fPhase = 1;
- p->nCreated = 1;
+ p->nObjs[DAR_AIG_CONST1]++;
// start the table
p->nTableSize = nNodesMax;
p->pTable = ALLOC( Dar_Obj_t *, p->nTableSize );
@@ -100,10 +101,10 @@ void Dar_ManStop( Dar_Man_t * p )
// Dar_TableProfile( p );
Dar_MmFixedStop( p->pMemObjs, 0 );
Dar_MmFlexStop( p->pMemCuts, 0 );
- if ( p->vPis ) Vec_PtrFree( p->vPis );
- if ( p->vPos ) Vec_PtrFree( p->vPos );
- if ( p->vObjs ) Vec_PtrFree( p->vObjs );
- if ( p->vRequired ) Vec_IntFree( p->vRequired );
+ if ( p->vPis ) Vec_PtrFree( p->vPis );
+ if ( p->vPos ) Vec_PtrFree( p->vPos );
+ if ( p->vObjs ) Vec_PtrFree( p->vObjs );
+ if ( p->vRequired ) Vec_IntFree( p->vRequired );
if ( p->vLeavesBest ) Vec_PtrFree( p->vLeavesBest );
free( p->pTable );
free( p );
@@ -151,12 +152,15 @@ int Dar_ManCleanup( Dar_Man_t * p )
***********************************************************************/
void Dar_ManPrintStats( Dar_Man_t * p )
{
- printf( "PI/PO = %d/%d. ", Dar_ManPiNum(p), Dar_ManPoNum(p) );
- printf( "A = %7d. ", Dar_ManAndNum(p) );
- printf( "X = %5d. ", Dar_ManExorNum(p) );
- printf( "Cre = %7d. ", p->nCreated );
- printf( "Del = %7d. ", p->nDeleted );
- printf( "Lev = %3d. ", Dar_ManCountLevels(p) );
+ printf( "PI/PO/Lat = %5d/%5d/%5d ", Dar_ManPiNum(p), Dar_ManPoNum(p), Dar_ManLatchNum(p) );
+ printf( "A = %6d. ", Dar_ManAndNum(p) );
+ if ( Dar_ManExorNum(p) )
+ printf( "X = %5d. ", Dar_ManExorNum(p) );
+ if ( Dar_ManBufNum(p) )
+ printf( "B = %3d. ", Dar_ManBufNum(p) );
+ printf( "Cre = %6d. ", p->nCreated );
+ printf( "Del = %6d. ", p->nDeleted );
+// printf( "Lev = %3d. ", Dar_ManCountLevels(p) );
printf( "\n" );
}
diff --git a/src/aig/dar/darObj.c b/src/aig/dar/darObj.c
index faf9336e..2db13c71 100644
--- a/src/aig/dar/darObj.c
+++ b/src/aig/dar/darObj.c
@@ -89,7 +89,7 @@ Dar_Obj_t * Dar_ObjCreate( Dar_Man_t * p, Dar_Obj_t * pGhost )
{
Dar_Obj_t * pObj;
assert( !Dar_IsComplement(pGhost) );
- assert( Dar_ObjIsNode(pGhost) );
+ assert( Dar_ObjIsHash(pGhost) );
assert( pGhost == &p->Ghost );
// get memory for the new object
pObj = Dar_ManFetchMemory( p );
@@ -116,7 +116,7 @@ Dar_Obj_t * Dar_ObjCreate( Dar_Man_t * p, Dar_Obj_t * pGhost )
void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFan0, Dar_Obj_t * pFan1 )
{
assert( !Dar_IsComplement(pObj) );
- assert( Dar_ObjIsNode(pObj) );
+ assert( !Dar_ObjIsPi(pObj) );
// add the first fanin
pObj->pFanin0 = pFan0;
pObj->pFanin1 = pFan1;
@@ -137,7 +137,7 @@ void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFan0, Dar_Obj
pObj->fPhase = Dar_ObjFaninPhase(pFan0);
}
// add the node to the structural hash table
- if ( Dar_ObjIsNode(pObj) )
+ if ( Dar_ObjIsHash(pObj) )
Dar_TableInsert( p, pObj );
}
@@ -161,7 +161,7 @@ void Dar_ObjDisconnect( Dar_Man_t * p, Dar_Obj_t * pObj )
if ( pObj->pFanin1 != NULL )
Dar_ObjDeref(Dar_ObjFanin1(pObj));
// remove the node from the structural hash table
- if ( Dar_ObjIsNode(pObj) )
+ if ( Dar_ObjIsHash(pObj) )
Dar_TableDelete( p, pObj );
// add the first fanin
pObj->pFanin0 = NULL;
@@ -184,7 +184,7 @@ void Dar_ObjDelete( Dar_Man_t * p, Dar_Obj_t * pObj )
assert( !Dar_IsComplement(pObj) );
assert( !Dar_ObjIsTerm(pObj) );
assert( Dar_ObjRefs(pObj) == 0 );
- p->nDeleted++;
+ p->nObjs[pObj->Type]--;
Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
Dar_ManRecycleMemory( p, pObj );
}
@@ -206,11 +206,10 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop )
assert( !Dar_IsComplement(pObj) );
if ( Dar_ObjIsConst1(pObj) || Dar_ObjIsPi(pObj) )
return;
- assert( Dar_ObjIsNode(pObj) );
+ assert( !Dar_ObjIsPo(pObj) );
pFanin0 = Dar_ObjFanin0(pObj);
pFanin1 = Dar_ObjFanin1(pObj);
Dar_ObjDisconnect( p, pObj );
- p->nObjs[pObj->Type]--;
if ( fFreeTop )
Dar_ObjDelete( p, pObj );
if ( pFanin0 && !Dar_ObjIsNone(pFanin0) && Dar_ObjRefs(pFanin0) == 0 )
@@ -221,6 +220,33 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop )
/**Function*************************************************************
+ Synopsis [Replaces the first fanin of the node by the new fanin.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_ObjPatchFanin0( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFaninNew )
+{
+ Dar_Obj_t * pFaninOld;
+ assert( !Dar_IsComplement(pObj) );
+ pFaninOld = Dar_ObjFanin0(pObj);
+ // decrement ref and remove fanout
+ Dar_ObjDeref( pFaninOld );
+ // update the fanin
+ pObj->pFanin0 = pFaninNew;
+ // increment ref and add fanout
+ Dar_ObjRef( Dar_Regular(pFaninNew) );
+ // get rid of old fanin
+ if ( !Dar_ObjIsPi(pFaninOld) && !Dar_ObjIsConst1(pFaninOld) && Dar_ObjRefs(pFaninOld) == 0 )
+ Dar_ObjDelete_rec( p, pFaninOld, 1 );
+}
+
+/**Function*************************************************************
+
Synopsis [Replaces one object by another.]
Description [Both objects are currently in the manager. The new object
@@ -232,27 +258,27 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop )
SeeAlso []
***********************************************************************/
-void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew )
+void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew, int fNodesOnly )
{
Dar_Obj_t * pObjNewR = Dar_Regular(pObjNew);
// the object to be replaced cannot be complemented
assert( !Dar_IsComplement(pObjOld) );
// the object to be replaced cannot be a terminal
assert( !Dar_ObjIsPi(pObjOld) && !Dar_ObjIsPo(pObjOld) );
- // the object to be used cannot be a buffer
+ // the object to be used cannot be a buffer or a PO
assert( !Dar_ObjIsBuf(pObjNewR) && !Dar_ObjIsPo(pObjNewR) );
// the object cannot be the same
assert( pObjOld != pObjNewR );
// make sure object is not pointing to itself
- assert( pObjOld != Dar_ObjFanin0(pObjNewR) );
+// assert( pObjOld != Dar_ObjFanin0(pObjNewR) );
assert( pObjOld != Dar_ObjFanin1(pObjNewR) );
- // delete the old node
+ // recursively delete the old node - but leave the object there
Dar_ObjDelete_rec( p, pObjOld, 0 );
// if the new object is complemented or already used, create a buffer
- if ( Dar_IsComplement(pObjNew) || Dar_ObjRefs(pObjNew) > 0 || !Dar_ObjIsNode(pObjNew) )
+ p->nObjs[pObjOld->Type]--;
+ if ( Dar_IsComplement(pObjNew) || Dar_ObjRefs(pObjNew) > 0 || (fNodesOnly && !Dar_ObjIsNode(pObjNew)) )
{
pObjOld->Type = DAR_AIG_BUF;
- p->nObjs[pObjOld->Type]++;
Dar_ObjConnect( p, pObjOld, pObjNew, NULL );
}
else
@@ -261,9 +287,10 @@ void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew )
Dar_Obj_t * pFanin1 = pObjNew->pFanin1;
pObjOld->Type = pObjNew->Type;
Dar_ObjDisconnect( p, pObjNew );
- Dar_ObjDelete( p, pObjNew );
Dar_ObjConnect( p, pObjOld, pFanin0, pFanin1 );
+ Dar_ObjDelete( p, pObjNew );
}
+ p->nObjs[pObjOld->Type]++;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/dar/darOper.c b/src/aig/dar/darOper.c
index 8921fe33..cfb89e31 100644
--- a/src/aig/dar/darOper.c
+++ b/src/aig/dar/darOper.c
@@ -89,6 +89,43 @@ Dar_Obj_t * Dar_Oper( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t
/**Function*************************************************************
+ Synopsis [Creates the canonical form of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dar_Obj_t * Dar_CanonPair_rec( Dar_Man_t * p, Dar_Obj_t * pGhost )
+{
+ Dar_Obj_t * pResult, * pLat0, * pLat1;
+ int fCompl0, fCompl1;
+ Dar_Type_t Type;
+ assert( Dar_ObjIsNode(pGhost) );
+ // consider the case when the pair is canonical
+ if ( !Dar_ObjIsLatch(Dar_ObjFanin0(pGhost)) || !Dar_ObjIsLatch(Dar_ObjFanin1(pGhost)) )
+ {
+ if ( pResult = Dar_TableLookup( p, pGhost ) )
+ return pResult;
+ return Dar_ObjCreate( p, pGhost );
+ }
+ /// remember the latches
+ pLat0 = Dar_ObjFanin0(pGhost);
+ pLat1 = Dar_ObjFanin1(pGhost);
+ // remember type and compls
+ Type = Dar_ObjType(pGhost);
+ fCompl0 = Dar_ObjFaninC0(pGhost);
+ fCompl1 = Dar_ObjFaninC1(pGhost);
+ // call recursively
+ pResult = Dar_Oper( p, Dar_NotCond(Dar_ObjChild0(pLat0), fCompl0), Dar_NotCond(Dar_ObjChild0(pLat1), fCompl1), Type );
+ // build latch on top of this
+ return Dar_Latch( p, pResult, (Type == DAR_AIG_AND)? fCompl0 & fCompl1 : fCompl0 ^ fCompl1 );
+}
+
+/**Function*************************************************************
+
Synopsis [Performs canonicization step.]
Description [The argument nodes can be complemented.]
@@ -114,11 +151,30 @@ Dar_Obj_t * Dar_And( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 )
// check if it can be an EXOR gate
// if ( Dar_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
// return Dar_Exor( p, pFan0, pFan1 );
- // check the table
pGhost = Dar_ObjCreateGhost( p, p0, p1, DAR_AIG_AND );
- if ( pResult = Dar_TableLookup( p, pGhost ) )
- return pResult;
- return Dar_ObjCreate( p, pGhost );
+ pResult = Dar_CanonPair_rec( p, pGhost );
+ return pResult;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the canonical form of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dar_Obj_t * Dar_Latch( Dar_Man_t * p, Dar_Obj_t * pObj, int fInitOne )
+{
+ Dar_Obj_t * pGhost, * pResult;
+ pGhost = Dar_ObjCreateGhost( p, Dar_NotCond(pObj, fInitOne), NULL, DAR_AIG_LATCH );
+ pResult = Dar_TableLookup( p, pGhost );
+ if ( pResult == NULL )
+ pResult = Dar_ObjCreate( p, pGhost );
+ return Dar_NotCond( pResult, fInitOne );
}
/**Function*************************************************************
diff --git a/src/aig/dar/darSeq.c b/src/aig/dar/darSeq.c
new file mode 100644
index 00000000..bf3807f4
--- /dev/null
+++ b/src/aig/dar/darSeq.c
@@ -0,0 +1,471 @@
+/**CFile****************************************************************
+
+ FileName [darSeq.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: darSeq.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Converts combinational AIG manager into a sequential one.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_ManSeqStrashConvert( Dar_Man_t * p, int nLatches, int * pInits )
+{
+ Dar_Obj_t * pObjLi, * pObjLo, * pLatch;
+ int i;
+ // collect the POs to be converted into latches
+ for ( i = 0; i < nLatches; i++ )
+ {
+ // get the corresponding PI/PO pair
+ pObjLi = Dar_ManPo( p, Dar_ManPoNum(p) - nLatches + i );
+ pObjLo = Dar_ManPi( p, Dar_ManPiNum(p) - nLatches + i );
+ // create latch
+ pLatch = Dar_Latch( p, Dar_ObjChild0(pObjLi), pInits? pInits[i] : 0 );
+ // recycle the old PO object
+ Dar_ObjDisconnect( p, pObjLi );
+ Vec_PtrWriteEntry( p->vObjs, pObjLi->Id, NULL );
+ Dar_ManRecycleMemory( p, pObjLi );
+ // convert the corresponding PI to be a buffer and connect it to the latch
+ pObjLo->Type = DAR_AIG_BUF;
+ Dar_ObjConnect( p, pObjLo, pLatch, NULL );
+ }
+ // shrink the arrays
+ Vec_PtrShrink( p->vPis, Dar_ManPiNum(p) - nLatches );
+ Vec_PtrShrink( p->vPos, Dar_ManPoNum(p) - nLatches );
+ // update the counters of different objects
+ p->nObjs[DAR_AIG_PI] -= nLatches;
+ p->nObjs[DAR_AIG_PO] -= nLatches;
+ p->nObjs[DAR_AIG_BUF] += nLatches;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects internal nodes in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_ManDfsSeq_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+ assert( !Dar_IsComplement(pObj) );
+ if ( pObj == NULL )
+ return;
+ if ( Dar_ObjIsTravIdCurrent( p, pObj ) )
+ return;
+ Dar_ObjSetTravIdCurrent( p, pObj );
+ if ( Dar_ObjIsPi(pObj) )
+ return;
+ Dar_ManDfsSeq_rec( p, Dar_ObjFanin0(pObj), vNodes );
+ Dar_ManDfsSeq_rec( p, Dar_ObjFanin1(pObj), vNodes );
+ Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects internal nodes in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Dar_ManDfsSeq( Dar_Man_t * p )
+{
+ Vec_Ptr_t * vNodes;
+ Dar_Obj_t * pObj;
+ int i;
+ Dar_ManIncrementTravId( p );
+ vNodes = Vec_PtrAlloc( Dar_ManNodeNum(p) );
+ Dar_ManForEachPo( p, pObj, i )
+ Dar_ManDfsSeq_rec( p, Dar_ObjFanin0(pObj), vNodes );
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects internal nodes in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_ManDfsUnreach_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+ assert( !Dar_IsComplement(pObj) );
+ if ( pObj == NULL )
+ return;
+ if ( Dar_ObjIsTravIdPrevious(p, pObj) || Dar_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Dar_ObjSetTravIdPrevious( p, pObj ); // assume unknown
+ Dar_ManDfsUnreach_rec( p, Dar_ObjFanin0(pObj), vNodes );
+ Dar_ManDfsUnreach_rec( p, Dar_ObjFanin1(pObj), vNodes );
+ if ( Dar_ObjIsTravIdPrevious(p, Dar_ObjFanin0(pObj)) &&
+ (Dar_ObjFanin1(pObj) == NULL || Dar_ObjIsTravIdPrevious(p, Dar_ObjFanin1(pObj))) )
+ Vec_PtrPush( vNodes, pObj );
+ else
+ Dar_ObjSetTravIdCurrent( p, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects internal nodes unreachable from PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Dar_ManDfsUnreach( Dar_Man_t * p )
+{
+ Vec_Ptr_t * vNodes;
+ Dar_Obj_t * pObj, * pFanin;
+ int i, k;//, RetValue;
+ // collect unreachable nodes
+ Dar_ManIncrementTravId( p );
+ Dar_ManIncrementTravId( p );
+ // mark the constant and PIs
+ Dar_ObjSetTravIdPrevious( p, Dar_ManConst1(p) );
+ Dar_ManForEachPi( p, pObj, i )
+ Dar_ObjSetTravIdCurrent( p, pObj );
+ // curr marks visited nodes reachable from PIs
+ // prev marks visited nodes unreachable or unknown
+
+ // collect the unreachable nodes
+ vNodes = Vec_PtrAlloc( 32 );
+ Dar_ManForEachPo( p, pObj, i )
+ Dar_ManDfsUnreach_rec( p, Dar_ObjFanin0(pObj), vNodes );
+
+ // refine resulting nodes
+ do
+ {
+ k = 0;
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ assert( Dar_ObjIsTravIdPrevious(p, pObj) );
+ if ( Dar_ObjIsLatch(pObj) || Dar_ObjIsBuf(pObj) )
+ {
+ pFanin = Dar_ObjFanin0(pObj);
+ assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) );
+ if ( Dar_ObjIsTravIdCurrent(p, pFanin) )
+ {
+ Dar_ObjSetTravIdCurrent( p, pObj );
+ continue;
+ }
+ }
+ else // AND gate
+ {
+ assert( Dar_ObjIsNode(pObj) );
+ pFanin = Dar_ObjFanin0(pObj);
+ assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) );
+ if ( Dar_ObjIsTravIdCurrent(p, pFanin) )
+ {
+ Dar_ObjSetTravIdCurrent( p, pObj );
+ continue;
+ }
+ pFanin = Dar_ObjFanin1(pObj);
+ assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) );
+ if ( Dar_ObjIsTravIdCurrent(p, pFanin) )
+ {
+ Dar_ObjSetTravIdCurrent( p, pObj );
+ continue;
+ }
+ }
+ // write it back
+ Vec_PtrWriteEntry( vNodes, k++, pObj );
+ }
+ Vec_PtrShrink( vNodes, k );
+ }
+ while ( k < i );
+
+ if ( Vec_PtrSize(vNodes) > 0 )
+ printf( "Found %d unreachable.\n", Vec_PtrSize(vNodes) );
+ return vNodes;
+
+/*
+ // the resulting array contains all unreachable nodes except const 1
+ if ( Vec_PtrSize(vNodes) == 0 )
+ {
+ Vec_PtrFree( vNodes );
+ return 0;
+ }
+ RetValue = Vec_PtrSize(vNodes);
+
+ // mark these nodes
+ Dar_ManIncrementTravId( p );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Dar_ObjSetTravIdCurrent( p, pObj );
+ Vec_PtrFree( vNodes );
+ return RetValue;
+*/
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Removes nodes that do not fanout into POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dar_ManRemoveUnmarked( Dar_Man_t * p )
+{
+ Vec_Ptr_t * vNodes;
+ Dar_Obj_t * pObj;
+ int i, RetValue;
+ // collect unmarked nodes
+ vNodes = Vec_PtrAlloc( 100 );
+ Dar_ManForEachObj( p, pObj, i )
+ {
+ if ( Dar_ObjIsTerm(pObj) )
+ continue;
+ if ( Dar_ObjIsTravIdCurrent(p, pObj) )
+ continue;
+//Dar_ObjPrintVerbose( pObj, 0 );
+ Dar_ObjDisconnect( p, pObj );
+ Vec_PtrPush( vNodes, pObj );
+ }
+ if ( Vec_PtrSize(vNodes) == 0 )
+ {
+ Vec_PtrFree( vNodes );
+ return 0;
+ }
+ // remove the dangling objects
+ RetValue = Vec_PtrSize(vNodes);
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Dar_ObjDelete( p, pObj );
+ printf( "Removes %d dangling.\n", Vec_PtrSize(vNodes) );
+ Vec_PtrFree( vNodes );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Dar_Obj_t * Dar_ObjReal_rec( Dar_Obj_t * pObj )
+{
+ Dar_Obj_t * pObjNew, * pObjR = Dar_Regular(pObj);
+ if ( !Dar_ObjIsBuf(pObjR) )
+ return pObj;
+ pObjNew = Dar_ObjReal_rec( Dar_ObjChild0(pObjR) );
+ return Dar_NotCond( pObjNew, Dar_IsComplement(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Rehashes the nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dar_ManSeqRehashOne( Dar_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach )
+{
+ Dar_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1;
+ int i, RetValue = 0;
+ // mark the unreachable nodes
+ Dar_ManIncrementTravId( p );
+ Vec_PtrForEachEntry( vUnreach, pObj, i )
+ Dar_ObjSetTravIdCurrent(p, pObj);
+ // go through the nodes while skipping unreachable
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ // skip nodes unreachable from the PIs
+ if ( Dar_ObjIsTravIdCurrent(p, pObj) )
+ continue;
+ // process the node
+ if ( Dar_ObjIsPo(pObj) )
+ {
+ if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) )
+ continue;
+ pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+ Dar_ObjPatchFanin0( p, pObj, pFanin0 );
+ continue;
+ }
+ if ( Dar_ObjIsLatch(pObj) )
+ {
+ if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) )
+ continue;
+ pObjNew = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+ pObjNew = Dar_Latch( p, pObjNew, 0 );
+ Dar_ObjReplace( p, pObj, pObjNew, 1 );
+ RetValue = 1;
+ continue;
+ }
+ if ( Dar_ObjIsNode(pObj) )
+ {
+ if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) && !Dar_ObjIsBuf(Dar_ObjFanin1(pObj)) )
+ continue;
+ pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+ pFanin1 = Dar_ObjReal_rec( Dar_ObjChild1(pObj) );
+ pObjNew = Dar_And( p, pFanin0, pFanin1 );
+ Dar_ObjReplace( p, pObj, pObjNew, 1 );
+ RetValue = 1;
+ continue;
+ }
+ }
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [If AIG contains buffers, this procedure removes them.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_ManRemoveBuffers( Dar_Man_t * p )
+{
+ Dar_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1;
+ int i;
+ if ( Dar_ManBufNum(p) == 0 )
+ return;
+ Dar_ManForEachObj( p, pObj, i )
+ {
+ if ( Dar_ObjIsPo(pObj) )
+ {
+ if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) )
+ continue;
+ pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+ Dar_ObjPatchFanin0( p, pObj, pFanin0 );
+ }
+ else if ( Dar_ObjIsLatch(pObj) )
+ {
+ if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) )
+ continue;
+ pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+ pObjNew = Dar_Latch( p, pFanin0, 0 );
+ Dar_ObjReplace( p, pObj, pObjNew, 0 );
+ }
+ else if ( Dar_ObjIsAnd(pObj) )
+ {
+ if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) && !Dar_ObjIsBuf(Dar_ObjFanin1(pObj)) )
+ continue;
+ pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
+ pFanin1 = Dar_ObjReal_rec( Dar_ObjChild1(pObj) );
+ pObjNew = Dar_And( p, pFanin0, pFanin1 );
+ Dar_ObjReplace( p, pObj, pObjNew, 0 );
+ }
+ }
+ assert( Dar_ManBufNum(p) == 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dar_ManSeqStrash( Dar_Man_t * p, int nLatches, int * pInits )
+{
+ Vec_Ptr_t * vNodes, * vUnreach;
+ Dar_Obj_t * pObj;
+ int i;
+ int RetValue = 1;
+ // create latches out of the additional PI/PO pairs
+ Dar_ManSeqStrashConvert( p, nLatches, pInits );
+ // iteratively rehash the network
+ while ( RetValue )
+ {
+ Dar_ManPrintStats( p );
+
+ Dar_ManForEachObj( p, pObj, i )
+ assert( pObj->Type > 0 );
+
+ // mark nodes unreachable from the PIs
+ vUnreach = Dar_ManDfsUnreach( p );
+ // collect nodes reachable from the POs
+ vNodes = Dar_ManDfsSeq( p );
+ // remove nodes unreachable from the POs
+ Dar_ManRemoveUnmarked( p );
+ // continue rehashing as long as there are changes
+ RetValue = Dar_ManSeqRehashOne( p, vNodes, vUnreach );
+ Vec_PtrFree( vNodes );
+ Vec_PtrFree( vUnreach );
+ }
+ // perform the final cleanup
+ Dar_ManIncrementTravId( p );
+ vNodes = Dar_ManDfsSeq( p );
+ Dar_ManRemoveUnmarked( p );
+ Vec_PtrFree( vNodes );
+ // remove buffers if they are left
+// Dar_ManRemoveBuffers( p );
+ // clean up
+ if ( !Dar_ManCheck( p ) )
+ {
+ printf( "Dar_ManSeqStrash: The network check has failed.\n" );
+ return 0;
+ }
+ return 1;
+
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/darTable.c b/src/aig/dar/darTable.c
index 8b4bfaf3..af9956ec 100644
--- a/src/aig/dar/darTable.c
+++ b/src/aig/dar/darTable.c
@@ -39,8 +39,15 @@ static unsigned long Dar_Hash( Dar_Obj_t * pObj, int TableSize )
static Dar_Obj_t ** Dar_TableFind( Dar_Man_t * p, Dar_Obj_t * pObj )
{
Dar_Obj_t ** ppEntry;
- assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) );
- assert( Dar_ObjFanin0(pObj)->Id < Dar_ObjFanin1(pObj)->Id );
+ if ( Dar_ObjIsLatch(pObj) )
+ {
+ assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) == NULL );
+ }
+ else
+ {
+ assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) );
+ assert( Dar_ObjFanin0(pObj)->Id < Dar_ObjFanin1(pObj)->Id );
+ }
for ( ppEntry = p->pTable + Dar_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext )
if ( *ppEntry == pObj )
return ppEntry;
@@ -70,10 +77,20 @@ Dar_Obj_t * Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost )
{
Dar_Obj_t * pEntry;
assert( !Dar_IsComplement(pGhost) );
- assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) );
- assert( Dar_ObjFanin0(pGhost)->Id < Dar_ObjFanin1(pGhost)->Id );
- if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) || !Dar_ObjRefs(Dar_ObjFanin1(pGhost)) )
- return NULL;
+ if ( pGhost->Type == DAR_AIG_LATCH )
+ {
+ assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) == NULL );
+ if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) )
+ return NULL;
+ }
+ else
+ {
+ assert( pGhost->Type == DAR_AIG_AND );
+ assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) );
+ assert( Dar_ObjFanin0(pGhost)->Id < Dar_ObjFanin1(pGhost)->Id );
+ if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) || !Dar_ObjRefs(Dar_ObjFanin1(pGhost)) )
+ return NULL;
+ }
for ( pEntry = p->pTable[Dar_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
{
if ( Dar_ObjChild0(pEntry) == Dar_ObjChild0(pGhost) &&
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index b682f8ae..39e985c0 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -55,7 +55,10 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) );
// visit the transitive fanin of the node
Abc_ObjForEachFanin( pNode, pFanin, i )
+ {
+// pFanin = Abc_ObjFanin( pNode, Abc_ObjFaninNum(pNode)-1-i );
Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(pFanin), vNodes );
+ }
// add the node after the fanins have been added
Vec_PtrPush( vNodes, pNode );
}
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index ce187f60..7d8d0f0f 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -987,7 +987,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
Abc_Obj_t * pNet, * pNode;
int i;
- if ( Abc_NtkNodeNum(pNtk) == 0 )
+ if ( Abc_NtkNodeNum(pNtk) == 0 && Abc_NtkBoxNum(pNtk) == 0 )
return;
// check for non-driven nets
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1e0fed0c..d5321e6d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -330,7 +330,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Kit_TruthCountMintermsPrecomp();
// Kit_DsdPrecompute4Vars();
- Dar_LibStart();
+// Dar_LibStart();
}
/**Function*************************************************************
@@ -346,7 +346,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
***********************************************************************/
void Abc_End()
{
- Dar_LibStop();
+// Dar_LibStop();
Abc_NtkFraigStoreClean();
// Rwt_Man4ExplorePrint();
@@ -5931,7 +5931,7 @@ usage:
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk;//, * pNtkRes;
+ Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int nLevels;
// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
@@ -5940,6 +5940,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern int Pr_ManProofTest( char * pFileName );
extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk );
extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk );
+ extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -6049,8 +6050,21 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_Ntk4VarTable( pNtk );
// Dat_NtkGenerateArrays( pNtk );
- return 0;
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "Network should be strashed. Command has failed.\n" );
+ return 1;
+ }
+ pNtkRes = Abc_NtkDar( pNtk );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Command has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
usage:
fprintf( pErr, "usage: test [-h]\n" );
fprintf( pErr, "\t testbench for new procedures\n" );
@@ -7286,6 +7300,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
int fAllNodes;
int fExdc;
int c;
+ int fPartition = 0;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -7307,7 +7322,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pParams->fVerbose = 0; // the verbosiness flag
pParams->fVerboseP = 0; // the verbosiness flag
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscpvaeh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscptvaeh" ) ) != EOF )
{
switch ( c )
{
@@ -7360,6 +7375,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
pParams->fVerbose ^= 1;
break;
+ case 't':
+ fPartition ^= 1;
+ break;
case 'a':
fAllNodes ^= 1;
break;
@@ -7388,13 +7406,28 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pParams->fVerboseP = pParams->fTryProve;
// get the new network
- if ( Abc_NtkIsStrash(pNtk) )
- pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+ if ( fPartition )
+ {
+ pNtkRes = Abc_NtkDup( pNtk );
+ if ( Abc_NtkIsStrash(pNtk) )
+ Abc_NtkFraigPartitionedTime( pNtk, &Params );
+ else
+ {
+ pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
+ Abc_NtkFraigPartitionedTime( pNtk, &Params );
+ Abc_NtkDelete( pNtk );
+ }
+ }
else
{
- pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
- pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
- Abc_NtkDelete( pNtk );
+ if ( Abc_NtkIsStrash(pNtk) )
+ pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+ else
+ {
+ pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 );
+ pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
+ Abc_NtkDelete( pNtk );
+ }
}
if ( pNtkRes == NULL )
{
@@ -7411,7 +7444,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
sprintf( Buffer, "%d", pParams->nBTLimit );
- fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvah]\n" );
+ fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvtah]\n" );
fprintf( pErr, "\t transforms a logic network into a functionally reduced AIG\n" );
fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsRand );
fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna );
@@ -7423,6 +7456,7 @@ usage:
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pParams->fVerbose? "yes": "no" );
fprintf( pErr, "\t-e : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" );
fprintf( pErr, "\t-a : toggle between all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "dfs" );
+ fprintf( pErr, "\t-t : toggle using partitioned representation [default = %s]\n", fPartition? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 0863061b..81278515 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -25,62 +25,12 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk );
-static Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan );
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis [Gives the current ABC network to AIG manager for processing.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
-{
- Abc_Ntk_t * pNtkAig;
- Dar_Man_t * pMan;//, * pTemp;
- assert( Abc_NtkIsStrash(pNtk) );
- // convert to the AIG manager
- pMan = Abc_NtkToDar( pNtk );
- if ( pMan == NULL )
- return NULL;
- if ( !Dar_ManCheck( pMan ) )
- {
- printf( "Abc_NtkDar: AIG check has failed.\n" );
- Dar_ManStop( pMan );
- return NULL;
- }
- // perform balance
- Dar_ManPrintStats( pMan );
-// Dar_ManDumpBlif( pMan, "aig_temp.blif" );
- pMan->pPars = Dar_ManDefaultParams();
- Dar_ManRewrite( pMan );
- Dar_ManPrintStats( pMan );
- // convert from the AIG manager
- pNtkAig = Abc_NtkFromDar( pNtk, pMan );
- if ( pNtkAig == NULL )
- return NULL;
- Dar_ManStop( pMan );
- // make sure everything is okay
- if ( !Abc_NtkCheck( pNtkAig ) )
- {
- printf( "Abc_NtkDar: The network check has failed.\n" );
- Abc_NtkDelete( pNtkAig );
- return NULL;
- }
- return pNtkAig;
-}
-
-/**Function*************************************************************
-
Synopsis [Converts the network from the AIG manager into ABC.]
Description []
@@ -96,7 +46,7 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
Abc_Obj_t * pObj;
int i;
// create the manager
- pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) );
+ pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
// transfer the pointers to the basic nodes
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Dar_ManConst1(pMan);
Abc_NtkForEachCi( pNtk, pObj, i )
@@ -122,14 +72,14 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan )
{
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkNew;
Dar_Obj_t * pObj;
int i;
// perform strashing
- pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
// transfer the pointers to the basic nodes
Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
Dar_ManForEachPi( pMan, pObj, i )
@@ -147,6 +97,159 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan )
return pNtkNew;
}
+/**Function*************************************************************
+
+ Synopsis [Converts the network from the AIG manager into ABC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
+ Dar_Obj_t * pObj;
+ int i;
+// assert( Dar_ManLatchNum(pMan) > 0 );
+ // perform strashing
+ pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ // transfer the pointers to the basic nodes
+ Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+ Dar_ManForEachPi( pMan, pObj, i )
+ pObj->pData = Abc_NtkPi(pNtkNew, i);
+ // create latches of the new network
+ Dar_ManForEachObj( pMan, pObj, i )
+ {
+ if ( !Dar_ObjIsLatch(pObj) )
+ continue;
+ pObjNew = Abc_NtkCreateLatch( pNtkNew );
+ pFaninNew0 = Abc_NtkCreateBi( pNtkNew );
+ pFaninNew1 = Abc_NtkCreateBo( pNtkNew );
+ Abc_ObjAddFanin( pObjNew, pFaninNew0 );
+ Abc_ObjAddFanin( pFaninNew1, pObjNew );
+ Abc_LatchSetInit0( pObjNew );
+ pObj->pData = Abc_ObjFanout0( pObjNew );
+ }
+ Abc_NtkAddDummyBoxNames( pNtkNew );
+ // rebuild the AIG
+ vNodes = Dar_ManDfs( pMan );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ // add the first fanin
+ pObj->pData = pFaninNew0 = (Abc_Obj_t *)Dar_ObjChild0Copy(pObj);
+ if ( Dar_ObjIsBuf(pObj) )
+ continue;
+ // add the second fanin
+ pFaninNew1 = (Abc_Obj_t *)Dar_ObjChild1Copy(pObj);
+ // create the new node
+ if ( Dar_ObjIsExor(pObj) )
+ pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+ else
+ pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
+ }
+ Vec_PtrFree( vNodes );
+ // connect the PO nodes
+ Dar_ManForEachPo( pMan, pObj, i )
+ {
+ pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj );
+ Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew );
+ }
+ // connect the latches
+ Dar_ManForEachObj( pMan, pObj, i )
+ {
+ if ( !Dar_ObjIsLatch(pObj) )
+ continue;
+ pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj );
+ Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew );
+ }
+ if ( !Abc_NtkCheck( pNtkNew ) )
+ fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collect latch values.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pLatch;
+ int i, * pArray;
+ pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) );
+ Abc_NtkForEachLatch( pNtk, pLatch, i )
+ pArray[i] = Abc_LatchIsInit1(pLatch);
+ return pArray;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
+{
+ Abc_Ntk_t * pNtkAig;
+ Dar_Man_t * pMan;//, * pTemp;
+ int * pArray;
+
+ assert( Abc_NtkIsStrash(pNtk) );
+ // convert to the AIG manager
+ pMan = Abc_NtkToDar( pNtk );
+ if ( pMan == NULL )
+ return NULL;
+ if ( !Dar_ManCheck( pMan ) )
+ {
+ printf( "Abc_NtkDar: AIG check has failed.\n" );
+ Dar_ManStop( pMan );
+ return NULL;
+ }
+ // perform balance
+ Dar_ManPrintStats( pMan );
+
+ pArray = Abc_NtkGetLatchValues(pNtk);
+ Dar_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray );
+ free( pArray );
+
+// Dar_ManDumpBlif( pMan, "aig_temp.blif" );
+// pMan->pPars = Dar_ManDefaultParams();
+// Dar_ManRewrite( pMan );
+ Dar_ManPrintStats( pMan );
+ // convert from the AIG manager
+ if ( Dar_ManLatchNum(pMan) )
+ pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan );
+ else
+ pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+ if ( pNtkAig == NULL )
+ return NULL;
+ Dar_ManStop( pMan );
+ // make sure everything is okay
+ if ( !Abc_NtkCheck( pNtkAig ) )
+ {
+ printf( "Abc_NtkDar: The network check has failed.\n" );
+ Abc_NtkDelete( pNtkAig );
+ return NULL;
+ }
+ return pNtkAig;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 30e49af2..fa6771b3 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -687,7 +687,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
// set the number of networks stored
Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 );
}
-// printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
+ printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
return 1;
}
@@ -734,7 +734,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
Fraig_ParamsSetDefault( &Params );
Params.nPatsRand = nWordsMin * 32; // the number of words of random simulation info
Params.nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info
- Params.nBTLimit = 99; // the max number of backtracks to perform
+ Params.nBTLimit = 999999; // the max number of backtracks to perform
Params.fFuncRed = 1; // performs only one level hashing
Params.fFeedBack = 1; // enables solver feedback
Params.fDist1Pats = 1; // enables distance-1 patterns
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 748868de..787e3f88 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -698,12 +698,67 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
// derive the final network
pNtkFraig = Abc_NtkPartStitchChoices( pNtk, vFraigs );
Vec_PtrForEachEntry( vFraigs, pNtkAig, i )
+ {
+// Abc_NtkPrintStats( stdout, pNtkAig, 0 );
Abc_NtkDelete( pNtkAig );
+ }
Vec_PtrFree( vFraigs );
return pNtkFraig;
}
+/**Function*************************************************************
+
+ Synopsis [Stitches together several networks with choice nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams )
+{
+ extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+ extern void * Abc_FrameGetGlobalFrame();
+
+ Vec_Vec_t * vParts;
+ Vec_Ptr_t * vFraigs, * vOne;
+ Abc_Ntk_t * pNtkAig, * pNtkFraig;
+ int i;
+ int clk = clock();
+
+ // perform partitioning
+ assert( Abc_NtkIsStrash(pNtk) );
+// vParts = Abc_NtkPartitionNaive( pNtk, 20 );
+ vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
+
+ Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
+
+ // fraig each partition
+ vFraigs = Vec_PtrAlloc( Vec_VecSize(vParts) );
+ Vec_VecForEachLevel( vParts, vOne, i )
+ {
+ pNtkAig = Abc_NtkCreateConeArray( pNtk, vOne, 0 );
+ pNtkFraig = Abc_NtkFraig( pNtkAig, pParams, 0, 0 );
+ Vec_PtrPush( vFraigs, pNtkFraig );
+ Abc_NtkDelete( pNtkAig );
+
+ printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) );
+ }
+ Vec_VecFree( vParts );
+
+ Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
+
+ // derive the final network
+ Vec_PtrForEachEntry( vFraigs, pNtkAig, i )
+ Abc_NtkDelete( pNtkAig );
+ Vec_PtrFree( vFraigs );
+
+ PRT( "Partitioned fraiging time", clock() - clk );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index a54a00fe..fe519476 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -96,7 +96,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
// prepare the array of nodes
vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
- Vec_PtrPush( vNodes, Abc_AigConst1(pNtkNew) );
+ Vec_PtrPush( vNodes, Abc_ObjNot( Abc_AigConst1(pNtkNew) ) );
// create the PIs
for ( i = 0; i < nInputs; i++ )
@@ -122,6 +122,8 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Vec_PtrPush( vNodes, pNode1 );
// assign names to latch and its input
Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
+
+ printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
}
// remember the beginning of latch/PO literals
@@ -156,14 +158,17 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) );
+ pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Abc_ObjAddFanin( pObj, pNode0 );
+
+ printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id );
+
}
// read the PO driver literals
Abc_NtkForEachPo( pNtkNew, pObj, i )
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
- pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) );
+ pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Abc_ObjAddFanin( pObj, pNode0 );
}
@@ -204,7 +209,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" );
// mark the node as named
pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
- }
+ }
// skipping the comments
free( pContents );
Vec_PtrFree( vNodes );
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 2730ba69..ba622e40 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -118,7 +118,13 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
if ( strncmp(pType, "DFF", 3) == 0 ) // works for both DFF and DFFRSE
{
pNode = Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] );
- Abc_LatchSetInit0( pNode );
+// Abc_LatchSetInit0( pNode );
+ if ( pType[3] == '0' )
+ Abc_LatchSetInit0( pNode );
+ else if ( pType[3] == '1' )
+ Abc_LatchSetInit1( pNode );
+ else
+ Abc_LatchSetInitDc( pNode );
}
else if ( strcmp(pType, "LUT") == 0 )
{
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index a02d53fd..a4eeb78f 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -113,7 +113,12 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
{
// write inputs and outputs
// fprintf( pFile, "module %s ( gclk,\n ", Abc_NtkName(pNtk) );
- fprintf( pFile, "module %s ( \n ", Abc_NtkName(pNtk) );
+ fprintf( pFile, "module %s ( ", Abc_NtkName(pNtk) );
+ // add the clock signal if it does not exist
+ if ( Abc_NtkLatchNum(pNtk) > 0 && Nm_ManFindIdByName(pNtk->pManName, "clock", ABC_OBJ_PI) == -1 )
+ fprintf( pFile, "clock, " );
+ // write other primary inputs
+ fprintf( pFile, "\n " );
if ( Abc_NtkPiNum(pNtk) > 0 )
{
Io_WriteVerilogPis( pFile, pNtk, 3 );
@@ -435,7 +440,8 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
return;
// write the latches
// fprintf( pFile, " always @(posedge %s) begin\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0))) );
- fprintf( pFile, " always begin\n" );
+// fprintf( pFile, " always begin\n" );
+ fprintf( pFile, " always @ (posedge clock) begin\n" );
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
fprintf( pFile, " %s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) );
diff --git a/src/base/io/ioWriteVerilog.zip b/src/base/io/ioWriteVerilog.zip
new file mode 100644
index 00000000..19e68a89
--- /dev/null
+++ b/src/base/io/ioWriteVerilog.zip
Binary files differ
diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h
index cf2b7497..9c538ac4 100644
--- a/src/base/ver/ver.h
+++ b/src/base/ver/ver.h
@@ -66,6 +66,7 @@ struct Ver_Man_t_
Vec_Ptr_t * vNames;
Vec_Ptr_t * vStackFn;
Vec_Int_t * vStackOp;
+ Vec_Int_t * vPerm;
};
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index 12c54dba..6d7d230e 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -110,6 +110,7 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib )
p->vNames = Vec_PtrAlloc( 100 );
p->vStackFn = Vec_PtrAlloc( 100 );
p->vStackOp = Vec_IntAlloc( 100 );
+ p->vPerm = Vec_IntAlloc( 100 );
// create the design library and assign the technology library
p->pDesign = Abc_LibCreate( pFileName );
p->pDesign->pLibrary = pGateLib;
@@ -136,6 +137,7 @@ void Ver_ParseStop( Ver_Man_t * p )
Vec_PtrFree( p->vNames );
Vec_PtrFree( p->vStackFn );
Vec_IntFree( p->vStackOp );
+ Vec_IntFree( p->vPerm );
free( p );
}
@@ -1193,6 +1195,12 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen());
else
{
+ // "assign foo = \bar ;"
+ if ( *pEquation == '\\' )
+ {
+ pEquation++;
+ pEquation[strlen(pEquation) - 1] = 0;
+ }
if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
{
sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." );
@@ -1358,6 +1366,29 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga
/**Function*************************************************************
+ Synopsis [Returns the index of the given pin the gate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ver_FindGateInput( Mio_Gate_t * pGate, char * pName )
+{
+ Mio_Pin_t * pGatePin;
+ int i;
+ for ( i = 0, pGatePin = Mio_GateReadPins(pGate); pGatePin != NULL; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+ if ( strcmp(pName, Mio_PinReadName(pGatePin)) == 0 )
+ return i;
+ if ( strcmp(pName, Mio_GateReadOutName(pGate)) == 0 )
+ return i;
+ return -1;
+}
+
+/**Function*************************************************************
+
Synopsis [Parses one directive.]
Description []
@@ -1369,10 +1400,10 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga
***********************************************************************/
int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
{
- Mio_Pin_t * pGatePin;
Ver_Stream_t * p = pMan->pReader;
Abc_Obj_t * pNetActual, * pNode;
char * pWord, Symbol;
+ int Input, i, nFanins = Mio_GateReadInputs(pGate);
// convert from the blackbox into the network with local functions representated by gates
if ( 1 != pMan->fMapped )
@@ -1404,7 +1435,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
pNode->pData = pGate;
// parse pairs of formal/actural inputs
- pGatePin = Mio_GateReadPins(pGate);
+ Vec_IntClear( pMan->vPerm );
while ( 1 )
{
// process one pair of formal/actual parameters
@@ -1420,24 +1451,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
if ( pWord == NULL )
return 0;
- // make sure that the formal name is the same as the gate's
- if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) )
- {
- if ( strcmp(pWord, Mio_GateReadOutName(pGate)) )
- {
- sprintf( pMan->sError, "Formal output name listed %s is different from the name of the gate output %s.", pWord, Mio_GateReadOutName(pGate) );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
- }
- }
- else
+ // find the corresponding pin of the gate
+ Input = Ver_FindGateInput( pGate, pWord );
+ if ( Input == -1 )
{
- if ( strcmp(pWord, Mio_PinReadName(pGatePin)) )
- {
- sprintf( pMan->sError, "Formal input name listed %s is different from the name of the corresponding pin %s.", pWord, Mio_PinReadName(pGatePin) );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
- }
+ sprintf( pMan->sError, "Formal input name %s cannot be found in the gate %s.", pWord, Mio_GateReadOutName(pGate) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
}
// open the paranthesis
@@ -1482,10 +1502,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
}
// add the fanin
- if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) )
- Abc_ObjAddFanin( pNetActual, pNode ); // fanout
- else
+ if ( Input < nFanins )
+ {
+ Vec_IntPush( pMan->vPerm, Input );
Abc_ObjAddFanin( pNode, pNetActual ); // fanin
+ }
+ else
+ Abc_ObjAddFanin( pNetActual, pNode ); // fanout
// check if it is the end of gate
Ver_ParseSkipComments( pMan );
@@ -1501,13 +1524,10 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
return 0;
}
Ver_ParseSkipComments( pMan );
-
- // get the next pin
- pGatePin = Mio_PinReadNext(pGatePin);
}
// check that the gate as the same number of input
- if ( !(Abc_ObjFaninNum(pNode) == Mio_GateReadInputs(pGate) && Abc_ObjFanoutNum(pNode) == 1) )
+ if ( !(Abc_ObjFaninNum(pNode) == nFanins && Abc_ObjFanoutNum(pNode) == 1) )
{
sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) );
Ver_ParsePrintErrorMessage( pMan );
@@ -1522,6 +1542,20 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
+
+ // check if we need to permute the inputs
+ Vec_IntForEachEntry( pMan->vPerm, Input, i )
+ if ( Input != i )
+ break;
+ if ( i < Vec_IntSize(pMan->vPerm) )
+ {
+ // add the fanin numnbers to the end of the permuation array
+ for ( i = 0; i < nFanins; i++ )
+ Vec_IntPush( pMan->vPerm, Abc_ObjFaninId(pNode, i) );
+ // write the fanin numbers into their corresponding places (according to the gate)
+ for ( i = 0; i < nFanins; i++ )
+ Vec_IntWriteEntry( &pNode->vFanins, Vec_IntEntry(pMan->vPerm, i), Vec_IntEntry(pMan->vPerm, i+nFanins) );
+ }
return 1;
}
@@ -1546,6 +1580,7 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
Abc_Obj_t * pNode;
char * pWord, Symbol;
int fCompl, fFormalIsGiven;
+ int i, k, Bit, Limit, nMsb, nLsb, fQuit, flag;
// gate the name of the box
pWord = Ver_ParseGetName( pMan );
@@ -1613,8 +1648,6 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
// consider the case of vector-inputs
if ( Symbol == '{' )
{
- int i, k, Bit, Limit, nMsb, nLsb, fQuit;
-
// skip this char
Ver_StreamPopChar(p);
@@ -1673,7 +1706,8 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
pNetActual = Ver_ParseFindNet( pNtk, pWord );
if ( pNetActual == NULL )
{
- if ( !strncmp(pWord, "Open_", 5) )
+ if ( !strncmp(pWord, "Open_", 5) ||
+ !strncmp(pWord, "dct_unconnected", 15) )
pNetActual = Abc_NtkCreateNet( pNtk );
else
{
@@ -1697,7 +1731,8 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
pNetActual = Ver_ParseFindNet( pNtk, Buffer );
if ( pNetActual == NULL )
{
- if ( !strncmp(pWord, "Open_", 5) )
+ if ( !strncmp(pWord, "Open_", 5) ||
+ !strncmp(pWord, "dct_unconnected", 15) )
pNetActual = Abc_NtkCreateNet( pNtk );
else
{
@@ -1738,34 +1773,72 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
if ( pWord[0] == 0 )
{
pNetActual = Abc_NtkCreateNet( pNtk );
+ Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
}
else
{
-/*
- // check if the name is complemented
- fCompl = (pWord[0] == '~');
- if ( fCompl )
- {
- pWord++;
- if ( pNtk->pData == NULL )
- pNtk->pData = Extra_MmFlexStart();
- }
-*/
// get the actual net
+ flag=0;
pNetActual = Ver_ParseFindNet( pNtk, pWord );
- if ( pNetActual == NULL )
+ if ( pNetActual == NULL )
{
- if ( !strncmp(pWord, "Open_", 5) )
- pNetActual = Abc_NtkCreateNet( pNtk );
- else
+ Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
+ if ( nMsb == -1 && nLsb == -1 )
{
- sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
+ Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
+ if ( nMsb == -1 && nLsb == -1 )
+ {
+ if ( !strncmp(pWord, "Open_", 5) ||
+ !strncmp(pWord, "dct_unconnected", 15) )
+ {
+ pNetActual = Abc_NtkCreateNet( pNtk );
+ Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+ }
+ else
+ {
+ sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ }
+ else
+ {
+ flag=1;
+ }
+ }
+ else
+ {
+ flag=1;
}
+ if (flag)
+ {
+ Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;
+ for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--)
+ {
+ // get the actual net
+ sprintf( Buffer, "%s[%d]", pWord, Bit );
+ pNetActual = Ver_ParseFindNet( pNtk, Buffer );
+ if ( pNetActual == NULL )
+ {
+ if ( !strncmp(pWord, "Open_", 5) ||
+ !strncmp(pWord, "dct_unconnected", 15))
+ pNetActual = Abc_NtkCreateNet( pNtk );
+ else
+ {
+ sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
+ }
+ Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+ }
+ }
+ }
+ else
+ {
+ Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
}
}
- Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
}
if ( fFormalIsGiven )
@@ -2000,8 +2073,8 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
}
if ( pBundle == NULL )
{
- printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.",
- pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
+// printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.",
+// pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
continue;
}
}
diff --git a/src/base/ver/verCore.zip b/src/base/ver/verCore.zip
index 45574008..cdfcf5a4 100644
--- a/src/base/ver/verCore.zip
+++ b/src/base/ver/verCore.zip
Binary files differ
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index f4ffa4c1..f3fa049e 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -427,6 +427,26 @@ int If_ManCrossCut( If_Man_t * p )
return nCutSizeMax;
}
+/**Function*************************************************************
+
+ Synopsis [Computes cross-cut of the circuit.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int If_ManCountTrueArea( If_Man_t * p )
+{
+ If_Obj_t * pObj;
+ int i, Area = 0;
+ Vec_PtrForEachEntry( p->vMapped, pObj, i )
+ Area += 1 + (If_ObjCutBest(pObj)->nLeaves > (unsigned)p->pPars->nLutSize / 2);
+ return Area;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 05:44:49 +0000