From c645bac3663c265470024b44ed91b0afdbe59b88 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 10 Apr 2008 08:01:00 -0700 Subject: Version abc80410 --- src/aig/aig/aig.h | 5 +- src/aig/aig/aigDfs.c | 6 +- src/aig/aig/aigDup.c | 70 +++++++++- src/aig/aig/aigMan.c | 1 + src/aig/aig/aigObj.c | 2 + src/aig/aig/aigRepr.c | 2 + src/aig/aig/aigScl.c | 96 ++++++++++++-- src/aig/fra/fraSec.c | 10 +- src/aig/ioa/ioaWriteAig.c | 6 +- src/aig/ntl/module.make | 2 + src/aig/ntl/ntl.h | 34 ++++- src/aig/ntl/ntlCheck.c | 10 +- src/aig/ntl/ntlCore.c | 10 +- src/aig/ntl/ntlEc.c | 317 ++++++++++++++++++++++++++++++++++++++++++++++ src/aig/ntl/ntlExtract.c | 219 +++++++++++++++++++++++++++++++- src/aig/ntl/ntlFraig.c | 164 +++++++++++++++++++++++- src/aig/ntl/ntlInsert.c | 90 ++++++------- src/aig/ntl/ntlMan.c | 137 ++++++++++++++++++-- src/aig/ntl/ntlObj.c | 29 ++++- src/aig/ntl/ntlReadBlif.c | 6 +- src/aig/ntl/ntlSweep.c | 165 ++++++++++++++++++++++++ src/aig/ntl/ntlTable.c | 20 +++ src/aig/ntl/ntlUtil.c | 208 +++++++++++++++++++++++++++++- src/aig/nwk/nwkMan.c | 2 +- 24 files changed, 1505 insertions(+), 106 deletions(-) create mode 100644 src/aig/ntl/ntlEc.c create mode 100644 src/aig/ntl/ntlSweep.c (limited to 'src/aig') diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 2231b4e7..88d7aa50 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -140,6 +140,7 @@ struct Aig_Man_t_ void * pManCuts; Vec_Ptr_t * vMapped; Vec_Int_t * vFlopNums; + Vec_Int_t * vFlopReprs; void * pSeqModel; Aig_Man_t * pManExdc; Vec_Ptr_t * vOnehots; @@ -314,7 +315,7 @@ static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; } static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pReprs? p->pReprs[pObj->Id] : NULL; } -static inline int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)pObj->pNext; } +static inline int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)(long)pObj->pNext; } static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin ) { if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; @@ -461,6 +462,7 @@ extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t extern void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes ); extern int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ); /*=== aigDup.c ==========================================================*/ +extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p ); @@ -560,6 +562,7 @@ extern int Aig_ManSeqCleanup( Aig_Man_t * p ); extern int Aig_ManCountMergeRegs( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ); extern void Aig_ManComputeSccs( Aig_Man_t * p ); +extern Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose ); /*=== aigShow.c ========================================================*/ extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ); /*=== aigTable.c ========================================================*/ diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 917558c6..9f7d286d 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -449,10 +449,10 @@ int Aig_ManChoiceLevel( Aig_Man_t * p ) LevelMax = Aig_ObjLevel(pObj); } Aig_ManCleanPioNumbers( p ); - Aig_ManForEachNode( p, pObj, i ) - assert( Aig_ObjLevel(pObj) > 0 ); +// Aig_ManForEachNode( p, pObj, i ) +// assert( Aig_ObjLevel(pObj) > 0 ); return LevelMax; -} +} //#endif diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index fb0a8ba8..b435aade 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -29,6 +29,72 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager.] + + Description [Orders nodes as follows: PIs, ANDs, POs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManDup( Aig_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjNew; + int i; + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + pNew->nRegs = p->nRegs; + pNew->nAsserts = p->nAsserts; + if ( p->vFlopNums ) + pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig; + Aig_ManForEachPi( p, pObj, i ) + { + pObjNew = Aig_ObjCreatePi( pNew ); + pObjNew->pHaig = pObj->pHaig; + pObjNew->Level = pObj->Level; + pObj->pData = pObjNew; + } + // duplicate internal nodes + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjIsBuf(pObj) ) + { + pObjNew = Aig_ObjChild0Copy(pObj); + Aig_Regular(pObjNew)->pHaig = pObj->pHaig; + pObj->pData = pObjNew; + } + else if ( Aig_ObjIsNode(pObj) ) + { + pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_Regular(pObjNew)->pHaig = pObj->pHaig; + pObj->pData = pObjNew; + } + // add the POs + Aig_ManForEachPo( p, pObj, i ) + { + pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + pObjNew->pHaig = pObj->pHaig; + pObj->pData = pObjNew; + } + assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); + // duplicate the timing manager + if ( p->pManTime ) + pNew->pManTime = Tim_ManDup( p->pManTime, 0 ); + // check the resulting network + if ( !Aig_ManCheck(pNew) ) + printf( "Aig_ManDup(): The check has failed.\n" ); + return pNew; +} + /**Function************************************************************* Synopsis [Duplicates the AIG manager.] @@ -543,7 +609,7 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p ) } // check the new manager if ( !Aig_ManCheck(pNew) ) - printf( "Aig_ManDupReprentative: Check has failed.\n" ); + printf( "Aig_ManDupRepres: Check has failed.\n" ); return pNew; } @@ -616,7 +682,7 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p ) } // check the new manager if ( !Aig_ManCheck(pNew) ) - printf( "Aig_ManDupReprentative: Check has failed.\n" ); + printf( "Aig_ManDupRepresDfs: Check has failed.\n" ); return pNew; } diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 58f0d797..4c4b7aad 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -206,6 +206,7 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->vLevelR ) Vec_IntFree( p->vLevelR ); if ( p->vLevels ) Vec_VecFree( p->vLevels ); if ( p->vFlopNums) Vec_IntFree( p->vFlopNums ); + if ( p->vFlopReprs)Vec_IntFree( p->vFlopReprs ); if ( p->pManExdc ) Aig_ManStop( p->pManExdc ); if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots ); FREE( p->pData ); diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index d02e3228..a66eb2b8 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -258,6 +258,8 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew Aig_ObjDeref( pFaninOld ); // update the fanin pObj->pFanin0 = pFaninNew; + pObj->Level = Aig_ObjLevelNew( pObj ); + pObj->fPhase = Aig_ObjPhaseReal(pObj->pFanin0); // increment ref and add fanout if ( p->pFanData ) Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj ); diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c index 4eefa283..94a1c844 100644 --- a/src/aig/aig/aigRepr.c +++ b/src/aig/aig/aigRepr.c @@ -278,6 +278,8 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered ) Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Aig_ManForEachPi( p, pObj, i ) pObj->pData = Aig_ObjCreatePi(pNew); +// Aig_ManForEachPi( p, pObj, i ) +// pObj->pData = Aig_ObjGetRepr( p, pObj ); // map the internal nodes if ( fOrdered ) { diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c index 92bfcd28..c32f2f4f 100644 --- a/src/aig/aig/aigScl.c +++ b/src/aig/aig/aigScl.c @@ -44,25 +44,52 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ) { Aig_Man_t * pNew; Aig_Obj_t * pObj, * pObjMapped; - int i; + int i, nTruePis; // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); pNew->pSpec = Aig_UtilStrsav( p->pSpec ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; + assert( p->vFlopNums == NULL || Vec_IntSize(p->vFlopNums) == p->nRegs ); if ( p->vFlopNums ) pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); + if ( p->vFlopReprs ) + pNew->vFlopReprs = Vec_IntDup( p->vFlopReprs ); // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Aig_ManForEachPi( p, pObj, i ) pObj->pData = Aig_ObjCreatePi(pNew); // implement the mapping + nTruePis = Aig_ManPiNum(p)-Aig_ManRegNum(p); + if ( p->vFlopReprs ) + { + Aig_ManForEachLoSeq( p, pObj, i ) + pObj->pNext = (Aig_Obj_t *)(long)Vec_IntEntry( p->vFlopNums, i-nTruePis ); + } Aig_ManForEachPi( p, pObj, i ) { pObjMapped = Vec_PtrEntry( vMap, i ); pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) ); + if ( pNew->vFlopReprs && i >= nTruePis && pObj != pObjMapped ) + { + Vec_IntPush( pNew->vFlopReprs, Aig_ObjPioNum(pObj) ); + if ( Aig_ObjIsConst1( Aig_Regular(pObjMapped) ) ) + Vec_IntPush( pNew->vFlopReprs, -1 ); + else + { + assert( !Aig_IsComplement(pObjMapped) ); + assert( Aig_ObjIsPi(pObjMapped) ); + assert( Aig_ObjPioNum(pObj) != Aig_ObjPioNum(pObjMapped) ); + Vec_IntPush( pNew->vFlopReprs, Aig_ObjPioNum(pObjMapped) ); + } + } + } + if ( p->vFlopReprs ) + { + Aig_ManForEachLoSeq( p, pObj, i ) + pObj->pNext = NULL; } // duplicate internal nodes Aig_ManForEachObj( p, pObj, i ) @@ -158,16 +185,15 @@ int Aig_ManSeqCleanup( Aig_Man_t * p ) if ( p->vFlopNums ) { int nTruePos = Aig_ManPoNum(p)-Aig_ManRegNum(p); - // remember numbers of flops in the flops - Aig_ManForEachLiSeq( p, pObj, i ) - pObj->pNext = (Aig_Obj_t *)(long)Vec_IntEntry( p->vFlopNums, i - nTruePos ); - // reset the flop numbers - Vec_PtrForEachEntryStart( vNodes, pObj, i, nTruePos ) - Vec_IntWriteEntry( p->vFlopNums, i - nTruePos, (int)(long)pObj->pNext ); - Vec_IntShrink( p->vFlopNums, Vec_PtrSize(vNodes) - nTruePos ); - // clean the next pointer - Aig_ManForEachLiSeq( p, pObj, i ) - pObj->pNext = NULL; + int iNum, k = 0; + Aig_ManForEachPo( p, pObj, i ) + if ( i >= nTruePos && Aig_ObjIsTravIdCurrent(p, pObj) ) + { + iNum = Vec_IntEntry( p->vFlopNums, i - nTruePos ); + Vec_IntWriteEntry( p->vFlopNums, k++, iNum ); + } + assert( k == Vec_PtrSize(vNodes) - nTruePos ); + Vec_IntShrink( p->vFlopNums, k ); } // collect new CIs/COs vCis = Vec_PtrAlloc( Aig_ManPiNum(p) ); @@ -505,6 +531,54 @@ void Aig_ManComputeSccs( Aig_Man_t * p ) Vec_VecFree( (Vec_Vec_t *)vSupports ); } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose ) +{ + Aig_Man_t * pAigInit, * pAigNew; + Aig_Obj_t * pFlop1, * pFlop2; + int i, Entry1, Entry2, nTruePis; + // store the original AIG + assert( pAig->vFlopNums == NULL ); + pAigInit = pAig; + pAig = Aig_ManDup( pAig ); + // create storage for latch numbers + pAig->vFlopNums = Vec_IntStartNatural( pAig->nRegs ); + pAig->vFlopReprs = Vec_IntAlloc( 100 ); + Aig_ManSeqCleanup( pAig ); + if ( fLatchConst && pAig->nRegs ) + pAig = Aig_ManConstReduce( pAig, fVerbose ); + if ( fLatchEqual && pAig->nRegs ) + pAig = Aig_ManReduceLaches( pAig, fVerbose ); + // translate pairs into reprs + nTruePis = Aig_ManPiNum(pAigInit)-Aig_ManRegNum(pAigInit); + Aig_ManReprStart( pAigInit, Aig_ManObjNumMax(pAigInit) ); + Vec_IntForEachEntry( pAig->vFlopReprs, Entry1, i ) + { + Entry2 = Vec_IntEntry( pAig->vFlopReprs, ++i ); + pFlop1 = Aig_ManPi( pAigInit, nTruePis + Entry1 ); + pFlop2 = (Entry2 == -1)? Aig_ManConst1(pAigInit) : Aig_ManPi( pAigInit, nTruePis + Entry2 ); + assert( pFlop1 != pFlop2 ); + if ( pFlop1->Id > pFlop2->Id ) + pAigInit->pReprs[pFlop1->Id] = pFlop2; + else + pAigInit->pReprs[pFlop2->Id] = pFlop1; + } + Aig_ManStop( pAig ); +// Aig_ManSeqCleanup( pAigInit ); + pAigNew = Aig_ManDupRepr( pAigInit, 0 ); + Aig_ManSeqCleanup( pAigNew ); + return pAigNew; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 389c3e2f..012c7651 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -47,13 +47,18 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging Aig_Man_t * pNew, * pTemp; int nFrames, RetValue, nIter, clk, clkTotal = clock(); int fLatchCorr = 0; + + // try the miter before solving + RetValue = Fra_FraigMiterStatus( p ); + if ( RetValue == 0 || RetValue == 1 ) + goto finish; + // prepare parameters memset( pPars, 0, sizeof(Fra_Ssw_t) ); pPars->fLatchCorr = fLatchCorr; pPars->fVerbose = fVeryVerbose; - pNew = Aig_ManDupOrdered( p ); -// pNew = Aig_ManDupDfs( p ); + pNew = Aig_ManDup( p ); if ( fVerbose ) { printf( "Original miter: Latches = %5d. Nodes = %6d.\n", @@ -208,6 +213,7 @@ PRT( "Time", clock() - clkTotal ); // get the miter status RetValue = Fra_FraigMiterStatus( pNew ); +finish: // report the miter if ( RetValue == 1 ) { diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c index 166dca4b..aa731463 100644 --- a/src/aig/ioa/ioaWriteAig.c +++ b/src/aig/ioa/ioaWriteAig.c @@ -145,7 +145,7 @@ static void Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num ) { pObj->iD SeeAlso [] ***********************************************************************/ -int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ) +int Ioa_WriteAigerEncode( unsigned char * pBuffer, int Pos, unsigned x ) { unsigned char ch; while (x & ~0x7f) @@ -332,8 +332,8 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); assert( uLit0 < uLit1 ); - Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) ); - Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) ); + Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 ); + Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 ); if ( Pos > nBufferSize - 10 ) { printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" ); diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make index d3f2cfdd..7f885a90 100644 --- a/src/aig/ntl/module.make +++ b/src/aig/ntl/module.make @@ -1,5 +1,6 @@ SRC += src/aig/ntl/ntlCheck.c \ src/aig/ntl/ntlCore.c \ + src/aig/ntl/ntlEc.c \ src/aig/ntl/ntlExtract.c \ src/aig/ntl/ntlFraig.c \ src/aig/ntl/ntlInsert.c \ @@ -7,6 +8,7 @@ SRC += src/aig/ntl/ntlCheck.c \ src/aig/ntl/ntlMap.c \ src/aig/ntl/ntlObj.c \ src/aig/ntl/ntlReadBlif.c \ + src/aig/ntl/ntlSweep.c \ src/aig/ntl/ntlTable.c \ src/aig/ntl/ntlTime.c \ src/aig/ntl/ntlUtil.c \ diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index 2e109f05..6b6424c0 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -54,8 +54,9 @@ typedef enum { NTL_OBJ_PO, // 2: primary output NTL_OBJ_LATCH, // 3: latch node NTL_OBJ_NODE, // 4: logic node - NTL_OBJ_BOX, // 5: white box or black box - NTL_OBJ_VOID // 6: unused object + NTL_OBJ_LUT1, // 5: inverter/buffer + NTL_OBJ_BOX, // 6: white box or black box + NTL_OBJ_VOID // 7: unused object } Ntl_Type_t; struct Ntl_Man_t_ @@ -122,7 +123,7 @@ struct Ntl_Net_t_ Ntl_Obj_t * pDriver; // driver of the net char nVisits; // the number of times the net is visited char fMark; // temporary mark - char fCompl; // complemented attribue + char fCompl; // complemented attribute char pName[0]; // the name of this net }; @@ -148,6 +149,7 @@ static inline Ntl_Mod_t * Ntl_ManRootModel( Ntl_Man_t * p ) { return Vec_P static inline int Ntl_ModelPiNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PI]; } static inline int Ntl_ModelPoNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PO]; } static inline int Ntl_ModelNodeNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_NODE]; } +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]; } @@ -228,27 +230,35 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int /*=== ntlCore.c ==========================================================*/ extern int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig ); extern int Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig ); +/*=== ntlEc.c ==========================================================*/ +extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 ); +extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ); /*=== ntlExtract.c ==========================================================*/ extern Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ); -extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ); +extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq ); +extern Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p ); +extern Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 ); extern char * Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover ); /*=== ntlInsert.c ==========================================================*/ -extern int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ); -extern int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ); -extern int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ); +extern Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ); +extern Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ); +extern Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ); /*=== ntlCheck.c ==========================================================*/ extern int Ntl_ManCheck( Ntl_Man_t * pMan ); extern int Ntl_ModelCheck( Ntl_Mod_t * pModel ); extern void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel ); /*=== ntlMan.c ============================================================*/ extern Ntl_Man_t * Ntl_ManAlloc( char * pFileName ); +extern void Ntl_ManCleanup( Ntl_Man_t * p ); extern Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * p ); extern Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * p ); extern void Ntl_ManFree( Ntl_Man_t * p ); +extern int Ntl_ManIsComb( Ntl_Man_t * p ); extern Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName ); extern void Ntl_ManPrintStats( Ntl_Man_t * p ); extern Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p ); extern Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName ); +extern Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ); extern Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ); extern void Ntl_ModelFree( Ntl_Mod_t * p ); /*=== ntlMap.c ============================================================*/ @@ -263,15 +273,19 @@ extern Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel ); extern Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins ); extern Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts ); extern Ntl_Obj_t * Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld ); +extern Ntl_Obj_t * Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName ); extern char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName ); extern char * Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop ); extern char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName ); +/*=== ntlSweep.c ==========================================================*/ +extern Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose ); /*=== ntlTable.c ==========================================================*/ extern Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName ); extern Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ); extern int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber ); extern int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ); extern void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet ); +extern int Ntl_ModelCountNets( Ntl_Mod_t * p ); /*=== ntlTime.c ==========================================================*/ extern Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p ); /*=== ntlReadBlif.c ==========================================================*/ @@ -279,9 +293,15 @@ extern Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck ); /*=== ntlWriteBlif.c ==========================================================*/ extern void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName ); /*=== ntlUtil.c ==========================================================*/ +extern int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot ); +extern int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p ); extern int Ntl_ManTransformCoDrivers( Ntl_Man_t * p ); +extern int Ntl_ManReconnectCoDrivers( Ntl_Man_t * p ); extern Vec_Ptr_t * Ntl_ManCollectCiNames( Ntl_Man_t * p ); extern Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p ); +extern void Ntl_ManMarkCiCoNets( Ntl_Man_t * p ); +extern void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p ); +extern int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel ); #ifdef __cplusplus } diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c index 5973e967..9fd4af9f 100644 --- a/src/aig/ntl/ntlCheck.c +++ b/src/aig/ntl/ntlCheck.c @@ -31,7 +31,7 @@ /**Function************************************************************* - Synopsis [] + Synopsis [Checks one model.] Description [] @@ -49,12 +49,12 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel ) { if ( pNet->pName == NULL ) { - printf( "Net %d does not have a name\n", i ); + printf( "Net in bin %d does not have a name\n", i ); fStatus = 0; } if ( pNet->pDriver == NULL ) { - printf( "Net %d (%s) does not have a driver\n", i, pNet->pName ); + printf( "Net %s does not have a driver\n", pNet->pName ); fStatus = 0; } } @@ -78,7 +78,7 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel ) /**Function************************************************************* - Synopsis [] + Synopsis [Checks the netlist.] Description [] @@ -131,7 +131,7 @@ int Ntl_ManCheck( Ntl_Man_t * pMan ) /**Function************************************************************* - Synopsis [Reads the verilog file.] + Synopsis [Fixed problems with non-driven nets in the model.] Description [] diff --git a/src/aig/ntl/ntlCore.c b/src/aig/ntl/ntlCore.c index fb4bb620..a5c40444 100644 --- a/src/aig/ntl/ntlCore.c +++ b/src/aig/ntl/ntlCore.c @@ -69,10 +69,13 @@ Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdate ***********************************************************************/ int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig ) { + Ntl_Man_t * pNew; Vec_Ptr_t * vMapping; int RetValue; vMapping = Ntl_MappingFromAig( pAig ); - RetValue = Ntl_ManInsert( p, vMapping, pAig ); + pNew = Ntl_ManInsertMapping( p, vMapping, pAig ); + RetValue = (pNew != NULL); + Ntl_ManFree( pNew ); Vec_PtrFree( vMapping ); return RetValue; } @@ -90,10 +93,13 @@ int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig ) ***********************************************************************/ int Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig ) { + Ntl_Man_t * pNew; Vec_Ptr_t * vMapping; int RetValue; vMapping = Ntl_MappingIf( p, pAig ); - RetValue = Ntl_ManInsert( p, vMapping, pAig ); + pNew = Ntl_ManInsertMapping( p, vMapping, pAig ); + RetValue = (pNew != NULL); + Ntl_ManFree( pNew ); Vec_PtrFree( vMapping ); return RetValue; } diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c new file mode 100644 index 00000000..6b7b1a41 --- /dev/null +++ b/src/aig/ntl/ntlEc.c @@ -0,0 +1,317 @@ +/**CFile**************************************************************** + + FileName [ntlEc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [Equivalence checking procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ntlEc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ntl.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adds PIs to both models, so that they have the same PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 ) + { + pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName ); + if ( pNet == NULL ) + Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName ); + } + if ( !fSeq ) + { + Ntl_ModelForEachLatch( p1, pObj, i ) + { + pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName ); + if ( pNet == NULL ) + Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName ); + } + Ntl_ModelForEachLatch( p2, pObj, i ) + { + pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName ); + if ( pNet == NULL ) + Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName ); + } + } +} + +/**Function************************************************************* + + Synopsis [Creates arrays of combinational inputs in the same order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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) ); + // order the CIs + Vec_PtrClear( pMan1->vCis ); + Vec_PtrClear( pMan2->vCis ); + Ntl_ModelForEachPi( p1, pObj, i ) + { + pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" ); + return; + } + Vec_PtrPush( pMan1->vCis, pObj ); + Vec_PtrPush( pMan2->vCis, pNet->pDriver ); + } + if ( !fSeq ) + { + Ntl_ModelForEachLatch( p1, pObj, i ) + { + pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" ); + return; + } + Vec_PtrPush( pMan1->vCis, pObj ); + Vec_PtrPush( pMan2->vCis, pNet->pDriver ); + } + } +} + +/**Function************************************************************* + + Synopsis [Creates arrays of combinational outputs in the same order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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; + // order the COs + Vec_PtrClear( pMan1->vCos ); + Vec_PtrClear( pMan2->vCos ); + Ntl_ModelForEachPo( p1, pObj, i ) + { + pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", + Ntl_ObjFanin0(pObj)->pName ); + continue; + } + Vec_PtrPush( pMan1->vCos, pObj ); + Vec_PtrPush( pMan2->vCos, pNet->pCopy ); + } + if ( !fSeq ) + { + Ntl_ModelForEachLatch( p2, pObj, i ) + Ntl_ObjFanin0(pObj)->pCopy = pObj; + Ntl_ModelForEachLatch( p1, pObj, i ) + { + pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName ); + if ( pNet == NULL ) + { + printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", + Ntl_ObjFanin0(pObj)->pName ); + continue; + } + Vec_PtrPush( pMan1->vCos, pObj ); + Vec_PtrPush( pMan2->vCos, pNet->pCopy ); + } + } +} + +/**Function************************************************************* + + Synopsis [Prepares AIGs for combinational equivalence checking.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 ) +{ + Ntl_Man_t * pMan1, * pMan2; + Ntl_Mod_t * pModel1, * pModel2; + *ppMan1 = NULL; + *ppMan2 = NULL; + // read the netlists + pMan1 = Ioa_ReadBlif( pFileName1, 1 ); + pMan2 = Ioa_ReadBlif( pFileName2, 1 ); + if ( !pMan1 || !pMan2 ) + { + if ( pMan1 ) Ntl_ManFree( pMan1 ); + if ( pMan2 ) Ntl_ManFree( pMan2 ); + printf( "Ntl_ManPrepareCec(): Reading designs from file has failed.\n" ); + return; + } + // make sure they are compatible + pModel1 = Ntl_ManRootModel( pMan1 ); + pModel2 = Ntl_ManRootModel( pMan2 ); + if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) ) + { + printf( "Warning: The number of inputs in the designs is different (%d and %d).\n", + Ntl_ModelCiNum(pModel1), Ntl_ModelCiNum(pModel2) ); + } + if ( Ntl_ModelCoNum(pModel1) != Ntl_ModelCoNum(pModel2) ) + { + printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", + Ntl_ModelCoNum(pModel1), Ntl_ModelCoNum(pModel2) ); + } + // normalize inputs/outputs + Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 ); + Ntl_ManDeriveCommonCis( pMan1, pMan2, 0 ); + Ntl_ManDeriveCommonCos( pMan1, pMan2, 0 ); + if ( Vec_PtrSize(pMan1->vCos) == 0 ) + { + printf( "Ntl_ManPrepareCec(): There is no identically-named primary outputs to compare.\n" ); + if ( pMan1 ) Ntl_ManFree( pMan1 ); + if ( pMan2 ) Ntl_ManFree( pMan2 ); + return; + } + // derive AIGs + *ppMan1 = Ntl_ManCollapseForCec( pMan1 ); + *ppMan2 = Ntl_ManCollapseForCec( pMan2 ); + // cleanup + Ntl_ManFree( pMan1 ); + Ntl_ManFree( pMan2 ); +} + +/**Function************************************************************* + + Synopsis [Prepares AIGs for sequential equivalence checking.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ) +{ + Aig_Man_t * pAig; + Ntl_Man_t * pMan1, * pMan2; + Ntl_Mod_t * pModel1, * pModel2; + // read the netlists + pMan1 = Ioa_ReadBlif( pFileName1, 1 ); + pMan2 = Ioa_ReadBlif( pFileName2, 1 ); + if ( !pMan1 || !pMan2 ) + { + if ( pMan1 ) Ntl_ManFree( pMan1 ); + if ( pMan2 ) Ntl_ManFree( pMan2 ); + printf( "Ntl_ManPrepareSec(): Reading designs from file has failed.\n" ); + return NULL; + } + // make sure they are compatible + pModel1 = Ntl_ManRootModel( pMan1 ); + pModel2 = Ntl_ManRootModel( pMan2 ); + if ( Ntl_ModelLatchNum(pModel1) == 0 || Ntl_ModelLatchNum(pModel2) == 0 ) + { + if ( pMan1 ) Ntl_ManFree( pMan1 ); + if ( pMan2 ) Ntl_ManFree( pMan2 ); + printf( "Ntl_ManPrepareSec(): The designs have no latches. Used combinational command \"*cec\".\n" ); + return NULL; + } + if ( Ntl_ModelPiNum(pModel1) != Ntl_ModelPiNum(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) ) + { + printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", + Ntl_ModelPoNum(pModel1), Ntl_ModelPoNum(pModel2) ); + } + // normalize inputs/outputs + Ntl_ManCreateMissingInputs( pModel1, pModel2, 1 ); + Ntl_ManDeriveCommonCis( pMan1, pMan2, 1 ); + Ntl_ManDeriveCommonCos( pMan1, pMan2, 1 ); + if ( Vec_PtrSize(pMan1->vCos) == 0 ) + { + printf( "Ntl_ManPrepareSec(): There is no identically-named primary outputs to compare.\n" ); + if ( pMan1 ) Ntl_ManFree( pMan1 ); + if ( pMan2 ) Ntl_ManFree( pMan2 ); + return NULL; + } + // derive AIGs + pAig = Ntl_ManCollapseForSec( pMan1, pMan2 ); + // cleanup + pMan1->pAig = pMan2->pAig = NULL; + Ntl_ManFree( pMan1 ); + Ntl_ManFree( pMan2 ); + return pAig; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index 848f113a..9c3666ab 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -467,6 +467,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) Ntl_Obj_t * pObj; Ntl_Net_t * pNet; int i, nUselessObjects; + Ntl_ManCleanup( p ); assert( Vec_PtrSize(p->vCis) == 0 ); assert( Vec_PtrSize(p->vCos) == 0 ); assert( Vec_PtrSize(p->vNodes) == 0 ); @@ -540,7 +541,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) Aig_ObjCreatePo( p->pAig, pNet->pCopy ); } // report the number of dangling objects - nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes); + nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelLut1Num(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes); if ( nUselessObjects ) printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects ); // cleanup the AIG @@ -658,7 +659,7 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ) +Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq ) { Aig_Man_t * pAig; Ntl_Mod_t * pRoot; @@ -694,6 +695,8 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ) 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" ); @@ -721,6 +724,60 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ) 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 ); + } + // cleanup the AIG + Aig_ManCleanup( p->pAig ); + pAig = p->pAig; p->pAig = NULL; + return pAig; +} + +/**Function************************************************************* + + Synopsis [Derives AIG for CEC.] + + Description [Uses CIs/COs collected in the internal arrays.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p ) +{ + Aig_Man_t * pAig; + Ntl_Obj_t * pObj; + Ntl_Net_t * pNet; + int i; + // 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 @@ -729,6 +786,164 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ) return pAig; } +/**Function************************************************************* + + Synopsis [Performs DFS.] + + 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 * pAig; + Aig_Obj_t * pMiter; + Ntl_Mod_t * pRoot1, * pRoot2; + 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) ); + + ///////////////////////////////////////////////////// + // 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 + pRoot1 = Ntl_ManRootModel(p1); + 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 ); + } + + ///////////////////////////////////////////////////// + // 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 + pRoot2 = Ntl_ManRootModel(p2); + 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 ); + pAig->nRegs = Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 ); + Aig_ManCleanup( pAig ); + return pAig; +} + + /**Function************************************************************* Synopsis [Increments reference counter of the net.] diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 7153f081..8a172e6c 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "ntl.h" +#include "fra.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -30,10 +31,10 @@ /**Function************************************************************* - Synopsis [Returns AIG with WB after fraiging.] + Synopsis [Transfers equivalence class info from pAigCol to pAig.] - Description [pAig points to the nodes of pNew derived using it. - pNew points to the nodes of pAigCol derived using it.] + Description [pAig points to the nodes of netlist (pNew) derived using it. + pNew points to the nodes of the collapsed AIG (pAigCol) derived using it.] SideEffects [] @@ -59,6 +60,9 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_ } // create mapping from the collapsed manager into the original manager + // (each node in the collapsed manager may have more than one equivalent node + // in the original manager; this procedure finds the first node in the original + // manager that is equivalent to the given node in the collapsed manager) pMapBack = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAigCol) ); memset( pMapBack, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAigCol) ); Aig_ManForEachObj( pAig, pObj, i ) @@ -115,16 +119,15 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC assert( pAig->pReprs == NULL ); // create a new netlist whose nodes are in 1-to-1 relationship with AIG - pNew = Ntl_ManDup( p ); - if ( !Ntl_ManInsertAig( pNew, pAig ) ) + pNew = Ntl_ManInsertAig( p, pAig ); + if ( pNew == NULL ) { - Ntl_ManFree( pNew ); printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" ); return NULL; } // collapse the AIG - pAigCol = Ntl_ManCollapse( pNew ); + pAigCol = Ntl_ManCollapse( pNew, 0 ); // perform fraiging for the given design if ( nPartSize == 0 ) nPartSize = Aig_ManPoNum(pAigCol); @@ -148,6 +151,153 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC return pTemp; } +/**Function************************************************************* + + Synopsis [Performs sequential cleanup.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ntl_ManScl( Ntl_Man_t * p, Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose ) +{ + Ntl_Man_t * pNew; + Aig_Man_t * pAigCol, * pTemp; + assert( pAig->pReprs == NULL ); + + // create a new netlist whose nodes are in 1-to-1 relationship with AIG + pNew = Ntl_ManInsertAig( p, pAig ); + if ( pNew == NULL ) + { + printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" ); + return NULL; + } + + // collapse the AIG + pAigCol = Ntl_ManCollapse( pNew, 1 ); + // perform fraiging for the given design + pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p)); + pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose ); + Aig_ManStop( pTemp ); + + // transfer equivalence classes to the original AIG + pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol ); + pAig->nReprsAlloc = Aig_ManObjNumMax(pAig); + // cleanup + Aig_ManStop( pAigCol ); + Ntl_ManFree( pNew ); + + // derive the new AIG + pTemp = Aig_ManDupRepresDfs( pAig ); + // duplicate the timing manager + if ( pAig->pManTime ) + pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 ); + // reset levels + Aig_ManChoiceLevel( pTemp ); + return pTemp; +} + +/**Function************************************************************* + + Synopsis [Returns AIG with WB after fraiging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, Aig_Man_t * pAig, int nConfMax, int fVerbose ) +{ + Ntl_Man_t * pNew; + Aig_Man_t * pAigCol, * pTemp; + assert( pAig->pReprs == NULL ); + + // create a new netlist whose nodes are in 1-to-1 relationship with AIG + pNew = Ntl_ManInsertAig( p, pAig ); + if ( pNew == NULL ) + { + printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" ); + return NULL; + } + + // collapse the AIG + pAigCol = Ntl_ManCollapse( pNew, 1 ); + // perform fraiging for the given design + pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p)); + pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL ); + Aig_ManStop( pTemp ); + + // transfer equivalence classes to the original AIG + pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol ); + pAig->nReprsAlloc = Aig_ManObjNumMax(pAig); + // cleanup + Aig_ManStop( pAigCol ); + Ntl_ManFree( pNew ); + + // derive the new AIG + pTemp = Aig_ManDupRepresDfs( pAig ); + // duplicate the timing manager + if ( pAig->pManTime ) + pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 ); + // reset levels + Aig_ManChoiceLevel( pTemp ); + return pTemp; +} + +/**Function************************************************************* + + Synopsis [Returns AIG with WB after fraiging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Aig_Man_t * pAig, Fra_Ssw_t * pPars ) +{ + Ntl_Man_t * pNew; + Aig_Man_t * pAigCol, * pTemp; + assert( pAig->pReprs == NULL ); + + // create a new netlist whose nodes are in 1-to-1 relationship with AIG + pNew = Ntl_ManInsertAig( p, pAig ); + if ( pNew == NULL ) + { + printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" ); + return NULL; + } + + // collapse the AIG + pAigCol = Ntl_ManCollapse( pNew, 1 ); + // perform fraiging for the given design + pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p)); + pTemp = Fra_FraigInduction( pAigCol, pPars ); + Aig_ManStop( pTemp ); + + // transfer equivalence classes to the original AIG + pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol ); + pAig->nReprsAlloc = Aig_ManObjNumMax(pAig); + // cleanup + Aig_ManStop( pAigCol ); + Ntl_ManFree( pNew ); + + // derive the new AIG + pTemp = Aig_ManDupRepresDfs( pAig ); + // duplicate the timing manager + if ( pAig->pManTime ) + pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 ); + // reset levels + Aig_ManChoiceLevel( pTemp ); + return pTemp; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c index 10b83660..77fb606a 100644 --- a/src/aig/ntl/ntlInsert.c +++ b/src/aig/ntl/ntlInsert.c @@ -40,7 +40,7 @@ SeeAlso [] ***********************************************************************/ -int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ) +Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ) { char Buffer[100]; Vec_Ptr_t * vCopies; @@ -50,16 +50,14 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ) Ntl_Net_t * pNet, * pNetCo; Ntl_Lut_t * pLut; int i, k, nDigits; + assert( Vec_PtrSize(p->vCis) == Aig_ManPiNum(pAig) ); + assert( Vec_PtrSize(p->vCos) == Aig_ManPoNum(pAig) ); + p = Ntl_ManStartFrom( p ); + pRoot = Ntl_ManRootModel( p ); + assert( Ntl_ModelNodeNum(pRoot) == 0 ); // map the AIG back onto the design Ntl_ManForEachCiNet( p, pNet, i ) pNet->pCopy = Aig_ManPi( pAig, i ); - Ntl_ManForEachCoNet( p, pNet, i ) - pNet->pCopy = Aig_ObjChild0( Aig_ManPo( pAig, i ) ); - // remove old nodes - pRoot = Ntl_ManRootModel( p ); - Ntl_ModelForEachNode( pRoot, pNode, i ) - Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL ); - pRoot->nObjs[NTL_OBJ_NODE] = 0; // start mapping of AIG nodes into their copies vCopies = Vec_PtrStart( Aig_ManObjNumMax(pAig) ); Ntl_ManForEachCiNet( p, pNet, i ) @@ -101,19 +99,19 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ) Vec_IntFree( vCover ); // mark CIs and outputs of the registers Ntl_ManForEachCiNet( p, pNetCo, i ) - pNetCo->nVisits = 101; // using "101" is harmless because nVisits can only be 0, 1 or 2 + pNetCo->fMark = 1; // update the CO pointers Ntl_ManForEachCoNet( p, pNetCo, i ) { - if ( pNetCo->nVisits == 101 ) + if ( pNetCo->fMark ) continue; - pNetCo->nVisits = 101; + pNetCo->fMark = 1; pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pCopy)->Id ); pNode = Ntl_ModelCreateNode( pRoot, 1 ); pNode->pSop = Aig_IsComplement(pNetCo->pCopy)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" ); Ntl_ObjSetFanin( pNode, pNet, 0 ); // update the CO driver net - pNetCo->pDriver = NULL; + assert( pNetCo->pDriver == NULL ); if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) ) { printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" ); @@ -121,7 +119,11 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ) } } Vec_PtrFree( vCopies ); - return 1; + // clean CI/CO marks + Ntl_ManUnmarkCiCoNets( p ); + if ( !Ntl_ManCheck( p ) ) + printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName ); + return p; } /**Function************************************************************* @@ -135,7 +137,7 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ) SeeAlso [] ***********************************************************************/ -int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ) +Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ) { char Buffer[100]; Ntl_Mod_t * pRoot; @@ -145,17 +147,13 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ) int i, nDigits, Counter; assert( Vec_PtrSize(p->vCis) == Aig_ManPiNum(pAig) ); assert( Vec_PtrSize(p->vCos) == Aig_ManPoNum(pAig) ); + p = Ntl_ManStartFrom( p ); + pRoot = Ntl_ManRootModel( p ); + assert( Ntl_ModelNodeNum(pRoot) == 0 ); // set the correspondence between the PI/PO nodes Aig_ManCleanData( pAig ); Ntl_ManForEachCiNet( p, pNet, i ) Aig_ManPi( pAig, i )->pData = pNet; -// Ntl_ManForEachCoNet( p, pNet, i ) -// Nwk_ManCo( pNtk, i )->pCopy = pNet; - // remove old nodes - pRoot = Ntl_ManRootModel( p ); - Ntl_ModelForEachNode( pRoot, pNode, i ) - Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL ); - pRoot->nObjs[NTL_OBJ_NODE] = 0; // create constant node if needed if ( Aig_ManConst1(pAig)->nRefs > 0 ) { @@ -213,13 +211,13 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ) } // mark CIs and outputs of the registers Ntl_ManForEachCiNet( p, pNetCo, i ) - pNetCo->nVisits = 101; + pNetCo->fMark = 1; // update the CO pointers Ntl_ManForEachCoNet( p, pNetCo, i ) { - if ( pNetCo->nVisits == 101 ) + if ( pNetCo->fMark ) continue; - pNetCo->nVisits = 101; + pNetCo->fMark = 1; // get the corresponding PO and its driver pObj = Aig_ManPo( pAig, i ); pFanin = Aig_ObjFanin0( pObj ); @@ -229,14 +227,18 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ) pNode->pSop = Aig_ObjFaninC0(pObj)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" ); Ntl_ObjSetFanin( pNode, pNet, 0 ); // update the CO driver net - pNetCo->pDriver = NULL; + assert( pNetCo->pDriver == NULL ); if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) ) { - printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" ); + printf( "Ntl_ManInsertAig(): Internal error: PO net has more than one fanin.\n" ); return 0; } } - return 1; + // clean CI/CO marks + Ntl_ManUnmarkCiCoNets( p ); + if ( !Ntl_ManCheck( p ) ) + printf( "Ntl_ManInsertAig: The check has failed for design %s.\n", p->pName ); + return p; } @@ -251,7 +253,7 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig ) SeeAlso [] ***********************************************************************/ -int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) +Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) { char Buffer[100]; Vec_Ptr_t * vObjs; @@ -265,16 +267,12 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) unsigned * pTruth; assert( Vec_PtrSize(p->vCis) == Nwk_ManCiNum(pNtk) ); assert( Vec_PtrSize(p->vCos) == Nwk_ManCoNum(pNtk) ); + p = Ntl_ManStartFrom( p ); + pRoot = Ntl_ManRootModel( p ); + assert( Ntl_ModelNodeNum(pRoot) == 0 ); // set the correspondence between the PI/PO nodes Ntl_ManForEachCiNet( p, pNet, i ) Nwk_ManCi( pNtk, i )->pCopy = pNet; -// Ntl_ManForEachCoNet( p, pNet, i ) -// Nwk_ManCo( pNtk, i )->pCopy = pNet; - // remove old nodes - pRoot = Ntl_ManRootModel( p ); - Ntl_ModelForEachNode( pRoot, pNode, i ) - Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL ); - pRoot->nObjs[NTL_OBJ_NODE] = 0; // create a new node for each LUT vTruth = Vec_IntAlloc( 1 << 16 ); vCover = Vec_IntAlloc( 1 << 16 ); @@ -298,7 +296,7 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) pNet = pFanin->pCopy; if ( pNet == NULL ) { - printf( "Ntl_ManInsert(): Internal error: Net not found.\n" ); + printf( "Ntl_ManInsertNtk(): Internal error: Net not found.\n" ); return 0; } Ntl_ObjSetFanin( pNode, pNet, k ); @@ -307,13 +305,13 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) sprintf( Buffer, "lut%0*d", nDigits, i ); if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) ) { - printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" ); + printf( "Ntl_ManInsertNtk(): Internal error: Intermediate net name is not unique.\n" ); return 0; } pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer ); if ( !Ntl_ModelSetNetDriver( pNode, pNet ) ) { - printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" ); + printf( "Ntl_ManInsertNtk(): Internal error: Net has more than one fanin.\n" ); return 0; } pObj->pCopy = pNet; @@ -323,13 +321,13 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) Vec_IntFree( vTruth ); // mark CIs and outputs of the registers Ntl_ManForEachCiNet( p, pNetCo, i ) - pNetCo->nVisits = 101; + pNetCo->fMark = 1; // update the CO pointers Ntl_ManForEachCoNet( p, pNetCo, i ) { - if ( pNetCo->nVisits == 101 ) + if ( pNetCo->fMark ) continue; - pNetCo->nVisits = 101; + pNetCo->fMark = 1; // get the corresponding PO and its driver pObj = Nwk_ManCo( pNtk, i ); pFanin = Nwk_ObjFanin0( pObj ); @@ -339,14 +337,18 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pCopy)*/? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" ); Ntl_ObjSetFanin( pNode, pNet, 0 ); // update the CO driver net - pNetCo->pDriver = NULL; + assert( pNetCo->pDriver == NULL ); if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) ) { - printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" ); + printf( "Ntl_ManInsertNtk(): Internal error: PO net has more than one fanin.\n" ); return 0; } } - return 1; + // clean CI/CO marks + Ntl_ManUnmarkCiCoNets( p ); + if ( !Ntl_ManCheck( p ) ) + printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName ); + return p; } diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c index 83219df7..82131091 100644 --- a/src/aig/ntl/ntlMan.c +++ b/src/aig/ntl/ntlMan.c @@ -61,7 +61,36 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName ) /**Function************************************************************* - Synopsis [Duplicates the interface of the top level model.] + Synopsis [Cleanups extended representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManCleanup( Ntl_Man_t * p ) +{ + Vec_PtrClear( p->vCis ); + Vec_PtrClear( p->vCos ); + Vec_PtrClear( p->vNodes ); + Vec_IntClear( p->vBox1Cos ); + if ( p->pAig ) + { + Aig_ManStop( p->pAig ); + p->pAig = NULL; + } + if ( p->pManTime ) + { + Tim_ManStop( p->pManTime ); + p->pManTime = NULL; + } +} + +/**Function************************************************************* + + Synopsis [Duplicates the design without the nodes of the root model.] Description [] @@ -72,12 +101,36 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName ) ***********************************************************************/ Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld ) { - return NULL; + Ntl_Man_t * pNew; + Ntl_Mod_t * pModel; + Ntl_Obj_t * pBox; + Ntl_Net_t * pNet; + int i, k; + pNew = Ntl_ManAlloc( pOld->pSpec ); + Vec_PtrForEachEntry( pOld->vModels, pModel, i ) + if ( i == 0 ) + { + Ntl_ManMarkCiCoNets( pOld ); + pModel->pCopy = Ntl_ModelStartFrom( pNew, pModel ); + Ntl_ManUnmarkCiCoNets( pOld ); + } + else + pModel->pCopy = Ntl_ModelDup( pNew, pModel ); + Vec_PtrForEachEntry( pOld->vModels, pModel, i ) + Ntl_ModelForEachBox( pModel, pBox, k ) + ((Ntl_Obj_t *)pBox->pCopy)->pImplem = pBox->pImplem->pCopy; + Ntl_ManForEachCiNet( pOld, pNet, i ) + Vec_PtrPush( pNew->vCis, pNet->pCopy ); + Ntl_ManForEachCoNet( pOld, pNet, i ) + Vec_PtrPush( pNew->vCos, pNet->pCopy ); + if ( pOld->pManTime ) + pNew->pManTime = Tim_ManDup( pOld->pManTime, 0 ); + return pNew; } /**Function************************************************************* - Synopsis [Duplicates the interface of the top level model.] + Synopsis [Duplicates the design.] Description [] @@ -142,6 +195,22 @@ void Ntl_ManFree( Ntl_Man_t * p ) free( p ); } +/**Function************************************************************* + + Synopsis [Returns 1 if the design is combinational.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ManIsComb( Ntl_Man_t * p ) +{ + return Ntl_ModelLatchNum(Ntl_ManRootModel(p)) == 0; +} + /**Function************************************************************* Synopsis [Find the model with the given name.] @@ -178,15 +247,18 @@ void Ntl_ManPrintStats( Ntl_Man_t * p ) { Ntl_Mod_t * pRoot; pRoot = Ntl_ManRootModel( p ); - printf( "%-15s : ", p->pName ); - printf( "pi = %5d ", Ntl_ModelPiNum(pRoot) ); - printf( "po = %5d ", Ntl_ModelPoNum(pRoot) ); - printf( "lat = %5d ", Ntl_ModelLatchNum(pRoot) ); - printf( "node = %5d ", Ntl_ModelNodeNum(pRoot) ); - printf( "box = %4d ", Ntl_ModelBoxNum(pRoot) ); - printf( "mod = %3d", Vec_PtrSize(p->vModels) ); + printf( "%-15s : ", p->pName ); + printf( "pi = %5d ", Ntl_ModelPiNum(pRoot) ); + printf( "po = %5d ", Ntl_ModelPoNum(pRoot) ); + printf( "lat = %5d ", Ntl_ModelLatchNum(pRoot) ); + printf( "node = %5d ", Ntl_ModelNodeNum(pRoot) ); + printf( "inv/buf = %5d ", Ntl_ModelLut1Num(pRoot) ); + printf( "box = %4d ", Ntl_ModelBoxNum(pRoot) ); + printf( "mod = %3d ", Vec_PtrSize(p->vModels) ); + printf( "net = %d", Ntl_ModelCountNets(pRoot) ); printf( "\n" ); fflush( stdout ); + assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) ); } /**Function************************************************************* @@ -235,6 +307,50 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName ) return p; } +/**Function************************************************************* + + Synopsis [Duplicates the model without nodes but with CI/CO nets.] + + Description [The CI/CO nets of the old model should be marked before + calling this procedure.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ) +{ + Ntl_Mod_t * pModelNew; + Ntl_Net_t * pNet; + Ntl_Obj_t * pObj; + int i, k; + pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName ); + Ntl_ModelForEachNet( pModelOld, pNet, i ) + if ( pNet->fMark ) + pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName ); + else + pNet->pCopy = NULL; + Ntl_ModelForEachObj( pModelOld, pObj, i ) + { + if ( Ntl_ObjIsNode(pObj) ) + continue; + pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj ); + Ntl_ObjForEachFanin( pObj, pNet, k ) + if ( pNet->pCopy != NULL ) + Ntl_ObjSetFanin( pObj->pCopy, pNet->pCopy, k ); + Ntl_ObjForEachFanout( pObj, pNet, k ) + if ( pNet->pCopy != NULL ) + Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k ); + if ( Ntl_ObjIsLatch(pObj) ) + ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId; + } + 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; + return pModelNew; +} + /**Function************************************************************* Synopsis [Duplicates the model.] @@ -286,6 +402,7 @@ 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 ); diff --git a/src/aig/ntl/ntlObj.c b/src/aig/ntl/ntlObj.c index ad43623a..68b5cfe8 100644 --- a/src/aig/ntl/ntlObj.c +++ b/src/aig/ntl/ntlObj.c @@ -131,7 +131,10 @@ Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins ) p->Type = NTL_OBJ_NODE; p->nFanins = nFanins; p->nFanouts = 1; - pModel->nObjs[NTL_OBJ_NODE]++; + if ( nFanins == 1 ) + pModel->nObjs[NTL_OBJ_LUT1]++; + else + pModel->nObjs[NTL_OBJ_NODE]++; return p; } @@ -188,6 +191,30 @@ Ntl_Obj_t * Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld ) return pNew; } + +/**Function************************************************************* + + Synopsis [Creates the primary input with the given name.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Obj_t * Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName ) +{ + Ntl_Obj_t * pObj; + Ntl_Net_t * pNet; + pNet = Ntl_ModelFindOrCreateNet( pModel, pName ); + if ( pNet->pDriver ) + return NULL; + pObj = Ntl_ModelCreatePi( pModel ); + Ntl_ModelSetNetDriver( pObj, pNet ); + return pObj; +} + /**Function************************************************************* Synopsis [Allocates memory and copies the name into it.] diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index ce3a2051..dd74f9ba 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -109,7 +109,7 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck ) FILE * pFile; Ioa_ReadMan_t * p; Ntl_Man_t * pDesign; - int nNodes; +// int nNodes; // check that the file is available pFile = fopen( pFileName, "rb" ); @@ -166,8 +166,8 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck ) } // transform the design by removing the CO drivers - if ( (nNodes = Ntl_ManTransformCoDrivers(pDesign)) ) - printf( "The design was transformed by removing %d buf/inv CO drivers.\n", nNodes ); +// if ( (nNodes = Ntl_ManReconnectCoDrivers(pDesign)) ) +// printf( "The design was transformed by removing %d buf/inv CO drivers.\n", nNodes ); //Ioa_WriteBlif( pDesign, "_temp_.blif" ); return pDesign; } diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c new file mode 100644 index 00000000..3b9cd61f --- /dev/null +++ b/src/aig/ntl/ntlSweep.c @@ -0,0 +1,165 @@ +/**CFile**************************************************************** + + FileName [ntlSweep.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [Performs structural sweep of the netlist.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ntlSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ntl.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Detects logic that does not fanout into POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManSweepMark_rec( Ntl_Man_t * p, Ntl_Obj_t * pObj ) +{ + Ntl_Net_t * pNet; + int i; + if ( pObj->fMark ) + return; + pObj->fMark = 1; + Ntl_ObjForEachFanin( pObj, pNet, i ) + Ntl_ManSweepMark_rec( p, pNet->pDriver ); +} + +/**Function************************************************************* + + Synopsis [Detects logic that does not fanout into POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManSweepMark( Ntl_Man_t * p ) +{ + Ntl_Mod_t * pRoot; + Ntl_Obj_t * pObj; + int i; + // get the root model + pRoot = Ntl_ManRootModel( p ); + // clear net visited flags + Ntl_ModelForEachObj( pRoot, pObj, i ) + assert( pObj->fMark == 0 ); + // label the primary inputs + Ntl_ModelForEachPi( pRoot, pObj, i ) + pObj->fMark = 1; + // start from the primary outputs + Ntl_ModelForEachPo( pRoot, pObj, i ) + Ntl_ManSweepMark_rec( p, pObj ); +} + +/**Function************************************************************* + + Synopsis [Derives new netlist by sweeping current netlist with the current AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose ) +{ + int nObjsOld[NTL_OBJ_VOID]; + Ntl_Man_t * pNew; + Ntl_Mod_t * pRoot; + Ntl_Net_t * pNet; + Ntl_Obj_t * pObj; + int i, k, nNetsOld; + + // insert the AIG into the netlist + pNew = Ntl_ManInsertAig( p, pAig ); + if ( pNew == NULL ) + { + printf( "Ntl_ManSweep(): Inserting AIG has failed.\n" ); + return NULL; + } + + // remember the number of objects + pRoot = Ntl_ManRootModel( pNew ); + for ( i = 0; i < NTL_OBJ_VOID; i++ ) + nObjsOld[i] = pRoot->nObjs[i]; + nNetsOld = Ntl_ModelCountNets(pRoot); + + // mark the nets that do not fanout into POs + Ntl_ManSweepMark( pNew ); + + // remove the useless objects and their nets + Ntl_ModelForEachObj( pRoot, pObj, i ) + { + if ( pObj->fMark ) + { + pObj->fMark = 0; + continue; + } + // remove the fanout nets + Ntl_ObjForEachFanout( pObj, pNet, k ) + Ntl_ModelDeleteNet( pRoot, Ntl_ObjFanout0(pObj) ); + // remove the object + if ( Ntl_ObjIsNode(pObj) && Ntl_ObjFaninNum(pObj) == 1 ) + pRoot->nObjs[NTL_OBJ_LUT1]--; + else + pRoot->nObjs[pObj->Type]--; + Vec_PtrWriteEntry( pRoot->vObjs, pObj->Id, NULL ); + pObj->Id = NTL_OBJ_NONE; + } + + // print detailed statistics of sweeping + if ( fVerbose ) + { + printf( "Sweep:" ); + printf( " Node = %d (%4.1f %%)", + nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE], + !nObjsOld[NTL_OBJ_NODE]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE]) / nObjsOld[NTL_OBJ_NODE] ); + printf( " Buf/Inv = %d (%4.1f %%)", + nObjsOld[NTL_OBJ_LUT1] - pRoot->nObjs[NTL_OBJ_LUT1], + !nObjsOld[NTL_OBJ_LUT1]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_LUT1] - pRoot->nObjs[NTL_OBJ_LUT1]) / nObjsOld[NTL_OBJ_LUT1] ); + printf( " Lat = %d (%4.1f %%)", + nObjsOld[NTL_OBJ_LATCH] - pRoot->nObjs[NTL_OBJ_LATCH], + !nObjsOld[NTL_OBJ_LATCH]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_LATCH] - pRoot->nObjs[NTL_OBJ_LATCH]) / nObjsOld[NTL_OBJ_LATCH] ); + printf( " Box = %d (%4.1f %%)", + nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX], + !nObjsOld[NTL_OBJ_BOX]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX]) / nObjsOld[NTL_OBJ_BOX] ); + printf( "\n" ); +// printf( "Also, sweep reduced %d nets.\n", nNetsOld - Ntl_ModelCountNets(pRoot) ); + } + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c index df982481..07794492 100644 --- a/src/aig/ntl/ntlTable.c +++ b/src/aig/ntl/ntlTable.c @@ -239,6 +239,26 @@ int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ) return 1; } +/**Function************************************************************* + + Synopsis [Finds or creates the net.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCountNets( Ntl_Mod_t * p ) +{ + Ntl_Net_t * pNet; + int i, Counter = 0; + Ntl_ModelForEachNet( p, pNet, i ) + Counter++; + return Counter; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c index b13dd3a7..626bcbe1 100644 --- a/src/aig/ntl/ntlUtil.c +++ b/src/aig/ntl/ntlUtil.c @@ -30,7 +30,28 @@ /**Function************************************************************* - Synopsis [Returns 1 if netlist was written by ABC with added bufs/invs.] + Synopsis [Counts COs that are connected to the internal nodes through invs/bufs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot ) +{ + Ntl_Obj_t * pObj; + int i, Counter = 0; + Ntl_ModelForEachNode( pRoot, pObj, i ) + if ( Ntl_ObjFaninNum(pObj) == 1 ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Connects COs to the internal nodes other than inv/bufs.] Description [Should be called immediately after reading from file.] @@ -38,6 +59,63 @@ SeeAlso [] +***********************************************************************/ +int Ntl_ManCountSimpleCoDriversOne( Ntl_Net_t * pNetCo ) +{ + Ntl_Net_t * pNetFanin; + // skip the case when the net is not driven by a node + if ( !Ntl_ObjIsNode(pNetCo->pDriver) ) + return 0; + // skip the case when the node is not an inv/buf + if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 ) + return 0; + // skip the case when the second-generation driver is not a node + pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver); + if ( !Ntl_ObjIsNode(pNetFanin->pDriver) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Counts COs that are connected to the internal nodes through invs/bufs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p ) +{ + Ntl_Net_t * pNetCo; + Ntl_Obj_t * pObj; + Ntl_Mod_t * pRoot; + int i, k, Counter; + Counter = 0; + pRoot = Ntl_ManRootModel( p ); + Ntl_ModelForEachPo( pRoot, pObj, i ) + Counter += Ntl_ManCountSimpleCoDriversOne( Ntl_ObjFanin0(pObj) ); + Ntl_ModelForEachLatch( pRoot, pObj, i ) + Counter += Ntl_ManCountSimpleCoDriversOne( Ntl_ObjFanin0(pObj) ); + Ntl_ModelForEachBox( pRoot, pObj, i ) + Ntl_ObjForEachFanin( pObj, pNetCo, k ) + Counter += Ntl_ManCountSimpleCoDriversOne( pNetCo ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Removes the CO drivers that are bufs/invs.] + + Description [Should be called immediately after reading from file.] + + SideEffects [This procedure does not work because the internal net + (pNetFanin) may have other drivers.] + + SeeAlso [] + ***********************************************************************/ int Ntl_ManTransformCoDrivers( Ntl_Man_t * p ) { @@ -110,7 +188,71 @@ int Ntl_ManTransformCoDrivers( Ntl_Man_t * p ) Counter++; } Vec_PtrFree( vCoNets ); - pRoot->nObjs[NTL_OBJ_NODE] -= Counter; + pRoot->nObjs[NTL_OBJ_LUT1] -= Counter; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Connects COs to the internal nodes other than inv/bufs.] + + Description [Should be called immediately after reading from file.] + + SideEffects [This procedure does not work because the internal net + (pNetFanin) may have other drivers.] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ManReconnectCoDriverOne( Ntl_Net_t * pNetCo ) +{ + Ntl_Net_t * pNetFanin; + // skip the case when the net is not driven by a node + if ( !Ntl_ObjIsNode(pNetCo->pDriver) ) + return 0; + // skip the case when the node is not an inv/buf + if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 ) + return 0; + // skip the case when the second-generation driver is not a node + pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver); + if ( !Ntl_ObjIsNode(pNetFanin->pDriver) ) + return 0; + // set the complemented attribute of the net + pNetCo->fCompl = (int)(pNetCo->pDriver->pSop[0] == '0'); + // drive the CO net with the second-generation driver + pNetCo->pDriver = NULL; + pNetFanin->pDriver->pFanio[pNetFanin->pDriver->nFanins] = NULL; + if ( !Ntl_ModelSetNetDriver( pNetFanin->pDriver, pNetCo ) ) + printf( "Ntl_ManReconnectCoDriverOne(): Cannot connect the net.\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Connects COs to the internal nodes other than inv/bufs.] + + Description [Should be called immediately after reading from file.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ManReconnectCoDrivers( Ntl_Man_t * p ) +{ + Ntl_Net_t * pNetCo; + Ntl_Obj_t * pObj; + Ntl_Mod_t * pRoot; + int i, k, Counter; + Counter = 0; + pRoot = Ntl_ManRootModel( p ); + Ntl_ModelForEachPo( pRoot, pObj, i ) + Counter += Ntl_ManReconnectCoDriverOne( Ntl_ObjFanin0(pObj) ); + Ntl_ModelForEachLatch( pRoot, pObj, i ) + Counter += Ntl_ManReconnectCoDriverOne( Ntl_ObjFanin0(pObj) ); + Ntl_ModelForEachBox( pRoot, pObj, i ) + Ntl_ObjForEachFanin( pObj, pNetCo, k ) + Counter += Ntl_ManReconnectCoDriverOne( pNetCo ); return Counter; } @@ -158,6 +300,68 @@ Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p ) return vNames; } +/**Function************************************************************* + + Synopsis [Marks the CI/CO nets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManMarkCiCoNets( Ntl_Man_t * p ) +{ + Ntl_Net_t * pNet; + int i; + Ntl_ManForEachCiNet( p, pNet, i ) + pNet->fMark = 1; + Ntl_ManForEachCoNet( p, pNet, i ) + pNet->fMark = 1; +} + +/**Function************************************************************* + + Synopsis [Unmarks the CI/CO nets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p ) +{ + Ntl_Net_t * pNet; + int i; + Ntl_ManForEachCiNet( p, pNet, i ) + pNet->fMark = 0; + Ntl_ManForEachCoNet( p, pNet, i ) + 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; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c index 9c2c5ed8..a1f20a8e 100644 --- a/src/aig/nwk/nwkMan.c +++ b/src/aig/nwk/nwkMan.c @@ -100,7 +100,6 @@ void Nwk_ManPrintLutSizes( Nwk_Man_t * p, If_Lib_t * pLutLib ) printf( "LUTs by size: " ); for ( i = 0; i <= pLutLib->LutMax; i++ ) printf( "%d:%d ", i, Counters[i] ); - printf( "\n" ); } /**Function************************************************************* @@ -124,6 +123,7 @@ void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib ) printf( "co = %5d ", Nwk_ManCoNum(p) ); printf( "lat = %5d ", Nwk_ManLatchNum(p) ); printf( "node = %5d ", Nwk_ManNodeNum(p) ); + printf( "edge = %5d ", Nwk_ManGetTotalFanins(p) ); printf( "aig = %6d ", Nwk_ManGetAigNodeNum(p) ); printf( "lev = %3d ", Nwk_ManLevel(p) ); // printf( "lev2 = %3d ", Nwk_ManLevelBackup(p) ); -- cgit v1.2.3