diff options
60 files changed, 2366 insertions, 578 deletions
@@ -19,7 +19,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \ src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \ src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \ src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \ - src/aig/bdc src/aig/bar src/aig/ntl src/aig/tim + src/aig/bdc src/aig/bar src/aig/ntl src/aig/ntk src/aig/tim default: $(PROG) @@ -42,7 +42,7 @@ RSC=rc.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c -# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c +# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/ntk" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -66,7 +66,7 @@ LINK32=link.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c -# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c +# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/ntk" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c # SUBTRACT CPP /X # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" @@ -1898,6 +1898,10 @@ SOURCE=.\src\map\if\ifCut.c # End Source File # Begin Source File +SOURCE=.\src\map\if\ifLib.c +# End Source File +# Begin Source File + SOURCE=.\src\map\if\ifMan.c # End Source File # Begin Source File @@ -2478,6 +2482,10 @@ SOURCE=.\src\aig\hop\hopTable.c # End Source File # Begin Source File +SOURCE=.\src\aig\hop\hopTruth.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\hop\hopUtil.c # End Source File # End Group @@ -2942,10 +2950,6 @@ SOURCE=.\src\aig\aig\aigFrames.c # End Source File # Begin Source File -SOURCE=.\src\aig\aig\aigHaig.c -# End Source File -# Begin Source File - SOURCE=.\src\aig\aig\aigInter.c # End Source File # Begin Source File @@ -3102,6 +3106,14 @@ SOURCE=.\src\aig\ntk\ntk.h # End Source File # Begin Source File +SOURCE=.\src\aig\ntk\ntkBidec.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\ntk\ntkCheck.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\ntk\ntkDfs.c # End Source File # Begin Source File diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 8901e8bb..8a61a530 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -103,6 +103,7 @@ struct Aig_Box_t_ struct Aig_Man_t_ { char * pName; // the design name + char * pSpec; // the input file name // AIG nodes Vec_Ptr_t * vPis; // the array of PIs Vec_Ptr_t * vPos; // the array of POs @@ -328,7 +329,6 @@ static inline int Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert( static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); } 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_ObjHaig( Aig_Obj_t * pObj ) { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); } static inline int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)pObj->pNext; } static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin ) { @@ -540,6 +540,7 @@ extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize ); extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize ); extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose ); extern Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose ); +extern Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose ); /*=== aigPartReg.c =========================================================*/ extern Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize ); extern Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize ); @@ -612,6 +613,7 @@ extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName ); extern void Aig_ManSetPioNumbers( Aig_Man_t * p ); extern void Aig_ManCleanPioNumbers( Aig_Man_t * p ); +extern int Aig_ManCountChoices( Aig_Man_t * p ); /*=== aigWin.c =========================================================*/ extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit ); diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 062173e6..665401c3 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -96,6 +96,7 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ) { pObjNew = Aig_ObjCreatePi( pNew ); pObjNew->Level = pObj->Level; + pObjNew->pHaig = pObj->pHaig; pObj->pData = pObjNew; } return pNew; @@ -114,20 +115,16 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ) ***********************************************************************/ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) { + Aig_Obj_t * pObjNew; if ( pObj->pData ) return pObj->pData; Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) ); if ( Aig_ObjIsBuf(pObj) ) return pObj->pData = Aig_ObjChild0Copy(pObj); Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) ); - if ( pNew->pManHaig == NULL ) - return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - else - { - Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig); - return pObj->pData = pObjNew; - } + pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_Regular(pObjNew)->pHaig = pObj->pHaig; + return pObj->pData = pObjNew; } /**Function************************************************************* @@ -156,8 +153,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) 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; // duplicate internal nodes if ( fOrdered ) { @@ -165,61 +160,42 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) { if ( Aig_ObjIsBuf(pObj) ) { - if ( pNew->pManHaig == NULL ) - pObj->pData = Aig_ObjChild0Copy(pObj); - else - { - Aig_Obj_t * pObjNew = Aig_ObjChild0Copy(pObj); - Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig); - pObj->pData = pObjNew; - } + pObjNew = Aig_ObjChild0Copy(pObj); } else if ( Aig_ObjIsNode(pObj) ) { - if ( pNew->pManHaig == NULL ) - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - else - { - Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig); - pObj->pData = pObjNew; - } + pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); } else if ( Aig_ObjIsPi(pObj) ) { pObjNew = Aig_ObjCreatePi( pNew ); - pObjNew->pHaig = pObj->pHaig; pObjNew->Level = pObj->Level; - pObj->pData = pObjNew; } else if ( Aig_ObjIsPo(pObj) ) { pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); - pObjNew->pHaig = pObj->pHaig; - pObj->pData = pObjNew; + } + else if ( Aig_ObjIsConst1(pObj) ) + { + pObjNew = Aig_ManConst1(pNew); } else assert( 0 ); + Aig_Regular(pObjNew)->pHaig = pObj->pHaig; + pObj->pData = pObjNew; } } else { -/* - Aig_ManForEachPi( p, pObj, i ) - { - pObjNew = Aig_ObjCreatePi( pNew ); - pObjNew->pHaig = pObj->pHaig; - pObjNew->Level = pObj->Level; - pObj->pData = pObjNew; - } -*/ + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig; Aig_ManForEachObj( p, pObj, i ) { if ( Aig_ObjIsPi(pObj) ) { pObjNew = Aig_ObjCreatePi( pNew ); - pObjNew->pHaig = pObj->pHaig; pObjNew->Level = pObj->Level; + Aig_Regular(pObjNew)->pHaig = pObj->pHaig; pObj->pData = pObjNew; } else if ( Aig_ObjIsPo(pObj) ) @@ -227,18 +203,10 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) ); // assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level ); pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); - pObjNew->pHaig = pObj->pHaig; + Aig_Regular(pObjNew)->pHaig = pObj->pHaig; pObj->pData = pObjNew; } } -/* - Aig_ManForEachPo( p, pObj, i ) - { - pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); - pObjNew->pHaig = pObj->pHaig; - pObj->pData = pObjNew; - } -*/ } // add the POs assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); @@ -372,6 +340,7 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots ); FREE( p->pSeqModel ); FREE( p->pName ); + FREE( p->pSpec ); FREE( p->pObjCopies ); FREE( p->pReprs ); FREE( p->pEquivs ); @@ -410,6 +379,27 @@ int Aig_ManCleanup( Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Performs one iteration of AIG rewriting.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManHaigCounter( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj; + int Counter, i; + Counter = 0; + Aig_ManForEachNode( pAig, pObj, i ) + Counter += (pObj->pHaig != NULL); + return Counter; +} + +/**Function************************************************************* + Synopsis [Stops the AIG manager.] Description [] @@ -421,8 +411,12 @@ int Aig_ManCleanup( Aig_Man_t * p ) ***********************************************************************/ void Aig_ManPrintStats( Aig_Man_t * p ) { + int nChoices = Aig_ManCountChoices(p); printf( "PI/PO/Lat = %5d/%5d/%5d ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) ); - printf( "A = %7d. ", Aig_ManAndNum(p) ); + printf( "A = %7d. ", Aig_ManAndNum(p) ); + printf( "Eq = %7d. ", Aig_ManHaigCounter(p) ); + if ( nChoices ) + printf( "Ch = %5d. ", nChoices ); if ( Aig_ManExorNum(p) ) printf( "X = %5d. ", Aig_ManExorNum(p) ); if ( Aig_ManBufNum(p) ) diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index 80838e19..734f1277 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -97,12 +97,14 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost ) // update node counters of the manager p->nObjs[Aig_ObjType(pObj)]++; assert( pObj->pData == NULL ); +/* if ( p->pManHaig ) { pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 ); pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 ); pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost ); } +*/ return pObj; } @@ -360,6 +362,7 @@ int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel ) void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel ) { Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew); + Aig_Obj_t * pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig; // the object to be replaced cannot be complemented assert( !Aig_IsComplement(pObjOld) ); // the object to be replaced cannot be a terminal @@ -422,6 +425,7 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) ); Aig_ManPropagateBuffers( p, fNodesOnly, fUpdateLevel ); } + pObjOld->pHaig = pHaig; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index 1fb93eb7..2a9800cf 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "aig.h" +#include "tim.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -1346,6 +1347,235 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM } + + +/**Function************************************************************* + + Synopsis [Set the representative.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ) +{ + assert( p->pReprs != NULL ); + assert( !Aig_IsComplement(pNode1) ); + assert( !Aig_IsComplement(pNode2) ); + assert( pNode1->Id < p->nReprsAlloc ); + assert( pNode2->Id < p->nReprsAlloc ); + if ( pNode1 == pNode2 ) + return; + if ( pNode1->Id < pNode2->Id ) + p->pReprs[pNode2->Id] = pNode1; + else + p->pReprs[pNode1->Id] = pNode2; +} + +/**Function************************************************************* + + Synopsis [Constructively accumulates choices.] + + Description [pNew is a new AIG with choices under construction. + pPrev is the AIG preceding pThis in the order of deriving choices. + pThis is the current AIG to be added to pNew while creating choices.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_t * pThis ) +{ + Aig_Obj_t * pObj, * pObjNew; + int i; + assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(pPrev) ); + assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(pThis) ); + assert( Aig_ManPoNum(pNew) == Aig_ManPoNum(pPrev) ); + assert( Aig_ManPoNum(pNew) == Aig_ManPoNum(pThis) ); + // make sure the nodes of pPrev point to pNew + Aig_ManForEachObj( pNew, pObj, i ) + pObj->fMarkB = 1; + Aig_ManForEachObj( pPrev, pObj, i ) + assert( Aig_Regular(pObj->pData)->fMarkB ); + Aig_ManForEachObj( pNew, pObj, i ) + pObj->fMarkB = 0; + // make sure the nodes of pThis point to pPrev + Aig_ManForEachObj( pPrev, pObj, i ) + pObj->fMarkB = 1; + Aig_ManForEachObj( pThis, pObj, i ) + assert( pObj->pHaig == NULL || (!Aig_IsComplement(pObj->pHaig) && pObj->pHaig->fMarkB) ); + Aig_ManForEachObj( pPrev, pObj, i ) + pObj->fMarkB = 0; + // remap nodes of pThis on top of pNew using pPrev + pObj = Aig_ManConst1(pThis); + pObj->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( pThis, pObj, i ) + pObj->pData = Aig_ManPi(pNew, i); + Aig_ManForEachPo( pThis, pObj, i ) + pObj->pData = Aig_ManPo(pNew, i); + // go through the nodes in the topological order + Aig_ManForEachNode( pThis, pObj, i ) + { + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + if ( pObj->pHaig == NULL ) + continue; + // pObj->pData and pObj->pHaig->pData are equivalent + Aig_ObjSetRepr( pNew, Aig_Regular(pObj->pData), Aig_Regular(pObj->pHaig->pData) ); + } + // set the inputs of POs as equivalent + Aig_ManForEachPo( pThis, pObj, i ) + { + pObjNew = Aig_ObjFanin0( Aig_ManPo(pNew,i) ); + // pObjNew and Aig_ObjFanin0(pObj)->pData are equivalent + Aig_ObjSetRepr( pNew, pObjNew, Aig_Regular(Aig_ObjFanin0(pObj)->pData) ); + } +} + +/**Function************************************************************* + + Synopsis [Computes levels for AIG with choices and white boxes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pNext; + int i, iBox, iTerm1, nTerms, LevelMax = 0; + if ( Aig_ObjIsTravIdCurrent( pNew, pObj ) ) + return; + Aig_ObjSetTravIdCurrent( pNew, pObj ); + if ( Aig_ObjIsPi(pObj) ) + { + if ( pNew->pManTime ) + { + iBox = Tim_ManBoxForCi( pNew->pManTime, Aig_ObjPioNum(pObj) ); + if ( iBox >= 0 ) // this is not a true PI + { + iTerm1 = Tim_ManBoxInputFirst( pNew->pManTime, iBox ); + nTerms = Tim_ManBoxInputNum( pNew->pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pNext = Aig_ManPo(pNew, iTerm1 + i); + Aig_ManChoiceLevel_rec( pNew, pNext ); + if ( LevelMax < Aig_ObjLevel(pNext) ) + LevelMax = Aig_ObjLevel(pNext); + } + LevelMax++; + } + } + } + else if ( Aig_ObjIsPo(pObj) ) + { + pNext = Aig_ObjFanin0(pObj); + Aig_ManChoiceLevel_rec( pNew, pNext ); + if ( LevelMax < Aig_ObjLevel(pNext) ) + LevelMax = Aig_ObjLevel(pNext); + } + else if ( Aig_ObjIsNode(pObj) ) + { + // get the maximum level of the two fanins + pNext = Aig_ObjFanin0(pObj); + Aig_ManChoiceLevel_rec( pNew, pNext ); + if ( LevelMax < Aig_ObjLevel(pNext) ) + LevelMax = Aig_ObjLevel(pNext); + pNext = Aig_ObjFanin1(pObj); + Aig_ManChoiceLevel_rec( pNew, pNext ); + if ( LevelMax < Aig_ObjLevel(pNext) ) + LevelMax = Aig_ObjLevel(pNext); + LevelMax++; + + // get the level of the nodes in the choice node + if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->iData]) ) + { + Aig_ManChoiceLevel_rec( pNew, pNext ); + if ( LevelMax < Aig_ObjLevel(pNext) ) + LevelMax = Aig_ObjLevel(pNext); + } + } + else + assert( 0 ); + Aig_ObjSetLevel( pObj, LevelMax ); +} + +/**Function************************************************************* + + Synopsis [Computes levels for AIG with choices and white boxes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManChoiceLevel( Aig_Man_t * pNew ) +{ + Aig_Obj_t * pObj; + int i, LevelMax = 0; + Aig_ManForEachObj( pNew, pObj, i ) + Aig_ObjSetLevel( pObj, 0 ); + Aig_ManSetPioNumbers( pNew ); + Aig_ManIncrementTravId( pNew ); + Aig_ManForEachPo( pNew, pObj, i ) + { + Aig_ManChoiceLevel_rec( pNew, pObj ); + if ( LevelMax < Aig_ObjLevel(pObj) ) + LevelMax = Aig_ObjLevel(pObj); + } + Aig_ManCleanPioNumbers( pNew ); + return LevelMax; +} + +/**Function************************************************************* + + Synopsis [Constructively accumulates choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose ) +{ + Aig_Man_t * pNew, * pThis, * pPrev; + int i; + // start AIG with choices + pPrev = Vec_PtrEntry( vAigs, 0 ); + pNew = Aig_ManDup( pPrev, 1 ); + // create room for equivalent nodes and representatives + assert( pNew->pReprs == NULL ); + pNew->nReprsAlloc = Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pNew); + pNew->pReprs = ALLOC( Aig_Obj_t *, pNew->nReprsAlloc ); + memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * pNew->nReprsAlloc ); + // add other AIGs one by one + Vec_PtrForEachEntryStart( vAigs, pThis, i, 1 ) + { + Aig_ManChoiceConstructiveOne( pNew, pPrev, pThis ); + pPrev = pThis; + } + // derive the result of choicing +//Aig_ManPrintStats( pNew ); + pNew = Aig_ManRehash( pNew ); +//Aig_ManPrintStats( pNew ); + // create the equivalent nodes lists + Aig_ManMarkValidChoices( pNew ); +//Aig_ManPrintStats( pNew ); + // reset levels + Aig_ManChoiceLevel( pNew ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigRetF.c b/src/aig/aig/aigRetF.c index 8ca4fba1..4318be9d 100644 --- a/src/aig/aig/aigRetF.c +++ b/src/aig/aig/aigRetF.c @@ -178,6 +178,7 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax ) p->nObjs[AIG_OBJ_BUF]++; Aig_ObjConnect( p, pObj, Aig_NotCond(pObjLo, fCompl), NULL ); // create HAIG if defined +/* if ( p->pManHaig ) { // create HAIG latch @@ -188,6 +189,7 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax ) assert( pObjLo->pHaig->pHaig == NULL ); pObjLo->pHaig->pHaig = Aig_Regular(pObj->pHaig); } +*/ // mark the change fChange = 1; // check the limit diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index 7900da51..dcc0a118 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -890,6 +890,28 @@ void Aig_ManCleanPioNumbers( Aig_Man_t * p ) pObj->pNext = NULL; } +/**Function************************************************************* + + Synopsis [Sets the PI/PO numbers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManCountChoices( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + Aig_ManForEachNode( p, pObj, i ) + Counter += Aig_ObjIsChoice( p, pObj ); + return Counter; +} + + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index b02d3bb5..00a85c26 100644 --- a/src/aig/aig/module.make +++ b/src/aig/aig/module.make @@ -3,7 +3,6 @@ SRC += src/aig/aig/aigCheck.c \ src/aig/aig/aigDfs.c \ src/aig/aig/aigFanout.c \ src/aig/aig/aigFrames.c \ - src/aig/aig/aigHaig.c \ src/aig/aig/aigInter.c \ src/aig/aig/aigMan.c \ src/aig/aig/aigMem.c \ diff --git a/src/aig/bdc/bdc.h b/src/aig/bdc/bdc.h index e0c35773..fc476ec6 100644 --- a/src/aig/bdc/bdc.h +++ b/src/aig/bdc/bdc.h @@ -37,6 +37,7 @@ extern "C" { /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// +typedef struct Bdc_Fun_t_ Bdc_Fun_t; typedef struct Bdc_Man_t_ Bdc_Man_t; typedef struct Bdc_Par_t_ Bdc_Par_t; struct Bdc_Par_t_ @@ -47,6 +48,12 @@ struct Bdc_Par_t_ int fVeryVerbose; // enable detailed stats }; +// working with complemented attributes of objects +static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01); } +static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01); } +static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)01); } +static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)(c!=0)); } + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -59,6 +66,13 @@ struct Bdc_Par_t_ extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ); extern void Bdc_ManFree( Bdc_Man_t * p ); extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax ); +extern Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i ); +extern Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p ); +extern int Bdc_ManNodeNum( Bdc_Man_t * p ); +extern Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p ); +extern Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p ); +extern void * Bdc_FuncCopy( Bdc_Fun_t * p ); +extern void Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy ); #ifdef __cplusplus diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c index d7811f82..e7675420 100644 --- a/src/aig/bdc/bdcCore.c +++ b/src/aig/bdc/bdcCore.c @@ -24,12 +24,32 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [Accessing contents of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i ) { return Bdc_FunWithId(p, i); } +Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p ) { return p->pRoot; } +int Bdc_ManNodeNum( Bdc_Man_t * p ) { return p->nNodes; } +Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p ) { return p->pFan0; } +Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p ) { return p->pFan1; } +void * Bdc_FuncCopy( Bdc_Fun_t * p ) { return p->pCopy; } +void Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy ) { p->pCopy = pCopy; } + +/**Function************************************************************* + Synopsis [Allocate resynthesis manager.] Description [] diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h index afba0e67..ab800269 100644 --- a/src/aig/bdc/bdcInt.h +++ b/src/aig/bdc/bdcInt.h @@ -54,7 +54,6 @@ typedef enum { BDC_TYPE_OTHER // 7: unused } Bdc_Type_t; -typedef struct Bdc_Fun_t_ Bdc_Fun_t; struct Bdc_Fun_t_ { int Type; // Const1, PI, AND, XOR, MUX @@ -122,12 +121,6 @@ struct Bdc_Man_t_ int timeTotal; }; -// working with complemented attributes of objects -static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01); } -static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01); } -static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)01); } -static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)(c!=0)); } - static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p ) { Bdc_Fun_t * pRes; if ( p->nNodes >= p->nNodesAlloc || p->nNodesNew >= p->nNodesMax ) return NULL; pRes = p->pNodes + p->nNodes++; p->nNodesNew++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); return pRes; } static inline Bdc_Fun_t * Bdc_FunWithId( Bdc_Man_t * p, int Id ) { assert( Id < p->nNodes ); return p->pNodes + Id; } static inline int Bdc_FunId( Bdc_Man_t * p, Bdc_Fun_t * pFun ) { return pFun - p->pNodes; } diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h index a428f435..d93af02e 100644 --- a/src/aig/dar/dar.h +++ b/src/aig/dar/dar.h @@ -92,7 +92,7 @@ extern Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig ); extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ); extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ); extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose ); -extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose ); +extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose ); #ifdef __cplusplus } diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index 01f75e32..03707481 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -164,6 +164,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * // make sure the balanced node is not assigned // assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level ); assert( pObjOld->pData == NULL ); + Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig; return pObjOld->pData = pObjNew; } diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index fad4148c..a4ac9082 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -112,6 +112,26 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) return pAig; } +/**Function************************************************************* + + Synopsis [Performs one iteration of AIG rewriting.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManHaigPrintStats( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj; + int Counter, i; + Counter = 0; + Aig_ManForEachNode( pAig, pObj, i ) + Counter += (pObj->pHaig != NULL); + printf( "Total nodes = %6d. Equiv nodes = %6d.\n", Aig_ManNodeNum(pAig), Counter ); +} /**Function************************************************************* @@ -314,42 +334,28 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL //alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" { Vec_Ptr_t * vAigs; + Aig_Obj_t * pObj; + int i; + vAigs = Vec_PtrAlloc( 3 ); pAig = Aig_ManDup(pAig, 0); Vec_PtrPush( vAigs, pAig ); - pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose); - Vec_PtrPush( vAigs, pAig ); - pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose); - Vec_PtrPush( vAigs, pAig ); - return vAigs; -} -/**Function************************************************************* + Aig_ManForEachObj( pAig, pObj, i ) + pObj->pHaig = pObj; - Synopsis [Gives the current ABC network to AIG manager for processing.] - - Description [] - - SideEffects [] + pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose); + Vec_PtrPush( vAigs, pAig ); +//Aig_ManPrintStats( pAig ); - SeeAlso [] + Aig_ManForEachObj( pAig, pObj, i ) + pObj->pHaig = pObj; -***********************************************************************/ -/* -Vec_Ptr_t * Dar_ManChoiceSynthesisExt() -{ - Vec_Ptr_t * vAigs; - Aig_Man_t * pMan; - vAigs = Vec_PtrAlloc( 3 ); - pMan = Ioa_ReadAiger( "i10_1.aig", 1 ); - Vec_PtrPush( vAigs, pMan ); - pMan = Ioa_ReadAiger( "i10_2.aig", 1 ); - Vec_PtrPush( vAigs, pMan ); - pMan = Ioa_ReadAiger( "i10_3.aig", 1 ); - Vec_PtrPush( vAigs, pMan ); + pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose); + Vec_PtrPush( vAigs, pAig ); +//Aig_ManPrintStats( pAig ); return vAigs; } -*/ /**Function************************************************************* @@ -362,7 +368,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesisExt() SeeAlso [] ***********************************************************************/ -Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose ) +Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose ) { Aig_Man_t * pMan, * pTemp; Vec_Ptr_t * vAigs; @@ -374,16 +380,22 @@ clk = clock(); // swap the first and last network // this should lead to the primary choice being "better" because of synthesis - pMan = Vec_PtrPop( vAigs ); - Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) ); - Vec_PtrWriteEntry( vAigs, 0, pMan ); + if ( !fConstruct ) + { + pMan = Vec_PtrPop( vAigs ); + Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) ); + Vec_PtrWriteEntry( vAigs, 0, pMan ); + } if ( fVerbose ) { PRT( "Synthesis time", clock() - clk ); } clk = clock(); - pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose ); + if ( fConstruct ) + pMan = Aig_ManChoiceConstructive( vAigs, fVerbose ); + else + pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose ); Vec_PtrForEachEntry( vAigs, pTemp, i ) Aig_ManStop( pTemp ); Vec_PtrFree( vAigs ); diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h index 6390ff70..d7f525a2 100644 --- a/src/aig/hop/hop.h +++ b/src/aig/hop/hop.h @@ -321,6 +321,8 @@ extern void Hop_TableInsert( Hop_Man_t * p, Hop_Obj_t * pObj ); extern void Hop_TableDelete( Hop_Man_t * p, Hop_Obj_t * pObj ); extern int Hop_TableCountEntries( Hop_Man_t * p ); extern void Hop_TableProfile( Hop_Man_t * p ); +/*=== hopTruth.c ========================================================*/ +unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst ); /*=== hopUtil.c =========================================================*/ extern void Hop_ManIncrementTravId( Hop_Man_t * p ); extern void Hop_ManCleanData( Hop_Man_t * p ); diff --git a/src/aig/hop/hopTruth.c b/src/aig/hop/hopTruth.c new file mode 100644 index 00000000..9a2161b6 --- /dev/null +++ b/src/aig/hop/hopTruth.c @@ -0,0 +1,210 @@ +/**CFile**************************************************************** + + FileName [hopTruth.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: hopTruth.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "hop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Hop_ManTruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } + +static inline void Hop_ManTruthCopy( unsigned * pOut, unsigned * pIn, int nVars ) +{ + int w; + for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = pIn[w]; +} +static inline void Hop_ManTruthClear( unsigned * pOut, int nVars ) +{ + int w; + for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = 0; +} +static inline void Hop_ManTruthFill( unsigned * pOut, int nVars ) +{ + int w; + for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = ~(unsigned)0; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Construct BDDs and mark AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Hop_ManConvertAigToTruth_rec1( Hop_Obj_t * pObj ) +{ + int Counter = 0; + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) + return 0; + Counter += Hop_ManConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) ); + Counter += Hop_ManConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) ); + assert( !Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjSetMarkA( pObj ); + return Counter + 1; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Hop_ManConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords ) +{ + unsigned * pTruth, * pTruth0, * pTruth1; + int i; + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) ) + return pObj->pData; + // compute the truth tables of the fanins + pTruth0 = Hop_ManConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords ); + pTruth1 = Hop_ManConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords ); + // creat the truth table of the node + pTruth = Vec_IntFetch( vTruth, nWords ); + if ( Hop_ObjIsExor(pObj) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] ^ pTruth1[i]; + else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & pTruth1[i]; + else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & ~pTruth1[i]; + else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & pTruth1[i]; + else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & ~pTruth1[i]; + assert( Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjClearMarkA( pObj ); + pObj->pData = pTruth; + return pTruth; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the node.] + + Description [Assumes that the structural support is no more than 8 inputs. + Uses array vTruth to store temporary truth tables. The returned pointer should + be used immediately.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst ) +{ + static unsigned uTruths[8][8] = { // elementary truth tables + { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, + { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, + { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, + { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, + { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, + { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, + { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, + { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } + }; + Hop_Obj_t * pObj; + unsigned * pTruth, * pTruth2; + int i, nWords, nNodes; + Vec_Ptr_t * vTtElems; + + // if the number of variables is more than 8, allocate truth tables + if ( nVars > 8 ) + vTtElems = Vec_PtrAllocTruthTables( nVars ); + else + vTtElems = NULL; + + // clear the data fields and set marks + nNodes = Hop_ManConvertAigToTruth_rec1( pRoot ); + // prepare memory + nWords = Hop_TruthWordNum( nVars ); + Vec_IntClear( vTruth ); + Vec_IntGrow( vTruth, nWords * (nNodes+1) ); + pTruth = Vec_IntFetch( vTruth, nWords ); + // check the case of a constant + if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) ) + { + assert( nNodes == 0 ); + if ( Hop_IsComplement(pRoot) ) + Hop_ManTruthClear( pTruth, nVars ); + else + Hop_ManTruthFill( pTruth, nVars ); + return pTruth; + } + // set elementary truth tables at the leaves + assert( nVars <= Hop_ManPiNum(p) ); +// assert( Hop_ManPiNum(p) <= 8 ); + if ( fMsbFirst ) + { + Hop_ManForEachPi( p, pObj, i ) + { + if ( vTtElems ) + pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i); + else + pObj->pData = (void *)uTruths[nVars-1-i]; + } + } + else + { + Hop_ManForEachPi( p, pObj, i ) + { + if ( vTtElems ) + pObj->pData = Vec_PtrEntry(vTtElems, i); + else + pObj->pData = (void *)uTruths[i]; + } + } + // clear the marks and compute the truth table + pTruth2 = Hop_ManConvertAigToTruth_rec2( pRoot, vTruth, nWords ); + // copy the result + Hop_ManTruthCopy( pTruth, pTruth2, nVars ); + if ( vTtElems ) + Vec_PtrFree( vTtElems ); + return pTruth; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/hop/hop_.c b/src/aig/hop/hop_.c index 468413fa..658b8c4e 100644 --- a/src/aig/hop/hop_.c +++ b/src/aig/hop/hop_.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [ivy_.c] + FileName [hop_.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,11 +14,11 @@ Date [Ver. 1.0. Started - May 11, 2006.] - Revision [$Id: ivy_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + Revision [$Id: hop_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] ***********************************************************************/ -#include "ivy.h" +#include "hop.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/aig/hop/module.make b/src/aig/hop/module.make index b06d91fd..e60ec4e8 100644 --- a/src/aig/hop/module.make +++ b/src/aig/hop/module.make @@ -6,4 +6,5 @@ SRC += src/aig/hop/hopBalance.c \ src/aig/hop/hopObj.c \ src/aig/hop/hopOper.c \ src/aig/hop/hopTable.c \ + src/aig/hop/hopTruth.c \ src/aig/hop/hopUtil.c diff --git a/src/aig/ntk/module.make b/src/aig/ntk/module.make new file mode 100644 index 00000000..b668de2f --- /dev/null +++ b/src/aig/ntk/module.make @@ -0,0 +1,9 @@ +SRC += src/aig/ntk/ntkCheck.c \ + src/aig/ntk/ntkBidec.c \ + src/aig/ntk/ntkDfs.c \ + src/aig/ntk/ntkFanio.c \ + src/aig/ntk/ntkMan.c \ + src/aig/ntk/ntkMap.c \ + src/aig/ntk/ntkObj.c \ + src/aig/ntk/ntkTiming.c \ + src/aig/ntk/ntkUtil.c diff --git a/src/aig/ntk/ntk.h b/src/aig/ntk/ntk.h index 6ddfac81..2fcb6ddc 100644 --- a/src/aig/ntk/ntk.h +++ b/src/aig/ntk/ntk.h @@ -30,7 +30,9 @@ extern "C" { //////////////////////////////////////////////////////////////////////// #include "aig.h" +#include "hop.h" #include "tim.h" +#include "if.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -66,7 +68,7 @@ struct Ntk_Man_t_ int nObjs[NTK_OBJ_VOID]; // counter of objects of each type int nFanioPlus; // the number of extra fanins/fanouts alloc by default // functionality, timing, memory, etc - Aig_Man_t * pAig; // the functionality representation + Hop_Man_t * pManHop; // the functionality representation Tim_Man_t * pManTime; // the timing manager Aig_MmFlex_t * pMemObjs; // memory for objects Vec_Ptr_t * vTemp; // array used for incremental updates @@ -77,9 +79,10 @@ struct Ntk_Obj_t_ { Ntk_Man_t * pMan; // the manager void * pCopy; // temporary pointer - void * pFunc; // functionality + Hop_Obj_t * pFunc; // functionality // node information int Id; // unique ID + int PioId; // number of this node in the PI/PO list unsigned Type : 3; // object type unsigned fCompl : 1; // complemented attribute unsigned MarkA : 1; // temporary mark @@ -113,6 +116,10 @@ static inline int Ntk_ManLatchNum( Ntk_Man_t * p ) { return p->nO static inline int Ntk_ManBoxNum( Ntk_Man_t * p ) { return p->nObjs[NTK_OBJ_BOX]; } static inline int Ntk_ManObjNumMax( Ntk_Man_t * p ) { return Vec_PtrSize(p->vObjs); } +static inline Ntk_Obj_t * Ntk_ManCi( Ntk_Man_t * p, int i ) { return Vec_PtrEntry( p->vCis, i ); } +static inline Ntk_Obj_t * Ntk_ManCo( Ntk_Man_t * p, int i ) { return Vec_PtrEntry( p->vCos, i ); } +static inline Ntk_Obj_t * Ntk_ManObj( Ntk_Man_t * p, int i ) { return Vec_PtrEntry( p->vObjs, i ); } + static inline int Ntk_ObjFaninNum( Ntk_Obj_t * p ) { return p->nFanins; } static inline int Ntk_ObjFanoutNum( Ntk_Obj_t * p ) { return p->nFanouts; } @@ -126,8 +133,8 @@ static inline int Ntk_ObjIsCo( Ntk_Obj_t * p ) { return p->Ty static inline int Ntk_ObjIsNode( Ntk_Obj_t * p ) { return p->Type == NTK_OBJ_NODE; } static inline int Ntk_ObjIsLatch( Ntk_Obj_t * p ) { return p->Type == NTK_OBJ_LATCH; } static inline int Ntk_ObjIsBox( Ntk_Obj_t * p ) { return p->Type == NTK_OBJ_BOX; } -static inline int Ntk_ObjIsPi( Ntk_Obj_t * p ) { return Ntk_ObjFaninNum(p) == 0 || (Ntk_ObjFaninNum(p) == 1 && Ntk_ObjIsLatch(Ntk_ObjFanin0(p))); } -static inline int Ntk_ObjIsPo( Ntk_Obj_t * p ) { return Ntk_ObjFanoutNum(p)== 0 || (Ntk_ObjFanoutNum(p)== 1 && Ntk_ObjIsLatch(Ntk_ObjFanout0(p))); } +static inline int Ntk_ObjIsPi( Ntk_Obj_t * p ) { return Ntk_ObjIsCi(p) && Tim_ManBoxForCi(p->pMan->pManTime, p->PioId) == -1; } +static inline int Ntk_ObjIsPo( Ntk_Obj_t * p ) { return Ntk_ObjIsCo(p) && Tim_ManBoxForCo(p->pMan->pManTime, p->PioId) == -1; } static inline float Ntk_ObjArrival( Ntk_Obj_t * pObj ) { return pObj->tArrival; } static inline float Ntk_ObjRequired( Ntk_Obj_t * pObj ) { return pObj->tRequired; } @@ -181,42 +188,41 @@ static inline int Ntk_ObjIsTravIdPrevious( Ntk_Obj_t * pObj ) { r /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== ntlDfs.c ==========================================================*/ +/*=== ntkDfs.c ==========================================================*/ +extern int Ntk_ManLevel( Ntk_Man_t * pNtk ); +extern int Ntk_ManLevel2( Ntk_Man_t * pNtk ); extern Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk ); extern Vec_Ptr_t * Ntk_ManDfsReverse( Ntk_Man_t * pNtk ); -/*=== ntlFanio.c ==========================================================*/ +/*=== ntkFanio.c ==========================================================*/ extern void Ntk_ObjCollectFanins( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes ); extern void Ntk_ObjCollectFanouts( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes ); extern void Ntk_ObjAddFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin ); extern void Ntk_ObjDeleteFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin ); extern void Ntk_ObjPatchFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFaninOld, Ntk_Obj_t * pFaninNew ); extern void Ntk_ObjReplace( Ntk_Obj_t * pNodeOld, Ntk_Obj_t * pNodeNew ); -/*=== ntlMan.c ============================================================*/ +/*=== ntkMan.c ============================================================*/ extern Ntk_Man_t * Ntk_ManAlloc(); extern void Ntk_ManFree( Ntk_Man_t * p ); -extern void Ntk_ManPrintStats( Ntk_Man_t * p ); -/*=== ntlMap.c ============================================================*/ -extern Ntk_Man_t * Ntk_MappingIf( Aig_Man_t * p, void * pPars ); -/*=== ntlObj.c ============================================================*/ -extern Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * pMan ); -extern Ntk_Obj_t * Ntk_ManCreatePo( Ntk_Man_t * pMan ); +extern void Ntk_ManPrintStats( Ntk_Man_t * p, If_Lib_t * pLutLib ); +/*=== ntkMap.c ============================================================*/ +/*=== ntkObj.c ============================================================*/ +extern Ntk_Obj_t * Ntk_ManCreateCi( Ntk_Man_t * pMan, int nFanouts ); +extern Ntk_Obj_t * Ntk_ManCreateCo( Ntk_Man_t * pMan ); extern Ntk_Obj_t * Ntk_ManCreateNode( Ntk_Man_t * pMan, int nFanins, int nFanouts ); extern Ntk_Obj_t * Ntk_ManCreateBox( Ntk_Man_t * pMan, int nFanins, int nFanouts ); extern Ntk_Obj_t * Ntk_ManCreateLatch( Ntk_Man_t * pMan ); extern void Ntk_ManDeleteNode( Ntk_Obj_t * pObj ); extern void Ntk_ManDeleteNode_rec( Ntk_Obj_t * pObj ); -/*=== ntlUtil.c ============================================================*/ +/*=== ntkTiming.c ============================================================*/ +extern float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, If_Lib_t * pLutLib ); +extern void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, If_Lib_t * pLutLib ); +/*=== ntkUtil.c ============================================================*/ extern void Ntk_ManIncrementTravId( Ntk_Man_t * pNtk ); extern int Ntk_ManGetFaninMax( Ntk_Man_t * pNtk ); extern int Ntk_ManGetTotalFanins( Ntk_Man_t * pNtk ); -extern int Ntk_ManLevel( Ntk_Man_t * pNtk ); extern int Ntk_ManPiNum( Ntk_Man_t * pNtk ); extern int Ntk_ManPoNum( Ntk_Man_t * pNtk ); - -/*=== ntlReadBlif.c ==========================================================*/ -extern Ntk_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck ); -/*=== ntlWriteBlif.c ==========================================================*/ -extern void Ioa_WriteBlif( Ntk_Man_t * p, char * pFileName ); +extern int Ntk_ManGetAigNodeNum( Ntk_Man_t * pNtk ); #ifdef __cplusplus } diff --git a/src/aig/ntk/ntkBidec.c b/src/aig/ntk/ntkBidec.c new file mode 100644 index 00000000..43426d13 --- /dev/null +++ b/src/aig/ntk/ntkBidec.c @@ -0,0 +1,123 @@ +/**CFile**************************************************************** + + FileName [ntkBidec.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [Bi-decomposition of local functions.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ntkBidec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ntk.h" +#include "bdc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) ); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Resynthesizes nodes using bi-decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Ntk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare ) +{ + unsigned * pTruth; + Bdc_Fun_t * pFunc; + int nNodes, i; + assert( nVars <= 16 ); + // derive truth table + pTruth = Hop_ManConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 ); + if ( Hop_IsComplement(pRoot) ) + for ( i = Aig_TruthWordNum(nVars)-1; i >= 0; i-- ) + pTruth[i] = ~pTruth[i]; + // decompose truth table + Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 ); + // convert back into HOP + Bdc_FuncSetCopy( Bdc_ManFunc( p, 0 ), Hop_ManConst1( pHop ) ); + for ( i = 0; i < nVars; i++ ) + Bdc_FuncSetCopy( Bdc_ManFunc( p, i+1 ), Hop_ManPi( pHop, i ) ); + nNodes = Bdc_ManNodeNum(p); + for ( i = nVars + 1; i < nNodes; i++ ) + { + pFunc = Bdc_ManFunc( p, i ); + Bdc_FuncSetCopy( pFunc, Hop_And( pHop, Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) ); + } + return Bdc_FunCopyHop( Bdc_ManRoot(p) ); +} + +/**Function************************************************************* + + Synopsis [Resynthesizes nodes using bi-decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntk_ManBidecResyn( Ntk_Man_t * pNtk, int fVerbose ) +{ + Bdc_Par_t Pars = {0}, * pPars = &Pars; + Bdc_Man_t * p; + Ntk_Obj_t * pObj; + Vec_Int_t * vTruth; + int i, nGainTotal = 0, nNodes1, nNodes2; + int clk = clock(); + pPars->nVarsMax = Ntk_ManGetFaninMax( pNtk ); + pPars->fVerbose = fVerbose; + if ( pPars->nVarsMax > 15 ) + { + if ( fVerbose ) + printf( "Resynthesis is not performed for nodes with more than 15 inputs.\n" ); + pPars->nVarsMax = 15; + } + vTruth = Vec_IntAlloc( 0 ); + p = Bdc_ManAlloc( pPars ); + Ntk_ManForEachNode( pNtk, pObj, i ) + { + if ( Ntk_ObjFaninNum(pObj) > 15 ) + continue; + nNodes1 = Hop_DagSize(pObj->pFunc); + pObj->pFunc = Ntk_NodeIfNodeResyn( p, pNtk->pManHop, pObj->pFunc, Ntk_ObjFaninNum(pObj), vTruth, NULL ); + nNodes2 = Hop_DagSize(pObj->pFunc); + nGainTotal += nNodes1 - nNodes2; + } + Bdc_ManFree( p ); + Vec_IntFree( vTruth ); + if ( fVerbose ) + { + printf( "Total gain in AIG nodes = %d. ", nGainTotal ); + PRT( "Total runtime", clock() - clk ); + } +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ntk/ntkCheck.c b/src/aig/ntk/ntkCheck.c new file mode 100644 index 00000000..6bbb67a6 --- /dev/null +++ b/src/aig/ntk/ntkCheck.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [ntk_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Netlist representation.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ntk_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ntk.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ntk/ntkDfs.c b/src/aig/ntk/ntkDfs.c index ce176898..263a2740 100644 --- a/src/aig/ntk/ntkDfs.c +++ b/src/aig/ntk/ntkDfs.c @@ -30,6 +30,62 @@ /**Function************************************************************* + Synopsis [Computes the number of logic levels not counting PIs/POs.] + + Description [Assumes that white boxes have unit level.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntk_ManLevel( Ntk_Man_t * pNtk ) +{ + Tim_Man_t * pManTimeUnit; + Ntk_Obj_t * pObj, * pFanin; + int i, k, LevelMax, Level; + // clean the levels + Ntk_ManForEachObj( pNtk, pObj, i ) + Ntk_ObjSetLevel( pObj, 0 ); + // perform level computation + LevelMax = 0; + pManTimeUnit = Tim_ManDupUnit( pNtk->pManTime ); + Tim_ManIncrementTravId( pManTimeUnit ); + Ntk_ManForEachObj( pNtk, pObj, i ) + { + if ( Ntk_ObjIsCi(pObj) ) + { + Level = (int)Tim_ManGetPiArrival( pManTimeUnit, pObj->PioId ); + Ntk_ObjSetLevel( pObj, Level ); + } + else if ( Ntk_ObjIsCo(pObj) ) + { + Level = Ntk_ObjLevel( Ntk_ObjFanin0(pObj) ); + Tim_ManSetPoArrival( pManTimeUnit, pObj->PioId, (float)Level ); + Ntk_ObjSetLevel( pObj, Level ); + if ( LevelMax < Ntk_ObjLevel(pObj) ) + LevelMax = Ntk_ObjLevel(pObj); + } + else if ( Ntk_ObjIsNode(pObj) ) + { + Level = 0; + Ntk_ObjForEachFanin( pObj, pFanin, k ) + if ( Level < Ntk_ObjLevel(pFanin) ) + Level = Ntk_ObjLevel(pFanin); + Ntk_ObjSetLevel( pObj, Level + 1 ); + } + else + assert( 0 ); + } + // set the old timing manager + Tim_ManStop( pManTimeUnit ); + return LevelMax; +} + + + +/**Function************************************************************* + Synopsis [Performs DFS for one node.] Description [] @@ -39,16 +95,96 @@ SeeAlso [] ***********************************************************************/ -void Ntk_ManDfs_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes ) +void Ntk_ManLevel2_rec( Ntk_Obj_t * pObj ) +{ + Ntk_Obj_t * pNext; + int i, iBox, iTerm1, nTerms, LevelMax = 0; + if ( Ntk_ObjIsTravIdCurrent( pObj ) ) + return; + Ntk_ObjSetTravIdCurrent( pObj ); + if ( Ntk_ObjIsCi(pObj) ) + { + iBox = Tim_ManBoxForCi( pObj->pMan->pManTime, pObj->PioId ); + if ( iBox >= 0 ) // this is not a true PI + { + iTerm1 = Tim_ManBoxInputFirst( pObj->pMan->pManTime, iBox ); + nTerms = Tim_ManBoxInputNum( pObj->pMan->pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pNext = Ntk_ManCo(pObj->pMan, iTerm1 + i); + Ntk_ManLevel2_rec( pNext ); + if ( LevelMax < Ntk_ObjLevel(pNext) ) + LevelMax = Ntk_ObjLevel(pNext); + } + LevelMax++; + } + } + else if ( Ntk_ObjIsNode(pObj) || Ntk_ObjIsCo(pObj) ) + { + Ntk_ObjForEachFanin( pObj, pNext, i ) + { + Ntk_ManLevel2_rec( pNext ); + if ( LevelMax < Ntk_ObjLevel(pNext) ) + LevelMax = Ntk_ObjLevel(pNext); + } + if ( Ntk_ObjIsNode(pObj) ) + LevelMax++; + } + else + assert( 0 ); + Ntk_ObjSetLevel( pObj, LevelMax ); +} + +/**Function************************************************************* + + Synopsis [Returns the DFS ordered array of all objects except latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntk_ManLevel2( Ntk_Man_t * pNtk ) +{ + Ntk_Obj_t * pObj; + int i, LevelMax = 0; + Ntk_ManForEachObj( pNtk, pObj, i ) + Ntk_ObjSetLevel( pObj, 0 ); + Ntk_ManIncrementTravId( pNtk ); + Ntk_ManForEachPo( pNtk, pObj, i ) + { + Ntk_ManLevel2_rec( pObj ); + if ( LevelMax < Ntk_ObjLevel(pObj) ) + LevelMax = Ntk_ObjLevel(pObj); + } + return LevelMax; +} + + + +/**Function************************************************************* + + Synopsis [Performs DFS for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntk_ManDfs_rec( Ntk_Obj_t * pObj, Vec_Ptr_t * vNodes ) { Ntk_Obj_t * pNext; int i; - if ( Ntk_ObjIsTravIdCurrent( pNode ) ) + if ( Ntk_ObjIsTravIdCurrent( pObj ) ) return; - Ntk_ObjSetTravIdCurrent( pNode ); - Ntk_ObjForEachFanin( pNode, pNext, i ) + Ntk_ObjSetTravIdCurrent( pObj ); + Ntk_ObjForEachFanin( pObj, pNext, i ) Ntk_ManDfs_rec( pNext, vNodes ); - Vec_PtrPush( vNodes, pNode ); + Vec_PtrPush( vNodes, pObj ); } /**Function************************************************************* @@ -69,8 +205,16 @@ Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk ) int i; Ntk_ManIncrementTravId( pNtk ); vNodes = Vec_PtrAlloc( 100 ); - Ntk_ManForEachPo( pNtk, pObj, i ) - Ntk_ManDfs_rec( pObj, vNodes ); + Ntk_ManForEachObj( pNtk, pObj, i ) + { + if ( Ntk_ObjIsCi(pObj) ) + { + Ntk_ObjSetTravIdCurrent( pObj ); + Vec_PtrPush( vNodes, pObj ); + } + else if ( Ntk_ObjIsCo(pObj) ) + Ntk_ManDfs_rec( pObj, vNodes ); + } return vNodes; } @@ -85,16 +229,35 @@ Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Ntk_ManDfsReverse_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes ) +void Ntk_ManDfsReverse_rec( Ntk_Obj_t * pObj, Vec_Ptr_t * vNodes ) { Ntk_Obj_t * pNext; - int i; - if ( Ntk_ObjIsTravIdCurrent( pNode ) ) + int i, iBox, iTerm1, nTerms; + if ( Ntk_ObjIsTravIdCurrent( pObj ) ) return; - Ntk_ObjSetTravIdCurrent( pNode ); - Ntk_ObjForEachFanout( pNode, pNext, i ) - Ntk_ManDfsReverse_rec( pNext, vNodes ); - Vec_PtrPush( vNodes, pNode ); + Ntk_ObjSetTravIdCurrent( pObj ); + if ( Ntk_ObjIsCo(pObj) ) + { + iBox = Tim_ManBoxForCo( pObj->pMan->pManTime, pObj->PioId ); + if ( iBox >= 0 ) // this is not a true PO + { + iTerm1 = Tim_ManBoxOutputFirst( pObj->pMan->pManTime, iBox ); + nTerms = Tim_ManBoxOutputNum( pObj->pMan->pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pNext = Ntk_ManCi(pObj->pMan, iTerm1 + i); + Ntk_ManDfsReverse_rec( pNext, vNodes ); + } + } + } + else if ( Ntk_ObjIsNode(pObj) || Ntk_ObjIsCi(pObj) ) + { + Ntk_ObjForEachFanout( pObj, pNext, i ) + Ntk_ManDfsReverse_rec( pNext, vNodes ); + } + else + assert( 0 ); + Vec_PtrPush( vNodes, pObj ); } /**Function************************************************************* diff --git a/src/aig/ntk/ntkFanio.c b/src/aig/ntk/ntkFanio.c index 73019231..135929af 100644 --- a/src/aig/ntk/ntkFanio.c +++ b/src/aig/ntk/ntkFanio.c @@ -279,7 +279,7 @@ void Ntk_ObjTransferFanout( Ntk_Obj_t * pNodeFrom, Ntk_Obj_t * pNodeTo ) Vec_Ptr_t * vFanouts = pNodeFrom->pMan->vTemp; Ntk_Obj_t * pTemp; int nFanoutsOld, i; - assert( !Ntk_ObjIsPo(pNodeFrom) && !Ntk_ObjIsPo(pNodeTo) ); + assert( !Ntk_ObjIsCo(pNodeFrom) && !Ntk_ObjIsCo(pNodeTo) ); assert( pNodeFrom->pMan == pNodeTo->pMan ); assert( pNodeFrom != pNodeTo ); assert( Ntk_ObjFanoutNum(pNodeFrom) > 0 ); diff --git a/src/aig/ntk/ntkMan.c b/src/aig/ntk/ntkMan.c index e302a98c..1a077495 100644 --- a/src/aig/ntk/ntkMan.c +++ b/src/aig/ntk/ntkMan.c @@ -50,6 +50,7 @@ Ntk_Man_t * Ntk_ManAlloc() p->vTemp = Vec_PtrAlloc( 1000 ); p->nFanioPlus = 4; p->pMemObjs = Aig_MmFlexStart(); + p->pManHop = Hop_ManStart(); return p; } @@ -72,9 +73,9 @@ void Ntk_ManFree( Ntk_Man_t * p ) if ( p->vCos ) Vec_PtrFree( p->vCos ); if ( p->vObjs ) Vec_PtrFree( p->vObjs ); if ( p->vTemp ) Vec_PtrFree( p->vTemp ); - if ( p->pAig ) Aig_ManStop( p->pAig ); if ( p->pManTime ) Tim_ManStop( p->pManTime ); if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 ); + if ( p->pManHop ) Hop_ManStop( p->pManHop ); free( p ); } @@ -89,7 +90,7 @@ void Ntk_ManFree( Ntk_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Ntk_ManPrintStats( Ntk_Man_t * p ) +void Ntk_ManPrintStats( Ntk_Man_t * p, If_Lib_t * pLutLib ) { printf( "%-15s : ", p->pName ); printf( "pi = %5d ", Ntk_ManPiNum(p) ); @@ -97,10 +98,15 @@ void Ntk_ManPrintStats( Ntk_Man_t * p ) printf( "ci = %5d ", Ntk_ManCiNum(p) ); printf( "co = %5d ", Ntk_ManCoNum(p) ); printf( "lat = %5d ", Ntk_ManLatchNum(p) ); - printf( "box = %5d ", Ntk_ManBoxNum(p) ); +// printf( "box = %5d ", Ntk_ManBoxNum(p) ); printf( "node = %5d ", Ntk_ManNodeNum(p) ); - printf( "aig = %6d ", Aig_ManNodeNum(p->pAig) ); + printf( "aig = %6d ", Ntk_ManGetAigNodeNum(p) ); + printf( "lev = %3d ", Ntk_ManLevel(p) ); + printf( "lev2 = %3d ", Ntk_ManLevel2(p) ); + printf( "delay = %5.2f", Ntk_ManDelayTraceLut(p, pLutLib) ); printf( "\n" ); + + Ntk_ManDelayTracePrint( p, pLutLib ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntk/ntkMap.c b/src/aig/ntk/ntkMap.c index 7700fc63..9c780498 100644 --- a/src/aig/ntk/ntkMap.c +++ b/src/aig/ntk/ntkMap.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "ntk.h" +#include "if.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -30,6 +31,209 @@ /**Function************************************************************* + Synopsis [Load the network into FPGA manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntk_ManSetIfParsDefault( If_Par_t * pPars ) +{ +// extern void * Abc_FrameReadLibLut(); + // set defaults + memset( pPars, 0, sizeof(If_Par_t) ); + // user-controlable paramters +// pPars->nLutSize = -1; + pPars->nLutSize = 6; + pPars->nCutsMax = 8; + pPars->nFlowIters = 1; + pPars->nAreaIters = 2; + pPars->DelayTarget = -1; + pPars->Epsilon = (float)0.01; + pPars->fPreprocess = 1; + pPars->fArea = 0; + pPars->fFancy = 0; + pPars->fExpRed = 0; + pPars->fLatchPaths = 0; + pPars->fEdge = 1; + pPars->fCutMin = 1; + pPars->fSeqMap = 0; + pPars->fVerbose = 1; + // internal parameters + pPars->fTruth = 0; + pPars->nLatches = 0; + pPars->fLiftLeaves = 0; +// pPars->pLutLib = Abc_FrameReadLibLut(); + pPars->pLutLib = NULL; + pPars->pTimesArr = NULL; + pPars->pTimesArr = NULL; + pPars->pFuncCost = NULL; +/* + if ( pPars->nLutSize == -1 ) + { + if ( pPars->pLutLib == NULL ) + { + printf( "The LUT library is not given.\n" ); + return; + } + // get LUT size from the library + pPars->nLutSize = pPars->pLutLib->LutMax; + } +*/ +} + +/**Function************************************************************* + + Synopsis [Load the network into FPGA manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars ) +{ + If_Man_t * pIfMan; + Aig_Obj_t * pNode;//, * pFanin, * pPrev; + int i; + // start the mapping manager and set its parameters + pIfMan = If_ManStart( pPars ); + // print warning about excessive memory usage +// if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 ) +// printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", +// 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) ); + // load the AIG into the mapper + Aig_ManForEachObj( p, pNode, i ) + { + if ( Aig_ObjIsAnd(pNode) ) + pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, + If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), + If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) ); + else if ( Aig_ObjIsPi(pNode) ) + { + pNode->pData = If_ManCreateCi( pIfMan ); + ((If_Obj_t *)pNode->pData)->Level = pNode->Level; + if ( pIfMan->nLevelMax < (int)pNode->Level ) + pIfMan->nLevelMax = (int)pNode->Level; + } + else if ( Aig_ObjIsPo(pNode) ) + pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) ); + else if ( Aig_ObjIsConst1(pNode) ) + Aig_ManConst1(p)->pData = If_ManConst1( pIfMan ); + else // add the node to the mapper + assert( 0 ); + // set up the choice node +// if ( Aig_AigNodeIsChoice( pNode ) ) +// { +// pIfMan->nChoices++; +// for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData ) +// If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData ); +// If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData ); +// } + { + If_Obj_t * pIfObj = pNode->pData; + assert( !If_IsComplement(pIfObj) ); + assert( pIfObj->Id == pNode->Id ); + } + } + return pIfMan; +} + + +/**Function************************************************************* + + Synopsis [Recursively derives the truth table for the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Ntk_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited ) +{ + If_Cut_t * pCut; + If_Obj_t * pTemp; + Hop_Obj_t * gFunc, * gFunc0, * gFunc1; + // get the best cut + pCut = If_ObjCutBest(pIfObj); + // if the cut is visited, return the result + if ( If_CutData(pCut) ) + return If_CutData(pCut); + // mark the node as visited + Vec_PtrPush( vVisited, pCut ); + // insert the worst case + If_CutSetData( pCut, (void *)1 ); + // skip in case of primary input + if ( If_ObjIsCi(pIfObj) ) + return If_CutData(pCut); + // compute the functions of the children + for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv ) + { + gFunc0 = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin0, vVisited ); + if ( gFunc0 == (void *)1 ) + continue; + gFunc1 = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin1, vVisited ); + if ( gFunc1 == (void *)1 ) + continue; + // both branches are solved + gFunc = Hop_And( pHopMan, Hop_NotCond(gFunc0, pTemp->fCompl0), Hop_NotCond(gFunc1, pTemp->fCompl1) ); + if ( pTemp->fPhase != pIfObj->fPhase ) + gFunc = Hop_Not(gFunc); + If_CutSetData( pCut, gFunc ); + break; + } + return If_CutData(pCut); +} + +/**Function************************************************************* + + Synopsis [Derives the truth table for one cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Ntk_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj ) +{ + If_Cut_t * pCut; + Hop_Obj_t * gFunc; + If_Obj_t * pLeaf; + int i; + // get the best cut + pCut = If_ObjCutBest(pIfObj); + assert( pCut->nLeaves > 1 ); + // set the leaf variables + If_CutForEachLeaf( pIfMan, pCut, pLeaf, i ) + If_CutSetData( If_ObjCutBest(pLeaf), Hop_IthVar(pHopMan, i) ); + // recursively compute the function while collecting visited cuts + Vec_PtrClear( pIfMan->vTemp ); + gFunc = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); + if ( gFunc == (void *)1 ) + { + printf( "Ntk_NodeIfToHop(): Computing local AIG has failed.\n" ); + return NULL; + } +// printf( "%d ", Vec_PtrSize(p->vTemp) ); + // clean the cuts + If_CutForEachLeaf( pIfMan, pCut, pLeaf, i ) + If_CutSetData( If_ObjCutBest(pLeaf), NULL ); + Vec_PtrForEachEntry( pIfMan->vTemp, pCut, i ) + If_CutSetData( pCut, NULL ); + return gFunc; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -39,6 +243,95 @@ SeeAlso [] ***********************************************************************/ +Ntk_Man_t * Ntk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p ) +{ + Ntk_Man_t * pNtk; + Ntk_Obj_t * pObjNew; + Aig_Obj_t * pObj; + If_Obj_t * pIfObj; + If_Cut_t * pCutBest; + int i, k, nLeaves, * ppLeaves; + assert( Aig_ManPiNum(p) == If_ManCiNum(pIfMan) ); + assert( Aig_ManPoNum(p) == If_ManCoNum(pIfMan) ); + assert( Aig_ManNodeNum(p) == If_ManAndNum(pIfMan) ); + If_ManCleanCutData( pIfMan ); + // construct the network + pNtk = Ntk_ManAlloc(); + pNtk->pName = Aig_UtilStrsav( p->pName ); + pNtk->pSpec = Aig_UtilStrsav( p->pSpec ); + Aig_ManForEachObj( p, pObj, i ) + { + pIfObj = If_ManObj( pIfMan, i ); + if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) ) + continue; + if ( Aig_ObjIsNode(pObj) ) + { + pCutBest = If_ObjCutBest( pIfObj ); + nLeaves = If_CutLeaveNum( pCutBest ); + ppLeaves = If_CutLeaves( pCutBest ); + // create node + pObjNew = Ntk_ManCreateNode( pNtk, nLeaves, pIfObj->nRefs ); + for ( k = 0; k < nLeaves; k++ ) + Ntk_ObjAddFanin( pObjNew, Aig_ManObj(p, ppLeaves[k])->pData ); + // get the functionality + pObjNew->pFunc = Ntk_NodeIfToHop( pNtk->pManHop, pIfMan, pIfObj ); + } + else if ( Aig_ObjIsPi(pObj) ) + pObjNew = Ntk_ManCreateCi( pNtk, pIfObj->nRefs ); + else if ( Aig_ObjIsPo(pObj) ) + { + pObjNew = Ntk_ManCreateCo( pNtk ); + pObjNew->fCompl = Aig_ObjFaninC0(pObj); + Ntk_ObjAddFanin( pObjNew, Aig_ObjFanin0(pObj)->pData ); + } + else if ( Aig_ObjIsConst1(pObj) ) + { + pObjNew = Ntk_ManCreateNode( pNtk, 0, pIfObj->nRefs ); + pObjNew->pFunc = Hop_ManConst1( pNtk->pManHop ); + } + else + assert( 0 ); + pObj->pData = pObjNew; + } + pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 ); + return pNtk; +} + +/**Function************************************************************* + + Synopsis [Interface with the FPGA mapping package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntk_Man_t * Ntk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars ) +{ + Ntk_Man_t * pNtk; + If_Man_t * pIfMan; + // perform FPGA mapping + // set the arrival times + pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) ); + memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) ); + // translate into the mapper + pIfMan = Ntk_ManToIf( p, pPars ); + if ( pIfMan == NULL ) + return NULL; + pIfMan->pManTim = Tim_ManDup( pManTime, 0 ); + if ( !If_ManPerformMapping( pIfMan ) ) + { + If_ManStop( pIfMan ); + return NULL; + } + // transform the result of mapping into the new network + pNtk = Ntk_ManFromIf( pIfMan, p ); + If_ManStop( pIfMan ); + return pNtk; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/ntk/ntkObj.c b/src/aig/ntk/ntkObj.c index 259ed79d..7bd2f552 100644 --- a/src/aig/ntk/ntkObj.c +++ b/src/aig/ntk/ntkObj.c @@ -63,10 +63,11 @@ Ntk_Obj_t * Ntk_ManCreateObj( Ntk_Man_t * p, int nFanins, int nFanouts ) SeeAlso [] ***********************************************************************/ -Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * p ) +Ntk_Obj_t * Ntk_ManCreateCi( Ntk_Man_t * p, int nFanouts ) { Ntk_Obj_t * pObj; - pObj = Ntk_ManCreateObj( p, 1, 1 ); + pObj = Ntk_ManCreateObj( p, 1, nFanouts ); + pObj->PioId = Vec_PtrSize( p->vCis ); Vec_PtrPush( p->vCis, pObj ); pObj->Type = NTK_OBJ_CI; p->nObjs[NTK_OBJ_CI]++; @@ -84,10 +85,11 @@ Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * p ) SeeAlso [] ***********************************************************************/ -Ntk_Obj_t * Ntk_ManCreatePo( Ntk_Man_t * p ) +Ntk_Obj_t * Ntk_ManCreateCo( Ntk_Man_t * p ) { Ntk_Obj_t * pObj; pObj = Ntk_ManCreateObj( p, 1, 1 ); + pObj->PioId = Vec_PtrSize( p->vCos ); Vec_PtrPush( p->vCos, pObj ); pObj->Type = NTK_OBJ_CO; p->nObjs[NTK_OBJ_CO]++; @@ -200,7 +202,7 @@ void Ntk_ManDeleteNode_rec( Ntk_Obj_t * pObj ) { Vec_Ptr_t * vNodes; int i; - assert( !Ntk_ObjIsPi(pObj) ); + assert( !Ntk_ObjIsCi(pObj) ); assert( Ntk_ObjFanoutNum(pObj) == 0 ); vNodes = Vec_PtrAlloc( 100 ); Ntk_ObjCollectFanins( pObj, vNodes ); diff --git a/src/aig/ntk/ntkTiming.c b/src/aig/ntk/ntkTiming.c index f57c7987..ff867e02 100644 --- a/src/aig/ntk/ntkTiming.c +++ b/src/aig/ntk/ntkTiming.c @@ -19,7 +19,6 @@ ***********************************************************************/ #include "ntk.h" -#include "if.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -108,19 +107,17 @@ void Ntk_ManDelayTraceSortPins( Ntk_Obj_t * pNode, int * pPinPerm, float * pPinD SeeAlso [] ***********************************************************************/ -float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib ) +float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, If_Lib_t * pLutLib ) { int fUseSorting = 1; int pPinPerm[32]; float pPinDelays[32]; - If_Lib_t * pLutLib; - Ntk_Obj_t * pNode, * pFanin; + Ntk_Obj_t * pObj, * pFanin; Vec_Ptr_t * vNodes; float tArrival, tRequired, tSlack, * pDelays; int i, k; // get the library - pLutLib = fUseLutLib? Abc_FrameReadLibLut() : NULL; if ( pLutLib && pLutLib->LutMax < Ntk_ManGetFaninMax(pNtk) ) { printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", @@ -128,107 +125,138 @@ float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib ) return -AIG_INFINITY; } + // compute the reverse order of all objects + vNodes = Ntk_ManDfsReverse( pNtk ); + // initialize the arrival times Abc_NtkPrepareTiming( pNtk ); // propagate arrival times - vNodes = Ntk_ManDfs( pNtk ); - Vec_PtrForEachEntry( vNodes, pNode, i ) + Tim_ManIncrementTravId( pNtk->pManTime ); + Ntk_ManForEachObj( pNtk, pObj, i ) { - tArrival = -AIG_INFINITY; - if ( pLutLib == NULL ) - { - Ntk_ObjForEachFanin( pNode, pFanin, k ) - if ( tArrival < Ntk_ObjArrival(pFanin) + 1.0 ) - tArrival = Ntk_ObjArrival(pFanin) + 1.0; - } - else if ( !pLutLib->fVarPinDelays ) + if ( Ntk_ObjIsNode(pObj) ) { - pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)]; - Ntk_ObjForEachFanin( pNode, pFanin, k ) - if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[0] ) - tArrival = Ntk_ObjArrival(pFanin) + pDelays[0]; - } - else - { - pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)]; - if ( fUseSorting ) + tArrival = -AIG_INFINITY; + if ( pLutLib == NULL ) { - Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays ); - Ntk_ObjForEachFanin( pNode, pFanin, k ) - if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] ) - tArrival = Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k]; + Ntk_ObjForEachFanin( pObj, pFanin, k ) + if ( tArrival < Ntk_ObjArrival(pFanin) + 1.0 ) + tArrival = Ntk_ObjArrival(pFanin) + 1.0; + } + else if ( !pLutLib->fVarPinDelays ) + { + pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)]; + Ntk_ObjForEachFanin( pObj, pFanin, k ) + if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[0] ) + tArrival = Ntk_ObjArrival(pFanin) + pDelays[0]; } else { - Ntk_ObjForEachFanin( pNode, pFanin, k ) - if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[k] ) - tArrival = Ntk_ObjArrival(pFanin) + pDelays[k]; + pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)]; + if ( fUseSorting ) + { + Ntk_ManDelayTraceSortPins( pObj, pPinPerm, pPinDelays ); + Ntk_ObjForEachFanin( pObj, pFanin, k ) + if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin(pObj,pPinPerm[k])) + pDelays[k] ) + tArrival = Ntk_ObjArrival(Ntk_ObjFanin(pObj,pPinPerm[k])) + pDelays[k]; + } + else + { + Ntk_ObjForEachFanin( pObj, pFanin, k ) + if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[k] ) + tArrival = Ntk_ObjArrival(pFanin) + pDelays[k]; + } } + if ( Ntk_ObjFaninNum(pObj) == 0 ) + tArrival = 0.0; } - if ( Ntk_ObjFaninNum(pNode) == 0 ) - tArrival = 0.0; - Ntk_ObjSetArrival( pNode, tArrival ); + else if ( Ntk_ObjIsCi(pObj) ) + { + tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId ); + } + else if ( Ntk_ObjIsCo(pObj) ) + { + tArrival = Ntk_ObjArrival( Ntk_ObjFanin0(pObj) ); + Tim_ManSetPoArrival( pNtk->pManTime, pObj->PioId, tArrival ); + } + else + assert( 0 ); + Ntk_ObjSetArrival( pObj, tArrival ); } - Vec_PtrFree( vNodes ); // get the latest arrival times tArrival = -AIG_INFINITY; - Ntk_ManForEachPo( pNtk, pNode, i ) - if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin0(pNode)) ) - tArrival = Ntk_ObjArrival(Ntk_ObjFanin0(pNode)); + Ntk_ManForEachPo( pNtk, pObj, i ) + if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin0(pObj)) ) + tArrival = Ntk_ObjArrival(Ntk_ObjFanin0(pObj)); // initialize the required times - Ntk_ManForEachPo( pNtk, pNode, i ) - if ( Ntk_ObjRequired(Ntk_ObjFanin0(pNode)) > tArrival ) - Ntk_ObjSetRequired( Ntk_ObjFanin0(pNode), tArrival ); + Ntk_ManForEachPo( pNtk, pObj, i ) + if ( Ntk_ObjRequired(Ntk_ObjFanin0(pObj)) > tArrival ) + Ntk_ObjSetRequired( Ntk_ObjFanin0(pObj), tArrival ); // propagate the required times - vNodes = Ntk_ManDfsReverse( pNtk ); - Vec_PtrForEachEntry( vNodes, pNode, i ) + Tim_ManIncrementTravId( pNtk->pManTime ); + Vec_PtrForEachEntry( vNodes, pObj, i ) { - if ( pLutLib == NULL ) - { - tRequired = Ntk_ObjRequired(pNode) - (float)1.0; - Ntk_ObjForEachFanin( pNode, pFanin, k ) - if ( Ntk_ObjRequired(pFanin) > tRequired ) - Ntk_ObjSetRequired( pFanin, tRequired ); - } - else if ( !pLutLib->fVarPinDelays ) - { - pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)]; - tRequired = Ntk_ObjRequired(pNode) - pDelays[0]; - Ntk_ObjForEachFanin( pNode, pFanin, k ) - if ( Ntk_ObjRequired(pFanin) > tRequired ) - Ntk_ObjSetRequired( pFanin, tRequired ); - } - else + if ( Ntk_ObjIsNode(pObj) ) { - pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)]; - if ( fUseSorting ) + if ( pLutLib == NULL ) { - Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays ); - Ntk_ObjForEachFanin( pNode, pFanin, k ) - { - tRequired = Ntk_ObjRequired(pNode) - pDelays[k]; - if ( Ntk_ObjRequired(Ntk_ObjFanin(pNode,pPinPerm[k])) > tRequired ) - Ntk_ObjSetRequired( Ntk_ObjFanin(pNode,pPinPerm[k]), tRequired ); - } + tRequired = Ntk_ObjRequired(pObj) - (float)1.0; + Ntk_ObjForEachFanin( pObj, pFanin, k ) + if ( Ntk_ObjRequired(pFanin) > tRequired ) + Ntk_ObjSetRequired( pFanin, tRequired ); } - else + else if ( !pLutLib->fVarPinDelays ) { - Ntk_ObjForEachFanin( pNode, pFanin, k ) - { - tRequired = Ntk_ObjRequired(pNode) - pDelays[k]; + pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)]; + tRequired = Ntk_ObjRequired(pObj) - pDelays[0]; + Ntk_ObjForEachFanin( pObj, pFanin, k ) if ( Ntk_ObjRequired(pFanin) > tRequired ) Ntk_ObjSetRequired( pFanin, tRequired ); + } + else + { + pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)]; + if ( fUseSorting ) + { + Ntk_ManDelayTraceSortPins( pObj, pPinPerm, pPinDelays ); + Ntk_ObjForEachFanin( pObj, pFanin, k ) + { + tRequired = Ntk_ObjRequired(pObj) - pDelays[k]; + if ( Ntk_ObjRequired(Ntk_ObjFanin(pObj,pPinPerm[k])) > tRequired ) + Ntk_ObjSetRequired( Ntk_ObjFanin(pObj,pPinPerm[k]), tRequired ); + } + } + else + { + Ntk_ObjForEachFanin( pObj, pFanin, k ) + { + tRequired = Ntk_ObjRequired(pObj) - pDelays[k]; + if ( Ntk_ObjRequired(pFanin) > tRequired ) + Ntk_ObjSetRequired( pFanin, tRequired ); + } } } } + else if ( Ntk_ObjIsCi(pObj) ) + { + tRequired = Ntk_ObjRequired(pObj); + Tim_ManSetPiRequired( pNtk->pManTime, pObj->PioId, tRequired ); + } + else if ( Ntk_ObjIsCo(pObj) ) + { + tRequired = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId ); + if ( Ntk_ObjRequired(Ntk_ObjFanin0(pObj)) > tRequired ) + Ntk_ObjSetRequired( Ntk_ObjFanin0(pObj), tRequired ); + } + // set slack for this object - tSlack = Ntk_ObjRequired(pNode) - Ntk_ObjArrival(pNode); + tSlack = Ntk_ObjRequired(pObj) - Ntk_ObjArrival(pObj); assert( tSlack + 0.001 > 0.0 ); - Ntk_ObjSetSlack( pNode, tSlack < 0.0 ? 0.0 : tSlack ); + Ntk_ObjSetSlack( pObj, tSlack < 0.0 ? 0.0 : tSlack ); } Vec_PtrFree( vNodes ); return tArrival; @@ -236,52 +264,6 @@ float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib ) /**Function************************************************************* - Synopsis [Determines timing-critical edges of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned Ntk_ManDelayTraceTCEdges( Ntk_Man_t * pNtk, Ntk_Obj_t * pNode, float tDelta, int fUseLutLib ) -{ - int pPinPerm[32]; - float pPinDelays[32]; - If_Lib_t * pLutLib; - Ntk_Obj_t * pFanin; - unsigned uResult = 0; - float tRequired, * pDelays; - int k; - pLutLib = fUseLutLib? Abc_FrameReadLibLut() : NULL; - tRequired = Ntk_ObjRequired(pNode); - if ( pLutLib == NULL ) - { - Ntk_ObjForEachFanin( pNode, pFanin, k ) - if ( tRequired < Ntk_ObjArrival(pFanin) + 1.0 + tDelta ) - uResult |= (1 << k); - } - else if ( !pLutLib->fVarPinDelays ) - { - pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)]; - Ntk_ObjForEachFanin( pNode, pFanin, k ) - if ( tRequired < Ntk_ObjArrival(pFanin) + pDelays[0] + tDelta ) - uResult |= (1 << k); - } - else - { - pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)]; - Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays ); - Ntk_ObjForEachFanin( pNode, pFanin, k ) - if ( tRequired < Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] + tDelta ) - uResult |= (1 << pPinPerm[k]); - } - return uResult; -} - -/**Function************************************************************* - Synopsis [Delay tracing of the LUT mapped network.] Description [] @@ -291,14 +273,12 @@ unsigned Ntk_ManDelayTraceTCEdges( Ntk_Man_t * pNtk, Ntk_Obj_t * pNode, float tD SeeAlso [] ***********************************************************************/ -void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose ) +void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, If_Lib_t * pLutLib ) { Ntk_Obj_t * pNode; - If_Lib_t * pLutLib; int i, Nodes, * pCounters; float tArrival, tDelta, nSteps, Num; // get the library - pLutLib = fUseLutLib? Abc_FrameReadLibLut() : NULL; if ( pLutLib && pLutLib->LutMax < Ntk_ManGetFaninMax(pNtk) ) { printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", @@ -306,11 +286,11 @@ void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose ) return; } // decide how many steps - nSteps = fUseLutLib ? 20 : Ntk_ManLevel(pNtk); + nSteps = pLutLib ? 20 : Ntk_ManLevel(pNtk); pCounters = ALLOC( int, nSteps + 1 ); memset( pCounters, 0, sizeof(int)*(nSteps + 1) ); // perform delay trace - tArrival = Ntk_ManDelayTraceLut( pNtk, fUseLutLib ); + tArrival = Ntk_ManDelayTraceLut( pNtk, pLutLib ); tDelta = tArrival / nSteps; // count how many nodes have slack in the corresponding intervals Ntk_ManForEachNode( pNtk, pNode, i ) @@ -318,17 +298,19 @@ void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose ) if ( Ntk_ObjFaninNum(pNode) == 0 ) continue; Num = Ntk_ObjSlack(pNode) / tDelta; + if ( Num > nSteps ) + continue; assert( Num >=0 && Num <= nSteps ); pCounters[(int)Num]++; } // print the results - printf( "Max delay = %6.2f. Delay trace using %s model:\n", tArrival, fUseLutLib? "LUT library" : "unit-delay" ); + printf( "Max delay = %6.2f. Delay trace using %s model:\n", tArrival, pLutLib? "LUT library" : "unit-delay" ); Nodes = 0; for ( i = 0; i < nSteps; i++ ) { Nodes += pCounters[i]; - printf( "%3d %s : %5d (%6.2f %%)\n", fUseLutLib? 5*(i+1) : i+1, - fUseLutLib? "%":"lev", Nodes, 100.0*Nodes/Ntk_ManNodeNum(pNtk) ); + printf( "%3d %s : %5d (%6.2f %%)\n", pLutLib? 5*(i+1) : i+1, + pLutLib? "%":"lev", Nodes, 100.0*Nodes/Ntk_ManNodeNum(pNtk) ); } free( pCounters ); } diff --git a/src/aig/ntk/ntkUtil.c b/src/aig/ntk/ntkUtil.c index 543d1a60..931a26ee 100644 --- a/src/aig/ntk/ntkUtil.c +++ b/src/aig/ntk/ntkUtil.c @@ -95,36 +95,25 @@ int Ntk_ManGetTotalFanins( Ntk_Man_t * pNtk ) return nFanins; } + /**Function************************************************************* - Synopsis [Computes the number of logic levels not counting PIs/POs.] + Synopsis [] - Description [Assumes topological ordering of the nodes.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -int Ntk_ManLevel( Ntk_Man_t * pNtk ) +int Ntk_ManPiNum( Ntk_Man_t * pNtk ) { - Ntk_Obj_t * pObj, * pFanin; - int i, k, LevelMax; - Ntk_ManForEachPi( pNtk, pObj, i ) - Ntk_ObjSetLevel( pObj, 0 ); - Ntk_ManForEachNode( pNtk, pObj, i ) - { - LevelMax = 0; - Ntk_ObjForEachFanin( pObj, pFanin, k ) - if ( LevelMax < Ntk_ObjLevel(pFanin) ) - LevelMax = Ntk_ObjLevel(pFanin); - Ntk_ObjSetLevel( pFanin, LevelMax+1 ); - } - LevelMax = 0; - Ntk_ManForEachPo( pNtk, pObj, i ) - if ( LevelMax < Ntk_ObjLevel(pObj) ) - LevelMax = Ntk_ObjLevel(pObj); - return LevelMax; + Ntk_Obj_t * pNode; + int i, Counter = 0; + Ntk_ManForEachCi( pNtk, pNode, i ) + Counter += Ntk_ObjIsPi( pNode ); + return Counter; } /**Function************************************************************* @@ -138,18 +127,18 @@ int Ntk_ManLevel( Ntk_Man_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Ntk_ManPiNum( Ntk_Man_t * pNtk ) +int Ntk_ManPoNum( Ntk_Man_t * pNtk ) { Ntk_Obj_t * pNode; int i, Counter = 0; - Ntk_ManForEachPi( pNtk, pNode, i ) - Counter++; + Ntk_ManForEachCo( pNtk, pNode, i ) + Counter += Ntk_ObjIsPo( pNode ); return Counter; } /**Function************************************************************* - Synopsis [] + Synopsis [Reads the number of BDD nodes.] Description [] @@ -158,13 +147,22 @@ int Ntk_ManPiNum( Ntk_Man_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Ntk_ManPoNum( Ntk_Man_t * pNtk ) +int Ntk_ManGetAigNodeNum( Ntk_Man_t * pNtk ) { Ntk_Obj_t * pNode; - int i, Counter = 0; - Ntk_ManForEachPo( pNtk, pNode, i ) - Counter++; - return Counter; + int i, nNodes = 0; + Ntk_ManForEachNode( pNtk, pNode, i ) + { + if ( pNode->pFunc == NULL ) + { + printf( "Ntk_ManGetAigNodeNum(): Local AIG of node %d is not assigned.\n", pNode->Id ); + continue; + } + if ( Ntk_ObjFaninNum(pNode) < 2 ) + continue; + nNodes += Hop_DagSize( pNode->pFunc ); + } + return nNodes; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index caaa86f8..72a5674b 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -31,6 +31,7 @@ extern "C" { #include "aig.h" #include "tim.h" +#include "ntk.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -227,6 +228,7 @@ extern Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ); 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_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk ); /*=== ntlCheck.c ==========================================================*/ extern int Ntl_ManCheck( Ntl_Man_t * pMan ); extern int Ntl_ModelCheck( Ntl_Mod_t * pModel ); @@ -236,6 +238,7 @@ extern Ntl_Man_t * Ntl_ManAlloc( char * pFileName ); extern void Ntl_ManFree( 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 void Ntl_ModelFree( Ntl_Mod_t * p ); /*=== ntlMap.c ============================================================*/ diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index 72a8bc40..a54618e5 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -438,6 +438,8 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) // start the AIG manager assert( p->pAig == NULL ); p->pAig = Aig_ManStart( 10000 ); + p->pAig->pName = Aig_UtilStrsav( p->pName ); + p->pAig->pSpec = Aig_UtilStrsav( p->pSpec ); // get the root model pRoot = Vec_PtrEntry( p->vModels, 0 ); // collect primary inputs diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c index 971d1278..84a7af84 100644 --- a/src/aig/ntl/ntlInsert.c +++ b/src/aig/ntl/ntlInsert.c @@ -123,6 +123,105 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ) return 1; } +/**Function************************************************************* + + Synopsis [Inserts the given mapping into the netlist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk ) +{ + char Buffer[100]; + Vec_Int_t * vTruth; + Vec_Int_t * vCover; + Ntl_Mod_t * pRoot; + Ntl_Obj_t * pNode; + Ntl_Net_t * pNet, * pNetCo; + Ntk_Obj_t * pObj, * pFanin; + int i, k, nDigits; + unsigned * pTruth; + assert( Vec_PtrSize(p->vCis) == Ntk_ManCiNum(pNtk) ); + assert( Vec_PtrSize(p->vCos) == Ntk_ManCoNum(pNtk) ); + // set the correspondence between the PI/PO nodes + Ntl_ManForEachCiNet( p, pNet, i ) + Ntk_ManCi( pNtk, i )->pCopy = pNet; +// Ntl_ManForEachCoNet( p, pNet, i ) +// Ntk_ManCo( pNtk, i )->pCopy = pNet; + // remove old nodes + pRoot = Vec_PtrEntry( p->vModels, 0 ); + Ntl_ModelForEachNode( pRoot, pNode, i ) + Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL ); + // create a new node for each LUT + vTruth = Vec_IntAlloc( 1 << 16 ); + vCover = Vec_IntAlloc( 1 << 16 ); + nDigits = Aig_Base10Log( Ntk_ManNodeNum(pNtk) ); + Ntk_ManForEachNode( pNtk, pObj, i ) + { + pNode = Ntl_ModelCreateNode( pRoot, Ntk_ObjFaninNum(pObj) ); + pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, pObj->pFunc, Ntk_ObjFaninNum(pObj), vTruth, 0 ); + pNode->pSop = Ntl_SopFromTruth( p, pTruth, Ntk_ObjFaninNum(pObj), vCover ); + if ( !Kit_TruthIsConst0(pTruth, Ntk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Ntk_ObjFaninNum(pObj)) ) + { + Ntk_ObjForEachFanin( pObj, pFanin, k ) + { + pNet = pFanin->pCopy; + if ( pNet == NULL ) + { + printf( "Ntl_ManInsert(): Internal error: Net not found.\n" ); + return 0; + } + Ntl_ObjSetFanin( pNode, pNet, k ); + } + } + 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" ); + return 0; + } + pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer ); + if ( !Ntl_ModelSetNetDriver( pNode, pNet ) ) + { + printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" ); + return 0; + } + pObj->pCopy = pNet; + } + Vec_IntFree( vCover ); + Vec_IntFree( vTruth ); + // mark CIs and outputs of the registers + Ntl_ManForEachCiNet( p, pNetCo, i ) + pNetCo->nVisits = 101; + // update the CO pointers + Ntl_ManForEachCoNet( p, pNetCo, i ) + { + if ( pNetCo->nVisits == 101 ) + continue; + pNetCo->nVisits = 101; + // get the corresponding PO and its driver + pObj = Ntk_ManCo( pNtk, i ); + pFanin = Ntk_ObjFanin0( pObj ); + // get the net driving the driver + pNet = pFanin->pCopy; //Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id ); + pNode = Ntl_ModelCreateNode( pRoot, 1 ); + pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pFunc)*/? 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; + if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) ) + { + printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" ); + return 0; + } + } + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c index b5331ae2..9614a423 100644 --- a/src/aig/ntl/ntlMan.c +++ b/src/aig/ntl/ntlMan.c @@ -139,6 +139,22 @@ void Ntl_ManPrintStats( Ntl_Man_t * p ) /**Function************************************************************* + Synopsis [Deallocates the netlist manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p ) +{ + return p->pManTime; +} + +/**Function************************************************************* + Synopsis [Allocates the model.] Description [] diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c index 3de74200..20bc79cf 100644 --- a/src/aig/ntl/ntlMap.c +++ b/src/aig/ntl/ntlMap.c @@ -117,7 +117,7 @@ Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Ntk_ManSetIfParsDefault( If_Par_t * pPars ) +void Ntl_ManSetIfParsDefault( If_Par_t * pPars ) { // extern void * Abc_FrameReadLibLut(); // set defaults @@ -162,57 +162,6 @@ void Ntk_ManSetIfParsDefault( If_Par_t * pPars ) */ } -/**Function************************************************************* - - Synopsis [Load the network into FPGA manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -If_Man_t * Ntk_ManToIf_old( Aig_Man_t * p, If_Par_t * pPars ) -{ - If_Man_t * pIfMan; - Aig_Obj_t * pNode;//, * pFanin, * pPrev; - Vec_Ptr_t * vNodes; - int i; - // start the mapping manager and set its parameters - pIfMan = If_ManStart( pPars ); - // print warning about excessive memory usage - if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 ) - printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", - 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) ); - // load the AIG into the mapper - vNodes = Aig_ManDfsPio( p ); - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - if ( Aig_ObjIsAnd(pNode) ) - pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, - If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), - If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) ); - else if ( Aig_ObjIsPi(pNode) ) - pNode->pData = If_ManCreateCi( pIfMan ); - else if ( Aig_ObjIsPo(pNode) ) - If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) ); - else if ( Aig_ObjIsConst1(pNode) ) - Aig_ManConst1(p)->pData = If_ManConst1( pIfMan ); - else // add the node to the mapper - assert( 0 ); - // set up the choice node -// if ( Aig_AigNodeIsChoice( pNode ) ) -// { -// pIfMan->nChoices++; -// for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData ) -// If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData ); -// If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData ); -// } - } - Vec_PtrFree( vNodes ); - return pIfMan; -} /**Function************************************************************* @@ -225,7 +174,7 @@ If_Man_t * Ntk_ManToIf_old( Aig_Man_t * p, If_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars ) +If_Man_t * Ntl_ManToIf( Aig_Man_t * p, If_Par_t * pPars ) { If_Man_t * pIfMan; Aig_Obj_t * pNode;//, * pFanin, * pPrev; @@ -251,7 +200,7 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars ) pIfMan->nLevelMax = (int)pNode->Level; } else if ( Aig_ObjIsPo(pNode) ) - If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) ); + pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) ); else if ( Aig_ObjIsConst1(pNode) ) Aig_ManConst1(p)->pData = If_ManConst1( pIfMan ); else // add the node to the mapper @@ -264,6 +213,11 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars ) // If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData ); // If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData ); // } + { + If_Obj_t * pIfObj = pNode->pData; + assert( !If_IsComplement(pIfObj) ); + assert( pIfObj->Id == pNode->Id ); + } } return pIfMan; } @@ -279,7 +233,7 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan ) +Vec_Ptr_t * Ntl_ManFromIf( Aig_Man_t * p, If_Man_t * pMan ) { Vec_Ptr_t * vIfMap; If_Obj_t * pNode, * pLeaf; @@ -356,12 +310,12 @@ Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p ) If_Par_t Pars, * pPars = &Pars; If_Man_t * pIfMan; // perform FPGA mapping - Ntk_ManSetIfParsDefault( pPars ); + Ntl_ManSetIfParsDefault( pPars ); // set the arrival times pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) ); memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) ); // translate into the mapper - pIfMan = Ntk_ManToIf( p, pPars ); + pIfMan = Ntl_ManToIf( p, pPars ); if ( pIfMan == NULL ) return NULL; pIfMan->pManTim = Tim_ManDup( pMan->pManTime, 0 ); @@ -371,7 +325,7 @@ Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p ) return NULL; } // transform the result of mapping into the new network - vMapping = Ntk_ManFromIf( p, pIfMan ); + vMapping = Ntl_ManFromIf( p, pIfMan ); If_ManStop( pIfMan ); if ( vMapping == NULL ) return NULL; diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c index a71e1497..77967ef6 100644 --- a/src/aig/tim/tim.c +++ b/src/aig/tim/tim.c @@ -150,7 +150,8 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos ) Synopsis [Duplicates the timing manager.] - Description [] + Description [Derives discrete-delay-model timing manager. + Useful for AIG optimization with approximate timing information.] SideEffects [] @@ -171,16 +172,21 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete ) for ( k = 0; k < p->nPos; k++ ) pNew->pPos[k].TravId = 0; if ( fDiscrete ) + { for ( k = 0; k < p->nPis; k++ ) pNew->pPis[k].timeArr = 0.0; // modify here + // modify the required times + } pNew->vDelayTables = Vec_PtrAlloc( 100 ); Tim_ManForEachBox( p, pBox, i ) { pDelayTableNew = ALLOC( float, pBox->nInputs * pBox->nOutputs ); Vec_PtrPush( pNew->vDelayTables, pDelayTableNew ); if ( fDiscrete ) + { for ( k = 0; k < pBox->nInputs * pBox->nOutputs; k++ ) pDelayTableNew[k] = 1.0; // modify here + } else memcpy( pDelayTableNew, pBox->pDelayTable, sizeof(float) * pBox->nInputs * pBox->nOutputs ); Tim_ManCreateBoxFirst( pNew, pBox->Inouts[0], pBox->nInputs, @@ -191,6 +197,47 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete ) /**Function************************************************************* + Synopsis [Duplicates the timing manager.] + + Description [Derives unit-delay-model timing manager. + Useful for levelizing the network.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Tim_Man_t * Tim_ManDupUnit( Tim_Man_t * p ) +{ + Tim_Man_t * pNew; + Tim_Box_t * pBox; + float * pDelayTableNew; + int i, k; + pNew = Tim_ManStart( p->nPis, p->nPos ); + memcpy( pNew->pPis, p->pPis, sizeof(Tim_Obj_t) * p->nPis ); + memcpy( pNew->pPos, p->pPos, sizeof(Tim_Obj_t) * p->nPos ); + for ( k = 0; k < p->nPis; k++ ) + { + pNew->pPis[k].TravId = 0; + pNew->pPis[k].timeArr = 0.0; + } + for ( k = 0; k < p->nPos; k++ ) + pNew->pPos[k].TravId = 0; + pNew->vDelayTables = Vec_PtrAlloc( 100 ); + Tim_ManForEachBox( p, pBox, i ) + { + pDelayTableNew = ALLOC( float, pBox->nInputs * pBox->nOutputs ); + Vec_PtrPush( pNew->vDelayTables, pDelayTableNew ); + for ( k = 0; k < pBox->nInputs * pBox->nOutputs; k++ ) + pDelayTableNew[k] = 1.0; + Tim_ManCreateBoxFirst( pNew, pBox->Inouts[0], pBox->nInputs, + pBox->Inouts[pBox->nInputs], pBox->nOutputs, pDelayTableNew ); + } + return pNew; +} + +/**Function************************************************************* + Synopsis [Stops the timing manager.] Description [] @@ -567,6 +614,110 @@ float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo ) return pObjThis->timeReq; } +/**Function************************************************************* + + Synopsis [Returns the box number for the given input.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Tim_ManBoxForCi( Tim_Man_t * p, int iCi ) +{ + if ( iCi >= p->nPis ) + return -1; + return p->pPis[iCi].iObj2Box; +} + +/**Function************************************************************* + + Synopsis [Returns the box number for the given output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Tim_ManBoxForCo( Tim_Man_t * p, int iCo ) +{ + if ( iCo >= p->nPos ) + return -1; + return p->pPos[iCo].iObj2Box; +} + +/**Function************************************************************* + + Synopsis [Returns the first input of the box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Tim_ManBoxInputFirst( Tim_Man_t * p, int iBox ) +{ + Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox ); + return pBox->Inouts[0]; +} + +/**Function************************************************************* + + Synopsis [Returns the first input of the box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Tim_ManBoxOutputFirst( Tim_Man_t * p, int iBox ) +{ + Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox ); + return pBox->Inouts[pBox->nInputs]; +} + +/**Function************************************************************* + + Synopsis [Returns the first input of the box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Tim_ManBoxInputNum( Tim_Man_t * p, int iBox ) +{ + Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox ); + return pBox->nInputs; +} + +/**Function************************************************************* + + Synopsis [Returns the first input of the box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox ) +{ + Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox ); + return pBox->nOutputs; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h index f1fb992c..f56b0881 100644 --- a/src/aig/tim/tim.h +++ b/src/aig/tim/tim.h @@ -59,6 +59,7 @@ typedef struct Tim_Man_t_ Tim_Man_t; /*=== time.c ===========================================================*/ extern Tim_Man_t * Tim_ManStart( int nPis, int nPos ); extern Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete ); +extern Tim_Man_t * Tim_ManDupUnit( Tim_Man_t * p ); extern void Tim_ManStop( Tim_Man_t * p ); extern void Tim_ManPrint( Tim_Man_t * p ); extern void Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables ); @@ -73,6 +74,12 @@ extern void Tim_ManSetPoRequired( Tim_Man_t * p, int iPo, float Delay extern void Tim_ManSetPoRequiredAll( Tim_Man_t * p, float Delay ); extern float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi ); extern float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo ); +extern int Tim_ManBoxForCi( Tim_Man_t * p, int iCo ); +extern int Tim_ManBoxForCo( Tim_Man_t * p, int iCi ); +extern int Tim_ManBoxInputFirst( Tim_Man_t * p, int iBox ); +extern int Tim_ManBoxOutputFirst( Tim_Man_t * p, int iBox ); +extern int Tim_ManBoxInputNum( Tim_Man_t * p, int iBox ); +extern int Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox ); #ifdef __cplusplus } diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 1d5195c7..7dce5154 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -582,6 +582,7 @@ extern Vec_Ptr_t * Abc_NtkSupport( Abc_Ntk_t * pNtk ); extern Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes ); extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos ); extern Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi ); +extern Vec_Vec_t * Abc_NtkLevelize( Abc_Ntk_t * pNtk ); extern int Abc_NtkLevel( Abc_Ntk_t * pNtk ); extern int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk ); extern bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk ); @@ -612,7 +613,6 @@ extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover ); extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ); extern int Abc_NtkSopToAig( Abc_Ntk_t * pNtk ); extern int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk ); -extern unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst ); extern int Abc_NtkMapToSop( Abc_Ntk_t * pNtk ); extern int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect ); extern int Abc_NtkToBdd( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index 4c6a7fb0..c82faa15 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -978,6 +978,32 @@ int Abc_NtkLevelReverse_rec( Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ +Vec_Vec_t * Abc_NtkLevelize( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + Vec_Vec_t * vLevels; + int nLevels, i; + nLevels = Abc_NtkLevel( pNtk ); + vLevels = Vec_VecStart( nLevels + 1 ); + Abc_NtkForEachNode( pNtk, pObj, i ) + { + assert( (int)pObj->Level <= nLevels ); + Vec_VecPush( vLevels, pObj->Level, pObj ); + } + return vLevels; +} + +/**Function************************************************************* + + Synopsis [Computes the number of logic levels not counting PIs/POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_NtkLevel( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pNode; diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index f3297d8f..e99cc88b 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -785,159 +785,6 @@ DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot ) -/**Function************************************************************* - - Synopsis [Construct BDDs and mark AIG nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_ConvertAigToTruth_rec1( Hop_Obj_t * pObj ) -{ - int Counter = 0; - assert( !Hop_IsComplement(pObj) ); - if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) - return 0; - Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) ); - Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) ); - assert( !Hop_ObjIsMarkA(pObj) ); // loop detection - Hop_ObjSetMarkA( pObj ); - return Counter + 1; -} - -/**Function************************************************************* - - Synopsis [Computes truth table of the cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords ) -{ - unsigned * pTruth, * pTruth0, * pTruth1; - int i; - assert( !Hop_IsComplement(pObj) ); - if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) ) - return pObj->pData; - // compute the truth tables of the fanins - pTruth0 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords ); - pTruth1 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords ); - // creat the truth table of the node - pTruth = Vec_IntFetch( vTruth, nWords ); - if ( Hop_ObjIsExor(pObj) ) - for ( i = 0; i < nWords; i++ ) - pTruth[i] = pTruth0[i] ^ pTruth1[i]; - else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) ) - for ( i = 0; i < nWords; i++ ) - pTruth[i] = pTruth0[i] & pTruth1[i]; - else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) ) - for ( i = 0; i < nWords; i++ ) - pTruth[i] = pTruth0[i] & ~pTruth1[i]; - else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) ) - for ( i = 0; i < nWords; i++ ) - pTruth[i] = ~pTruth0[i] & pTruth1[i]; - else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) ) - for ( i = 0; i < nWords; i++ ) - pTruth[i] = ~pTruth0[i] & ~pTruth1[i]; - assert( Hop_ObjIsMarkA(pObj) ); // loop detection - Hop_ObjClearMarkA( pObj ); - pObj->pData = pTruth; - return pTruth; -} - -/**Function************************************************************* - - Synopsis [Computes truth table of the node.] - - Description [Assumes that the structural support is no more than 8 inputs. - Uses array vTruth to store temporary truth tables. The returned pointer should - be used immediately.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst ) -{ - static unsigned uTruths[8][8] = { // elementary truth tables - { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, - { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, - { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, - { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, - { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, - { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, - { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, - { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } - }; - Hop_Obj_t * pObj; - unsigned * pTruth, * pTruth2; - int i, nWords, nNodes; - Vec_Ptr_t * vTtElems; - - // if the number of variables is more than 8, allocate truth tables - if ( nVars > 8 ) - vTtElems = Vec_PtrAllocTruthTables( nVars ); - else - vTtElems = NULL; - - // clear the data fields and set marks - nNodes = Abc_ConvertAigToTruth_rec1( pRoot ); - // prepare memory - nWords = Hop_TruthWordNum( nVars ); - Vec_IntClear( vTruth ); - Vec_IntGrow( vTruth, nWords * (nNodes+1) ); - pTruth = Vec_IntFetch( vTruth, nWords ); - // check the case of a constant - if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) ) - { - assert( nNodes == 0 ); - if ( Hop_IsComplement(pRoot) ) - Extra_TruthClear( pTruth, nVars ); - else - Extra_TruthFill( pTruth, nVars ); - return pTruth; - } - // set elementary truth tables at the leaves - assert( nVars <= Hop_ManPiNum(p) ); -// assert( Hop_ManPiNum(p) <= 8 ); - if ( fMsbFirst ) - { - Hop_ManForEachPi( p, pObj, i ) - { - if ( vTtElems ) - pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i); - else - pObj->pData = (void *)uTruths[nVars-1-i]; - } - } - else - { - Hop_ManForEachPi( p, pObj, i ) - { - if ( vTtElems ) - pObj->pData = Vec_PtrEntry(vTtElems, i); - else - pObj->pData = (void *)uTruths[i]; - } - } - // clear the marks and compute the truth table - pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords ); - // copy the result - Extra_TruthCopy( pTruth, pTruth2, nVars ); - if ( vTtElems ) - Vec_PtrFree( vTtElems ); - return pTruth; -} - /**Function************************************************************* diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d9c68bc4..65403609 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -205,6 +205,8 @@ static int Abc_CommandAbc8Write ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandAbc8Ps ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8If ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8DChoice ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8ReadLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc8PrintLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Scl ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Lcorr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc8Ssw ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -431,6 +433,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC8", "*ps", Abc_CommandAbc8Ps, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*if", Abc_CommandAbc8If, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*dchoice", Abc_CommandAbc8DChoice, 0 ); + Cmd_CommandAdd( pAbc, "ABC8", "*read_lut", Abc_CommandAbc8ReadLut, 0 ); + Cmd_CommandAdd( pAbc, "ABC8", "*print_lut", Abc_CommandAbc8PrintLut, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*scl", Abc_CommandAbc8Scl, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*lcorr", Abc_CommandAbc8Lcorr, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*ssw", Abc_CommandAbc8Ssw, 0 ); @@ -473,6 +477,11 @@ void Abc_Init( Abc_Frame_t * pAbc ) void Abc_End() { Abc_FrameClearDesign(); + { + extern void If_LutLibFree( void * pLutLib ); + if ( Abc_FrameGetGlobalFrame()->pAbc8Lib ) + If_LutLibFree( Abc_FrameGetGlobalFrame()->pAbc8Lib ); + } // Dar_LibDumpPriorities(); { @@ -1754,7 +1763,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Currently works only for up to 16 inputs.\n" ); return 1; } - pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 ); + pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 ); if ( Hop_IsComplement(pObj->pData) ) Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) ); Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) ); @@ -3387,7 +3396,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nDivMax = 250; pPars->nWinSizeMax = 300; pPars->nGrowthLevel = 0; - pPars->nBTLimit =10000; + pPars->nBTLimit = 5000; pPars->fResub = 1; pPars->fArea = 0; pPars->fMoreEffort = 0; @@ -7073,7 +7082,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); // extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); - extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ); +// extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ); // extern void Abc_NtkDarTestBlif( char * pFileName ); // extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk ); @@ -8111,10 +8120,10 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - int fBalance, fVerbose, fUpdateLevel, c; + int fBalance, fVerbose, fUpdateLevel, fConstruct, c; int nConfMax, nLevelMax; - extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -8123,11 +8132,12 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fBalance = 1; fUpdateLevel = 1; + fConstruct = 0; nConfMax = 1000; nLevelMax = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CLblvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CLblcvh" ) ) != EOF ) { switch ( c ) { @@ -8159,6 +8169,9 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'l': fUpdateLevel ^= 1; break; + case 'c': + fConstruct ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -8178,7 +8191,7 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "This command works only for strashed networks.\n" ); return 1; } - pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose ); + pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -8189,12 +8202,13 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dchoice [-C num] [-L num] [-blvh]\n" ); + fprintf( pErr, "usage: dchoice [-C num] [-L num] [-blcvh]\n" ); fprintf( pErr, "\t performs partitioned choicing using a new AIG package\n" ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax ); fprintf( pErr, "\t-L num : the max level of nodes to consider (0 = not used) [default = %d]\n", nLevelMax ); fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" ); fprintf( pErr, "\t-l : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" ); + fprintf( pErr, "\t-c : toggle constructive computation of choices [default = %s]\n", fConstruct? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -14751,6 +14765,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv ) char * pFileName; int c; extern void Ioa_WriteBlif( void * p, char * pFileName ); + extern int Ntl_ManInsertNtk( void * p, void * pNtk ); // set defaults Extra_UtilGetoptReset(); @@ -14772,6 +14787,17 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the input file name pFileName = argv[globalUtilOptind]; + if ( pAbc->pAbc8Ntk != NULL ) + { + if ( !Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Ntk ) ) + { + printf( "Abc_CommandAbc8Write(): There is no design to write.\n" ); + return 1; + } + printf( "Writing the mapped design.\n" ); + } + else + printf( "Writing the original design.\n" ); Ioa_WriteBlif( pAbc->pAbc8Ntl, pFileName ); return 0; @@ -14797,6 +14823,7 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) { int c; extern void Ntl_ManPrintStats( void * p ); + extern void Ntk_ManPrintStats( void * p, void * pLutLib ); // set defaults Extra_UtilGetoptReset(); @@ -14821,6 +14848,8 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) Ntl_ManPrintStats( pAbc->pAbc8Ntl ); if ( pAbc->pAbc8Aig ) Aig_ManPrintStats( pAbc->pAbc8Aig ); + if ( pAbc->pAbc8Ntk ) + Ntk_ManPrintStats( pAbc->pAbc8Ntk, pAbc->pAbc8Lib ); return 0; usage: @@ -14843,11 +14872,26 @@ usage: ***********************************************************************/ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv ) { + If_Par_t Pars, * pPars = &Pars; + void * pNtkNew; int c; extern int Ntl_ManInsertTest( void * p, Aig_Man_t * pAig ); extern int Ntl_ManInsertTestIf( void * p, Aig_Man_t * pAig ); + extern void * Ntk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars ); + extern Tim_Man_t * Ntl_ManReadTimeMan( void * p ); + extern void * If_SetSimpleLutLib( int nLutSize ); + extern void Ntk_ManSetIfParsDefault( If_Par_t * pPars ); + extern void Ntk_ManFree( void * ); + + if ( pAbc->pAbc8Lib == NULL ) + { + printf( "LUT library is not given. Using defaul 6-LUT library.\n" ); + pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 ); + } // set defaults + Ntk_ManSetIfParsDefault( pPars ); + pPars->pLutLib = pAbc->pAbc8Lib; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { @@ -14864,7 +14908,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc8Write(): There is no AIG to map.\n" ); return 1; } - +/* // get the input file name if ( !Ntl_ManInsertTestIf( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) ) // if ( !Ntl_ManInsertTest( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) ) @@ -14872,6 +14916,16 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc8Write(): Tranformation of the netlist has failed.\n" ); return 1; } +*/ + pNtkNew = Ntk_MappingIf( pAbc->pAbc8Aig, Ntl_ManReadTimeMan(pAbc->pAbc8Ntl), pPars ); + if ( pNtkNew == NULL ) + { + printf( "Abc_CommandAbc8If(): Mapping of the AIG has failed.\n" ); + return 1; + } + if ( pAbc->pAbc8Ntk != NULL ) + Ntk_ManFree( pAbc->pAbc8Ntk ); + pAbc->pAbc8Ntk = pNtkNew; return 0; usage: @@ -14937,6 +14991,138 @@ usage: /**Function************************************************************* + Synopsis [Command procedure to read LUT libraries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc8ReadLut( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + FILE * pFile; + char * FileName; + void * pLib; + int c; + extern void * If_LutLibRead( char * FileName ); + extern void If_LutLibFree( void * pLutLib ); + + // set the defaults + Extra_UtilGetoptReset(); + while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) + { + switch (c) + { + case 'h': + goto usage; + break; + default: + goto usage; + } + } + + + if ( argc != globalUtilOptind + 1 ) + { + goto usage; + } + + // get the input file name + FileName = argv[globalUtilOptind]; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + fprintf( stdout, "Cannot open input file \"%s\". ", FileName ); + if ( FileName = Extra_FileGetSimilarName( FileName, ".lut", NULL, NULL, NULL, NULL ) ) + fprintf( stdout, "Did you mean \"%s\"?", FileName ); + fprintf( stdout, "\n" ); + return 1; + } + fclose( pFile ); + + // set the new network + pLib = If_LutLibRead( FileName ); + if ( pLib == NULL ) + { + fprintf( stdout, "Reading LUT library has failed.\n" ); + goto usage; + } + // replace the current library + if ( pAbc->pAbc8Lib != NULL ) + If_LutLibFree( pAbc->pAbc8Lib ); + pAbc->pAbc8Lib = pLib; + return 0; + +usage: + fprintf( stdout, "\nusage: *read_lut [-h]\n"); + fprintf( stdout, "\t read the LUT library from the file\n" ); + fprintf( stdout, "\t-h : print the command usage\n"); + fprintf( stdout, "\t \n"); + fprintf( stdout, "\t File format for a LUT library:\n"); + fprintf( stdout, "\t (the default library is shown)\n"); + fprintf( stdout, "\t \n"); + fprintf( stdout, "\t # The area/delay of k-variable LUTs:\n"); + fprintf( stdout, "\t # k area delay\n"); + fprintf( stdout, "\t 1 1 1\n"); + fprintf( stdout, "\t 2 2 2\n"); + fprintf( stdout, "\t 3 4 3\n"); + fprintf( stdout, "\t 4 8 4\n"); + fprintf( stdout, "\t 5 16 5\n"); + fprintf( stdout, "\t 6 32 6\n"); + return 1; /* error exit */ +} + +/**Function************************************************************* + + Synopsis [Command procedure to read LUT libraries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc8PrintLut( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + int c; + extern void If_LutLibPrint( void * pLutLib ); + + // set the defaults + Extra_UtilGetoptReset(); + while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) + { + switch (c) + { + case 'h': + goto usage; + break; + default: + goto usage; + } + } + + if ( argc != globalUtilOptind ) + { + goto usage; + } + + // set the new network + if ( pAbc->pAbc8Lib == NULL ) + printf( "LUT library is not specified.\n" ); + else + If_LutLibPrint( pAbc->pAbc8Lib ); + return 0; + +usage: + fprintf( stdout, "\nusage: *print_lut [-h]\n"); + fprintf( stdout, "\t print the current LUT library\n" ); + fprintf( stdout, "\t-h : print the command usage\n"); + return 1; /* error exit */ +} +/**Function************************************************************* + Synopsis [] Description [] diff --git a/src/base/abci/abcBidec.c b/src/base/abci/abcBidec.c index ad332314..bb114578 100644 --- a/src/base/abci/abcBidec.c +++ b/src/base/abci/abcBidec.c @@ -19,15 +19,13 @@ ***********************************************************************/ #include "abc.h" - #include "bdc.h" -#include "bdcInt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) ); } +static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) ); } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -48,24 +46,25 @@ Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pR { unsigned * pTruth; Bdc_Fun_t * pFunc; - int i; + int nNodes, i; assert( nVars <= 16 ); // derive truth table - pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 ); + pTruth = Hop_ManConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 ); if ( Hop_IsComplement(pRoot) ) Extra_TruthNot( pTruth, pTruth, nVars ); // decompose truth table Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 ); // convert back into HOP - Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop ); + Bdc_FuncSetCopy( Bdc_ManFunc( p, 0 ), Hop_ManConst1( pHop ) ); for ( i = 0; i < nVars; i++ ) - Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i ); - for ( i = nVars + 1; i < p->nNodes; i++ ) + Bdc_FuncSetCopy( Bdc_ManFunc( p, i+1 ), Hop_ManPi( pHop, i ) ); + nNodes = Bdc_ManNodeNum(p); + for ( i = nVars + 1; i < nNodes; i++ ) { - pFunc = Bdc_FunWithId( p, i ); - pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) ); + pFunc = Bdc_ManFunc( p, i ); + Bdc_FuncSetCopy( pFunc, Hop_And( pHop, Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) ); } - return Bdc_FunCopyHop(p->pRoot); + return Bdc_FunCopyHop( Bdc_ManRoot(p) ); } /**Function************************************************************* diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 94b6c52b..dd8f8221 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -769,7 +769,7 @@ clk = clock(); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose ) +Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose ) { Aig_Man_t * pMan, * pTemp; Abc_Ntk_t * pNtkAig; @@ -777,7 +777,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; - pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose ); + pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose ); Aig_ManStop( pTemp ); pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); Aig_ManStop( pMan ); @@ -1432,6 +1432,7 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) ***********************************************************************/ void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ) { +/* Aig_Man_t * pMan; pMan = Abc_NtkToDar( pNtk, 1 ); if ( pMan == NULL ) @@ -1442,6 +1443,7 @@ void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ) pMan->vFlopNums = NULL; Aig_ManHaigRecord( pMan ); Aig_ManStop( pMan ); +*/ } /**Function************************************************************* diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 744d9c95..c1e0faf0 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -383,7 +383,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, int fReco extern int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars ); int nVars = Abc_NtkRecVarNum(); Vec_Int_t * vMemory = Abc_NtkRecMemory(); - unsigned * pTruth = Abc_ConvertAigToTruth( pMan, Hop_Regular(pRoot), nVars, vMemory, 0 ); + unsigned * pTruth = Hop_ManConvertAigToTruth( pMan, Hop_Regular(pRoot), nVars, vMemory, 0 ); assert( Extra_TruthSupportSize(pTruth, nVars) == Abc_ObjFaninNum(pNodeOld) ); // should be swept if ( Hop_IsComplement(pRoot) ) Extra_TruthNot( pTruth, pTruth, nVars ); diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c index 4b766a47..df4a6259 100644 --- a/src/base/io/ioWriteBench.c +++ b/src/base/io/ioWriteBench.c @@ -258,7 +258,7 @@ int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth nFanins = Abc_ObjFaninNum(pNode); assert( nFanins <= 8 ); // compute the truth table - pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 ); + pTruth = Hop_ManConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 ); if ( Hop_IsComplement(pNode->pData) ) Extra_TruthNot( pTruth, pTruth, nFanins ); // consider simple cases diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index 0261d7da..7196b952 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -78,6 +78,7 @@ struct Abc_Frame_t_ void * pAbc8Ntl; // the current design void * pAbc8Ntk; // the current mapped network void * pAbc8Aig; // the current AIG + void * pAbc8Lib; // the current LUT library }; //////////////////////////////////////////////////////////////////////// diff --git a/src/map/fpga/fpga.c b/src/map/fpga/fpga.c index 40423f4f..31edf689 100644 --- a/src/map/fpga/fpga.c +++ b/src/map/fpga/fpga.c @@ -146,7 +146,7 @@ int Fpga_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) fclose( pFile ); // set the new network - pLib = Fpga_LutLibCreate( FileName, fVerbose ); + pLib = Fpga_LutLibRead( FileName, fVerbose ); if ( pLib == NULL ) { fprintf( pErr, "Reading LUT library has failed.\n" ); @@ -228,7 +228,7 @@ int Fpga_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; usage: - fprintf( pErr, "\nusage: read_print [-vh]\n"); + fprintf( pErr, "\nusage: print_lut [-vh]\n"); fprintf( pErr, "\t print the current LUT library\n" ); fprintf( pErr, "\t-v : toggles enabling of verbose output [default = %s]\n", (fVerbose? "yes" : "no") ); fprintf( pErr, "\t-h : print the command usage\n"); diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h index be790a55..1e4ac1d4 100644 --- a/src/map/fpga/fpgaInt.h +++ b/src/map/fpga/fpgaInt.h @@ -314,7 +314,7 @@ extern void Fpga_NodeAddFaninFanout( Fpga_Node_t * pFanin, Fpga_Nod extern void Fpga_NodeRemoveFaninFanout( Fpga_Node_t * pFanin, Fpga_Node_t * pFanoutToRemove ); extern int Fpga_NodeGetFanoutNum( Fpga_Node_t * pNode ); /*=== fpgaLib.c ============================================================*/ -extern Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose ); +extern Fpga_LutLib_t * Fpga_LutLibRead( char * FileName, int fVerbose ); extern void Fpga_LutLibFree( Fpga_LutLib_t * p ); extern void Fpga_LutLibPrint( Fpga_LutLib_t * pLutLib ); extern int Fpga_LutLibDelaysAreDiscrete( Fpga_LutLib_t * pLutLib ); diff --git a/src/map/fpga/fpgaLib.c b/src/map/fpga/fpgaLib.c index b1bb4cdc..77fc3a6f 100644 --- a/src/map/fpga/fpgaLib.c +++ b/src/map/fpga/fpgaLib.c @@ -52,7 +52,7 @@ float Fpga_LutLibReadLutArea( Fpga_LutLib_t * p, int Size ) { assert( S SeeAlso [] ***********************************************************************/ -Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose ) +Fpga_LutLib_t * Fpga_LutLibRead( char * FileName, int fVerbose ) { char pBuffer[1000], * pToken; Fpga_LutLib_t * p; diff --git a/src/map/if/if.h b/src/map/if/if.h index d42dd0af..d97a1154 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -245,8 +245,9 @@ static inline If_Obj_t * If_ManObj( If_Man_t * p, int i ) { r static inline int If_ObjIsConst1( If_Obj_t * pObj ) { return pObj->Type == IF_CONST1; } static inline int If_ObjIsCi( If_Obj_t * pObj ) { return pObj->Type == IF_CI; } static inline int If_ObjIsCo( If_Obj_t * pObj ) { return pObj->Type == IF_CO; } -//static inline int If_ObjIsPi( If_Obj_t * pObj ) { return If_ObjIsCi(pObj) && pObj->pFanin0 == NULL; } -static inline int If_ObjIsLatch( If_Obj_t * pObj ) { return If_ObjIsCi(pObj) && pObj->pFanin0 != NULL; } +static inline int If_ObjIsTerm( If_Obj_t * pObj ) { return pObj->Type == IF_CI || pObj->Type == IF_CO; } +//static inline int If_ObjIsPi( If_Obj_t * pObj ) { return If_ObjIsCi(pObj) && pObj->pFanin0 == NULL; } +static inline int If_ObjIsLatch( If_Obj_t * pObj ) { return If_ObjIsCi(pObj) && pObj->pFanin0 != NULL; } static inline int If_ObjIsAnd( If_Obj_t * pObj ) { return pObj->Type == IF_AND; } static inline If_Obj_t * If_ObjFanin0( If_Obj_t * pObj ) { return pObj->pFanin0; } @@ -402,6 +403,8 @@ extern int If_ManCrossCut( If_Man_t * p ); extern Vec_Ptr_t * If_ManReverseOrder( If_Man_t * p ); extern void If_ManMarkMapping( If_Man_t * p ); extern Vec_Ptr_t * If_ManCollectMappingDirect( If_Man_t * p ); +extern Vec_Int_t * If_ManCollectMappingInt( If_Man_t * p ); + extern int If_ManCountSpecialPos( If_Man_t * p ); diff --git a/src/map/if/ifLib.c b/src/map/if/ifLib.c new file mode 100644 index 00000000..2089ca3c --- /dev/null +++ b/src/map/if/ifLib.c @@ -0,0 +1,273 @@ +/**CFile**************************************************************** + + FileName [ifLib.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [FPGA mapping based on priority cuts.] + + Synopsis [LUT library.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 21, 2006.] + + Revision [$Id: ifLib.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "if.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline char * If_UtilStrsav( char *s ) { return !s ? s : strcpy(ALLOC(char, strlen(s)+1), s); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Reads the description of LUTs from the LUT library file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Lib_t * If_LutLibRead( char * FileName ) +{ + char pBuffer[1000], * pToken; + If_Lib_t * p; + FILE * pFile; + int i, k; + + pFile = fopen( FileName, "r" ); + if ( pFile == NULL ) + { + printf( "Cannot open LUT library file \"%s\".\n", FileName ); + return NULL; + } + + p = ALLOC( If_Lib_t, 1 ); + memset( p, 0, sizeof(If_Lib_t) ); + p->pName = If_UtilStrsav( FileName ); + + i = 1; + while ( fgets( pBuffer, 1000, pFile ) != NULL ) + { + pToken = strtok( pBuffer, " \t\n" ); + if ( pToken == NULL ) + continue; + if ( pToken[0] == '#' ) + continue; + if ( i != atoi(pToken) ) + { + printf( "Error in the LUT library file \"%s\".\n", FileName ); + free( p ); + return NULL; + } + + // read area + pToken = strtok( NULL, " \t\n" ); + p->pLutAreas[i] = (float)atof(pToken); + + // read delays + k = 0; + while ( pToken = strtok( NULL, " \t\n" ) ) + p->pLutDelays[i][k++] = (float)atof(pToken); + + // check for out-of-bound + if ( k > i ) + { + printf( "LUT %d has too many pins (%d). Max allowed is %d.\n", i, k, i ); + return NULL; + } + + // check if var delays are specifies + if ( k > 1 ) + p->fVarPinDelays = 1; + + if ( i == IF_MAX_LUTSIZE ) + { + printf( "Skipping LUTs of size more than %d.\n", i ); + return NULL; + } + i++; + } + p->LutMax = i-1; + + // check the library + if ( p->fVarPinDelays ) + { + for ( i = 1; i <= p->LutMax; i++ ) + for ( k = 0; k < i; k++ ) + { + if ( p->pLutDelays[i][k] <= 0.0 ) + printf( "Warning: Pin %d of LUT %d has delay %f. Pin delays should be non-negative numbers. Technology mapping may not work correctly.\n", + k, i, p->pLutDelays[i][k] ); + if ( k && p->pLutDelays[i][k-1] > p->pLutDelays[i][k] ) + printf( "Warning: Pin %d of LUT %d has delay %f. Pin %d of LUT %d has delay %f. Pin delays should be in non-decreasing order. Technology mapping may not work correctly.\n", + k-1, i, p->pLutDelays[i][k-1], + k, i, p->pLutDelays[i][k] ); + } + } + else + { + for ( i = 1; i <= p->LutMax; i++ ) + { + if ( p->pLutDelays[i][0] <= 0.0 ) + printf( "Warning: LUT %d has delay %f. Pin delays should be non-negative numbers. Technology mapping may not work correctly.\n", + k, i, p->pLutDelays[i][0] ); + } + } + + return p; +} + +/**Function************************************************************* + + Synopsis [Duplicates the LUT library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Lib_t * If_LutLibDup( If_Lib_t * p ) +{ + If_Lib_t * pNew; + pNew = ALLOC( If_Lib_t, 1 ); + *pNew = *p; + pNew->pName = If_UtilStrsav( pNew->pName ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Frees the LUT library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_LutLibFree( If_Lib_t * pLutLib ) +{ + if ( pLutLib == NULL ) + return; + FREE( pLutLib->pName ); + FREE( pLutLib ); +} + + +/**Function************************************************************* + + Synopsis [Prints the LUT library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_LutLibPrint( If_Lib_t * pLutLib ) +{ + int i, k; + printf( "# The area/delay of k-variable LUTs:\n" ); + printf( "# k area delay\n" ); + if ( pLutLib->fVarPinDelays ) + { + for ( i = 1; i <= pLutLib->LutMax; i++ ) + { + printf( "%d %7.2f ", i, pLutLib->pLutAreas[i] ); + for ( k = 0; k < i; k++ ) + printf( " %7.2f", pLutLib->pLutDelays[i][k] ); + printf( "\n" ); + } + } + else + for ( i = 1; i <= pLutLib->LutMax; i++ ) + printf( "%d %7.2f %7.2f\n", i, pLutLib->pLutAreas[i], pLutLib->pLutDelays[i][0] ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the delays are discrete.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_LutLibDelaysAreDiscrete( If_Lib_t * pLutLib ) +{ + float Delay; + int i; + for ( i = 1; i <= pLutLib->LutMax; i++ ) + { + Delay = pLutLib->pLutDelays[i][0]; + if ( ((float)((int)Delay)) != Delay ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Sets simple LUT library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Lib_t * If_SetSimpleLutLib( int nLutSize ) +{ + If_Lib_t s_LutLib10= { "lutlib",10, 0, {0,1,1,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1},{1},{1}} }; + If_Lib_t s_LutLib9 = { "lutlib", 9, 0, {0,1,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1},{1}} }; + If_Lib_t s_LutLib8 = { "lutlib", 8, 0, {0,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1}} }; + If_Lib_t s_LutLib7 = { "lutlib", 7, 0, {0,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1}} }; + If_Lib_t s_LutLib6 = { "lutlib", 6, 0, {0,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1}} }; + If_Lib_t s_LutLib5 = { "lutlib", 5, 0, {0,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1}} }; + If_Lib_t s_LutLib4 = { "lutlib", 4, 0, {0,1,1,1,1}, {{0},{1},{1},{1},{1}} }; + If_Lib_t s_LutLib3 = { "lutlib", 3, 0, {0,1,1,1}, {{0},{1},{1},{1}} }; + If_Lib_t * pLutLib; + assert( nLutSize >= 3 && nLutSize <= 10 ); + switch ( nLutSize ) + { + case 3: pLutLib = &s_LutLib3; break; + case 4: pLutLib = &s_LutLib4; break; + case 5: pLutLib = &s_LutLib5; break; + case 6: pLutLib = &s_LutLib6; break; + case 7: pLutLib = &s_LutLib7; break; + case 8: pLutLib = &s_LutLib8; break; + case 9: pLutLib = &s_LutLib9; break; + case 10: pLutLib = &s_LutLib10; break; + default: pLutLib = NULL; break; + } + if ( pLutLib == NULL ) + return NULL; + return If_LutLibDup(pLutLib); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index fafd454d..81521abf 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -295,13 +295,6 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr { arrTime = Tim_ManGetPiArrival( p->pManTim, pObj->IdPio ); If_ObjSetArrTime( pObj, arrTime ); -/* - if ( pObj->IdPio >= 2000 ) - { - int x = 0; - printf( "+%d %6.3f ", pObj->IdPio, arrTime ); - } -*/ } else if ( If_ObjIsCo(pObj) ) { diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c index c114236d..74880409 100644 --- a/src/map/if/ifUtil.c +++ b/src/map/if/ifUtil.c @@ -653,6 +653,40 @@ Vec_Ptr_t * If_ManCollectMappingDirect( If_Man_t * p ) /**Function************************************************************* + Synopsis [Collects nodes used in the mapping in the topological order.] + + Description [Represents mapping as an array of integers.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * If_ManCollectMappingInt( If_Man_t * p ) +{ + Vec_Int_t * vOrder; + If_Cut_t * pCutBest; + If_Obj_t * pObj; + int i, k, nLeaves, * ppLeaves; + If_ManMarkMapping( p ); + vOrder = Vec_IntAlloc( If_ManObjNum(p) ); + If_ManForEachObj( p, pObj, i ) + if ( If_ObjIsAnd(pObj) && pObj->nRefs ) + { + pCutBest = If_ObjCutBest( pObj ); + nLeaves = If_CutLeaveNum( pCutBest ); + ppLeaves = If_CutLeaves( pCutBest ); + // save the number of leaves, the leaves, and finally, the root + Vec_IntPush( vOrder, nLeaves ); + for ( k = 0; k < nLeaves; k++ ) + Vec_IntPush( vOrder, ppLeaves[k] ); + Vec_IntPush( vOrder, pObj->Id ); + } + return vOrder; +} + +/**Function************************************************************* + Synopsis [Returns the number of POs pointing to the same internal nodes.] Description [] diff --git a/src/map/if/module.make b/src/map/if/module.make index c14428da..7489d3b4 100644 --- a/src/map/if/module.make +++ b/src/map/if/module.make @@ -1,5 +1,6 @@ SRC += src/map/if/ifCore.c \ src/map/if/ifCut.c \ + src/map/if/ifLib.c \ src/map/if/ifMan.c \ src/map/if/ifMap.c \ src/map/if/ifReduce.c \ diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make deleted file mode 100644 index e69de29b..00000000 --- a/src/map/pcm/module.make +++ /dev/null diff --git a/src/map/ply/module.make b/src/map/ply/module.make deleted file mode 100644 index e69de29b..00000000 --- a/src/map/ply/module.make +++ /dev/null diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 59ee7488..2a2c9d43 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -101,6 +101,7 @@ p->timeSat += clock() - clk; int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) { Hop_Obj_t * pObj; + int RetValue; extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare ); int nGain, clk; @@ -129,8 +130,15 @@ clk = clock(); if ( p->pSat == NULL ) return 0; // solve the SAT problem - Abc_NtkMfsSolveSat( p, pNode ); + RetValue = Abc_NtkMfsSolveSat( p, pNode ); + p->nTotConfLevel += p->pSat->stats.conflicts; p->timeSat += clock() - clk; + if ( RetValue == 0 ) + { + p->nTimeOutsLevel++; + p->nTimeOuts++; + return 0; + } // minimize the local function of the node using bi-decomposition assert( p->nFanins == Abc_ObjFaninNum(pNode) ); pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare ); @@ -139,6 +147,7 @@ p->timeSat += clock() - clk; { p->nNodesDec++; p->nNodesGained += nGain; + p->nNodesGainedLevel += nGain; pNode->pData = pObj; } return 1; @@ -163,7 +172,9 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) ProgressBar * pProgress; Mfs_Man_t * p; Abc_Obj_t * pObj; - int i, nFaninMax, clk = clock(); + Vec_Vec_t * vLevels; + Vec_Ptr_t * vNodes; + int i, k, nNodes, nFaninMax, clk = clock(), clk2; int nTotalNodesBeg = Abc_NtkNodeNum(pNtk); int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk); @@ -223,24 +234,44 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel ); // compute don't-cares for each node + nNodes = 0; p->nTotalNodesBeg = nTotalNodesBeg; p->nTotalEdgesBeg = nTotalEdgesBeg; - pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) ); - Abc_NtkForEachNode( pNtk, pObj, i ) + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) ); + vLevels = Abc_NtkLevelize( pNtk ); + Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 ) { - if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax ) - continue; - if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX ) - continue; if ( !p->pPars->fVeryVerbose ) - Extra_ProgressBarUpdate( pProgress, i, NULL ); - if ( pPars->fResub ) - Abc_NtkMfsResub( p, pObj ); - else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 ) - Abc_NtkMfsNode( p, pObj ); + Extra_ProgressBarUpdate( pProgress, nNodes, NULL ); + p->nNodesGainedLevel = 0; + p->nTotConfLevel = 0; + p->nTimeOutsLevel = 0; + clk2 = clock(); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax ) + break; + if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX ) + continue; + if ( pPars->fResub ) + Abc_NtkMfsResub( p, pObj ); + else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 ) + Abc_NtkMfsNode( p, pObj ); + } + nNodes += Vec_PtrSize(vNodes); + if ( pPars->fVerbose ) + { + printf( "Lev = %2d. Node = %4d. Ave gain = %6.2f. Ave conf = %6.2f. Timeouts = %6.2f %% ", + k, Vec_PtrSize(vNodes), + 1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes), + 1.0*p->nTotConfLevel/Vec_PtrSize(vNodes), + 100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) ); + PRT( "Time", clock() - clk2 ); + } } Extra_ProgressBarStop( pProgress ); Abc_NtkStopReverseLevels( pNtk ); + Vec_VecFree( vLevels ); // perform the sweeping if ( !pPars->fResub ) diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index f4da45ef..37521189 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -70,6 +70,7 @@ struct Mfs_Man_t_ Bdc_Man_t * pManDec; int nNodesDec; int nNodesGained; + int nNodesGainedLevel; // solving data Aig_Man_t * pAigWin; // window AIG with constraints Cnf_Dat_t * pCnf; // the CNF for the window @@ -78,6 +79,8 @@ struct Mfs_Man_t_ Vec_Int_t * vMem; // memory for intermediate SOPs Vec_Vec_t * vLevels; // levelized structure for updating Vec_Ptr_t * vFanins; // the new set of fanins + int nTotConfLim; // total conflict limit + int nTotConfLevel; // total conflicts on this level // the result of solving int nFanins; // the number of fanins int nWords; // the number of words @@ -91,6 +94,7 @@ struct Mfs_Man_t_ int nNodesBad; int nTotalDivs; int nTimeOuts; + int nTimeOutsLevel; int nDcMints; double dTotalRatios; // node/edge stats @@ -136,7 +140,7 @@ extern int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode extern int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode ); extern int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsSat.c ==========================================================*/ -extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ); +extern int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsStrash.c ==========================================================*/ extern Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ); extern double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode ); diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index f1b3f44c..d0642368 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -126,13 +126,13 @@ void Mfs_ManPrint( Mfs_Man_t * p ) } else { - printf( "Nodes = %d. DC mints in local space = %d. Total mints = %d. Ratio = %5.2f.\n", - p->nNodesTried, p->nMintsTotal-p->nMintsCare, p->nMintsTotal, + printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n", + Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare, 1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal ); // printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", // 1.0-(p->dTotalRatios/p->nNodesTried) ); - printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d.\n", - p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained ); + printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d. Timeouts = %d.\n", + p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts ); } /* PRTP( "Win", p->timeWin , p->timeTotal ); diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c index 2529e207..5023bf62 100644 --- a/src/opt/mfs/mfsSat.c +++ b/src/opt/mfs/mfsSat.c @@ -42,9 +42,14 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) { int Lits[MFS_FANIN_MAX]; - int RetValue, iVar, b, Mint; - RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); - assert( RetValue == l_False || RetValue == l_True ); + int RetValue, nBTLimit, iVar, b, Mint; + if ( p->nTotConfLim && p->nTotConfLim <= p->pSat->stats.conflicts ) + return -1; + nBTLimit = p->nTotConfLim? p->nTotConfLim - p->pSat->stats.conflicts : 0; + RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + assert( RetValue == l_Undef || RetValue == l_True || RetValue == l_False ); + if ( RetValue == l_Undef ) + return -1; if ( RetValue == l_False ) return 0; p->nCares++; @@ -77,12 +82,12 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) SideEffects [] SeeAlso [] - + ***********************************************************************/ -void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) +int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) { Aig_Obj_t * pObjPo; - int i; + int RetValue, i; // collect projection variables Vec_IntClear( p->vProjVars ); Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) ) @@ -98,7 +103,10 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) // iterate through the SAT assignments p->nCares = 0; - while ( Abc_NtkMfsSolveSat_iter(p) ); + p->nTotConfLim = p->pPars->nBTLimit; + while ( (RetValue = Abc_NtkMfsSolveSat_iter(p)) == 1 ); + if ( RetValue == -1 ) + return 0; // write statistics p->nMintsCare += p->nCares; @@ -113,7 +121,7 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) // map the care if ( p->nFanins > 4 ) - return; + return 1; if ( p->nFanins == 4 ) p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16); if ( p->nFanins == 3 ) @@ -122,6 +130,7 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) p->uCare[0] = p->uCare[0] | (p->uCare[0] << 4) | (p->uCare[0] << 8) | (p->uCare[0] << 12) | (p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28); assert( p->nFanins != 1 ); + return 1; } //////////////////////////////////////////////////////////////////////// |