luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc70608

This commit is contained in:
Alan Mishchenko 2007-06-08 08:01:00 -07:00
parent feb8fb692e
commit d47752011d
24 changed files with 1103 additions and 210 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abc.dsp
View File

@ -858,6 +858,10 @@ SOURCE=.\src\aig\dar\darOper.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darSeq.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darTable.c
# End Source File
# Begin Source File

38
src/aig/dar/dar.h
View File

@ -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 );

13
src/aig/dar/darCheck.c
View File

@ -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) )

4
src/aig/dar/darCore.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

55
src/aig/dar/darDfs.c
View File

@ -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;
}

26
src/aig/dar/darMan.c
View File

@ -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" );
}

55
src/aig/dar/darObj.c
View File

@ -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 )
@ -219,6 +218,33 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop )
Dar_ObjDelete_rec( p, pFanin1, 1 );
}
/**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.]
@ -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]++;
}
////////////////////////////////////////////////////////////////////////

64
src/aig/dar/darOper.c
View File

@ -87,6 +87,43 @@ Dar_Obj_t * Dar_Oper( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t
return NULL;
}
/**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.]
@ -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*************************************************************

471
src/aig/dar/darSeq.c Normal file
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

29
src/aig/dar/darTable.c
View File

@ -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) &&

3
src/base/abc/abcDfs.c
View File

@ -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 );
}

2
src/base/abc/abcNtk.c
View File

@ -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

56
src/base/abci/abc.c
View File

@ -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;
}

209
src/base/abci/abcDar.c
View File

@ -25,60 +25,10 @@
/// 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.]
@ -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 ///
////////////////////////////////////////////////////////////////////////

4
src/base/abci/abcFraig.c
View File

@ -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

55
src/base/abci/abcPart.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

13
src/base/io/ioReadAiger.c
View File

@ -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 );

8
src/base/io/ioReadBench.c
View File

@ -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 )
{

10
src/base/io/ioWriteVerilog.c
View File

@ -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)))) );

BIN
src/base/io/ioWriteVerilog.zip Normal file
View File

Binary file not shown.

1
src/base/ver/ver.h
View File

@ -66,6 +66,7 @@ struct Ver_Man_t_
Vec_Ptr_t * vNames;
Vec_Ptr_t * vStackFn;
Vec_Int_t * vStackOp;
Vec_Int_t * vPerm;
};

173
src/base/ver/verCore.c
View File

@ -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." );
@ -1356,6 +1364,29 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga
return 1;
}
/**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.]
@ -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) )
// find the corresponding pin of the gate
Input = Ver_FindGateInput( pGate, pWord );
if ( Input == -1 )
{
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
{
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;
}
}

BIN
src/base/ver/verCore.zip
View File

Binary file not shown.

20
src/map/if/ifUtil.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////