Skip to content

A
abc
Commit 93c3f160 by Alan Mishchenko
Options

Version abc80329

parent 416ffc11
Showing with 322 additions and 211 deletions
Makefile
...@@ -19,7 +19,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \ ...@@ -19,7 +19,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \ src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \
src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \ src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \ src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
src/aig/bdc src/aig/bar src/aig/ntl src/aig/ntk src/aig/tim src/aig/bdc src/aig/bar src/aig/ntl src/aig/tim
default: $(PROG) default: $(PROG)
......
src/aig/aig/aig.h
...@@ -47,7 +47,6 @@ extern "C" { ...@@ -47,7 +47,6 @@ extern "C" {
typedef struct Aig_Man_t_ Aig_Man_t; typedef struct Aig_Man_t_ Aig_Man_t;
typedef struct Aig_Obj_t_ Aig_Obj_t; typedef struct Aig_Obj_t_ Aig_Obj_t;
typedef struct Aig_Box_t_ Aig_Box_t;
typedef struct Aig_MmFixed_t_ Aig_MmFixed_t; typedef struct Aig_MmFixed_t_ Aig_MmFixed_t;
typedef struct Aig_MmFlex_t_ Aig_MmFlex_t; typedef struct Aig_MmFlex_t_ Aig_MmFlex_t;
typedef struct Aig_MmStep_t_ Aig_MmStep_t; typedef struct Aig_MmStep_t_ Aig_MmStep_t;
...@@ -61,9 +60,7 @@ typedef enum { ...@@ -61,9 +60,7 @@ typedef enum {
AIG_OBJ_BUF, // 4: buffer node AIG_OBJ_BUF, // 4: buffer node
AIG_OBJ_AND, // 5: AND node AIG_OBJ_AND, // 5: AND node
AIG_OBJ_EXOR, // 6: EXOR node AIG_OBJ_EXOR, // 6: EXOR node
AIG_OBJ_LATCH, // 7: latch AIG_OBJ_VOID // 7: unused object
AIG_OBJ_BOX, // 8: latch
AIG_OBJ_VOID // 9: unused object
} Aig_Type_t; } Aig_Type_t;
// the AIG node // the AIG node
...@@ -73,11 +70,11 @@ struct Aig_Obj_t_ // 8 words ...@@ -73,11 +70,11 @@ struct Aig_Obj_t_ // 8 words
Aig_Obj_t * pFanin0; // fanin Aig_Obj_t * pFanin0; // fanin
Aig_Obj_t * pFanin1; // fanin Aig_Obj_t * pFanin1; // fanin
Aig_Obj_t * pHaig; // pointer to the HAIG node Aig_Obj_t * pHaig; // pointer to the HAIG node
unsigned int Type : 4; // object type unsigned int Type : 3; // object type
unsigned int fPhase : 1; // value under 000...0 pattern unsigned int fPhase : 1; // value under 000...0 pattern
unsigned int fMarkA : 1; // multipurpose mask unsigned int fMarkA : 1; // multipurpose mask
unsigned int fMarkB : 1; // multipurpose mask unsigned int fMarkB : 1; // multipurpose mask
unsigned int nRefs : 25; // reference count unsigned int nRefs : 26; // reference count
unsigned Level : 24; // the level of this node unsigned Level : 24; // the level of this node
unsigned nCuts : 8; // the number of cuts unsigned nCuts : 8; // the number of cuts
int TravId; // unique ID of last traversal involving the node int TravId; // unique ID of last traversal involving the node
...@@ -89,16 +86,6 @@ struct Aig_Obj_t_ // 8 words ...@@ -89,16 +86,6 @@ struct Aig_Obj_t_ // 8 words
}; };
}; };
// the AIG box
struct Aig_Box_t_
{
int nInputs; // the number of box inputs (POs)
int i1Input; // the first PO of the interval
int nOutputs; // the number of box outputs (PIs)
int i1Output; // the first PI of the interval
float ** pTable; // the delay table of the box
};
// the AIG manager // the AIG manager
struct Aig_Man_t_ struct Aig_Man_t_
{ {
...@@ -154,7 +141,6 @@ struct Aig_Man_t_ ...@@ -154,7 +141,6 @@ struct Aig_Man_t_
Vec_Ptr_t * vMapped; Vec_Ptr_t * vMapped;
Vec_Int_t * vFlopNums; Vec_Int_t * vFlopNums;
void * pSeqModel; void * pSeqModel;
Aig_Man_t * pManHaig;
Aig_Man_t * pManExdc; Aig_Man_t * pManExdc;
Vec_Ptr_t * vOnehots; Vec_Ptr_t * vOnehots;
// timing statistics // timing statistics
...@@ -265,7 +251,6 @@ static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nO ...@@ -265,7 +251,6 @@ static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nO
static inline int Aig_ManBufNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_BUF]; } static inline int Aig_ManBufNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_BUF]; }
static inline int Aig_ManAndNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]; } static inline int Aig_ManAndNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]; }
static inline int Aig_ManExorNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_EXOR]; } static inline int Aig_ManExorNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManLatchNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_LATCH]; }
static inline int Aig_ManNodeNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+p->nObjs[AIG_OBJ_EXOR]; } static inline int Aig_ManNodeNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManGetCost( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; } static inline int Aig_ManGetCost( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; } static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; }
...@@ -289,10 +274,9 @@ static inline int Aig_ObjIsPo( Aig_Obj_t * pObj ) { return pObj- ...@@ -289,10 +274,9 @@ static inline int Aig_ObjIsPo( Aig_Obj_t * pObj ) { return pObj-
static inline int Aig_ObjIsBuf( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_BUF; } static inline int Aig_ObjIsBuf( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_BUF; }
static inline int Aig_ObjIsAnd( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND; } static inline int Aig_ObjIsAnd( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND; }
static inline int Aig_ObjIsExor( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_EXOR; } static inline int Aig_ObjIsExor( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_EXOR; }
static inline int Aig_ObjIsLatch( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_LATCH; }
static inline int Aig_ObjIsNode( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; } static inline int Aig_ObjIsNode( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; }
static inline int Aig_ObjIsTerm( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_PI || pObj->Type == AIG_OBJ_PO || pObj->Type == AIG_OBJ_CONST1; } static inline int Aig_ObjIsTerm( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_PI || pObj->Type == AIG_OBJ_PO || pObj->Type == AIG_OBJ_CONST1; }
static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR || pObj->Type == AIG_OBJ_LATCH; } static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; }
static inline int Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0; } static inline int Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0; }
static inline int Aig_ObjIsMarkA( Aig_Obj_t * pObj ) { return pObj->fMarkA; } static inline int Aig_ObjIsMarkA( Aig_Obj_t * pObj ) { return pObj->fMarkA; }
...@@ -405,6 +389,9 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry ) ...@@ -405,6 +389,9 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
// iterator over all nodes // iterator over all nodes
#define Aig_ManForEachNode( p, pObj, i ) \ #define Aig_ManForEachNode( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
// iterator over all nodes
#define Aig_ManForEachExor( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
// iterator over the nodes whose IDs are stored in the array // iterator over the nodes whose IDs are stored in the array
#define Aig_ManForEachNodeVec( p, vIds, pObj, i ) \ #define Aig_ManForEachNodeVec( p, vIds, pObj, i ) \
for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ ) for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
...@@ -458,6 +445,7 @@ extern Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLea ...@@ -458,6 +445,7 @@ extern Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLea
extern void Aig_ManCutStop( Aig_ManCut_t * p ); extern void Aig_ManCutStop( Aig_ManCut_t * p );
/*=== aigDfs.c ==========================================================*/ /*=== aigDfs.c ==========================================================*/
extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p );
extern Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ); extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p );
...@@ -514,7 +502,6 @@ extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_O ...@@ -514,7 +502,6 @@ extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_O
extern Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i ); extern Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i );
extern Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type ); extern Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type );
extern Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ); extern Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
extern Aig_Obj_t * Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne );
extern Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ); extern Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
extern Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ); extern Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
extern Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 ); extern Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 );
...@@ -565,8 +552,6 @@ extern int Aig_ManSeqCleanup( Aig_Man_t * p ); ...@@ -565,8 +552,6 @@ extern int Aig_ManSeqCleanup( Aig_Man_t * p );
extern int Aig_ManCountMergeRegs( Aig_Man_t * p ); extern int Aig_ManCountMergeRegs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ); extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
extern void Aig_ManComputeSccs( Aig_Man_t * p ); extern void Aig_ManComputeSccs( Aig_Man_t * p );
/*=== aigSeq.c ========================================================*/
extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
/*=== aigShow.c ========================================================*/ /*=== aigShow.c ========================================================*/
extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ); extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
/*=== aigTable.c ========================================================*/ /*=== aigTable.c ========================================================*/
......
src/aig/aig/aigCheck.c
...@@ -90,23 +90,23 @@ int Aig_ManCheck( Aig_Man_t * p ) ...@@ -90,23 +90,23 @@ int Aig_ManCheck( Aig_Man_t * p )
} }
// count the total number of nodes // count the total number of nodes
if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) +
Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) ) Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) )
{ {
printf( "Aig_ManCheck: The number of created nodes is wrong.\n" ); printf( "Aig_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", printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Total = %d.\n",
1, Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManBufNum(p), Aig_ManAndNum(p), Aig_ManExorNum(p), Aig_ManLatchNum(p), 1, Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManBufNum(p), Aig_ManAndNum(p), Aig_ManExorNum(p),
1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) ); 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) );
printf( "Created = %d. Deleted = %d. Existing = %d.\n", printf( "Created = %d. Deleted = %d. Existing = %d.\n",
p->nCreated, p->nDeleted, p->nCreated - p->nDeleted ); p->nCreated, p->nDeleted, p->nCreated - p->nDeleted );
return 0; return 0;
} }
// count the number of nodes in the table // count the number of nodes in the table
if ( Aig_TableCountEntries(p) != Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) ) if ( Aig_TableCountEntries(p) != Aig_ManAndNum(p) + Aig_ManExorNum(p) )
{ {
printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" ); printf( "Aig_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", printf( "Entries = %d. And = %d. Xor = %d. Total = %d.\n",
Aig_TableCountEntries(p), Aig_ManAndNum(p), Aig_ManExorNum(p), Aig_ManLatchNum(p), Aig_TableCountEntries(p), Aig_ManAndNum(p), Aig_ManExorNum(p),
Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) ); Aig_ManAndNum(p) + Aig_ManExorNum(p) );
return 0; return 0;
} }
......
src/aig/aig/aigDfs.c
...@@ -78,11 +78,6 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p ) ...@@ -78,11 +78,6 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
Aig_ManForEachPi( p, pObj, i ) Aig_ManForEachPi( p, pObj, i )
Aig_ObjSetTravIdCurrent( p, pObj ); Aig_ObjSetTravIdCurrent( p, pObj );
// if there are latches, mark them
if ( Aig_ManLatchNum(p) > 0 )
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjIsLatch(pObj) )
Aig_ObjSetTravIdCurrent( p, pObj );
// go through the nodes // go through the nodes
vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) ); vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
Aig_ManForEachObj( p, pObj, i ) Aig_ManForEachObj( p, pObj, i )
...@@ -93,6 +88,32 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p ) ...@@ -93,6 +88,32 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Levelizes the nodes
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
Vec_Vec_t * vLevels;
int nLevels, i;
nLevels = Aig_ManLevelNum( p );
vLevels = Vec_VecStart( nLevels + 1 );
Aig_ManForEachNode( p, pObj, i )
{
assert( (int)pObj->Level <= nLevels );
Vec_VecPush( vLevels, pObj->Level, pObj );
}
return vLevels;
}
/**Function*************************************************************
Synopsis [Collects internal nodes in the DFS order.] Synopsis [Collects internal nodes in the DFS order.]
Description [] Description []
...@@ -130,7 +151,6 @@ Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ) ...@@ -130,7 +151,6 @@ Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
Vec_Ptr_t * vNodes; Vec_Ptr_t * vNodes;
// Aig_Obj_t * pObj; // Aig_Obj_t * pObj;
int i; int i;
assert( Aig_ManLatchNum(p) == 0 );
Aig_ManIncrementTravId( p ); Aig_ManIncrementTravId( p );
// mark constant and PIs // mark constant and PIs
Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
...@@ -245,11 +265,6 @@ Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p ) ...@@ -245,11 +265,6 @@ Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p )
// mark POs // mark POs
Aig_ManForEachPo( p, pObj, i ) Aig_ManForEachPo( p, pObj, i )
Aig_ObjSetTravIdCurrent( p, pObj ); Aig_ObjSetTravIdCurrent( p, pObj );
// if there are latches, mark them
if ( Aig_ManLatchNum(p) > 0 )
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjIsLatch(pObj) )
Aig_ObjSetTravIdCurrent( p, pObj );
// go through the nodes // go through the nodes
vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) ); vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
Aig_ManForEachObj( p, pObj, i ) Aig_ManForEachObj( p, pObj, i )
......
src/aig/aig/aigMan.c
...@@ -102,6 +102,8 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ) ...@@ -102,6 +102,8 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
return pNew; return pNew;
} }
//#if 0
/**Function************************************************************* /**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.] Synopsis [Duplicates the AIG manager recursively.]
...@@ -122,7 +124,7 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) ...@@ -122,7 +124,7 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
if ( Aig_ObjIsBuf(pObj) ) if ( Aig_ObjIsBuf(pObj) )
return pObj->pData = Aig_ObjChild0Copy(pObj); return pObj->pData = Aig_ObjChild0Copy(pObj);
Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) ); Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig; Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
return pObj->pData = pObjNew; return pObj->pData = pObjNew;
} }
...@@ -148,7 +150,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) ...@@ -148,7 +150,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
pNew->pName = Aig_UtilStrsav( p->pName ); pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs; pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts; pNew->nAsserts = p->nAsserts;
pNew->pManHaig = p->pManHaig;
if ( p->vFlopNums ) if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// create the PIs // create the PIs
...@@ -164,7 +165,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) ...@@ -164,7 +165,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
} }
else if ( Aig_ObjIsNode(pObj) ) else if ( Aig_ObjIsNode(pObj) )
{ {
pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
} }
else if ( Aig_ObjIsPi(pObj) ) else if ( Aig_ObjIsPi(pObj) )
{ {
...@@ -187,6 +188,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) ...@@ -187,6 +188,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
} }
else else
{ {
/*
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig; Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachObj( p, pObj, i ) Aig_ManForEachObj( p, pObj, i )
...@@ -207,13 +210,73 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) ...@@ -207,13 +210,73 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
pObj->pData = pObjNew; pObj->pData = pObjNew;
} }
} }
*/
Vec_Vec_t * vLevels;
int k;
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachPi( p, pObj, i )
{
pObjNew = Aig_ObjCreatePi( pNew );
pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
} }
vLevels = Aig_ManLevelize( p );
Vec_VecForEachEntry( vLevels, pObj, i, k )
{
pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
Vec_VecFree( vLevels );
// add the POs // add the POs
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); Aig_ManForEachPo( p, pObj, i )
// pass the HAIG to the new AIG {
p->pManHaig = NULL; pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
/*
Aig_ManForEachObj( p, pObj, i ) Aig_ManForEachObj( p, pObj, i )
pObj->pHaig = NULL; {
if ( Aig_ObjIsPi(pObj) )
{
pObjNew = Aig_ObjCreatePi( pNew );
pObjNew->Level = pObj->Level;
}
else if ( Aig_ObjIsPo(pObj) )
{
// pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
}
else if ( Aig_ObjIsConst1(pObj) )
{
pObjNew = Aig_ManConst1(pNew);
}
else
{
pObjNew = Aig_ManDup_rec( pNew, p, pObj );
}
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
// add the POs
Aig_ManForEachPo( p, pObj, i )
{
pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
*/
}
// add the POs
// assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
// duplicate the timing manager // duplicate the timing manager
if ( p->pManTime ) if ( p->pManTime )
pNew->pManTime = Tim_ManDup( p->pManTime, 0 ); pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
...@@ -223,6 +286,117 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) ...@@ -223,6 +286,117 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
return pNew; return pNew;
} }
//#endif
#if 0
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pObjNew;
if ( pObj->pData )
return pObj->pData;
Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
if ( Aig_ObjIsBuf(pObj) )
return pObj->pData = Aig_ObjChild0Copy(pObj);
Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
return pObj->pData = pObjNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjNew;
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachPi( p, pObj, i )
{
pObjNew = Aig_ObjCreatePi( pNew );
pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
}
// duplicate internal nodes
if ( fOrdered )
{
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
{
pObj->pData = Aig_ObjChild0Copy(pObj);
}
else if ( Aig_ObjIsNode(pObj) )
{
pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
}
}
else
{
Aig_ManForEachObj( p, pObj, i )
if ( !Aig_ObjIsPo(pObj) )
{
Aig_ManDup_rec( pNew, p, pObj );
assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
}
}
// add the POs
Aig_ManForEachPo( p, pObj, i )
{
pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
/*
printf( "PIs : " );
Aig_ManForEachPi( p, pObj, i )
printf( "%d ", pObj->Id );
printf( "\n" );
printf( "PIs : " );
Aig_ManForEachPo( p, pObj, i )
printf( "%d ", pObj->Id );
printf( "\n" );
*/
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDup(): The check has failed.\n" );
return pNew;
}
#endif
/**Function************************************************************* /**Function*************************************************************
Synopsis [Duplicates the AIG manager.] Synopsis [Duplicates the AIG manager.]
...@@ -252,7 +426,7 @@ Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p ) ...@@ -252,7 +426,7 @@ Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
{ {
assert( !Aig_ObjIsBuf(pObj) ); assert( !Aig_ObjIsBuf(pObj) );
if ( Aig_ObjIsNode(pObj) ) if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
} }
return pNew; return pNew;
} }
...@@ -311,8 +485,6 @@ void Aig_ManStop( Aig_Man_t * p ) ...@@ -311,8 +485,6 @@ void Aig_ManStop( Aig_Man_t * p )
{ {
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int i; int i;
if ( p->pManHaig )
Aig_ManStop( p->pManHaig );
if ( p->vMapped ) if ( p->vMapped )
Vec_PtrFree( p->vMapped ); Vec_PtrFree( p->vMapped );
// print time // print time
...@@ -412,7 +584,7 @@ int Aig_ManHaigCounter( Aig_Man_t * pAig ) ...@@ -412,7 +584,7 @@ int Aig_ManHaigCounter( Aig_Man_t * pAig )
void Aig_ManPrintStats( Aig_Man_t * p ) void Aig_ManPrintStats( Aig_Man_t * p )
{ {
int nChoices = Aig_ManCountChoices(p); int nChoices = Aig_ManCountChoices(p);
printf( "PI/PO/Lat = %5d/%5d/%5d ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) ); printf( "PI/PO = %5d/%5d ", Aig_ManPiNum(p), Aig_ManPoNum(p) );
printf( "A = %7d. ", Aig_ManAndNum(p) ); printf( "A = %7d. ", Aig_ManAndNum(p) );
printf( "Eq = %7d. ", Aig_ManHaigCounter(p) ); printf( "Eq = %7d. ", Aig_ManHaigCounter(p) );
if ( nChoices ) if ( nChoices )
......
src/aig/aig/aigObj.c
...@@ -88,7 +88,7 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost ) ...@@ -88,7 +88,7 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
assert( !Aig_IsComplement(pGhost) ); assert( !Aig_IsComplement(pGhost) );
assert( Aig_ObjIsHash(pGhost) ); assert( Aig_ObjIsHash(pGhost) );
// assert( pGhost == &p->Ghost ); assert( pGhost == &p->Ghost );
// get memory for the new object // get memory for the new object
pObj = Aig_ManFetchMemory( p ); pObj = Aig_ManFetchMemory( p );
pObj->Type = pGhost->Type; pObj->Type = pGhost->Type;
...@@ -97,14 +97,6 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost ) ...@@ -97,14 +97,6 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
// update node counters of the manager // update node counters of the manager
p->nObjs[Aig_ObjType(pObj)]++; p->nObjs[Aig_ObjType(pObj)]++;
assert( pObj->pData == NULL ); assert( pObj->pData == NULL );
/*
if ( p->pManHaig )
{
pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 );
pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 );
pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost );
}
*/
return pObj; return pObj;
} }
...@@ -374,13 +366,6 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in ...@@ -374,13 +366,6 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
// make sure object is not pointing to itself // make sure object is not pointing to itself
assert( pObjOld != Aig_ObjFanin0(pObjNewR) ); assert( pObjOld != Aig_ObjFanin0(pObjNewR) );
assert( pObjOld != Aig_ObjFanin1(pObjNewR) ); assert( pObjOld != Aig_ObjFanin1(pObjNewR) );
// map the HAIG nodes
if ( p->pManHaig != NULL )
{
assert( pObjNewR->pHaig != NULL );
assert( pObjNewR->pHaig->pHaig == NULL );
pObjNewR->pHaig->pHaig = pObjOld->pHaig;
}
// recursively delete the old node - but leave the object there // recursively delete the old node - but leave the object there
pObjNewR->nRefs++; pObjNewR->nRefs++;
Aig_ObjDelete_rec( p, pObjOld, 0 ); Aig_ObjDelete_rec( p, pObjOld, 0 );
......
src/aig/aig/aigOper.c
...@@ -89,43 +89,6 @@ Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t ...@@ -89,43 +89,6 @@ Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t
/**Function************************************************************* /**Function*************************************************************
Synopsis [Creates the canonical form of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_CanonPair_rec( Aig_Man_t * p, Aig_Obj_t * pGhost )
{
Aig_Obj_t * pResult, * pLat0, * pLat1;
int fCompl0, fCompl1;
Aig_Type_t Type;
assert( Aig_ObjIsNode(pGhost) );
// consider the case when the pair is canonical
if ( !Aig_ObjIsLatch(Aig_ObjFanin0(pGhost)) || !Aig_ObjIsLatch(Aig_ObjFanin1(pGhost)) )
{
if ( (pResult = Aig_TableLookup( p, pGhost )) )
return pResult;
return Aig_ObjCreate( p, pGhost );
}
/// remember the latches
pLat0 = Aig_ObjFanin0(pGhost);
pLat1 = Aig_ObjFanin1(pGhost);
// remember type and compls
Type = Aig_ObjType(pGhost);
fCompl0 = Aig_ObjFaninC0(pGhost);
fCompl1 = Aig_ObjFaninC1(pGhost);
// call recursively
pResult = Aig_Oper( p, Aig_NotCond(Aig_ObjChild0(pLat0), fCompl0), Aig_NotCond(Aig_ObjChild0(pLat1), fCompl1), Type );
// build latch on top of this
return Aig_Latch( p, pResult, (Type == AIG_OBJ_AND)? fCompl0 & fCompl1 : fCompl0 ^ fCompl1 );
}
/**Function*************************************************************
Synopsis [Performs canonicization step.] Synopsis [Performs canonicization step.]
Description [The argument nodes can be complemented.] Description [The argument nodes can be complemented.]
...@@ -138,16 +101,7 @@ Aig_Obj_t * Aig_CanonPair_rec( Aig_Man_t * p, Aig_Obj_t * pGhost ) ...@@ -138,16 +101,7 @@ Aig_Obj_t * Aig_CanonPair_rec( Aig_Man_t * p, Aig_Obj_t * pGhost )
Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ) Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
{ {
Aig_Obj_t * pGhost, * pResult; Aig_Obj_t * pGhost, * pResult;
// Aig_Obj_t * pFan0, * pFan1; Aig_Obj_t * pFan0, * pFan1;
if ( p->pTable == NULL )
{
// pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND );
pGhost = Aig_ManGhost(p);
pGhost->Type = AIG_OBJ_AND;
pGhost->pFanin0 = p0;
pGhost->pFanin1 = p1;
return Aig_ObjCreate( p, pGhost );
}
// check trivial cases // check trivial cases
if ( p0 == p1 ) if ( p0 == p1 )
return p0; return p0;
...@@ -241,32 +195,12 @@ Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ) ...@@ -241,32 +195,12 @@ Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
} }
} }
// check if it can be an EXOR gate // check if it can be an EXOR gate
// if ( Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) ) if ( p->fCatchExor && Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
// return Aig_Exor( p, pFan0, pFan1 ); return Aig_Exor( p, pFan0, pFan1 );
pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND ); pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND );
pResult = Aig_CanonPair_rec( p, pGhost ); if ( (pResult = Aig_TableLookup( p, pGhost )) )
return pResult; return pResult;
} return Aig_ObjCreate( p, pGhost );
/**Function*************************************************************
Synopsis [Creates the canonical form of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne )
{
Aig_Obj_t * pGhost, * pResult;
pGhost = Aig_ObjCreateGhost( p, Aig_NotCond(pObj, fInitOne), NULL, AIG_OBJ_LATCH );
pResult = Aig_TableLookup( p, pGhost );
if ( pResult == NULL )
pResult = Aig_ObjCreate( p, pGhost );
return Aig_NotCond( pResult, fInitOne );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -282,8 +216,8 @@ Aig_Obj_t * Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne ) ...@@ -282,8 +216,8 @@ Aig_Obj_t * Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne )
***********************************************************************/ ***********************************************************************/
Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ) Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
{ {
/*
Aig_Obj_t * pGhost, * pResult; Aig_Obj_t * pGhost, * pResult;
int fCompl;
// check trivial cases // check trivial cases
if ( p0 == p1 ) if ( p0 == p1 )
return Aig_Not(p->pConst1); return Aig_Not(p->pConst1);
...@@ -293,13 +227,19 @@ Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ) ...@@ -293,13 +227,19 @@ Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
return Aig_NotCond( p1, p0 == p->pConst1 ); return Aig_NotCond( p1, p0 == p->pConst1 );
if ( Aig_Regular(p1) == p->pConst1 ) if ( Aig_Regular(p1) == p->pConst1 )
return Aig_NotCond( p0, p1 == p->pConst1 ); return Aig_NotCond( p0, p1 == p->pConst1 );
// check the table // when there is no special XOR gates
if ( !p->fCatchExor )
return Aig_Or( p, Aig_And(p, p0, Aig_Not(p1)), Aig_And(p, Aig_Not(p0), p1) );
// canonicize
fCompl = Aig_IsComplement(p0) ^ Aig_IsComplement(p1);
p0 = Aig_Regular(p0);
p1 = Aig_Regular(p1);
pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_EXOR ); pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_EXOR );
// check the table
if ( pResult = Aig_TableLookup( p, pGhost ) ) if ( pResult = Aig_TableLookup( p, pGhost ) )
return pResult; return Aig_NotCond( pResult, fCompl );
return Aig_ObjCreate( p, pGhost ); pResult = Aig_ObjCreate( p, pGhost );
*/ return Aig_NotCond( pResult, fCompl );
return Aig_Or( p, Aig_And(p, p0, Aig_Not(p1)), Aig_And(p, Aig_Not(p0), p1) );
} }
/**Function************************************************************* /**Function*************************************************************
......
src/aig/aig/aigRetF.c
...@@ -178,18 +178,6 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax ) ...@@ -178,18 +178,6 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
p->nObjs[AIG_OBJ_BUF]++; p->nObjs[AIG_OBJ_BUF]++;
Aig_ObjConnect( p, pObj, Aig_NotCond(pObjLo, fCompl), NULL ); Aig_ObjConnect( p, pObj, Aig_NotCond(pObjLo, fCompl), NULL );
// create HAIG if defined // create HAIG if defined
/*
if ( p->pManHaig )
{
// create HAIG latch
pObjLo->pHaig = Aig_ObjCreatePi( p->pManHaig );
pObjLi->pHaig = Aig_ObjCreatePo( p->pManHaig, Aig_ObjHaig( Aig_ObjChild0(pObjLi) ) );
// create equivalence class
assert( pObjLo->pHaig != NULL );
assert( pObjLo->pHaig->pHaig == NULL );
pObjLo->pHaig->pHaig = Aig_Regular(pObj->pHaig);
}
*/
// mark the change // mark the change
fChange = 1; fChange = 1;
// check the limit // check the limit
......
src/aig/aig/aigShow.c
...@@ -170,7 +170,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * ...@@ -170,7 +170,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
*/ */
fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
fprintf( pFile, ", shape = %s", (Aig_ObjIsLatch(pNode)? "box":"invtriangle") ); fprintf( pFile, ", shape = %s", "invtriangle" );
fprintf( pFile, ", color = coral, fillcolor = coral" ); fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" ); fprintf( pFile, "];\n" );
} }
...@@ -237,7 +237,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * ...@@ -237,7 +237,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
*/ */
fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
fprintf( pFile, ", shape = %s", (Aig_ObjIsLatch(pNode)? "box":"triangle") ); fprintf( pFile, ", shape = %s", "triangle" );
fprintf( pFile, ", color = coral, fillcolor = coral" ); fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" ); fprintf( pFile, "];\n" );
} }
...@@ -248,7 +248,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * ...@@ -248,7 +248,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
// generate invisible edges from the square down // generate invisible edges from the square down
fprintf( pFile, "title1 -> title2 [style = invis];\n" ); fprintf( pFile, "title1 -> title2 [style = invis];\n" );
Aig_ManForEachPo( pMan, pNode, i ) Aig_ManForEachPo( pMan, pNode, i )
fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":"") ); fprintf( pFile, "title2 -> Node%d [style = invis];\n", pNode->Id );
// generate edges // generate edges
Aig_ManForEachObj( pMan, pNode, i ) Aig_ManForEachObj( pMan, pNode, i )
...@@ -256,9 +256,9 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * ...@@ -256,9 +256,9 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
if ( !Aig_ObjIsNode(pNode) && !Aig_ObjIsPo(pNode) && !Aig_ObjIsBuf(pNode) ) if ( !Aig_ObjIsNode(pNode) && !Aig_ObjIsPo(pNode) && !Aig_ObjIsBuf(pNode) )
continue; continue;
// generate the edge from this node to the next // generate the edge from this node to the next
fprintf( pFile, "Node%d%s", pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":"") ); fprintf( pFile, "Node%d", pNode->Id );
fprintf( pFile, " -> " ); fprintf( pFile, " -> " );
fprintf( pFile, "Node%d%s", Aig_ObjFaninId0(pNode), (Aig_ObjIsLatch(Aig_ObjFanin0(pNode))? "_out":"") ); fprintf( pFile, "Node%d", Aig_ObjFaninId0(pNode) );
fprintf( pFile, " [" ); fprintf( pFile, " [" );
fprintf( pFile, "style = %s", Aig_ObjFaninC0(pNode)? "dotted" : "bold" ); fprintf( pFile, "style = %s", Aig_ObjFaninC0(pNode)? "dotted" : "bold" );
// if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 ) // if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 )
...@@ -270,7 +270,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * ...@@ -270,7 +270,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
// generate the edge from this node to the next // generate the edge from this node to the next
fprintf( pFile, "Node%d", pNode->Id ); fprintf( pFile, "Node%d", pNode->Id );
fprintf( pFile, " -> " ); fprintf( pFile, " -> " );
fprintf( pFile, "Node%d%s", Aig_ObjFaninId1(pNode), (Aig_ObjIsLatch(Aig_ObjFanin1(pNode))? "_out":"") ); fprintf( pFile, "Node%d", Aig_ObjFaninId1(pNode) );
fprintf( pFile, " [" ); fprintf( pFile, " [" );
fprintf( pFile, "style = %s", Aig_ObjFaninC1(pNode)? "dotted" : "bold" ); fprintf( pFile, "style = %s", Aig_ObjFaninC1(pNode)? "dotted" : "bold" );
// if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 ) // if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 )
......
src/aig/aig/aigTable.c
...@@ -39,15 +39,8 @@ static unsigned long Aig_Hash( Aig_Obj_t * pObj, int TableSize ) ...@@ -39,15 +39,8 @@ static unsigned long Aig_Hash( Aig_Obj_t * pObj, int TableSize )
static Aig_Obj_t ** Aig_TableFind( Aig_Man_t * p, Aig_Obj_t * pObj ) static Aig_Obj_t ** Aig_TableFind( Aig_Man_t * p, Aig_Obj_t * pObj )
{ {
Aig_Obj_t ** ppEntry; Aig_Obj_t ** ppEntry;
if ( Aig_ObjIsLatch(pObj) )
{
assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) == NULL );
}
else
{
assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) ); assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) );
assert( Aig_ObjFanin0(pObj)->Id < Aig_ObjFanin1(pObj)->Id ); assert( Aig_ObjFanin0(pObj)->Id < Aig_ObjFanin1(pObj)->Id );
}
for ( ppEntry = p->pTable + Aig_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext ) for ( ppEntry = p->pTable + Aig_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext )
if ( *ppEntry == pObj ) if ( *ppEntry == pObj )
return ppEntry; return ppEntry;
...@@ -119,20 +112,11 @@ Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost ) ...@@ -119,20 +112,11 @@ Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost )
{ {
Aig_Obj_t * pEntry; Aig_Obj_t * pEntry;
assert( !Aig_IsComplement(pGhost) ); assert( !Aig_IsComplement(pGhost) );
if ( pGhost->Type == AIG_OBJ_LATCH ) assert( Aig_ObjIsNode(pGhost) );
{
assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) == NULL );
if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) )
return NULL;
}
else
{
assert( pGhost->Type == AIG_OBJ_AND );
assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) ); assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) );
assert( Aig_ObjFanin0(pGhost)->Id < Aig_ObjFanin1(pGhost)->Id ); assert( Aig_ObjFanin0(pGhost)->Id < Aig_ObjFanin1(pGhost)->Id );
if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost)) ) if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost)) )
return NULL; return NULL;
}
for ( pEntry = p->pTable[Aig_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext ) for ( pEntry = p->pTable[Aig_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
{ {
if ( Aig_ObjChild0(pEntry) == Aig_ObjChild0(pGhost) && if ( Aig_ObjChild0(pEntry) == Aig_ObjChild0(pGhost) &&
...@@ -184,8 +168,6 @@ Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * ...@@ -184,8 +168,6 @@ Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t *
void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj ) void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
{ {
Aig_Obj_t ** ppPlace; Aig_Obj_t ** ppPlace;
if ( p->pTable == NULL )
return;
assert( !Aig_IsComplement(pObj) ); assert( !Aig_IsComplement(pObj) );
assert( Aig_TableLookup(p, pObj) == NULL ); assert( Aig_TableLookup(p, pObj) == NULL );
if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Aig_ManNodeNum(p) ) if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Aig_ManNodeNum(p) )
...@@ -209,8 +191,6 @@ void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj ) ...@@ -209,8 +191,6 @@ void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj ) void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
{ {
Aig_Obj_t ** ppPlace; Aig_Obj_t ** ppPlace;
if ( p->pTable == NULL )
return;
assert( !Aig_IsComplement(pObj) ); assert( !Aig_IsComplement(pObj) );
ppPlace = Aig_TableFind( p, pObj ); ppPlace = Aig_TableFind( p, pObj );
assert( *ppPlace == pObj ); // node should be in the table assert( *ppPlace == pObj ); // node should be in the table
......
src/aig/aig/module.make
...@@ -16,7 +16,6 @@ SRC += src/aig/aig/aigCheck.c \ ...@@ -16,7 +16,6 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigRet.c \ src/aig/aig/aigRet.c \
src/aig/aig/aigRetF.c \ src/aig/aig/aigRetF.c \
src/aig/aig/aigScl.c \ src/aig/aig/aigScl.c \
src/aig/aig/aigSeq.c \
src/aig/aig/aigShow.c \ src/aig/aig/aigShow.c \
src/aig/aig/aigTable.c \ src/aig/aig/aigTable.c \
src/aig/aig/aigTiming.c \ src/aig/aig/aigTiming.c \
......
src/aig/dar/darScript.c
...@@ -201,14 +201,6 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i ...@@ -201,14 +201,6 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig ); if ( fVerbose ) Aig_ManPrintStats( pAig );
// balance
if ( fBalance )
{
pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
}
return pAig; return pAig;
} }
......
src/aig/fra/fraCore.c
...@@ -371,7 +371,6 @@ Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars ) ...@@ -371,7 +371,6 @@ Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
if ( Aig_ManNodeNum(pManAig) == 0 ) if ( Aig_ManNodeNum(pManAig) == 0 )
return Aig_ManDup(pManAig, 1); return Aig_ManDup(pManAig, 1);
clk = clock(); clk = clock();
assert( Aig_ManLatchNum(pManAig) == 0 );
p = Fra_ManStart( pManAig, pPars ); p = Fra_ManStart( pManAig, pPars );
p->pManFraig = Fra_ManPrepareComb( p ); p->pManFraig = Fra_ManPrepareComb( p );
p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords ); p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
......
src/aig/fra/fraInd.c
...@@ -344,7 +344,6 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams ) ...@@ -344,7 +344,6 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
pParams->nIters = 0; pParams->nIters = 0;
return Aig_ManDup(pManAig, 1); return Aig_ManDup(pManAig, 1);
} }
assert( Aig_ManLatchNum(pManAig) == 0 );
assert( Aig_ManRegNum(pManAig) > 0 ); assert( Aig_ManRegNum(pManAig) > 0 );
assert( pParams->nFramesK > 0 ); assert( pParams->nFramesK > 0 );
//Aig_ManShow( pManAig, 0, NULL ); //Aig_ManShow( pManAig, 0, NULL );
......
src/aig/fra/fraLcr.c
...@@ -516,7 +516,6 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC ...@@ -516,7 +516,6 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
if ( pnIter ) *pnIter = 0; if ( pnIter ) *pnIter = 0;
return Aig_ManDup(pAig, 1); return Aig_ManDup(pAig, 1);
} }
assert( Aig_ManLatchNum(pAig) == 0 );
assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManRegNum(pAig) > 0 );
// simulate the AIG // simulate the AIG
......
src/aig/hop/hopTruth.c
...@@ -176,8 +176,10 @@ unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars ...@@ -176,8 +176,10 @@ unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars
// assert( Hop_ManPiNum(p) <= 8 ); // assert( Hop_ManPiNum(p) <= 8 );
if ( fMsbFirst ) if ( fMsbFirst )
{ {
Hop_ManForEachPi( p, pObj, i ) // Hop_ManForEachPi( p, pObj, i )
for ( i = 0; i < nVars; i++ )
{ {
pObj = Hop_ManPi( p, i );
if ( vTtElems ) if ( vTtElems )
pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i); pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
else else
...@@ -186,8 +188,10 @@ unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars ...@@ -186,8 +188,10 @@ unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars
} }
else else
{ {
Hop_ManForEachPi( p, pObj, i ) // Hop_ManForEachPi( p, pObj, i )
for ( i = 0; i < nVars; i++ )
{ {
pObj = Hop_ManPi( p, i );
if ( vTtElems ) if ( vTtElems )
pObj->pData = Vec_PtrEntry(vTtElems, i); pObj->pData = Vec_PtrEntry(vTtElems, i);
else else
......
src/base/abci/abc.c
...@@ -2255,6 +2255,9 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2255,6 +2255,9 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
bool fDuplicate; bool fDuplicate;
bool fSelective; bool fSelective;
bool fUpdateLevel; bool fUpdateLevel;
int fExor;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
...@@ -2264,8 +2267,10 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2264,8 +2267,10 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
fDuplicate = 0; fDuplicate = 0;
fSelective = 0; fSelective = 0;
fUpdateLevel = 1; fUpdateLevel = 1;
fExor = 0;
fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ldsh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "ldsxvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -2278,6 +2283,12 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2278,6 +2283,12 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's': case 's':
fSelective ^= 1; fSelective ^= 1;
break; break;
case 'x':
fExor ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h': case 'h':
goto usage; goto usage;
default: default:
...@@ -2293,6 +2304,9 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2293,6 +2304,9 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network // get the new network
if ( Abc_NtkIsStrash(pNtk) ) if ( Abc_NtkIsStrash(pNtk) )
{ {
if ( fExor )
pNtkRes = Abc_NtkBalanceExor( pNtk, fUpdateLevel, fVerbose );
else
pNtkRes = Abc_NtkBalance( pNtk, fDuplicate, fSelective, fUpdateLevel ); pNtkRes = Abc_NtkBalance( pNtk, fDuplicate, fSelective, fUpdateLevel );
} }
else else
...@@ -2303,6 +2317,9 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2303,6 +2317,9 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Strashing before balancing has failed.\n" ); fprintf( pErr, "Strashing before balancing has failed.\n" );
return 1; return 1;
} }
if ( fExor )
pNtkRes = Abc_NtkBalanceExor( pNtkTemp, fUpdateLevel, fVerbose );
else
pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate, fSelective, fUpdateLevel ); pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate, fSelective, fUpdateLevel );
Abc_NtkDelete( pNtkTemp ); Abc_NtkDelete( pNtkTemp );
} }
...@@ -2318,11 +2335,13 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2318,11 +2335,13 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: balance [-ldsh]\n" ); fprintf( pErr, "usage: balance [-ldsxvh]\n" );
fprintf( pErr, "\t transforms the current network into a well-balanced AIG\n" ); fprintf( pErr, "\t transforms the current network into a well-balanced AIG\n" );
fprintf( pErr, "\t-l : toggle minimizing the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); fprintf( pErr, "\t-l : toggle minimizing the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
fprintf( pErr, "\t-d : toggle duplication of logic [default = %s]\n", fDuplicate? "yes": "no" ); fprintf( pErr, "\t-d : toggle duplication of logic [default = %s]\n", fDuplicate? "yes": "no" );
fprintf( pErr, "\t-s : toggle duplication on the critical paths [default = %s]\n", fSelective? "yes": "no" ); fprintf( pErr, "\t-s : toggle duplication on the critical paths [default = %s]\n", fSelective? "yes": "no" );
fprintf( pErr, "\t-x : toggle balancing multi-input EXORs [default = %s]\n", fExor? "yes": "no" );
fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-h : print the command usage\n");
return 1; return 1;
} }
...@@ -7085,6 +7104,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -7085,6 +7104,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ); // extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
// extern void Abc_NtkDarTestBlif( char * pFileName ); // extern void Abc_NtkDarTestBlif( char * pFileName );
// extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
...@@ -7269,7 +7290,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -7269,7 +7290,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_NtkDarPartition( pNtk ); // Abc_NtkDarPartition( pNtk );
/* /*
pNtkRes = Abc_NtkDarPartition( pNtk ); pNtkRes = Abc_NtkTestExor( pNtk, 0 );
if ( pNtkRes == NULL ) if ( pNtkRes == NULL )
{ {
fprintf( pErr, "Command has failed.\n" ); fprintf( pErr, "Command has failed.\n" );
...@@ -13363,7 +13384,6 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -13363,7 +13384,6 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames ); extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames );
extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ); extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
extern void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
pNtk = Abc_FrameReadNtk(pAbc); pNtk = Abc_FrameReadNtk(pAbc);
...@@ -13453,9 +13473,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -13453,9 +13473,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
// perform equivalence checking // perform equivalence checking
if ( fRetime ) if ( fSat )
Abc_NtkSecRetime( pNtk1, pNtk2 );
else if ( fSat )
Abc_NtkSecSat( pNtk1, pNtk2, nConfLimit, nInsLimit, nFrames ); Abc_NtkSecSat( pNtk1, pNtk2, nConfLimit, nInsLimit, nFrames );
else else
Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose ); Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose );
......
src/opt/mfs/mfsCore.c
...@@ -180,11 +180,22 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) ...@@ -180,11 +180,22 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
assert( Abc_NtkIsLogic(pNtk) ); assert( Abc_NtkIsLogic(pNtk) );
nFaninMax = Abc_NtkGetFaninMax(pNtk); nFaninMax = Abc_NtkGetFaninMax(pNtk);
if ( pPars->fResub )
{
if ( nFaninMax > 8 )
{
printf( "Nodes with more than %d fanins will node be processed.\n", 8 );
nFaninMax = 8;
}
}
else
{
if ( nFaninMax > MFS_FANIN_MAX ) if ( nFaninMax > MFS_FANIN_MAX )
{ {
printf( "Nodes with more than %d fanins will node be processed.\n", MFS_FANIN_MAX ); printf( "Nodes with more than %d fanins will node be processed.\n", MFS_FANIN_MAX );
nFaninMax = MFS_FANIN_MAX; nFaninMax = MFS_FANIN_MAX;
} }
}
// perform the network sweep // perform the network sweep
Abc_NtkSweep( pNtk, 0 ); Abc_NtkSweep( pNtk, 0 );
// convert into the AIG // convert into the AIG
...@@ -237,6 +248,26 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) ...@@ -237,6 +248,26 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
nNodes = 0; nNodes = 0;
p->nTotalNodesBeg = nTotalNodesBeg; p->nTotalNodesBeg = nTotalNodesBeg;
p->nTotalEdgesBeg = nTotalEdgesBeg; p->nTotalEdgesBeg = nTotalEdgesBeg;
if ( pPars->fResub )
{
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachNode( pNtk, pObj, i )
{
if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
continue;
if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
continue;
if ( !p->pPars->fVeryVerbose )
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( pPars->fResub )
Abc_NtkMfsResub( p, pObj );
else
Abc_NtkMfsNode( p, pObj );
}
Extra_ProgressBarStop( pProgress );
}
else
{
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) ); pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
vLevels = Abc_NtkLevelize( pNtk ); vLevels = Abc_NtkLevelize( pNtk );
Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 ) Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
...@@ -251,17 +282,17 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) ...@@ -251,17 +282,17 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{ {
if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax ) if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
break; break;
if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX ) if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
continue; continue;
if ( pPars->fResub ) if ( pPars->fResub )
Abc_NtkMfsResub( p, pObj ); Abc_NtkMfsResub( p, pObj );
else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 ) else
Abc_NtkMfsNode( p, pObj ); Abc_NtkMfsNode( p, pObj );
} }
nNodes += Vec_PtrSize(vNodes); nNodes += Vec_PtrSize(vNodes);
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
printf( "Lev = %2d. Node = %4d. Ave gain = %6.2f. Ave conf = %6.2f. Timeouts = %6.2f %% ", printf( "Lev = %2d. Node = %5d. Ave gain = %5.2f. Ave conf = %5.2f. T/o = %6.2f %% ",
k, Vec_PtrSize(vNodes), k, Vec_PtrSize(vNodes),
1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes), 1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
1.0*p->nTotConfLevel/Vec_PtrSize(vNodes), 1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
...@@ -270,8 +301,9 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) ...@@ -270,8 +301,9 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
} }
} }
Extra_ProgressBarStop( pProgress ); Extra_ProgressBarStop( pProgress );
Abc_NtkStopReverseLevels( pNtk );
Vec_VecFree( vLevels ); Vec_VecFree( vLevels );
}
Abc_NtkStopReverseLevels( pNtk );
// perform the sweeping // perform the sweeping
if ( !pPars->fResub ) if ( !pPars->fResub )
......
src/opt/mfs/mfsResub.c
...@@ -176,6 +176,7 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f ...@@ -176,6 +176,7 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
if ( fVeryVerbose ) if ( fVeryVerbose )
printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin ); printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
p->nNodesResub++; p->nNodesResub++;
p->nNodesGainedLevel++;
if ( fSkipUpdate ) if ( fSkipUpdate )
return 1; return 1;
clk = clock(); clk = clock();
...@@ -243,6 +244,7 @@ p->timeInt += clock() - clk; ...@@ -243,6 +244,7 @@ p->timeInt += clock() - clk;
if ( fVeryVerbose ) if ( fVeryVerbose )
printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar ); printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
p->nNodesResub++; p->nNodesResub++;
p->nNodesGainedLevel++;
if ( fSkipUpdate ) if ( fSkipUpdate )
return 1; return 1;
clk = clock(); clk = clock();
...@@ -315,6 +317,7 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int ...@@ -315,6 +317,7 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
if ( fVeryVerbose ) if ( fVeryVerbose )
printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 ); printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
p->nNodesResub++; p->nNodesResub++;
p->nNodesGainedLevel++;
clk = clock(); clk = clock();
// derive the function // derive the function
pFunc = Abc_NtkMfsInterplate( p, pCands, nCands ); pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
...@@ -388,6 +391,7 @@ p->timeInt += clock() - clk; ...@@ -388,6 +391,7 @@ p->timeInt += clock() - clk;
if ( fVeryVerbose ) if ( fVeryVerbose )
printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 ); printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
p->nNodesResub++; p->nNodesResub++;
p->nNodesGainedLevel++;
clk = clock(); clk = clock();
// derive the function // derive the function
pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 ); pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment