From 9d09f583b6ea1181ebd5af1654acd3432c427445 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 10 Jun 2008 08:01:00 -0700 Subject: Version abc80610 --- src/aig/ntl/ntl.h | 103 +++++++++-- src/aig/ntl/ntlCheck.c | 143 +++++++++++++-- src/aig/ntl/ntlEc.c | 193 ++++++++++--------- src/aig/ntl/ntlExtract.c | 449 +++++++++++++-------------------------------- src/aig/ntl/ntlFraig.c | 16 +- src/aig/ntl/ntlInsert.c | 2 +- src/aig/ntl/ntlMan.c | 177 +++++++++++++++--- src/aig/ntl/ntlReadBlif.c | 184 +++++++++++-------- src/aig/ntl/ntlSweep.c | 2 +- src/aig/ntl/ntlTable.c | 117 +++++++++++- src/aig/ntl/ntlTime.c | 28 ++- src/aig/ntl/ntlUtil.c | 149 ++++++++++++--- src/aig/ntl/ntlWriteBlif.c | 81 +++++--- 13 files changed, 1045 insertions(+), 599 deletions(-) (limited to 'src/aig/ntl') diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index 4179754c..b496cb13 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -43,6 +43,7 @@ extern "C" { typedef struct Ntl_Man_t_ Ntl_Man_t; typedef struct Ntl_Mod_t_ Ntl_Mod_t; +typedef struct Ntl_Reg_t_ Ntl_Reg_t; typedef struct Ntl_Obj_t_ Ntl_Obj_t; typedef struct Ntl_Net_t_ Ntl_Net_t; typedef struct Ntl_Lut_t_ Ntl_Lut_t; @@ -65,6 +66,7 @@ struct Ntl_Man_t_ char * pName; // the name of this design char * pSpec; // the name of input file Vec_Ptr_t * vModels; // the array of all models used to represent boxes + int BoxTypes[15]; // the array of box types among the models // memory managers Aig_MmFlex_t * pMemObjs; // memory for objects Aig_MmFlex_t * pMemSops; // memory for SOPs @@ -75,6 +77,12 @@ struct Ntl_Man_t_ Vec_Int_t * vBox1Cos; // the first COs of the boxes Aig_Man_t * pAig; // the extracted AIG Tim_Man_t * pManTime; // the timing manager + int iLastCi; // the last true CI + Vec_Ptr_t * vLatchIns; // the AIG nodes driving latch inputs for internal latches + // hashing names into models + Ntl_Mod_t ** pModTable; // the hash table of names into models + int nModTableSize; // the allocated table size + int nModEntries; // the number of entries in the hash table }; struct Ntl_Mod_t_ @@ -86,21 +94,33 @@ struct Ntl_Mod_t_ Vec_Ptr_t * vPis; // the array of PI objects Vec_Ptr_t * vPos; // the array of PO objects int nObjs[NTL_OBJ_VOID]; // counter of objects of each type - int fKeep; // indicates persistant model + // box attributes + unsigned int attrWhite : 1; // box has known logic + unsigned int attrBox : 1; // box is to remain unmapped + unsigned int attrComb : 1; // box is combinational + unsigned int attrKeep : 1; // box cannot be removed by structural sweep // hashing names into nets Ntl_Net_t ** pTable; // the hash table of names into nets int nTableSize; // the allocated table size int nEntries; // the number of entries in the hash table // delay information Vec_Int_t * vDelays; - Vec_Int_t * vArrivals; - Vec_Int_t * vRequireds; + Vec_Int_t * vTimeInputs; + Vec_Int_t * vTimeOutputs; float * pDelayTable; // other data members + Ntl_Mod_t * pNext; void * pCopy; int nUsed, nRems; }; +struct Ntl_Reg_t_ +{ + unsigned int regInit : 2; // register initial value + unsigned int regType : 3; // register type + unsigned int regClass : 28; // register class +}; + struct Ntl_Obj_t_ { Ntl_Mod_t * pModel; // the model @@ -113,7 +133,11 @@ struct Ntl_Obj_t_ union { // functionality Ntl_Mod_t * pImplem; // model (for boxes) char * pSop; // SOP (for logic nodes) - unsigned LatchId; // init state + register class (for latches) + Ntl_Reg_t LatchId; // init state + register class (for latches) + }; + union { // clock / other data + Ntl_Net_t * pClock; // clock (for registers) + void * pTemp; // other data }; Ntl_Net_t * pFanio[0]; // fanins/fanouts }; @@ -164,8 +188,6 @@ static inline int Ntl_ModelNodeNum( Ntl_Mod_t * p ) { return p->nO static inline int Ntl_ModelLut1Num( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_LUT1]; } static inline int Ntl_ModelLatchNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_LATCH]; } static inline int Ntl_ModelBoxNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_BOX]; } -static inline int Ntl_ModelCiNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PI] + p->nObjs[NTL_OBJ_LATCH]; } -static inline int Ntl_ModelCoNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PO] + p->nObjs[NTL_OBJ_LATCH]; } static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i ) { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPis, i); } static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i ) { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPos, i); } @@ -173,8 +195,6 @@ static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i ) { return (Ntl_ static inline char * Ntl_ModelPiName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPi(p, i)->pFanio[0]->pName; } static inline char * Ntl_ModelPoName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPo(p, i)->pFanio[0]->pName; } -static inline int Ntl_ModelIsBlackBox( Ntl_Mod_t * p ) { return Ntl_ModelPiNum(p) + Ntl_ModelPoNum(p) == Vec_PtrSize(p->vObjs); } - static inline int Ntl_ObjFaninNum( Ntl_Obj_t * p ) { return p->nFanins; } static inline int Ntl_ObjFanoutNum( Ntl_Obj_t * p ) { return p->nFanouts; } @@ -193,6 +213,23 @@ static inline Ntl_Net_t * Ntl_ObjFanout( Ntl_Obj_t * p, int i ) { return p->pF static inline void Ntl_ObjSetFanin( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i ) { p->pFanio[i] = pNet; } static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i ) { p->pFanio[p->nFanins+i] = pNet; pNet->pDriver = p; } +static inline int Ntl_ObjIsInit1( Ntl_Obj_t * p ) { assert( Ntl_ObjIsLatch(p) ); return p->LatchId.regInit == 1; } +static inline void Ntl_ObjSetInit0( Ntl_Obj_t * p ) { assert( Ntl_ObjIsLatch(p) ); p->LatchId.regInit = 0; } + +static inline int Ntl_BoxIsWhite( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return p->pImplem->attrWhite; } +static inline int Ntl_BoxIsBlack( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrWhite; } +static inline int Ntl_BoxIsComb( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return p->pImplem->attrComb; } +static inline int Ntl_BoxIsSeq( Ntl_Obj_t * p ) { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrComb; } + +static inline int Ntl_ObjIsMapLeaf( Ntl_Obj_t * p ) { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p)); } +static inline int Ntl_ObjIsMapRoot( Ntl_Obj_t * p ) { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p)); } + +static inline int Ntl_ObjIsCombLeaf( Ntl_Obj_t * p ) { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && (Ntl_BoxIsSeq(p) || Ntl_BoxIsBlack(p))); } +static inline int Ntl_ObjIsCombRoot( Ntl_Obj_t * p ) { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && (Ntl_BoxIsSeq(p) || Ntl_BoxIsBlack(p))); } + +static inline int Ntl_ObjIsSeqLeaf( Ntl_Obj_t * p ) { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsBlack(p)); } +static inline int Ntl_ObjIsSeqRoot( Ntl_Obj_t * p ) { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsBlack(p)); } + //////////////////////////////////////////////////////////////////////// /// ITERATORS /// //////////////////////////////////////////////////////////////////////// @@ -203,10 +240,10 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int Vec_PtrForEachEntry( p->vCis, pNet, i ) #define Ntl_ManForEachCoNet( p, pNet, i ) \ Vec_PtrForEachEntry( p->vCos, pNet, i ) -#define Ntl_ManForEachNode( p, pObj, i ) \ +#define Ntl_ManForEachNode( p, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \ if ( (pObj) == NULL || !Ntl_ObjIsNode(pObj) ) {} else -#define Ntl_ManForEachBox( p, pObj, i ) \ +#define Ntl_ManForEachBox( p, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \ if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else @@ -214,6 +251,9 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int for ( i = 0; (i < Vec_PtrSize(pNwk->vPis)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPis, i)), 1); i++ ) #define Ntl_ModelForEachPo( pNwk, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(pNwk->vPos)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPos, i)), 1); i++ ) +#define Ntl_ModelForEachNet( pNwk, pNet, i ) \ + for ( i = 0; i < pNwk->nTableSize; i++ ) \ + for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext ) #define Ntl_ModelForEachObj( pNwk, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ if ( pObj == NULL ) {} else @@ -226,15 +266,31 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int #define Ntl_ModelForEachBox( pNwk, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else -#define Ntl_ModelForEachNet( pNwk, pNet, i ) \ - for ( i = 0; i < pNwk->nTableSize; i++ ) \ - for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext ) #define Ntl_ObjForEachFanin( pObj, pFanin, i ) \ for ( i = 0; (i < (pObj)->nFanins) && (((pFanin) = (pObj)->pFanio[i]), 1); i++ ) #define Ntl_ObjForEachFanout( pObj, pFanout, i ) \ for ( i = 0; (i < (pObj)->nFanouts) && (((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]), 1); i++ ) +#define Ntl_ModelForEachMapLeaf( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsMapLeaf(pObj) ) {} else +#define Ntl_ModelForEachMapRoot( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsMapRoot(pObj) ) {} else +#define Ntl_ModelForEachCombLeaf( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsCombLeaf(pObj) ) {} else +#define Ntl_ModelForEachCombRoot( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsCombRoot(pObj) ) {} else +#define Ntl_ModelForEachSeqLeaf( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsSeqLeaf(pObj) ) {} else +#define Ntl_ModelForEachSeqRoot( pNwk, pObj, i ) \ + for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \ + if ( (pObj) == NULL || !Ntl_ObjIsSeqRoot(pObj) ) {} else + //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -247,17 +303,17 @@ extern ABC_DLL void Ntl_ManPrepareCec( char * pFileName1, char * pFil extern ABC_DLL Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ); /*=== ntlExtract.c ==========================================================*/ extern ABC_DLL Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ); -extern ABC_DLL Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq ); -extern ABC_DLL Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p ); -extern ABC_DLL Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 ); +extern ABC_DLL Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p ); +extern ABC_DLL Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p ); /*=== ntlInsert.c ==========================================================*/ extern ABC_DLL Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ); extern ABC_DLL Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ); extern ABC_DLL Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ); /*=== ntlCheck.c ==========================================================*/ extern ABC_DLL int Ntl_ManCheck( Ntl_Man_t * pMan ); -extern ABC_DLL int Ntl_ModelCheck( Ntl_Mod_t * pModel ); +extern ABC_DLL int Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain ); extern ABC_DLL void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel ); +extern ABC_DLL void Ntl_ModelTransformLatches( Ntl_Mod_t * pModel ); /*=== ntlMan.c ============================================================*/ extern ABC_DLL Ntl_Man_t * Ntl_ManAlloc(); extern ABC_DLL void Ntl_ManCleanup( Ntl_Man_t * p ); @@ -269,10 +325,12 @@ extern ABC_DLL int Ntl_ManLatchNum( Ntl_Man_t * p ); extern ABC_DLL Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ); extern ABC_DLL void Ntl_ManPrintStats( Ntl_Man_t * p ); extern ABC_DLL Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p ); +extern ABC_DLL void Ntl_ManPrintTypes( Ntl_Man_t * p ); extern ABC_DLL Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName ); extern ABC_DLL Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ); extern ABC_DLL Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ); extern ABC_DLL void Ntl_ModelFree( Ntl_Mod_t * p ); +extern ABC_DLL Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init ); /*=== ntlMap.c ============================================================*/ extern ABC_DLL Vec_Ptr_t * Ntl_MappingAlloc( int nLuts, int nVars ); extern ABC_DLL Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p ); @@ -294,11 +352,13 @@ extern ABC_DLL int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ); /*=== ntlTable.c ==========================================================*/ extern ABC_DLL Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName ); extern ABC_DLL Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ); -extern ABC_DLL int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber ); +extern ABC_DLL int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber ); extern ABC_DLL int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ); extern ABC_DLL int Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ); extern ABC_DLL void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet ); extern ABC_DLL int Ntl_ModelCountNets( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel ); +extern ABC_DLL Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ); /*=== ntlTime.c ==========================================================*/ extern ABC_DLL Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p ); /*=== ntlReadBlif.c ==========================================================*/ @@ -315,9 +375,14 @@ extern ABC_DLL Vec_Ptr_t * Ntl_ManCollectCiNames( Ntl_Man_t * p ); extern ABC_DLL Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManMarkCiCoNets( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p ); -extern ABC_DLL int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel ); extern ABC_DLL void Ntl_ManSetZeroInitValues( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManTransformInitValues( Ntl_Man_t * p ); +extern ABC_DLL int Ntl_ModelCombLeafNum( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ModelCombRootNum( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ModelSeqLeafNum( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ModelSeqRootNum( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel ); +extern ABC_DLL void Ntl_ModelClearNets( Ntl_Mod_t * pModel ); #ifdef __cplusplus } diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c index d5100312..d3aecc8d 100644 --- a/src/aig/ntl/ntlCheck.c +++ b/src/aig/ntl/ntlCheck.c @@ -40,11 +40,100 @@ SeeAlso [] ***********************************************************************/ -int Ntl_ModelCheck( Ntl_Mod_t * pModel ) +int Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain ) { Ntl_Obj_t * pObj; Ntl_Net_t * pNet; int i, k, fStatus = 1; + + // check root level model + if ( fMain ) + { + if ( Ntl_ModelLatchNum(pModel) > 0 ) + { + printf( "Root level model has %d registers.\n", pModel->pName, Ntl_ModelLatchNum(pModel) ); + fStatus = 0; + } + goto checkobjs; + } + + // check delay information + if ( pModel->attrBox && pModel->attrComb ) + { + if ( pModel->vDelays == NULL ) + { + printf( "Warning: Comb model %s does not have delay info. Default 1.0 delays are assumed.\n", pModel->pName ); + pModel->vDelays = Vec_IntAlloc( 3 ); + Vec_IntPush( pModel->vDelays, -1 ); + Vec_IntPush( pModel->vDelays, -1 ); + Vec_IntPush( pModel->vDelays, Aig_Float2Int(1.0) ); + } + if ( pModel->vTimeInputs != NULL ) + { + printf( "Combinational model %s has input arrival/required time information.\n", pModel->pName ); + fStatus = 0; + } + if ( pModel->vTimeOutputs != NULL ) + { + printf( "Combinational model %s has output arrival/required time information.\n", pModel->pName ); + fStatus = 0; + } + } + if ( pModel->attrBox && !pModel->attrComb ) + { + if ( pModel->vDelays != NULL ) + { + printf( "Sequential model %s has delay info.\n", pModel->pName ); + fStatus = 0; + } + if ( pModel->vTimeInputs == NULL ) + { + printf( "Warning: Seq model %s does not have input arrival/required time info. Default 0.0 is assumed.\n", pModel->pName ); + pModel->vTimeInputs = Vec_IntAlloc( 2 ); + Vec_IntPush( pModel->vTimeInputs, -1 ); + Vec_IntPush( pModel->vTimeInputs, Aig_Float2Int(1.0) ); + } + if ( pModel->vTimeOutputs == NULL ) + { + printf( "Warning: Seq model %s does not have output arrival/required time info. Default 0.0 is assumed.\n", pModel->pName ); + pModel->vTimeOutputs = Vec_IntAlloc( 2 ); + Vec_IntPush( pModel->vTimeOutputs, -1 ); + Vec_IntPush( pModel->vTimeOutputs, Aig_Float2Int(1.0) ); + } + } + + // check box attributes + if ( pModel->attrBox ) + { + if ( !pModel->attrWhite ) + { + if ( Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) > 0 ) + { + printf( "Model %s is a blackbox, yet it has %d nodes.\n", pModel->pName, Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) ); + fStatus = 0; + } + if ( Ntl_ModelLatchNum(pModel) > 0 ) + { + printf( "Model %s is a blackbox, yet it has %d registers.\n", pModel->pName, Ntl_ModelLatchNum(pModel) ); + fStatus = 0; + } + return fStatus; + } + // this is a white box + if ( pModel->attrComb && Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) == 0 ) + { + printf( "Model %s is a comb blackbox, yet it has no nodes.\n", pModel->pName ); + fStatus = 0; + } + if ( !pModel->attrComb && Ntl_ModelLatchNum(pModel) == 0 ) + { + printf( "Model %s is a seq blackbox, yet it has no registers.\n", pModel->pName ); + fStatus = 0; + } + } + +checkobjs: + // check nets Ntl_ModelForEachNet( pModel, pNet, i ) { if ( pNet->pName == NULL ) @@ -58,6 +147,8 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel ) fStatus = 0; } } + + // check objects Ntl_ModelForEachObj( pModel, pObj, i ) { Ntl_ObjForEachFanin( pObj, pNet, k ) @@ -89,8 +180,8 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel ) ***********************************************************************/ int Ntl_ManCheck( Ntl_Man_t * pMan ) { - Ntl_Mod_t * pMod1, * pMod2; - int i, k, fStatus = 1; + Ntl_Mod_t * pMod1; + int i, fStatus = 1; // check that the models have unique names Ntl_ManForEachModel( pMan, pMod1, i ) { @@ -99,16 +190,6 @@ int Ntl_ManCheck( Ntl_Man_t * pMan ) printf( "Model %d does not have a name\n", i ); fStatus = 0; } - Ntl_ManForEachModel( pMan, pMod2, k ) - { - if ( i >= k ) - continue; - if ( strcmp(pMod1->pName, pMod2->pName) == 0 ) - { - printf( "Models %d and %d have the same name (%s).\n", i, k, pMod1->pName ); - fStatus = 0; - } - } } // check that the models (except the first one) do not have boxes Ntl_ManForEachModel( pMan, pMod1, i ) @@ -124,9 +205,8 @@ int Ntl_ManCheck( Ntl_Man_t * pMan ) // check models Ntl_ManForEachModel( pMan, pMod1, i ) { - if ( !Ntl_ModelCheck( pMod1 ) ) + if ( !Ntl_ModelCheck( pMod1, i==0 ) ) fStatus = 0; - break; } return fStatus; } @@ -150,7 +230,7 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel ) Ntl_Obj_t * pNode; int i; - if ( Ntl_ModelIsBlackBox(pModel) ) + if ( !pModel->attrWhite ) return; // check for non-driven nets @@ -186,6 +266,37 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel ) Vec_PtrFree( vNets ); } +/**Function************************************************************* + + Synopsis [Fixed problems with non-driven nets in the model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ModelTransformLatches( Ntl_Mod_t * pModel ) +{ + Ntl_Mod_t * pMod[3] = { NULL }; + Ntl_Obj_t * pLatch; + int i, Init; + if ( Ntl_ModelLatchNum(pModel) == 0 ) + return; + Ntl_ModelForEachLatch( pModel, pLatch, i ) + { + Init = pLatch->LatchId.regInit; + if ( pMod[Init] == NULL ) + pMod[Init] = Ntl_ManCreateLatchModel( pModel->pMan, Init ); + pLatch->pImplem = pMod[Init]; + pLatch->Type = NTL_OBJ_BOX; + } + printf( "Root level model %s: %d registers turned into white seq boxes.\n", pModel->pName, Ntl_ModelLatchNum(pModel) ); + pModel->nObjs[NTL_OBJ_BOX] += Ntl_ModelLatchNum(pModel); + pModel->nObjs[NTL_OBJ_LATCH] = 0; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c index 8c7f7156..3ed6556d 100644 --- a/src/aig/ntl/ntlEc.c +++ b/src/aig/ntl/ntlEc.c @@ -42,33 +42,48 @@ void Ntl_ManCreateMissingInputs( Ntl_Mod_t * p1, Ntl_Mod_t * p2, int fSeq ) { Ntl_Obj_t * pObj; - Ntl_Net_t * pNet; - int i; - Ntl_ModelForEachPi( p1, pObj, i ) - { - pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName ); - if ( pNet == NULL ) - Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName ); - } - Ntl_ModelForEachPi( p2, pObj, i ) + Ntl_Net_t * pNet, * pNext; + int i, k; + if ( fSeq ) { - pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName ); - if ( pNet == NULL ) - Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName ); + Ntl_ModelForEachSeqLeaf( p1, pObj, i ) + { + Ntl_ObjForEachFanout( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + Ntl_ModelCreatePiWithName( p2, pNext->pName ); + } + } + Ntl_ModelForEachSeqLeaf( p2, pObj, i ) + { + Ntl_ObjForEachFanout( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p1, pNext->pName ); + if ( pNet == NULL ) + Ntl_ModelCreatePiWithName( p1, pNext->pName ); + } + } } - if ( !fSeq ) + else { - Ntl_ModelForEachLatch( p1, pObj, i ) + Ntl_ModelForEachCombLeaf( p1, pObj, i ) { - pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName ); - if ( pNet == NULL ) - Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName ); + Ntl_ObjForEachFanout( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + Ntl_ModelCreatePiWithName( p2, pNext->pName ); + } } - Ntl_ModelForEachLatch( p2, pObj, i ) + Ntl_ModelForEachCombLeaf( p2, pObj, i ) { - pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName ); - if ( pNet == NULL ) - Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName ); + Ntl_ObjForEachFanout( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p1, pNext->pName ); + if ( pNet == NULL ) + Ntl_ModelCreatePiWithName( p1, pNext->pName ); + } } } } @@ -89,38 +104,45 @@ void Ntl_ManDeriveCommonCis( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq ) Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1); Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2); Ntl_Obj_t * pObj; - Ntl_Net_t * pNet; - int i; - if ( fSeq ) - assert( Ntl_ModelPiNum(p1) == Ntl_ModelPiNum(p2) ); - else - assert( Ntl_ModelCiNum(p1) == Ntl_ModelCiNum(p2) ); + Ntl_Net_t * pNet, * pNext; + int i, k; // order the CIs Vec_PtrClear( pMan1->vCis ); Vec_PtrClear( pMan2->vCis ); - Ntl_ModelForEachPi( p1, pObj, i ) + if ( fSeq ) { - pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName ); - if ( pNet == NULL ) + assert( Ntl_ModelSeqLeafNum(p1) == Ntl_ModelSeqLeafNum(p2) ); + Ntl_ModelForEachSeqLeaf( p1, pObj, i ) { - printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" ); - return; + Ntl_ObjForEachFanout( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" ); + return; + } + Vec_PtrPush( pMan1->vCis, pNext ); + Vec_PtrPush( pMan2->vCis, pNet ); + } } - Vec_PtrPush( pMan1->vCis, pObj ); - Vec_PtrPush( pMan2->vCis, pNet->pDriver ); } - if ( !fSeq ) + else { - Ntl_ModelForEachLatch( p1, pObj, i ) + assert( Ntl_ModelCombLeafNum(p1) == Ntl_ModelCombLeafNum(p2) ); + Ntl_ModelForEachCombLeaf( p1, pObj, i ) { - pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName ); - if ( pNet == NULL ) + Ntl_ObjForEachFanout( pObj, pNext, k ) { - printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" ); - return; + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" ); + return; + } + Vec_PtrPush( pMan1->vCis, pNext ); + Vec_PtrPush( pMan2->vCis, pNet ); } - Vec_PtrPush( pMan1->vCis, pObj ); - Vec_PtrPush( pMan2->vCis, pNet->pDriver ); } } } @@ -141,45 +163,47 @@ void Ntl_ManDeriveCommonCos( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq ) Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1); Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2); Ntl_Obj_t * pObj; - Ntl_Net_t * pNet; - int i; -// if ( fSeq ) -// assert( Ntl_ModelPoNum(p1) == Ntl_ModelPoNum(p2) ); -// else -// assert( Ntl_ModelCoNum(p1) == Ntl_ModelCoNum(p2) ); - // remember PO in the corresponding net of the second design - Ntl_ModelForEachPo( p2, pObj, i ) - Ntl_ObjFanin0(pObj)->pCopy = pObj; + Ntl_Net_t * pNet, * pNext; + int i, k; // order the COs Vec_PtrClear( pMan1->vCos ); Vec_PtrClear( pMan2->vCos ); - Ntl_ModelForEachPo( p1, pObj, i ) + if ( fSeq ) { - pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName ); - if ( pNet == NULL ) + assert( Ntl_ModelSeqRootNum(p1) == Ntl_ModelSeqRootNum(p2) ); + Ntl_ModelForEachSeqRoot( p1, pObj, i ) { - printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", - Ntl_ObjFanin0(pObj)->pName ); - continue; + Ntl_ObjForEachFanin( pObj, pNext, k ) + { + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", + pNext->pName ); + continue; + } + Vec_PtrPush( pMan1->vCos, pNext ); + Vec_PtrPush( pMan2->vCos, pNet ); + } } - Vec_PtrPush( pMan1->vCos, pObj ); - Vec_PtrPush( pMan2->vCos, pNet->pCopy ); } - if ( !fSeq ) + else { - Ntl_ModelForEachLatch( p2, pObj, i ) - Ntl_ObjFanin0(pObj)->pCopy = pObj; - Ntl_ModelForEachLatch( p1, pObj, i ) + assert( Ntl_ModelCombRootNum(p1) == Ntl_ModelCombRootNum(p2) ); + Ntl_ModelForEachCombRoot( p1, pObj, i ) { - pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName ); - if ( pNet == NULL ) + Ntl_ObjForEachFanin( pObj, pNext, k ) { - printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", - Ntl_ObjFanin0(pObj)->pName ); - continue; + pNet = Ntl_ModelFindNet( p2, pNext->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", + pNext->pName ); + continue; + } + Vec_PtrPush( pMan1->vCos, pNext ); + Vec_PtrPush( pMan2->vCos, pNet ); } - Vec_PtrPush( pMan1->vCos, pObj ); - Vec_PtrPush( pMan2->vCos, pNet->pCopy ); } } } @@ -214,19 +238,19 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan // make sure they are compatible pModel1 = Ntl_ManRootModel( pMan1 ); pModel2 = Ntl_ManRootModel( pMan2 ); - if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) ) + if ( Ntl_ModelCombLeafNum(pModel1) != Ntl_ModelCombLeafNum(pModel2) ) { printf( "Warning: The number of inputs in the designs is different (%d and %d).\n", - Ntl_ModelCiNum(pModel1), Ntl_ModelCiNum(pModel2) ); + Ntl_ModelCombLeafNum(pModel1), Ntl_ModelCombLeafNum(pModel2) ); } - if ( Ntl_ModelCoNum(pModel1) != Ntl_ModelCoNum(pModel2) ) + if ( Ntl_ModelCombRootNum(pModel1) != Ntl_ModelCombRootNum(pModel2) ) { printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", - Ntl_ModelCoNum(pModel1), Ntl_ModelCoNum(pModel2) ); + Ntl_ModelCombRootNum(pModel1), Ntl_ModelCombRootNum(pModel2) ); } // normalize inputs/outputs Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 ); - if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) ) + if ( Ntl_ModelCombLeafNum(pModel1) != Ntl_ModelCombLeafNum(pModel2) ) { if ( pMan1 ) Ntl_ManFree( pMan1 ); if ( pMan2 ) Ntl_ManFree( pMan2 ); @@ -243,8 +267,8 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan return; } // derive AIGs - *ppMan1 = Ntl_ManCollapseForCec( pMan1 ); - *ppMan2 = Ntl_ManCollapseForCec( pMan2 ); + *ppMan1 = Ntl_ManCollapseComb( pMan1 ); + *ppMan2 = Ntl_ManCollapseComb( pMan2 ); // cleanup Ntl_ManFree( pMan1 ); Ntl_ManFree( pMan2 ); @@ -263,7 +287,9 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan ***********************************************************************/ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ) { - Aig_Man_t * pAig; + extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); + + Aig_Man_t * pAig1, * pAig2, * pAig; Ntl_Man_t * pMan1, * pMan2; Ntl_Mod_t * pModel1, * pModel2; // read the netlists @@ -286,12 +312,12 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ) printf( "Ntl_ManPrepareSec(): The designs have no latches. Use combinational command \"*cec\".\n" ); return NULL; } - if ( Ntl_ModelPiNum(pModel1) != Ntl_ModelPiNum(pModel2) ) + if ( Ntl_ModelSeqLeafNum(pModel1) != Ntl_ModelSeqLeafNum(pModel2) ) { printf( "Warning: The number of inputs in the designs is different (%d and %d).\n", Ntl_ModelPiNum(pModel1), Ntl_ModelPiNum(pModel2) ); } - if ( Ntl_ModelPoNum(pModel1) != Ntl_ModelPoNum(pModel2) ) + if ( Ntl_ModelSeqRootNum(pModel1) != Ntl_ModelSeqRootNum(pModel2) ) { printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", Ntl_ModelPoNum(pModel1), Ntl_ModelPoNum(pModel2) ); @@ -308,9 +334,12 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ) return NULL; } // derive AIGs - pAig = Ntl_ManCollapseForSec( pMan1, pMan2 ); + pAig1 = Ntl_ManCollapseSeq( pMan1 ); + pAig2 = Ntl_ManCollapseSeq( pMan2 ); + pAig = Saig_ManCreateMiter( pAig1, pAig2, 0 ); + Aig_ManStop( pAig1 ); + Aig_ManStop( pAig2 ); // cleanup - pMan1->pAig = pMan2->pAig = NULL; Ntl_ManFree( pMan1 ); Ntl_ManFree( pMan2 ); return pAig; diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index be6626df..a552f949 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -178,6 +178,9 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) if ( Ntl_ObjIsBox(pObj) ) { int LevelCur, LevelMax = -TIM_ETERNITY; + assert( Ntl_BoxIsComb(pObj) ); + assert( Ntl_ModelLatchNum(pObj->pImplem) == 0 ); + assert( pObj->pImplem->vDelays != NULL ); Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) ); Ntl_ObjForEachFanin( pObj, pNetFanin, i ) { @@ -218,7 +221,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) Ntl_Mod_t * pRoot; Ntl_Obj_t * pObj; Ntl_Net_t * pNet; - int i, nUselessObjects; + int i, k, nUselessObjects; Ntl_ManCleanup( p ); assert( Vec_PtrSize(p->vCis) == 0 ); assert( Vec_PtrSize(p->vCos) == 0 ); @@ -231,63 +234,39 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) p->pAig->pSpec = Aig_UtilStrsav( p->pSpec ); // get the root model pRoot = Ntl_ManRootModel( p ); + assert( Ntl_ModelLatchNum(pRoot) == 0 ); // clear net visited flags - Ntl_ModelForEachNet( pRoot, pNet, i ) + Ntl_ModelClearNets( pRoot ); + // collect mapping leafs + Ntl_ModelForEachMapLeaf( pRoot, pObj, i ) { - pNet->nVisits = 0; - pNet->pCopy = NULL; - } - // collect primary inputs - Ntl_ModelForEachPi( pRoot, pObj, i ) - { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); - Vec_PtrPush( p->vCis, pNet ); - pNet->pCopy = Aig_ObjCreatePi( p->pAig ); - if ( pNet->nVisits ) - { - printf( "Ntl_ManExtract(): Primary input appears twice in the list.\n" ); - return 0; - } - pNet->nVisits = 2; - } - // collect latch outputs - Ntl_ModelForEachLatch( pRoot, pObj, i ) - { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); - Vec_PtrPush( p->vCis, pNet ); - pNet->pCopy = Aig_ObjCreatePi( p->pAig ); - if ( pNet->nVisits ) + assert( !Ntl_ObjIsBox(pObj) || Ntl_BoxIsBlack(pObj) || Ntl_ModelLatchNum(pObj->pImplem) > 0 ); + Ntl_ObjForEachFanout( pObj, pNet, k ) { - printf( "Ntl_ManExtract(): Latch output is duplicated or defined as a primary input.\n" ); - return 0; + Vec_PtrPush( p->vCis, pNet ); + pNet->pCopy = Aig_ObjCreatePi( p->pAig ); + if ( pNet->nVisits ) + { + printf( "Ntl_ManExtract(): Seq leaf is duplicated or defined as a primary input.\n" ); + return 0; + } + pNet->nVisits = 2; } - pNet->nVisits = 2; } - // visit the nodes starting from primary outputs - Ntl_ModelForEachPo( pRoot, pObj, i ) + p->iLastCi = Aig_ManPiNum(p->pAig); + // collect mapping roots + Ntl_ModelForEachMapRoot( pRoot, pObj, i ) { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManExtract_rec( p, pNet ) ) - { - printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" ); - return 0; - } - Vec_PtrPush( p->vCos, pNet ); - Aig_ObjCreatePo( p->pAig, pNet->pCopy ); - } - // visit the nodes starting from latch inputs - Ntl_ModelForEachLatch( pRoot, pObj, i ) - { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManExtract_rec( p, pNet ) ) + Ntl_ObjForEachFanin( pObj, pNet, k ) { - printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" ); - return 0; + if ( !Ntl_ManExtract_rec( p, pNet ) ) + { + printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" ); + return 0; + } + Vec_PtrPush( p->vCos, pNet ); + Aig_ObjCreatePo( p->pAig, pNet->pCopy ); } - Vec_PtrPush( p->vCos, pNet ); - Aig_ObjCreatePo( p->pAig, pNet->pCopy ); } // visit dangling boxes Ntl_ModelForEachBox( pRoot, pObj, i ) @@ -314,6 +293,9 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) return pAig; } + + + /**Function************************************************************* Synopsis [Collects the nodes in a topological order.] @@ -325,9 +307,9 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox ) +int Ntl_ManCollapseBox_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq ) { - extern int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ); + extern int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, int fSeq ); Ntl_Mod_t * pModel = pBox->pImplem; Ntl_Obj_t * pObj; Ntl_Net_t * pNet, * pNetBox; @@ -335,8 +317,7 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox ) assert( Ntl_ObjFaninNum(pBox) == Ntl_ModelPiNum(pModel) ); assert( Ntl_ObjFanoutNum(pBox) == Ntl_ModelPoNum(pModel) ); // clear net visited flags - Ntl_ModelForEachNet( pModel, pNet, i ) - pNet->nVisits = 0; + Ntl_ModelClearNets( pModel ); // transfer from the box to the PIs of the model Ntl_ModelForEachPi( pModel, pObj, i ) { @@ -345,17 +326,41 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox ) pNet->pCopy = pNetBox->pCopy; pNet->nVisits = 2; } + // check if there are registers + if ( Ntl_ModelLatchNum(pModel) ) + { + Ntl_ModelForEachLatch( pModel, pObj, i ) + { + pNet = Ntl_ObjFanout0(pObj); + pNet->pCopy = Aig_ObjCreatePi( p->pAig ); + if ( fSeq && Ntl_ObjIsInit1( pObj ) ) + pNet->pCopy = Aig_Not(pNet->pCopy); + pNet->nVisits = 2; + } + } // compute AIG for the internal nodes - Ntl_ModelForEachPo( pModel, pObj, i ) - if ( !Ntl_ManCollapse_rec( p, Ntl_ObjFanin0(pObj) ) ) - return 0; - // transfer from the POs of the model to the box Ntl_ModelForEachPo( pModel, pObj, i ) { pNet = Ntl_ObjFanin0(pObj); + if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) ) + return 0; pNetBox = Ntl_ObjFanout( pBox, i ); pNetBox->pCopy = pNet->pCopy; } + // compute AIGs for the registers + if ( Ntl_ModelLatchNum(pModel) ) + { + Ntl_ModelForEachLatch( pModel, pObj, i ) + { + pNet = Ntl_ObjFanin0(pObj); + if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) ) + return 0; + if ( fSeq && Ntl_ObjIsInit1( pObj ) ) + Vec_PtrPush( p->vLatchIns, Aig_Not(pNet->pCopy) ); + else + Vec_PtrPush( p->vLatchIns, pNet->pCopy ); + } + } return 1; } @@ -370,7 +375,7 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox ) SeeAlso [] ***********************************************************************/ -int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) +int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, int fSeq ) { Ntl_Obj_t * pObj; Ntl_Net_t * pNetFanin; @@ -388,12 +393,13 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) assert( Ntl_ObjIsNode(pObj) || Ntl_ObjIsBox(pObj) ); // visit the input nets of the box Ntl_ObjForEachFanin( pObj, pNetFanin, i ) - if ( !Ntl_ManCollapse_rec( p, pNetFanin ) ) + if ( !Ntl_ManCollapse_rec( p, pNetFanin, fSeq ) ) return 0; // add box inputs/outputs to COs/CIs if ( Ntl_ObjIsBox(pObj) ) { - if ( !Ntl_ManBuildModelAig( p, pObj ) ) + assert( Ntl_BoxIsWhite(pObj) ); + if ( !Ntl_ManCollapseBox_rec( p, pObj, fSeq ) ) return 0; } if ( Ntl_ObjIsNode(pObj) ) @@ -417,310 +423,125 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq ) { Aig_Man_t * pAig; + Aig_Obj_t * pTemp; Ntl_Mod_t * pRoot; - Ntl_Obj_t * pObj; Ntl_Net_t * pNet; int i; - // start the AIG manager - assert( p->pAig == NULL ); + assert( Vec_PtrSize(p->vCis) != 0 ); + assert( Vec_PtrSize(p->vCos) != 0 ); + assert( Vec_PtrSize(p->vLatchIns) == 0 ); + // clear net visited flags + pRoot = Ntl_ManRootModel(p); + Ntl_ModelClearNets( pRoot ); + assert( Ntl_ModelLatchNum(pRoot) == 0 ); + // create the manager p->pAig = Aig_ManStart( 10000 ); p->pAig->pName = Aig_UtilStrsav( p->pName ); p->pAig->pSpec = Aig_UtilStrsav( p->pSpec ); - // get the root model - pRoot = Ntl_ManRootModel( p ); - // clear net visited flags - Ntl_ModelForEachNet( pRoot, pNet, i ) - { - pNet->nVisits = 0; - pNet->pCopy = NULL; - } - // collect primary inputs - Ntl_ModelForEachPi( pRoot, pObj, i ) - { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); - pNet->pCopy = Aig_ObjCreatePi( p->pAig ); - if ( pNet->nVisits ) - { - printf( "Ntl_ManCollapse(): Primary input appears twice in the list.\n" ); - return 0; - } - pNet->nVisits = 2; - } - // collect latch outputs - Ntl_ModelForEachLatch( pRoot, pObj, i ) + // set the inputs + Ntl_ManForEachCiNet( p, pNet, i ) { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); pNet->pCopy = Aig_ObjCreatePi( p->pAig ); - if ( fSeq && (pObj->LatchId & 3) == 1 ) - pNet->pCopy = Aig_Not(pNet->pCopy); if ( pNet->nVisits ) { - printf( "Ntl_ManCollapse(): Latch output is duplicated or defined as a primary input.\n" ); + printf( "Ntl_ManCollapseForCec(): Primary input appears twice in the list.\n" ); return 0; } pNet->nVisits = 2; } - // visit the nodes starting from primary outputs - Ntl_ModelForEachPo( pRoot, pObj, i ) + // derive the outputs + Ntl_ManForEachCoNet( p, pNet, i ) { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManCollapse_rec( p, pNet ) ) + if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) ) { - printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" ); + printf( "Ntl_ManCollapseForCec(): Error: Combinational loop is detected.\n" ); return 0; } Aig_ObjCreatePo( p->pAig, pNet->pCopy ); } - // visit the nodes starting from latch inputs outputs - Ntl_ModelForEachLatch( pRoot, pObj, i ) - { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManCollapse_rec( p, pNet ) ) - { - printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" ); - return 0; - } - if ( fSeq && (pObj->LatchId & 3) == 1 ) - Aig_ObjCreatePo( p->pAig, Aig_Not(pNet->pCopy) ); - else - Aig_ObjCreatePo( p->pAig, pNet->pCopy ); - } + // add the latch inputs + Vec_PtrForEachEntry( p->vLatchIns, pTemp, i ) + Aig_ObjCreatePo( p->pAig, pTemp ); // cleanup the AIG + Aig_ManSetRegNum( p->pAig, Vec_PtrSize(p->vLatchIns) ); Aig_ManCleanup( p->pAig ); pAig = p->pAig; p->pAig = NULL; return pAig; } + /**Function************************************************************* - Synopsis [Derives AIG for CEC.] + Synopsis [Collapses the netlist combinationally.] - Description [Uses CIs/COs collected in the internal arrays.] + Description [Checks for combinational loops. Collects PI/PO nets. + Collects nodes in the topological order.] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p ) +Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p ) { - Aig_Man_t * pAig; Ntl_Mod_t * pRoot; Ntl_Obj_t * pObj; Ntl_Net_t * pNet; - int i; - // clear net visited flags + int i, k; + Vec_PtrClear( p->vCis ); + Vec_PtrClear( p->vCos ); + Vec_PtrClear( p->vLatchIns ); + // prepare the model pRoot = Ntl_ManRootModel(p); - Ntl_ModelForEachNet( pRoot, pNet, i ) - { - pNet->nVisits = 0; - pNet->pCopy = NULL; - } - // create the manager - p->pAig = Aig_ManStart( 10000 ); - p->pAig->pName = Aig_UtilStrsav( p->pName ); - p->pAig->pSpec = Aig_UtilStrsav( p->pSpec ); - // set the inputs - Ntl_ManForEachCiNet( p, pObj, i ) - { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); - pNet->pCopy = Aig_ObjCreatePi( p->pAig ); - if ( pNet->nVisits ) - { - printf( "Ntl_ManCollapseForCec(): Primary input appears twice in the list.\n" ); - return 0; - } - pNet->nVisits = 2; - } - // derive the outputs - Ntl_ManForEachCoNet( p, pObj, i ) - { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManCollapse_rec( p, pNet ) ) - { - printf( "Ntl_ManCollapseForCec(): Error: Combinational loop is detected.\n" ); - return 0; - } - Aig_ObjCreatePo( p->pAig, pNet->pCopy ); - } - // cleanup the AIG - Aig_ManCleanup( p->pAig ); - pAig = p->pAig; p->pAig = NULL; - return pAig; + // collect the leaves for this traversal + Ntl_ModelForEachCombLeaf( pRoot, pObj, i ) + Ntl_ObjForEachFanout( pObj, pNet, k ) + Vec_PtrPush( p->vCis, pNet ); + // collect the roots for this traversal + Ntl_ModelForEachCombRoot( pRoot, pObj, i ) + Ntl_ObjForEachFanin( pObj, pNet, k ) + Vec_PtrPush( p->vCos, pNet ); + // perform the traversal + return Ntl_ManCollapse( p, 0 ); } /**Function************************************************************* - Synopsis [Derives AIG for SEC.] + Synopsis [Collapses the netlist combinationally.] - Description [Uses CIs/COs collected in the internal arrays.] + Description [Checks for combinational loops. Collects PI/PO nets. + Collects nodes in the topological order.] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 ) +Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p ) { - Aig_Man_t * pAig; - Aig_Obj_t * pMiter; - Ntl_Mod_t * pRoot1, * pRoot2; + Ntl_Mod_t * pRoot; Ntl_Obj_t * pObj; Ntl_Net_t * pNet; - Vec_Ptr_t * vPairs; - int i; - assert( Vec_PtrSize(p1->vCis) > 0 ); - assert( Vec_PtrSize(p1->vCos) > 0 ); - assert( Vec_PtrSize(p1->vCis) == Vec_PtrSize(p2->vCis) ); - assert( Vec_PtrSize(p1->vCos) == Vec_PtrSize(p2->vCos) ); - - // create the manager - pAig = p1->pAig = p2->pAig = Aig_ManStart( 10000 ); - pAig->pName = Aig_UtilStrsav( p1->pName ); - pAig->pSpec = Aig_UtilStrsav( p1->pSpec ); - vPairs = Vec_PtrStart( 2 * Vec_PtrSize(p1->vCos) ); - // placehoder output to be used later for the miter output - Aig_ObjCreatePo( pAig, Aig_ManConst1(pAig) ); - - ///////////////////////////////////////////////////// - // clear net visited flags - pRoot1 = Ntl_ManRootModel(p1); - Ntl_ModelForEachNet( pRoot1, pNet, i ) - { - pNet->nVisits = 0; - pNet->pCopy = NULL; - } - // primary inputs - Ntl_ManForEachCiNet( p1, pObj, i ) - { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); - pNet->pCopy = Aig_ObjCreatePi( pAig ); - if ( pNet->nVisits ) - { - printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" ); - return 0; - } - pNet->nVisits = 2; - } - // latch outputs - Ntl_ModelForEachLatch( pRoot1, pObj, i ) - { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); - pNet->pCopy = Aig_ObjCreatePi( pAig ); - if ( (pObj->LatchId & 3) == 1 ) - pNet->pCopy = Aig_Not(pNet->pCopy); - if ( pNet->nVisits ) - { - printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" ); - return 0; - } - pNet->nVisits = 2; - } - // derive the outputs - Ntl_ManForEachCoNet( p1, pObj, i ) - { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManCollapse_rec( p1, pNet ) ) - { - printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" ); - return 0; - } -// Aig_ObjCreatePo( pAig, pNet->pCopy ); - Vec_PtrWriteEntry( vPairs, 2 * i, pNet->pCopy ); - } - // visit the nodes starting from latch inputs outputs - Ntl_ModelForEachLatch( pRoot1, pObj, i ) - { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManCollapse_rec( p1, pNet ) ) - { - printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" ); - return 0; - } - if ( (pObj->LatchId & 3) == 1 ) - Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) ); - else - Aig_ObjCreatePo( pAig, pNet->pCopy ); - } - - ///////////////////////////////////////////////////// - // clear net visited flags - pRoot2 = Ntl_ManRootModel(p2); - Ntl_ModelForEachNet( pRoot2, pNet, i ) - { - pNet->nVisits = 0; - pNet->pCopy = NULL; - } - // primary inputs - Ntl_ManForEachCiNet( p2, pObj, i ) - { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); - pNet->pCopy = Aig_ManPi( pAig, i ); - if ( pNet->nVisits ) - { - printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" ); - return 0; - } - pNet->nVisits = 2; - } - // latch outputs - Ntl_ModelForEachLatch( pRoot2, pObj, i ) - { - assert( Ntl_ObjFanoutNum(pObj) == 1 ); - pNet = Ntl_ObjFanout0(pObj); - pNet->pCopy = Aig_ObjCreatePi( pAig ); - if ( (pObj->LatchId & 3) == 1 ) - pNet->pCopy = Aig_Not(pNet->pCopy); - if ( pNet->nVisits ) - { - printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" ); - return 0; - } - pNet->nVisits = 2; - } - // derive the outputs - Ntl_ManForEachCoNet( p2, pObj, i ) - { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManCollapse_rec( p2, pNet ) ) - { - printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" ); - return 0; - } -// Aig_ObjCreatePo( pAig, pNet->pCopy ); - Vec_PtrWriteEntry( vPairs, 2 * i + 1, pNet->pCopy ); - } - // visit the nodes starting from latch inputs outputs - Ntl_ModelForEachLatch( pRoot2, pObj, i ) - { - pNet = Ntl_ObjFanin0(pObj); - if ( !Ntl_ManCollapse_rec( p2, pNet ) ) - { - printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" ); - return 0; - } - if ( (pObj->LatchId & 3) == 1 ) - Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) ); - else - Aig_ObjCreatePo( pAig, pNet->pCopy ); - } - - ///////////////////////////////////////////////////// - pMiter = Aig_Miter(pAig, vPairs); - Vec_PtrFree( vPairs ); - Aig_ObjPatchFanin0( pAig, Aig_ManPo(pAig,0), pMiter ); - Aig_ManSetRegNum( pAig, Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 ) ); - Aig_ManCleanup( pAig ); - return pAig; + int i, k; + Vec_PtrClear( p->vCis ); + Vec_PtrClear( p->vCos ); + Vec_PtrClear( p->vLatchIns ); + // prepare the model + pRoot = Ntl_ManRootModel(p); + // collect the leaves for this traversal + Ntl_ModelForEachSeqLeaf( pRoot, pObj, i ) + Ntl_ObjForEachFanout( pObj, pNet, k ) + Vec_PtrPush( p->vCis, pNet ); + // collect the roots for this traversal + Ntl_ModelForEachSeqRoot( pRoot, pObj, i ) + Ntl_ObjForEachFanin( pObj, pNet, k ) + Vec_PtrPush( p->vCos, pNet ); + // perform the traversal + return Ntl_ManCollapse( p, 1 ); } + /**Function************************************************************* Synopsis [Increments reference counter of the net.] @@ -806,11 +627,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan vCover = Vec_IntAlloc( 100 ); vMemory = Vec_IntAlloc( 1 << 16 ); // count the number of fanouts of each net - Ntl_ModelForEachNet( pRoot, pNet, i ) - { - pNet->pCopy = NULL; - pNet->fMark = 0; - } + Ntl_ModelClearNets( pRoot ); Ntl_ModelForEachObj( pRoot, pObj, i ) Ntl_ObjForEachFanin( pObj, pNet, k ) Ntl_NetIncrementRefs( pNet ); @@ -867,11 +684,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan } } // Aig_ManCleanPioNumbers( pAig ); - Ntl_ModelForEachNet( pRoot, pNet, i ) - { - pNet->pCopy = NULL; - pNet->fMark = 0; - } + Ntl_ModelClearNets( pRoot ); Vec_IntFree( vCover ); Vec_IntFree( vMemory ); // create timing manager from the current design diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 6de41679..cdc1323b 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -203,7 +203,7 @@ void Ntl_ManResetComplemented( Ntl_Man_t * p, Aig_Man_t * pAigCol ) pRoot = Ntl_ManRootModel(p); Ntl_ModelForEachLatch( pRoot, pObj, i ) { - if ( (pObj->LatchId & 3) == 1 ) + if ( Ntl_ObjIsInit1( pObj ) ) { pObjCol = Ntl_ObjFanout0(pObj)->pCopy; assert( pObjCol->fPhase == 0 ); @@ -275,7 +275,7 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew, 0 ); + pAigCol = Ntl_ManCollapseComb( pNew ); // perform fraiging for the given design nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol); @@ -309,7 +309,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew, 1 ); + pAigCol = Ntl_ManCollapseSeq( pNew ); // perform SCL for the given design Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) ); @@ -343,7 +343,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew, 1 ); + pAigCol = Ntl_ManCollapseSeq( pNew ); // perform SCL for the given design Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) ); @@ -377,7 +377,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars ) // collapse the AIG pAig = Ntl_ManExtract( p ); pNew = Ntl_ManInsertAig( p, pAig ); - pAigCol = Ntl_ManCollapse( pNew, 1 ); + pAigCol = Ntl_ManCollapseSeq( pNew ); // perform SCL for the given design Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) ); @@ -502,7 +502,7 @@ void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol ) iLatch = 0; Ntl_ModelForEachLatch( pRoot, pObj, i ) { - if ( (pObj->LatchId & 3) == 1 ) + if ( Ntl_ObjIsInit1( pObj ) ) { pObjCol = Aig_ManPi( pAigCol, Ntl_ModelPiNum(pRoot) + iLatch ); assert( pObjCol->fMarkA == 0 ); @@ -524,7 +524,7 @@ void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol ) iLatch = 0; Ntl_ModelForEachLatch( pRoot, pObj, i ) { - if ( (pObj->LatchId & 3) == 1 ) + if ( Ntl_ObjIsInit1( pObj ) ) { // flip the latch input pObjCol = Aig_ManPo( pAigCol, Ntl_ModelPoNum(pRoot) + iLatch ); @@ -554,7 +554,7 @@ Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars ) Ntl_Man_t * pNew; Aig_Man_t * pAigRed, * pAigCol; // collapse the AIG - pAigCol = Ntl_ManCollapse( p, 1 ); + pAigCol = Ntl_ManCollapseSeq( p ); Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) ); // transform the collapsed AIG pAigRed = Fra_FraigInduction( pAigCol, pPars ); diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c index 3cd9470b..9675eb28 100644 --- a/src/aig/ntl/ntlInsert.c +++ b/src/aig/ntl/ntlInsert.c @@ -257,7 +257,7 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ) ***********************************************************************/ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) { - char Buffer[100]; + char Buffer[100]; Vec_Ptr_t * vObjs; Vec_Int_t * vTruth; Vec_Int_t * vCover; diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c index e80e02c6..0083e04c 100644 --- a/src/aig/ntl/ntlMan.c +++ b/src/aig/ntl/ntlMan.c @@ -50,9 +50,14 @@ Ntl_Man_t * Ntl_ManAlloc() p->vCos = Vec_PtrAlloc( 1000 ); p->vNodes = Vec_PtrAlloc( 1000 ); p->vBox1Cos = Vec_IntAlloc( 1000 ); + p->vLatchIns = Vec_PtrAlloc( 1000 ); // start the manager p->pMemObjs = Aig_MmFlexStart(); p->pMemSops = Aig_MmFlexStart(); + // allocate model table + p->nModTableSize = Aig_PrimeCudd( 100 ); + p->pModTable = ALLOC( Ntl_Mod_t *, p->nModTableSize ); + memset( p->pModTable, 0, sizeof(Ntl_Mod_t *) * p->nModTableSize ); return p; } @@ -185,14 +190,16 @@ void Ntl_ManFree( Ntl_Man_t * p ) Ntl_ModelFree( pModel ); Vec_PtrFree( p->vModels ); } - if ( p->vCis ) Vec_PtrFree( p->vCis ); - if ( p->vCos ) Vec_PtrFree( p->vCos ); - if ( p->vNodes ) Vec_PtrFree( p->vNodes ); - if ( p->vBox1Cos ) Vec_IntFree( p->vBox1Cos ); - if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 ); - if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 ); - if ( p->pAig ) Aig_ManStop( p->pAig ); - if ( p->pManTime ) Tim_ManStop( p->pManTime ); + if ( p->vCis ) Vec_PtrFree( p->vCis ); + if ( p->vCos ) Vec_PtrFree( p->vCos ); + if ( p->vNodes ) Vec_PtrFree( p->vNodes ); + if ( p->vBox1Cos ) Vec_IntFree( p->vBox1Cos ); + if ( p->vLatchIns ) Vec_PtrFree( p->vLatchIns ); + if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 ); + if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 ); + if ( p->pAig ) Aig_ManStop( p->pAig ); + if ( p->pManTime ) Tim_ManStop( p->pManTime ); + FREE( p->pModTable ); free( p ); } @@ -239,7 +246,7 @@ int Ntl_ManLatchNum( Ntl_Man_t * p ) SeeAlso [] ***********************************************************************/ -Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ) +Ntl_Mod_t * Ntl_ManFindModel_old( Ntl_Man_t * p, char * pName ) { Ntl_Mod_t * pModel; int i; @@ -276,6 +283,8 @@ void Ntl_ManPrintStats( Ntl_Man_t * p ) printf( "\n" ); fflush( stdout ); assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) ); + Ntl_ManPrintTypes( p ); + fflush( stdout ); } /**Function************************************************************* @@ -294,6 +303,67 @@ Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p ) return p->pManTime; } +/**Function************************************************************* + + Synopsis [Saves the model type.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManSaveBoxType( Ntl_Obj_t * pObj ) +{ + Ntl_Mod_t * pModel = pObj->pImplem; + int Number = 0; + assert( Ntl_ObjIsBox(pObj) ); + Number |= (pModel->attrWhite << 0); + Number |= (pModel->attrBox << 1); + Number |= (pModel->attrComb << 2); + Number |= (pModel->attrKeep << 3); + pModel->pMan->BoxTypes[Number]++; +} + +/**Function************************************************************* + + Synopsis [Saves the model type.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManPrintTypes( Ntl_Man_t * p ) +{ + Ntl_Mod_t * pModel; + Ntl_Obj_t * pObj; + int i; + pModel = Ntl_ManRootModel( p ); + if ( Ntl_ModelBoxNum(pModel) == 0 ) + return; + printf( "BOX STATISTICS:\n" ); + Ntl_ModelForEachBox( pModel, pObj, i ) + Ntl_ManSaveBoxType( pObj ); + for ( i = 0; i < 15; i++ ) + { + if ( !p->BoxTypes[i] ) + continue; + printf( "%5d :", p->BoxTypes[i] ); + printf( " %s", ((i & 1) > 0)? "white": "black" ); + printf( " %s", ((i & 2) > 0)? "box ": "logic" ); + printf( " %s", ((i & 4) > 0)? "comb ": "seq " ); + printf( " %s", ((i & 8) > 0)? "keep ": "sweep" ); + printf( "\n" ); + } + printf( "Total box instances = %6d.\n\n", Ntl_ModelBoxNum(pModel) ); + for ( i = 0; i < 15; i++ ) + p->BoxTypes[i] = 0; +} + /**Function************************************************************* Synopsis [Allocates the model.] @@ -311,16 +381,25 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName ) // start the manager p = ALLOC( Ntl_Mod_t, 1 ); memset( p, 0, sizeof(Ntl_Mod_t) ); + p->attrBox = 1; + p->attrComb = 1; + p->attrWhite = 1; + p->attrKeep = 0; p->pMan = pMan; p->pName = Ntl_ManStoreName( p->pMan, pName ); - Vec_PtrPush( pMan->vModels, p ); - p->vObjs = Vec_PtrAlloc( 1000 ); - p->vPis = Vec_PtrAlloc( 100 ); - p->vPos = Vec_PtrAlloc( 100 ); + p->vObjs = Vec_PtrAlloc( 100 ); + p->vPis = Vec_PtrAlloc( 10 ); + p->vPos = Vec_PtrAlloc( 10 ); // start the table - p->nTableSize = Aig_PrimeCudd( 1000 ); + p->nTableSize = Aig_PrimeCudd( 100 ); p->pTable = ALLOC( Ntl_Net_t *, p->nTableSize ); memset( p->pTable, 0, sizeof(Ntl_Net_t *) * p->nTableSize ); + // add model to the table + if ( !Ntl_ManAddModel( pMan, p ) ) + { + Ntl_ModelFree( p ); + return NULL; + } return p; } @@ -371,11 +450,14 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) if ( pNet->pCopy != NULL ) Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k ); if ( Ntl_ObjIsLatch(pObj) ) + { ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId; + ((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock->pCopy; + } } pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL; - pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL; - pModelNew->vRequireds = pModelOld->vRequireds? Vec_IntDup( pModelOld->vRequireds ) : NULL; + pModelNew->vTimeInputs = pModelOld->vTimeInputs? Vec_IntDup( pModelOld->vTimeInputs ) : NULL; + pModelNew->vTimeOutputs = pModelOld->vTimeOutputs? Vec_IntDup( pModelOld->vTimeOutputs ) : NULL; return pModelNew; } @@ -397,11 +479,20 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) Ntl_Obj_t * pObj; int i, k; pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName ); + pModelNew->attrWhite = pModelOld->attrWhite; + pModelNew->attrBox = pModelOld->attrBox; + pModelNew->attrComb = pModelOld->attrComb; + pModelNew->attrKeep = pModelOld->attrKeep; Ntl_ModelForEachObj( pModelOld, pObj, i ) pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj ); Ntl_ModelForEachNet( pModelOld, pNet, i ) { pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName ); + if ( pNet->pDriver == NULL ) + { + assert( !pModelOld->attrWhite ); + continue; + } ((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy; assert( pNet->pDriver->pCopy != NULL ); } @@ -412,13 +503,16 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) Ntl_ObjForEachFanout( pObj, pNet, k ) Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k ); if ( Ntl_ObjIsLatch(pObj) ) + { ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId; + ((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock->pCopy; + } if ( Ntl_ObjIsNode(pObj) ) ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew->pMemSops, pObj->pSop ); } pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL; - pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL; - pModelNew->vRequireds = pModelOld->vRequireds? Vec_IntDup( pModelOld->vRequireds ) : NULL; + pModelNew->vTimeInputs = pModelOld->vTimeInputs? Vec_IntDup( pModelOld->vTimeInputs ) : NULL; + pModelNew->vTimeOutputs = pModelOld->vTimeOutputs? Vec_IntDup( pModelOld->vTimeOutputs ) : NULL; return pModelNew; } @@ -435,10 +529,10 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) ***********************************************************************/ void Ntl_ModelFree( Ntl_Mod_t * p ) { - assert( Ntl_ManCheckNetsAreNotMarked(p) ); - if ( p->vRequireds ) Vec_IntFree( p->vRequireds ); - if ( p->vArrivals ) Vec_IntFree( p->vArrivals ); - if ( p->vDelays ) Vec_IntFree( p->vDelays ); + assert( Ntl_ModelCheckNetsAreNotMarked(p) ); + if ( p->vTimeOutputs ) Vec_IntFree( p->vTimeOutputs ); + if ( p->vTimeInputs ) Vec_IntFree( p->vTimeInputs ); + if ( p->vDelays ) Vec_IntFree( p->vDelays ); Vec_PtrFree( p->vObjs ); Vec_PtrFree( p->vPis ); Vec_PtrFree( p->vPos ); @@ -446,6 +540,45 @@ void Ntl_ModelFree( Ntl_Mod_t * p ) free( p ); } +/**Function************************************************************* + + Synopsis [Create model equal to the latch with the given init value.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init ) +{ + char Name[100]; + Ntl_Mod_t * pModel; + Ntl_Obj_t * pObj; + Ntl_Net_t * pNetLi, * pNetLo; + // create model + sprintf( Name, "%s%d", "latch", Init ); + pModel = Ntl_ModelAlloc( pMan, Name ); + pModel->attrWhite = 1; + pModel->attrBox = 1; + pModel->attrComb = 0; + pModel->attrKeep = 0; + // create primary input + pObj = Ntl_ModelCreatePi( pModel ); + pNetLi = Ntl_ModelFindOrCreateNet( pModel, "li" ); + Ntl_ModelSetNetDriver( pObj, pNetLi ); + // create latch + pObj = Ntl_ModelCreateLatch( pModel ); + pObj->LatchId.regInit = Init; + pObj->pFanio[0] = pNetLi; + // create primary output + pNetLo = Ntl_ModelFindOrCreateNet( pModel, "lo" ); + Ntl_ModelSetNetDriver( pObj, pNetLo ); + pObj = Ntl_ModelCreatePo( pModel, pNetLo ); + return pModel; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index a291f8a0..ebfb2a80 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -38,8 +38,8 @@ struct Ioa_ReadMod_t_ Vec_Ptr_t * vNames; // .names lines Vec_Ptr_t * vSubckts; // .subckt lines Vec_Ptr_t * vDelays; // .delay lines - Vec_Ptr_t * vArrivals; // .input_arrival lines - Vec_Ptr_t * vRequireds; // .output_required lines + Vec_Ptr_t * vTimeInputs; // .input_arrival/required lines + Vec_Ptr_t * vTimeOutputs; // .output_required/arrival lines int fBlackBox; // indicates blackbox model // the resulting network Ntl_Mod_t * pNtk; @@ -249,14 +249,14 @@ static Ioa_ReadMod_t * Ioa_ReadModAlloc() Ioa_ReadMod_t * p; p = ALLOC( Ioa_ReadMod_t, 1 ); memset( p, 0, sizeof(Ioa_ReadMod_t) ); - p->vInputs = Vec_PtrAlloc( 512 ); - p->vOutputs = Vec_PtrAlloc( 512 ); - p->vLatches = Vec_PtrAlloc( 512 ); - p->vNames = Vec_PtrAlloc( 512 ); - p->vSubckts = Vec_PtrAlloc( 512 ); - p->vDelays = Vec_PtrAlloc( 512 ); - p->vArrivals = Vec_PtrAlloc( 512 ); - p->vRequireds = Vec_PtrAlloc( 512 ); + p->vInputs = Vec_PtrAlloc( 8 ); + p->vOutputs = Vec_PtrAlloc( 8 ); + p->vLatches = Vec_PtrAlloc( 8 ); + p->vNames = Vec_PtrAlloc( 8 ); + p->vSubckts = Vec_PtrAlloc( 8 ); + p->vDelays = Vec_PtrAlloc( 8 ); + p->vTimeInputs = Vec_PtrAlloc( 8 ); + p->vTimeOutputs = Vec_PtrAlloc( 8 ); return p; } @@ -279,8 +279,8 @@ static void Ioa_ReadModFree( Ioa_ReadMod_t * p ) Vec_PtrFree( p->vNames ); Vec_PtrFree( p->vSubckts ); Vec_PtrFree( p->vDelays ); - Vec_PtrFree( p->vArrivals ); - Vec_PtrFree( p->vRequireds ); + Vec_PtrFree( p->vTimeInputs ); + Vec_PtrFree( p->vTimeOutputs ); free( p ); } @@ -509,10 +509,12 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p ) Vec_PtrPush( p->pLatest->vSubckts, pCur ); else if ( !strncmp(pCur, "delay", 5) ) Vec_PtrPush( p->pLatest->vDelays, pCur ); - else if ( !strncmp(pCur, "input_arrival", 13) ) - Vec_PtrPush( p->pLatest->vArrivals, pCur ); - else if ( !strncmp(pCur, "output_required", 15) ) - Vec_PtrPush( p->pLatest->vRequireds, pCur ); + else if ( !strncmp(pCur, "input_arrival", 13) || + !strncmp(pCur, "input_required", 14) ) + Vec_PtrPush( p->pLatest->vTimeInputs, pCur ); + else if ( !strncmp(pCur, "output_required", 14) || + !strncmp(pCur, "output_arrival", 13) ) + Vec_PtrPush( p->pLatest->vTimeOutputs, pCur ); else if ( !strncmp(pCur, "blackbox", 8) ) p->pLatest->fBlackBox = 1; else if ( !strncmp(pCur, "model", 5) ) @@ -522,7 +524,12 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p ) p->pLatest->pMan = p; } else if ( !strncmp(pCur, "attrib", 6) ) - p->pLatest->pAttrib = pCur; + { + if ( p->pLatest->pAttrib != NULL ) + fprintf( stdout, "Line %d: Skipping second .attrib line for this model.\n", Ioa_ReadGetLine(p, pCur) ); + else + p->pLatest->pAttrib = pCur; + } else if ( !strncmp(pCur, "end", 3) ) { if ( p->pLatest ) @@ -537,15 +544,6 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p ) else if ( !strncmp(pCur, "no_merge", 8) ) { } - else if ( !strncmp(pCur, "attribute", 9) ) - { - } - else if ( !strncmp(pCur, "input_required", 14) ) - { - } - else if ( !strncmp(pCur, "output_arrival", 14) ) - { - } else { pCur--; @@ -593,10 +591,10 @@ static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p ) Vec_PtrForEachEntry( pMod->vDelays, pLine, k ) if ( !Ioa_ReadParseLineDelay( pMod, pLine ) ) return 0; - Vec_PtrForEachEntry( pMod->vArrivals, pLine, k ) + Vec_PtrForEachEntry( pMod->vTimeInputs, pLine, k ) if ( !Ioa_ReadParseLineTimes( pMod, pLine, 0 ) ) return 0; - Vec_PtrForEachEntry( pMod->vRequireds, pLine, k ) + Vec_PtrForEachEntry( pMod->vTimeOutputs, pLine, k ) if ( !Ioa_ReadParseLineTimes( pMod, pLine, 1 ) ) return 0; } @@ -643,6 +641,8 @@ static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p ) return NULL; // update the design name pMod = Vec_PtrEntry( p->vModels, 0 ); + if ( Ntl_ModelLatchNum(pMod->pNtk) > 0 ) + Ntl_ModelTransformLatches( pMod->pNtk ); p->pDesign->pName = Ntl_ManStoreName( p->pDesign, pMod->pNtk->pName ); // return the network pDesign = p->pDesign; @@ -674,6 +674,11 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine ) return 0; } p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) ); + if ( p->pNtk == NULL ) + { + sprintf( p->pMan->sError, "Line %d: Model %s already exists.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); + return 0; + } return 1; } @@ -692,23 +697,33 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine ) { Vec_Ptr_t * vTokens = p->pMan->vTokens; char * pToken; + int i; Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); pToken = Vec_PtrEntry( vTokens, 0 ); assert( !strncmp(pToken, "attrib", 6) ); -/* - if ( Vec_PtrSize(vTokens) != 2 ) - { - sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .attrib line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) ); - return 0; - } - if ( strcmp( Vec_PtrEntry(vTokens, 1), "keep" ) == 0 ) - p->pNtk->fKeep = 1; - else + Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 ) { - sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), p->pNtk->pName ); - return 0; + pToken = Vec_PtrEntry( vTokens, i ); + if ( strcmp( pToken, "white" ) == 0 ) + p->pNtk->attrWhite = 1; + else if ( strcmp( pToken, "black" ) == 0 ) + p->pNtk->attrWhite = 0; + else if ( strcmp( pToken, "box" ) == 0 ) + p->pNtk->attrBox = 1; + else if ( strcmp( pToken, "white" ) == 0 ) + p->pNtk->attrWhite = 1; + else if ( strcmp( pToken, "comb" ) == 0 ) + p->pNtk->attrComb = 1; + else if ( strcmp( pToken, "seq" ) == 0 ) + p->pNtk->attrComb = 0; + else if ( strcmp( pToken, "keep" ) == 0 ) + p->pNtk->attrKeep = 1; + else + { + sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), pToken, p->pNtk->pName ); + return 0; + } } -*/ return 1; } @@ -792,7 +807,6 @@ static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine ) Ntl_Net_t * pNetLi, * pNetLo; Ntl_Obj_t * pObj; char * pToken, * pNameLi, * pNameLo; - int Init, Class; Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); pToken = Vec_PtrEntry(vTokens,0); assert( !strcmp(pToken, "latch") ); @@ -815,31 +829,47 @@ static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine ) } // get initial value if ( Vec_PtrSize(vTokens) > 3 ) - Init = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) ); + pObj->LatchId.regInit = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) ); else - Init = 2; - if ( Init < 0 || Init > 2 ) + pObj->LatchId.regInit = 2; + if ( pObj->LatchId.regInit < 0 || pObj->LatchId.regInit > 2 ) { sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) ); return 0; } // get the register class if ( Vec_PtrSize(vTokens) == 6 ) - Class = atoi( Vec_PtrEntry(vTokens,3) ); - else - Class = 0; - if ( Class < 0 || Class > (1<<24) ) { - sprintf( p->pMan->sError, "Line %d: Class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,4) ); + pToken = Vec_PtrEntry(vTokens,3); + if ( strcmp( pToken, "fe" ) == 0 ) + pObj->LatchId.regType = 1; + else if ( strcmp( pToken, "re" ) == 0 ) + pObj->LatchId.regType = 2; + else if ( strcmp( pToken, "ah" ) == 0 ) + pObj->LatchId.regType = 3; + else if ( strcmp( pToken, "al" ) == 0 ) + pObj->LatchId.regType = 4; + else if ( strcmp( pToken, "as" ) == 0 ) + pObj->LatchId.regType = 5; + else if ( pToken[0] >= '0' && pToken[0] <= '9' ) + pObj->LatchId.regClass = atoi(pToken); + else + { + sprintf( p->pMan->sError, "Line %d: Type/class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), pToken ); + return 0; + } + } + if ( pObj->LatchId.regClass < 0 || pObj->LatchId.regClass > (1<<24) ) + { + sprintf( p->pMan->sError, "Line %d: Class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) ); return 0; } - pObj->LatchId = (Class << 2) | Init; // get the clock if ( Vec_PtrSize(vTokens) == 5 || Vec_PtrSize(vTokens) == 6 ) { pToken = Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-2); pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pToken ); -// pObj->pFanio[1] = pNetLi; + pObj->pClock = pNetLi; } return 1; } @@ -984,7 +1014,7 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine ) RetValue1 = 0; Number1 = -1; if ( Vec_PtrSize(vTokens) > 2 ) { - RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number1 ); + RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, 0, 0, Vec_PtrEntry(vTokens, 1), &Number1 ); if ( RetValue1 == 0 ) { sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); @@ -994,7 +1024,7 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine ) RetValue2 = 0; Number2 = -1; if ( Vec_PtrSize(vTokens) > 3 ) { - RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 2), &Number2 ); + RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, 0, 0, Vec_PtrEntry(vTokens, 2), &Number2 ); if ( RetValue2 == 0 ) { sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 2) ); @@ -1037,19 +1067,19 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine ) static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput ) { Vec_Ptr_t * vTokens = p->pMan->vTokens; - int RetValue, Number; + int RetValue, Number = -1; char * pToken, * pTokenNum; float Delay; assert( sizeof(float) == sizeof(int) ); Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); pToken = Vec_PtrEntry(vTokens,0); if ( fOutput ) - assert( !strcmp(pToken, "output_required") ); + assert( !strncmp(pToken, "output_", 7) ); else - assert( !strcmp(pToken, "input_arrival") ); - if ( Vec_PtrSize(vTokens) != 3 ) + assert( !strncmp(pToken, "input_", 6) ); + if ( Vec_PtrSize(vTokens) != 2 && Vec_PtrSize(vTokens) != 3 ) { - sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (3).", Ioa_ReadGetLine(p->pMan, pToken) ); + sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (2 or 3).", Ioa_ReadGetLine(p->pMan, pToken) ); return 0; } // find the delay number @@ -1068,31 +1098,37 @@ static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput // find the PI/PO numbers if ( fOutput ) { - RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number ); - if ( RetValue == 0 ) + if ( Vec_PtrSize(vTokens) == 3 ) { - sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); - return 0; + RetValue = Ntl_ModelFindPioNumber( p->pNtk, 0, 1, Vec_PtrEntry(vTokens, 1), &Number ); + if ( RetValue == 0 ) + { + sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); + return 0; + } } // store the values - if ( p->pNtk->vRequireds == NULL ) - p->pNtk->vRequireds = Vec_IntAlloc( 100 ); - Vec_IntPush( p->pNtk->vRequireds, Number ); - Vec_IntPush( p->pNtk->vRequireds, Aig_Float2Int(Delay) ); + if ( p->pNtk->vTimeOutputs == NULL ) + p->pNtk->vTimeOutputs = Vec_IntAlloc( 100 ); + Vec_IntPush( p->pNtk->vTimeOutputs, Number ); + Vec_IntPush( p->pNtk->vTimeOutputs, Aig_Float2Int(Delay) ); } else { - RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number ); - if ( RetValue == 0 ) + if ( Vec_PtrSize(vTokens) == 3 ) { - sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); - return 0; + RetValue = Ntl_ModelFindPioNumber( p->pNtk, 1, 0, Vec_PtrEntry(vTokens, 1), &Number ); + if ( RetValue == 0 ) + { + sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); + return 0; + } } // store the values - if ( p->pNtk->vArrivals == NULL ) - p->pNtk->vArrivals = Vec_IntAlloc( 100 ); - Vec_IntPush( p->pNtk->vArrivals, Number ); - Vec_IntPush( p->pNtk->vArrivals, Aig_Float2Int(Delay) ); + if ( p->pNtk->vTimeInputs == NULL ) + p->pNtk->vTimeInputs = Vec_IntAlloc( 100 ); + Vec_IntPush( p->pNtk->vTimeInputs, Number ); + Vec_IntPush( p->pNtk->vTimeInputs, Aig_Float2Int(Delay) ); } return 1; } diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c index 8309e1b3..991d701a 100644 --- a/src/aig/ntl/ntlSweep.c +++ b/src/aig/ntl/ntlSweep.c @@ -79,7 +79,7 @@ void Ntl_ManSweepMark( Ntl_Man_t * p ) Ntl_ManSweepMark_rec( p, pObj ); // start from the persistant boxes Ntl_ModelForEachBox( pRoot, pObj, i ) - if ( pObj->pImplem->fKeep ) + if ( pObj->pImplem->attrKeep ) Ntl_ManSweepMark_rec( p, pObj ); } diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c index c3acc0b1..fe58e2f8 100644 --- a/src/aig/ntl/ntlTable.c +++ b/src/aig/ntl/ntlTable.c @@ -189,7 +189,7 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ) SeeAlso [] ***********************************************************************/ -int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber ) +int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber ) { Ntl_Net_t * pNet; Ntl_Obj_t * pObj; @@ -198,6 +198,30 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber ) pNet = Ntl_ModelFindNet( p, pName ); if ( pNet == NULL ) return 0; + if ( fPiOnly ) + { + Ntl_ModelForEachPi( p, pObj, i ) + { + if ( Ntl_ObjFanout0(pObj) == pNet ) + { + *pNumber = i; + return -1; + } + } + return 0; + } + if ( fPoOnly ) + { + Ntl_ModelForEachPo( p, pObj, i ) + { + if ( Ntl_ObjFanin0(pObj) == pNet ) + { + *pNumber = i; + return 1; + } + } + return 0; + } Ntl_ModelForEachPo( p, pObj, i ) { if ( Ntl_ObjFanin0(pObj) == pNet ) @@ -281,6 +305,97 @@ int Ntl_ModelCountNets( Ntl_Mod_t * p ) return Counter; } + + + +/**Function************************************************************* + + Synopsis [Resizes the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManModelTableResize( Ntl_Man_t * p ) +{ + Ntl_Mod_t ** pModTableNew, ** ppSpot, * pEntry, * pEntry2; + int nModTableSizeNew, Counter, e, clk; +clk = clock(); + // get the new table size + nModTableSizeNew = Aig_PrimeCudd( 3 * p->nModTableSize ); + // allocate a new array + pModTableNew = ALLOC( Ntl_Mod_t *, nModTableSizeNew ); + memset( pModTableNew, 0, sizeof(Ntl_Mod_t *) * nModTableSizeNew ); + // rehash entries + Counter = 0; + for ( e = 0; e < p->nModTableSize; e++ ) + for ( pEntry = p->pModTable[e], pEntry2 = pEntry? pEntry->pNext : NULL; + pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNext : NULL ) + { + ppSpot = pModTableNew + Ntl_HashString( pEntry->pName, nModTableSizeNew ); + pEntry->pNext = *ppSpot; + *ppSpot = pEntry; + Counter++; + } + assert( Counter == p->nModEntries ); +// printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew ); +// PRT( "Time", clock() - clk ); + // replace the table and the parameters + free( p->pModTable ); + p->pModTable = pModTableNew; + p->nModTableSize = nModTableSizeNew; +} + +/**Function************************************************************* + + Synopsis [Finds or creates the net.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel ) +{ + Ntl_Mod_t * pEnt; + unsigned Key = Ntl_HashString( pModel->pName, p->nModTableSize ); + for ( pEnt = p->pModTable[Key]; pEnt; pEnt = pEnt->pNext ) + if ( !strcmp( pEnt->pName, pModel->pName ) ) + return 0; + pModel->pNext = p->pModTable[Key]; + p->pModTable[Key] = pModel; + if ( ++p->nModEntries > 2 * p->nModTableSize ) + Ntl_ManModelTableResize( p ); + Vec_PtrPush( p->vModels, pModel ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Finds or creates the net.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ) +{ + Ntl_Mod_t * pEnt; + unsigned Key = Ntl_HashString( pName, p->nModTableSize ); + for ( pEnt = p->pModTable[Key]; pEnt; pEnt = pEnt->pNext ) + if ( !strcmp( pEnt->pName, pName ) ) + return pEnt; + return NULL; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlTime.c b/src/aig/ntl/ntlTime.c index 94691ab8..c23a4e24 100644 --- a/src/aig/ntl/ntlTime.c +++ b/src/aig/ntl/ntlTime.c @@ -88,13 +88,27 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p ) // start the timing manager pMan = Tim_ManStart( Aig_ManPiNum(p->pAig), Aig_ManPoNum(p->pAig) ); // unpack the data in the arrival times - if ( pRoot->vArrivals ) - Vec_IntForEachEntry( pRoot->vArrivals, Entry, i ) - Tim_ManInitCiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vArrivals,++i)) ); + if ( pRoot->vTimeInputs ) + { + Vec_IntForEachEntry( pRoot->vTimeInputs, Entry, i ) + { + if ( Entry == -1 ) + Tim_ManSetCiArrivalAll( pMan, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeInputs,++i)) ); + else + Tim_ManInitCiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeInputs,++i)) ); + } + } // unpack the data in the required times - if ( pRoot->vRequireds ) - Vec_IntForEachEntry( pRoot->vRequireds, Entry, i ) - Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vRequireds,++i)) ); + if ( pRoot->vTimeOutputs ) + { + Vec_IntForEachEntry( pRoot->vTimeOutputs, Entry, i ) + { + if ( Entry == -1 ) + Tim_ManSetCoRequiredAll( pMan, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeOutputs,++i)) ); + else + Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeOutputs,++i)) ); + } + } // derive timing tables vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vModels) ); Ntl_ManForEachModel( p, pModel, i ) @@ -106,7 +120,7 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p ) Tim_ManSetDelayTables( pMan, vDelayTables ); // set up the boxes iBox = 0; - curPi = Ntl_ModelCiNum(pRoot); + curPi = p->iLastCi; Ntl_ManForEachBox( p, pObj, i ) { Tim_ManCreateBoxFirst( pMan, Vec_IntEntry(p->vBox1Cos, iBox), Ntl_ObjFaninNum(pObj), curPi, Ntl_ObjFanoutNum(pObj), pObj->pImplem->pDelayTable ); diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c index 6849889d..c9ef2dc4 100644 --- a/src/aig/ntl/ntlUtil.c +++ b/src/aig/ntl/ntlUtil.c @@ -236,26 +236,6 @@ void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p ) pNet->fMark = 0; } -/**Function************************************************************* - - Synopsis [Unmarks the CI/CO nets.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel ) -{ - Ntl_Net_t * pNet; - int i; - Ntl_ModelForEachNet( pModel, pNet, i ) - assert( pNet->fMark == 0 ); - return 1; -} - /**Function************************************************************* Synopsis [Convert initial values of registers to be zero.] @@ -274,7 +254,7 @@ void Ntl_ManSetZeroInitValues( Ntl_Man_t * p ) int i; pRoot = Ntl_ManRootModel(p); Ntl_ModelForEachLatch( pRoot, pObj, i ) - pObj->LatchId &= ~3; + pObj->LatchId.regInit = 0; } /**Function************************************************************* @@ -296,7 +276,7 @@ void Ntl_ManAddInverters( Ntl_Obj_t * pObj ) Ntl_Net_t * pNetLo, * pNetLi, * pNetLoInv, * pNetLiInv; Ntl_Obj_t * pNode; int nLength, RetValue; - assert( (pObj->LatchId & 3) == 1 ); + assert( Ntl_ObjIsInit1( pObj ) ); // get the nets pNetLi = Ntl_ObjFanin0(pObj); pNetLo = Ntl_ObjFanout0(pObj); @@ -362,11 +342,132 @@ void Ntl_ManTransformInitValues( Ntl_Man_t * p ) pRoot = Ntl_ManRootModel(p); Ntl_ModelForEachLatch( pRoot, pObj, i ) { - if ( (pObj->LatchId & 3) == 1 ) + if ( Ntl_ObjIsInit1( pObj ) ) Ntl_ManAddInverters( pObj ); - pObj->LatchId &= ~3; + pObj->LatchId.regInit = 0; } +} + +/**Function************************************************************* + + Synopsis [Counts the number of CIs in the model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCombLeafNum( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pObj; + int i, Counter = 0; + Ntl_ModelForEachCombLeaf( p, pObj, i ) + Counter += Ntl_ObjFanoutNum( pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of COs in the model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCombRootNum( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pObj; + int i, Counter = 0; + Ntl_ModelForEachCombRoot( p, pObj, i ) + Counter += Ntl_ObjFaninNum( pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of CIs in the model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelSeqLeafNum( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pObj; + int i, Counter = 0; + Ntl_ModelForEachSeqLeaf( p, pObj, i ) + Counter += Ntl_ObjFanoutNum( pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of COs in the model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelSeqRootNum( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pObj; + int i, Counter = 0; + Ntl_ModelForEachSeqRoot( p, pObj, i ) + Counter += Ntl_ObjFaninNum( pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Unmarks the CI/CO nets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel ) +{ + Ntl_Net_t * pNet; + int i; + Ntl_ModelForEachNet( pModel, pNet, i ) + assert( pNet->fMark == 0 ); + return 1; +} + +/**Function************************************************************* + Synopsis [Unmarks the CI/CO nets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ModelClearNets( Ntl_Mod_t * pModel ) +{ + Ntl_Net_t * pNet; + int i; + Ntl_ModelForEachNet( pModel, pNet, i ) + { + pNet->nVisits = 0; + pNet->pCopy = NULL; + } } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c index 51d41c26..f93e3fa1 100644 --- a/src/aig/ntl/ntlWriteBlif.c +++ b/src/aig/ntl/ntlWriteBlif.c @@ -40,15 +40,22 @@ SeeAlso [] ***********************************************************************/ -void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) +void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel, int fMain ) { Ntl_Obj_t * pObj; Ntl_Net_t * pNet; float Delay; - int i, k, fClockAdded = 0; + int i, k; fprintf( pFile, ".model %s\n", pModel->pName ); - if ( pModel->fKeep ) - fprintf( pFile, ".attrib keep\n" ); + if ( pModel->attrWhite || pModel->attrBox || pModel->attrComb || pModel->attrKeep ) + { + fprintf( pFile, ".attrib" ); + fprintf( pFile, " %s", pModel->attrWhite? "white": "black" ); + fprintf( pFile, " %s", pModel->attrBox? "box" : "logic" ); + fprintf( pFile, " %s", pModel->attrComb? "comb" : "seq" ); +// fprintf( pFile, " %s", pModel->attrKeep? "keep" : "sweep" ); + fprintf( pFile, "\n" ); + } fprintf( pFile, ".inputs" ); Ntl_ModelForEachPi( pModel, pObj, i ) fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName ); @@ -63,19 +70,25 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) for ( i = 0; i < Vec_IntSize(pModel->vDelays); i += 3 ) { fprintf( pFile, ".delay" ); - fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vDelays,i)))->pName ); - fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vDelays,i+1)))->pName ); + if ( Vec_IntEntry(pModel->vDelays,i) != -1 ) + fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vDelays,i)))->pName ); + if ( Vec_IntEntry(pModel->vDelays,i+1) != -1 ) + fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vDelays,i+1)))->pName ); fprintf( pFile, " %.3f", Aig_Int2Float(Vec_IntEntry(pModel->vDelays,i+2)) ); fprintf( pFile, "\n" ); } } - if ( pModel->vArrivals ) + if ( pModel->vTimeInputs ) { - for ( i = 0; i < Vec_IntSize(pModel->vArrivals); i += 2 ) + for ( i = 0; i < Vec_IntSize(pModel->vTimeInputs); i += 2 ) { - fprintf( pFile, ".input_arrival" ); - fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vArrivals,i)))->pName ); - Delay = Aig_Int2Float(Vec_IntEntry(pModel->vArrivals,i+1)); + if ( fMain ) + fprintf( pFile, ".input_arrival" ); + else + fprintf( pFile, ".input_required" ); + if ( Vec_IntEntry(pModel->vTimeInputs,i) != -1 ) + fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vTimeInputs,i)))->pName ); + Delay = Aig_Int2Float(Vec_IntEntry(pModel->vTimeInputs,i+1)); if ( Delay == -TIM_ETERNITY ) fprintf( pFile, " -inf" ); else if ( Delay == TIM_ETERNITY ) @@ -85,13 +98,17 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) fprintf( pFile, "\n" ); } } - if ( pModel->vRequireds ) + if ( pModel->vTimeOutputs ) { - for ( i = 0; i < Vec_IntSize(pModel->vRequireds); i += 2 ) + for ( i = 0; i < Vec_IntSize(pModel->vTimeOutputs); i += 2 ) { - fprintf( pFile, ".output_required" ); - fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vRequireds,i)))->pName ); - Delay = Aig_Int2Float(Vec_IntEntry(pModel->vRequireds,i+1)); + if ( fMain ) + fprintf( pFile, ".output_required" ); + else + fprintf( pFile, ".output_arrival" ); + if ( Vec_IntEntry(pModel->vTimeOutputs,i) != -1 ) + fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vTimeOutputs,i)))->pName ); + Delay = Aig_Int2Float(Vec_IntEntry(pModel->vTimeOutputs,i+1)); if ( Delay == -TIM_ETERNITY ) fprintf( pFile, " -inf" ); else if ( Delay == TIM_ETERNITY ) @@ -117,13 +134,27 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) fprintf( pFile, ".latch" ); fprintf( pFile, " %s", Ntl_ObjFanin0(pObj)->pName ); fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName ); - if ( pObj->LatchId >> 2 ) - fprintf( pFile, " %d", pObj->LatchId >> 2 ); - if ( Ntl_ObjFanin(pObj, 1) != NULL ) - fprintf( pFile, " %s", Ntl_ObjFanin(pObj, 1)->pName ); - else if ( pObj->LatchId >> 2 ) - fprintf( pFile, " clock99" ), fClockAdded = 1; - fprintf( pFile, " %d", pObj->LatchId & 3 ); + assert( pObj->LatchId.regType == 0 || pObj->LatchId.regClass == 0 ); + if ( pObj->LatchId.regType ) + { + if ( pObj->LatchId.regType == 1 ) + fprintf( pFile, " fe" ); + else if ( pObj->LatchId.regType == 2 ) + fprintf( pFile, " re" ); + else if ( pObj->LatchId.regType == 3 ) + fprintf( pFile, " ah" ); + else if ( pObj->LatchId.regType == 4 ) + fprintf( pFile, " al" ); + else if ( pObj->LatchId.regType == 5 ) + fprintf( pFile, " as" ); + else + assert( 0 ); + } + else if ( pObj->LatchId.regClass ) + fprintf( pFile, " %d", pObj->LatchId.regClass ); + if ( pObj->pClock ) + fprintf( pFile, " %s", pObj->pClock->pName ); + fprintf( pFile, " %d", pObj->LatchId.regInit ); fprintf( pFile, "\n" ); } else if ( Ntl_ObjIsBox(pObj) ) @@ -136,8 +167,6 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel ) fprintf( pFile, "\n" ); } } - if ( fClockAdded ) - fprintf( pFile, ".names clock99\n 0\n" ); fprintf( pFile, ".end\n\n" ); } @@ -167,7 +196,7 @@ void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName ) fprintf( pFile, "# Benchmark \"%s\" written by ABC-8 on %s\n", p->pName, Ioa_TimeStamp() ); // write the models Ntl_ManForEachModel( p, pModel, i ) - Ioa_WriteBlifModel( pFile, pModel ); + Ioa_WriteBlifModel( pFile, pModel, i==0 ); // close the file fclose( pFile ); } -- cgit v1.2.3