diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-08-24 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-08-24 08:01:00 -0700 |
| commit | 735bca1658f92881e12a616f9bdc6a58d0a4c60b (patch) | |
| tree | bf38d65e91be84e4086b585c489411876750f041 /src | |
| parent | 7b09d2d28aa81916f9c06f0993f2569a7ad18596 (diff) | |
| download | abc-735bca1658f92881e12a616f9bdc6a58d0a4c60b.tar.gz abc-735bca1658f92881e12a616f9bdc6a58d0a4c60b.tar.bz2 abc-735bca1658f92881e12a616f9bdc6a58d0a4c60b.zip | |
Version abc60824
Diffstat (limited to 'src')
47 files changed, 827 insertions, 2703 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index e106d5eb..1a3f3264 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -90,12 +90,14 @@ typedef enum { ABC_OBJ_PO, // 4: primary output terminal ABC_OBJ_BI, // 5: box input terminal ABC_OBJ_BO, // 6: box output terminal - ABC_OBJ_ASSERT, // 7: assertion output + ABC_OBJ_ASSERT, // 7: assertion terminal ABC_OBJ_NET, // 8: net ABC_OBJ_NODE, // 9: node - ABC_OBJ_LATCH, // 10: latch - ABC_OBJ_BOX, // 11: box - ABC_OBJ_NUMBER // 12: unused + ABC_OBJ_GATE, // 10: mapped node + ABC_OBJ_LATCH, // 11: latch + ABC_OBJ_TRI, // 12: tristate element + ABC_OBJ_BLACKBOX, // 13: box with unknown contents + ABC_OBJ_NUMBER // 14: unused } Abc_ObjType_t; // latch initial values @@ -138,6 +140,7 @@ struct Abc_Obj_t_ // 12 words // high-level information Abc_Ntk_t * pNtk; // the host network int Id; // the object ID + int TravId; // the traversal ID (if changed, update Abc_NtkIncrementTravId) // internal information unsigned Type : 4; // the object type unsigned fMarkA : 1; // the multipurpose mark @@ -148,8 +151,7 @@ struct Abc_Obj_t_ // 12 words unsigned fPersist: 1; // marks the persistant AIG node unsigned fCompl0 : 1; // complemented attribute of the first fanin in the AIG unsigned fCompl1 : 1; // complemented attribute of the second fanin in the AIG - unsigned TravId : 8; // the traversal ID (if changed, update Abc_NtkIncrementTravId) - unsigned Level : 12; // the level of the node + unsigned Level : 20; // the level of the node // connectivity Vec_Int_t vFanins; // the array of fanins Vec_Int_t vFanouts; // the array of fanouts @@ -169,12 +171,11 @@ struct Abc_Ntk_t_ Nm_Man_t * pManName; // name manager (stores names of objects) // components of the network Vec_Ptr_t * vObjs; // the array of all objects (net, nodes, latches, etc) + Vec_Ptr_t * vPis; // the array of primary inputs + Vec_Ptr_t * vPos; // the array of primary outputs Vec_Ptr_t * vCis; // the array of combinational inputs (PIs, latches) Vec_Ptr_t * vCos; // the array of combinational outputs (POs, asserts, latches) - Vec_Ptr_t * vPis; // the array of PIs - Vec_Ptr_t * vPos; // the array of POs Vec_Ptr_t * vPios; // the array of PIOs - Vec_Ptr_t * vLatches; // the array of latches (or the cutset in the sequential network) Vec_Ptr_t * vAsserts; // the array of assertions Vec_Ptr_t * vBoxes; // the array of boxes Vec_Ptr_t * vCutSet; // the array of cutset nodes (used in the sequential AIG) @@ -190,7 +191,7 @@ struct Abc_Ntk_t_ short fHieVisited; // flag to mark the visited network short fHiePath; // flag to mark the network on the path // miscellaneous data members - unsigned nTravIds; // the unique traversal IDs of nodes + int nTravIds; // the unique traversal IDs of nodes Extra_MmFixed_t * pMmObj; // memory manager for objects Extra_MmStep_t * pMmStep; // memory manager for arrays void * pManFunc; // functionality manager (AIG manager, BDD manager, or memory manager for SOPs) @@ -257,7 +258,6 @@ static inline bool Abc_NtkIsSopLogic( Abc_Ntk_t * pNtk ) { return pN static inline bool Abc_NtkIsBddLogic( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_BDD && pNtk->ntkType == ABC_NTK_LOGIC ; } static inline bool Abc_NtkIsAigLogic( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_AIG && pNtk->ntkType == ABC_NTK_LOGIC ; } static inline bool Abc_NtkIsMappedLogic( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_MAP && pNtk->ntkType == ABC_NTK_LOGIC ; } -static inline bool Abc_NtkIsComb( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vLatches) == 0; } // reading data members of the network static inline char * Abc_NtkName( Abc_Ntk_t * pNtk ) { return pNtk->pName; } @@ -274,29 +274,48 @@ static inline void Abc_NtkSetBackup( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNetBa static inline void Abc_NtkSetStep ( Abc_Ntk_t * pNtk, int iStep ) { pNtk->iStep = iStep; } // getting the number of objects -static inline int Abc_NtkObjNumMax( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vObjs); } -static inline int Abc_NtkObjNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjs; } -static inline int Abc_NtkNetNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_NET]; } -static inline int Abc_NtkNodeNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_NODE]; } -static inline int Abc_NtkBoxNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_BOX]; } -static inline int Abc_NtkPiNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vPis); } -static inline int Abc_NtkPoNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vPos); } -static inline int Abc_NtkCiNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vCis); } -static inline int Abc_NtkCoNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vCos); } -static inline int Abc_NtkLatchNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vLatches); } -static inline int Abc_NtkAssertNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vAsserts); } -static inline int Abc_NtkCutSetNodeNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vCutSet); } +static inline int Abc_NtkObjNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjs; } +static inline int Abc_NtkObjNumMax( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vObjs); } +static inline int Abc_NtkPiNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vPis); } +static inline int Abc_NtkPoNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vPos); } +static inline int Abc_NtkCiNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vCis); } +static inline int Abc_NtkCoNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vCos); } +static inline int Abc_NtkAssertNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vAsserts); } +static inline int Abc_NtkBoxNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vBoxes); } +static inline int Abc_NtkCutSetNodeNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vCutSet); } +static inline int Abc_NtkBiNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_BI]; } +static inline int Abc_NtkBoNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_BO]; } +static inline int Abc_NtkNetNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_NET]; } +static inline int Abc_NtkNodeNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_NODE]; } +static inline int Abc_NtkGateNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_GATE]; } +static inline int Abc_NtkLatchNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_LATCH]; } +static inline int Abc_NtkTriNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_TRI]; } +static inline int Abc_NtkBlackboxNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_BLACKBOX]; } +static inline bool Abc_NtkIsComb( Abc_Ntk_t * pNtk ) { return Abc_NtkLatchNum(pNtk) == 0; } +static inline bool Abc_NtkHasOnlyLatchBoxes(Abc_Ntk_t * pNtk ){ return Abc_NtkLatchNum(pNtk) == Abc_NtkBoxNum(pNtk); } + +// creating simple objects +extern inline Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); +static inline Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PI ); } +static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PO ); } +static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BI ); } +static inline Abc_Obj_t * Abc_NtkCreateBo( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BO ); } +static Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_ASSERT ); } +static inline Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NODE ); } +static inline Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_LATCH ); } +static inline Abc_Obj_t * Abc_NtkCreateGate( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_GATE ); } +static inline Abc_Obj_t * Abc_NtkCreateTri( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_TRI ); } +static inline Abc_Obj_t * Abc_NtkCreateBlackbox( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BLACKBOX ); } // reading objects static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vObjs, i ); } -static inline Abc_Obj_t * Abc_NtkBox( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vBoxes, i ); } -static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vLatches, i );} -static inline Abc_Obj_t * Abc_NtkAssert( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vAsserts, i );} -static inline Abc_Obj_t * Abc_NtkCutSetNode( Abc_Ntk_t * pNtk, int i){ return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCutSet, i ); } -static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCis, i ); } -static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCos, i ); } static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vPis, i ); } static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vPos, i ); } +static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCis, i ); } +static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCos, i ); } +static inline Abc_Obj_t * Abc_NtkAssert( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vAsserts, i );} +static inline Abc_Obj_t * Abc_NtkBox( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vBoxes, i ); } +static inline Abc_Obj_t * Abc_NtkCutSetNode( Abc_Ntk_t * pNtk, int i){ return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCutSet, i ); } // reading data members of the object static inline unsigned Abc_ObjType( Abc_Obj_t * pObj ) { return pObj->Type; } @@ -319,19 +338,22 @@ static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p ) { return (A static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c ) { return (Abc_Obj_t *)((unsigned long)p ^ (unsigned long)(c!=0)); } // checking the object type -static inline bool Abc_ObjIsPi( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PI; } -static inline bool Abc_ObjIsPo( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PO; } -static inline bool Abc_ObjIsBi( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_BI; } -static inline bool Abc_ObjIsBo( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_BO; } -static inline bool Abc_ObjIsPio( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO; } -static inline bool Abc_ObjIsCi( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_BI || pObj->Type == ABC_OBJ_LATCH; } -static inline bool Abc_ObjIsCo( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_BO || pObj->Type == ABC_OBJ_LATCH || pObj->Type == ABC_OBJ_ASSERT; } -static inline bool Abc_ObjIsCio( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH || pObj->Type == ABC_OBJ_ASSERT; } -static inline bool Abc_ObjIsAssert( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_ASSERT; } -static inline bool Abc_ObjIsNet( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_NET; } -static inline bool Abc_ObjIsNode( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_NODE; } -static inline bool Abc_ObjIsLatch( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_LATCH; } -static inline bool Abc_ObjIsBox( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_BOX; } +static inline bool Abc_ObjIsPio( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PIO; } +static inline bool Abc_ObjIsPi( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PI; } +static inline bool Abc_ObjIsPo( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PO; } +static inline bool Abc_ObjIsBi( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_BI; } +static inline bool Abc_ObjIsBo( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_BO; } +static inline bool Abc_ObjIsAssert( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_ASSERT; } +static inline bool Abc_ObjIsCi( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_BI; } +static inline bool Abc_ObjIsCo( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_BO || pObj->Type == ABC_OBJ_ASSERT; } +static inline bool Abc_ObjIsTerm( Abc_Obj_t * pObj ) { return Abc_ObjIsCi(pObj) || Abc_ObjIsCo(pObj); } +static inline bool Abc_ObjIsNet( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_NET; } +static inline bool Abc_ObjIsNode( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_NODE; } +static inline bool Abc_ObjIsGate( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_GATE; } +static inline bool Abc_ObjIsLatch( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_LATCH; } +static inline bool Abc_ObjIsTri( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_TRI; } +static inline bool Abc_ObjIsBlackbox( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_BLACKBOX;} +static inline bool Abc_ObjIsBox( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_LATCH || pObj->Type == ABC_OBJ_TRI || pObj->Type == ABC_OBJ_BLACKBOX; } // working with fanin/fanout edges static inline int Abc_ObjFaninNum( Abc_Obj_t * pObj ) { return pObj->vFanins.nSize; } @@ -359,18 +381,6 @@ static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Ab static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); } static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) ); } -// creating simple objects -extern inline Abc_Obj_t * Abc_NtkObjAdd( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); -static inline Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ) { return Abc_NtkObjAdd( pNtk, Type ); } -static inline Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_NODE ); } -static inline Abc_Obj_t * Abc_NtkCreateBox( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_BOX ); } -static inline Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_PI ); } -static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_PO ); } -static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_BI ); } -static inline Abc_Obj_t * Abc_NtkCreateBo( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_BO ); } -static inline Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_LATCH ); } -static Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_ASSERT ); } - // checking the AIG node types static inline bool Abc_AigNodeIsConst( Abc_Obj_t * pNode ) { assert(Abc_NtkIsStrash(Abc_ObjRegular(pNode)->pNtk)||Abc_NtkIsSeq(Abc_ObjRegular(pNode)->pNtk)); return Abc_ObjRegular(pNode)->Type == ABC_OBJ_CONST1; } static inline bool Abc_AigNodeIsAnd( Abc_Obj_t * pNode ) { assert(!Abc_ObjIsComplement(pNode)); assert(Abc_NtkIsStrash(pNode->pNtk)||Abc_NtkIsSeq(pNode->pNtk)); return Abc_ObjFaninNum(pNode) == 2; } @@ -420,15 +430,33 @@ static inline float Abc_NtkGetLatSkew ( Abc_Ntk_t * pNtk, int lat ) #define Abc_NtkForEachNode( pNtk, pNode, i ) \ for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNode) = Abc_NtkObj(pNtk, i)), 1); i++ ) \ if ( (pNode) == NULL || !Abc_ObjIsNode(pNode) ) {} else +#define Abc_NtkForEachGate( pNtk, pNode, i ) \ + for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNode) = Abc_NtkObj(pNtk, i)), 1); i++ ) \ + if ( (pNode) == NULL || !Abc_ObjIsGate(pNode) ) {} else #define Abc_AigForEachAnd( pNtk, pNode, i ) \ for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNode) = Abc_NtkObj(pNtk, i)), 1); i++ ) \ if ( (pNode) == NULL || !Abc_AigNodeIsAnd(pNode) ) {} else -#define Abc_NtkForEachBox( pNtk, pNode, i ) \ - for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pNode) = Abc_NtkBox(pNtk, i)), 1); i++ ) \ - if ( (pNode) == NULL ) {} else #define Abc_SeqForEachCutsetNode( pNtk, pNode, i ) \ for ( i = 0; (i < Abc_NtkCutSetNodeNum(pNtk)) && (((pNode) = Abc_NtkCutSetNode(pNtk, i)), 1); i++ )\ if ( (pNode) == NULL ) {} else +// various boxes +#define Abc_NtkForEachBox( pNtk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_NtkBox(pNtk, i)), 1); i++ ) +#define Abc_NtkForEachLatch( pNtk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_NtkBox(pNtk, i)), 1); i++ ) \ + if ( !Abc_ObjIsLatch(pObj) ) {} else +#define Abc_NtkForEachLatchInput( pNtk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_ObjFanin0(Abc_NtkBox(pNtk, i))), 1); i++ ) \ + if ( !Abc_ObjIsLatch(Abc_NtkBox(pNtk, i)) ) {} else +#define Abc_NtkForEachLatchOutput( pNtk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_ObjFanout0(Abc_NtkBox(pNtk, i))), 1); i++ ) \ + if ( !Abc_ObjIsLatch(Abc_NtkBox(pNtk, i)) ) {} else +#define Abc_NtkForEachTri( pNtk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_NtkBox(pNtk, i)), 1); i++ ) \ + if ( !Abc_ObjIsTri(pObj) ) {} else +#define Abc_NtkForEachBlackbox( pNtk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pObj) = Abc_NtkBox(pNtk, i)), 1); i++ ) \ + if ( !Abc_ObjIsBlackbox(pObj) ) {} else // inputs and outputs #define Abc_NtkForEachPi( pNtk, pPi, i ) \ for ( i = 0; (i < Abc_NtkPiNum(pNtk)) && (((pPi) = Abc_NtkPi(pNtk, i)), 1); i++ ) @@ -436,12 +464,10 @@ static inline float Abc_NtkGetLatSkew ( Abc_Ntk_t * pNtk, int lat ) for ( i = 0; (i < Abc_NtkCiNum(pNtk)) && (((pCi) = Abc_NtkCi(pNtk, i)), 1); i++ ) #define Abc_NtkForEachPo( pNtk, pPo, i ) \ for ( i = 0; (i < Abc_NtkPoNum(pNtk)) && (((pPo) = Abc_NtkPo(pNtk, i)), 1); i++ ) -#define Abc_NtkForEachAssert( pNtk, pAssert, i ) \ - for ( i = 0; (i < Vec_PtrSize((pNtk)->vAsserts)) && (((pAssert) = Abc_NtkAssert(pNtk, i)), 1); i++ ) -#define Abc_NtkForEachLatch( pNtk, pLatch, i ) \ - for ( i = 0; (i < Vec_PtrSize((pNtk)->vLatches)) && (((pLatch) = Abc_NtkLatch(pNtk, i)), 1); i++ ) #define Abc_NtkForEachCo( pNtk, pCo, i ) \ for ( i = 0; (i < Abc_NtkCoNum(pNtk)) && (((pCo) = Abc_NtkCo(pNtk, i)), 1); i++ ) +#define Abc_NtkForEachAssert( pNtk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize((pNtk)->vAsserts)) && (((pObj) = Abc_NtkAssert(pNtk, i)), 1); i++ ) // fanin and fanouts #define Abc_ObjForEachFanin( pObj, pFanin, i ) \ for ( i = 0; (i < Abc_ObjFaninNum(pObj)) && (((pFanin) = Abc_ObjFanin(pObj, i)), 1); i++ ) @@ -568,14 +594,16 @@ extern Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fIni /*=== abcObj.c ==========================================================*/ extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); extern void Abc_ObjRecycle( Abc_Obj_t * pObj ); -extern Abc_Obj_t * Abc_NtkObjAdd( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); +extern Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj ); extern void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj ); -extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ); +extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName ); +extern Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName ); extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode ); extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ); extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName ); extern Abc_Obj_t * Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName ); extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName ); extern Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk ); extern Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk ); @@ -593,13 +621,11 @@ extern bool Abc_NodeIsInv( Abc_Obj_t * pNode ); extern void Abc_NodeComplement( Abc_Obj_t * pNode ); /*=== abcNames.c ====================================================*/ extern char * Abc_ObjName( Abc_Obj_t * pNode ); +extern char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix ); extern char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix ); extern char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits ); -extern char * Abc_NtkLogicStoreName( Abc_Obj_t * pNodeNew, char * pNameOld ); -extern char * Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pNodeNew, char * pNameOld, char * pSuffix ); -extern void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); -extern void Abc_NtkDupCioNamesTableNoLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); -extern void Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); +extern void Abc_NtkTrasferNames( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); +extern void Abc_NtkTrasferNamesNoLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); extern Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode ); extern Vec_Ptr_t * Abc_NodeGetFakeNames( int nNames ); extern void Abc_NodeFreeNames( Vec_Ptr_t * vNames ); @@ -609,7 +635,7 @@ extern void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb ); extern void Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk ); extern void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk ); extern void Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk ); -extern void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk ); +extern void Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk ); extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk ); /*=== abcNetlist.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ); @@ -627,7 +653,6 @@ extern void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan ); extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); extern Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); -extern Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); extern void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); extern Abc_Ntk_t * Abc_NtkStartRead( char * pName ); extern void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ); @@ -762,6 +787,7 @@ extern int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk ); extern void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk ); extern void Abc_NtkCleanNext( Abc_Ntk_t * pNtk ); extern void Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk ); +extern Abc_Obj_t * Abc_NodeHasCoFanout( Abc_Obj_t * pNode ); extern Abc_Obj_t * Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode ); extern bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk ); extern int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate ); diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 7a261cf4..ce430cf4 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -137,7 +137,7 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig ) pMan->vStackReplaceNew = Vec_PtrAlloc( 100 ); // create the constant node assert( pNtkAig->vObjs->nSize == 0 ); - pMan->pConst1 = Abc_NtkObjAdd( pNtkAig, ABC_OBJ_NODE ); + pMan->pConst1 = Abc_NtkCreateObj( pNtkAig, ABC_OBJ_NODE ); pMan->pConst1->Type = ABC_OBJ_CONST1; pNtkAig->nObjCounts[ABC_OBJ_NODE]--; // save the current network @@ -1329,16 +1329,16 @@ void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk ) int i; assert( Abc_NtkIsDfsOrdered(pNtk) ); Abc_AigConst1(pNtk)->fPhase = 1; -// Abc_NtkForEachCi( pNtk, pObj, i ) -// pObj->fPhase = 0; Abc_NtkForEachPi( pNtk, pObj, i ) pObj->fPhase = 0; - Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkForEachLatchOutput( pNtk, pObj, i ) pObj->fPhase = Abc_LatchIsInit1(pObj); Abc_AigForEachAnd( pNtk, pObj, i ) pObj->fPhase = (Abc_ObjFanin0(pObj)->fPhase ^ Abc_ObjFaninC0(pObj)) & (Abc_ObjFanin1(pObj)->fPhase ^ Abc_ObjFaninC1(pObj)); Abc_NtkForEachPo( pNtk, pObj, i ) pObj->fPhase = (Abc_ObjFanin0(pObj)->fPhase ^ Abc_ObjFaninC0(pObj)); + Abc_NtkForEachLatchInput( pNtk, pObj, i ) + pObj->fPhase = (Abc_ObjFanin0(pObj)->fPhase ^ Abc_ObjFaninC0(pObj)); } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index 12a2fab7..0156b331 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -111,23 +111,23 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk ) return 0; } } - +/* // check CI/CO numbers if ( Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCiNum(pNtk) ) { fprintf( stdout, "NetworkCheck: Number of CIs does not match number of PIs and latches.\n" ); fprintf( stdout, "One possible reason is that latches are added twice:\n" ); - fprintf( stdout, "in procedure Abc_NtkObjAdd() and in the user's code.\n" ); + fprintf( stdout, "in procedure Abc_NtkCreateObj() and in the user's code.\n" ); return 0; } if ( Abc_NtkPoNum(pNtk) + Abc_NtkAssertNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCoNum(pNtk) ) { fprintf( stdout, "NetworkCheck: Number of COs does not match number of POs, asserts, and latches.\n" ); fprintf( stdout, "One possible reason is that latches are added twice:\n" ); - fprintf( stdout, "in procedure Abc_NtkObjAdd() and in the user's code.\n" ); + fprintf( stdout, "in procedure Abc_NtkCreateObj() and in the user's code.\n" ); return 0; } - +*/ // check the names if ( !Abc_NtkCheckNames( pNtk ) ) return 0; @@ -241,36 +241,36 @@ bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk ) char * pName; int i, NameId; - // check that each CI/CO has a name - Abc_NtkForEachCi( pNtk, pObj, i ) + if ( Abc_NtkIsNetlist(pNtk) ) { - pObj = Abc_ObjFanout0Ntk(pObj); - if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL ) + // check that each net has a name + Abc_NtkForEachNet( pNtk, pObj, i ) { - fprintf( stdout, "NetworkCheck: CI with ID %d is in the network but not in the name table.\n", pObj->Id ); - return 0; + if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) ) + { + fprintf( stdout, "NetworkCheck: Net \"%s\" has different name in the name table and at the data pointer.\n", pObj->pData ); + return 0; + } } } - Abc_NtkForEachCo( pNtk, pObj, i ) + else { - if ( Abc_ObjIsLatch(pObj) ) - continue; - pObj = Abc_ObjFanin0Ntk(pObj); - if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL ) + // check that each CI/CO has a name + Abc_NtkForEachCi( pNtk, pObj, i ) { - fprintf( stdout, "NetworkCheck: CO with ID %d is in the network but not in the name table.\n", pObj->Id ); - return 0; + pObj = Abc_ObjFanout0Ntk(pObj); + if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL ) + { + fprintf( stdout, "NetworkCheck: CI with ID %d is in the network but not in the name table.\n", pObj->Id ); + return 0; + } } - } - - if ( Abc_NtkIsNetlist(pNtk) ) - { - Abc_NtkForEachNet( pNtk, pObj, i ) + Abc_NtkForEachCo( pNtk, pObj, i ) { - pName = Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id); - if ( pObj->pData && strcmp( pName, pObj->pData ) != 0 ) + pObj = Abc_ObjFanin0Ntk(pObj); + if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL ) { - fprintf( stdout, "NetworkCheck: Net \"%s\" has different name in the name table and at the data pointer.\n", pObj->pData ); + fprintf( stdout, "NetworkCheck: CO with ID %d is in the network but not in the name table.\n", pObj->Id ); return 0; } } @@ -543,7 +543,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ) return 0; } } - else if ( !Abc_NtkHasMapping(pNtk) ) + else if ( !Abc_NtkHasMapping(pNtk) && !Abc_NtkHasAig(pNtk) ) { assert( 0 ); } @@ -564,15 +564,10 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ) bool Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch ) { int Value = 1; - if ( pNtk->vLatches->nSize != Abc_NtkLatchNum(pNtk) ) - { - fprintf( stdout, "NetworkCheck: Incorrect size of the latch array.\n" ); - return 0; - } // check whether the object is a latch if ( !Abc_ObjIsLatch(pLatch) ) { - fprintf( stdout, "NodeCheck: Latch \"%s\" is in a latch list but has not latch label.\n", Abc_ObjName(pLatch) ); + fprintf( stdout, "NodeCheck: Latch \"%s\" is in a latch list but is not a latch.\n", Abc_ObjName(pLatch) ); Value = 0; } // make sure the latch has a reasonable return value @@ -588,6 +583,12 @@ bool Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch ) fprintf( stdout, "NodeCheck: Latch \"%s\" has wrong number (%d) of fanins.\n", Abc_ObjName(pLatch), Abc_ObjFaninNum(pLatch) ); Value = 0; } + // make sure the latch has only one fanin + if ( Abc_ObjFanoutNum(pLatch) != 1 ) + { + fprintf( stdout, "NodeCheck: Latch \"%s\" has wrong number (%d) of fanouts.\n", Abc_ObjName(pLatch), Abc_ObjFanoutNum(pLatch) ); + Value = 0; + } return Value; } @@ -671,24 +672,26 @@ bool Abc_NtkComparePos( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) SeeAlso [] ***********************************************************************/ -bool Abc_NtkCompareLatches( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) +bool Abc_NtkCompareBoxes( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) { Abc_Obj_t * pObj1; int i; + assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) ); if ( !fComb ) return 1; - if ( Abc_NtkLatchNum(pNtk1) != Abc_NtkLatchNum(pNtk2) ) + if ( Abc_NtkBoxNum(pNtk1) != Abc_NtkBoxNum(pNtk2) ) { printf( "Networks have different number of latches.\n" ); return 0; } // for each PI of pNet1 find corresponding PI of pNet2 and reorder them - Abc_NtkForEachLatch( pNtk1, pObj1, i ) + Abc_NtkForEachBox( pNtk1, pObj1, i ) { - if ( strcmp( Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkLatch(pNtk2,i)) ) != 0 ) + if ( strcmp( Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkBox(pNtk2,i)) ) != 0 ) { - printf( "Latch #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n", - i, Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkLatch(pNtk2,i)) ); + printf( "Box #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n", + i, Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkBox(pNtk2,i)) ); return 0; } } @@ -710,7 +713,7 @@ bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) { Abc_NtkOrderObjsByName( pNtk1, fComb ); Abc_NtkOrderObjsByName( pNtk2, fComb ); - if ( !Abc_NtkCompareLatches( pNtk1, pNtk2, fComb ) ) + if ( !Abc_NtkCompareBoxes( pNtk1, pNtk2, fComb ) ) return 0; if ( !Abc_NtkComparePis( pNtk1, pNtk2, fComb ) ) return 0; diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c index be487051..8b0a1608 100644 --- a/src/base/abc/abcLatch.c +++ b/src/base/abc/abcLatch.c @@ -45,10 +45,10 @@ bool Abc_NtkLatchIsSelfFeed_rec( Abc_Obj_t * pLatch, Abc_Obj_t * pLatchRoot ) assert( Abc_ObjIsLatch(pLatch) ); if ( pLatch == pLatchRoot ) return 1; - pFanin = Abc_ObjFanin0(pLatch); - if ( !Abc_ObjIsLatch(pFanin) ) + pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch)); + if ( !Abc_ObjIsBi(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) ) return 0; - return Abc_NtkLatchIsSelfFeed_rec( pFanin, pLatch ); + return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatch ); } /**Function************************************************************* @@ -66,10 +66,10 @@ bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch ) { Abc_Obj_t * pFanin; assert( Abc_ObjIsLatch(pLatch) ); - pFanin = Abc_ObjFanin0(pLatch); - if ( !Abc_ObjIsLatch(pFanin) ) + pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch)); + if ( !Abc_ObjIsBi(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) ) return 0; - return Abc_NtkLatchIsSelfFeed_rec( pFanin, pLatch ); + return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatch ); } /**Function************************************************************* @@ -121,7 +121,7 @@ int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk ) pConst1 = Abc_AigConst1(pNtk); else pConst1 = Abc_NodeCreateConst1(pNtk); - Abc_ObjPatchFanin( pLatch, Abc_ObjFanin0(pLatch), pConst1 ); + Abc_ObjPatchFanin( pLatch, Abc_ObjFanin0(Abc_ObjFanin0(pLatch)), pConst1 ); Counter++; } } @@ -160,7 +160,7 @@ void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches ) Abc_ObjAddFanin( pLatch, pFanin ); Abc_LatchSetInitDc( pLatch ); // create the name of the new latch - Abc_NtkLogicStoreName( pLatch, Abc_ObjNameDummy("LL", i*nLatches + k, nDigits) ); + Abc_ObjAssignName( pLatch, Abc_ObjNameDummy("LL", i*nLatches + k, nDigits), NULL ); } // patch the PI fanouts Vec_PtrForEachEntry( vNodes, pFanout, k ) diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c index 1d6619f0..3a7e4d5b 100644 --- a/src/base/abc/abcLib.c +++ b/src/base/abc/abcLib.c @@ -125,6 +125,7 @@ Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib ) ***********************************************************************/ int Abc_LibDeriveBlackBoxes( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib ) { +/* Abc_Obj_t * pObj, * pFanin, * pFanout; int i, k; assert( Abc_NtkIsNetlist(pNtk) ); @@ -161,6 +162,8 @@ int Abc_LibDeriveBlackBoxes( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib ) } } return Vec_PtrSize(pNtk->vBoxes); +*/ + return 1; } /**Function************************************************************* diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c index 0deb20e3..274cf243 100644 --- a/src/base/abc/abcNames.c +++ b/src/base/abc/abcNames.c @@ -30,11 +30,12 @@ /**Function************************************************************* - Synopsis [Gets the long name of the object.] + Synopsis [Returns the unique name for the object.] - Description [The temporary name is stored in a static buffer inside this - procedure. It is important that the name is used before the function is - called again!] + Description [If the name previously did not exist, creates a new unique + name but does not assign this name to the object. The temporary unique + name is stored in a static buffer inside this procedure. It is important + that the name is used before the function is called again!] SideEffects [] @@ -43,119 +44,51 @@ ***********************************************************************/ char * Abc_ObjName( Abc_Obj_t * pObj ) { - static char Buffer[500]; - char * pName; - int Counter; - - // check if the object is in the lookup table -// if ( stmm_lookup( pObj->pNtk->tObj2Name, (char *)pObj, &pName ) ) -// return pName; - if ( pName = Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) ) - return pName; - - // consider network types - if ( Abc_NtkIsNetlist(pObj->pNtk) ) - { - // in a netlist, nets have names, nodes have no names - if ( Abc_ObjIsNode(pObj) ) - pObj = Abc_ObjFanout0(pObj); - assert( Abc_ObjIsNet(pObj) ); - // if the name is not given, invent it - if ( pObj->pData ) - sprintf( Buffer, "%s", pObj->pData ); - else - { - sprintf( Buffer, "[%d]", pObj->Id ); // make sure this name is unique!!! - for ( Counter = 1; Nm_ManFindIdByName(pObj->pNtk->pManName, Buffer, NULL) >= 0; Counter++ ) - sprintf( Buffer, "[%d]_%d", pObj->Id, Counter ); - } - } - else - { - // in a logic network, PI/PO/latch names are stored in the hash table - // internal nodes have made up names - assert( Abc_ObjIsNode(pObj) || Abc_ObjIsLatch(pObj) ); - sprintf( Buffer, "[%d]", pObj->Id ); - for ( Counter = 1; Nm_ManFindIdByName(pObj->pNtk->pManName, Buffer, NULL) >= 0; Counter++ ) - sprintf( Buffer, "[%d]_%d", pObj->Id, Counter ); - } - return Buffer; + return Nm_ManCreateUniqueName( pObj->pNtk->pManName, pObj->Id ); } /**Function************************************************************* - Synopsis [Gets the long name of the node.] + Synopsis [Assigns the given name to the object.] - Description [This name is the output net's name.] + Description [The object should not have a name assigned. The same + name may be used for several objects, which they share the same net + in the original netlist. (For example, latch output and primary output + may have the same name.) This procedure returns the pointer to the + internally stored representation of the given name.] SideEffects [] SeeAlso [] ***********************************************************************/ -char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix ) +char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix ) { - static char Buffer[500]; - sprintf( Buffer, "%s%s", Abc_ObjName(pObj), pSuffix ); - return Buffer; + assert( pName != NULL ); + return Nm_ManStoreIdName( pObj->pNtk->pManName, pObj->Id, pObj->Type, pName, pSuffix ); } - /**Function************************************************************* - Synopsis [Returns the dummy PI name.] + Synopsis [Gets the long name of the node.] - Description [] + Description [This name is the output net's name.] SideEffects [] SeeAlso [] ***********************************************************************/ -char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits ) +char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix ) { - static char Buffer[100]; - sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num ); + static char Buffer[500]; + sprintf( Buffer, "%s%s", Abc_ObjName(pObj), pSuffix ); return Buffer; } - /**Function************************************************************* - Synopsis [Adds new name to the network.] - - Description [The new object (pObjNew) is a PI, PO or latch. The name - is registered and added to the hash table.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Abc_NtkLogicStoreName( Abc_Obj_t * pObjNew, char * pNameOld ) -{ - return Nm_ManStoreIdName( pObjNew->pNtk->pManName, pObjNew->Id, pNameOld, NULL ); -} - -/**Function************************************************************* - - Synopsis [Adds new name to the network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pObjNew, char * pNameOld, char * pSuffix ) -{ - return Nm_ManStoreIdName( pObjNew->pNtk->pManName, pObjNew->Id, pNameOld, pSuffix ); -} - -/**Function************************************************************* - - Synopsis [Duplicates the name arrays.] + Synopsis [Returns the dummy PI name.] Description [] @@ -164,97 +97,73 @@ char * Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pObjNew, char * pNameOld, char * p SeeAlso [] ***********************************************************************/ -void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits ) { - Abc_Obj_t * pObj, * pTerm; - int i, k; - assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) ); - assert( Abc_NtkPoNum(pNtk) == Abc_NtkPoNum(pNtkNew) ); - assert( Abc_NtkAssertNum(pNtk) == Abc_NtkAssertNum(pNtkNew) ); - assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) ); - assert( Nm_ManNumEntries(pNtk->pManName) > 0 ); - assert( Nm_ManNumEntries(pNtkNew->pManName) == 0 ); - // copy the CI/CO names if given - Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) ); - Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) ); - Abc_NtkForEachAssert( pNtk, pObj, i ) - Abc_NtkLogicStoreName( Abc_NtkAssert(pNtkNew,i), Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) ); - Abc_NtkForEachBox( pNtk, pObj, i ) - { - Abc_ObjForEachFanin( pObj, pTerm, k ) - Abc_NtkLogicStoreName( pTerm->pCopy, Abc_ObjName(Abc_ObjFanin0Ntk(pTerm)) ); - Abc_ObjForEachFanout( pObj, pTerm, k ) - Abc_NtkLogicStoreName( pTerm->pCopy, Abc_ObjName(Abc_ObjFanout0Ntk(pTerm)) ); - } - if ( !Abc_NtkIsSeq(pNtk) ) - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) ); + static char Buffer[100]; + sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num ); + return Buffer; } /**Function************************************************************* - Synopsis [Duplicates the name arrays.] + Synopsis [Tranfers names to the old network.] - Description [] + Description [Assumes that the new nodes are attached using pObj->pCopy.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Abc_NtkDupCioNamesTableNoLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +void Abc_NtkTrasferNames( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) { Abc_Obj_t * pObj; int i; assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) ); assert( Abc_NtkPoNum(pNtk) == Abc_NtkPoNum(pNtkNew) ); + assert( Abc_NtkBoxNum(pNtk) == Abc_NtkBoxNum(pNtkNew) ); assert( Abc_NtkAssertNum(pNtk) == Abc_NtkAssertNum(pNtkNew) ); assert( Nm_ManNumEntries(pNtk->pManName) > 0 ); assert( Nm_ManNumEntries(pNtkNew->pManName) == 0 ); - // copy the CI/CO names if given - Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) ); - Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) ); - Abc_NtkForEachAssert( pNtk, pObj, i ) - Abc_NtkLogicStoreName( Abc_NtkAssert(pNtkNew,i), Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) ); + // copy the CI/CO/box names + Abc_NtkForEachCi( pNtk, pObj, i ) + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(Abc_ObjFanout0Ntk(pObj)), NULL ); + Abc_NtkForEachCo( pNtk, pObj, i ) + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(Abc_ObjFanin0Ntk(pObj)), NULL ); + Abc_NtkForEachBox( pNtk, pObj, i ) + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); } /**Function************************************************************* - Synopsis [Duplicates the name arrays.] + Synopsis [Tranfers names to the old network.] - Description [] + Description [Assumes that the new nodes are attached using pObj->pCopy.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +void Abc_NtkTrasferNamesNoLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) { Abc_Obj_t * pObj; int i; assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) ); - assert( Abc_NtkPoNum(pNtk) * 2 == Abc_NtkPoNum(pNtkNew) ); - assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) ); + assert( Abc_NtkPoNum(pNtk) == Abc_NtkPoNum(pNtkNew) ); + assert( Abc_NtkAssertNum(pNtk) == Abc_NtkAssertNum(pNtkNew) ); assert( Nm_ManNumEntries(pNtk->pManName) > 0 ); assert( Nm_ManNumEntries(pNtkNew->pManName) == 0 ); - // copy the CI/CO names if given - Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pObj) ); - Abc_NtkForEachPo( pNtk, pObj, i ) - { - Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+0), Abc_ObjName(pObj), "_pos" ); - Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+1), Abc_ObjName(pObj), "_neg" ); - } - Abc_NtkForEachAssert( pNtk, pObj, i ) - Abc_NtkLogicStoreName( Abc_NtkAssert(pNtkNew,i), Abc_ObjName(pObj) ); - if ( !Abc_NtkIsSeq(pNtk) ) - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) ); + // copy the CI/CO/box name and skip latches and theirs inputs/outputs + Abc_NtkForEachCi( pNtk, pObj, i ) + if ( Abc_ObjFaninNum(pObj) == 0 || !Abc_ObjIsLatch(Abc_ObjFanin0(pObj)) ) + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(Abc_ObjFanout0Ntk(pObj)), NULL ); + Abc_NtkForEachCo( pNtk, pObj, i ) + if ( Abc_ObjFanoutNum(pObj) == 0 || !Abc_ObjIsLatch(Abc_ObjFanout0(pObj)) ) + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(Abc_ObjFanin0Ntk(pObj)), NULL ); + Abc_NtkForEachBox( pNtk, pObj, i ) + if ( !Abc_ObjIsLatch(pObj) ) + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); } /**Function************************************************************* @@ -403,12 +312,14 @@ void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb ) { Abc_Obj_t * pObj; int i; + assert( Abc_NtkAssertNum(pNtk) == 0 ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk) ); // temporarily store the names in the copy field Abc_NtkForEachPi( pNtk, pObj, i ) pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); Abc_NtkForEachPo( pNtk, pObj, i ) pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); - Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkForEachBox( pNtk, pObj, i ) pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); // order objects alphabetically qsort( (void *)Vec_PtrArray(pNtk->vPis), Vec_PtrSize(pNtk->vPis), sizeof(Abc_Obj_t *), @@ -417,7 +328,7 @@ void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb ) (int (*)(const void *, const void *)) Abc_NodeCompareNames ); // if the comparison if combinational (latches as PIs/POs), order them too if ( fComb ) - qsort( (void *)Vec_PtrArray(pNtk->vLatches), Vec_PtrSize(pNtk->vLatches), sizeof(Abc_Obj_t *), + qsort( (void *)Vec_PtrArray(pNtk->vBoxes), Vec_PtrSize(pNtk->vBoxes), sizeof(Abc_Obj_t *), (int (*)(const void *, const void *)) Abc_NodeCompareNames ); // order CIs/COs first PIs/POs(Asserts) then latches Abc_NtkOrderCisCos( pNtk ); @@ -426,7 +337,7 @@ void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb ) pObj->pCopy = NULL; Abc_NtkForEachPo( pNtk, pObj, i ) pObj->pCopy = NULL; - Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkForEachBox( pNtk, pObj, i ) pObj->pCopy = NULL; } @@ -447,7 +358,7 @@ void Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk ) int nDigits, i; nDigits = Extra_Base10Log( Abc_NtkPiNum(pNtk) ); Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("pi", i, nDigits) ); + Abc_ObjAssignName( pObj, Abc_ObjNameDummy("pi", i, nDigits), NULL ); } /**Function************************************************************* @@ -467,7 +378,7 @@ void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk ) int nDigits, i; nDigits = Extra_Base10Log( Abc_NtkPoNum(pNtk) ); Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("po", i, nDigits) ); + Abc_ObjAssignName( pObj, Abc_ObjNameDummy("po", i, nDigits), NULL ); } /**Function************************************************************* @@ -487,7 +398,7 @@ void Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk ) int nDigits, i; nDigits = Extra_Base10Log( Abc_NtkAssertNum(pNtk) ); Abc_NtkForEachAssert( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("a", i, nDigits) ); + Abc_ObjAssignName( pObj, Abc_ObjNameDummy("a", i, nDigits), NULL ); } /**Function************************************************************* @@ -501,13 +412,37 @@ void Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk ) +void Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk ) { - Abc_Obj_t * pObj; - int nDigits, i; + Abc_Obj_t * pObj, * pTerm; + int nDigits, nDigitsF, i, k; + char * pName; nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtk) ); Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("L", i, nDigits) ); + { + Abc_ObjAssignName( pObj, Abc_ObjNameDummy("L", i, nDigits), NULL ); + Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjNameDummy("Li", i, nDigits), NULL ); + Abc_ObjAssignName( Abc_ObjFanout0(pObj), Abc_ObjNameDummy("Lo", i, nDigits), NULL ); + } + nDigits = Extra_Base10Log( Abc_NtkTriNum(pNtk) ); + Abc_NtkForEachTri( pNtk, pObj, i ) + { + Abc_ObjAssignName( pObj, Abc_ObjNameDummy("T", i, nDigits), NULL ); + Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjNameDummy("Ti0", i, nDigits), NULL ); + Abc_ObjAssignName( Abc_ObjFanin1(pObj), Abc_ObjNameDummy("Ti1", i, nDigits), NULL ); + Abc_ObjAssignName( Abc_ObjFanout0(pObj), Abc_ObjNameDummy("To", i, nDigits), NULL ); + } + nDigits = Extra_Base10Log( Abc_NtkBlackboxNum(pNtk) ); + Abc_NtkForEachBlackbox( pNtk, pObj, i ) + { + pName = Abc_ObjAssignName( pObj, Abc_ObjNameDummy("B", i, nDigits), NULL ); + nDigitsF = Extra_Base10Log( Abc_ObjFaninNum(pObj) ); + Abc_ObjForEachFanin( pObj, pTerm, k ) + Abc_ObjAssignName( Abc_ObjFanin0(pObj), pName, Abc_ObjNameDummy("i", k, nDigitsF) ); + nDigitsF = Extra_Base10Log( Abc_ObjFanoutNum(pObj) ); + Abc_ObjForEachFanout( pObj, pTerm, k ) + Abc_ObjAssignName( Abc_ObjFanin0(pObj), pName, Abc_ObjNameDummy("o", k, nDigitsF) ); + } } /**Function************************************************************* @@ -524,11 +459,11 @@ void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk ) void Abc_NtkShortNames( Abc_Ntk_t * pNtk ) { Nm_ManFree( pNtk->pManName ); - pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk) - Abc_NtkLatchNum(pNtk) + 10 ); + pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk) + Abc_NtkBoxNum(pNtk) ); Abc_NtkAddDummyPiNames( pNtk ); Abc_NtkAddDummyPoNames( pNtk ); Abc_NtkAddDummyAssertNames( pNtk ); - Abc_NtkAddDummyLatchNames( pNtk ); + Abc_NtkAddDummyBoxNames( pNtk ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c index 145531db..0650896d 100644 --- a/src/base/abc/abcNetlist.c +++ b/src/base/abc/abcNetlist.c @@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk ) pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, pNtk->ntkFunc ); // duplicate the nodes Abc_NtkForEachNode( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj(pNtkNew, pObj, 0); // reconnect the internal nodes in the new network Abc_NtkForEachNode( pNtk, pObj, i ) Abc_ObjForEachFanin( pObj, pFanin, k ) @@ -109,13 +109,13 @@ Abc_Ntk_t * Abc_NtkNetlistToLogicHie( Abc_Ntk_t * pNtk ) // clone PIs/POs/latches and make old nets point to new terminals; create names Abc_NtkForEachCi( pNtk, pObj, i ) { - Abc_ObjFanout0(pObj)->pCopy = Abc_NtkDupObj(pNtkNew, pObj); - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(Abc_ObjFanout0(pObj)) ); + Abc_ObjFanout0(pObj)->pCopy = Abc_NtkDupObj(pNtkNew, pObj, 0); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(Abc_ObjFanout0(pObj)), NULL ); } Abc_NtkForEachPo( pNtk, pObj, i ) { - Abc_NtkDupObj(pNtkNew, pObj); - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(Abc_ObjFanin0(pObj)) ); + Abc_NtkDupObj(pNtkNew, pObj, 0); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(Abc_ObjFanin0(pObj)), NULL ); } // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes Abc_NtkNetlistToLogicHie_rec( pNtkNew, pNtk, &Counter ); @@ -164,7 +164,7 @@ void Abc_NtkNetlistToLogicHie_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int if ( Abc_ObjIsNode(pNode) ) { // duplicate the node and save it in the fanout net - Abc_NtkDupObj( pNtkNew, pNode ); + Abc_NtkDupObj( pNtkNew, pNode, 0 ); Abc_ObjFanout0(pNode)->pCopy = pNode->pCopy; continue; } @@ -184,14 +184,14 @@ void Abc_NtkNetlistToLogicHie_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int { pObj->pCopy = Abc_NtkCreatePi( pNtkNew ); Abc_ObjFanout(pNode, k)->pCopy = pObj->pCopy; - Abc_NtkLogicStoreNamePlus( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanin0(pObj)) ); + Abc_ObjAssignName( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanin0(pObj)) ); } // create new POs from the PIs of the box Abc_NtkForEachPi( pNtkModel, pObj, k ) { pObj->pCopy = Abc_NtkCreatePo( pNtkNew ); // Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin(pNode, k)->pCopy ); - Abc_NtkLogicStoreNamePlus( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanout0(pObj)) ); + Abc_ObjAssignName( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanout0(pObj)) ); } (*pCounter)++; Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) ); @@ -319,12 +319,10 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ) { Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObj, * pNet, * pDriver, * pFanin; - char * pNameCo; int i, k; assert( Abc_NtkIsLogic(pNtk) ); assert( Abc_NtkLogicHasSimpleCos(pNtk) ); - if ( Abc_NtkIsBddLogic(pNtk) ) { if ( !Abc_NtkBddToSop(pNtk,0) ) @@ -333,22 +331,19 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ) // start the netlist by creating PI/PO/Latch objects pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, pNtk->ntkFunc ); - // create the CI nets and remember them in the new CI nodes Abc_NtkForEachCi( pNtk, pObj, i ) { pNet = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pObj) ); Abc_ObjAddFanin( pNet, pObj->pCopy ); pObj->pCopy->pCopy = pNet; -//printf( "%s ", Abc_ObjName(pObj) ); } -//printf( "\n" ); // duplicate all nodes Abc_NtkForEachNode( pNtk, pObj, i ) { if ( Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 ) continue; - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj(pNtkNew, pObj, 0); } // first add the nets to the CO drivers Abc_NtkForEachCo( pNtk, pObj, i ) @@ -361,18 +356,18 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ) continue; } assert( Abc_ObjIsNode(pDriver) ); - // the driver is a node - - // get the CO name - pNameCo = Abc_ObjIsLatch(pObj)? Abc_ObjNameSuffix( pObj, "_in" ) : Abc_ObjName(pObj); - // make sure CO has a unique name - assert( Abc_NtkFindNet( pNtkNew, pNameCo ) == NULL ); - // create the CO net and connect it to CO - pNet = Abc_NtkFindOrCreateNet( pNtkNew, pNameCo ); - Abc_ObjAddFanin( pObj->pCopy, pNet ); - // connect the CO net to the new driver and remember it in the new driver - Abc_ObjAddFanin( pNet, pDriver->pCopy ); - pDriver->pCopy->pCopy = pNet; + // if the CO drive has no net, create it + if ( pDriver->pCopy->pCopy == NULL ) + { + // create the CO net and connect it to CO + pNet = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pObj) ); + Abc_ObjAddFanin( pObj->pCopy, pNet ); + // connect the CO net to the new driver and remember it in the new driver + Abc_ObjAddFanin( pNet, pDriver->pCopy ); + pDriver->pCopy->pCopy = pNet; + } + else + assert( !strcmp( Abc_ObjName(pDriver->pCopy->pCopy), Abc_ObjName(pObj) ) ); } // create the missing nets Abc_NtkForEachNode( pNtk, pObj, i ) @@ -425,7 +420,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk ) // duplicate the nodes and create node functions Abc_NtkForEachNode( pNtk, pObj, i ) { - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj(pNtkNew, pObj, 0); pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); } // create the choice nodes @@ -519,7 +514,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk ) // duplicate the nodes, create node functions, and inverters Vec_PtrForEachEntry( vNodes, pObj, i ) { - Abc_NtkDupObj( pNtkNew, pObj ); + Abc_NtkDupObj( pNtkNew, pObj, 0 ); pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2, NULL ); if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) ) pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy ); diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index e94e0a2f..37461c22 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -52,7 +52,6 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan pNtk->ntkFunc = Func; // start the object storage pNtk->vObjs = Vec_PtrAlloc( 100 ); - pNtk->vLatches = Vec_PtrAlloc( 100 ); pNtk->vAsserts = Vec_PtrAlloc( 100 ); pNtk->vPios = Vec_PtrAlloc( 100 ); pNtk->vPis = Vec_PtrAlloc( 100 ); @@ -83,7 +82,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan else if ( !Abc_NtkHasBlackbox(pNtk) ) assert( 0 ); // name manager - pNtk->pManName = Nm_ManCreate( 1000 ); + pNtk->pManName = Nm_ManCreate( 200 ); return pNtk; } @@ -101,43 +100,33 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ) { Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pTerm; - int i, k; + Abc_Obj_t * pObj; + int fCopyNames, i; if ( pNtk == NULL ) return NULL; + // decide whether to copy the names + fCopyNames = ( Type != ABC_NTK_NETLIST ); // start the network pNtkNew = Abc_NtkAlloc( Type, Func, 1 ); // duplicate the name and the spec pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec); // clean the node copy fields - Abc_NtkForEachNode( pNtk, pObj, i ) - pObj->pCopy = NULL; + Abc_NtkCleanCopy( pNtk ); // map the constant nodes if ( Abc_NtkIsStrash(pNtk) && Abc_NtkIsStrash(pNtkNew) ) Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - // clone the PIs/POs/latches + // clone CIs/CIs/boxes Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj( pNtkNew, pObj, fCopyNames ); Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj( pNtkNew, pObj, fCopyNames ); Abc_NtkForEachAssert( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj( pNtkNew, pObj, fCopyNames ); Abc_NtkForEachBox( pNtk, pObj, i ) - { - Abc_NtkDupObj(pNtkNew, pObj); - if ( Abc_NtkIsNetlist(pNtk) ) - continue; - Abc_ObjForEachFanin( pObj, pTerm, k ) - Abc_NtkDupObj(pNtkNew, pTerm); - Abc_ObjForEachFanout( pObj, pTerm, k ) - Abc_NtkDupObj(pNtkNew, pTerm); - } + Abc_NtkDupBox( pNtkNew, pObj, fCopyNames ); // transfer the names - if ( Type != ABC_NTK_NETLIST ) - Abc_NtkDupCioNamesTable( pNtk, pNtkNew ); +// Abc_NtkTrasferNames( pNtk, pNtkNew ); Abc_ManTimeDup( pNtk, pNtkNew ); // check that the CI/CO/latches are copied correctly assert( Abc_NtkCiNum(pNtk) == Abc_NtkCiNum(pNtkNew) ); @@ -164,29 +153,32 @@ Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc int i; if ( pNtk == NULL ) return NULL; + assert( Type != ABC_NTK_NETLIST ); // start the network pNtkNew = Abc_NtkAlloc( Type, Func, 1 ); // duplicate the name and the spec pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec); // clean the node copy fields - Abc_NtkForEachNode( pNtk, pObj, i ) - pObj->pCopy = NULL; + Abc_NtkCleanCopy( pNtk ); // map the constant nodes if ( Abc_NtkIsStrash(pNtk) && Abc_NtkIsStrash(pNtkNew) ) Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - // clone the PIs/POs/latches + // clone CIs/CIs/boxes Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj( pNtkNew, pObj, 1 ); Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj( pNtkNew, pObj, 1 ); Abc_NtkForEachAssert( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj( pNtkNew, pObj, 1 ); Abc_NtkForEachBox( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); + { + if ( Abc_ObjIsLatch(pObj) ) + continue; + Abc_NtkDupBox(pNtkNew, pObj, 1); + } // transfer the names - if ( Type != ABC_NTK_NETLIST ) - Abc_NtkDupCioNamesTableNoLatches( pNtk, pNtkNew ); +// Abc_NtkTrasferNamesNoLatches( pNtk, pNtkNew ); Abc_ManTimeDup( pNtk, pNtkNew ); // check that the CI/CO/latches are copied correctly assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) ); @@ -196,63 +188,6 @@ Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc /**Function************************************************************* - Synopsis [Starts a new network using existing network as a model.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pObjNew; - int i; - if ( pNtk == NULL ) - return NULL; - // start the network - pNtkNew = Abc_NtkAlloc( Type, Func, 1 ); - // duplicate the name and the spec - pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); - pNtkNew->pSpec = NULL; - // clean the node copy fields - Abc_NtkForEachNode( pNtk, pObj, i ) - pObj->pCopy = NULL; - // map the constant nodes - if ( Abc_NtkIsStrash(pNtk) && Abc_NtkIsStrash(pNtkNew) ) - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - // clone the PIs/POs/latches - Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); - Abc_NtkForEachPo( pNtk, pObj, i ) - { - Abc_NtkDupObj(pNtkNew, pObj); - pObjNew = pObj->pCopy; - Abc_NtkDupObj(pNtkNew, pObj); - // connect second to the first - pObjNew->pCopy = pObj->pCopy; - // collect first to old - pObj->pCopy = pObjNew; - } - Abc_NtkForEachAssert( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); - Abc_NtkForEachBox( pNtk, pObj, i ) - Abc_NtkDupObj(pNtkNew, pObj); - // transfer the names - Abc_NtkDupCioNamesTableDual( pNtk, pNtkNew ); - // check that the CI/CO/latches are copied correctly - assert( Abc_NtkCiNum(pNtk) == Abc_NtkCiNum(pNtkNew) ); - assert( Abc_NtkCoNum(pNtk)* 2 == Abc_NtkCoNum(pNtkNew) ); - assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) ); - return pNtkNew; -} - -/**Function************************************************************* - Synopsis [Finalizes the network using the existing network as a model.] Description [] @@ -314,7 +249,7 @@ void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ) int i; if ( Abc_NtkHasBlackbox(pNtk) ) { - pBox = Abc_NtkCreateBox(pNtk); + pBox = Abc_NtkCreateBlackbox(pNtk); Abc_NtkForEachPi( pNtk, pObj, i ) Abc_ObjAddFanin( pBox, Abc_ObjFanout0(pObj) ); Abc_NtkForEachPo( pNtk, pObj, i ) @@ -374,7 +309,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) Abc_NtkForEachObj( pNtk, pObj, i ) if ( pObj->pCopy == NULL ) { - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj(pNtkNew, pObj, 0); pObj->pCopy->Level = pObj->Level; pObj->pCopy->fPhase = pObj->fPhase; } @@ -403,11 +338,12 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) // duplicate the nets and nodes (CIs/COs/latches already dupped) Abc_NtkForEachObj( pNtk, pObj, i ) if ( pObj->pCopy == NULL ) - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj(pNtkNew, pObj, 0); // reconnect all objects (no need to transfer attributes on edges) Abc_NtkForEachObj( pNtk, pObj, i ) - Abc_ObjForEachFanin( pObj, pFanin, k ) - Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); + if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) ) + Abc_ObjForEachFanin( pObj, pFanin, k ) + Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); } // duplicate the EXDC Ntk if ( pNtk->pExdc ) @@ -457,12 +393,12 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode if ( fUseAllCis || Abc_NodeIsTravIdCurrent(pObj) ) // TravId is set by DFS { pObj->pCopy = Abc_NtkCreatePi(pNtkNew); - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); } } // add the PO corresponding to this output pNodeCoNew = Abc_NtkCreatePo( pNtkNew ); - Abc_NtkLogicStoreName( pNodeCoNew, pNodeName ); + Abc_ObjAssignName( pNodeCoNew, pNodeName, NULL ); // copy the nodes Vec_PtrForEachEntry( vNodes, pObj, i ) { @@ -473,7 +409,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode } else { - Abc_NtkDupObj( pNtkNew, pObj ); + Abc_NtkDupObj( pNtkNew, pObj, 0 ); Abc_ObjForEachFanin( pObj, pFanin, k ) Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); } @@ -529,11 +465,11 @@ Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode Vec_PtrForEachEntry( vSupp, pObj, i ) { pObj->pCopy = Abc_NtkCreatePi(pNtkNew); - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); } // create the PO pNodeCoNew = Abc_NtkCreatePo( pNtkNew ); - Abc_NtkLogicStoreName( pNodeCoNew, pNodeName ); + Abc_ObjAssignName( pNodeCoNew, pNodeName, NULL ); // copy the nodes Vec_PtrForEachEntry( vCone, pObj, i ) { @@ -544,7 +480,7 @@ Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode } else { - Abc_NtkDupObj( pNtkNew, pObj ); + Abc_NtkDupObj( pNtkNew, pObj, 0 ); Abc_ObjForEachFanin( pObj, pFanin, k ) Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); } @@ -594,7 +530,7 @@ Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t Abc_NtkForEachCi( pNtk, pObj, i ) { pObj->pCopy = Abc_NtkCreatePi(pNtkNew); - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); } // copy the nodes Vec_PtrForEachEntry( vNodes, pObj, i ) @@ -617,7 +553,7 @@ Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t // add the PO corresponding to this output pNodePo = Abc_NtkCreatePo( pNtkNew ); Abc_ObjAddFanin( pNodePo, pFinal ); - Abc_NtkLogicStoreName( pNodePo, "miter" ); + Abc_ObjAssignName( pNodePo, "miter", NULL ); if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkCreateTarget(): Network check has failed.\n" ); return pNtkNew; @@ -646,16 +582,16 @@ Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ) Abc_ObjForEachFanin( pNode, pFanin, i ) { pFanin->pCopy = Abc_NtkCreatePi( pNtkNew ); - Abc_NtkLogicStoreName( pFanin->pCopy, Abc_ObjName(pFanin) ); + Abc_ObjAssignName( pFanin->pCopy, Abc_ObjName(pFanin), NULL ); } // duplicate and connect the node - pNode->pCopy = Abc_NtkDupObj( pNtkNew, pNode ); + pNode->pCopy = Abc_NtkDupObj( pNtkNew, pNode, 0 ); Abc_ObjForEachFanin( pNode, pFanin, i ) Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy ); // create the only PO pNodePo = Abc_NtkCreatePo( pNtkNew ); Abc_ObjAddFanin( pNodePo, pNode->pCopy ); - Abc_NtkLogicStoreName( pNodePo, Abc_ObjName(pNode) ); + Abc_ObjAssignName( pNodePo, Abc_ObjName(pNode), NULL ); if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkCreateFromNode(): Network check has failed.\n" ); return pNtkNew; @@ -686,7 +622,7 @@ Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop ) nVars = Abc_SopGetVarNum( pSop ); vNames = Abc_NodeGetFakeNames( nVars ); for ( i = 0; i < nVars; i++ ) - Abc_NtkLogicStoreName( Abc_NtkCreatePi(pNtkNew), Vec_PtrEntry(vNames, i) ); + Abc_ObjAssignName( Abc_NtkCreatePi(pNtkNew), Vec_PtrEntry(vNames, i), NULL ); Abc_NodeFreeNames( vNames ); // create the node, add PIs as fanins, set the function pNode = Abc_NtkCreateNode( pNtkNew ); @@ -696,7 +632,7 @@ Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop ) // create the only PO pNodePo = Abc_NtkCreatePo(pNtkNew); Abc_ObjAddFanin( pNodePo, pNode ); - Abc_NtkLogicStoreName( pNodePo, "F" ); + Abc_ObjAssignName( pNodePo, "F", NULL ); if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkCreateWithNode(): Network check has failed.\n" ); return pNtkNew; @@ -765,7 +701,6 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) Vec_PtrFree( pNtk->vCis ); Vec_PtrFree( pNtk->vCos ); Vec_PtrFree( pNtk->vAsserts ); - Vec_PtrFree( pNtk->vLatches ); Vec_PtrFree( pNtk->vObjs ); Vec_PtrFree( pNtk->vCutSet ); Vec_PtrFree( pNtk->vBoxes ); diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index 27f5040c..48b6b187 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -99,7 +99,7 @@ void Abc_ObjRecycle( Abc_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NtkObjAdd( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ) +Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ) { Abc_Obj_t * pObj; // create new object, assign ID, and add to the array @@ -139,16 +139,14 @@ Abc_Obj_t * Abc_NtkObjAdd( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ) Vec_PtrPush( pNtk->vCos, pObj ); break; case ABC_OBJ_NET: - break; case ABC_OBJ_NODE: + case ABC_OBJ_GATE: break; case ABC_OBJ_LATCH: pObj->pData = (void *)ABC_INIT_NONE; - Vec_PtrPush( pNtk->vLatches, pObj ); - Vec_PtrPush( pNtk->vCis, pObj ); - Vec_PtrPush( pNtk->vCos, pObj ); - break; - case ABC_OBJ_BOX: + case ABC_OBJ_TRI: + case ABC_OBJ_BLACKBOX: + Vec_PtrPush( pNtk->vBoxes, pObj ); break; default: assert(0); @@ -189,8 +187,8 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj ) pNtk->nObjCounts[pObj->Type]--; pNtk->nObjs--; // remove from the table of names -// if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) ) -// Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id); + if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) ) + Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id); // perform specialized operations depending on the object type switch (pObj->Type) { @@ -222,7 +220,7 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj ) Vec_PtrRemove( pNtk->vCos, pObj ); break; case ABC_OBJ_NET: - pObj->pData = NULL; + case ABC_OBJ_GATE: break; case ABC_OBJ_NODE: if ( Abc_NtkHasBdd(pNtk) ) @@ -230,11 +228,9 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj ) pObj->pData = NULL; break; case ABC_OBJ_LATCH: - Vec_PtrRemove( pNtk->vLatches, pObj ); - Vec_PtrRemove( pNtk->vCis, pObj ); - Vec_PtrRemove( pNtk->vCos, pObj ); - break; - case ABC_OBJ_BOX: + case ABC_OBJ_TRI: + case ABC_OBJ_BLACKBOX: + Vec_PtrRemove( pNtk->vBoxes, pObj ); break; default: assert(0); @@ -283,11 +279,21 @@ void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ) +Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName ) { Abc_Obj_t * pObjNew; // create the new object - pObjNew = Abc_NtkObjAdd( pNtkNew, pObj->Type ); + pObjNew = Abc_NtkCreateObj( pNtkNew, pObj->Type ); + // transfer names of the terminal objects + if ( fCopyName ) + { + if ( Abc_ObjIsCi(pObj) ) + Abc_ObjAssignName( pObjNew, Abc_ObjName(Abc_ObjFanout0Ntk(pObj)), NULL ); + else if ( Abc_ObjIsCo(pObj) ) + Abc_ObjAssignName( pObjNew, Abc_ObjName(Abc_ObjFanin0Ntk(pObj)), NULL ); + else if ( Abc_ObjIsBox(pObj) ) + Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL ); + } // copy functionality/names if ( Abc_ObjIsNode(pObj) ) // copy the function if functionality is compatible { @@ -308,7 +314,8 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ) } else if ( Abc_ObjIsNet(pObj) ) // copy the name { - pObjNew->pData = Nm_ManStoreIdName( pNtkNew->pManName, pObjNew->Id, pObj->pData, NULL ); + assert( 0 ); +// pObjNew->pData = Nm_ManStoreIdName( pNtkNew->pManName, pObjNew->Id, pObj->pData, NULL ); } else if ( Abc_ObjIsLatch(pObj) ) // copy the reset value pObjNew->pData = pObj->pData; @@ -318,6 +325,33 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ) /**Function************************************************************* + Synopsis [Duplicates the latch with its input/output terminals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName ) +{ + Abc_Obj_t * pTerm, * pBoxNew; + int i; + assert( Abc_ObjIsBox(pBox) ); + // duplicate the box + pBoxNew = Abc_NtkDupObj( pNtkNew, pBox, fCopyName ); + // duplicate the fanins and connect them + Abc_ObjForEachFanin( pBox, pTerm, i ) + Abc_ObjAddFanin( pBoxNew, Abc_NtkDupObj(pNtkNew, pTerm, fCopyName) ); + // duplicate the fanouts and connect them + Abc_ObjForEachFanout( pBox, pTerm, i ) + Abc_ObjAddFanin( Abc_NtkDupObj(pNtkNew, pTerm, fCopyName), pBoxNew ); + return pBoxNew; +} + +/**Function************************************************************* + Synopsis [Clones the objects in the same network but does not assign its function.] Description [] @@ -331,7 +365,7 @@ Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pObj ) { Abc_Obj_t * pClone, * pFanin; int i; - pClone = Abc_NtkObjAdd( pObj->pNtk, pObj->Type ); + pClone = Abc_NtkCreateObj( pObj->pNtk, pObj->Type ); Abc_ObjForEachFanin( pObj, pFanin, i ) Abc_ObjAddFanin( pClone, pFanin ); return pClone; @@ -351,34 +385,18 @@ Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pObj ) ***********************************************************************/ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ) { - Abc_Obj_t * pObj, * pDriver; - int i, Num; - // check if the node is among CIs - Abc_NtkForEachCi( pNtk, pObj, i ) - { - if ( strcmp( Abc_ObjName(pObj), pName ) == 0 ) - { - if ( i < Abc_NtkPiNum(pNtk) ) - printf( "Node \"%s\" is a primary input.\n", pName ); - else - printf( "Node \"%s\" is a latch output.\n", pName ); - return NULL; - } - } - // search the node among COs - Abc_NtkForEachCo( pNtk, pObj, i ) - { - if ( strcmp( Abc_ObjName(pObj), pName ) == 0 ) - { - pDriver = Abc_ObjFanin0(pObj); - if ( !Abc_ObjIsNode(pDriver) ) - { - printf( "Node \"%s\" does not have logic associated with it.\n", pName ); - return NULL; - } - return pDriver; - } - } + Abc_Obj_t * pObj; + int Num; + // try to find the terminal + Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_PO ); + if ( Num >= 0 ) + return Abc_NtkObj( pNtk, Num ); + Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO ); + if ( Num >= 0 ) + return Abc_NtkObj( pNtk, Num ); + Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_NODE ); + if ( Num >= 0 ) + return Abc_NtkObj( pNtk, Num ); // find the internal node if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' ) { @@ -421,7 +439,7 @@ Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName ) Abc_Obj_t * pNet; int ObjId; assert( Abc_NtkIsNetlist(pNtk) ); - ObjId = Nm_ManFindIdByName( pNtk->pManName, pName, NULL ); + ObjId = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_NET ); if ( ObjId == -1 ) return NULL; pNet = Abc_NtkObj( pNtk, ObjId ); @@ -430,29 +448,55 @@ Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName ) /**Function************************************************************* - Synopsis [Returns the CI/CO terminal with the given name.] + Synopsis [Returns CI with the given name.] - Description [] - - SideEffects [] + Description [] + + SideEffects [] - SeeAlso [] + SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName ) +Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName ) { - Abc_Obj_t * pNet; - int ObjId; + int Num; assert( !Abc_NtkIsNetlist(pNtk) ); - ObjId = Nm_ManFindIdByName( pNtk->pManName, pName, NULL ); - if ( ObjId == -1 ) - return NULL; - pNet = Abc_NtkObj( pNtk, ObjId ); - return pNet; + Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_PI ); + if ( Num >= 0 ) + return Abc_NtkObj( pNtk, Num ); + Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BI ); + if ( Num >= 0 ) + return Abc_NtkObj( pNtk, Num ); + return NULL; } /**Function************************************************************* + Synopsis [Returns CO with the given name.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName ) +{ + int Num; + assert( !Abc_NtkIsNetlist(pNtk) ); + Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_PO ); + if ( Num >= 0 ) + return Abc_NtkObj( pNtk, Num ); + Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO ); + if ( Num >= 0 ) + return Abc_NtkObj( pNtk, Num ); + return NULL; +} + + +/**Function************************************************************* + Synopsis [Finds or creates the net.] Description [] @@ -469,8 +513,9 @@ Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName ) if ( pName && (pNet = Abc_NtkFindNet( pNtk, pName )) ) return pNet; // create a new net - pNet = Abc_NtkObjAdd( pNtk, ABC_OBJ_NET ); - pNet->pData = pName? Nm_ManStoreIdName( pNtk->pManName, pNet->Id, pName, NULL ) : NULL; + pNet = Abc_NtkCreateObj( pNtk, ABC_OBJ_NET ); + if ( pName ) + Nm_ManStoreIdName( pNtk->pManName, pNet->Id, pNet->Type, pName, NULL ); return pNet; } diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 33025292..2dbfef33 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -47,7 +47,7 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pObj; int i; - if ( pNtk->nTravIds == (1<<8)-1 ) + if ( pNtk->nTravIds == (1<<30)-1 ) { pNtk->nTravIds = 0; Abc_NtkForEachObj( pNtk, pObj, i ) @@ -69,8 +69,8 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk ) ***********************************************************************/ void Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk ) { - Abc_Obj_t * pObj; - int i; + Abc_Obj_t * pObj, * pTerm; + int i, k; Vec_PtrClear( pNtk->vCis ); Vec_PtrClear( pNtk->vCos ); Abc_NtkForEachPi( pNtk, pObj, i ) @@ -79,10 +79,12 @@ void Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk ) Vec_PtrPush( pNtk->vCos, pObj ); Abc_NtkForEachAssert( pNtk, pObj, i ) Vec_PtrPush( pNtk->vCos, pObj ); - Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkForEachBox( pNtk, pObj, i ) { - Vec_PtrPush( pNtk->vCis, pObj ); - Vec_PtrPush( pNtk->vCos, pObj ); + Abc_ObjForEachFanin( pObj, pTerm, k ) + Vec_PtrPush( pNtk->vCos, pTerm ); + Abc_ObjForEachFanout( pObj, pTerm, k ) + Vec_PtrPush( pNtk->vCis, pTerm ); } } @@ -433,11 +435,34 @@ void Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk ) /**Function************************************************************* - Synopsis [Checks if the internal node has a unique CO.] + Synopsis [Checks if the internal node has CO fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NodeHasCoFanout( Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanout; + int i; + if ( !Abc_ObjIsNode(pNode) ) + return NULL; + Abc_ObjForEachFanout( pNode, pFanout, i ) + if ( Abc_ObjIsCo(pFanout) ) + return pFanout; + return NULL; +} + +/**Function************************************************************* + + Synopsis [Checks if the internal node has CO drivers with the same name.] - Description [Checks if the internal node can borrow a name from a CO - fanout. This is possible if there is only one CO with non-complemented - fanin edge pointing to this node.] + Description [Checks if the internal node can borrow a name from CO fanouts. + This is possible if all COs with non-complemented fanin edge pointing to this + node have the same name.] SideEffects [] @@ -447,23 +472,27 @@ void Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk ) Abc_Obj_t * Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode ) { Abc_Obj_t * pFanout, * pFanoutCo; - int i, Counter; + int i; if ( !Abc_ObjIsNode(pNode) ) return NULL; - Counter = 0; + pFanoutCo = NULL; Abc_ObjForEachFanout( pNode, pFanout, i ) { - if ( Abc_ObjIsCo(pFanout) && !Abc_ObjFaninC0(pFanout) ) + if ( !Abc_ObjIsCo(pFanout) ) + continue; + if ( Abc_ObjFaninC0(pFanout) ) + continue; + if ( pFanoutCo == NULL ) { assert( Abc_ObjFaninNum(pFanout) == 1 ); assert( Abc_ObjFanin0(pFanout) == pNode ); pFanoutCo = pFanout; - Counter++; + continue; } + if ( strcmp( Abc_ObjName(pFanoutCo), Abc_ObjName(pFanout) ) ) // they have diff names + return NULL; } - if ( Counter == 1 ) - return pFanoutCo; - return NULL; + return pFanoutCo; } /**Function************************************************************* @@ -508,7 +537,7 @@ bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk ) Description [The COs of a logic network are simple under three conditions: (1) The edge from the CO to its driver is not complemented. - (2) No two COs share the same driver. + (2) No two COs share the same driver (unless they have the same name!). (3) The driver is not a CI unless the CI and the CO have the same name (and so the inv/buf should not be written into a file). In some cases, such as FPGA mapping, we prevent the increase in delay @@ -537,15 +566,15 @@ int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate ) continue; } } - else + else if ( !Abc_ObjFaninC0(pNode) ) { - // skip the case when the driver's unique CO fanout is this CO - if ( Abc_NodeHasUniqueCoFanout(pDriver) == pNode ) + // skip the case when all CO fanouts of the driver have the same name + if ( Abc_NodeHasUniqueCoFanout(pDriver) ) continue; } if ( fDuplicate && !Abc_ObjIsCi(pDriver) ) { - pDriverNew = Abc_NtkDupObj( pNtk, pDriver ); + pDriverNew = Abc_NtkDupObj( pNtk, pDriver, 0 ); Abc_ObjForEachFanin( pDriver, pFanin, k ) Abc_ObjAddFanin( pDriverNew, pFanin ); if ( Abc_ObjFaninC0(pNode) ) @@ -1091,11 +1120,21 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk ) pNode->Id = Vec_PtrSize( vObjsNew ); Vec_PtrPush( vObjsNew, pNode ); } - // put latches next - Abc_NtkForEachLatch( pNtk, pNode, i ) + // put latches and their inputs/outputs next + Abc_NtkForEachBox( pNtk, pNode, i ) { pNode->Id = Vec_PtrSize( vObjsNew ); Vec_PtrPush( vObjsNew, pNode ); + Abc_ObjForEachFanin( pNode, pTemp, k ) + { + pTemp->Id = Vec_PtrSize( vObjsNew ); + Vec_PtrPush( vObjsNew, pTemp ); + } + Abc_ObjForEachFanout( pNode, pTemp, k ) + { + pTemp->Id = Vec_PtrSize( vObjsNew ); + Vec_PtrPush( vObjsNew, pTemp ); + } } // finally, internal nodes in the DFS order vNodes = Abc_AigDfs( pNtk, 1, 0 ); @@ -1139,6 +1178,7 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk ) ***********************************************************************/ void Abc_NtkDetectMatching( Abc_Ntk_t * pNtk ) { +/* Abc_Obj_t * pLatch, * pFanin; int i, nTFFs, nJKFFs; nTFFs = nJKFFs = 0; @@ -1157,13 +1197,6 @@ void Abc_NtkDetectMatching( Abc_Ntk_t * pNtk ) Abc_ObjFaninNum( Abc_ObjFanin1(pFanin) ) != 2 ) continue; -/* - if ( !Abc_ObjFaninC0(pLatch) || - !Abc_ObjFaninC0( Abc_ObjFanin0(pFanin) ) || - !Abc_ObjFaninC1( Abc_ObjFanin0(pFanin) ) ) - continue; -*/ - if ( (Abc_ObjFanin0(Abc_ObjFanin0(pFanin)) == pLatch || Abc_ObjFanin1(Abc_ObjFanin0(pFanin)) == pLatch) && (Abc_ObjFanin0(Abc_ObjFanin1(pFanin)) == pLatch || @@ -1174,6 +1207,7 @@ void Abc_NtkDetectMatching( Abc_Ntk_t * pNtk ) } printf( "D = %6d. T = %6d. JK = %6d. (%6.2f %%)\n", Abc_NtkLatchNum(pNtk), nTFFs, nJKFFs, 100.0 * nJKFFs / Abc_NtkLatchNum(pNtk) ); +*/ } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8cf0e0af..bbc9a226 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3901,8 +3901,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( argc == globalUtilOptind + 1 ) { - pNodeCo = Abc_NtkFindTerm( pNtk, argv[globalUtilOptind] ); - pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); + pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); if ( pNode == NULL ) { fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] ); @@ -7433,6 +7432,8 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); + printf( "This command is not implemented\n" ); + // set defaults nFrames = 1; fExdc = 1; @@ -7495,10 +7496,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - if ( fImp ) - pNtkRes = Abc_NtkVanImp( pNtk, nFrames, fExdc, fVerbose ); - else - pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose ); +// if ( fImp ) +// pNtkRes = Abc_NtkVanImp( pNtk, nFrames, fExdc, fVerbose ); +// else +// pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose ); + pNtkRes = NULL; if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential FPGA mapping has failed.\n" ); diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c index 1de087e8..650f379f 100644 --- a/src/base/abci/abcClpBdd.c +++ b/src/base/abci/abcClpBdd.c @@ -25,7 +25,6 @@ //////////////////////////////////////////////////////////////////////// static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ); -static Abc_Ntk_t * Abc_NtkFromGlobalBddsDual( Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ); //////////////////////////////////////////////////////////////////////// @@ -59,10 +58,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i } // create the new network - if ( fDualRail ) - pNtkNew = Abc_NtkFromGlobalBddsDual( pNtk ); - else - pNtkNew = Abc_NtkFromGlobalBdds( pNtk ); + pNtkNew = Abc_NtkFromGlobalBdds( pNtk ); Abc_NtkFreeGlobalBdds( pNtk ); if ( pNtkNew == NULL ) { @@ -134,42 +130,6 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFromGlobalBddsDual( Abc_Ntk_t * pNtk ) -{ - ProgressBar * pProgress; - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pNode, * pNodeNew; - DdManager * dd = pNtk->pManGlob; - int i; - // start the new network - pNtkNew = Abc_NtkStartFromDual( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); - // make sure the new manager has the same number of inputs - Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 ); - // process the POs - pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); - Abc_NtkForEachCo( pNtk, pNode, i ) - { - Extra_ProgressBarUpdate( pProgress, i, NULL ); - pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Cudd_Not( Vec_PtrEntry(pNtk->vFuncsGlob, i) ) ); - Abc_ObjAddFanin( pNode->pCopy->pCopy, pNodeNew ); - pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) ); - Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); - } - Extra_ProgressBarStop( pProgress ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Derives the network with the given global BDD.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ) { Abc_Obj_t * pNodeNew, * pTemp; diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 6538b360..dae5408d 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -502,6 +502,10 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i ) { pObjNew = Abc_NtkCreateLatch( pNtk ); + pFaninNew0 = Abc_NtkCreateBo( pNtk ); + pFaninNew1 = Abc_NtkCreateBi( pNtk ); + Abc_ObjAddFanin( pObjNew, pFaninNew0 ); + Abc_ObjAddFanin( pFaninNew1, pObjNew ); if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC ) Abc_LatchSetInitDc( pObjNew ); else if ( Ivy_ObjInit(pNode) == IVY_INIT_1 ) @@ -509,8 +513,9 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig else if ( Ivy_ObjInit(pNode) == IVY_INIT_0 ) Abc_LatchSetInit0( pObjNew ); else assert( 0 ); - pNode->TravId = Abc_EdgeFromNode( pObjNew ); + pNode->TravId = Abc_EdgeFromNode( pFaninNew1 ); } + Abc_NtkAddDummyBoxNames( pNtk ); // rebuild the AIG Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i ) { @@ -556,7 +561,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i ) { pFaninNew = Abc_ObjFanin0Ivy( pNtk, pNode ); - Abc_ObjAddFanin( Abc_NtkLatch(pNtk, i), pFaninNew ); + Abc_ObjAddFanin( Abc_ObjFanin0(Abc_NtkBox(pNtk, i)), pFaninNew ); } Vec_IntFree( vLatches ); Vec_IntFree( vNodes ); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index ff05fe69..ab61dd45 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -54,6 +54,8 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) { Abc_Ntk_t * pTemp = NULL; int fRemove1, fRemove2; + assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) ); // check that the networks have the same PIs/POs/latches if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fComb ) ) return NULL; @@ -139,12 +141,12 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk pObj = Abc_NtkCi(pNtk2, i); pObj->pCopy = pObjNew; // add name - Abc_NtkLogicStoreName( pObjNew, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL ); } // create the only PO pObjNew = Abc_NtkCreatePo( pNtkMiter ); // add the PO name - Abc_NtkLogicStoreName( pObjNew, "miter" ); + Abc_ObjAssignName( pObjNew, "miter", NULL ); } else { @@ -157,24 +159,28 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk pObj = Abc_NtkPi(pNtk2, i); pObj->pCopy = pObjNew; // add name - Abc_NtkLogicStoreName( pObjNew, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL ); } // create the only PO pObjNew = Abc_NtkCreatePo( pNtkMiter ); // add the PO name - Abc_NtkLogicStoreName( pObjNew, "miter" ); + Abc_ObjAssignName( pObjNew, "miter", NULL ); // create the latches Abc_NtkForEachLatch( pNtk1, pObj, i ) { - pObjNew = Abc_NtkDupObj( pNtkMiter, pObj ); - // add name - Abc_NtkLogicStoreNamePlus( pObjNew, Abc_ObjName(pObj), "_1" ); + pObjNew = Abc_NtkDupBox( pNtkMiter, pObj, 0 ); + // add names + Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), "_1" ); + Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pObj)), "_1" ); + Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pObj)), "_1" ); } Abc_NtkForEachLatch( pNtk2, pObj, i ) { - pObjNew = Abc_NtkDupObj( pNtkMiter, pObj ); + pObjNew = Abc_NtkDupBox( pNtkMiter, pObj, 0 ); // add name - Abc_NtkLogicStoreNamePlus( pObjNew, Abc_ObjName(pObj), "_2" ); + Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), "_2" ); + Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pObj)), "_2" ); + Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pObj)), "_2" ); } } } @@ -265,9 +271,9 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt } // connect new latches Abc_NtkForEachLatch( pNtk1, pNode, i ) - Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); + Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) ); Abc_NtkForEachLatch( pNtk2, pNode, i ) - Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); + Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) ); } // add the miter pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs ); @@ -302,6 +308,8 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) assert( 0 == Abc_NtkLatchNum(pNtk1) ); assert( 0 == Abc_NtkLatchNum(pNtk2) ); assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) ); // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); @@ -354,6 +362,7 @@ Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues ) assert( Abc_NtkIsStrash(pNtk) ); assert( 1 == Abc_NtkCoNum(pNtk) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk) ); // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); @@ -421,6 +430,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In assert( Out < Abc_NtkCoNum(pNtk) ); assert( In1 < Abc_NtkCiNum(pNtk) ); assert( In2 < Abc_NtkCiNum(pNtk) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk) ); // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); @@ -486,6 +496,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist ) assert( Abc_NtkIsStrash(pNtk) ); assert( 1 == Abc_NtkCoNum(pNtk) ); assert( In < Abc_NtkCiNum(pNtk) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk) ); // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); @@ -545,6 +556,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk ) Abc_Ntk_t * pNtkTemp; Abc_Obj_t * pObj; int i; + assert( Abc_NtkHasOnlyLatchBoxes(pNtk) ); Abc_NtkForEachPi( pNtk, pObj, i ) { @@ -663,34 +675,38 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) char Buffer[1000]; ProgressBar * pProgress; Abc_Ntk_t * pNtkFrames; - Abc_Obj_t * pLatch, * pLatchNew; + Abc_Obj_t * pLatch, * pLatchOut; int i, Counter; assert( nFrames > 0 ); assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkIsDfsOrdered(pNtk) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk) ); // start the new network pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames ); pNtkFrames->pName = Extra_UtilStrsav(Buffer); + // map the constant nodes + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); // create new latches (or their initial values) and remember them in the new latches if ( !fInitial ) { Abc_NtkForEachLatch( pNtk, pLatch, i ) - Abc_NtkDupObj( pNtkFrames, pLatch ); + Abc_NtkDupBox( pNtkFrames, pLatch, 1 ); } else { Counter = 0; Abc_NtkForEachLatch( pNtk, pLatch, i ) { + pLatchOut = Abc_ObjFanout0(pLatch); if ( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI { - pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames); - Abc_NtkLogicStoreName( pLatch->pCopy, Abc_ObjName(pLatch) ); + pLatchOut->pCopy = Abc_NtkCreatePi(pNtkFrames); + Abc_ObjAssignName( pLatchOut->pCopy, Abc_ObjName(pLatchOut), NULL ); Counter++; } else - pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) ); + pLatchOut->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) ); } if ( Counter ) printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter ); @@ -708,22 +724,15 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) // connect the new latches to the outputs of the last frame if ( !fInitial ) { + // we cannot use pLatch->pCopy here because pLatch->pCopy is used for temporary storage of strashed values Abc_NtkForEachLatch( pNtk, pLatch, i ) - { - pLatchNew = Abc_NtkLatch(pNtkFrames, i); - Abc_ObjAddFanin( pLatchNew, pLatch->pCopy ); - Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); - } + Abc_ObjAddFanin( Abc_ObjFanin0(pLatch)->pCopy, Abc_ObjFanout0(pLatch)->pCopy ); } - Abc_NtkForEachLatch( pNtk, pLatch, i ) - pLatch->pNext = NULL; // remove dangling nodes Abc_AigCleanup( pNtkFrames->pManFunc ); - // reorder the latches Abc_NtkOrderCisCos( pNtkFrames ); - // make sure that everything is okay if ( !Abc_NtkCheck( pNtkFrames ) ) { @@ -755,31 +764,29 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame ) int i; // create the prefix to be added to the node names sprintf( Buffer, "_%02d", iFrame ); - // map the constant nodes - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); // add the new PI nodes Abc_NtkForEachPi( pNtk, pNode, i ) - Abc_NtkLogicStoreNamePlus( Abc_NtkDupObj(pNtkFrames, pNode), Abc_ObjName(pNode), Buffer ); + Abc_ObjAssignName( Abc_NtkDupObj(pNtkFrames, pNode, 0), Abc_ObjName(pNode), Buffer ); // add the internal nodes Abc_AigForEachAnd( pNtk, pNode, i ) pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); // add the new POs Abc_NtkForEachPo( pNtk, pNode, i ) { - Abc_NtkLogicStoreNamePlus( Abc_NtkDupObj(pNtkFrames, pNode), Abc_ObjName(pNode), Buffer ); + Abc_ObjAssignName( Abc_NtkDupObj(pNtkFrames, pNode, 0), Abc_ObjName(pNode), Buffer ); Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); } // add the new asserts Abc_NtkForEachAssert( pNtk, pNode, i ) { - Abc_NtkLogicStoreNamePlus( Abc_NtkDupObj(pNtkFrames, pNode), Abc_ObjName(pNode), Buffer ); + Abc_ObjAssignName( Abc_NtkDupObj(pNtkFrames, pNode, 0), Abc_ObjName(pNode), Buffer ); Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); } - // transfer the implementation of the latch drivers to the latches + // transfer the implementation of the latch inputs to the latch outputs Abc_NtkForEachLatch( pNtk, pLatch, i ) - pLatch->pNext = Abc_ObjChild0Copy(pLatch); + pLatch->pCopy = Abc_ObjChild0Copy(Abc_ObjFanin0(pLatch)); Abc_NtkForEachLatch( pNtk, pLatch, i ) - pLatch->pCopy = pLatch->pNext; + Abc_ObjFanout0(pLatch)->pCopy = pLatch->pCopy; } @@ -797,6 +804,7 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg ) { +/* char Buffer[1000]; ProgressBar * pProgress; Abc_Ntk_t * pNtkFrames; @@ -825,7 +833,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram if ( Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI { pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames); - Abc_NtkLogicStoreName( pLatch->pCopy, Abc_ObjName(pLatch) ); + Abc_ObjAssignName( pLatch->pCopy, Abc_ObjName(pLatch), NULL ); Counter++; } else { @@ -854,9 +862,9 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram { Abc_NtkForEachLatch( pNtk, pLatch, i ) { - pLatchNew = Abc_NtkLatch(pNtkFrames, i); + pLatchNew = Abc_NtkBox(pNtkFrames, i); Abc_ObjAddFanin( pLatchNew, pLatch->pCopy ); - Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); + Abc_ObjAssignName( pLatchNew, Abc_ObjName(pLatch), NULL ); } } Abc_NtkForEachLatch( pNtk, pLatch, i ) @@ -876,6 +884,8 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram return NULL; } return pNtkFrames; +*/ + return NULL; } /**Function************************************************************* @@ -894,6 +904,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram ***********************************************************************/ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg ) { +/* char Buffer[10]; Abc_Obj_t * pNode, * pNodeNew, * pLatch; Abc_Obj_t * pConst1, * pConst1New; @@ -907,7 +918,7 @@ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec Abc_NtkForEachPi( pNtk, pNode, i ) { pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode ); - Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer ); + Abc_ObjAssignName( pNodeNew, Abc_ObjName(pNode), Buffer ); if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg); } // add the internal nodes @@ -925,7 +936,7 @@ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec { pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode ); Abc_ObjAddFanin( pNodeNew, Abc_ObjChild0Copy(pNode) ); - Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer ); + Abc_ObjAssignName( pNodeNew, Abc_ObjName(pNode), Buffer ); if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg); } // transfer the implementation of the latch drivers to the latches @@ -953,6 +964,7 @@ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec addFrameMapping(pLatch->pCopy, pLatch, iFrame+1, arg); } } +*/ } @@ -993,12 +1005,12 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk ) // add the PO corresponding to control input pPoNew = Abc_NtkCreatePo( pNtk ); Abc_ObjAddFanin( pPoNew, pNodeC ); - Abc_NtkLogicStoreName( pPoNew, "addOut1" ); + Abc_ObjAssignName( pPoNew, "addOut1", NULL ); // add the PO corresponding to other input pPoNew = Abc_NtkCreatePo( pNtk ); Abc_ObjAddFanin( pPoNew, pNodeB ); - Abc_NtkLogicStoreName( pPoNew, "addOut2" ); + Abc_ObjAssignName( pPoNew, "addOut2", NULL ); // mark the nodes in the first cone pNodeB = Abc_ObjRegular(pNodeB); @@ -1047,7 +1059,7 @@ int Abc_NtkOrPos( Abc_Ntk_t * pNtk ) // create the new PO pNode = Abc_NtkCreatePo( pNtk ); Abc_ObjAddFanin( pNode, pMiter ); - Abc_NtkLogicStoreName( pNode, "miter" ); + Abc_ObjAssignName( pNode, "miter", NULL ); // make sure that everything is okay if ( !Abc_NtkCheck( pNtk ) ) { diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index ac46501c..9a88db99 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -84,7 +84,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) ); // add the PIs corresponding to the names Vec_PtrForEachEntry( vNamesPi, pName, i ) - Abc_NtkLogicStoreName( Abc_NtkCreatePi(pNtk), pName ); + Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), pName, NULL ); // create the node pNode = Abc_NtkCreateNode( pNtk ); pNode->pData = Cudd_bddTransfer( dd, pNtk->pManFunc, bFunc ); Cudd_Ref(pNode->pData); @@ -93,7 +93,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo // create the only PO pNodePo = Abc_NtkCreatePo( pNtk ); Abc_ObjAddFanin( pNodePo, pNode ); - Abc_NtkLogicStoreName( pNodePo, pNamePo ); + Abc_ObjAssignName( pNodePo, pNamePo, NULL ); // make the network minimum base Abc_NtkMinimumBase( pNtk ); if ( vNamesPiFake ) @@ -246,7 +246,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly { ProgressBar * pProgress; Vec_Ptr_t * vFuncsGlob; - Abc_Obj_t * pNode, * pFanin; + Abc_Obj_t * pObj, * pFanin; DdNode * bFunc; DdManager * dd; int i, k, Counter; @@ -264,17 +264,17 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly // clean storage for local BDDs Abc_NtkCleanCopy( pNtk ); // set the elementary variables - Abc_NtkForEachCi( pNtk, pNode, i ) - if ( Abc_ObjFanoutNum(pNode) > 0 ) + Abc_NtkForEachCi( pNtk, pObj, i ) + if ( Abc_ObjFanoutNum(pObj) > 0 ) { - pNode->pCopy = (Abc_Obj_t *)dd->vars[i]; + pObj->pCopy = (Abc_Obj_t *)dd->vars[i]; Cudd_Ref( dd->vars[i] ); } // assign the constant node BDD - pNode = Abc_AigConst1(pNtk); - if ( Abc_ObjFanoutNum(pNode) > 0 ) + pObj = Abc_AigConst1(pNtk); + if ( Abc_ObjFanoutNum(pObj) > 0 ) { - pNode->pCopy = (Abc_Obj_t *)dd->one; + pObj->pCopy = (Abc_Obj_t *)dd->one; Cudd_Ref( dd->one ); } @@ -285,9 +285,9 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly { // construct the BDDs pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) ); - Abc_NtkForEachLatch( pNtk, pNode, i ) + Abc_NtkForEachLatchInput( pNtk, pObj, i ) { - bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose ); + bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pObj), nBddSizeMax, pProgress, &Counter, fVerbose ); if ( bFunc == NULL ) { if ( fVerbose ) @@ -296,7 +296,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly Cudd_Quit( dd ); return NULL; } - bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc ); + bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pObj) ); Cudd_Ref( bFunc ); Vec_PtrPush( vFuncsGlob, bFunc ); } Extra_ProgressBarStop( pProgress ); @@ -305,9 +305,9 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly { // construct the BDDs pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) ); - Abc_NtkForEachCo( pNtk, pNode, i ) + Abc_NtkForEachCo( pNtk, pObj, i ) { - bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose ); + bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pObj), nBddSizeMax, pProgress, &Counter, fVerbose ); if ( bFunc == NULL ) { if ( fVerbose ) @@ -316,34 +316,35 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly Cudd_Quit( dd ); return NULL; } - bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc ); + bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pObj) ); Cudd_Ref( bFunc ); Vec_PtrPush( vFuncsGlob, bFunc ); } Extra_ProgressBarStop( pProgress ); } /* // derefence the intermediate BDDs - Abc_NtkForEachNode( pNtk, pNode, i ) - if ( pNode->pCopy ) + Abc_NtkForEachNode( pNtk, pObj, i ) + if ( pObj->pCopy ) { - Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy ); - pNode->pCopy = NULL; + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pCopy ); + pObj->pCopy = NULL; } */ /* // make sure all nodes are derefed - Abc_NtkForEachObj( pNtk, pNode, i ) + Abc_NtkForEachObj( pNtk, pObj, i ) { - if ( pNode->pCopy != NULL ) - printf( "Abc_NtkGlobalBdds() error: Node %d has BDD assigned\n", pNode->Id ); - if ( pNode->vFanouts.nSize > 0 ) - printf( "Abc_NtkGlobalBdds() error: Node %d has refs assigned\n", pNode->Id ); + if ( pObj->pCopy != NULL ) + printf( "Abc_NtkGlobalBdds() error: Node %d has BDD assigned\n", pObj->Id ); + if ( pObj->vFanouts.nSize > 0 ) + printf( "Abc_NtkGlobalBdds() error: Node %d has refs assigned\n", pObj->Id ); } */ // reset references - Abc_NtkForEachObj( pNtk, pNode, i ) - Abc_ObjForEachFanin( pNode, pFanin, k ) - pFanin->vFanouts.nSize++; + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) ) + Abc_ObjForEachFanin( pObj, pFanin, k ) + pFanin->vFanouts.nSize++; // reorder one more time if ( fReorder ) diff --git a/src/base/abci/abcOrder.c b/src/base/abci/abcOrder.c index c9ebdc12..04417f77 100644 --- a/src/base/abci/abcOrder.c +++ b/src/base/abci/abcOrder.c @@ -70,7 +70,7 @@ void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, vSupp = Vec_PtrAlloc( Abc_NtkCiNum(pNtk) ); while ( fscanf( pFile, "%s", Buffer ) == 1 ) { - pObj = Abc_NtkFindTerm( pNtk, Buffer ); + pObj = Abc_NtkFindCi( pNtk, Buffer ); if ( pObj == NULL || !Abc_ObjIsCi(pObj) ) { printf( "Name \"%s\" is not a PI name. Cannot use this order.\n", Buffer ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index e3bb764d..81059a0f 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -247,7 +247,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ) assert( Init < 4 ); InitNums[Init]++; - pFanin = Abc_ObjFanin0(pLatch); + pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch)); if ( !Abc_ObjIsNode(pFanin) || !Abc_NodeIsConst(pFanin) ) continue; diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 9fcc6979..61be3dee 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -147,9 +147,9 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd if ( fUpdateLevel ) Abc_NtkStartReverseLevels( pNtk ); - if ( Abc_NtkLatchNum(pNtk) ) - Abc_NtkForEachLatch(pNtk, pNode, i) - pNode->pNext = pNode->pData; +// if ( Abc_NtkLatchNum(pNtk) ) +// Abc_NtkForEachLatch(pNtk, pNode, i) +// pNode->pNext = pNode->pData; // resynthesize each node once nNodes = Abc_NtkObjNumMax(pNtk); @@ -221,9 +221,9 @@ pManRes->timeTotal = clock() - clkStart; Abc_NtkForEachObj( pNtk, pNode, i ) pNode->pData = NULL; - if ( Abc_NtkLatchNum(pNtk) ) - Abc_NtkForEachLatch(pNtk, pNode, i) - pNode->pData = pNode->pNext, pNode->pNext = NULL; +// if ( Abc_NtkLatchNum(pNtk) ) +// Abc_NtkForEachLatch(pNtk, pNode, i) +// pNode->pData = pNode->pNext, pNode->pNext = NULL; // put the nodes into the DFS order and reassign their IDs Abc_NtkReassignIds( pNtk ); diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c index 03073075..63beac6c 100644 --- a/src/base/abci/abcRr.c +++ b/src/base/abci/abcRr.c @@ -106,8 +106,8 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa p->nNodesOld = Abc_NtkNodeNum(pNtk); p->nLevelsOld = Abc_AigGetLevelNum(pNtk); // remember latch values - Abc_NtkForEachLatch( pNtk, pNode, i ) - pNode->pNext = pNode->pData; +// Abc_NtkForEachLatch( pNtk, pNode, i ) +// pNode->pNext = pNode->pData; // go through the nodes Abc_NtkCleanCopy(pNtk); nNodes = Abc_NtkObjNumMax(pNtk); @@ -216,8 +216,8 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa Abc_RRManPrintStats( p ); Abc_RRManStop( p ); // restore latch values - Abc_NtkForEachLatch( pNtk, pNode, i ) - pNode->pData = pNode->pNext, pNode->pNext = NULL; +// Abc_NtkForEachLatch( pNtk, pNode, i ) +// pNode->pData = pNode->pNext, pNode->pNext = NULL; // put the nodes into the DFS order and reassign their IDs Abc_NtkReassignIds( pNtk ); Abc_NtkGetLevelNum( pNtk ); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index c54ea33c..d00be668 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -327,7 +327,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ) pPoNew = Abc_NtkCreatePo(pNtkNew); Abc_ObjAddFanin( pPoNew, pObjNew ); Abc_NtkAddDummyPiNames( pNtkNew ); - Abc_NtkLogicStoreName( pPoNew, Abc_ObjName(Abc_NtkPo(pNtk, 0)) ); + Abc_ObjAssignName( pPoNew, Abc_ObjName(Abc_NtkPo(pNtk, 0)), NULL ); // make sure everything is okay if ( !Abc_NtkCheck( pNtkNew ) ) { diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index 8f1ab180..7c6df88a 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -59,11 +59,31 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose ) Abc_Ntk_t * pNtkAig; Fraig_Man_t * pMan; stmm_table * tEquiv; + Abc_Obj_t * pObj; + int i, fUseTrick; assert( !Abc_NtkIsStrash(pNtk) ); + // save gate assignments + fUseTrick = 0; + if ( Abc_NtkIsMappedLogic(pNtk) ) + { + fUseTrick = 1; + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pNext = pObj->pData; + } // derive the AIG pNtkAig = Abc_NtkStrash( pNtk, 0, 1 ); + // reconstruct gate assignments + if ( fUseTrick ) + { + extern void * Abc_FrameReadLibGen(); + Aig_ManStop( pNtk->pManFunc ); + pNtk->pManFunc = Abc_FrameReadLibGen(); + pNtk->ntkFunc = ABC_FUNC_MAP; + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pData = pObj->pNext, pObj->pNext = NULL; + } // perform fraiging of the AIG Fraig_ParamsSetDefault( &Params ); @@ -176,8 +196,8 @@ stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose ) // skip the dangling nodes if ( pNodeAig == NULL ) continue; - // skip the nodes that fanout into POs - if ( Abc_NodeHasUniqueCoFanout(pNode) ) + // skip the nodes that fanout into COs + if ( Abc_NodeHasCoFanout(pNode) ) continue; // get the FRAIG node gNode = Fraig_NotCond( Abc_ObjRegular(pNodeAig)->pCopy, Abc_ObjIsComplement(pNodeAig) ); diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c index 5add0dda..8364b783 100644 --- a/src/base/abci/abcTiming.c +++ b/src/base/abci/abcTiming.c @@ -254,9 +254,9 @@ void Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk ) continue; *pTime = pNtk->pManTime->tReqDef; } - // set the 0 arrival times for latches and constant nodes + // set the 0 arrival times for latch outputs and constant nodes ppTimes = (Abc_Time_t **)pNtk->pManTime->vArrs->pArray; - Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkForEachLatchOutput( pNtk, pObj, i ) { pTime = ppTimes[pObj->Id]; pTime->Fall = pTime->Rise = pTime->Worst = 0.0; diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index 156d9b3d..cced1c47 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -278,6 +278,7 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b ***********************************************************************/ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach ) { +/* Abc_Ntk_t * pNtkNew; Abc_Obj_t * pNode, * pNodeNew; int * pPermute; @@ -290,7 +291,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn // create PIs corresponding to LOs Abc_NtkForEachLatch( pNtk, pNode, i ) - Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode) ); + Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode), NULL ); // cannot ADD POs here because pLatch->pCopy point to the PIs // create a new node @@ -313,9 +314,9 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn // for each CO, create PO (skip POs equal to CIs because of name conflict) Abc_NtkForEachPo( pNtk, pNode, i ) if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) ) - Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode) ); + Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL ); Abc_NtkForEachLatch( pNtk, pNode, i ) - Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pNode, "_in") ); + Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pNode, "_in"), NULL ); // link to the POs of the network Abc_NtkForEachPo( pNtk, pNode, i ) @@ -337,6 +338,8 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn return NULL; } return pNtkNew; +*/ + return NULL; } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c deleted file mode 100644 index 50baa285..00000000 --- a/src/base/abci/abcVanEijk.c +++ /dev/null @@ -1,824 +0,0 @@ -/**CFile**************************************************************** - - FileName [abcVanEijk.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [Implementation of van Eijk's method for finding - signal correspondence: C. A. J. van Eijk. "Sequential equivalence - checking based on structural similarities", IEEE Trans. CAD, - vol. 19(7), July 2000, pp. 814-819.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - October 2, 2005.] - - Revision [$Id: abcVanEijk.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "fraig.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ); -static Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames ); -static Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame ); -static int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses ); -static void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses ); -static int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ); -static void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses ); - -extern Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ); -extern void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); -extern Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); - -static Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ); - -//////////////////////////////////////////////////////////////////////// -/// INLINED FUNCTIONS /// -//////////////////////////////////////////////////////////////////////// - -// sets the correspondence of the node in the frame -static inline void Abc_NodeVanEijkWriteCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame, Abc_Obj_t * pEntry ) -{ - Vec_PtrWriteEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id, pEntry ); -} -// returns the correspondence of the node in the frame -static inline Abc_Obj_t * Abc_NodeVanEijkReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) -{ - return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id ); -} -// returns the hash value of the node in the frame -static inline Abc_Obj_t * Abc_NodeVanEijkHash( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) -{ - return Abc_ObjRegular( Abc_NodeVanEijkReadCorresp(pNode, vCorresp, iFrame)->pCopy ); -} -// returns the representative node of the class to which the node belongs -static inline Abc_Obj_t * Abc_NodeVanEijkRepr( Abc_Obj_t * pNode ) -{ - if ( pNode->pNext == NULL ) - return NULL; - while ( pNode->pNext ) - pNode = pNode->pNext; - return pNode; -} - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Derives classes of sequentially equivalent nodes.] - - Description [Performs sequential sweep by combining the equivalent - nodes. Adds EXDC network to the current network to record the subset - of unreachable states computed by identifying the equivalent nodes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ) -{ - Fraig_Params_t Params; - Abc_Ntk_t * pNtkSingle; - Vec_Ptr_t * vClasses; - Abc_Ntk_t * pNtkNew; - - assert( Abc_NtkIsStrash(pNtk) ); - - // FRAIG the network to get rid of combinational equivalences - Fraig_ParamsSetDefaultFull( &Params ); - pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 ); - Abc_AigSetNodePhases( pNtkSingle ); - Abc_NtkCleanNext(pNtkSingle); - - // get the equivalence classes - vClasses = Abc_NtkVanEijkClasses( pNtkSingle, nFrames, fVerbose ); - if ( Vec_PtrSize(vClasses) > 0 ) - { - // transform the network by merging nodes in the equivalence classes - pNtkNew = Abc_NtkVanEijkFrames( pNtkSingle, NULL, 1, 0, 1 ); -// pNtkNew = Abc_NtkDup( pNtkSingle ); - // derive the EXDC network if asked - if ( fExdc ) - pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtkSingle, vClasses ); - } - else - pNtkNew = Abc_NtkDup( pNtkSingle ); - Abc_NtkVanEijkClassesTest( pNtkSingle, vClasses ); - Vec_PtrFree( vClasses ); - - Abc_NtkDelete( pNtkSingle ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Derives the classes of sequentially equivalent nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVerbose ) -{ - Fraig_Man_t * pFraig; - Abc_Ntk_t * pNtkMulti; - Vec_Ptr_t * vCorresp, * vClasses; - int nIter, RetValue; - int nAddFrames = 0; - - if ( fVerbose ) - printf( "The number of ANDs after FRAIGing = %d.\n", Abc_NtkNodeNum(pNtkSingle) ); - - // get the AIG of the base case - vCorresp = Vec_PtrAlloc( 100 ); - pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames + nAddFrames, 0, 0 ); - if ( fVerbose ) - printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + nAddFrames, Abc_NtkNodeNum(pNtkMulti) ); - - // FRAIG the initialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys) - pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 1 ); - Fraig_ManFree( pFraig ); - - // find initial equivalence classes - vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames + nAddFrames ); - if ( fVerbose ) - printf( "The number of classes in the base case = %5d. Pairs = %8d.\n", Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) ); - Abc_NtkDelete( pNtkMulti ); - - // refine the classes using iterative FRAIGing - for ( nIter = 1; Vec_PtrSize(vClasses) > 0; nIter++ ) - { - // derive the network with equivalence classes - Abc_NtkVanEijkClassesOrder( vClasses ); - pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 1, 0 ); - // simulate with classes (TO DO) - - // FRAIG the unitialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys) - pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 0 ); - Fraig_ManFree( pFraig ); - - // refine the classes - RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, nFrames, vClasses ); - Abc_NtkDelete( pNtkMulti ); - if ( fVerbose ) - printf( "The number of classes after %2d iterations = %5d. Pairs = %8d.\n", nIter, Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) ); - // quit if there is no change - if ( RetValue == 0 ) - break; - } - Vec_PtrFree( vCorresp ); - - if ( fVerbose ) - { - Abc_Obj_t * pObj, * pClass; - int i, Counter; - printf( "The classes are: " ); - Vec_PtrForEachEntry( vClasses, pClass, i ) - { - Counter = 0; - for ( pObj = pClass; pObj; pObj = pObj->pNext ) - Counter++; - printf( " %d", Counter ); -/* - printf( " = {" ); - for ( pObj = pClass; pObj; pObj = pObj->pNext ) - printf( " %d", pObj->Id ); - printf( " } " ); -*/ - } - printf( "\n" ); - } - return vClasses; -} - -/**Function************************************************************* - - Synopsis [Computes the equivalence classes of nodes using the base case.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vCorresp, int nFrames ) -{ - Vec_Ptr_t * vClasses; - int i, RetValue; - // derive the classes for the last frame - vClasses = Abc_NtkVanEijkClassesDeriveFirst( pNtkSingle, vCorresp, nFrames - 1 ); - // refine the classes using other timeframes - for ( i = 0; i < nFrames - 1; i++ ) - { - if ( Vec_PtrSize(vClasses) == 0 ) - break; - RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, i, vClasses ); -// if ( RetValue ) -// printf( " yes%s", (i==nFrames-2 ? "\n":"") ); -// else -// printf( " no%s", (i==nFrames-2 ? "\n":"") ); - } - return vClasses; -} - - -/**Function************************************************************* - - Synopsis [Computes the equivalence classes of nodes.] - - Description [Original network (pNtk) is mapped into the unfolded frames - using given array of nodes (vCorresp). Each node in the unfolded frames - is mapped into a FRAIG node (pNode->pCopy). This procedure uses next - pointers (pNode->pNext) to combine the nodes into equivalence classes. - Each class is represented by its representative node with the minimum level. - Only the last frame is considered.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame ) -{ - Abc_Obj_t * pNode, * pKey, ** ppSlot; - stmm_table * tTable; - stmm_generator * gen; - Vec_Ptr_t * vClasses; - int i; - // start the table hashing FRAIG nodes into classes of original network nodes - tTable = stmm_init_table( st_ptrcmp, st_ptrhash ); - // create the table - Abc_NtkCleanNext( pNtk ); - Abc_NtkForEachObj( pNtk, pNode, i ) - { - if ( Abc_ObjIsPo(pNode) ) - continue; - pKey = Abc_NodeVanEijkHash( pNode, vCorresp, iFrame ); - if ( !stmm_find_or_add( tTable, (char *)pKey, (char ***)&ppSlot ) ) - *ppSlot = NULL; - pNode->pNext = *ppSlot; - *ppSlot = pNode; - } - // collect only non-trivial classes - vClasses = Vec_PtrAlloc( 100 ); - stmm_foreach_item( tTable, gen, (char **)&pKey, (char **)&pNode ) - if ( pNode->pNext ) - Vec_PtrPush( vClasses, pNode ); - stmm_free_table( tTable ); - return vClasses; -} - -/**Function************************************************************* - - Synopsis [Refines the classes using one frame.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses ) -{ - Abc_Obj_t * pHeadSame, ** ppTailSame; - Abc_Obj_t * pHeadDiff, ** ppTailDiff; - Abc_Obj_t * pNode, * pClass, * pKey; - int i, k, fChange = 0; - Vec_PtrForEachEntry( vClasses, pClass, i ) - { -// assert( pClass->pNext ); - pKey = Abc_NodeVanEijkHash( pClass, vCorresp, iFrame ); - for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext ) - if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey ) - break; - if ( pNode == NULL ) - continue; - fChange = 1; - // create two classes - pHeadSame = NULL; ppTailSame = &pHeadSame; - pHeadDiff = NULL; ppTailDiff = &pHeadDiff; - for ( pNode = pClass; pNode; pNode = pNode->pNext ) - if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey ) - *ppTailDiff = pNode, ppTailDiff = &pNode->pNext; - else - *ppTailSame = pNode, ppTailSame = &pNode->pNext; - *ppTailSame = NULL; - *ppTailDiff = NULL; - assert( pHeadSame && pHeadDiff ); - // put the updated class back - Vec_PtrWriteEntry( vClasses, i, pHeadSame ); - // append the new class to be processed later - Vec_PtrPush( vClasses, pHeadDiff ); - } - // remove trivial classes - k = 0; - Vec_PtrForEachEntry( vClasses, pClass, i ) - if ( pClass->pNext ) - Vec_PtrWriteEntry( vClasses, k++, pClass ); - Vec_PtrShrink( vClasses, k ); - return fChange; -} - -/**Function************************************************************* - - Synopsis [Orders nodes in the equivalence classes.] - - Description [Finds a min-level representative of each class and puts it last.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses ) -{ - Abc_Obj_t * pClass, * pNode, * pPrev, * pNodeMin, * pPrevMin; - int i; - // go through the classes - Vec_PtrForEachEntry( vClasses, pClass, i ) - { - assert( pClass->pNext ); - pPrevMin = NULL; - pNodeMin = pClass; - for ( pPrev = pClass, pNode = pClass->pNext; pNode; pPrev = pNode, pNode = pNode->pNext ) - if ( pNodeMin->Level >= pNode->Level ) - { - pPrevMin = pPrev; - pNodeMin = pNode; - } - if ( pNodeMin->pNext == NULL ) // already last - continue; - // update the class - if ( pNodeMin == pClass ) - Vec_PtrWriteEntry( vClasses, i, pNodeMin->pNext ); - else - pPrevMin->pNext = pNodeMin->pNext; - // attach the min node - assert( pPrev->pNext == NULL ); - pPrev->pNext = pNodeMin; - pNodeMin->pNext = NULL; - } - Vec_PtrForEachEntry( vClasses, pClass, i ) - assert( pClass->pNext ); -} - -/**Function************************************************************* - - Synopsis [Counts pairs of equivalent nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ) -{ - Abc_Obj_t * pClass, * pNode; - int i, nPairs = 0; - Vec_PtrForEachEntry( vClasses, pClass, i ) - { - assert( pClass->pNext ); - for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext ) - nPairs++; - } - return nPairs; -} - -/**Function************************************************************* - - Synopsis [Sanity check for the class representation.] - - Description [Checks that pNode->pNext is only used in the classes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses ) -{ - Abc_Obj_t * pClass, * pObj; - int i; - Abc_NtkCleanCopy( pNtkSingle ); - Vec_PtrForEachEntry( vClasses, pClass, i ) - for ( pObj = pClass; pObj; pObj = pObj->pNext ) - if ( pObj->pNext ) - pObj->pCopy = (Abc_Obj_t *)1; - Abc_NtkForEachObj( pNtkSingle, pObj, i ) - assert( (pObj->pCopy != NULL) == (pObj->pNext != NULL) ); - Abc_NtkCleanCopy( pNtkSingle ); -} - - -/**Function************************************************************* - - Synopsis [Performs DFS for one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanEijkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) -{ - Abc_Obj_t * pRepr; - // skip CI and const - if ( Abc_ObjFaninNum(pNode) < 2 ) - return; - // if this node is already visited, skip - if ( Abc_NodeIsTravIdCurrent( pNode ) ) - return; - // mark the node as visited - Abc_NodeSetTravIdCurrent( pNode ); - assert( Abc_ObjIsNode( pNode ) ); - // check if the node belongs to the class - if ( pRepr = Abc_NodeVanEijkRepr(pNode) ) - Abc_NtkVanEijkDfs_rec( pRepr, vNodes ); - else - { - Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pNode), vNodes ); - Abc_NtkVanEijkDfs_rec( Abc_ObjFanin1(pNode), vNodes ); - } - // add the node after the fanins have been added - Vec_PtrPush( vNodes, pNode ); -} - -/**Function************************************************************* - - Synopsis [Finds DFS ordering of nodes using equivalence classes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NtkVanEijkDfs( Abc_Ntk_t * pNtk ) -{ - Vec_Ptr_t * vNodes; - Abc_Obj_t * pObj; - int i; - vNodes = Vec_PtrAlloc( 100 ); - Abc_NtkIncrementTravId( pNtk ); - Abc_NtkForEachCo( pNtk, pObj, i ) - Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pObj), vNodes ); - return vNodes; -} - - -/**Function************************************************************* - - Synopsis [Derives the timeframes of the network.] - - Description [Returns mapping of the orig nodes into the frame nodes (vCorresp).] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ) -{ - char Buffer[100]; - Abc_Ntk_t * pNtkFrames; - Abc_Obj_t * pLatch, * pLatchNew; - Vec_Ptr_t * vOrder; - int i; - assert( nFrames > 0 ); - assert( Abc_NtkIsStrash(pNtk) ); - assert( Abc_NtkIsDfsOrdered(pNtk) ); - // clean the array of connections - if ( vCorresp ) - Vec_PtrFill( vCorresp, (nFrames + fAddLast)*Abc_NtkObjNumMax(pNtk), NULL ); - // start the new network - pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); - if ( fShortNames ) - { - pNtkFrames->pName = Extra_UtilStrsav(pNtk->pName); - pNtkFrames->pSpec = Extra_UtilStrsav(pNtk->pSpec); - } - else - { - sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames + fAddLast ); - pNtkFrames->pName = Extra_UtilStrsav(Buffer); - } - // map the constant nodes - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); - // create new latches and remember them in the new latches - Abc_NtkForEachLatch( pNtk, pLatch, i ) - Abc_NtkDupObj( pNtkFrames, pLatch ); - // collect nodes in such a way each class representative goes first - vOrder = Abc_NtkVanEijkDfs( pNtk ); - // create the timeframes - for ( i = 0; i < nFrames; i++ ) - Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, i, vCorresp, vOrder, fShortNames ); - Vec_PtrFree( vOrder ); - // add one more timeframe without class info - if ( fAddLast ) - Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, nFrames, vCorresp, NULL, fShortNames ); - // connect the new latches to the outputs of the last frame - Abc_NtkForEachLatch( pNtk, pLatch, i ) - { - pLatchNew = Abc_NtkLatch(pNtkFrames, i); - Abc_ObjAddFanin( pLatchNew, pLatch->pCopy ); - Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); - pLatch->pNext = NULL; - } - // remove dangling nodes -// Abc_AigCleanup( pNtkFrames->pManFunc ); - // otherwise some external nodes may have dandling pointers - - // make sure that everything is okay - if ( !Abc_NtkCheck( pNtkFrames ) ) - printf( "Abc_NtkVanEijkFrames: The network check has failed.\n" ); - return pNtkFrames; -} - -/**Function************************************************************* - - Synopsis [Adds one time frame to the new network.] - - Description [If the ordering of nodes is given, uses it. Otherwise, - uses the DSF order of the nodes in the network.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ) -{ - char Buffer[10]; - Abc_Obj_t * pNode, * pLatch, * pRepr; - Vec_Ptr_t * vTemp; - int i; - // create the prefix to be added to the node names - sprintf( Buffer, "_%02d", iFrame ); - // add the new PI nodes - Abc_NtkForEachPi( pNtk, pNode, i ) - { - pNode->pCopy = Abc_NtkCreatePi(pNtkFrames); - if ( fShortNames ) - Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); - else - Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer ); - } - // remember the CI mapping - if ( vCorresp ) - { - pNode = Abc_AigConst1(pNtk); - Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); - Abc_NtkForEachCi( pNtk, pNode, i ) - Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); - } - // go through the nodes in the given order or in the natural order - if ( vOrder ) - { - // add the internal nodes - Vec_PtrForEachEntry( vOrder, pNode, i ) - { - if ( pRepr = Abc_NodeVanEijkRepr(pNode) ) - pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pNode->fPhase ^ pRepr->fPhase ); - else - pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); - assert( Abc_ObjRegular(pNode->pCopy) != NULL ); - if ( vCorresp ) - Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); - } - } - else - { - // add the internal nodes - Abc_AigForEachAnd( pNtk, pNode, i ) - { - pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); - assert( Abc_ObjRegular(pNode->pCopy) != NULL ); - if ( vCorresp ) - Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); - } - } - // add the new POs - Abc_NtkForEachPo( pNtk, pNode, i ) - { - pNode->pCopy = Abc_NtkCreatePo(pNtkFrames); - Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); - if ( fShortNames ) - Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); - else - Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer ); - } - // transfer the implementation of the latch drivers to the latches - vTemp = Vec_PtrAlloc( 100 ); - Abc_NtkForEachLatch( pNtk, pLatch, i ) - Vec_PtrPush( vTemp, Abc_ObjChild0Copy(pLatch) ); - Abc_NtkForEachLatch( pNtk, pLatch, i ) - pLatch->pCopy = Vec_PtrEntry( vTemp, i ); - Vec_PtrFree( vTemp ); - - Abc_AigForEachAnd( pNtk, pNode, i ) - pNode->pCopy = NULL; -} - -/**Function************************************************************* - - Synopsis [Fraigs the network with or without initialization.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ) -{ - Fraig_Man_t * pMan; - Fraig_Params_t Params; - ProgressBar * pProgress; - Abc_Obj_t * pNode; - int i; - assert( Abc_NtkIsStrash(pMulti) ); - // create the FRAIG manager - Fraig_ParamsSetDefaultFull( &Params ); - pMan = Fraig_ManCreate( &Params ); - // clean the copy fields in the old network - Abc_NtkCleanCopy( pMulti ); - // map the constant nodes - Abc_AigConst1(pMulti)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); - if ( fInit ) - { - // map the PI nodes - Abc_NtkForEachPi( pMulti, pNode, i ) - pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i); - // map the latches - Abc_NtkForEachLatch( pMulti, pNode, i ) - pNode->pCopy = (Abc_Obj_t *)Fraig_NotCond( Fraig_ManReadConst1(pMan), !Abc_LatchIsInit1(pNode) ); - } - else - { - // map the CI nodes - Abc_NtkForEachCi( pMulti, pNode, i ) - pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i); - } - // perform fraiging - pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pMulti) ); - Abc_AigForEachAnd( pMulti, pNode, i ) - { - Extra_ProgressBarUpdate( pProgress, i, NULL ); - pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, - Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ), - Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) ); - } - Extra_ProgressBarStop( pProgress ); - return pMan; -} - - -/**Function************************************************************* - - Synopsis [Create EXDC from the equivalence classes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;//, *pObjNew; - Abc_Obj_t * pMiter, * pTotal; - Vec_Ptr_t * vCone; - int i, k; - - assert( Abc_NtkIsStrash(pNtk) ); - - // start the network - pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); - pNtkNew->pName = Extra_UtilStrsav("exdc"); - pNtkNew->pSpec = NULL; - - // map the constant nodes - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - // for each CI, create PI - Abc_NtkForEachCi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) ); - // cannot add latches here because pLatch->pCopy pointers are used - - // create the cones for each pair of nodes in an equivalence class - pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); - Vec_PtrForEachEntry( vClasses, pClass, i ) - { - assert( pClass->pNext ); - // get the cone for the representative node - pRepr = Abc_NodeVanEijkRepr( pClass ); - if ( Abc_ObjFaninNum(pRepr) == 2 ) - { - vCone = Abc_NtkDfsNodes( pNtk, &pRepr, 1 ); - Vec_PtrForEachEntry( vCone, pObj, k ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - Vec_PtrFree( vCone ); - assert( pObj == pRepr ); - } - // go through the node pairs (representative is last in the list) - for ( pNode = pClass; pNode != pRepr; pNode = pNode->pNext ) - { - // get the cone for the node - assert( Abc_ObjFaninNum(pNode) == 2 ); - vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); - Vec_PtrForEachEntry( vCone, pObj, k ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - Vec_PtrFree( vCone ); - assert( pObj == pNode ); - // complement if there is phase difference - pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase ^ pRepr->fPhase ); - // add the miter - pMiter = Abc_AigXor( pNtkNew->pManFunc, pRepr->pCopy, pNode->pCopy ); - } - // add the miter to the final - pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter ); - } - -/* - // create the only PO - pObjNew = Abc_NtkCreatePo( pNtkNew ); - // add the PO name - Abc_NtkLogicStoreName( pObjNew, "DC" ); - // add the PO - Abc_ObjAddFanin( pObjNew, pTotal ); - - // quontify the PIs existentially - pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew ); - - // get the new PO - pObjNew = Abc_NtkPo( pNtkNew, 0 ); - // remember the miter output - pTotal = Abc_ObjChild0( pObjNew ); - // remove the PO - Abc_NtkDeleteObj( pObjNew ); - - // make the old network point to the new things - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - Abc_NtkForEachCi( pNtk, pObj, i ) - pObj->pCopy = Abc_NtkPi( pNtkNew, i ); -*/ - - // for each CO, create PO (skip POs equal to CIs because of name conflict) - Abc_NtkForEachPo( pNtk, pObj, i ) - if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) ); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( pObj, "_in") ); - - // link to the POs of the network - Abc_NtkForEachPo( pNtk, pObj, i ) - if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) - Abc_ObjAddFanin( pObj->pCopy, pTotal ); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_ObjAddFanin( pObj->pCopy, pTotal ); - - // remove the extra nodes - Abc_AigCleanup( pNtkNew->pManFunc ); - - // check the result - if ( !Abc_NtkCheck( pNtkNew ) ) - { - printf( "Abc_NtkVanEijkDeriveExdc: The network check has failed.\n" ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } - return pNtkNew; -} - - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c deleted file mode 100644 index 339d64d1..00000000 --- a/src/base/abci/abcVanImp.c +++ /dev/null @@ -1,1002 +0,0 @@ -/**CFile**************************************************************** - - FileName [abcVanImp.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [Implementation of van Eijk's method for implications.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - October 2, 2005.] - - Revision [$Id: abcVanImp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "fraig.h" -#include "sim.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Van_Man_t_ Van_Man_t; -struct Van_Man_t_ -{ - // single frame representation - Abc_Ntk_t * pNtkSingle; // single frame - Vec_Int_t * vCounters; // the counters of 1s in the simulation info - Vec_Ptr_t * vZeros; // the set of constant 0 candidates - Vec_Int_t * vImps; // the set of all implications - Vec_Int_t * vImpsMis; // the minimum independent set of implications - // multiple frame representation - Abc_Ntk_t * pNtkMulti; // multiple frame - Vec_Ptr_t * vCorresp; // the correspondence between single frame and multiple frames - // parameters - int nFrames; // the number of timeframes - int nWords; // the number of simulation words - int nIdMax; // the maximum ID in the single frame - int fVerbose; // the verbosiness flag - // statistics - int nPairsAll; - int nImpsAll; - int nEquals; - int nZeros; - // runtime - int timeAll; - int timeSim; - int timeAdd; - int timeCheck; - int timeInfo; - int timeMis; -}; - -static void Abc_NtkVanImpCompute( Van_Man_t * p ); -static Vec_Ptr_t * Abc_NtkVanImpSortByOnes( Van_Man_t * p ); -static void Abc_NtkVanImpComputeAll( Van_Man_t * p ); -static Vec_Int_t * Abc_NtkVanImpComputeMis( Van_Man_t * p ); -static void Abc_NtkVanImpManFree( Van_Man_t * p ); -static void Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ); -static int Abc_NtkVanImpCountEqual( Van_Man_t * p ); - -static Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ); - -extern Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ); -extern void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); -extern Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); - -//////////////////////////////////////////////////////////////////////// -/// INLINED FUNCTIONS /// -//////////////////////////////////////////////////////////////////////// - -// returns the correspondence of the node in the frame -static inline Abc_Obj_t * Abc_NodeVanImpReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) -{ - return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id ); -} -// returns the left node of the implication -static inline Abc_Obj_t * Abc_NodeVanGetLeft( Abc_Ntk_t * pNtk, unsigned Imp ) -{ - return Abc_NtkObj( pNtk, Imp >> 16 ); -} -// returns the right node of the implication -static inline Abc_Obj_t * Abc_NodeVanGetRight( Abc_Ntk_t * pNtk, unsigned Imp ) -{ - return Abc_NtkObj( pNtk, Imp & 0xFFFF ); -} -// returns the implication -static inline unsigned Abc_NodeVanGetImp( Abc_Obj_t * pLeft, Abc_Obj_t * pRight ) -{ - return (pLeft->Id << 16) | pRight->Id; -} -// returns the right node of the implication -static inline void Abc_NodeVanPrintImp( unsigned Imp ) -{ - printf( "%d -> %d ", Imp >> 16, Imp & 0xFFFF ); -} - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Derives implications that hold sequentially.] - - Description [Adds EXDC network to the current network to record the - set of computed sequentially equivalence implications, representing - a subset of unreachable states.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ) -{ - Fraig_Params_t Params; - Abc_Ntk_t * pNtkNew; - Van_Man_t * p; - - assert( Abc_NtkIsStrash(pNtk) ); - - // start the manager - p = ALLOC( Van_Man_t, 1 ); - memset( p, 0, sizeof(Van_Man_t) ); - p->nFrames = nFrames; - p->fVerbose = fVerbose; - p->vCorresp = Vec_PtrAlloc( 100 ); - - // FRAIG the network to get rid of combinational equivalences - Fraig_ParamsSetDefaultFull( &Params ); - p->pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 ); - p->nIdMax = Abc_NtkObjNumMax( p->pNtkSingle ); - Abc_AigSetNodePhases( p->pNtkSingle ); - Abc_NtkCleanNext( p->pNtkSingle ); -// if ( fVerbose ) -// printf( "The number of ANDs in 1 timeframe = %d.\n", Abc_NtkNodeNum(p->pNtkSingle) ); - - // derive multiple time-frames and node correspondence (to be used in the inductive case) - p->pNtkMulti = Abc_NtkVanEijkFrames( p->pNtkSingle, p->vCorresp, nFrames, 1, 0 ); -// if ( fVerbose ) -// printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + 1, Abc_NtkNodeNum(p->pNtkMulti) ); - - // get the implications - Abc_NtkVanImpCompute( p ); - - // create the new network with EXDC correspondingn to the computed implications - if ( fExdc && (Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImpsMis) > 0) ) - { - if ( p->pNtkSingle->pExdc ) - { - printf( "The old EXDC network is thrown away.\n" ); - Abc_NtkDelete( p->pNtkSingle->pExdc ); - p->pNtkSingle->pExdc = NULL; - } - pNtkNew = Abc_NtkDup( p->pNtkSingle ); - pNtkNew->pExdc = Abc_NtkVanImpDeriveExdc( p->pNtkSingle, p->vZeros, p->vImpsMis ); - } - else - pNtkNew = Abc_NtkDup( p->pNtkSingle ); - - // free stuff - Abc_NtkVanImpManFree( p ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Frees the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanImpManFree( Van_Man_t * p ) -{ - Abc_NtkDelete( p->pNtkMulti ); - Abc_NtkDelete( p->pNtkSingle ); - Vec_PtrFree( p->vCorresp ); - Vec_PtrFree( p->vZeros ); - Vec_IntFree( p->vCounters ); - Vec_IntFree( p->vImpsMis ); - Vec_IntFree( p->vImps ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Derives the minimum independent set of sequential implications.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanImpCompute( Van_Man_t * p ) -{ - Fraig_Man_t * pFraig; - Vec_Ptr_t * vZeros; - Vec_Int_t * vImps, * vImpsTemp; - int nIters, clk; - - // compute all implications and count 1s in the simulation info -clk = clock(); - Abc_NtkVanImpComputeAll( p ); -p->timeAll += clock() - clk; - - // compute the MIS -clk = clock(); - p->vImpsMis = Abc_NtkVanImpComputeMis( p ); -p->timeMis += clock() - clk; - - if ( p->fVerbose ) - { - printf( "Pairs = %8d. Imps = %8d. Seq = %7d. MIS = %7d. Equ = %5d. Const = %5d.\n", - p->nPairsAll, p->nImpsAll, Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), p->nEquals, p->nZeros ); - PRT( "Visiting all nodes pairs while preparing for the inductive case", p->timeAll ); - printf( "Start : Seq = %7d. MIS = %7d. Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) ); - } - - // iterate to perform the iterative filtering of implications - for ( nIters = 1; Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImps) > 0; nIters++ ) - { - // FRAIG the ununitialized frames - pFraig = Abc_NtkVanEijkFraig( p->pNtkMulti, 0 ); - - // assuming that zeros and imps hold in the first k-1 frames - // check if they hold in the k-th frame - vZeros = Vec_PtrAlloc( 100 ); - vImps = Vec_IntAlloc( 100 ); - Abc_NtkVanImpFilter( p, pFraig, vZeros, vImps ); - Fraig_ManFree( pFraig ); - -clk = clock(); - vImpsTemp = p->vImps; - p->vImps = vImps; - Vec_IntFree( p->vImpsMis ); - p->vImpsMis = Abc_NtkVanImpComputeMis( p ); - p->vImps = vImpsTemp; -p->timeMis += clock() - clk; - - // report the results - if ( p->fVerbose ) - printf( "Iter = %2d: Seq = %7d. MIS = %7d. Const = %5d.\n", nIters, Vec_IntSize(vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(vZeros) ); - - // if the fixed point is reaches, quit the loop - if ( Vec_PtrSize(vZeros) == Vec_PtrSize(p->vZeros) && Vec_IntSize(vImps) == Vec_IntSize(p->vImps) ) - { // no change - Vec_PtrFree(vZeros); - Vec_IntFree(vImps); - break; - } - - // update the sets - Vec_PtrFree( p->vZeros ); p->vZeros = vZeros; - Vec_IntFree( p->vImps ); p->vImps = vImps; - } - - // compute the MIS -clk = clock(); - Vec_IntFree( p->vImpsMis ); - p->vImpsMis = Abc_NtkVanImpComputeMis( p ); -// p->vImpsMis = Vec_IntDup( p->vImps ); -p->timeMis += clock() - clk; - if ( p->fVerbose ) - printf( "Final : Seq = %7d. MIS = %7d. Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) ); - - -/* - if ( p->fVerbose ) - { - PRT( "All ", p->timeAll ); - PRT( "Sim ", p->timeSim ); - PRT( "Add ", p->timeAdd ); - PRT( "Check ", p->timeCheck ); - PRT( "Mis ", p->timeMis ); - } -*/ - -/* - // print the implications in the MIS - if ( p->fVerbose ) - { - Abc_Obj_t * pNode, * pNode1, * pNode2; - unsigned Imp; - int i; - if ( Vec_PtrSize(p->vZeros) ) - { - printf( "The const nodes are: " ); - Vec_PtrForEachEntry( p->vZeros, pNode, i ) - printf( "%d(%d) ", pNode->Id, pNode->fPhase ); - printf( "\n" ); - } - if ( Vec_IntSize(p->vImpsMis) ) - { - printf( "The implications are: " ); - Vec_IntForEachEntry( p->vImpsMis, Imp, i ) - { - pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); - pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); - printf( "%d(%d)=>%d(%d) ", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase ); - } - printf( "\n" ); - } - } -*/ -} - -/**Function************************************************************* - - Synopsis [Filters zeros and implications by performing one inductive step.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ) -{ - ProgressBar * pProgress; - Abc_Obj_t * pNode, * pNodeM1, * pNodeM2, * pNode1, * pNode2, * pObj; - Fraig_Node_t * pFNode1, * pFNode2; - Fraig_Node_t * ppFNodes[2]; - unsigned Imp; - int i, f, k, clk; - -clk = clock(); - for ( f = 0; f < p->nFrames; f++ ) - { - // add new clauses for zeros - Vec_PtrForEachEntry( p->vZeros, pNode, i ) - { - pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, f ); - pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); - pFNode1 = Fraig_NotCond( pFNode1, !pNode->fPhase ); - Fraig_ManAddClause( pFraig, &pFNode1, 1 ); - } - // add new clauses for imps - Vec_IntForEachEntry( p->vImps, Imp, i ) - { - pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); - pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); - pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, f ); - pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, f ); - pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); - pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) ); - ppFNodes[0] = Fraig_NotCond( pFNode1, !pNode1->fPhase ); - ppFNodes[1] = Fraig_NotCond( pFNode2, pNode2->fPhase ); -// assert( Fraig_Regular(ppFNodes[0]) != Fraig_Regular(ppFNodes[1]) ); - Fraig_ManAddClause( pFraig, ppFNodes, 2 ); - } - } -p->timeAdd += clock() - clk; - - // check the zero nodes -clk = clock(); - Vec_PtrClear( vZeros ); - Vec_PtrForEachEntry( p->vZeros, pNode, i ) - { - pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, p->nFrames ); - pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); - pFNode1 = Fraig_Regular(pFNode1); - pFNode2 = Fraig_ManReadConst1(pFraig); - if ( pFNode1 == pFNode2 || Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) ) - Vec_PtrPush( vZeros, pNode ); - else - { - // since we disproved this zero, we should add all possible implications to p->vImps - // these implications will be checked below and only correct ones will remain - Abc_NtkForEachObj( p->pNtkSingle, pObj, k ) - { - if ( Abc_ObjIsPo(pObj) ) - continue; - if ( Vec_IntEntry( p->vCounters, pObj->Id ) > 0 ) - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode, pObj) ); - } - } - } - - // check implications - pProgress = Extra_ProgressBarStart( stdout, p->vImps->nSize ); - Vec_IntClear( vImps ); - Vec_IntForEachEntry( p->vImps, Imp, i ) - { - Extra_ProgressBarUpdate( pProgress, i, NULL ); - pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); - pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); - pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, p->nFrames ); - pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, p->nFrames ); - pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); - pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) ); - pFNode1 = Fraig_NotCond( pFNode1, !pNode1->fPhase ); - pFNode2 = Fraig_NotCond( pFNode2, pNode2->fPhase ); - if ( pFNode1 == Fraig_Not(pFNode2) ) - { - Vec_IntPush( vImps, Imp ); - continue; - } - if ( pFNode1 == pFNode2 ) - { - if ( pFNode1 == Fraig_Not( Fraig_ManReadConst1(pFraig) ) ) - continue; - if ( pFNode1 == Fraig_ManReadConst1(pFraig) ) - { - Vec_IntPush( vImps, Imp ); - continue; - } - pFNode1 = Fraig_Regular(pFNode1); - pFNode2 = Fraig_ManReadConst1(pFraig); - if ( Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) ) - Vec_IntPush( vImps, Imp ); - continue; - } - - if ( Fraig_ManCheckClauseUsingSat( pFraig, pFNode1, pFNode2, -1 ) ) - Vec_IntPush( vImps, Imp ); - } - Extra_ProgressBarStop( pProgress ); -p->timeCheck += clock() - clk; -} - -/**Function************************************************************* - - Synopsis [Computes all implications.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanImpComputeAll( Van_Man_t * p ) -{ - ProgressBar * pProgress; - Fraig_Man_t * pManSingle; - Vec_Ptr_t * vInfo; - Abc_Obj_t * pObj, * pNode1, * pNode2, * pConst1; - Fraig_Node_t * pFNode1, * pFNode2; - unsigned * pPats1, * pPats2; - int nFrames, nUnsigned, RetValue; - int clk, i, k, Count1, Count2; - - // decide how many frames to simulate - nFrames = 32; - nUnsigned = 32; - p->nWords = nFrames * nUnsigned; - - // simulate randomly the initialized frames -clk = clock(); - vInfo = Sim_SimulateSeqRandom( p->pNtkSingle, nFrames, nUnsigned ); - - // complement the info for those nodes whose phase is 1 - Abc_NtkForEachObj( p->pNtkSingle, pObj, i ) - if ( pObj->fPhase ) - Sim_UtilSetCompl( Sim_SimInfoGet(vInfo, pObj), p->nWords ); - - // compute the number of ones for each node - p->vCounters = Sim_UtilCountOnesArray( vInfo, p->nWords ); -p->timeSim += clock() - clk; - - // FRAIG the uninitialized frame - pManSingle = Abc_NtkVanEijkFraig( p->pNtkSingle, 0 ); - // now pNode->pCopy are assigned the pointers to the corresponding FRAIG nodes - -/* -Abc_NtkForEachPi( p->pNtkSingle, pNode1, i ) -printf( "PI = %d\n", pNode1->Id ); -Abc_NtkForEachLatch( p->pNtkSingle, pNode1, i ) -printf( "Latch = %d\n", pNode1->Id ); -Abc_NtkForEachPo( p->pNtkSingle, pNode1, i ) -printf( "PO = %d\n", pNode1->Id ); -*/ - - // go through the pairs of signals in the frames - pProgress = Extra_ProgressBarStart( stdout, p->nIdMax ); - pConst1 = Abc_AigConst1(p->pNtkSingle); - p->vImps = Vec_IntAlloc( 100 ); - p->vZeros = Vec_PtrAlloc( 100 ); - Abc_NtkForEachObj( p->pNtkSingle, pNode1, i ) - { - if ( Abc_ObjIsPo(pNode1) ) - continue; - if ( pNode1 == pConst1 ) - continue; - Extra_ProgressBarUpdate( pProgress, i, NULL ); - - // get the number of zeros of this node - Count1 = Vec_IntEntry( p->vCounters, pNode1->Id ); - if ( Count1 == 0 ) - { - Vec_PtrPush( p->vZeros, pNode1 ); - p->nZeros++; - continue; - } - pPats1 = Sim_SimInfoGet(vInfo, pNode1); - - Abc_NtkForEachObj( p->pNtkSingle, pNode2, k ) - { - if ( k >= i ) - break; - if ( Abc_ObjIsPo(pNode2) ) - continue; - if ( pNode2 == pConst1 ) - continue; - p->nPairsAll++; - - // here we have a pair of nodes (pNode1 and pNode2) - // such that Id(pNode1) < Id(pNode2) - assert( pNode2->Id < pNode1->Id ); - - // get the number of zeros of this node - Count2 = Vec_IntEntry( p->vCounters, pNode2->Id ); - if ( Count2 == 0 ) - continue; - pPats2 = Sim_SimInfoGet(vInfo, pNode2); - - // check for implications - if ( Count1 < Count2 ) - { -//clk = clock(); - RetValue = Sim_UtilInfoIsImp( pPats1, pPats2, p->nWords ); -//p->timeInfo += clock() - clk; - if ( !RetValue ) - continue; - p->nImpsAll++; - // pPats1 => pPats2 or pPats1' v pPats2 - pFNode1 = Fraig_NotCond( pNode1->pCopy, !pNode1->fPhase ); - pFNode2 = Fraig_NotCond( pNode2->pCopy, pNode2->fPhase ); - // check if this implication is combinational - if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) ) - continue; - // otherwise record it - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) ); - } - else if ( Count2 < Count1 ) - { -//clk = clock(); - RetValue = Sim_UtilInfoIsImp( pPats2, pPats1, p->nWords ); -//p->timeInfo += clock() - clk; - if ( !RetValue ) - continue; - p->nImpsAll++; - // pPats2 => pPats2 or pPats2' v pPats1 - pFNode2 = Fraig_NotCond( pNode2->pCopy, !pNode2->fPhase ); - pFNode1 = Fraig_NotCond( pNode1->pCopy, pNode1->fPhase ); - // check if this implication is combinational - if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) ) - continue; - // otherwise record it - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); - } - else - { -//clk = clock(); - RetValue = Sim_UtilInfoIsEqual(pPats1, pPats2, p->nWords); -//p->timeInfo += clock() - clk; - if ( !RetValue ) - continue; - p->nEquals++; - // get the FRAIG nodes - pFNode1 = Fraig_NotCond( pNode1->pCopy, pNode1->fPhase ); - pFNode2 = Fraig_NotCond( pNode2->pCopy, pNode2->fPhase ); - - // check if this implication is combinational - if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, Fraig_Not(pFNode1), pFNode2 ) ) - { - if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) ) - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); - else - assert( 0 ); // impossible for FRAIG - } - else - { - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) ); - if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) ) - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); - } - } -// printf( "Implication %d %d -> %d %d \n", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase ); - } - } - Fraig_ManFree( pManSingle ); - Sim_UtilInfoFree( vInfo ); - Extra_ProgressBarStop( pProgress ); -} - - -/**Function************************************************************* - - Synopsis [Sorts the nodes.] - - Description [Sorts the nodes appearing in the left-hand sides of the - implications by the number of 1s in their simulation info.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NtkVanImpSortByOnes( Van_Man_t * p ) -{ - Abc_Obj_t * pNode, * pList; - Vec_Ptr_t * vSorted; - unsigned Imp; - int i, nOnes; - - // start the sorted array - vSorted = Vec_PtrStart( p->nWords * 32 ); - // go through the implications - Abc_NtkIncrementTravId( p->pNtkSingle ); - Vec_IntForEachEntry( p->vImps, Imp, i ) - { - pNode = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); - assert( !Abc_ObjIsPo(pNode) ); - // if this node is already visited, skip - if ( Abc_NodeIsTravIdCurrent( pNode ) ) - continue; - // mark the node as visited - Abc_NodeSetTravIdCurrent( pNode ); - - // add the node to the list - nOnes = Vec_IntEntry( p->vCounters, pNode->Id ); - pList = Vec_PtrEntry( vSorted, nOnes ); - pNode->pNext = pList; - Vec_PtrWriteEntry( vSorted, nOnes, pNode ); - } - return vSorted; -} - -/**Function************************************************************* - - Synopsis [Computes the array of beginnings.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Abc_NtkVanImpComputeBegs( Van_Man_t * p ) -{ - Vec_Int_t * vBegins; - unsigned Imp; - int i, ItemLast, ItemCur; - - // sort the implications (by the number of the left-hand-side node) - Vec_IntSort( p->vImps, 0 ); - - // start the array of beginnings - vBegins = Vec_IntStart( p->nIdMax + 1 ); - - // mark the begining of each node's implications - ItemLast = 0; - Vec_IntForEachEntry( p->vImps, Imp, i ) - { - ItemCur = (Imp >> 16); - if ( ItemCur == ItemLast ) - continue; - Vec_IntWriteEntry( vBegins, ItemCur, i ); - ItemLast = ItemCur; - } - // fill in the empty spaces - ItemLast = Vec_IntSize(p->vImps); - Vec_IntWriteEntry( vBegins, p->nIdMax, ItemLast ); - Vec_IntForEachEntryReverse( vBegins, ItemCur, i ) - { - if ( ItemCur == 0 ) - Vec_IntWriteEntry( vBegins, i, ItemLast ); - else - ItemLast = ItemCur; - } - - Imp = Vec_IntEntry( p->vImps, 0 ); - ItemCur = (Imp >> 16); - for ( i = 0; i <= ItemCur; i++ ) - Vec_IntWriteEntry( vBegins, i, 0 ); - return vBegins; -} - -/**Function************************************************************* - - Synopsis [Derives the minimum subset of implications.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanImpMark_rec( Abc_Obj_t * pNode, Vec_Vec_t * vImpsMis ) -{ - Vec_Int_t * vNexts; - int i, Next; - // if this node is already visited, skip - if ( Abc_NodeIsTravIdCurrent( pNode ) ) - return; - // mark the node as visited - Abc_NodeSetTravIdCurrent( pNode ); - // mark the children - vNexts = Vec_VecEntry( vImpsMis, pNode->Id ); - Vec_IntForEachEntry( vNexts, Next, i ) - Abc_NtkVanImpMark_rec( Abc_NtkObj(pNode->pNtk, Next), vImpsMis ); -} - -/**Function************************************************************* - - Synopsis [Derives the minimum subset of implications.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Abc_NtkVanImpComputeMis( Van_Man_t * p ) -{ - Abc_Obj_t * pNode, * pNext, * pList; - Vec_Vec_t * vMatrix; - Vec_Ptr_t * vSorted; - Vec_Int_t * vBegins; - Vec_Int_t * vImpsMis; - int i, k, iStart, iStop; - void * pEntry; - unsigned Imp; - - if ( Vec_IntSize(p->vImps) == 0 ) - return Vec_IntAlloc(0); - - // compute the sorted list of nodes by the number of 1s - Abc_NtkCleanNext( p->pNtkSingle ); - vSorted = Abc_NtkVanImpSortByOnes( p ); - - // compute the array of beginnings - vBegins = Abc_NtkVanImpComputeBegs( p ); - -/* -Vec_IntForEachEntry( p->vImps, Imp, i ) -{ - printf( "%d: ", i ); - Abc_NodeVanPrintImp( Imp ); -} -printf( "\n\n" ); -Vec_IntForEachEntry( vBegins, Imp, i ) - printf( "%d=%d ", i, Imp ); -printf( "\n\n" ); -*/ - - // compute the MIS by considering nodes in the reverse order of ones - vMatrix = Vec_VecStart( p->nIdMax ); - Vec_PtrForEachEntryReverse( vSorted, pList, i ) - { - for ( pNode = pList; pNode; pNode = pNode->pNext ) - { - // get the starting and stopping implication of this node - iStart = Vec_IntEntry( vBegins, pNode->Id ); - iStop = Vec_IntEntry( vBegins, pNode->Id + 1 ); - if ( iStart == iStop ) - continue; - assert( iStart < iStop ); - // go through all the implications of this node - Abc_NtkIncrementTravId( p->pNtkSingle ); - Abc_NodeIsTravIdCurrent( pNode ); - Vec_IntForEachEntryStartStop( p->vImps, Imp, k, iStart, iStop ) - { - assert( pNode == Abc_NodeVanGetLeft(p->pNtkSingle, Imp) ); - pNext = Abc_NodeVanGetRight(p->pNtkSingle, Imp); - // if this node is already visited, skip - if ( Abc_NodeIsTravIdCurrent( pNext ) ) - continue; - assert( pNode->Id != pNext->Id ); - // add implication - Vec_VecPush( vMatrix, pNode->Id, (void *)pNext->Id ); - // recursively mark dependent nodes - Abc_NtkVanImpMark_rec( pNext, vMatrix ); - } - } - } - Vec_IntFree( vBegins ); - Vec_PtrFree( vSorted ); - - // transfer the MIS into the normal array - vImpsMis = Vec_IntAlloc( 100 ); - Vec_VecForEachEntry( vMatrix, pEntry, i, k ) - { - assert( (i << 16) != ((int)pEntry) ); - Vec_IntPush( vImpsMis, (i << 16) | ((int)pEntry) ); - } - Vec_VecFree( vMatrix ); - return vImpsMis; -} - - -/**Function************************************************************* - - Synopsis [Count equal pairs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkVanImpCountEqual( Van_Man_t * p ) -{ - Abc_Obj_t * pNode1, * pNode2, * pNode3; - Vec_Int_t * vBegins; - int iStart, iStop; - unsigned Imp, ImpR; - int i, k, Counter; - - // compute the array of beginnings - vBegins = Abc_NtkVanImpComputeBegs( p ); - - // go through each node and out - Counter = 0; - Vec_IntForEachEntry( p->vImps, Imp, i ) - { - pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); - pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); - if ( pNode1->Id > pNode2->Id ) - continue; - iStart = Vec_IntEntry( vBegins, pNode2->Id ); - iStop = Vec_IntEntry( vBegins, pNode2->Id + 1 ); - Vec_IntForEachEntryStartStop( p->vImps, ImpR, k, iStart, iStop ) - { - assert( pNode2 == Abc_NodeVanGetLeft(p->pNtkSingle, ImpR) ); - pNode3 = Abc_NodeVanGetRight(p->pNtkSingle, ImpR); - if ( pNode1 == pNode3 ) - { - Counter++; - break; - } - } - } - Vec_IntFree( vBegins ); - return Counter; -} - - -/**Function************************************************************* - - Synopsis [Create EXDC from the equivalence classes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ) -{ - Abc_Ntk_t * pNtkNew; - Vec_Ptr_t * vCone; - Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2;//, * pObjNew; - unsigned Imp; - int i, k; - - assert( Abc_NtkIsStrash(pNtk) ); - - // start the network - pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); - pNtkNew->pName = Extra_UtilStrsav( "exdc" ); - pNtkNew->pSpec = NULL; - - // map the constant nodes - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - // for each CI, create PI - Abc_NtkForEachCi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) ); - // cannot add latches here because pLatch->pCopy pointers are used - - // build logic cone for zero nodes - pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); - Vec_PtrForEachEntry( vZeros, pNode, i ) - { - // build the logic cone for the node - if ( Abc_ObjFaninNum(pNode) == 2 ) - { - vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); - Vec_PtrForEachEntry( vCone, pObj, k ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - Vec_PtrFree( vCone ); - assert( pObj == pNode ); - } - // complement if there is phase difference - pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase ); - - // add it to the EXDC - pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pNode->pCopy ); - } - - // create logic cones for the implications - Vec_IntForEachEntry( vImps, Imp, i ) - { - pNode1 = Abc_NtkObj(pNtk, Imp >> 16); - pNode2 = Abc_NtkObj(pNtk, Imp & 0xFFFF); - - // build the logic cone for the first node - if ( Abc_ObjFaninNum(pNode1) == 2 ) - { - vCone = Abc_NtkDfsNodes( pNtk, &pNode1, 1 ); - Vec_PtrForEachEntry( vCone, pObj, k ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - Vec_PtrFree( vCone ); - assert( pObj == pNode1 ); - } - // complement if there is phase difference - pNode1->pCopy = Abc_ObjNotCond( pNode1->pCopy, pNode1->fPhase ); - - // build the logic cone for the second node - if ( Abc_ObjFaninNum(pNode2) == 2 ) - { - vCone = Abc_NtkDfsNodes( pNtk, &pNode2, 1 ); - Vec_PtrForEachEntry( vCone, pObj, k ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - Vec_PtrFree( vCone ); - assert( pObj == pNode2 ); - } - // complement if there is phase difference - pNode2->pCopy = Abc_ObjNotCond( pNode2->pCopy, pNode2->fPhase ); - - // build the implication and add it to the EXDC - pMiter = Abc_AigAnd( pNtkNew->pManFunc, pNode1->pCopy, Abc_ObjNot(pNode2->pCopy) ); - pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter ); - } -/* - // create the only PO - pObjNew = Abc_NtkCreatePo( pNtkNew ); - // add the PO name - Abc_NtkLogicStoreName( pObjNew, "DC" ); - // add the PO - Abc_ObjAddFanin( pObjNew, pTotal ); - - // quontify the PIs existentially - pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew ); - - // get the new PO - pObjNew = Abc_NtkPo( pNtkNew, 0 ); - // remember the miter output - pTotal = Abc_ObjChild0( pObjNew ); - // remove the PO - Abc_NtkDeleteObj( pObjNew ); - - // make the old network point to the new things - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - Abc_NtkForEachCi( pNtk, pObj, i ) - pObj->pCopy = Abc_NtkPi( pNtkNew, i ); -*/ - - // for each CO, create PO (skip POs equal to CIs because of name conflict) - Abc_NtkForEachPo( pNtk, pObj, i ) - if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) ); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pObj, "_in") ); - - // link to the POs of the network - Abc_NtkForEachPo( pNtk, pObj, i ) - if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) - Abc_ObjAddFanin( pObj->pCopy, pTotal ); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_ObjAddFanin( pObj->pCopy, pTotal ); - - // remove the extra nodes - Abc_AigCleanup( pNtkNew->pManFunc ); - - // check the result - if ( !Abc_NtkCheck( pNtkNew ) ) - { - printf( "Abc_NtkVanImpDeriveExdc: The network check has failed.\n" ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } - return pNtkNew; -} - - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index c6782b07..1fddc8cb 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -544,7 +544,7 @@ void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo ) Abc_NtkForEachCi( pNtk, pObj, i ) pObj->pCopy = NULL; Abc_NtkForEachLatch( pNtk, pObj, i ) - if ( Abc_NtkLatch(pFrames, i)->pCopy ) + if ( Abc_NtkBox(pFrames, i)->pCopy ) pObj->pCopy = (void *)1; Abc_NtkForEachPi( pNtk, pObj, i ) for ( k = 0; k <= iFrame; k++ ) diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 54c6f05c..dba9e6fd 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -33,6 +33,4 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcTiming.c \ src/base/abci/abcUnate.c \ src/base/abci/abcUnreach.c \ - src/base/abci/abcVanEijk.c \ - src/base/abci/abcVanImp.c \ src/base/abci/abcVerify.c diff --git a/src/base/io/io.c b/src/base/io/io.c index 86e8845b..8b80103b 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -595,6 +595,9 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCheck; int c; + printf( "Stand-alone structural Verilog reader is now available as command \"read_ver\".\n" ); + return 0; + fCheck = 1; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) @@ -629,7 +632,8 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv ) fclose( pFile ); // set the new network - pNtk = Io_ReadVerilog( FileName, fCheck ); +// pNtk = Io_ReadVerilog( FileName, fCheck ); + pNtk = NULL; if ( pNtk == NULL ) { fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" ); diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c index 70e648a7..33f23796 100644 --- a/src/base/io/ioRead.c +++ b/src/base/io/ioRead.c @@ -49,7 +49,7 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck ) if ( Extra_FileNameCheckExtension( pFileName, "blif" ) ) pNtk = Io_ReadBlif( pFileName, fCheck ); else if ( Extra_FileNameCheckExtension( pFileName, "v" ) ) - pNtk = Io_ReadVerilog( pFileName, fCheck ); + pNtk = NULL; //Io_ReadVerilog( pFileName, fCheck ); else if ( Extra_FileNameCheckExtension( pFileName, "bench" ) ) pNtk = Io_ReadBench( pFileName, fCheck ); else if ( Extra_FileNameCheckExtension( pFileName, "edf" ) ) diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c index 367d693b..15d75ba8 100644 --- a/src/base/io/ioReadBaf.c +++ b/src/base/io/ioReadBaf.c @@ -85,21 +85,30 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck ) for ( i = 0; i < nInputs; i++ ) { pObj = Abc_NtkCreatePi(pNtkNew); - Abc_NtkLogicStoreName( pObj, pCur ); while ( *pCur++ ); + Abc_ObjAssignName( pObj, pCur, NULL ); while ( *pCur++ ); Vec_PtrPush( vNodes, pObj ); } // create the POs for ( i = 0; i < nOutputs; i++ ) { pObj = Abc_NtkCreatePo(pNtkNew); - Abc_NtkLogicStoreName( pObj, pCur ); while ( *pCur++ ); + Abc_ObjAssignName( pObj, pCur, NULL ); while ( *pCur++ ); } // create the latches for ( i = 0; i < nLatches; i++ ) { pObj = Abc_NtkCreateLatch(pNtkNew); - Abc_NtkLogicStoreName( pObj, pCur ); while ( *pCur++ ); - Vec_PtrPush( vNodes, pObj ); + Abc_ObjAssignName( pObj, pCur, NULL ); while ( *pCur++ ); + + pNode0 = Abc_NtkCreateBo(pNtkNew); + Abc_ObjAssignName( pNode0, pCur, NULL ); while ( *pCur++ ); + + pNode1 = Abc_NtkCreateBi(pNtkNew); + Abc_ObjAssignName( pNode1, pCur, NULL ); while ( *pCur++ ); + Vec_PtrPush( vNodes, pNode1 ); + + Abc_ObjAddFanin( pObj, pNode0 ); + Abc_ObjAddFanin( pNode1, pObj ); } // get the pointer to the beginning of the node array @@ -129,9 +138,9 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck ) Abc_NtkForEachCo( pNtkNew, pObj, i ) { Num = pBufferNode[2*nAnds+i]; - if ( Abc_ObjIsLatch(pObj) ) + if ( Abc_ObjFanoutNum(pObj) > 0 && Abc_ObjIsLatch(Abc_ObjFanout0(pObj)) ) { - Abc_ObjSetData( pObj, (void *)(Num & 3) ); + Abc_ObjSetData( Abc_ObjFanout0(pObj), (void *)(Num & 3) ); Num >>= 2; } pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, Num >> 1), Num & 1 ); diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c index 5d6bc2f1..535789d2 100644 --- a/src/base/io/ioReadBlif.c +++ b/src/base/io/ioReadBlif.c @@ -621,7 +621,7 @@ int Io_ReadBlifNetworkSubcircuit( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens ) Vec_PtrPush( vNames, Extra_UtilStrsav(pName) ); // memory leak!!! // create a new box and add it to the network - pBox = Abc_NtkCreateBox( p->pNtkCur ); + pBox = Abc_NtkCreateBlackbox( p->pNtkCur ); // set the pointer to the node names Abc_ObjSetData( pBox, vNames ); // remember the line of the file diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c index 7c447523..188e5b8c 100644 --- a/src/base/io/ioReadEdif.c +++ b/src/base/io/ioReadEdif.c @@ -46,6 +46,9 @@ Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck ) Extra_FileReader_t * p; Abc_Ntk_t * pNtk; + printf( "Currently this parser does not work!\n" ); + return NULL; + // start the file p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t()" ); if ( p == NULL ) diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index 5482eed4..cc51cc1c 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -116,15 +116,23 @@ Abc_Obj_t * Io_ReadCreateAssert( Abc_Ntk_t * pNtk, char * pName ) ***********************************************************************/ Abc_Obj_t * Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO ) { - Abc_Obj_t * pLatch, * pNet; - // create a new latch and add it to the network - pLatch = Abc_NtkCreateLatch( pNtk ); + Abc_Obj_t * pLatch, * pTerm, * pNet; // get the LI net pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLI ); - Abc_ObjAddFanin( pLatch, pNet ); + // add the BO terminal + pTerm = Abc_NtkCreateBo( pNtk ); + Abc_ObjAddFanin( pTerm, pNet ); + // add the latch box + pLatch = Abc_NtkCreateLatch( pNtk ); + Abc_ObjAddFanin( pLatch, pTerm ); + // add the BI terminal + pTerm = Abc_NtkCreateBi( pNtk ); + Abc_ObjAddFanin( pTerm, pLatch ); // get the LO net pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLO ); - Abc_ObjAddFanin( pNet, pLatch ); + Abc_ObjAddFanin( pNet, pTerm ); + // set latch name + Abc_ObjAssignName( pLatch, pNetLO, "_latch" ); return pLatch; } diff --git a/src/base/io/ioWriteBaf.c b/src/base/io/ioWriteBaf.c index 5bba942b..fc0229a4 100644 --- a/src/base/io/ioWriteBaf.c +++ b/src/base/io/ioWriteBaf.c @@ -116,7 +116,11 @@ void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName ) fprintf( pFile, "%s%c", Abc_ObjName(pObj), 0 ); // write latches Abc_NtkForEachLatch( pNtk, pObj, i ) + { fprintf( pFile, "%s%c", Abc_ObjName(pObj), 0 ); + fprintf( pFile, "%s%c", Abc_ObjName(Abc_ObjFanin0(pObj)), 0 ); + fprintf( pFile, "%s%c", Abc_ObjName(Abc_ObjFanout0(pObj)), 0 ); + } // set the node numbers to be used in the output file Abc_NtkCleanCopy( pNtk ); @@ -143,8 +147,8 @@ void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName ) { Extra_ProgressBarUpdate( pProgress, nAnds, NULL ); pBufferNode[nAnds] = (((int)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj); - if ( Abc_ObjIsLatch(pObj) ) - pBufferNode[nAnds] = (pBufferNode[nAnds] << 2) | ((unsigned)Abc_ObjData(pObj) & 3); + if ( Abc_ObjFanoutNum(pObj) > 0 && Abc_ObjIsLatch(Abc_ObjFanout0(pObj)) ) + pBufferNode[nAnds] = (pBufferNode[nAnds] << 2) | ((unsigned)Abc_ObjData(Abc_ObjFanout0(pObj)) & 3); nAnds++; } Extra_ProgressBarStop( pProgress ); diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c index 26130d38..4cf320b1 100644 --- a/src/base/io/ioWriteBench.c +++ b/src/base/io/ioWriteBench.c @@ -89,7 +89,7 @@ int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk ) fprintf( pFile, "OUTPUT(%s)\n", Abc_ObjName(Abc_ObjFanin0(pNode)) ); Abc_NtkForEachLatch( pNtk, pNode, i ) fprintf( pFile, "%-11s = DFF(%s)\n", - Abc_ObjName(pNode), Abc_ObjName(Abc_ObjFanin0(pNode)) ); + Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode))), Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pNode))) ); // write internal nodes pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) ); diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c index 8cbd0cd0..3b8c41fa 100644 --- a/src/base/io/ioWriteBlif.c +++ b/src/base/io/ioWriteBlif.c @@ -379,8 +379,8 @@ void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch ) { Abc_Obj_t * pNetLi, * pNetLo; int Reset; - pNetLi = Abc_ObjFanin0( pLatch ); - pNetLo = Abc_ObjFanout0( pLatch ); + pNetLi = Abc_ObjFanin0( Abc_ObjFanin0(pLatch) ); + pNetLo = Abc_ObjFanout0( Abc_ObjFanout0(pLatch) ); Reset = (int)Abc_ObjData( pLatch ); // write the latch line fprintf( pFile, ".latch" ); diff --git a/src/base/io/ioWriteVer.c b/src/base/io/ioWriteVer.c index 2234b3a3..64438b05 100644 --- a/src/base/io/ioWriteVer.c +++ b/src/base/io/ioWriteVer.c @@ -331,7 +331,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) } Abc_NtkForEachLatch( pNtk, pTerm, i ) { - pNet = Abc_ObjFanin0(pTerm); + pNet = Abc_ObjFanin0(Abc_ObjFanin0(pTerm)); Counter++; // get the line length after this name is written AddedLength = strlen(Abc_ObjName(pNet)) + 2; @@ -377,7 +377,7 @@ void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) NameCounter = 0; Abc_NtkForEachLatch( pNtk, pLatch, i ) { - pNet = Abc_ObjFanout0(pLatch); + pNet = Abc_ObjFanout0(Abc_ObjFanout0(pLatch)); Counter++; // get the line length after this name is written AddedLength = strlen(Abc_ObjName(pNet)) + 2; @@ -412,14 +412,14 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk ) Abc_NtkForEachLatch( pNtk, pLatch, i ) { // fprintf( pFile, " always@(posedge gclk) begin %s", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); - fprintf( pFile, " always begin %s", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); - fprintf( pFile, " = %s; end\n", Abc_ObjName(Abc_ObjFanin0(pLatch)) ); + fprintf( pFile, " always begin %s", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); + fprintf( pFile, " = %s; end\n", Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) ); if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO ) // fprintf( pFile, " initial begin %s = 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); - fprintf( pFile, " initial begin %s = 0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); + fprintf( pFile, " initial begin %s = 0; end\n", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE ) // fprintf( pFile, " initial begin %s = 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); - fprintf( pFile, " initial begin %s = 1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); + fprintf( pFile, " initial begin %s = 1; end\n", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); } } @@ -431,11 +431,11 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk ) Abc_NtkForEachLatch( pNtk, pLatch, i ) { if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO ) - fprintf( pFile, " initial begin %s <= 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); + fprintf( pFile, " initial begin %s <= 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE ) - fprintf( pFile, " initial begin %s <= 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); - fprintf( pFile, " always@(posedge gclk) begin %s", Abc_ObjName(Abc_ObjFanout0(pLatch)) ); - fprintf( pFile, " <= %s; end\n", Abc_ObjName(Abc_ObjFanin0(pLatch)) ); + fprintf( pFile, " initial begin %s <= 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); + fprintf( pFile, " always@(posedge gclk) begin %s", Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch))) ); + fprintf( pFile, " <= %s; end\n", Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) ); } } */ diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c index 8dc29855..a4bcaefc 100644 --- a/src/base/seq/seqCreate.c +++ b/src/base/seq/seqCreate.c @@ -116,19 +116,19 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ) { Vec_PtrPush( pNtkNew->vPis, pObj->pCopy ); Vec_PtrPush( pNtkNew->vCis, pObj->pCopy ); - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); } Abc_NtkForEachPo( pNtk, pObj, i ) { Vec_PtrPush( pNtkNew->vPos, pObj->pCopy ); Vec_PtrPush( pNtkNew->vCos, pObj->pCopy ); - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); } Abc_NtkForEachAssert( pNtk, pObj, i ) { Vec_PtrPush( pNtkNew->vAsserts, pObj->pCopy ); Vec_PtrPush( pNtkNew->vCos, pObj->pCopy ); - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); } // relink the choice nodes @@ -268,7 +268,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) // duplicate the nodes Abc_AigForEachAnd( pNtk, pObj, i ) { - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj(pNtkNew, pObj, 0); pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); } // share and create the latches @@ -302,7 +302,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) Seq_NtkShareLatchesClean( pNtk ); // add the latches and their names - Abc_NtkAddDummyLatchNames( pNtkNew ); + Abc_NtkAddDummyBoxNames( pNtkNew ); Abc_NtkOrderCisCos( pNtkNew ); // fix the problem with complemented and duplicated CO edges Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); @@ -340,7 +340,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop_old( Abc_Ntk_t * pNtk ) if ( Abc_ObjFaninNum(pObj) == 0 ) continue; // duplicate the node - Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkDupObj(pNtkNew, pObj, 0); if ( Abc_ObjFaninNum(pObj) == 1 ) { assert( !Abc_ObjFaninC0(pObj) ); @@ -372,7 +372,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop_old( Abc_Ntk_t * pNtk ) // the complemented edges are subsumed by the node function } // add the latches and their names - Abc_NtkAddDummyLatchNames( pNtkNew ); + Abc_NtkAddDummyBoxNames( pNtkNew ); Abc_NtkOrderCisCos( pNtkNew ); // fix the problem with complemented and duplicated CO edges Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); diff --git a/src/base/seq/seqFpgaCore.c b/src/base/seq/seqFpgaCore.c index c6360363..b106ded2 100644 --- a/src/base/seq/seqFpgaCore.c +++ b/src/base/seq/seqFpgaCore.c @@ -126,7 +126,7 @@ Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk ) // duplicate the nodes in the mapping Vec_PtrForEachEntry( p->vMapAnds, pObj, i ) - Abc_NtkDupObj( pNtkNew, pObj ); + Abc_NtkDupObj( pNtkNew, pObj, 0 ); // recursively construct the internals of each node Vec_PtrForEachEntry( p->vMapAnds, pObj, i ) @@ -321,7 +321,7 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk ) } // add the latches and their names - Abc_NtkAddDummyLatchNames( pNtkMap ); + Abc_NtkAddDummyBoxNames( pNtkMap ); Abc_NtkOrderCisCos( pNtkMap ); // fix the problem with complemented and duplicated CO edges Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 ); diff --git a/src/base/seq/seqMapCore.c b/src/base/seq/seqMapCore.c index 3db29abd..c465f31f 100644 --- a/src/base/seq/seqMapCore.c +++ b/src/base/seq/seqMapCore.c @@ -412,7 +412,7 @@ Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk ) } // add the latches and their names - Abc_NtkAddDummyLatchNames( pNtkMap ); + Abc_NtkAddDummyBoxNames( pNtkMap ); Abc_NtkOrderCisCos( pNtkMap ); // fix the problem with complemented and duplicated CO edges Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 ); diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c index 1945826f..ba2c154c 100644 --- a/src/base/seq/seqRetCore.c +++ b/src/base/seq/seqRetCore.c @@ -125,14 +125,14 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose ) Abc_NtkCleanCopy( pNtk ); // clone the PIs/POs/latches Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkDupObj( pNtkNew, pObj ); + Abc_NtkDupObj( pNtkNew, pObj, 0 ); Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkDupObj( pNtkNew, pObj ); + Abc_NtkDupObj( pNtkNew, pObj, 0 ); // copy the names Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); // create one AND for each logic node in the topological order vMapAnds = Abc_NtkDfs( pNtk, 0 ); @@ -354,7 +354,7 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq ) Abc_NtkForEachNode( pNtkOld, pObj, i ) { if ( i == 0 ) continue; - Abc_NtkDupObj( pNtkNew, pObj ); + Abc_NtkDupObj( pNtkNew, pObj, 0 ); pObj->pNext->pCopy = pObj->pCopy; } Abc_NtkForEachLatch( pNtkOld, pObj, i ) @@ -407,7 +407,7 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq ) Seq_NtkShareLatchesClean( pNtkSeq ); // add the latches and their names - Abc_NtkAddDummyLatchNames( pNtkNew ); + Abc_NtkAddDummyBoxNames( pNtkNew ); Abc_NtkOrderCisCos( pNtkNew ); // fix the problem with complemented and duplicated CO edges Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); diff --git a/src/misc/nm/nm.h b/src/misc/nm/nm.h index 9c96c8ba..89a9efac 100644 --- a/src/misc/nm/nm.h +++ b/src/misc/nm/nm.h @@ -25,6 +25,27 @@ extern "C" { #endif +/* + This manager is designed to store ID-to-name and name-to-ID mapping + for Boolean networks and And-Inverter Graphs. + + In a netlist, net names are unique. In this case, there is a one-to-one + mapping between IDs and names. + + In a logic network, which do not have nets, several objects may have + the same name. For example, a latch output and a primary output. + Another example, a primary input and an input to a black box. + In this case, for each ID on an object there is only one name, + but for each name may be several IDs of objects having this name. + + The name manager maps ID-to-name uniquely but it allows one name to + be mapped into several IDs. When a query to find an ID of the object + by its name is submitted, it is possible to specify the object type, + which will help select one of several IDs. If the type is -1, and + there is more than one object with the given name, any object with + the given name is returned. +*/ + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -51,12 +72,11 @@ typedef struct Nm_Man_t_ Nm_Man_t; extern Nm_Man_t * Nm_ManCreate( int nSize ); extern void Nm_ManFree( Nm_Man_t * p ); extern int Nm_ManNumEntries( Nm_Man_t * p ); -extern char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, char * pName, char * pSuffix ); +extern char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, int Type, char * pName, char * pSuffix ); extern void Nm_ManDeleteIdName( Nm_Man_t * p, int ObjId ); extern char * Nm_ManCreateUniqueName( Nm_Man_t * p, int ObjId ); extern char * Nm_ManFindNameById( Nm_Man_t * p, int ObjId ); -extern int Nm_ManFindIdByName( Nm_Man_t * p, char * pName, int * pSecond ); -extern void Nm_ManPrintTables( Nm_Man_t * p ); +extern int Nm_ManFindIdByName( Nm_Man_t * p, char * pName, int Type ); extern Vec_Int_t * Nm_ManReturnNameIds( Nm_Man_t * p ); #ifdef __cplusplus diff --git a/src/misc/nm/nmApi.c b/src/misc/nm/nmApi.c index 120dbe91..f7bb0fe7 100644 --- a/src/misc/nm/nmApi.c +++ b/src/misc/nm/nmApi.c @@ -46,7 +46,7 @@ Nm_Man_t * Nm_ManCreate( int nSize ) p = ALLOC( Nm_Man_t, 1 ); memset( p, 0, sizeof(Nm_Man_t) ); // set the parameters - p->nSizeFactor = 2; // determined how much larger the table should be compared to data in it + p->nSizeFactor = 2; // determined the limit on the grow of data before the table resizes p->nGrowthFactor = 3; // determined how much the table grows after resizing // allocate and clean the bins p->nBins = Cudd_PrimeNm(nSize); @@ -106,29 +106,23 @@ int Nm_ManNumEntries( Nm_Man_t * p ) SeeAlso [] ***********************************************************************/ -char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, char * pName, char * pSuffix ) +char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, int Type, char * pName, char * pSuffix ) { - Nm_Entry_t * pEntry, * pEntry2; + Nm_Entry_t * pEntry; int RetValue, nEntrySize; + // check if the object with this ID is already stored if ( pEntry = Nm_ManTableLookupId(p, ObjId) ) { - if ( strcmp(pEntry->Name, pName) == 0 ) - printf( "Nm_ManStoreIdName(): Entry with the same ID and name already exists.\n" ); - else - printf( "Nm_ManStoreIdName(): Entry with the same ID and different name already exists.\n" ); - return NULL; - } - if ( pSuffix == NULL && (pEntry = Nm_ManTableLookupName(p, pName, &pEntry2)) && pEntry2 ) - { - printf( "Nm_ManStoreIdName(): Two entries with the same name already exist.\n" ); + printf( "Nm_ManStoreIdName(): Entry with the same ID already exists.\n" ); return NULL; } - // create the entry + // create a new entry nEntrySize = sizeof(Nm_Entry_t) + strlen(pName) + (pSuffix?strlen(pSuffix):0) + 1; nEntrySize = (nEntrySize / 4 + ((nEntrySize % 4) > 0)) * 4; pEntry = (Nm_Entry_t *)Extra_MmFlexEntryFetch( p->pMem, nEntrySize ); pEntry->pNextI2N = pEntry->pNextN2I = NULL; pEntry->ObjId = ObjId; + pEntry->Type = Type; sprintf( pEntry->Name, "%s%s", pName, pSuffix? pSuffix : "" ); // add the entry to the hash table RetValue = Nm_ManTableAdd( p, pEntry ); @@ -158,7 +152,7 @@ void Nm_ManDeleteIdName( Nm_Man_t * p, int ObjId ) return; } // remove entry from the table - Nm_ManTableDelete( p, pEntry ); + Nm_ManTableDelete( p, ObjId ); } @@ -167,7 +161,7 @@ void Nm_ManDeleteIdName( Nm_Man_t * p, int ObjId ) Synopsis [Finds a unique name for the node.] Description [If the name exists, tries appending numbers to it until - it becomes unique.] + it becomes unique. The name is not added to the table.] SideEffects [] @@ -182,9 +176,9 @@ char * Nm_ManCreateUniqueName( Nm_Man_t * p, int ObjId ) if ( pEntry = Nm_ManTableLookupId(p, ObjId) ) return pEntry->Name; sprintf( NameStr, "[%d]", ObjId ); - for ( i = 1; Nm_ManTableLookupName(p, NameStr, NULL); i++ ) + for ( i = 1; Nm_ManTableLookupName(p, NameStr, -1); i++ ) sprintf( NameStr, "[%d]_%d", ObjId, i ); - return Nm_ManStoreIdName( p, ObjId, NameStr, NULL ); + return NameStr; } /**Function************************************************************* @@ -218,69 +212,14 @@ char * Nm_ManFindNameById( Nm_Man_t * p, int ObjId ) SeeAlso [] ***********************************************************************/ -int Nm_ManFindIdByName( Nm_Man_t * p, char * pName, int * pSecond ) +int Nm_ManFindIdByName( Nm_Man_t * p, char * pName, int Type ) { - Nm_Entry_t * pEntry, * pEntry2; - if ( pEntry = Nm_ManTableLookupName(p, pName, &pEntry2) ) - { - if ( pSecond ) - *pSecond = pEntry2? pEntry2->ObjId : -1; + Nm_Entry_t * pEntry; + if ( pEntry = Nm_ManTableLookupName(p, pName, Type) ) return pEntry->ObjId; - } return -1; } - -/**Function************************************************************* - - Synopsis [Prints distribution of entries in the bins.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Nm_ManPrintTables( Nm_Man_t * p ) -{ - int i, Counter; - - // rehash the entries from the old table - Counter = 0; - printf( "Int2Name: " ); - for ( i = 0; i < p->nBins; i++ ) - { - if ( Counter == 0 && p->pBinsI2N[i] == NULL ) - continue; - if ( p->pBinsI2N[i] ) - Counter++; - else - { - printf( "%d ", Counter ); - Counter = 0; - } - } - printf( "\n" ); - - // rehash the entries from the old table - Counter = 0; - printf( "Name2Int: " ); - for ( i = 0; i < p->nBins; i++ ) - { - if ( Counter == 0 && p->pBinsN2I[i] == NULL ) - continue; - if ( p->pBinsN2I[i] ) - Counter++; - else - { - printf( "%d ", Counter ); - Counter = 0; - } - } - printf( "\n" ); -} - /**Function************************************************************* Synopsis [Return the IDs of objects with names.] diff --git a/src/misc/nm/nmInt.h b/src/misc/nm/nmInt.h index 8356a4cb..028316e1 100644 --- a/src/misc/nm/nmInt.h +++ b/src/misc/nm/nmInt.h @@ -44,9 +44,11 @@ extern "C" { typedef struct Nm_Entry_t_ Nm_Entry_t; struct Nm_Entry_t_ { - int ObjId; // object ID + unsigned Type : 4; // object type + unsigned ObjId : 28; // object ID Nm_Entry_t * pNextI2N; // the next entry in the ID hash table Nm_Entry_t * pNextN2I; // the next entry in the name hash table + Nm_Entry_t * pNameSake; // the next entry with the same name char Name[0]; // name of the object }; @@ -71,9 +73,9 @@ struct Nm_Man_t_ /*=== nmTable.c ==========================================================*/ extern int Nm_ManTableAdd( Nm_Man_t * p, Nm_Entry_t * pEntry ); -extern int Nm_ManTableDelete( Nm_Man_t * p, Nm_Entry_t * pEntry ); +extern int Nm_ManTableDelete( Nm_Man_t * p, int ObjId ); extern Nm_Entry_t * Nm_ManTableLookupId( Nm_Man_t * p, int ObjId ); -extern Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** ppSecond ); +extern Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, int Type ); extern unsigned int Cudd_PrimeNm( unsigned int p ); #ifdef __cplusplus diff --git a/src/misc/nm/nmTable.c b/src/misc/nm/nmTable.c index 4eeaf610..b209becd 100644 --- a/src/misc/nm/nmTable.c +++ b/src/misc/nm/nmTable.c @@ -67,37 +67,29 @@ static void Nm_ManResize( Nm_Man_t * p ); ***********************************************************************/ int Nm_ManTableAdd( Nm_Man_t * p, Nm_Entry_t * pEntry ) { - Nm_Entry_t ** ppSpot; -// int i; + Nm_Entry_t ** ppSpot, * pOther; // resize the tables if needed -// if ( p->nEntries * p->nSizeFactor > p->nBins ) if ( p->nEntries > p->nBins * p->nSizeFactor ) - { -// Nm_ManPrintTables( p ); Nm_ManResize( p ); - } -/* - // hash it by ID - for ( i = Nm_HashNumber(pEntry->ObjId, p->nBins); p->pBinsI2N[i]; i = (i+1) % p->nBins ) - if ( p->pBinsI2N[i] == pEntry ) - return 0; - assert( p->pBinsI2N[i] == NULL ); - p->pBinsI2N[i] = pEntry; - // hash it by Name - for ( i = Nm_HashString(pEntry->Name, p->nBins); p->pBinsN2I[i]; i = (i+1) % p->nBins ) - if ( p->pBinsN2I[i] == pEntry ) - return 0; - assert( p->pBinsN2I[i] == NULL ); - p->pBinsN2I[i] = pEntry; -*/ + // add the entry to the table Id->Name + assert( Nm_ManTableLookupId(p, pEntry->ObjId) == NULL ); ppSpot = p->pBinsI2N + Nm_HashNumber(pEntry->ObjId, p->nBins); pEntry->pNextI2N = *ppSpot; *ppSpot = pEntry; - - ppSpot = p->pBinsN2I + Nm_HashString(pEntry->Name, p->nBins); - pEntry->pNextN2I = *ppSpot; - *ppSpot = pEntry; - + // check if an entry with the same name already exists + if ( pOther = Nm_ManTableLookupName(p, pEntry->Name, -1) ) + { + // entry with the same name already exists - add it to the ring + pEntry->pNameSake = pOther->pNameSake? pOther->pNameSake : pOther; + pOther->pNameSake = pEntry; + } + else + { + // entry with the same name does not exist - add it to the table + ppSpot = p->pBinsN2I + Nm_HashString(pEntry->Name, p->nBins); + pEntry->pNextN2I = *ppSpot; + *ppSpot = pEntry; + } // report successfully added entry p->nEntries++; return 1; @@ -114,10 +106,51 @@ int Nm_ManTableAdd( Nm_Man_t * p, Nm_Entry_t * pEntry ) SeeAlso [] ***********************************************************************/ -int Nm_ManTableDelete( Nm_Man_t * p, Nm_Entry_t * pEntry ) +int Nm_ManTableDelete( Nm_Man_t * p, int ObjId ) { - assert( 0 ); - return 0; + Nm_Entry_t ** ppSpot, * pEntry, * pPrev; + int fRemoved; + // remove the entry from the table Id->Name + assert( Nm_ManTableLookupId(p, ObjId) != NULL ); + ppSpot = p->pBinsI2N + Nm_HashNumber(ObjId, p->nBins); + while ( (*ppSpot)->ObjId != (unsigned)ObjId ) + ppSpot = &(*ppSpot)->pNextI2N; + pEntry = *ppSpot; + *ppSpot = (*ppSpot)->pNextI2N; + // remove the entry from the table Name->Id + ppSpot = p->pBinsN2I + Nm_HashString(pEntry->Name, p->nBins); + while ( *ppSpot && *ppSpot != pEntry ) + ppSpot = &(*ppSpot)->pNextN2I; + // remember if we found this one in the list + fRemoved = (*ppSpot != NULL); + if ( *ppSpot ) + { + assert( *ppSpot == pEntry ); + *ppSpot = (*ppSpot)->pNextN2I; + } + // quit if this entry has no namesakes + if ( pEntry->pNameSake == NULL ) + { + assert( fRemoved ); + return 1; + } + // remove entry from the ring of namesakes + assert( pEntry->pNameSake != pEntry ); + for ( pPrev = pEntry; pPrev->pNameSake != pEntry; pPrev = pPrev->pNameSake ); + assert( !strcmp(pPrev->Name, pEntry->Name) ); + assert( pPrev->pNameSake == pEntry ); + if ( pEntry->pNameSake == pPrev ) // two entries in the ring + pPrev->pNameSake = NULL; + else + pPrev->pNameSake = pEntry->pNameSake; + // reinsert the ring back if we removed its connection with the list in the table + if ( fRemoved ) + { + assert( pPrev->pNextN2I == NULL ); + pPrev->pNextN2I = *ppSpot; + *ppSpot = pPrev; + } + return 1; } /**Function************************************************************* @@ -134,21 +167,15 @@ int Nm_ManTableDelete( Nm_Man_t * p, Nm_Entry_t * pEntry ) Nm_Entry_t * Nm_ManTableLookupId( Nm_Man_t * p, int ObjId ) { Nm_Entry_t * pEntry; -// int i; -/* - for ( i = Nm_HashNumber(ObjId, p->nBins); p->pBinsI2N[i]; i = (i+1) % p->nBins ) - if ( p->pBinsI2N[i]->ObjId == ObjId ) - return p->pBinsI2N[i]; -*/ for ( pEntry = p->pBinsI2N[ Nm_HashNumber(ObjId, p->nBins) ]; pEntry; pEntry = pEntry->pNextI2N ) - if ( pEntry->ObjId == ObjId ) + if ( pEntry->ObjId == (unsigned)ObjId ) return pEntry; return NULL; } /**Function************************************************************* - Synopsis [Looks up the entry by name. May return two entries.] + Synopsis [Looks up the entry by name and type.] Description [] @@ -157,42 +184,14 @@ Nm_Entry_t * Nm_ManTableLookupId( Nm_Man_t * p, int ObjId ) SeeAlso [] ***********************************************************************/ -Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** ppSecond ) +Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, int Type ) { - Nm_Entry_t * pFirst, * pSecond, * pEntry; + Nm_Entry_t * pEntry; int Counter = 0; - pFirst = pSecond = NULL; -/* - for ( i = Nm_HashString(pName, p->nBins); p->pBinsN2I[i]; i = (i+1) % p->nBins ) - if ( strcmp(p->pBinsN2I[i]->Name, pName) == 0 ) - { - if ( pFirst == NULL ) - pFirst = p->pBinsN2I[i]; - else if ( pSecond == NULL ) - pSecond = p->pBinsN2I[i]; - else - assert( 0 ); // name appears more than 2 times - } - else - Counter++; - if ( Counter > 100 ) - printf( "%d ", Counter ); -*/ for ( pEntry = p->pBinsN2I[ Nm_HashString(pName, p->nBins) ]; pEntry; pEntry = pEntry->pNextN2I ) - if ( strcmp(pEntry->Name, pName) == 0 ) - { - if ( pFirst == NULL ) - pFirst = pEntry; - else if ( pSecond == NULL ) - pSecond = pEntry; - else - assert( 0 ); // name appears more than 2 times - } - - // save the names - if ( ppSecond ) - *ppSecond = pSecond; - return pFirst; + if ( !strcmp(pEntry->Name, pName) && (Type == -1 || pEntry->Type == (unsigned)Type) ) + return pEntry; + return pEntry; } /**Function************************************************************* @@ -230,8 +229,6 @@ void Nm_ManProfile( Nm_Man_t * p ) printf( "\n" ); } - - /**Function************************************************************* Synopsis [Resizes the table.] @@ -256,39 +253,26 @@ clk = clock(); pBinsNewN2I = ALLOC( Nm_Entry_t *, nBinsNew ); memset( pBinsNewI2N, 0, sizeof(Nm_Entry_t *) * nBinsNew ); memset( pBinsNewN2I, 0, sizeof(Nm_Entry_t *) * nBinsNew ); - // rehash the entries from the old table + // rehash entries in Id->Name table Counter = 0; for ( e = 0; e < p->nBins; e++ ) - for ( pEntry = p->pBinsI2N[e], pEntry2 = pEntry? pEntry->pNextI2N : NULL; - pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNextI2N : NULL ) - { -// pEntry = p->pBinsI2N[e]; -// if ( pEntry == NULL ) -// continue; -/* - // hash it by ID - for ( i = Nm_HashNumber(pEntry->ObjId, nBinsNew); pBinsNewI2N[i]; i = (i+1) % nBinsNew ) - if ( pBinsNewI2N[i] == pEntry ) - assert( 0 ); - assert( pBinsNewI2N[i] == NULL ); - pBinsNewI2N[i] = pEntry; - // hash it by Name - for ( i = Nm_HashString(pEntry->Name, nBinsNew); pBinsNewN2I[i]; i = (i+1) % nBinsNew ) - if ( pBinsNewN2I[i] == pEntry ) - assert( 0 ); - assert( pBinsNewN2I[i] == NULL ); - pBinsNewN2I[i] = pEntry; -*/ - ppSpot = pBinsNewI2N + Nm_HashNumber(pEntry->ObjId, nBinsNew); - pEntry->pNextI2N = *ppSpot; - *ppSpot = pEntry; - - ppSpot = pBinsNewN2I + Nm_HashString(pEntry->Name, nBinsNew); - pEntry->pNextN2I = *ppSpot; - *ppSpot = pEntry; - - Counter++; - } + for ( pEntry = p->pBinsI2N[e], pEntry2 = pEntry? pEntry->pNextI2N : NULL; + pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNextI2N : NULL ) + { + ppSpot = pBinsNewI2N + Nm_HashNumber(pEntry->ObjId, nBinsNew); + pEntry->pNextI2N = *ppSpot; + *ppSpot = pEntry; + Counter++; + } + // rehash entries in Name->Id table + for ( e = 0; e < p->nBins; e++ ) + for ( pEntry = p->pBinsN2I[e], pEntry2 = pEntry? pEntry->pNextN2I : NULL; + pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNextN2I : NULL ) + { + ppSpot = pBinsNewN2I + Nm_HashString(pEntry->Name, nBinsNew); + pEntry->pNextN2I = *ppSpot; + *ppSpot = pEntry; + } assert( Counter == p->nEntries ); // printf( "Increasing the structural table size from %6d to %6d. ", p->nBins, nBinsNew ); // PRT( "Time", clock() - clk ); diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index 75ceab4b..76543e37 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -304,9 +304,9 @@ void ABC_Network_Finalize( ABC_Manager mng ) Abc_Obj_t * pObj; int i; Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, ABC_GetNodeName(mng, pObj) ); + Abc_ObjAssignName( pObj, ABC_GetNodeName(mng, pObj), NULL ); Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, ABC_GetNodeName(mng, pObj) ); + Abc_ObjAssignName( pObj, ABC_GetNodeName(mng, pObj), NULL ); assert( Abc_NtkLatchNum(pNtk) == 0 ); } diff --git a/src/temp/ver/verCore.c b/src/temp/ver/verCore.c index 99311c98..303fe7d1 100644 --- a/src/temp/ver/verCore.c +++ b/src/temp/ver/verCore.c @@ -752,7 +752,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) if ( Abc_NtkIsNetlist(pNtkGate) ) pNetFormal = Abc_NtkFindNet( pNtkGate, pWord ); else // if ( Abc_NtkIsStrash(pNtkGate) ) - pNetFormal = Abc_NtkFindTerm( pNtkGate, pWord ); + assert( 0 ); if ( pNetFormal == NULL ) { sprintf( pMan->sError, "Formal net is missing in gate %s.", pWord ); @@ -865,7 +865,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate ) memset( pPolarity, 0, nBytes ); } // create box to represent this gate - pNode = Abc_NtkCreateBox( pMan->pNtkCur ); + pNode = Abc_NtkCreateBlackbox( pMan->pNtkCur ); pNode->pNext = (Abc_Obj_t *)pPolarity; pNode->pData = pNtkGate; // connect to fanin nets |